diff --git a/.github/workflows/gen_matrix.pl b/.github/workflows/gen_matrix.pl index 8cb6139b..7c2ebf41 100644 --- a/.github/workflows/gen_matrix.pl +++ b/.github/workflows/gen_matrix.pl @@ -94,6 +94,7 @@ version(ubuntu, "ubuntu-latest"). +version(ghc, "9.8.1"). version(ghc, "9.6.2"). version(ghc, "9.4.4"). version(ghc, "9.2.2"). diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index dbf8cb8e..c56294d3 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -105,6 +105,7 @@ jobs: 9.2.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-22.05 ;; 9.4.4) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;; 9.6.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;; + 9.8.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.11 ;; *) GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;; esac echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV diff --git a/dependencies/aig b/dependencies/aig index 718fcd73..372d5336 160000 --- a/dependencies/aig +++ b/dependencies/aig @@ -1 +1 @@ -Subproject commit 718fcd738b6b44b8615916a7f30a4f2b7bc19795 +Subproject commit 372d533621b24ffdc7e911b92f66ddb0fdc361a9 diff --git a/what4-abc/what4-abc.cabal b/what4-abc/what4-abc.cabal index 4b9bc6a2..fd2135c6 100644 --- a/what4-abc/what4-abc.cabal +++ b/what4-abc/what4-abc.cabal @@ -17,7 +17,7 @@ Description: library build-depends: - base >= 4.7 && < 4.19, + base >= 4.7 && < 4.20, aig, abcBridge >= 0.11, bv-sized >= 1.0.0, diff --git a/what4-blt/what4-blt.cabal b/what4-blt/what4-blt.cabal index a81301c5..a1b82f71 100644 --- a/what4-blt/what4-blt.cabal +++ b/what4-blt/what4-blt.cabal @@ -26,7 +26,7 @@ common bldflags library import: bldflags build-depends: - base >= 4.7 && < 4.19, + base >= 4.7 && < 4.20, blt >= 0.12.1, containers, what4 >= 0.4, diff --git a/what4-transition-system/what4-transition-system.cabal b/what4-transition-system/what4-transition-system.cabal index 624ee5d1..265b061c 100644 --- a/what4-transition-system/what4-transition-system.cabal +++ b/what4-transition-system/what4-transition-system.cabal @@ -13,7 +13,7 @@ build-type: Simple common dependencies build-depends: , ansi-wl-pprint ^>=0.6 - , base >=4.12 && <4.19 + , base >=4.12 && <4.20 , bytestring , containers ^>=0.6 , io-streams diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index 16b1a60b..aba17498 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -112,6 +112,7 @@ import Data.Foldable import Data.HashMap.Lazy (HashMap) import qualified Data.HashMap.Lazy as HashMap import Data.IORef +import qualified Data.List as List import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map import Data.Monoid @@ -152,6 +153,7 @@ import qualified What4.Config as CFG import qualified What4.Expr.Builder as B import What4.Expr.GroundEval import qualified What4.Interface as I +import What4.Panic import What4.ProblemFeatures import What4.Protocol.Online import What4.Protocol.ReadDecimal @@ -1191,11 +1193,31 @@ parseExpr sym sexp = case sexp of liftIO $ Some <$> I.bvSelect sym j_repr n_repr arg_expr _ -> throwError "" SApp ((SAtom operator) : operands) -> case HashMap.lookup operator (opTable @sym) of + -- Sometimes, binary operators can be applied to more than two operands, + -- e.g., (+ 1 2 3 4). We want to uniformly represent binary operators such + -- that they are always applied to two operands, so this case converts the + -- expression above to: + -- + -- - (+ (+ (+ 1 2) 3) 4) (if + is left-associative) + -- - (+ 1 (+ 2 (+ 3 4))) (if + is right-associative) + -- + -- We then call `parseExpr` and recurse, which will reach one of the cases + -- below. Just op - | Just assoc <- opAssoc op - , length operands > 2 -> case assoc of - LeftAssoc -> parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) (head operands) (tail operands) - RightAssoc -> parseExpr sym $ foldr' (\arg acc -> SApp [SAtom operator, arg, acc]) (last operands) (init operands) + | Just LeftAssoc <- opAssoc op + , op1:op2:op3:ops <- operands -> + parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) op1 (op2:op3:ops) + + -- For right-associative operators, we could alternatively call + -- init/last on the list of operands and call foldr on the results. The + -- downside, however, is that init/last are partial functions. To avoid + -- this partiality, we instead match on `reverse operands` and call + -- foldl on the results (with the order of acc/arg swapped). This + -- achieves the same end result and maintains the same asymptotic + -- complexity as using init/tail. + | Just RightAssoc <- opAssoc op + , op1:op2:op3:ops <- List.reverse operands -> + parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, arg, acc]) op1 (op2:op3:ops) Just (Op1 arg_types fn) -> do args <- mapM (parseExpr sym) operands exprAssignment arg_types args >>= \case @@ -1236,6 +1258,7 @@ parseExpr sym sexp = case sexp of (show n) _ -> throwError "" _ -> throwError "" + -- | Verify a list of arguments has a single argument and -- return it, else raise an error. readOneArg :: @@ -1360,8 +1383,10 @@ instance SMTLib2Tweaks a => SMTReadWriter (Writer a) where AckUnsat -> Just $ Unsat () AckUnknown -> Just Unknown _ -> Nothing - in getLimitedSolverResponse "sat result" satRsp s - (head $ reverse $ checkCommands p) + cmd = case reverse $ checkCommands p of + cmd':_ -> cmd' + [] -> panic "smtSatResult" ["Empty list of checkCommands"] + in getLimitedSolverResponse "sat result" satRsp s cmd smtUnsatAssumptionsResult p s = let unsatAssumpRsp = \case diff --git a/what4/test/AdapterTest.hs b/what4/test/AdapterTest.hs index 9cec1d90..61b2d996 100644 --- a/what4/test/AdapterTest.hs +++ b/what4/test/AdapterTest.hs @@ -34,6 +34,7 @@ import Data.Parameterized.Some import What4.Config import What4.Expr import What4.Interface +import What4.Panic import What4.Protocol.SMTLib2.Response ( strictSMTParsing ) import What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness(..) ) import What4.Protocol.VerilogWriter @@ -224,6 +225,11 @@ mkConfigTests adapters = in fmap mkPCTest adaptrs deprecatedConfigTests adaptrs = + let firstAdapter adptrs = + case adptrs of + adptr:_ -> adptr + [] -> panic "deprecatedConfigTests" ["Empty list of adapters"] + in [ testCaseSteps "deprecated default_solver is equivalent to solver.default" $ @@ -258,7 +264,7 @@ mkConfigTests adapters = step "Update the value via regular (text identification)" res2 <- try $ setUnicodeOpt settera $ - pack $ solver_adapter_name $ head adaptrs + pack $ solver_adapter_name $ firstAdapter adaptrs case res2 of Right warns -> fmap show warns @?= [] Left (SomeException e) -> assertFailure $ show e @@ -283,7 +289,7 @@ mkConfigTests adapters = step "Reset to original value" res4 <- try $ setOpt settera' $ - pack $ solver_adapter_name $ head adaptrs + pack $ solver_adapter_name $ firstAdapter adaptrs case res4 of Right warns -> fmap show warns @?= [] Left (SomeException e) -> assertFailure $ show e diff --git a/what4/test/ConfigTest.hs b/what4/test/ConfigTest.hs index 1d71acb9..8667d8bd 100644 --- a/what4/test/ConfigTest.hs +++ b/what4/test/ConfigTest.hs @@ -471,10 +471,12 @@ testHelp = withChecklist "builtins" $ do cfg <- initialConfig 0 [] help <- configHelp "" cfg + let nonEmptyOr :: (a -> b) -> b -> [a] -> b + nonEmptyOr f = foldr (\h _ -> f h) help `checkValues` (Empty :> Val "num" length 1 - :> Val "verbosity" (L.isInfixOf "verbosity =" . show . head) True + :> Val "verbosity" (nonEmptyOr (L.isInfixOf "verbosity =" . show) False) True ) diff --git a/what4/test/ProbeSolvers.hs b/what4/test/ProbeSolvers.hs index 8b898c51..05eabbdc 100644 --- a/what4/test/ProbeSolvers.hs +++ b/what4/test/ProbeSolvers.hs @@ -27,7 +27,9 @@ getSolverVersion (SolverName solver) = if r == ExitSuccess then let ol = lines o in return $ Right $ SolverVersion - $ if null ol then (solver <> " v??") else head ol + $ case ol of + [] -> solver <> " v??" + olh:_ -> olh else return $ Left $ solver <> " version error: " <> show r <> " /;/ " <> e Left (err :: SomeException) -> return $ Left $ solver <> " invocation error: " <> show err