Merge pull request #91 from GaloisInc/tvalue

Refactor saw-core `Value` type to make a separate datatype for type values
GaloisInc · Oct 20, 2020 · 3dd70af · 3dd70af
2 parents d52a05c + d416a83
commit 3dd70af
Show file tree

Hide file tree

Showing 10 changed files with 143 additions and 108 deletions.
diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs
@@ -1357,7 +1357,7 @@ pIsNeq ty = case C.tNoUser ty of
 --------------------------------------------------------------------------------
 -- Utilities
 
-asCryptolTypeValue :: SC.CValue -> Maybe C.Type
+asCryptolTypeValue :: SC.TValue SC.Concrete -> Maybe C.Type
 asCryptolTypeValue v =
   case v of
     SC.VBoolType -> return C.tBit
@@ -1366,11 +1366,11 @@ asCryptolTypeValue v =
       t1 <- asCryptolTypeValue v1
       t2 <- asCryptolTypeValue v2
       return $ C.tArray t1 t2
-    SC.VVecType (SC.VNat n) v2 -> do
+    SC.VVecType n v2 -> do
       t2 <- asCryptolTypeValue v2
       return (C.tSeq (C.tNum n) t2)
     SC.VDataType "Prelude.Stream" [v1] -> do
-      t1 <- asCryptolTypeValue v1
+      t1 <- asCryptolTypeValue (SC.toTValue v1)
       return (C.tSeq C.tInf t1)
     SC.VUnitType -> return (C.tTuple [])
     SC.VPairType v1 v2 -> do
@@ -1405,7 +1405,7 @@ asCryptolTypeValue v =
 scCryptolType :: SharedContext -> Term -> IO C.Type
 scCryptolType sc t =
   do modmap <- scGetModuleMap sc
-     case asCryptolTypeValue (SC.evalSharedTerm modmap Map.empty t) of
+     case asCryptolTypeValue (SC.toTValue (SC.evalSharedTerm modmap Map.empty t)) of
        Just ty -> return ty
        Nothing -> panic "scCryptolType" ["scCryptolType: unsupported type " ++ showTerm t]
 

diff --git a/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs b/saw-core-aig/src/Verifier/SAW/Simulator/BitBlast.hs
@@ -269,7 +269,7 @@ beConstMap be =
   , ("Prelude.bvToInt" , bvToIntOp be)
   , ("Prelude.sbvToInt", sbvToIntOp be)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun VIntType)
+  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , toIntModOp)
   , ("Prelude.fromIntMod", constFun (VFun force))
   , ("Prelude.intModEq"  , intModEqOp be)
@@ -444,7 +444,7 @@ bitBlastBasic be m addlPrims ecMap t = do
   Sim.evalSharedTerm cfg t
 
 bitBlastExtCns ::
-  Map VarIndex (BValue (l s)) -> ExtCns (BValue (l s)) ->
+  Map VarIndex (BValue (l s)) -> ExtCns (TValue (BitBlast (l s))) ->
   IO (BValue (l s))
 bitBlastExtCns ecMap (EC idx name _v) =
   case Map.lookup idx ecMap of

diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
@@ -196,7 +196,7 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun VIntType)
+  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , constFun (VFun force))
   , ("Prelude.fromIntMod", fromIntModOp)
   , ("Prelude.intModEq"  , intModEqOp)
@@ -565,7 +565,7 @@ sbvSolveBasic m addlPrims unints t = do
   cfg <- Sim.evalGlobal m (Map.union constMap addlPrims) extcns uninterpreted
   Sim.evalSharedTerm cfg t
 
-parseUninterpreted :: [SVal] -> String -> SValue -> IO SValue
+parseUninterpreted :: [SVal] -> String -> TValue SBV -> IO SValue
 parseUninterpreted cws nm ty =
   case ty of
     (VPiType _ f)
@@ -581,10 +581,10 @@ parseUninterpreted cws nm ty =
     VIntType
       -> return $ vInteger $ mkUninterpreted KUnbounded cws nm
 
