Misc patches leading to the term model

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

@@ -1636,6 +1636,7 @@ asCryptolTypeValue v =
 
     -- TODO?
     SC.VPiType _nm _v1 (SC.VDependentPi _) -> Nothing
+    SC.VStringType -> Nothing
     SC.VRecordType{} -> Nothing
     SC.VRecursorType{} -> Nothing
     SC.VTyTerm{} -> Nothing

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

@@ -715,10 +715,10 @@ evaluateExpr sym st sc cache = f []
            y' <- SC.scBvToNat sc (natValue w) =<< f env y
            SC.scGlobalApply sc (SC.mkIdent SC.preludeName "rotateR") [n,bit,x',y']
         B.BVConcat _ x y -> fmap SAWExpr $ do
-           n <- SC.scNat sc (natValue (bvWidth x))
-           m <- SC.scNat sc (natValue (bvWidth y))
+           m <- SC.scNat sc (natValue (bvWidth x))
+           n <- SC.scNat sc (natValue (bvWidth y))
            t <- SC.scBoolType sc
-           join (SC.scAppend sc t n m <$> f env x <*> f env y)
+           join (SC.scAppend sc m n t <$> f env x <*> f env y)
         B.BVSelect start num x -> fmap SAWExpr $ do
            i <- SC.scNat sc (natValue (bvWidth x) - natValue num - natValue start)
            n <- SC.scNat sc (natValue num)

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

@@ -187,6 +187,11 @@ module Verifier.SAW.SharedTerm
   , scIntModType
   , scToIntMod
   , scFromIntMod
+  , scIntModEq
+  , scIntModAdd
+  , scIntModSub
+  , scIntModMul
+  , scIntModNeg
     -- *** Vectors
   , scAppend
   , scJoin
@@ -240,6 +245,7 @@ module Verifier.SAW.SharedTerm
   , getConstantSet
   , scInstantiateExt
   , scAbstractExts
+  , scAbstractExtsEtaCollapse
   , scGeneralizeExts
   , incVars
   , scUnfoldConstants
@@ -1624,7 +1630,7 @@ scIte sc t b x y = scGlobalApply sc "Prelude.ite" [t, b, x, y]
 -- > append : (m n : Nat) -> (e : sort 0) -> Vec m e -> Vec n e -> Vec (addNat m n) e;
 scAppend :: SharedContext -> Term -> Term -> Term ->
             Term -> Term -> IO Term
-scAppend sc t m n x y = scGlobalApply sc "Prelude.append" [m, n, t, x, y]
+scAppend sc m n t x y = scGlobalApply sc "Prelude.append" [m, n, t, x, y]
 
 -- | Create a term applying @Prelude.join@ to a vector of vectors.
 --
@@ -1909,6 +1915,36 @@ scToIntMod sc n x = scGlobalApply sc "Prelude.toIntMod" [n, x]
 scFromIntMod :: SharedContext -> Term -> Term -> IO Term
 scFromIntMod sc n x = scGlobalApply sc "Prelude.fromIntMod" [n, x]
 
+-- | Equality test on the @IntMod@ type
+--
+-- > intModEq  : (n : Nat) -> IntMod n -> IntMod n -> Bool;
+scIntModEq :: SharedContext -> Term -> Term -> Term -> IO Term
+scIntModEq sc n x y = scGlobalApply sc "Prelude.intModEq" [n,x,y]
+
+-- | Addition of @IntMod@ values
+--
+-- > intModAdd : (n : Nat) -> IntMod n -> IntMod n -> IntMod n;
+scIntModAdd :: SharedContext -> Term -> Term -> Term -> IO Term
+scIntModAdd sc n x y = scGlobalApply sc "Prelude.intModAdd" [n,x,y]
+
+-- | Subtraction of @IntMod@ values
+--
+-- > intModSub : (n : Nat) -> IntMod n -> IntMod n -> IntMod n;
+scIntModSub :: SharedContext -> Term -> Term -> Term -> IO Term
+scIntModSub sc n x y = scGlobalApply sc "Prelude.intModSub" [n,x,y]
+
+-- | Multiplication of @IntMod@ values
+--
+-- > intModMul : (n : Nat) -> IntMod n -> IntMod n -> IntMod n;
+scIntModMul :: SharedContext -> Term -> Term -> Term -> IO Term
+scIntModMul sc n x y = scGlobalApply sc "Prelude.intModMul" [n,x,y]
+
+-- | Negation (additive inverse) of @IntMod@ values
+--
+-- > intModNeg : (n : Nat) -> IntMod n -> IntMod n;
+scIntModNeg :: SharedContext -> Term -> Term -> IO Term
+scIntModNeg sc n x = scGlobalApply sc "Prelude.intModNeg" [n,x]
+
 
 -- Primitive operations on bitvectors
 
@@ -2359,6 +2395,28 @@ scAbstractExts sc exts x = loop (zip (inits exts) exts)
     loop [] = scExtsToLocals sc exts x
 
 
