Merge pull request #1368 from GaloisInc/term-model-fix

Tweak the term model to avoid a panic situation

Author: robdockins

saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs

@@ -170,7 +170,8 @@ pure3 f x y z = pure (f x y z)
 prims :: AIG.IsAIG l g => g s -> Prims.BasePrims (BitBlast (l s))
 prims be =
   Prims.BasePrims
-  { Prims.bpAsBool  = AIG.asConstant be
+  { Prims.bpIsSymbolicEvaluator = True
+  , Prims.bpAsBool  = AIG.asConstant be
     -- Bitvectors
   , Prims.bpUnpack  = pure1 vFromLV
   , Prims.bpPack    = pure1 lvFromV

saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs

@@ -105,7 +105,8 @@ pure3 f x y z = pure (f x y z)
 prims :: Prims.BasePrims SBV
 prims =
   Prims.BasePrims
-  { Prims.bpAsBool  = svAsBool
+  { Prims.bpIsSymbolicEvaluator = True
+  , Prims.bpAsBool  = svAsBool
   , Prims.bpUnpack  = svUnpack
   , Prims.bpPack    = pure1 symFromBits
   , Prims.bpBvAt    = pure2 svAt

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

@@ -161,7 +161,8 @@ prims :: forall sym.
    Sym sym => sym -> Prims.BasePrims (What4 sym)
 prims sym =
   Prims.BasePrims
-  { Prims.bpAsBool  = W.asConstantPred
+  { Prims.bpIsSymbolicEvaluator = True
+  , Prims.bpAsBool  = W.asConstantPred
     -- Bitvectors
   , Prims.bpUnpack  = SW.bvUnpackBE sym
   , Prims.bpPack    = SW.bvPackBE sym

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

@@ -35,7 +35,7 @@ import Prelude hiding (mapM)
 import Control.Applicative ((<$>))
 #endif
 import Control.Monad (foldM, liftM)
---import Control.Monad.IO.Class
+import Control.Monad.Trans.Except
 import Control.Monad.Trans.Maybe
 import Control.Monad.Fix (MonadFix(mfix))
 import Control.Monad.Identity (Identity)
@@ -624,6 +624,11 @@ evalPrim fallback pn = loop [] (primType pn)
              Just v -> loop ((ready x',t):env) tp' (f v)
              _ -> fallback msg ((ready x',t):env) tp'
 
+    loop env tp (Prims.PrimExcept m) =
+      runExceptT m >>= \case
+        Right v  -> pure v
+        Left msg -> fallback msg env tp
+
     loop _env _tp (Prims.Prim m) = m
     loop _env _tp (Prims.PrimValue v) = pure v
 

saw-core/src/Verifier/SAW/Simulator/Concrete.hs

@@ -132,7 +132,8 @@ ite b x y = if b then x else y
 prims :: Prims.BasePrims Concrete
 prims =
   Prims.BasePrims
-  { Prims.bpAsBool  = Just
+  { Prims.bpIsSymbolicEvaluator = False
+  , Prims.bpAsBool  = Just
   , Prims.bpUnpack  = pure1 Prim.unpackBitVector
   , Prims.bpPack    = pure1 Prim.packBitVector
   , Prims.bpBvAt    = pure2 Prim.bvAt