From 7d4268a581bcf75bf891e56339b0ccdb8260202b Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 30 Apr 2021 13:13:19 -0400 Subject: [PATCH 01/11] Use read_only=True in test_salsa20.py In addition, test `Salsa20CryptContract` on more inputs, just like the SAWScript version does, to make sure that it is working robustly. Fixes #1280. --- .../python/tests/saw/test_salsa20.py | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/saw-remote-api/python/tests/saw/test_salsa20.py b/saw-remote-api/python/tests/saw/test_salsa20.py index c8cfd2389c..b28a37978d 100644 --- a/saw-remote-api/python/tests/saw/test_salsa20.py +++ b/saw-remote-api/python/tests/saw/test_salsa20.py @@ -7,7 +7,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tuple[FreshVar, SetupVal]: """Add to``Contract`` ``c`` an allocation of a pointer of type ``ty`` initialized to an unknown fresh value. - + :returns A fresh variable bound to the pointers initial value and the newly allocated pointer. (The fresh variable will be assigned ``name`` if provided/available.)""" var = c.fresh_var(ty, name) @@ -15,7 +15,7 @@ def ptr_to_fresh(c : Contract, ty : LLVMType, name : Optional[str] = None) -> Tu return (var, ptr) def oneptr_update_func(c : Contract, ty : LLVMType, fn_name : str) -> None: - """Upcates contract ``c`` to declare calling it with a pointer of type ``ty`` + """Updates contract ``c`` to declare calling it with a pointer of type ``ty`` updates that pointer with the result, which is equal to calling the Cryptol function ``fn_name``.""" (x, x_p) = ptr_to_fresh(c, ty) @@ -92,8 +92,8 @@ class ExpandContract(Contract): def specification(self): k = self.fresh_var(LLVMArrayType(i8, 32)) n = self.fresh_var(LLVMArrayType(i8, 16)) - k_p = self.alloc(LLVMArrayType(i8, 32)) - n_p = self.alloc(LLVMArrayType(i8, 16)) + k_p = self.alloc(LLVMArrayType(i8, 32), read_only = True) + n_p = self.alloc(LLVMArrayType(i8, 16), read_only = True) ks_p = self.alloc(LLVMArrayType(i8, 64)) self.points_to(k_p, k) self.points_to(n_p, n) @@ -117,8 +117,8 @@ def specification(self): self.execute_func(k_p, v_p, cryptol('0 : [32]'), m_p, cryptol(f'{self.size!r} : [32]')) - self.returns(cryptol('0 : [32]')) self.points_to(m_p, cryptol("Salsa20_encrypt")((k, v, m))) + self.returns(cryptol('0 : [32]')) class Salsa20EasyTest(unittest.TestCase): def test_salsa20(self): @@ -146,8 +146,12 @@ def test_salsa20(self): self.assertIs(hash_result.is_success(), True) expand_result = llvm_verify(mod, 's20_expand32', ExpandContract(), lemmas=[hash_result]) self.assertIs(expand_result.is_success(), True) - crypt_result = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(63), lemmas=[expand_result]) - self.assertIs(crypt_result.is_success(), True) + crypt_result_63 = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(63), lemmas=[expand_result]) + self.assertIs(crypt_result_63.is_success(), True) + crypt_result_64 = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(64), lemmas=[expand_result]) + self.assertIs(crypt_result_64.is_success(), True) + crypt_result_65 = llvm_verify(mod, 's20_crypt32', Salsa20CryptContract(65), lemmas=[expand_result]) + self.assertIs(crypt_result_65.is_success(), True) if __name__ == "__main__": unittest.main() From 33034267e1aa9c7281365c4860b8c6cd0f8a7711 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 30 Apr 2021 08:02:00 -0700 Subject: [PATCH 02/11] Convert more uses of `String` to `Text`. --- .../src/Verifier/SAW/TypedTerm.hs | 3 ++- .../SAW/Simulator/What4/ReturnTrip.hs | 5 ++-- saw-core/src/Verifier/SAW/Constant.hs | 5 +++- saw-core/src/Verifier/SAW/Rewriter.hs | 5 ++-- saw-core/src/Verifier/SAW/SharedTerm.hs | 25 +++++++++---------- .../src/SAWServer/JVMCrucibleSetup.hs | 3 +-- .../src/SAWServer/LLVMCrucibleSetup.hs | 3 +-- src/SAWScript/Builtins.hs | 6 ++--- src/SAWScript/Crucible/Common/Setup/Type.hs | 5 ++-- src/SAWScript/Crucible/JVM/Builtins.hs | 3 ++- src/SAWScript/Crucible/LLVM/Builtins.hs | 7 +++--- .../Crucible/LLVM/ResolveSetupValue.hs | 1 + .../Crucible/LLVM/Skeleton/Builtins.hs | 6 ++--- src/SAWScript/JavaExpr.hs | 3 ++- src/SAWScript/Proof.hs | 10 ++++---- src/SAWScript/Prover/MRSolver.hs | 3 +-- 16 files changed, 49 insertions(+), 44 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs index e166d024ae..0480ba4ac9 100644 --- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs +++ b/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 diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs index 90c517d667..28c366cadf 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Constant.hs b/saw-core/src/Verifier/SAW/Constant.hs index 8b124445bc..2b064868f3 100644 --- a/saw-core/src/Verifier/SAW/Constant.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/Rewriter.hs b/saw-core/src/Verifier/SAW/Rewriter.hs index 18d18a4fcf..6db48c95b0 100644 --- a/saw-core/src/Verifier/SAW/Rewriter.hs +++ b/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 diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 1680dc138e..165f7e4fb3 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -392,17 +392,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 +1212,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 +1323,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 +1377,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 @@ -2337,7 +2336,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 diff --git a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs index e300be4e36..99b9a9bab9 100644 --- a/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs @@ -26,7 +26,6 @@ import Data.Foldable ( traverse_ ) import Data.Map (Map) import qualified Data.Map as Map import Data.Maybe ( maybeToList ) -import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -120,7 +119,7 @@ interpretJVMSetup fileReader bic cenv0 ss = evalStateT (traverse_ go ss) (mempty go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return -- TODO: do we really want two names here? go (SetupFresh name@(ServerName n) debugName ty) = - do t <- lift $ jvm_fresh_var (T.unpack debugName) ty + do t <- lift $ jvm_fresh_var debugName ty (env, cenv) <- get put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv) save name (Val (MS.SetupTerm t)) diff --git a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs index 8f38d952f8..ee2cbf0d18 100644 --- a/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs @@ -25,7 +25,6 @@ import Data.Aeson (FromJSON(..), withObject, (.:)) import Data.ByteString (ByteString) import Data.Map (Map) import qualified Data.Map as Map -import qualified Data.Text as T import qualified Cryptol.Parser.AST as P import Cryptol.Utils.Ident (mkIdent) @@ -102,7 +101,7 @@ compileLLVMContract fileReader bic ghostEnv cenv0 c = Nothing -> return () where setupFresh (ContractVar n dn ty) = - do t <- llvm_fresh_var (T.unpack dn) (llvmType ty) + do t <- llvm_fresh_var dn (llvmType ty) return (n, t) setupState allocs (env, cenv) vars = diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index baf2f26fde..9a38fd73fe 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -130,7 +130,7 @@ showPrim v = do opts <- fmap rwPPOpts getTopLevelRW return (SV.showsPrecValue opts 0 v "") -definePrim :: String -> TypedTerm -> TopLevel TypedTerm +definePrim :: Text -> TypedTerm -> TopLevel TypedTerm definePrim name (TypedTerm schema rhs) = do sc <- getSharedContext ty <- io $ Cryptol.importSchema sc Cryptol.emptyEnv schema @@ -526,7 +526,7 @@ goal_assume = do sc <- SV.scriptTopLevel getSharedContext execTactic (tacticAssume sc) -goal_intro :: String -> ProofScript TypedTerm +goal_intro :: Text -> ProofScript TypedTerm goal_intro s = do sc <- SV.scriptTopLevel getSharedContext execTactic (tacticIntro sc s) @@ -986,7 +986,7 @@ check_goal = fixPos :: Pos fixPos = PosInternal "FIXME" -freshSymbolicPrim :: String -> C.Schema -> TopLevel TypedTerm +freshSymbolicPrim :: Text -> C.Schema -> TopLevel TypedTerm freshSymbolicPrim x schema@(C.Forall [] [] ct) = do sc <- getSharedContext cty <- io $ Cryptol.importType sc Cryptol.emptyEnv ct diff --git a/src/SAWScript/Crucible/Common/Setup/Type.hs b/src/SAWScript/Crucible/Common/Setup/Type.hs index 8d61570a21..055ec60bd3 100644 --- a/src/SAWScript/Crucible/Common/Setup/Type.hs +++ b/src/SAWScript/Crucible/Common/Setup/Type.hs @@ -35,6 +35,7 @@ module SAWScript.Crucible.Common.Setup.Type import Control.Lens import Control.Monad.State (StateT) import Control.Monad.IO.Class (MonadIO(liftIO)) +import Data.Text (Text) import qualified Cryptol.TypeCheck.Type as Cryptol (Type) import qualified Verifier.SAW.Cryptol as Cryptol (importType, emptyEnv) @@ -101,7 +102,7 @@ addCondition cond = currentState . MS.csConditions %= (cond : ) freshTypedExtCns :: MonadIO m => SharedContext {- ^ shared context -} -> - String {- ^ variable name -} -> + Text {- ^ variable name -} -> Cryptol.Type {- ^ variable type -} -> CrucibleSetupT arch m TypedExtCns freshTypedExtCns sc name cty = @@ -116,7 +117,7 @@ freshTypedExtCns sc name cty = freshVariable :: MonadIO m => SharedContext {- ^ shared context -} -> - String {- ^ variable name -} -> + Text {- ^ variable name -} -> Cryptol.Type {- ^ variable type -} -> CrucibleSetupT arch m TypedTerm freshVariable sc name cty = diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index 3dbff7ee9e..424e820019 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -55,6 +55,7 @@ import qualified Data.Map as Map import Data.Set (Set) import qualified Data.Set as Set import qualified Data.Sequence as Seq +import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V import Data.Void (absurd) @@ -955,7 +956,7 @@ typeOfJavaType jty = -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. jvm_fresh_var :: - String {- ^ variable name -} -> + Text {- ^ variable name -} -> JavaType {- ^ variable type -} -> JVMSetupM TypedTerm {- ^ fresh typed term -} jvm_fresh_var name jty = diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index ceac360f54..a2f56ebfa0 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -106,6 +106,7 @@ import qualified Data.HashMap.Strict as HashMap import qualified Data.Set as Set import Data.Sequence (Seq) import qualified Data.Sequence as Seq +import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V import Prettyprinter @@ -1439,7 +1440,7 @@ setupArg sc sym ecRef tp = do freshGlobal cty sc_tp = do ecs <- readIORef ecRef let len = Seq.length ecs - ec <- scFreshEC sc ("arg_"++show len) sc_tp + ec <- scFreshEC sc ("arg_" <> Text.pack (show len)) sc_tp writeIORef ecRef (ecs Seq.|> TypedExtCns cty ec) scFlatTermF sc (ExtCns ec) @@ -1649,7 +1650,7 @@ cryptolTypeOfActual dl mt = -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. llvm_fresh_var :: - String {- ^ variable name -} -> + Text {- ^ variable name -} -> L.Type {- ^ variable type -} -> LLVMCrucibleSetupM TypedTerm {- ^ fresh typed term -} llvm_fresh_var name lty = @@ -1665,7 +1666,7 @@ llvm_fresh_var name lty = Just cty -> Setup.freshVariable sc name cty llvm_fresh_cryptol_var :: - String -> + Text -> Cryptol.Schema -> LLVMCrucibleSetupM TypedTerm llvm_fresh_cryptol_var name s = diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 5154b621cc..f5a4f4713c 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -10,6 +10,7 @@ Stability : provisional {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} diff --git a/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs b/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs index 4f24128885..879d3ef960 100644 --- a/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Skeleton/Builtins.hs @@ -202,7 +202,7 @@ buildArg arg idx $ arg ^. argSkelType . typeSkelLLVMType pure (Just val, Nothing, arg ^. argSkelName) where - ident = maybe ("arg" <> show idx) Text.unpack $ arg ^. argSkelName + ident = maybe ("arg" <> Text.pack (show idx)) id $ arg ^. argSkelName skeleton_prestate :: FunctionSkeleton -> @@ -237,7 +237,7 @@ rebuildArg (arg, prearg) idx -> LLVM.Array (fromIntegral $ s ^. sizeGuessElems) pt | otherwise -> pt _ -> pt - ident = maybe ("arg" <> show idx) Text.unpack nm + ident = maybe ("arg" <> Text.pack (show idx)) id nm in do val' <- llvm_fresh_var ident t llvm_points_to True ptr $ anySetupTerm val' @@ -255,7 +255,7 @@ skeleton_poststate skel prestate = do case skel ^. funSkelRet . typeSkelLLVMType of LLVM.PrimType LLVM.Void -> pure () t -> do - ret <- llvm_fresh_var ("return value of " <> (Text.unpack $ skel ^. funSkelName)) t + ret <- llvm_fresh_var ("return value of " <> (skel ^. funSkelName)) t llvm_return $ anySetupTerm ret pure $ SkeletonState{..} diff --git a/src/SAWScript/JavaExpr.hs b/src/SAWScript/JavaExpr.hs index 836b3b5a89..b3846b40a5 100644 --- a/src/SAWScript/JavaExpr.hs +++ b/src/SAWScript/JavaExpr.hs @@ -68,6 +68,7 @@ import Language.JVM.Common (ppFldId) import Data.List (intercalate) import Data.List.Split +import Data.Text (Text) import qualified Data.Text as Text import qualified Data.Vector as V import Text.Read hiding (lift) @@ -209,7 +210,7 @@ data LogicExpr = } deriving (Show) -scJavaValue :: SharedContext -> Term -> String -> IO Term +scJavaValue :: SharedContext -> Term -> Text -> IO Term scJavaValue sc ty name = do scFreshGlobal sc name ty diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs index fea336a5b2..709db3b9b5 100644 --- a/src/SAWScript/Proof.hs +++ b/src/SAWScript/Proof.hs @@ -188,7 +188,7 @@ evalProp sc unints (Prop p) = Just t -> pure t Nothing -> fail "goal_eval: expected EqTrue" - ecs <- traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args + ecs <- traverse (\(nm, ty) -> scFreshEC sc nm ty) args vars <- traverse (scExtCns sc) ecs t0 <- instantiateVarList sc 0 (reverse vars) body' @@ -726,7 +726,7 @@ predicateToSATQuery sc unintSet tm0 = case evalFOT mmap tp of Nothing -> fail ("predicateToSATQuery: expected first order type: " ++ showTerm tp) Just fot -> - do ec <- scFreshEC sc (Text.unpack lnm) tp + do ec <- scFreshEC sc lnm tp etm <- scExtCns sc ec body' <- instantiateVar sc 0 etm body processTerm mmap (Map.insert ec fot vars) body' @@ -779,7 +779,7 @@ propToSATQuery sc unintSet prop = case evalFOT mmap tp of Nothing -> fail ("propToSATQuery: expected first order type: " ++ showTerm tp) Just fot -> - do ec <- scFreshEC sc (Text.unpack lnm) tp + do ec <- scFreshEC sc lnm tp etm <- scExtCns sc ec body' <- instantiateVar sc 0 etm body processTerm mmap (Map.insert ec fot vars) xs body' @@ -830,12 +830,12 @@ goalApply sc rule goal = applyFirst (asPiLists (unProp rule)) -- for the binder. Return the generated fresh term. tacticIntro :: (F.MonadFail m, MonadIO m) => SharedContext -> - String {- ^ Name to give to the variable. If empty, will be chosen automatically from the goal. -} -> + Text {- ^ Name to give to the variable. If empty, will be chosen automatically from the goal. -} -> Tactic m TypedTerm tacticIntro sc usernm = Tactic \goal -> case asPi (unProp (goalProp goal)) of Just (nm, tp, body) -> - do let name = if null usernm then Text.unpack nm else usernm + do let name = if Text.null usernm then nm else usernm xv <- liftIO $ scFreshEC sc name tp x <- liftIO $ scExtCns sc xv tt <- liftIO $ mkTypedTerm sc x diff --git a/src/SAWScript/Prover/MRSolver.hs b/src/SAWScript/Prover/MRSolver.hs index 41ccc8cfcd..df5c8b3160 100644 --- a/src/SAWScript/Prover/MRSolver.hs +++ b/src/SAWScript/Prover/MRSolver.hs @@ -13,7 +13,6 @@ import Control.Monad.Reader import Control.Monad.State import Control.Monad.Except import Data.Semigroup -import qualified Data.Text as Text import Prettyprinter @@ -614,7 +613,7 @@ askMRSolver sc smt_conf timeout t1 t2 = flip evalStateT init_st $ runExceptT $ do mrSolveEq (Type tp1) (Type tp2) let (pi_args, ret_tp) = asPiList tp1 - vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal (Text.unpack x) x_tp) pi_args + vars <- mapM (\(x, x_tp) -> liftSC2 scFreshGlobal x x_tp) pi_args case asCompMApp ret_tp of Just _ -> return () Nothing -> throwError (NotCompFunType tp1) From c085c1830bdc1cb6a4fce9749dc25d7f0f34c86a Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Mon, 3 May 2021 16:42:47 -0700 Subject: [PATCH 03/11] Reimplement `refreshTerms` to register names in the naming environment. Fixes #869. --- src/SAWScript/Crucible/JVM/Override.hs | 4 ++-- src/SAWScript/Crucible/LLVM/Override.hs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 8825777f22..fe851433cc 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -381,8 +381,8 @@ refreshTerms sc ss = OM (termSub %= Map.union extension) where freshenTerm (TypedExtCns _cty ec) = - do new <- liftIO $ do i <- scFreshGlobalVar sc - scExtCns sc (EC i (ecName ec) (ecType ec)) + do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec) + new <- liftIO $ scExtCns sc ec' return (ecVarIndex ec, new) ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 423b35d66c..311648a35b 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -709,8 +709,8 @@ refreshTerms sc ss = OM (termSub %= Map.union extension) where freshenTerm (TypedExtCns _cty ec) = - do new <- liftIO $ do i <- scFreshGlobalVar sc - scExtCns sc (EC i (ecName ec) (ecType ec)) + do ec' <- liftIO $ scFreshEC sc (toShortName (ecName ec)) (ecType ec) + new <- liftIO $ scExtCns sc ec' return (ecVarIndex ec, new) ------------------------------------------------------------------------ From 1ffea324724126886a8eb09d6d121abd2c2e751a Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 28 Apr 2021 15:57:24 -0700 Subject: [PATCH 04/11] cryptol-saw-core: Fix tuple encoding used by `proveEq`. Fixes #1166. --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 37 ++++++++++++-------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 2e293779c3..3814999b86 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/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 From 2906402d86b1349a10d648a496becbcc601faa2f Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 29 Apr 2021 10:53:55 -0700 Subject: [PATCH 05/11] saw-core-sbv: Handle zero-width bitvectors properly in counterexamples. Fixes #1182. --- saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index d400089d04..a5e65d7f6f 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -667,6 +667,7 @@ data Labeler = BoolLabel String | IntegerLabel String | WordLabel String + | ZeroWidthWordLabel | VecLabel (Vector Labeler) | TupleLabel (Vector Labeler) | RecLabel (Map FieldName Labeler) @@ -684,7 +685,7 @@ 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))) + then pure (ZeroWidthWordLabel, pure (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) @@ -718,6 +719,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 From 63d03061b9a8107f28f62db053cec03813cf510c Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 29 Apr 2021 11:49:58 -0700 Subject: [PATCH 06/11] saw-core-sbv: Use meaningful user variable names in smtlib2 output. Fixes #1144. --- .../src/Verifier/SAW/Simulator/SBV.hs | 53 ++++++++++++------- 1 file changed, 33 insertions(+), 20 deletions(-) diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index a5e65d7f6f..eac92e4d92 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/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) @@ -674,29 +675,41 @@ data 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 pure (ZeroWidthWordLabel, pure (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 :: From a24bb18504b2d59da8fea65c9a4f9c6b76a30408 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 30 Apr 2021 12:24:21 -0700 Subject: [PATCH 07/11] Make `goal_eval_unint` work with polymorphic functions. Fixes #1045. --- saw-core-what4/src/Verifier/SAW/Simulator/What4.hs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 05d1495748..be2114cd59 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -1359,6 +1359,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 From f23a4fca5d100b05c5f7f03668440dbcc66d0cb7 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 4 May 2021 13:58:43 -0700 Subject: [PATCH 08/11] Redefine `precContains` more simply in terms of `(<=)`. --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 77b6416ae4..8b88bdea3d 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -119,23 +119,13 @@ data Prec | PrecProd -- ^ Nonterminal 'ProductTerm' | PrecApp -- ^ Nonterminal 'AppTerm' | PrecArg -- ^ Nonterminal 'AtomTerm' + deriving (Eq, Ord) -- | Test if the first precedence "contains" the second, meaning that terms at -- the latter precedence level can be printed in the context of the former -- without parentheses. --- --- NOTE: we write this explicitly here, instead of generating it from an 'Ord' --- instance, so that readers of this code understand it and know what it is. precContains :: Prec -> Prec -> Bool -precContains _ PrecArg = True -precContains PrecArg _ = False -precContains _ PrecApp = True -precContains PrecApp _ = False -precContains _ PrecProd = True -precContains PrecProd _ = False -precContains _ PrecLambda = True -precContains PrecLambda _ = False -precContains PrecNone PrecNone = True +precContains x y = x <= y -- | Optionally print parentheses around a document, iff the incoming, outer -- precedence (listed first) contains (as in 'precContains') the required From 4414514d594c4e3d24d219d8d1c6e8a69d442717 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 4 May 2021 14:00:21 -0700 Subject: [PATCH 09/11] Add new pretty-printer precedence level for comma-separated lists. This lets us print pair values using infix ',' with parens in the right places. Fixes #1147. --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 29 ++++++++++++------------ 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index 8b88bdea3d..fd3407e47d 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -114,9 +114,10 @@ depthAllowed _ _ = True -- | Precedence levels, each of which corresponds to a parsing nonterminal data Prec - = PrecNone -- ^ Nonterminal 'Term' + = PrecNone -- ^ Nonterminal 'Term' or "sepBy(Term, ',')" + | PrecTerm -- ^ Nonterminal 'Term' | PrecLambda -- ^ Nonterminal 'LTerm' - | PrecProd -- ^ Nonterminal 'ProductTerm' + | PrecProd -- ^ Nonterminal 'ProdTerm' | PrecApp -- ^ Nonterminal 'AppTerm' | PrecArg -- ^ Nonterminal 'AtomTerm' deriving (Eq, Ord) @@ -416,7 +417,7 @@ ppFlatTermF prec tf = Primitive ec -> annotate PrimitiveStyle <$> ppBestName (ecName ec) UnitValue -> return "(-empty-)" UnitType -> return "#(-empty-)" - PairValue x y -> ppPair prec <$> ppTerm' PrecLambda x <*> ppTerm' PrecNone y + PairValue x y -> ppPair prec <$> ppTerm' PrecTerm x <*> ppTerm' PrecNone y PairType x y -> ppPairType prec <$> ppTerm' PrecApp x <*> ppTerm' PrecProd y PairLeft t -> ppProj "1" <$> ppTerm' PrecArg t PairRight t -> ppProj "2" <$> ppTerm' PrecArg t @@ -428,7 +429,7 @@ ppFlatTermF prec tf = RecursorApp d params p_ret cs_fs ixs arg -> do params_pp <- mapM (ppTerm' PrecArg) params p_ret_pp <- ppTerm' PrecArg p_ret - fs_pp <- mapM (ppTerm' PrecNone . snd) cs_fs + fs_pp <- mapM (ppTerm' PrecTerm . snd) cs_fs ixs_pp <- mapM (ppTerm' PrecArg) ixs arg_pp <- ppTerm' PrecArg arg return $ @@ -439,14 +440,14 @@ ppFlatTermF prec tf = cs_fs fs_pp] ++ ixs_pp ++ [arg_pp]) RecordType alist -> - ppRecord True <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecNone t) alist + ppRecord True <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecTerm t) alist RecordValue alist -> - ppRecord False <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecNone t) alist + ppRecord False <$> mapM (\(fld,t) -> (fld,) <$> ppTerm' PrecTerm t) alist RecordProj e fld -> ppProj fld <$> ppTerm' PrecArg e Sort s -> return $ viaShow s NatLit i -> ppNat <$> (ppOpts <$> ask) <*> return (toInteger i) ArrayValue _ args -> - ppArrayValue <$> mapM (ppTerm' PrecNone) (V.toList args) + ppArrayValue <$> mapM (ppTerm' PrecTerm) (V.toList args) StringLit s -> return $ viaShow s ExtCns cns -> annotate ExtCnsStyle <$> ppBestName (ecName cns) @@ -608,7 +609,7 @@ ppWithBoundCtx [] m = (mempty ,) <$> m ppWithBoundCtx ((x,tp):ctx) m = (\tp_d (x', (ctx_d, ret)) -> (parens (ppTypeConstraint (pretty x') tp_d) <+> ctx_d, ret)) - <$> ppTerm' PrecNone tp <*> withBoundVarM x (ppWithBoundCtx ctx m) + <$> ppTerm' PrecTerm tp <*> withBoundVarM x (ppWithBoundCtx ctx m) -- | Pretty-print a term, also adding let-bindings for all subterms that occur -- more than once at the same binding level @@ -625,7 +626,7 @@ ppTermInCtx :: PPOpts -> [LocalName] -> Term -> SawDoc ppTermInCtx opts ctx trm = runPPM opts emptySAWNamingEnv $ flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $ - ppTermWithMemoTable PrecNone True trm + ppTermWithMemoTable PrecTerm True trm renderSawDoc :: PPOpts -> SawDoc -> String renderSawDoc ppOpts doc = @@ -646,7 +647,7 @@ scPrettyTermInCtx opts ctx trm = renderSawDoc opts $ runPPM opts emptySAWNamingEnv $ flip (Fold.foldl' (\m x -> snd <$> withBoundVarM x m)) ctx $ - ppTermWithMemoTable PrecNone False trm + ppTermWithMemoTable PrecTerm False trm -- | Pretty-print a term and render it to a string @@ -662,7 +663,7 @@ showTerm t = scPrettyTerm defaultPPOpts t -- more than once at the same binding level ppTermWithNames :: PPOpts -> SAWNamingEnv -> Term -> SawDoc ppTermWithNames opts ne trm = - runPPM opts ne $ ppTermWithMemoTable PrecNone True trm + runPPM opts ne $ ppTermWithMemoTable PrecTerm True trm showTermWithNames :: PPOpts -> SAWNamingEnv -> Term -> String showTermWithNames opts ne trm = @@ -696,10 +697,10 @@ ppPPModule opts (PPModule importNames decls) = ppWithBoundCtx dtIndices (return $ viaShow dtSort) <*> mapM (\(ctorName,ctorType) -> ppTypeConstraint (ppIdent ctorName) <$> - ppTerm' PrecNone ctorType) + ppTerm' PrecTerm ctorType) dtCtors) ppDecl (PPDefDecl defIdent defType defBody) = - ppDef (ppIdent defIdent) <$> ppTerm' PrecNone defType <*> + ppDef (ppIdent defIdent) <$> ppTerm' PrecTerm defType <*> case defBody of - Just body -> Just <$> ppTerm' PrecNone body + Just body -> Just <$> ppTerm' PrecTerm body Nothing -> return Nothing From da521bfbfe6ce983cd9cf7bd29a016fdb1975822 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 5 May 2021 08:05:27 -0700 Subject: [PATCH 10/11] Rename `PrecNone` to more suggestive name `PrecCommas`; fix haddocks. --- saw-core/src/Verifier/SAW/Term/Pretty.hs | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index fd3407e47d..d28e96c98d 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -114,12 +114,12 @@ depthAllowed _ _ = True -- | Precedence levels, each of which corresponds to a parsing nonterminal data Prec - = PrecNone -- ^ Nonterminal 'Term' or "sepBy(Term, ',')" - | PrecTerm -- ^ Nonterminal 'Term' - | PrecLambda -- ^ Nonterminal 'LTerm' - | PrecProd -- ^ Nonterminal 'ProdTerm' - | PrecApp -- ^ Nonterminal 'AppTerm' - | PrecArg -- ^ Nonterminal 'AtomTerm' + = PrecCommas -- ^ Nonterminal @sepBy(Term, \',\')@ + | PrecTerm -- ^ Nonterminal @Term@ + | PrecLambda -- ^ Nonterminal @LTerm@ + | PrecProd -- ^ Nonterminal @ProdTerm@ + | PrecApp -- ^ Nonterminal @AppTerm@ + | PrecArg -- ^ Nonterminal @AtomTerm@ deriving (Eq, Ord) -- | Test if the first precedence "contains" the second, meaning that terms at @@ -337,7 +337,7 @@ ppLetBlock defs body = -- | Pretty-print pairs as "(x, y)" ppPair :: Prec -> SawDoc -> SawDoc -> SawDoc -ppPair prec x y = ppParensPrec prec PrecNone (group (vcat [x <> pretty ',', y])) +ppPair prec x y = ppParensPrec prec PrecCommas (group (vcat [x <> pretty ',', y])) -- | Pretty-print pair types as "x * y" ppPairType :: Prec -> SawDoc -> SawDoc -> SawDoc @@ -417,7 +417,7 @@ ppFlatTermF prec tf = Primitive ec -> annotate PrimitiveStyle <$> ppBestName (ecName ec) UnitValue -> return "(-empty-)" UnitType -> return "#(-empty-)" - PairValue x y -> ppPair prec <$> ppTerm' PrecTerm x <*> ppTerm' PrecNone y + PairValue x y -> ppPair prec <$> ppTerm' PrecTerm x <*> ppTerm' PrecCommas y PairType x y -> ppPairType prec <$> ppTerm' PrecApp x <*> ppTerm' PrecProd y PairLeft t -> ppProj "1" <$> ppTerm' PrecArg t PairRight t -> ppProj "2" <$> ppTerm' PrecArg t From 4a471b61f30e144a01bb0ddc6d0ed96169f0f338 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 28 Apr 2021 13:08:15 -0700 Subject: [PATCH 11/11] Make `goal_eval_unint` handle `Z n` types. Fixes #1120. --- .../src/Verifier/SAW/Simulator/What4.hs | 16 ++++++++++++++++ saw-core/src/Verifier/SAW/SharedTerm.hs | 7 +++++++ 2 files changed, 23 insertions(+) diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index be2114cd59..cab2c98114 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/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) diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index 165f7e4fb3..dc9063e696 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -185,6 +185,7 @@ module Verifier.SAW.SharedTerm -- *** IntMod , scIntModType , scToIntMod + , scFromIntMod -- *** Vectors , scAppend , scJoin @@ -1829,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