+-- | Abstract over the given list of external constants by wrapping
+--   the given term with lambdas and replacing the external constant
+--   occurrences with the appropriate local variables.  However,
+--   the term will be eta-collapsed as far as possible, so unnecessary
+--   lambdas will simply be omitted.
+scAbstractExtsEtaCollapse :: SharedContext -> [ExtCns Term] -> Term -> IO Term
+scAbstractExtsEtaCollapse sc = \exts tm -> loop (reverse exts) tm
+  where
+    -- we eta-collapsed all the variables, nothing more to do
+    loop [] tm = pure tm
+
+    -- the final variable to abstract is applied to the
+    -- term, and does not appear elsewhere in the term,
+    -- so we can eta-collapse.
+    loop (ec:exts) (asApp -> Just (f,asExtCns -> Just ec'))
+      | ec == ec', not (Set.member ec (getAllExtSet f))
+      = loop exts f
+
+    -- cannot eta-collapse, do abstraction as usual
+    loop exts tm = scAbstractExts sc (reverse exts) tm
+
+
 -- | Generalize over the given list of external constants by wrapping
 -- the given term with foralls and replacing the external constant
 -- occurrences with the appropriate local variables.

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

@@ -142,10 +142,10 @@ evalTermF cfg lam recEval tf env =
                                     if inBitSet 0 (looseVars t2) then
                                       pure (VDependentPi (\x -> toTValue <$> lam t2 ((x,v) : env)))
                                     else
-                                      do val <- delay (panic "evalTermF"
-                                                         ["nondependent Pi type forced its value"
-                                                         , showTerm (Unshared tf)])
-                                         VNondependentPi . toTValue <$> lam t2 ((val,v) : env)
+                                      do -- put dummy values in the environment; the term should never reference them
+                                         let val = ready VUnit
+                                         let tp  = VUnitType
+                                         VNondependentPi . toTValue <$> lam t2 ((val,tp):env)
                                   return $ TValue $ VPiType nm v body
 
     LocalVar i              -> force (fst (env !! i))

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

@@ -32,6 +32,7 @@ module Verifier.SAW.Simulator.Prims
 , intFun
 , intModFun
 , tvalFun
+, stringFun
 , wordFun
 , vectorFun
 , Pack
@@ -134,6 +135,11 @@ tvalFun = PrimFilterFun "expected type value" r
   where r (TValue tv) = pure tv
         r _ = mzero
 
+stringFun :: VMonad l => (Text -> Prim l) -> Prim l
+stringFun = PrimFilterFun "expected string value" r
+  where r (VString x) = pure x
+        r _ = mzero
+
 -- | A primitive that requires a packed word argument
 wordFun :: VMonad l => Pack l -> (VWord l -> Prim l) -> Prim l
 wordFun pack = PrimFilterFun "expected word" r
@@ -346,11 +352,16 @@ constMap bp = Map.fromList
   , ("Prelude.coerce", coerceOp)
   , ("Prelude.bvNat", bvNatOp bp)
   , ("Prelude.bvToNat", bvToNatOp)
-  , ("Prelude.error", errorOp)
   , ("Prelude.fix", fixOp)
+  , ("Prelude.error", errorOp)
+
+  -- Strings
+  , ("Prelude.String", PrimValue (TValue VStringType))
+  , ("Prelude.equalString", equalStringOp bp)
+
   -- Overloaded
   , ("Prelude.ite", iteOp bp)
-  , ("Prelude.iteDep", iteOp bp)
+  , ("Prelude.iteDep", iteDepOp bp)
   -- SMT Arrays
   , ("Prelude.Array", arrayTypeOp)
   , ("Prelude.arrayConstant", arrayConstantOp bp)
@@ -636,6 +647,15 @@ natCaseOp =
     else do s' <- force s
             apply s' (ready (VNat (n - 1)))
 
+--------------------------------------------------------------------------------
+-- Strings
+
+equalStringOp :: VMonad l => BasePrims l -> Prim l
+equalStringOp bp =
+  stringFun $ \x ->
+  stringFun $ \y ->
+    Prim (VBool <$> bpBool bp (x == y))
+
 --------------------------------------------------------------------------------
 
 -- Vec :: (n :: Nat) -> (a :: sort 0) -> sort 0;
@@ -1051,20 +1071,32 @@ natToIntOp = natFun $ \x -> PrimValue $ VInt (toInteger x)
 errorOp :: VMonad l => Prim l
 errorOp =
   constFun $
-  strictFun $ \x -> Prim $
-  case x of
-    VString s -> Prim.userError (Text.unpack s)
-    _ -> Prim.userError "unknown error"
+  stringFun $ \msg ->
+  Prim $ Prim.userError (Text.unpack msg)
 
 ------------------------------------------------------------
 -- Conditionals
 
+iteDepOp :: (HasCallStack, VMonadLazy l, Show (Extra l)) => BasePrims l -> Prim l
+iteDepOp bp =
+  primFun $ \_p ->
+  boolFun $ \b ->
+  primFun $ \x ->
+  primFun $ \y ->
+  Prim $
+    case bpAsBool bp b of
+      Just True  -> force x
+      Just False -> force y
+      Nothing ->
+        unsupportedPrimitive "Symbolic backend" "iteDep" 
+
 iteOp :: (HasCallStack, VMonadLazy l, Show (Extra l)) => BasePrims l -> Prim l
 iteOp bp =
   tvalFun $ \tp ->
   boolFun $ \b ->
   primFun $ \x ->
-  primFun $ \y -> Prim $
+  primFun $ \y ->
+  Prim $
     lazyMuxValue bp tp b (force x) (force y)
 
 lazyMuxValue ::

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

@@ -82,6 +82,7 @@ data TValue l
   | VIntModType !Natural
   | VArrayType !(TValue l) !(TValue l)
   | VPiType LocalName !(TValue l) !(PiBody l)
+  | VStringType
   | VUnitType
   | VPairType !(TValue l) !(TValue l)
   | VDataType !(PrimName (TValue l)) ![Value l] ![Value l]
@@ -198,6 +199,7 @@ instance Show (Extra l) => Show (TValue l) where
   showsPrec p v =
     case v of
       VBoolType      -> showString "Bool"
+      VStringType    -> showString "String"
       VIntType       -> showString "Integer"
       VIntModType n  -> showParen True (showString "IntMod " . shows n)
       VArrayType{}   -> showString "Array"
@@ -323,6 +325,7 @@ asFirstOrderTypeTValue v =
       FOTRec . Map.fromList <$>
         mapM (traverse asFirstOrderTypeTValue) elem_tps
 
+    VStringType   -> Nothing
     VPiType{}   -> Nothing
     VDataType{} -> Nothing
     VSort{}     -> Nothing
@@ -351,6 +354,8 @@ suffixTValue tv =
       do a' <- suffixTValue a
          b' <- suffixTValue b
          Just ("_Pair" ++ a' ++ b')
+
+    VStringType -> Nothing
     VDataType {} -> Nothing
     VRecordType {} -> Nothing
     VSort {} -> Nothing

src/SAWScript/Builtins.hs

@@ -1218,6 +1218,14 @@ eval_list t = do
   ts <- io $ traverse (scAt sc n' a' (ttTerm t)) idxs
   return (map (TypedTerm (TypedTermSchema (C.tMono a))) ts)
 
+default_typed_term :: TypedTerm -> TopLevel TypedTerm
+default_typed_term tt = do
+  sc <- getSharedContext
+  cenv <- fmap rwCryptol getTopLevelRW
+  let cfg = CEnv.meSolverConfig (CEnv.eModuleEnv cenv)
+  opts <- getOptions
+  io $ defaultTypedTerm opts sc cfg tt
+
 -- | Default the values of the type variables in a typed term.
 defaultTypedTerm :: Options -> SharedContext -> C.SolverConfig -> TypedTerm -> IO TypedTerm
 defaultTypedTerm opts sc cfg tt@(TypedTerm (TypedTermSchema schema) trm)

src/SAWScript/Interpreter.hs

@@ -902,6 +902,11 @@ primitives = Map.fromList
     , "variables."
     ]
 
+  , prim "default_term" "Term -> Term"
+    (funVal1 default_typed_term)
+    Experimental
+    [ "Apply Cryptol defaulting rules to the given term." ]
+
   , prim "sbv_uninterpreted"   "String -> Term -> TopLevel Uninterp"
     (pureVal sbvUninterpreted)
     Deprecated

src/SAWScript/SBVParser.hs

@@ -113,7 +113,7 @@ parseSBVExpr opts sc unint nodes size (SBV.SBVApp operator sbvs) =
                    b <- scBoolType sc
                    -- SBV append takes the most-significant argument
                    -- first, as SAWCore does.
-                   scAppend sc b s1 s2 arg1 arg2
+                   scAppend sc s1 s2 b arg1 arg2
             _ -> fail "parseSBVExpr: wrong number of arguments for append"
       SBV.BVLkUp indexSize resultSize ->
           do (size1 : inSizes, arg1 : args) <- liftM unzip $ mapM (parseSBV sc nodes) sbvs
@@ -385,7 +385,7 @@ scAppendAll sc ((x, size1) : xs) =
        s1 <- scNat sc (fromInteger size1)
        s2 <- scNat sc (fromInteger size2)
        y <- scAppendAll sc xs
-       scAppend sc b s1 s2 x y
+       scAppend sc s1 s2 b x y
 
 typOf :: SBV.SBVPgm -> Typ
 typOf (SBV.SBVPgm (_, irtype, _, _, _, _)) = parseIRType irtype