Add saw-script functions term_eval and term_eval_unint.

saw-core-what4/src/Verifier/SAW/Simulator/What4.hs

@@ -51,6 +51,7 @@ module Verifier.SAW.Simulator.What4
   , w4EvalBasic
   , getLabelValues
 
+  , w4EvalTerm
   , w4SimulatorEval
   , NeutralTermException(..)
 
@@ -1275,6 +1276,96 @@ 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 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 st sc ps unintSet t =
+  do modmap <- scGetModuleMap sc
+     ref <- newIORef Map.empty
+     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 st sc tytval val
+  where
+    toTValue :: Value l -> IO (TValue l)
+    toTValue (TValue x) = pure x
+    toTValue _ = fail "toTValue"
+
+rebuildTerm ::
+  B.ExprBuilder n st fs ->
+  SAWCoreState n ->
+  SharedContext ->
+  TValue (What4 (B.ExprBuilder n st fs)) ->
+  SValue (B.ExprBuilder n st fs) ->
+  IO Term
+rebuildTerm sym st 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 st sc tx vx
+             y' <- rebuildTerm sym st 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 st sc tx) vs
+             tx' <- termOfTValue sc tx
+             scVectorReduced sc tx' xs'
+        _ -> fail "panic: rebuildTerm: internal error"
+    VBool x ->
+      toSC sym st x
+    VWord x ->
+      case x of
+        DBV w -> toSC sym st w
+        ZBV ->
+          do z <- scNat sc 0
+             scBvNat sc z z
+    VBVToNat _ _ ->
+      fail "rebuildTerm VBVToNat"
+    VIntToNat _ ->
+      fail "rebuildTerm VIntToNat"
+    VNat n ->
+      scNat sc n
+    VInt x ->
+      toSC sym st x
+    VIntMod _ _ ->
+      fail "rebuildTerm VIntMod"
+    VArray _ ->
+      fail "rebuildTerm VArray"
+    VString s ->
+      scString sc s
+    VRecordValue _ ->
+      fail "rebuildTerm VRecordValue"
+    VRecursor _ _ _ _ _ ->
+      fail "rebuildTerm VRecursor"
+    VExtra _ ->
+      fail "rebuildTerm VExtra"
+    TValue _tval ->
+      fail "rebuildTerm TValue"
+
 
 -- | Simplify a saw-core term by evaluating it through the saw backend
 -- of what4.

src/SAWScript/Builtins.hs

@@ -95,6 +95,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
 
@@ -128,6 +131,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)
@@ -1594,6 +1598,16 @@ 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
+     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)
+
 addsimp :: Theorem -> SV.SAWSimpset -> TopLevel SV.SAWSimpset
 addsimp thm ss =
   do sc <- getSharedContext

src/SAWScript/Interpreter.hs

@@ -2485,6 +2485,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