Merge branch 'master' into saw-core-heapster-final-merge

cryptol-saw-core/src/Verifier/SAW/Cryptol.hs

@@ -1408,27 +1408,34 @@ proveEq sc env t1 t2
            aEq <- proveEq sc env a1 a2
            bEq <- proveEq sc env b1 b2
            scGlobalApply sc "Cryptol.fun_cong" [a1', a2', b1', b2', aEq, bEq]
-      (C.tIsTuple -> Just (a1 : ts1), C.tIsTuple -> Just (a2 : ts2))
-        | length ts1 == length ts2 ->
-          do let b1 = C.tTuple ts1
-                 b2 = C.tTuple ts2
-             a1' <- importType sc env a1
-             a2' <- importType sc env a2
-             b1' <- importType sc env b1
-             b2' <- importType sc env b2
-             aEq <- proveEq sc env a1 a2
-             bEq <- proveEq sc env b1 b2
-             if b1 == b2
-               then scGlobalApply sc "Cryptol.pair_cong1" [a1', a2', b1', aEq]
-               else if a1 == a2
-                    then scGlobalApply sc "Cryptol.pair_cong2" [a1', b1', b2', bEq]
-                    else scGlobalApply sc "Cryptol.pair_cong" [a1', a2', b1', b2', aEq, bEq]
+      (tIsPair -> Just (a1, b1), tIsPair -> Just (a2, b2)) ->
+        do a1' <- importType sc env a1
+           a2' <- importType sc env a2
+           b1' <- importType sc env b1
+           b2' <- importType sc env b2
+           aEq <- proveEq sc env a1 a2
+           bEq <- proveEq sc env b1 b2
+           if b1 == b2
+             then scGlobalApply sc "Cryptol.pair_cong1" [a1', a2', b1', aEq]
+             else if a1 == a2
+                  then scGlobalApply sc "Cryptol.pair_cong2" [a1', b1', b2', bEq]
+                  else scGlobalApply sc "Cryptol.pair_cong" [a1', a2', b1', b2', aEq, bEq]
       (C.tIsRec -> Just tm1, C.tIsRec -> Just tm2)
         | map fst (C.canonicalFields tm1) == map fst (C.canonicalFields tm2) ->
           proveEq sc env (C.tTuple (map snd (C.canonicalFields tm1))) (C.tTuple (map snd (C.canonicalFields tm2)))
       (_, _) ->
         panic "proveEq" ["Internal type error:", pretty t1, pretty t2]
 
+-- | Deconstruct a cryptol tuple type as a pair according to the
+-- saw-core tuple type encoding.
+tIsPair :: C.Type -> Maybe (C.Type, C.Type)
+tIsPair t =
+  do ts <- C.tIsTuple t
+     case ts of
+       [] -> Nothing
+       [t1, t2] -> Just (t1, t2)
+       t1 : ts' -> Just (t1, C.tTuple ts')
+
 --------------------------------------------------------------------------------
 -- List comprehensions
 

cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs

@@ -10,6 +10,7 @@ module Verifier.SAW.TypedTerm where
 import Control.Monad (foldM)
 import Data.Map (Map)
 import qualified Data.Map as Map
+import Data.Text (Text)
 
 import Cryptol.ModuleSystem.Name (nameIdent)
 import qualified Cryptol.TypeCheck.AST as C
@@ -62,7 +63,7 @@ applyTypedTerms :: SharedContext -> TypedTerm -> [TypedTerm] -> IO TypedTerm
 applyTypedTerms sc = foldM (applyTypedTerm sc)
 
 -- | Create an abstract defined constant with the specified name and body.
-defineTypedTerm :: SharedContext -> String -> TypedTerm -> IO TypedTerm
+defineTypedTerm :: SharedContext -> Text -> TypedTerm -> IO TypedTerm
 defineTypedTerm sc name (TypedTerm schema t) =
   do ty <- scTypeOf sc t
      TypedTerm schema <$> scConstant sc name t ty

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

@@ -635,10 +635,11 @@ sbvSATQuery sc addlPrims query =
      t <- liftIO (foldM (scAnd sc) true (satAsserts query))
      let qvars = Map.toList (satVariables query)
      let unintSet = satUninterp query
+     let ecVars (ec, fot) = newVars (Text.unpack (toShortName (ecName ec))) fot
 
      (labels, vars) <-
        flip evalStateT 0 $ unzip <$>
-       mapM (newVars . snd) qvars
+       mapM ecVars qvars
 
      m <- liftIO (scGetModuleMap sc)
 
@@ -667,35 +668,48 @@ data Labeler
    = BoolLabel String
    | IntegerLabel String
    | WordLabel String
+   | ZeroWidthWordLabel
    | VecLabel (Vector Labeler)
    | TupleLabel (Vector Labeler)
    | RecLabel (Map FieldName Labeler)
      deriving (Show)
 
 nextId :: StateT Int IO String
-nextId = ST.get >>= (\s-> modify (+1) >> return ("x" ++ show s))
+nextId = ST.get >>= (\s -> modify (+1) >> return ("x" ++ show s))
+
+nextId' :: String -> StateT Int IO String
+nextId' nm = nextId <&> \s -> s ++ "_" ++ nm
 
 unzipMap :: Map k (a, b) -> (Map k a, Map k b)
 unzipMap m = (fmap fst m, fmap snd m)
 
-newVars :: FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue)
-newVars FOTBit = nextId <&> \s-> (BoolLabel s, vBool <$> existsSBool s)
-newVars FOTInt = nextId <&> \s-> (IntegerLabel s, vInteger <$> existsSInteger s)
-newVars (FOTIntMod n) = nextId <&> \s-> (IntegerLabel s, VIntMod n <$> existsSInteger s)
-newVars (FOTVec n FOTBit) =
-  if n == 0
-    then nextId <&> \s-> (WordLabel s, return (vWord (literalSWord 0 0)))
-    else nextId <&> \s-> (WordLabel s, vWord <$> existsSWord s (fromIntegral n))
-newVars (FOTVec n tp) = do
-  (labels, vals) <- V.unzip <$> V.replicateM (fromIntegral n) (newVars tp)
-  return (VecLabel labels, VVector <$> traverse (fmap ready) vals)
-newVars (FOTArray{}) = fail "FOTArray unimplemented for backend"
-newVars (FOTTuple ts) = do
-  (labels, vals) <- V.unzip <$> traverse newVars (V.fromList ts)
-  return (TupleLabel labels, vTuple <$> traverse (fmap ready) (V.toList vals))
-newVars (FOTRec tm) = do
-  (labels, vals) <- unzipMap <$> (traverse newVars tm :: StateT Int IO (Map FieldName (Labeler, Symbolic SValue)))
-  return (RecLabel labels, vRecord <$> traverse (fmap ready) (vals :: (Map FieldName (Symbolic SValue))))
+newVars :: String -> FirstOrderType -> StateT Int IO (Labeler, Symbolic SValue)
+newVars nm fot =
+  case fot of
+    FOTBit ->
+      nextId' nm <&> \s -> (BoolLabel s, vBool <$> existsSBool s)
+    FOTInt ->
+      nextId' nm <&> \s -> (IntegerLabel s, vInteger <$> existsSInteger s)
+    FOTIntMod n ->
+      nextId' nm <&> \s -> (IntegerLabel s, VIntMod n <$> existsSInteger s)
+    FOTVec 0 FOTBit ->
+      pure (ZeroWidthWordLabel, pure (vWord (literalSWord 0 0)))
+    FOTVec n FOTBit ->
+      nextId' nm <&> \s -> (WordLabel s, vWord <$> existsSWord s (fromIntegral n))
+    FOTVec n tp ->
+      do let f i = newVars (nm ++ "." ++ show i) tp
+         (labels, vals) <- V.unzip <$> V.generateM (fromIntegral n) f
+         pure (VecLabel labels, VVector <$> traverse (fmap ready) vals)
+    FOTArray{} ->
+      fail "FOTArray unimplemented for backend"
+    FOTTuple ts ->
+      do let f i t = newVars (nm ++ "." ++ show i) t
+         (labels, vals) <- V.unzip <$> V.imapM f (V.fromList ts)
+         pure (TupleLabel labels, vTuple <$> traverse (fmap ready) (V.toList vals))
+    FOTRec tm ->
+      do let f k t = newVars (nm ++ "." ++ Text.unpack k) t
+         (labels, vals) <- unzipMap <$> (Map.traverseWithKey f tm)
+         pure (RecLabel labels, vRecord <$> traverse (fmap ready) vals)
 
 
 getLabels ::
@@ -718,6 +732,8 @@ getLabels ls d args
   getLabel (WordLabel s)    = FOVWord (cvKind cv) (cvToInteger cv)
     where cv = d Map.! s
 
+  getLabel ZeroWidthWordLabel = FOVWord 0 0
+
   getLabel (VecLabel ns)
     | V.null ns = error "getLabel of empty vector"
     | otherwise = fovVec t vs

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

@@ -1193,6 +1193,9 @@ parseUninterpretedSAW sym st sc ref trm app ty =
     VIntType
       -> VInt  <$> mkUninterpretedSAW sym st ref trm app BaseIntegerRepr
 
+    VIntModType n
+      -> VIntMod n <$> mkUninterpretedSAW sym st ref (ArgTermFromIntMod n trm) app BaseIntegerRepr
+
     -- 0 width bitvector is a constant
     VVecType 0 VBoolType
       -> return $ VWord ZBV
@@ -1247,6 +1250,8 @@ mkUninterpretedSAW sym st ref trm (UnintApp nm args tys) ret =
 data ArgTerm
   = ArgTermVar
   | ArgTermBVZero -- ^ scBvNat 0 0
+  | ArgTermToIntMod Natural ArgTerm -- ^ toIntMod n x
+  | ArgTermFromIntMod Natural ArgTerm -- ^ fromIntMod n x
   | ArgTermVector Term [ArgTerm] -- ^ element type, elements
   | ArgTermUnit
   | ArgTermPair ArgTerm ArgTerm
@@ -1278,6 +1283,16 @@ reconstructArgTerm atrm sc ts =
           do z <- scNat sc 0
              x <- scBvNat sc z z
              return (x, ts0)
+        ArgTermToIntMod n at1 ->
+          do n' <- scNat sc n
+             (x1, ts1) <- parse at1 ts0
+             x <- scToIntMod sc n' x1
+             pure (x, ts1)
+        ArgTermFromIntMod n at1 ->
+          do n' <- scNat sc n
+             (x1, ts1) <- parse at1 ts0
+             x <- scFromIntMod sc n' x1
+             pure (x, ts1)
         ArgTermVector ty ats ->
           do (xs, ts1) <- parseList ats ts0
              x <- scVector sc ty xs
@@ -1336,6 +1351,7 @@ mkArgTerm sc ty val =
     (_, VWord ZBV)       -> return ArgTermBVZero     -- 0-width bitvector is a constant
     (_, VWord (DBV _))   -> return ArgTermVar
     (VUnitType, VUnit)   -> return ArgTermUnit
+    (VIntModType n, VIntMod _ _) -> pure (ArgTermToIntMod n ArgTermVar)
 
     (VVecType _ ety, VVector vv) ->
       do vs <- traverse force (V.toList vv)
@@ -1359,6 +1375,10 @@ mkArgTerm sc ty val =
          x <- scCtorApp sc i xs
          return (ArgTermConst x)
 
+    (_, TValue tval) ->
+      do x <- termOfTValue sc tval
+         pure (ArgTermConst x)
+
     _ -> fail $ "could not create uninterpreted function argument of type " ++ show ty
 
 termOfTValue :: SharedContext -> TValue (What4 sym) -> IO Term

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

@@ -49,6 +49,7 @@ import           Data.Ratio
 import           Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 import           Data.Word(Word64)
+import           Data.Text (Text)
 import qualified Data.Text as Text
 
 import           What4.BaseTypes
@@ -148,7 +149,7 @@ baseSCType sym sc bt =
 
 -- | Create a new symbolic variable.
 sawCreateVar :: SAWCoreState n
-             -> String                                       -- ^ the name of the variable
+             -> Text -- ^ the name of the variable
              -> SC.Term
              -> IO SC.Term
 sawCreateVar st nm tp = do
@@ -539,7 +540,7 @@ evaluateExpr sym st sc cache = f []
         B.UninterpVarKind -> do
           tp <- baseSCType sym sc (B.bvarType bv)
           SAWExpr <$> sawCreateVar st nm tp
-            where nm = Text.unpack $ solverSymbolAsText $ B.bvarName bv
+            where nm = solverSymbolAsText $ B.bvarName bv
         B.LatchVarKind ->
           unsupported sym "SAW backend does not support latch variables"
         B.QuantifierVarKind -> do

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

@@ -8,11 +8,14 @@ Portability : non-portable (language extensions)
 -}
 
 module Verifier.SAW.Constant (scConst) where
+
+import Data.Text (Text)
+
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Rewriter
 import Verifier.SAW.Conversion
 
-scConst :: SharedContext -> String -> Term -> IO Term
+scConst :: SharedContext -> Text -> Term -> IO Term
 scConst sc name t = do
   ty <- scTypeOf sc t
   ty' <- rewriteSharedTerm sc (addConvs natConversions emptySimpset) ty

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

@@ -68,7 +68,6 @@ import qualified Data.List as List
 import qualified Data.Map as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
-import qualified Data.Text as Text
 import Control.Monad.Trans.Writer.Strict
 import Numeric.Natural
 
@@ -222,7 +221,7 @@ scMatch sc pat term =
              let fvy = looseVars y `intersectBitSets` (completeBitSet depth)
              guard (fvy `unionBitSets` fvj == fvj)
              let fixVar t (nm, ty) =
-                   do v <- scFreshGlobal sc (Text.unpack nm) ty
+                   do v <- scFreshGlobal sc nm ty
                       let Just ec = R.asExtCns v
                       t' <- instantiateVar sc 0 v t
                       return (t', ec)
@@ -882,7 +881,7 @@ doHoistIfs sc ss hoistCache itePat = go
        goF _ (Pi nm tp body) = goBinder scPi nm tp body
 
        goBinder close nm tp body = do
-           (ec, body') <- scOpenTerm sc (Text.unpack nm) tp 0 body
+           (ec, body') <- scOpenTerm sc nm tp 0 body
            (body'', conds) <- go body'
            let (stuck, float) = List.partition (\(_,ecs) -> Set.member ec ecs) conds
 

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

@@ -185,6 +185,7 @@ module Verifier.SAW.SharedTerm
     -- *** IntMod
   , scIntModType
   , scToIntMod
+  , scFromIntMod
     -- *** Vectors
   , scAppend
   , scJoin
@@ -392,17 +393,16 @@ scShowTerm sc opts t =
      pure (showTermWithNames opts env t)
 
 -- | Create a global variable with the given identifier (which may be "_") and type.
-scFreshEC :: SharedContext -> String -> a -> IO (ExtCns a)
-scFreshEC sc x tp = do
-  i   <- scFreshGlobalVar sc
-  let x' = Text.pack x
-  let uri = scFreshNameURI x' i
-  let nmi = ImportedName uri [x',Text.pack (x <> "#" <>  show i)]
-  scRegisterName sc i nmi
-  pure (EC i nmi tp)
+scFreshEC :: SharedContext -> Text -> a -> IO (ExtCns a)
+scFreshEC sc x tp =
+  do i <- scFreshGlobalVar sc
+     let uri = scFreshNameURI x i
+     let nmi = ImportedName uri [x, x <> "#" <>  Text.pack (show i)]
+     scRegisterName sc i nmi
+     pure (EC i nmi tp)
 
 -- | Create a global variable with the given identifier (which may be "_") and type.
-scFreshGlobal :: SharedContext -> String -> Term -> IO Term
+scFreshGlobal :: SharedContext -> Text -> Term -> IO Term
 scFreshGlobal sc x tp = scExtCns sc =<< scFreshEC sc x tp
 
 -- | Returns shared term associated with ident.
@@ -1213,7 +1213,7 @@ scSort sc s = scFlatTermF sc (Sort s)
 scNat :: SharedContext -> Natural -> IO Term
 scNat sc n = scFlatTermF sc (NatLit n)
 
--- | Create a literal term (of saw-core type @String@) from a 'String'.
+-- | Create a literal term (of saw-core type @String@) from a 'Text'.
 scString :: SharedContext -> Text -> IO Term
 scString sc s = scFlatTermF sc (StringLit s)
 
@@ -1324,7 +1324,7 @@ scFunAll :: SharedContext
          -> IO Term
 scFunAll sc argTypes resultType = foldrM (scFun sc) resultType argTypes
 
--- | Create a lambda term from a parameter name (as a 'String'), parameter type
+-- | Create a lambda term from a parameter name (as a 'LocalName'), parameter type
 -- (as a 'Term'), and a body. Regarding deBruijn indices, in the body of the
 -- function, an index of 0 refers to the bound parameter.
 scLambda :: SharedContext
@@ -1378,7 +1378,7 @@ scLocalVar sc i = scTermF sc (LocalVar i)
 -- indices. If the body contains any ExtCns variables, they will be
 -- abstracted over and reapplied to the resulting constant.
 scConstant :: SharedContext
-           -> String -- ^ The name
+           -> Text   -- ^ The name
            -> Term   -- ^ The body
            -> Term   -- ^ The type
            -> IO Term
@@ -1830,6 +1830,12 @@ scIntModType sc n = scGlobalApply sc "Prelude.IntMod" [n]
 scToIntMod :: SharedContext -> Term -> Term -> IO Term
 scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
 
+-- | Convert an integer mod n to an integer.
+--
+-- > fromIntMod : (n : Nat) -> IntMod n -> Integer;
+scFromIntMod :: SharedContext -> Term -> Term -> IO Term
+scFromIntMod sc n x = scGlobalApply sc "Prelude.fromIntMod" [n, x]
+
 
 -- Primitive operations on bitvectors
 
@@ -2337,7 +2343,7 @@ scTreeSize = fst . go (0, Map.empty)
 -- | `openTerm sc nm ty i body` replaces the loose deBruijn variable `i`
 --   with a fresh external constant (with name `nm`, and type `ty`) in `body`.
 scOpenTerm :: SharedContext
-         -> String
+         -> Text
          -> Term
          -> DeBruijnIndex
          -> Term