what4 1.6 → 1.6.1
raw patch · 6 files changed
+107/−32 lines, 6 files
Files
- CHANGES.md +9/−0
- src/What4/Expr/GroundEval.hs +36/−0
- src/What4/Solver/CVC4.hs +8/−0
- src/What4/Solver/CVC5.hs +0/−8
- test/ExprBuilderSMTLib2.hs +53/−23
- what4.cabal +1/−1
CHANGES.md view
@@ -1,3 +1,12 @@+# 1.6.1 (Sep 2024)++* Fix a bug in which `what4`'s CVC5 adapter would fail to parse models+ involving structs. ([#265](https://github.com/GaloisInc/what4/issues/265))++* Add `What4.Expr.GroundEval.groundToSym`, which allows injecting+ `GroundValue`s back into `SymExpr`s.+ ([#268](https://github.com/GaloisInc/what4/pull/268))+ # 1.6 (May 2024) * Allow building with GHC 9.8.
src/What4/Expr/GroundEval.hs view
@@ -25,6 +25,7 @@ ( -- * Ground evaluation GroundValue , GroundValueWrapper(..)+ , groundToSym , GroundArray(..) , lookupArray , GroundEvalFn(..)@@ -82,6 +83,41 @@ GroundValue (BaseStringType si) = StringLiteral si GroundValue (BaseArrayType idx b) = GroundArray idx b GroundValue (BaseStructType ctx) = Ctx.Assignment GroundValueWrapper ctx++-- | Inject a 'GroundValue' back into a 'SymExpr'.+--+-- c.f. 'What4.Interface.concreteToSym'.+groundToSym ::+ IsExprBuilder sym =>+ sym ->+ BaseTypeRepr tp ->+ GroundValue tp ->+ IO (SymExpr sym tp)+groundToSym sym tpr val =+ case tpr of+ BaseBoolRepr -> pure (if val then truePred sym else falsePred sym)+ BaseBVRepr w -> bvLit sym w val+ BaseIntegerRepr -> intLit sym val+ BaseRealRepr -> realLit sym val+ BaseFloatRepr fpp -> floatLit sym fpp val+ BaseStringRepr _ -> stringLit sym val+ BaseComplexRepr -> mkComplexLit sym val+ BaseStructRepr tps ->+ mkStruct sym =<< Ctx.zipWithM (\tp (GVW gv) -> groundToSym sym tp gv) tps val+ BaseArrayRepr idxTy tpr' ->+ case val of+ ArrayConcrete def xs0 -> do+ def' <- groundToSym sym tpr' def+ arr <- constantArray sym idxTy def'+ go (Map.toAscList xs0) arr+ ArrayMapping _ -> fail "Can't evaluate `groundToSym` on `ArrayMapping`"+ where+ go [] arr = return arr+ go ((i, x) : xs) arr =+ do arr' <- go xs arr+ i' <- traverseFC (indexLit sym) i+ x' <- groundToSym sym tpr' x+ arrayUpdate sym arr' i' x' -- | A function that calculates ground values for elements. -- Clients of solvers should use the @groundEval@ function for computing
src/What4/Solver/CVC4.hs view
@@ -131,6 +131,14 @@ smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i) smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i) + -- CVC4's support for user-defined datatypes is somewhat buggy (see+ -- https://github.com/cvc5/cvc5/issues/3402). Instead of using user-defined+ -- datatypes to encode What4 structs, we instead use CVC4's built-in Tuple+ -- datatype, which does not suffer from this bug. We use the Tuple syntax+ -- described in https://cvc4.github.io/datatypes.html#tuples.+ --+ -- Note that this bug has been fixed in CVC5, so we do not apply the same+ -- workaround in What4.Solver.CVC5. smtlib2declareStructCmd _ = Nothing smtlib2StructSort [] = Syntax.varSort "Tuple" smtlib2StructSort tps = Syntax.Sort $ "(Tuple" <> foldMap f tps <> ")"
src/What4/Solver/CVC5.hs view
@@ -125,14 +125,6 @@ smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i) smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i) - smtlib2declareStructCmd _ = Nothing- smtlib2StructSort [] = Syntax.varSort "Tuple"- smtlib2StructSort tps = Syntax.Sort $ "(Tuple" <> foldMap f tps <> ")"- where f x = " " <> Syntax.unSort x-- smtlib2StructCtor args = Syntax.term_app "mkTuple" args- smtlib2StructProj _n i x = Syntax.term_app (Syntax.builder_list ["_", "tupSel", fromString (show i)]) [ x ]- cvc5Features :: ProblemFeatures cvc5Features = useComputableReals .|. useIntegerArithmetic
test/ExprBuilderSMTLib2.hs view
@@ -53,6 +53,7 @@ import What4.SatResult import What4.Solver.Adapter import qualified What4.Solver.CVC4 as CVC4+import qualified What4.Solver.CVC5 as CVC5 import qualified What4.Solver.Z3 as Z3 import qualified What4.Solver.Yices as Yices import qualified What4.Utils.BVDomain as WUB@@ -114,6 +115,8 @@ (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h)) (\(_,s) -> action sym s) +data CVC = CVC4 | CVC5 deriving (Eq, Show)+ withCVC4 :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer CVC4.CVC4) -> IO a) -> IO a@@ -126,6 +129,18 @@ (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h)) (\(_,s) -> action sym s) +withCVC5+ :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer CVC5.CVC5) -> IO a)+ -> IO a+withCVC5 action = withSym FloatRealRepr $ \sym -> do+ extendConfig CVC5.cvc5Options (getConfiguration sym)+ bracket+ (do h <- if debugOutputFiles then Just <$> openFile "cvc5.out" WriteMode else return Nothing+ s <- startSolverProcess (defaultFeatures CVC5.CVC5) h sym+ return (h,s))+ (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))+ (\(_,s) -> action sym s)+ withModel :: Session t Z3.Z3 -> BoolExpr t@@ -1068,8 +1083,8 @@ let idx = Ctx.Empty Ctx.:> idxInt let arrLookup = arrayLookup sym arr idx elt <- arrLookup- bvZero <- bvZero sym w- p <- bvEq sym elt bvZero+ zeroBV <- bvZero sym w+ p <- bvEq sym elt zeroBV checkSatisfiableWithModel solver "test" p $ \case Sat fn ->@@ -1246,38 +1261,54 @@ , arraySetTest , arrayCopySetTest ]- let cvc4Tests =- let skipPre1_8 why =- let shouldSkip = case lookup (SolverName "cvc4") solvers of+ let cvcTests cvc =+ let cvcTestCase name assertion = testCase (show cvc ++ " " ++ name) assertion+ skipPre1_8CVC4 why =+ let shouldSkip = cvc == CVC4 && case lookup (SolverName "cvc4") solvers of Just (SolverVersion v) -> any (`elem` [ "1.7" ]) $ words v Nothing -> True in if shouldSkip then expectFailBecause why else id unsuppStrings = "unicode and string escaping not supported for older CVC4 versions; upgrade to at least 1.8"+ ignoreCVC4TestBecause reason =+ if cvc == CVC4 then ignoreTestBecause reason else id++ withCVC ::+ (forall t solver. OnlineSolver solver+ => SimpleExprBuilder t (Flags FloatReal)+ -> SolverProcess t solver+ -> IO a)+ -> IO a+ withCVC k =+ case cvc of+ CVC4 -> withCVC4 k+ CVC5 -> withCVC5 k in [- ignoreTestBecause "This test stalls the solver for some reason; line-buffering issue?" $- testCase "CVC4 0-tuple" $ withCVC4 zeroTupleTest- , testCase "CVC4 1-tuple" $ withCVC4 oneTupleTest- , testCase "CVC4 pair" $ withCVC4 pairTest- , testCase "CVC4 forall binder" $ withCVC4 forallTest+ ignoreCVC4TestBecause "This test stalls the solver for some reason; line-buffering issue?" $+ cvcTestCase "0-tuple" $ withCVC zeroTupleTest+ , cvcTestCase "1-tuple" $ withCVC oneTupleTest+ , cvcTestCase "pair" $ withCVC pairTest+ , cvcTestCase "forall binder" $ withCVC forallTest - , testCase "CVC4 string1" $ withCVC4 stringTest1- , testCase "CVC4 string2" $ withCVC4 stringTest2- , skipPre1_8 unsuppStrings $ testCase "CVC4 string3" $ withCVC4 stringTest3- , testCase "CVC4 string4" $ withCVC4 stringTest4- , testCase "CVC4 string5" $ withCVC4 stringTest5- , skipPre1_8 unsuppStrings $ testCase "CVC4 string6" $ withCVC4 stringTest6- , testCase "CVC4 string7" $ withCVC4 stringTest7+ , cvcTestCase "string1" $ withCVC stringTest1+ , cvcTestCase "string2" $ withCVC stringTest2+ , skipPre1_8CVC4 unsuppStrings $ cvcTestCase "string3" $ withCVC stringTest3+ , cvcTestCase "string4" $ withCVC stringTest4+ , cvcTestCase "string5" $ withCVC stringTest5+ , skipPre1_8CVC4 unsuppStrings $ cvcTestCase "string6" $ withCVC stringTest6+ , cvcTestCase "string7" $ withCVC stringTest7 - , testCase "CVC4 binder tuple1" $ withCVC4 binderTupleTest1- , testCase "CVC4 binder tuple2" $ withCVC4 binderTupleTest2+ , cvcTestCase "binder tuple1" $ withCVC binderTupleTest1+ , cvcTestCase "binder tuple2" $ withCVC binderTupleTest2 - , testCase "CVC4 rounding" $ withCVC4 roundingTest+ , cvcTestCase "rounding" $ withCVC roundingTest - , testCase "CVC4 multidim array"$ withCVC4 multidimArrayTest+ , cvcTestCase "multidim array"$ withCVC multidimArrayTest - , testCase "CVC4 #182 test case" $ withCVC4 issue182Test+ , cvcTestCase "#182 test case" $ withCVC issue182Test ]+ let cvc4Tests = cvcTests CVC4+ let cvc5Tests = cvcTests CVC5 let yicesTests = [ testResolveSymBV WURB.ExponentialSearch@@ -1289,7 +1320,6 @@ , testCase "Yices rounding" $ withYices roundingTest , testCase "Yices #182 test case" $ withYices issue182Test ]- let cvc5Tests = cvc4Tests let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id else fmap (ignoreTestBecause (nm <> " not present")) defaultMain $ testGroup "Tests" $
what4.cabal view
@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name: what4-Version: 1.6+Version: 1.6.1 Author: Galois Inc. Maintainer: rscott@galois.com, kquick@galois.com Copyright: (c) Galois, Inc 2014-2023