-    (VVecType (VNat n) VBoolType)
+    (VVecType n VBoolType)
       -> return $ vWord $ mkUninterpreted (KBounded False (fromIntegral n)) cws nm
 
-    (VVecType (VNat n) ety)
+    (VVecType n ety)
       -> do xs <- sequence $
                   [ parseUninterpreted cws (nm ++ "@" ++ show i) ety
                   | i <- [0 .. n-1] ]
@@ -610,7 +610,7 @@ mkUninterpreted :: Kind -> [SVal] -> String -> SVal
 mkUninterpreted k args nm = svUninterpreted k nm' Nothing args
   where nm' = "|" ++ nm ++ "|" -- enclose name to allow primes and other non-alphanum chars
 
-asPredType :: SValue -> IO [SValue]
+asPredType :: TValue SBV -> IO [TValue SBV]
 asPredType v =
   case v of
     VBoolType -> return []
@@ -620,14 +620,14 @@ asPredType v =
          return (v1 : vs)
     _ -> fail $ "non-boolean result type: " ++ show v
 
-vAsFirstOrderType :: SValue -> Maybe FirstOrderType
+vAsFirstOrderType :: TValue SBV -> Maybe FirstOrderType
 vAsFirstOrderType v =
   case v of
     VBoolType
       -> return FOTBit
     VIntType
       -> return FOTInt
-    VVecType (VNat n) v2
+    VVecType n v2
       -> FOTVec n <$> vAsFirstOrderType v2
     VUnitType
       -> return (FOTTuple [])
@@ -655,7 +655,7 @@ sbvSolve sc addlPrims unints t = do
   let lamNames = map fst (fst (R.asLambdaList t))
   let varNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ]
   let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "")
-  argTs <- asPredType ty
+  argTs <- asPredType (toTValue ty)
   (labels, vars) <-
     flip evalStateT 0 $ unzip <$>
     sequence (zipWith newVarsForType argTs argNames)
@@ -685,7 +685,7 @@ nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s))
 myfun ::(Map String (Labeler, Symbolic SValue)) -> (Map String Labeler, Map String (Symbolic SValue))
 myfun = fmap fst A.&&& fmap snd
 
-newVarsForType :: SValue -> String -> StateT Int IO (Maybe Labeler, Symbolic SValue)
+newVarsForType :: TValue SBV -> String -> StateT Int IO (Maybe Labeler, Symbolic SValue)
 newVarsForType v nm =
   case vAsFirstOrderType v of
     Just fot ->

diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs
@@ -250,7 +250,7 @@ constMap =
   , ("Prelude.bvToInt" , bvToIntOp)
   , ("Prelude.sbvToInt", sbvToIntOp)
   -- Integers mod n
-  , ("Prelude.IntMod"    , constFun VIntType)
+  , ("Prelude.IntMod"    , constFun (TValue VIntType))
   , ("Prelude.toIntMod"  , constFun (VFun force))
   , ("Prelude.fromIntMod", fromIntModOp sym)
   , ("Prelude.intModEq"  , intModEqOp sym)
@@ -578,7 +578,7 @@ instance Show (SArray sym) where
 arrayConstant ::
   W.IsSymExprBuilder sym =>
   sym ->
-  SValue sym ->
+  TValue (What4 sym) ->
   SValue sym ->
   IO (SArray sym)
 arrayConstant sym ity elm
@@ -717,7 +717,7 @@ parseUninterpreted ::
   (IsSymExprBuilder sym) =>
   sym -> IORef (SymFnCache sym) ->
   UnintApp (SymExpr sym) ->
-  SValue sym -> IO (SValue sym)
+  TValue (What4 sym) -> IO (SValue sym)
 parseUninterpreted sym ref app ty =
   case ty of
     VPiType _ f
@@ -734,14 +734,14 @@ parseUninterpreted sym ref app ty =
       -> VInt  <$> mkUninterpreted sym ref app BaseIntegerRepr
 
     -- 0 width bitvector is a constant
