From 86bbf67fb357af70820ef069d1c299096e5202d1 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Wed, 17 Jan 2024 14:06:18 -0500 Subject: [PATCH 1/4] Allow building with GHC 9.8 This patch contains a variety of fixes needed to build the libraries in the what4 repo with GHC 9.8: * Bump the upper version bounds on `base` and `text` to allow building with the versions that are bundled with GHC 9.8 (`base-4.19.*` and `text-2.1.*`, respectively). * Replace uses of `head` and `tail` (which trigger `-Wx-partial` warnings with GHC 9.8) with total functions or `panic`s, depending on what is appropriate. * Bump the `aig` submodule to bring in the changes from GaloisInc/aig#16 and GaloisInc/aig#17. --- dependencies/aig | 2 +- what4-abc/what4-abc.cabal | 2 +- what4-blt/what4-blt.cabal | 2 +- .../what4-transition-system.cabal | 2 +- what4/src/What4/Protocol/SMTLib2.hs | 49 +++++++++++++++++-- what4/test/AdapterTest.hs | 10 +++- what4/test/ConfigTest.hs | 4 +- what4/test/ProbeSolvers.hs | 4 +- 8 files changed, 63 insertions(+), 12 deletions(-) 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..c861e17b 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 @@ -1194,8 +1196,24 @@ parseExpr sym sexp = case sexp of 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) + LeftAssoc -> + case List.uncons operands of + Just (operandHead, operandTail) -> + parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) operandHead operandTail + Nothing -> + panic "parseExpr" [ "Left-associative operator" + , Text.unpack operator + , "with empty list of operands" + ] + RightAssoc -> + case unsnoc operands of + Just (operandInit, operandLast) -> + parseExpr sym $ foldr' (\arg acc -> SApp [SAtom operator, arg, acc]) operandLast operandInit + Nothing -> + panic "parseExpr" [ "Right-associative operator" + , Text.unpack operator + , "with empty list of operands" + ] Just (Op1 arg_types fn) -> do args <- mapM (parseExpr sym) operands exprAssignment arg_types args >>= \case @@ -1236,6 +1254,27 @@ parseExpr sym sexp = case sexp of (show n) _ -> throwError "" _ -> throwError "" + +-- | \(\mathcal{O}(n)\). Decompose a list into 'init' and 'last'. +-- +-- * If the list is empty, returns 'Nothing'. +-- * If the list is non-empty, returns @'Just' (xs, x)@, +-- where @xs@ is the 'init'ial part of the list and @x@ is its 'last' element. +-- +-- +-- 'unsnoc' is dual to 'List.uncons': for a finite list @xs@ +-- +-- > unsnoc xs = (\(hd, tl) -> (reverse tl, hd)) <$> uncons (reverse xs) +-- +-- This is the same implementation that was introduced to "Data.List" in +-- @base-4.19.0.0@, but backported to support older versions of @base@. +unsnoc :: [a] -> Maybe ([a], a) +-- The lazy pattern ~(a, b) is important to be productive on infinite lists +-- and not to be prone to stack overflows. +-- Expressing the recursion via 'foldr' provides for list fusion. +unsnoc = foldr (\x -> Just . maybe ([], x) (\(~(a, b)) -> (x : a, b))) Nothing +{-# INLINABLE unsnoc #-} + -- | Verify a list of arguments has a single argument and -- return it, else raise an error. readOneArg :: @@ -1360,8 +1399,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 From 4a25bc23321400bc89337230c76c40dcd81a7320 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 26 Feb 2024 09:21:33 -0500 Subject: [PATCH 2/4] CI: Test GHC 9.8.1 --- .github/workflows/gen_matrix.pl | 1 + .github/workflows/test.yml | 1 + 2 files changed, 2 insertions(+) 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 From 11309c4843bf50c088a0bbc1064903910609f288 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 4 Mar 2024 12:46:49 -0500 Subject: [PATCH 3/4] Comment the `length operands > 2` case --- what4/src/What4/Protocol/SMTLib2.hs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index c861e17b..7f240359 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -1193,6 +1193,16 @@ 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 From 33f95836cd0c6bc0a544597a6023939b7579eda5 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 4 Mar 2024 13:56:20 -0500 Subject: [PATCH 4/4] Refactor code to avoid needing unsnoc The previous code, defined in terms of `unsnoc`, required multiple `panic` cases, which was somewhat unsightly. This new implementation is functionally equivalent, does not require any `panic` fall-through cases, and is much nicer to look at. --- what4/src/What4/Protocol/SMTLib2.hs | 54 ++++++++--------------------- 1 file changed, 14 insertions(+), 40 deletions(-) diff --git a/what4/src/What4/Protocol/SMTLib2.hs b/what4/src/What4/Protocol/SMTLib2.hs index 7f240359..aba17498 100644 --- a/what4/src/What4/Protocol/SMTLib2.hs +++ b/what4/src/What4/Protocol/SMTLib2.hs @@ -1204,26 +1204,20 @@ parseExpr sym sexp = case sexp of -- 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 -> - case List.uncons operands of - Just (operandHead, operandTail) -> - parseExpr sym $ foldl' (\acc arg -> SApp [SAtom operator, acc, arg]) operandHead operandTail - Nothing -> - panic "parseExpr" [ "Left-associative operator" - , Text.unpack operator - , "with empty list of operands" - ] - RightAssoc -> - case unsnoc operands of - Just (operandInit, operandLast) -> - parseExpr sym $ foldr' (\arg acc -> SApp [SAtom operator, arg, acc]) operandLast operandInit - Nothing -> - panic "parseExpr" [ "Right-associative operator" - , Text.unpack operator - , "with empty list of 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 @@ -1265,26 +1259,6 @@ parseExpr sym sexp = case sexp of _ -> throwError "" _ -> throwError "" --- | \(\mathcal{O}(n)\). Decompose a list into 'init' and 'last'. --- --- * If the list is empty, returns 'Nothing'. --- * If the list is non-empty, returns @'Just' (xs, x)@, --- where @xs@ is the 'init'ial part of the list and @x@ is its 'last' element. --- --- --- 'unsnoc' is dual to 'List.uncons': for a finite list @xs@ --- --- > unsnoc xs = (\(hd, tl) -> (reverse tl, hd)) <$> uncons (reverse xs) --- --- This is the same implementation that was introduced to "Data.List" in --- @base-4.19.0.0@, but backported to support older versions of @base@. -unsnoc :: [a] -> Maybe ([a], a) --- The lazy pattern ~(a, b) is important to be productive on infinite lists --- and not to be prone to stack overflows. --- Expressing the recursion via 'foldr' provides for list fusion. -unsnoc = foldr (\x -> Just . maybe ([], x) (\(~(a, b)) -> (x : a, b))) Nothing -{-# INLINABLE unsnoc #-} - -- | Verify a list of arguments has a single argument and -- return it, else raise an error. readOneArg ::