From ad97634ab42ddd4f99ec03638cdcbfc5bfad0314 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 20 Nov 2020 09:32:54 -0800 Subject: [PATCH 1/4] Add `w4EvalTerm` for round-tripping terms of any type through what4. Currently this only works for first-order values; function types are not supported yet. --- .../src/Verifier/SAW/Simulator/What4.hs | 84 +++++++++++++++++++ 1 file changed, 84 insertions(+) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index f106645b9e..11ff50e620 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -51,6 +51,7 @@ module Verifier.SAW.Simulator.What4 , w4EvalBasic , getLabelValues + , w4EvalTerm , w4SimulatorEval , NeutralTermException(..) @@ -99,6 +100,7 @@ import What4.Interface(SymExpr,Pred,SymInteger, IsExpr, IsExprBuilder,IsSymExprBuilder) import qualified What4.Interface as W import What4.BaseTypes +import What4.Protocol.Online (OnlineSolver) import qualified What4.SWord as SW import What4.SWord (SWord(..)) @@ -1166,6 +1168,88 @@ getLabelValues f = ---------------------------------------------------------------------- -- Evaluation through crucible-saw backend +-- | Simplify a saw-core term by evaluating it through the saw backend +-- of what4. The term may have any first-order monomorphic function +-- type. Return a term with the same type. +w4EvalTerm :: + forall n solver fs. + OnlineSolver solver => + CS.SAWCoreBackend n solver fs -> SharedContext -> + Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> Set VarIndex -> Term -> + IO Term +w4EvalTerm sym sc ps unintSet t = + do modmap <- scGetModuleMap sc + ref <- newIORef Map.empty + let eval = w4EvalBasic sym sc modmap ps ref unintSet + ty <- eval =<< scTypeOf sc t + -- evaluate term to an SValue + val <- eval t + -- convert SValue back into a Term + rebuildTerm sym sc (toTValue ty) val + +rebuildTerm :: + OnlineSolver solver => + CS.SAWCoreBackend n solver fs -> + SharedContext -> + TValue (What4 (CS.SAWCoreBackend n solver fs)) -> + SValue (CS.SAWCoreBackend n solver fs) -> + IO Term +rebuildTerm sym sc tv = + \case + VFun _ -> + fail "rebuildTerm VFun" + VUnit -> + scUnitValue sc + VPair x y -> + case tv of + VPairType tx ty -> + do vx <- force x + vy <- force y + x' <- rebuildTerm sym sc tx vx + y' <- rebuildTerm sym sc ty vy + scPairValue sc x' y' + _ -> fail "panic: rebuildTerm: internal error" + VCtorApp _ _ -> + fail "rebuildTerm VCtorApp" + VVector xs -> + case tv of + VVecType _ tx -> + do vs <- traverse force (V.toList xs) + xs' <- traverse (rebuildTerm sym sc tx) vs + tx' <- termOfTValue sc tx + scVectorReduced sc tx' xs' + _ -> fail "panic: rebuildTerm: internal error" + VBool x -> + CS.toSC sym x + VWord x -> + case x of + DBV w -> CS.toSC sym w + ZBV -> + do z <- scNat sc 0 + scBvNat sc z z + VToNat _ -> + fail "rebuildTerm VToNat" + VNat n -> + scNat sc n + VInt x -> + CS.toSC sym x + VIntMod _ _ -> + fail "rebuildTerm VIntMod" + VArray _ -> + fail "rebuildTerm VArray" + VString s -> + scString sc s + VFloat _ -> + fail "rebuildTerm VFloat" + VDouble _ -> + fail "rebuildTerm VDouble" + VRecordValue _ -> + fail "rebuildTerm VRecordValue" + VExtra _ -> + fail "rebuildTerm VExtra" + TValue _tval -> + fail "rebuildTerm TValue" + -- | Simplify a saw-core term by evaluating it through the saw backend -- of what4. From 627470644f2d09c1b9179e9fd72dbed79cc6ce8d Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 26 Apr 2021 17:47:00 -0700 Subject: [PATCH 2/4] Add saw-script functions `term_eval` and `term_eval_unint`. These are analogous to the `goal_eval` and `goal_eval_unint` proof tactics, but instead of proof goals they work on arbitrary terms. --- src/SAWScript/Builtins.hs | 9 +++++++++ src/SAWScript/Interpreter.hs | 11 +++++++++++ 2 files changed, 20 insertions(+) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index d6404c0f35..827e4a6717 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1111,6 +1111,15 @@ beta_reduce_term (TypedTerm schema t) = do t' <- io $ betaNormalize sc t return (TypedTerm schema t') +term_eval :: [String] -> TypedTerm -> TopLevel TypedTerm +term_eval unints (TypedTerm schema t0) = + do sc <- getSharedContext + unintSet <- resolveNames unints + let gen = globalNonceGenerator + sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen + t1 <- liftIO $ W4Sim.w4EvalTerm sym sc Map.empty unintSet t0 + pure (TypedTerm schema t1) + addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset addsimp thm ss = do sc <- getSharedContext diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index e5743e2b00..2c97c96175 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1913,6 +1913,17 @@ primitives = Map.fromList Current [ "Reduce the given term to beta-normal form." ] + , prim "term_eval" "Term -> Term" + (funVal1 (term_eval [])) + Current + [ "Evaluate the term to a first-order combination of primitives." ] + + , prim "term_eval_unint" "[String] -> Term -> Term" + (funVal2 term_eval) + Current + [ "Evaluate the term to a first-order combination of primitives." + , "Leave the given names, as defined with 'define', as uninterpreted." ] + , prim "cryptol_load" "String -> TopLevel CryptolModule" (pureVal (cryptol_load BS.readFile)) Current From 37e3cc6efc38907713deb219d8cd3c0034429252 Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Sun, 29 May 2022 19:36:38 -0400 Subject: [PATCH 3/4] Ensure everything builds after rebase --- .../src/Verifier/SAW/Simulator/What4.hs | 61 +++++++++++-------- src/SAWScript/Builtins.hs | 10 ++- 2 files changed, 41 insertions(+), 30 deletions(-) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 11ff50e620..7dd70c1d74 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -100,7 +100,6 @@ import What4.Interface(SymExpr,Pred,SymInteger, IsExpr, IsExprBuilder,IsSymExprBuilder) import qualified What4.Interface as W import What4.BaseTypes -import What4.Protocol.Online (OnlineSolver) import qualified What4.SWord as SW import What4.SWord (SWord(..)) @@ -1172,31 +1171,39 @@ getLabelValues f = -- of what4. The term may have any first-order monomorphic function -- type. Return a term with the same type. w4EvalTerm :: - forall n solver fs. - OnlineSolver solver => - CS.SAWCoreBackend n solver fs -> SharedContext -> - Map Ident (SValue (CS.SAWCoreBackend n solver fs)) -> Set VarIndex -> Term -> + forall n st fs. + B.ExprBuilder n st fs -> + SAWCoreState n -> + SharedContext -> + Map Ident (SPrim (B.ExprBuilder n st fs)) -> + Set VarIndex -> + Term -> IO Term -w4EvalTerm sym sc ps unintSet t = +w4EvalTerm sym st sc ps unintSet t = do modmap <- scGetModuleMap sc ref <- newIORef Map.empty - let eval = w4EvalBasic sym sc modmap ps ref unintSet + let eval = w4EvalBasic sym st sc modmap ps ref unintSet ty <- eval =<< scTypeOf sc t -- evaluate term to an SValue val <- eval t + tytval <- toTValue ty -- convert SValue back into a Term - rebuildTerm sym sc (toTValue ty) val + rebuildTerm sym st sc tytval val + where + toTValue :: Value l -> IO (TValue l) + toTValue (TValue x) = pure x + toTValue _ = fail "toTValue" rebuildTerm :: - OnlineSolver solver => - CS.SAWCoreBackend n solver fs -> + B.ExprBuilder n st fs -> + SAWCoreState n -> SharedContext -> - TValue (What4 (CS.SAWCoreBackend n solver fs)) -> - SValue (CS.SAWCoreBackend n solver fs) -> + TValue (What4 (B.ExprBuilder n st fs)) -> + SValue (B.ExprBuilder n st fs) -> IO Term -rebuildTerm sym sc tv = +rebuildTerm sym st sc tv = \case - VFun _ -> + VFun _ _ -> fail "rebuildTerm VFun" VUnit -> scUnitValue sc @@ -1205,46 +1212,46 @@ rebuildTerm sym sc tv = VPairType tx ty -> do vx <- force x vy <- force y - x' <- rebuildTerm sym sc tx vx - y' <- rebuildTerm sym sc ty vy + x' <- rebuildTerm sym st sc tx vx + y' <- rebuildTerm sym st sc ty vy scPairValue sc x' y' _ -> fail "panic: rebuildTerm: internal error" - VCtorApp _ _ -> + VCtorApp _ _ _ -> fail "rebuildTerm VCtorApp" VVector xs -> case tv of VVecType _ tx -> do vs <- traverse force (V.toList xs) - xs' <- traverse (rebuildTerm sym sc tx) vs + xs' <- traverse (rebuildTerm sym st sc tx) vs tx' <- termOfTValue sc tx scVectorReduced sc tx' xs' _ -> fail "panic: rebuildTerm: internal error" VBool x -> - CS.toSC sym x + toSC sym st x VWord x -> case x of - DBV w -> CS.toSC sym w + DBV w -> toSC sym st w ZBV -> do z <- scNat sc 0 scBvNat sc z z - VToNat _ -> - fail "rebuildTerm VToNat" + VBVToNat _ _ -> + fail "rebuildTerm VBVToNat" + VIntToNat _ -> + fail "rebuildTerm VIntToNat" VNat n -> scNat sc n VInt x -> - CS.toSC sym x + toSC sym st x VIntMod _ _ -> fail "rebuildTerm VIntMod" VArray _ -> fail "rebuildTerm VArray" VString s -> scString sc s - VFloat _ -> - fail "rebuildTerm VFloat" - VDouble _ -> - fail "rebuildTerm VDouble" VRecordValue _ -> fail "rebuildTerm VRecordValue" + VRecursor _ _ _ _ _ -> + fail "rebuildTerm VRecursor" VExtra _ -> fail "rebuildTerm VExtra" TValue _tval -> diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 827e4a6717..5ebf63ea5d 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -90,6 +90,9 @@ import qualified Verifier.SAW.CryptolEnv as CEnv -- saw-core-sbv import qualified Verifier.SAW.Simulator.SBV as SBVSim +-- saw-core-what4 +import qualified Verifier.SAW.Simulator.What4 as W4Sim + -- sbv import qualified Data.SBV.Dynamic as SBV @@ -120,6 +123,7 @@ import SAWScript.AST (getVal, pShow, Located(..)) import SAWScript.Options as Opts import SAWScript.Proof import SAWScript.Crucible.Common (PathSatSolver(..)) +import qualified SAWScript.Crucible.Common as Common import SAWScript.TopLevel import qualified SAWScript.Value as SV import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) @@ -1115,9 +1119,9 @@ term_eval :: [String] -> TypedTerm -> TopLevel TypedTerm term_eval unints (TypedTerm schema t0) = do sc <- getSharedContext unintSet <- resolveNames unints - let gen = globalNonceGenerator - sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen - t1 <- liftIO $ W4Sim.w4EvalTerm sym sc Map.empty unintSet t0 + sym <- liftIO $ Common.newSAWCoreExprBuilder sc + st <- liftIO $ Common.sawCoreState sym + t1 <- liftIO $ W4Sim.w4EvalTerm sym st sc Map.empty unintSet t0 pure (TypedTerm schema t1) addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset From ce93936e476e3942048a9a9e3179eb9c9a2cc2b3 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 14 Nov 2024 18:00:17 -0500 Subject: [PATCH 4/4] Make this branch build again. --- src/SAWScript/Builtins.hs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 968c7b7c6e..c84e985f58 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1602,7 +1602,8 @@ term_eval :: [String] -> TypedTerm -> TopLevel TypedTerm term_eval unints (TypedTerm schema t0) = do sc <- getSharedContext unintSet <- resolveNames unints - sym <- liftIO $ Common.newSAWCoreExprBuilder sc + what4PushMuxOps <- gets rwWhat4PushMuxOps + sym <- liftIO $ Common.newSAWCoreExprBuilder sc what4PushMuxOps st <- liftIO $ Common.sawCoreState sym t1 <- liftIO $ W4Sim.w4EvalTerm sym st sc Map.empty unintSet t0 pure (TypedTerm schema t1)