-    VVecType (VNat 0) VBoolType
+    VVecType 0 VBoolType
       -> return $ VWord ZBV
 
-    VVecType (VNat n) VBoolType
+    VVecType n VBoolType
       | Just (Some (PosNat w)) <- somePosNat n
       -> (VWord . DBV) <$> mkUninterpreted sym ref app (BaseBVRepr w)
 
-    VVecType (VNat n) ety
+    VVecType n ety
       ->  do xs <- sequence $
                   [ parseUninterpreted sym ref (suffixUnintApp ("_a" ++ show i) app) ety
                   | i <- [0 .. n-1] ]
@@ -845,7 +845,7 @@ w4SolveAny sym sc ps unints t = give sym $ do
   let moreNames = [ "var" ++ show (i :: Integer) | i <- [0 ..] ]
 
   -- and their types
-  argTs <- argTypes ty
+  argTs <- argTypes (toTValue ty)
 
   -- construct symbolic expressions for the variables
   vars' <-
@@ -876,7 +876,7 @@ w4Solve sym sc ps unints t =
 --
 -- Pull out argument types until bottoming out at a non-Pi type
 --
-argTypes :: IsSymExprBuilder sv => SValue sv -> IO [SValue sv]
+argTypes :: IsSymExprBuilder sym => TValue (What4 sym) -> IO [TValue (What4 sym)]
 argTypes v =
   case v of
     VPiType v1 f ->
@@ -888,14 +888,14 @@ argTypes v =
 --
 -- Convert a saw-core type expression to a FirstOrder type expression
 --
-vAsFirstOrderType :: forall sv. IsSymExprBuilder sv => SValue sv -> Maybe FirstOrderType
+vAsFirstOrderType :: forall sym. IsSymExprBuilder sym => TValue (What4 sym) -> Maybe FirstOrderType
 vAsFirstOrderType v =
   case v of
     VBoolType
       -> return FOTBit
     VIntType
       -> return FOTInt
-    VVecType (VNat n) v2
+    VVecType n v2
       -> FOTVec n <$> vAsFirstOrderType v2
     VArrayType iv ev
       -> FOTArray <$> vAsFirstOrderType iv <*> vAsFirstOrderType ev
@@ -912,7 +912,7 @@ vAsFirstOrderType v =
           mapM (\(f,tp) -> (f,) <$> vAsFirstOrderType tp) tps)
     _ -> Nothing
 
-valueAsBaseType :: IsSymExprBuilder sym => SValue sym -> Maybe (Some W.BaseTypeRepr)
+valueAsBaseType :: IsSymExprBuilder sym => TValue (What4 sym) -> Maybe (Some W.BaseTypeRepr)
 valueAsBaseType v = fmap fotToBaseType $ vAsFirstOrderType v
 
 ------------------------------------------------------------------------------
@@ -942,7 +942,7 @@ nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s))
 
 newVarsForType :: forall sym. (Given sym, IsSymExprBuilder sym) =>
   IORef (SymFnCache sym) ->
-  SValue sym -> String -> StateT Int IO (Maybe (Labeler sym), SValue sym)
+  TValue (What4 sym) -> String -> StateT Int IO (Maybe (Labeler sym), SValue sym)
 newVarsForType ref v nm =
   case vAsFirstOrderType v of
     Just fot -> do
@@ -1019,7 +1019,7 @@ w4EvalAny sym sc ps unints t =
      let argNames = zipWith (++) varNames (map ("_" ++) lamNames ++ repeat "")
 
      -- and their types
-     argTs <- argTypes ty
+     argTs <- argTypes (toTValue ty)
 
      -- construct symbolic expressions for the variables
      vars' <-
@@ -1082,7 +1082,7 @@ parseUninterpretedSAW ::
   IORef (SymFnCache (CS.SAWCoreBackend n solver fs)) ->
   ArgTerm {- ^ representation of function applied to arguments -} ->
   UnintApp (SymExpr (CS.SAWCoreBackend n solver fs)) ->
