Remove a variety of panic cases in the saw-core simulator primitives.

Also, add a switch that controls if the evalutor will be have in
a "symbolic" way.

Adding a new `PrimExcept` constructor that allows primitives to
cause fallback behavior after examining all their arguments.
As with the existing `PrimFilterFun`, this causes term reconstruction
in the term model evaluator, and raises an error in the other evaluators.
We use this new type of primitive to remove cases that would otherwise
panic.

In addition, we add a flag to the `BasePrims` record that controls
if we do symbolic muxing for sequence operations and `ite`. For the
term model, we disable this behavior and fall back earlier on term
reconstruction. This avoids constructing large mux trees in some cases.

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