Throw unsupported primitive exception. (#55)

* Throw unsupported primitive exception.

* Address comments.

src/Verifier/SAW/Prim.hs

@@ -271,6 +271,7 @@ lg2rem n = (k+1, 2*d+r)
 data EvalError
   = InvalidIndex Integer
   | DivideByZero
+  | UnsupportedPrimitive String String
   | UserError String
   deriving (Eq, Typeable)
 
@@ -280,6 +281,7 @@ instance Show EvalError where
   show e = case e of
     InvalidIndex i -> "invalid sequence index: " ++ show i
     DivideByZero -> "division by 0"
+    UnsupportedPrimitive b p -> "unsupported primitive " ++ p ++ " in " ++ b ++ " backend"
     UserError msg -> "Run-time error: " ++ msg
 
 -- | A sequencing operation has gotten an invalid index.
@@ -290,6 +292,11 @@ invalidIndex i = X.throw (InvalidIndex i)
 divideByZero :: a
 divideByZero = X.throw DivideByZero
 
+-- | A backend with a unsupported primitive.
+unsupportedPrimitive :: String -> String -> a
+unsupportedPrimitive backend primitive =
+  X.throw $ UnsupportedPrimitive backend primitive
+
 -- | For `error`
 userError :: String -> a
 userError msg = X.throw (UserError msg)

src/Verifier/SAW/Simulator/Concrete.hs

@@ -209,7 +209,7 @@ prims =
   , Prims.bpBvPopcount = pure1 (Prim.bvPopcount undefined)
   , Prims.bpBvCountLeadingZeros = pure1 (Prim.bvCountLeadingZeros undefined)
   , Prims.bpBvCountTrailingZeros = pure1 (Prim.bvCountTrailingZeros undefined)
-  , Prims.bpBvForall = error "bvForall unimplemented for backend"
+  , Prims.bpBvForall = unsupportedConcretePrimitive "bvForall"
 
     -- Integer operations
   , Prims.bpIntAdd = pure2 (+)
@@ -226,6 +226,9 @@ prims =
   , Prims.bpIntMax = pure2 max
   }
 
+unsupportedConcretePrimitive :: String -> a
+unsupportedConcretePrimitive = Prim.unsupportedPrimitive "concrete"
+
 constMap :: Map Ident CValue
 constMap =
   flip Map.union (Prims.constMap prims) $

src/Verifier/SAW/Simulator/RME.hs

@@ -174,7 +174,7 @@ prims =
   , Prims.bpBvURem = pure2 RMEV.urem
   , Prims.bpBvSDiv = pure2 RMEV.sdiv
   , Prims.bpBvSRem = pure2 RMEV.srem
-  , Prims.bpBvLg2  = undefined--pure1 Prim.bvLg2
+  , Prims.bpBvLg2  = unsupportedRMEPrimitive "bpBvLg2"
     -- Bitvector comparisons
   , Prims.bpBvEq   = pure2 RMEV.eq
   , Prims.bpBvsle  = pure2 RMEV.sle
@@ -198,7 +198,7 @@ prims =
   , Prims.bpBvPopcount = pure1 RMEV.popcount
   , Prims.bpBvCountLeadingZeros = pure1 RMEV.countLeadingZeros
   , Prims.bpBvCountTrailingZeros = pure1 RMEV.countTrailingZeros
-  , Prims.bpBvForall = error "bvForall unimplemented for backend"
+  , Prims.bpBvForall = unsupportedRMEPrimitive "bvForall"
     -- Integer operations
   , Prims.bpIntAdd = pure2 (+)
   , Prims.bpIntSub = pure2 (-)
@@ -210,10 +210,13 @@ prims =
   , Prims.bpIntEq  = pure2 (\x y -> RME.constant (x == y))
   , Prims.bpIntLe  = pure2 (\x y -> RME.constant (x <= y))
   , Prims.bpIntLt  = pure2 (\x y -> RME.constant (x < y))
-  , Prims.bpIntMin = undefined--pure2 min
-  , Prims.bpIntMax = undefined--pure2 max
+  , Prims.bpIntMin = unsupportedRMEPrimitive "bpIntMin"
+  , Prims.bpIntMax = unsupportedRMEPrimitive "bpIntMax"
   }
 
+unsupportedRMEPrimitive :: String -> a
+unsupportedRMEPrimitive = Prim.unsupportedPrimitive "RME"
+
 constMap :: Map Ident RValue
 constMap =
   Map.union (Prims.constMap prims) $
@@ -246,11 +249,11 @@ constMap =
 
 -- primitive bvToInt :: (n::Nat) -> bitvector n -> Integer;
 bvToIntOp :: RValue
-bvToIntOp = undefined -- constFun $ wordFun $ VInt . unsigned
+bvToIntOp = unsupportedRMEPrimitive "bvToIntOp"
 
 -- primitive sbvToInt :: (n::Nat) -> bitvector n -> Integer;
 sbvToIntOp :: RValue
-sbvToIntOp = undefined -- constFun $ wordFun $ VInt . signed
+sbvToIntOp = unsupportedRMEPrimitive "sbvToIntOp"
 
 -- primitive intToBv :: (n::Nat) -> Integer -> bitvector n;
 intToBvOp :: RValue