-  SValue (CS.SAWCoreBackend n solver fs) {- ^ return type -} ->
+  TValue (What4 (CS.SAWCoreBackend n solver fs)) {- ^ return type -} ->
   IO (SValue (CS.SAWCoreBackend n solver fs))
 parseUninterpretedSAW sym sc ref trm app ty =
   case ty of
@@ -1102,15 +1102,15 @@ parseUninterpretedSAW sym sc ref trm app ty =
       -> VInt  <$> mkUninterpretedSAW sym ref trm app BaseIntegerRepr
 
     -- 0 width bitvector is a constant
-    VVecType (VNat 0) VBoolType
+    VVecType 0 VBoolType
       -> return $ VWord ZBV
 
-    VVecType (VNat n) VBoolType
+    VVecType n VBoolType
       | Just (Some (PosNat w)) <- somePosNat n
       -> (VWord . DBV) <$> mkUninterpretedSAW sym ref trm app (BaseBVRepr w)
 
-    VVecType (VNat n) ety | n >= 0
-      ->  do ety' <- termOfSValue sc ety
+    VVecType n ety | n >= 0
+      ->  do ety' <- termOfTValue sc ety
              let mkElem i =
                    do let trm' = ArgTermAt n ety' trm i
                       let app' = suffixUnintApp ("_a" ++ show i) app
@@ -1234,7 +1234,7 @@ reconstructArgTerm atrm sc ts =
 -- 'ArgTerm' that builds a term of that type from local variables with
 -- base types. The number of 'ArgTermVar' constructors should match
 -- the number of arguments appended by 'applyUnintApp'.
-mkArgTerm :: SharedContext -> SValue sym -> SValue sym -> IO ArgTerm
+mkArgTerm :: SharedContext -> TValue (What4 sym) -> SValue sym -> IO ArgTerm
 mkArgTerm sc ty val =
   case (ty, val) of
     (VBoolType, VBool _) -> return ArgTermVar
@@ -1246,7 +1246,7 @@ mkArgTerm sc ty val =
     (VVecType _ ety, VVector vv) ->
       do vs <- traverse force (V.toList vv)
          xs <- traverse (mkArgTerm sc ety) vs
-         ety' <- termOfSValue sc ety
+         ety' <- termOfTValue sc ety
          return (ArgTermVector ety' xs)
 
     (VPairType ty1 ty2, VPair v1 v2) ->
@@ -1267,24 +1267,30 @@ mkArgTerm sc ty val =
 
     _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty
 
-termOfSValue :: SharedContext -> SValue sym -> IO Term
-termOfSValue sc val =
+termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term
+termOfTValue sc val =
   case val of
-    VUnit -> scUnitValue sc
     VBoolType -> scBoolType sc
     VIntType -> scIntegerType sc
     VUnitType -> scUnitType sc
-    VVecType (VNat n) a ->
+    VVecType n a ->
       do n' <- scNat sc n
-         a' <- termOfSValue sc a
+         a' <- termOfTValue sc a
          scVecType sc n' a'
     VPairType a b
-      -> do a' <- termOfSValue sc a
-            b' <- termOfSValue sc b
+      -> do a' <- termOfTValue sc a
+            b' <- termOfTValue sc b
             scPairType sc a' b'
     VRecordType flds
-      -> do flds' <- traverse (traverse (termOfSValue sc)) flds
+      -> do flds' <- traverse (traverse (termOfTValue sc)) flds
             scRecordType sc flds'
+    _ -> fail $ "termOfTValue: " ++ show val
+
+termOfSValue :: SharedContext -> SValue sym -> IO Term
+termOfSValue sc val =
+  case val of
+    VUnit -> scUnitValue sc
     VNat n
       -> scNat sc n
+    TValue tv -> termOfTValue sc tv
     _ -> fail $ "termOfSValue: " ++ show val