From 3c70694969021e450110e0aa95af0136020cfa9d Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 25 May 2021 14:50:36 -0700 Subject: [PATCH 1/7] Remove the obsolete `SAWScript.VerificationCheck` and `SAWScript.PathVC` modules. --- saw-script.cabal | 2 - src/SAWScript/PathVC.hs | 64 ----------------------- src/SAWScript/VerificationCheck.hs | 84 ------------------------------ 3 files changed, 150 deletions(-) delete mode 100644 src/SAWScript/PathVC.hs delete mode 100644 src/SAWScript/VerificationCheck.hs diff --git a/saw-script.cabal b/saw-script.cabal index 28e3ee7f21..1310c8c86b 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -120,7 +120,6 @@ library SAWScript.Options SAWScript.Panic SAWScript.Parser - SAWScript.PathVC SAWScript.Proof SAWScript.Position SAWScript.SBVParser @@ -130,7 +129,6 @@ library SAWScript.MGU SAWScript.Utils SAWScript.Value - SAWScript.VerificationCheck SAWScript.Crucible.Common SAWScript.Crucible.Common.MethodSpec diff --git a/src/SAWScript/PathVC.hs b/src/SAWScript/PathVC.hs deleted file mode 100644 index af005fc209..0000000000 --- a/src/SAWScript/PathVC.hs +++ /dev/null @@ -1,64 +0,0 @@ -{- | -Module : SAWScript.PathVC -Description : Assumptions and assertions for symbolic execution paths. -License : BSD3 -Maintainer : atomb -Stability : provisional --} -module SAWScript.PathVC where - -import Control.Monad.State -import Prettyprinter - -import Verifier.SAW.SharedTerm -import Verifier.SAW.Term.Pretty (SawDoc) - -import SAWScript.VerificationCheck - --- | Describes the verification result arising from one symbolic execution path. -data PathVC l = PathVC { - pvcStartLoc :: l - , pvcEndLoc :: Maybe l - -- | Assumptions on inputs. - , pvcAssumptions :: Term - -- | Static errors found in path. - , pvcStaticErrors :: [SawDoc] - -- | What to verify for this result. - , pvcChecks :: [VerificationCheck] - } - -ppPathVC :: PathVC l -> SawDoc -ppPathVC pvc = - nest 2 $ - vcat [ pretty "Path VC:" - , nest 2 $ - vcat [ pretty "Assumptions:" - , ppTerm defaultPPOpts (pvcAssumptions pvc) - ] - , nest 2 $ vcat $ - pretty "Static errors:" : - pvcStaticErrors pvc - , nest 2 $ vcat $ - pretty "Checks:" : - map ppCheck (pvcChecks pvc) - ] - -type PathVCGenerator l m = StateT (PathVC l) m - --- | Add verification condition to list. -pvcgAssertEq :: (Monad m) => - String -> Term -> Term - -> PathVCGenerator l m () -pvcgAssertEq name jv sv = - modify $ \pvc -> pvc { pvcChecks = EqualityCheck name jv sv : pvcChecks pvc } - -pvcgAssert :: (Monad m) => - String -> Term -> PathVCGenerator l m () -pvcgAssert nm v = - modify $ \pvc -> pvc { pvcChecks = AssertionCheck nm v : pvcChecks pvc } - -pvcgFail :: Monad m => - SawDoc -> PathVCGenerator l m () -pvcgFail msg = - modify $ \pvc -> pvc { pvcStaticErrors = msg : pvcStaticErrors pvc } - diff --git a/src/SAWScript/VerificationCheck.hs b/src/SAWScript/VerificationCheck.hs deleted file mode 100644 index 2bd4694259..0000000000 --- a/src/SAWScript/VerificationCheck.hs +++ /dev/null @@ -1,84 +0,0 @@ -{- | -Module : SAWScript.VerificationCheck -Description : Equality and predicate assertions. -License : BSD3 -Maintainer : atomb -Stability : provisional --} -module SAWScript.VerificationCheck where - -import Control.Monad -import Prettyprinter - -import qualified Cryptol.TypeCheck.AST as C -import qualified Cryptol.Backend.Monad as CV -import qualified Cryptol.Eval.Value as CV -import qualified Cryptol.Eval.Concrete as CV -import Verifier.SAW.Cryptol (exportValueWithSchema, scCryptolType) -import Verifier.SAW.SharedTerm -import Verifier.SAW.Simulator.Concrete (CValue) -import Verifier.SAW.Term.Pretty (SawDoc) - -import Verifier.SAW.Cryptol (scCryptolEq) -import qualified SAWScript.Value as SV (PPOpts(..), cryptolPPOpts) - -data VerificationCheck - = AssertionCheck String Term - -- ^ A predicate to check with a name and term. - | EqualityCheck String -- Name of value to compare - Term -- Value returned by implementation. - Term -- Expected value in Spec. - -- ^ Check that equality assertion is true. - -vcName :: VerificationCheck -> String -vcName (AssertionCheck nm _) = nm -vcName (EqualityCheck nm _ _) = nm - --- | Returns goal that one needs to prove. -vcGoal :: SharedContext -> VerificationCheck -> IO Term -vcGoal _ (AssertionCheck _ n) = return n -vcGoal sc (EqualityCheck _ x y) = scCryptolEq sc x y - -type CounterexampleFn = (Term -> IO CValue) -> IO SawDoc - --- | Returns documentation for check that fails. -vcCounterexample :: SharedContext -> SV.PPOpts -> VerificationCheck -> CounterexampleFn -vcCounterexample _ opts (AssertionCheck nm n) _ = do - let opts' = defaultPPOpts { ppBase = SV.ppOptsBase opts } - return $ pretty ("Assertion " ++ nm ++ " is unsatisfied:") <+> - ppTerm opts' n -vcCounterexample sc opts (EqualityCheck nm impNode specNode) evalFn = - do ln <- evalFn impNode - sn <- evalFn specNode - lty <- scTypeOf sc impNode - lct <- scCryptolType sc lty - sty <- scTypeOf sc specNode - sct <- scCryptolType sc sty - let lschema = (C.Forall [] [] lct) - sschema = (C.Forall [] [] sct) - unless (lschema == sschema) $ fail "Mismatched schemas in counterexample" - let lv = exportValueWithSchema lschema ln - sv = exportValueWithSchema sschema sn - opts' = SV.cryptolPPOpts opts - -- Grr. Different pretty-printers. - lv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' =<< lv) - sv_doc <- CV.runEval mempty (CV.ppValue CV.Concrete opts' =<< sv) - - return $ - vcat - [ pretty nm - , nest 2 (pretty "Encountered: " <+> pretty (show lv_doc)) - , nest 2 (pretty "Expected: " <+> pretty (show sv_doc)) - ] - -ppCheck :: VerificationCheck -> SawDoc -ppCheck (AssertionCheck nm tm) = - hsep [ pretty (nm ++ ":") - , ppTerm defaultPPOpts tm - ] -ppCheck (EqualityCheck nm tm tm') = - hsep [ pretty (nm ++ ":") - , ppTerm defaultPPOpts tm - , pretty ":=" - , ppTerm defaultPPOpts tm' - ] From 20ddad9b1ff1ca4fb8fdf6d805ce774cc3f52b35 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 30 Apr 2021 16:11:05 -0700 Subject: [PATCH 2/7] Add simulator value support for term model evaluation. This mostly just adds `LocalName` values to functions and Pi types so meaningful names can be round-tripped. We also add a `VTyTerm` constructor to `TValue` for types that cannot be fully evaluated (because they are blocked on a variable, etc). --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 2 +- .../src/Verifier/SAW/Simulator/SBV.hs | 4 +- .../src/Verifier/SAW/Simulator/What4.hs | 8 +- saw-core/src/Verifier/SAW/Simulator.hs | 6 +- saw-core/src/Verifier/SAW/Simulator/Prims.hs | 22 ++--- saw-core/src/Verifier/SAW/Simulator/Value.hs | 83 +++++++++++++++++-- saw-core/src/Verifier/SAW/Term/Pretty.hs | 1 + 7 files changed, 96 insertions(+), 30 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index 33617f7bc6..a149e290a5 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -1590,7 +1590,7 @@ asCryptolTypeValue v = case C.tIsTuple t2 of Just ts -> return (C.tTuple (t1 : ts)) Nothing -> return (C.tTuple [t1, t2]) - SC.VPiType v1 f -> do + SC.VPiType _nm v1 f -> do case v1 of -- if we see that the parameter is a Cryptol.Num, it's a -- pretty good guess that it originally was a diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index eac92e4d92..0ff394bc7e 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -274,7 +274,7 @@ flattenSValue nm v = do VNat n -> return ([], "_" ++ show n) TValue (suffixTValue -> Just s) -> return ([], s) - VFun _ -> fail $ "Cannot create uninterpreted higher-order function " ++ show nm + VFun _ _ -> fail $ "Cannot create uninterpreted higher-order function " ++ show nm _ -> fail $ "Cannot create uninterpreted function " ++ show nm ++ " with argument " ++ show v vWord :: SWord -> SValue @@ -584,7 +584,7 @@ sbvSolveBasic sc addlPrims unintSet t = do parseUninterpreted :: [SVal] -> String -> TValue SBV -> IO SValue parseUninterpreted cws nm ty = case ty of - (VPiType _ f) + (VPiType _ _ f) -> return $ strictFun $ \x -> do (cws', suffix) <- flattenSValue nm x diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 3f4d48ebd4..6367035fdf 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -731,7 +731,7 @@ parseUninterpreted :: TValue (What4 sym) -> IO (SValue sym) parseUninterpreted sym ref app ty = case ty of - VPiType _ f + VPiType _ _ f -> return $ strictFun $ \x -> do app' <- applyUnintApp sym app x @@ -852,7 +852,7 @@ applyUnintApp sym app0 v = VNat n -> return (suffixUnintApp ("_" ++ show n) app0) TValue (suffixTValue -> Just s) -> return (suffixUnintApp s app0) - VFun _ -> + VFun _ _ -> fail $ "Cannot create uninterpreted higher-order function " ++ show (stringOfUnintApp app0) @@ -888,7 +888,7 @@ w4Solve sym sc satq = argTypes :: IsSymExprBuilder sym => TValue (What4 sym) -> IO [TValue (What4 sym)] argTypes v = case v of - VPiType v1 f -> + VPiType _nm v1 f -> do x <- delay (fail "argTypes: unsupported dependent SAW-Core type") v2 <- f x vs <- argTypes v2 @@ -1178,7 +1178,7 @@ parseUninterpretedSAW :: IO (SValue (B.ExprBuilder n st fs)) parseUninterpretedSAW sym st sc ref trm app ty = case ty of - VPiType t1 f + VPiType _nm t1 f -> return $ strictFun $ \x -> do app' <- applyUnintApp sym app x diff --git a/saw-core/src/Verifier/SAW/Simulator.hs b/saw-core/src/Verifier/SAW/Simulator.hs index 7d9a1266b9..5f6d18bb50 100644 --- a/saw-core/src/Verifier/SAW/Simulator.hs +++ b/saw-core/src/Verifier/SAW/Simulator.hs @@ -120,9 +120,9 @@ evalTermF cfg lam recEval tf env = App t1 t2 -> do v <- recEval t1 x <- recEvalDelay t2 apply v x - Lambda _ _ t -> return $ VFun (\x -> lam t (x : env)) - Pi _ t1 t2 -> do v <- toTValue <$> recEval t1 - return $ TValue $ VPiType v (\x -> toTValue <$> lam t2 (x : env)) + Lambda nm _ t -> return $ VFun nm (\x -> lam t (x : env)) + Pi nm t1 t2 -> do v <- toTValue <$> recEval t1 + return $ TValue $ VPiType nm v (\x -> toTValue <$> lam t2 (x : env)) LocalVar i -> force (env !! i) Constant ec t -> do ec' <- traverse (fmap toTValue . recEval) ec maybe (recEval t) id (simConstant cfg tf ec') diff --git a/saw-core/src/Verifier/SAW/Simulator/Prims.hs b/saw-core/src/Verifier/SAW/Simulator/Prims.hs index 896bdcaa06..9a2bb9f077 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Prims.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Prims.hs @@ -316,7 +316,7 @@ toWord pack (VVector vv) = pack =<< V.mapM (liftM toBool . force) vv toWord _ x = panic $ unwords ["Verifier.SAW.Simulator.toWord", show x] toWordPred :: (VMonad l, Show (Extra l)) => Value l -> VWord l -> MBool l -toWordPred (VFun f) = fmap toBool . f . ready . VWord +toWordPred (VFun _ f) = fmap toBool . f . ready . VWord toWordPred x = panic $ unwords ["Verifier.SAW.Simulator.toWordPred", show x] toBits :: (VMonad l, Show (Extra l)) => Unpack l -> Value l -> @@ -433,7 +433,7 @@ coerceOp = constFun $ constFun $ constFun $ - VFun force + VFun "x" force ------------------------------------------------------------ -- Nat primitives @@ -573,8 +573,8 @@ ltNatOp bp = natCaseOp :: (VMonad l, Show (Extra l)) => Value l natCaseOp = constFun $ - VFun $ \z -> return $ - VFun $ \s -> return $ + VFun "z" $ \z -> return $ + VFun "s" $ \s -> return $ natFun' "natCase" $ \n -> if n == 0 then force z @@ -640,7 +640,7 @@ atWithDefaultOp :: (VMonadLazy l, Show (Extra l)) => BasePrims l -> Value l atWithDefaultOp bp = natFun $ \n -> return $ constFun $ - VFun $ \d -> return $ + VFun "d" $ \d -> return $ strictFun $ \x -> return $ strictFun $ \idx -> case idx of @@ -666,7 +666,7 @@ updOp bp = constFun $ vectorFun (bpUnpack bp) $ \xv -> return $ strictFun $ \idx -> return $ - VFun $ \y -> + VFun "y" $ \y -> case idx of VNat i | toInteger i < toInteger (V.length xv) @@ -853,7 +853,7 @@ shiftOp :: forall l. shiftOp bp vecOp wordIntOp wordOp = natFun $ \n -> return $ constFun $ - VFun $ \z -> return $ + VFun "z" $ \z -> return $ strictFun $ \xs -> return $ strictFun $ \y -> case y of @@ -1113,7 +1113,7 @@ foldrOp unpack = constFun $ constFun $ strictFun $ \f -> return $ - VFun $ \z -> return $ + VFun "z" $ \z -> return $ strictFun $ \xs -> do let g x m = do fx <- apply f x y <- delay m @@ -1220,8 +1220,8 @@ iteOp :: (VMonadLazy l, Show (Extra l)) => BasePrims l -> Value l iteOp bp = constFun $ strictFun $ \b -> return $ - VFun $ \x -> return $ - VFun $ \y -> lazyMuxValue bp (toBool b) (force x) (force y) + VFun "x" $ \x -> return $ + VFun "y" $ \y -> lazyMuxValue bp (toBool b) (force x) (force y) lazyMuxValue :: (VMonadLazy l, Show (Extra l)) => @@ -1241,7 +1241,7 @@ muxValue :: forall l. muxValue bp b = value where value :: Value l -> Value l -> MValue l - value (VFun f) (VFun g) = return $ VFun $ \a -> do + value (VFun nm f) (VFun _ g) = return $ VFun nm $ \a -> do x <- f a y <- g a value x y diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs index 377d180fa7..62901bd807 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Value.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Value.hs @@ -38,6 +38,7 @@ import Verifier.SAW.FiniteValue (FiniteType(..), FirstOrderType(..)) import Verifier.SAW.SharedTerm import Verifier.SAW.TypedAST import Verifier.SAW.Utils (panic) +import Verifier.SAW.Term.Pretty import Verifier.SAW.Simulator.MonadLazy @@ -49,7 +50,7 @@ Values are parameterized by the /name/ of an instantiation. The concrete parameters to use are computed from the name using a collection of type families (e.g., 'EvalM', 'VBool', etc.). -} data Value l - = VFun !(Thunk l -> MValue l) + = VFun !LocalName !(Thunk l -> MValue l) | VUnit | VPair (Thunk l) (Thunk l) -- TODO: should second component be strict? | VCtorApp !Ident !(Vector (Thunk l)) @@ -75,12 +76,31 @@ data TValue l | VIntType | VIntModType !Natural | VArrayType !(TValue l) !(TValue l) - | VPiType !(TValue l) !(Thunk l -> EvalM l (TValue l)) + | VPiType LocalName !(TValue l) !(Thunk l -> EvalM l (TValue l)) | VUnitType | VPairType !(TValue l) !(TValue l) | VDataType !Ident ![Value l] | VRecordType ![(FieldName, TValue l)] | VSort !Sort + | VTyTerm !Sort !Term + +-- | Neutral terms represent computations that are blocked +-- because some internal term cannot be evaluated +-- (e.g., because it is a variable, because it's definition +-- is being hidden, etc.) +data NeutralTerm + = NeutralBox Term -- the thing blocking evaluation + | NeutralPairLeft NeutralTerm -- left pair projection + | NeutralPairRight NeutralTerm -- right pair projection + | NeutralRecordProj NeutralTerm FieldName -- record projection + | NeutralApp NeutralTerm Term -- function application + | NeutralRecursor -- recursor application + Ident -- inductive type being eliminated + [Term] -- parameters of the inductive type + Term -- return type (AKA intent, AKA motive) + [(Ident,Term)] -- elimination functions for the constructors + [Term] -- indices for the inductive type + NeutralTerm -- argument being elminated type Thunk l = Lazy (EvalM l) (Value l) @@ -133,13 +153,15 @@ type instance Extra (WithM m l) = Extra l -------------------------------------------------------------------------------- strictFun :: VMonad l => (Value l -> MValue l) -> Value l -strictFun f = VFun (\x -> force x >>= f) +-- TODO, make callers provide a name? +strictFun f = VFun "x" (\x -> force x >>= f) pureFun :: VMonad l => (Value l -> Value l) -> Value l -pureFun f = VFun (\x -> liftM f (force x)) +-- TODO, make callers provide a name? +pureFun f = VFun "x" (\x -> liftM f (force x)) constFun :: VMonad l => Value l -> Value l -constFun x = VFun (\_ -> return x) +constFun x = VFun "_" (\_ -> return x) toTValue :: HasCallStack => Value l -> TValue l toTValue (TValue x) = x @@ -180,7 +202,7 @@ instance Show (Extra l) => Show (TValue l) where VIntType -> showString "Integer" VIntModType n -> showParen True (showString "IntMod " . shows n) VArrayType{} -> showString "Array" - VPiType t _ -> showParen True + VPiType _ t _ -> showParen True (shows t . showString " -> ...") VUnitType -> showString "#()" VPairType x y -> showParen True (shows x . showString " * " . shows y) @@ -194,6 +216,8 @@ instance Show (Extra l) => Show (TValue l) where . showString " " . showParen True (showsPrec p a) VSort s -> shows s + VTyTerm _ tm -> shows tm + data Nil = Nil instance Show Nil where @@ -235,8 +259,8 @@ valRecordProj v _ = ["Not a record value:", show v] apply :: (HasCallStack, VMonad l, Show (Extra l)) => Value l -> Thunk l -> MValue l -apply (VFun f) x = f x -apply (TValue (VPiType _ f)) x = TValue <$> f x +apply (VFun _ f) x = f x +apply (TValue (VPiType _ _ f)) x = TValue <$> f x apply v _x = panic "Verifier.SAW.Simulator.Value.apply" ["Not a function value:", show v] applyAll :: (VMonad l, Show (Extra l)) => Value l -> [Thunk l] -> MValue l @@ -296,6 +320,7 @@ asFirstOrderTypeTValue v = VPiType{} -> Nothing VDataType{} -> Nothing VSort{} -> Nothing + VTyTerm{} -> Nothing -- | A (partial) injective mapping from type values to strings. These -- are intended to be useful as suffixes for names of type instances @@ -313,7 +338,7 @@ suffixTValue tv = do a' <- suffixTValue a b' <- suffixTValue b Just ("_Array" ++ a' ++ b') - VPiType _ _ -> Nothing + VPiType _ _ _ -> Nothing VUnitType -> Just "_Unit" VPairType a b -> do a' <- suffixTValue a @@ -322,3 +347,43 @@ suffixTValue tv = VDataType {} -> Nothing VRecordType {} -> Nothing VSort {} -> Nothing + VTyTerm{} -> Nothing + +neutralToTerm :: NeutralTerm -> Term +neutralToTerm = loop + where + loop (NeutralBox tm) = tm + loop (NeutralPairLeft nt) = + Unshared (FTermF (PairLeft (loop nt))) + loop (NeutralPairRight nt) = + Unshared (FTermF (PairRight (loop nt))) + loop (NeutralRecordProj nt f) = + Unshared (FTermF (RecordProj (loop nt) f)) + loop (NeutralApp nt arg) = + Unshared (App (loop nt) arg) + loop (NeutralRecursor d ps p_ret cs_fs ixs x) = + Unshared (FTermF (RecursorApp d ps p_ret cs_fs ixs (loop x))) + +neutralToSharedTerm :: SharedContext -> NeutralTerm -> IO Term +neutralToSharedTerm sc = loop + where + loop (NeutralBox tm) = pure tm + loop (NeutralPairLeft nt) = + scFlatTermF sc . PairLeft =<< loop nt + loop (NeutralPairRight nt) = + scFlatTermF sc . PairRight =<< loop nt + loop (NeutralRecordProj nt f) = + do tm <- loop nt + scFlatTermF sc (RecordProj tm f) + loop (NeutralApp nt arg) = + do tm <- loop nt + scApply sc tm arg + loop (NeutralRecursor d ps p_ret cs_fs ixs nt) = + do tm <- loop nt + scFlatTermF sc (RecursorApp d ps p_ret cs_fs ixs tm) + +ppNeutral :: PPOpts -> NeutralTerm -> SawDoc +ppNeutral opts = ppTerm opts . neutralToTerm + +instance Show NeutralTerm where + show = renderSawDoc defaultPPOpts . ppNeutral defaultPPOpts diff --git a/saw-core/src/Verifier/SAW/Term/Pretty.hs b/saw-core/src/Verifier/SAW/Term/Pretty.hs index eb4d82fd84..faecd88453 100644 --- a/saw-core/src/Verifier/SAW/Term/Pretty.hs +++ b/saw-core/src/Verifier/SAW/Term/Pretty.hs @@ -37,6 +37,7 @@ module Verifier.SAW.Term.Pretty , OccurrenceMap , shouldMemoizeTerm , ppName + , renderSawDoc ) where import Data.Maybe (isJust) From 1e3657d575f84d0a7cf927a8c219e3334df823cb Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 17 May 2021 10:47:09 -0700 Subject: [PATCH 3/7] In the saw-core simulator, distinguish dependent from non-dependent Pi types. During simulation, notice the special case where the variable does not appear in the body of the Pi type. --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 21 +++++++++++-------- .../src/Verifier/SAW/Simulator/SBV.hs | 4 ++-- .../src/Verifier/SAW/Simulator/What4.hs | 12 +++++------ saw-core/src/Verifier/SAW/Simulator.hs | 11 +++++++++- saw-core/src/Verifier/SAW/Simulator/Value.hs | 14 +++++++++++-- 5 files changed, 42 insertions(+), 20 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index a149e290a5..e06b5e05b8 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -57,6 +57,7 @@ import Verifier.SAW.Cryptol.Panic import Verifier.SAW.Conversion import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..)) import qualified Verifier.SAW.Simulator.Concrete as SC +import qualified Verifier.SAW.Simulator.Value as SC import Verifier.SAW.Prim (BitVector(..)) import Verifier.SAW.Rewriter import Verifier.SAW.SharedTerm @@ -1590,7 +1591,7 @@ asCryptolTypeValue v = case C.tIsTuple t2 of Just ts -> return (C.tTuple (t1 : ts)) Nothing -> return (C.tTuple [t1, t2]) - SC.VPiType _nm v1 f -> do + SC.VPiType _nm v1 (SC.VDependentPi _) -> case v1 of -- if we see that the parameter is a Cryptol.Num, it's a -- pretty good guess that it originally was a @@ -1602,14 +1603,16 @@ asCryptolTypeValue v = ] in error msg -- otherwise we issue a generic error about dependent type inference - _ -> do - let msg = unwords ["asCryptolTypeValue: can't infer a Cryptol type" - ,"for a dependent SAW-Core type." - ] - let v2 = SC.runIdentity (f (error msg)) - t1 <- asCryptolTypeValue v1 - t2 <- asCryptolTypeValue v2 - return (C.tFun t1 t2) + _ -> + error $ unwords ["asCryptolTypeValue: can't infer a Cryptol type" + ,"for a dependent SAW-Core type." + ] + + SC.VPiType _nm v1 (SC.VNondependentPi v2) -> + do t1 <- asCryptolTypeValue v1 + t2 <- asCryptolTypeValue v2 + return (C.tFun t1 t2) + _ -> Nothing -- | Deprecated. diff --git a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs index 0ff394bc7e..d95df4feeb 100644 --- a/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs +++ b/saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs @@ -584,11 +584,11 @@ sbvSolveBasic sc addlPrims unintSet t = do parseUninterpreted :: [SVal] -> String -> TValue SBV -> IO SValue parseUninterpreted cws nm ty = case ty of - (VPiType _ _ f) + (VPiType _ _ body) -> return $ strictFun $ \x -> do (cws', suffix) <- flattenSValue nm x - t2 <- f (ready x) + t2 <- applyPiBody body (ready x) parseUninterpreted (cws ++ cws') (nm ++ suffix) t2 VBoolType diff --git a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs index 6367035fdf..20838094bf 100644 --- a/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs +++ b/saw-core-what4/src/Verifier/SAW/Simulator/What4.hs @@ -731,11 +731,11 @@ parseUninterpreted :: TValue (What4 sym) -> IO (SValue sym) parseUninterpreted sym ref app ty = case ty of - VPiType _ _ f + VPiType _ _ body -> return $ strictFun $ \x -> do app' <- applyUnintApp sym app x - t2 <- f (ready x) + t2 <- applyPiBody body (ready x) parseUninterpreted sym ref app' t2 VBoolType @@ -888,9 +888,9 @@ w4Solve sym sc satq = argTypes :: IsSymExprBuilder sym => TValue (What4 sym) -> IO [TValue (What4 sym)] argTypes v = case v of - VPiType _nm v1 f -> + VPiType _nm v1 body -> do x <- delay (fail "argTypes: unsupported dependent SAW-Core type") - v2 <- f x + v2 <- applyPiBody body x vs <- argTypes v2 return (v1 : vs) _ -> return [] @@ -1178,13 +1178,13 @@ parseUninterpretedSAW :: IO (SValue (B.ExprBuilder n st fs)) parseUninterpretedSAW sym st sc ref trm app ty = case ty of - VPiType _nm t1 f + VPiType _nm t1 body -> return $ strictFun $ \x -> do app' <- applyUnintApp sym app x arg <- mkArgTerm sc t1 x let trm' = ArgTermApply trm arg - t2 <- f (ready x) + t2 <- applyPiBody body (ready x) parseUninterpretedSAW sym st sc ref trm' app' t2 VBoolType diff --git a/saw-core/src/Verifier/SAW/Simulator.hs b/saw-core/src/Verifier/SAW/Simulator.hs index 5f6d18bb50..2943c2e354 100644 --- a/saw-core/src/Verifier/SAW/Simulator.hs +++ b/saw-core/src/Verifier/SAW/Simulator.hs @@ -122,7 +122,16 @@ evalTermF cfg lam recEval tf env = apply v x Lambda nm _ t -> return $ VFun nm (\x -> lam t (x : env)) Pi nm t1 t2 -> do v <- toTValue <$> recEval t1 - return $ TValue $ VPiType nm v (\x -> toTValue <$> lam t2 (x : env)) + body <- + if inBitSet 0 (looseVars t2) then + pure (VDependentPi (\x -> toTValue <$> lam t2 (x : env))) + else + do val <- delay (panic "evalTerF" + ["nondependent Pi type forced its value" + , showTerm (Unshared tf)]) + VNondependentPi . toTValue <$> lam t2 (val : env) + return $ TValue $ VPiType nm v body + LocalVar i -> force (env !! i) Constant ec t -> do ec' <- traverse (fmap toTValue . recEval) ec maybe (recEval t) id (simConstant cfg tf ec') diff --git a/saw-core/src/Verifier/SAW/Simulator/Value.hs b/saw-core/src/Verifier/SAW/Simulator/Value.hs index 62901bd807..f728137fdf 100644 --- a/saw-core/src/Verifier/SAW/Simulator/Value.hs +++ b/saw-core/src/Verifier/SAW/Simulator/Value.hs @@ -76,7 +76,7 @@ data TValue l | VIntType | VIntModType !Natural | VArrayType !(TValue l) !(TValue l) - | VPiType LocalName !(TValue l) !(Thunk l -> EvalM l (TValue l)) + | VPiType LocalName !(TValue l) !(PiBody l) | VUnitType | VPairType !(TValue l) !(TValue l) | VDataType !Ident ![Value l] @@ -84,6 +84,10 @@ data TValue l | VSort !Sort | VTyTerm !Sort !Term +data PiBody l + = VDependentPi !(Thunk l -> EvalM l (TValue l)) + | VNondependentPi !(TValue l) + -- | Neutral terms represent computations that are blocked -- because some internal term cannot be evaluated -- (e.g., because it is a variable, because it's definition @@ -260,12 +264,18 @@ valRecordProj v _ = apply :: (HasCallStack, VMonad l, Show (Extra l)) => Value l -> Thunk l -> MValue l apply (VFun _ f) x = f x -apply (TValue (VPiType _ _ f)) x = TValue <$> f x +apply (TValue (VPiType _ _ body)) x = TValue <$> applyPiBody body x + apply v _x = panic "Verifier.SAW.Simulator.Value.apply" ["Not a function value:", show v] applyAll :: (VMonad l, Show (Extra l)) => Value l -> [Thunk l] -> MValue l applyAll = foldM apply +{-# INLINE applyPiBody #-} +applyPiBody :: VMonad l => PiBody l -> Thunk l -> EvalM l (TValue l) +applyPiBody (VDependentPi f) x = f x +applyPiBody (VNondependentPi t) _ = pure t + asFiniteTypeValue :: Value l -> Maybe FiniteType asFiniteTypeValue v = case v of From b852b1419f253065f051a8cb219c338ad68204d3 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 25 May 2021 14:54:06 -0700 Subject: [PATCH 4/7] Expand the types of values that can be in a `TypedTerm`. In addition to Cryptol value types, Cryptol kinds and general SAWCore types can also appear. --- cryptol-saw-core/src/Verifier/SAW/Cryptol.hs | 115 ++++++------------ .../src/Verifier/SAW/CryptolEnv.hs | 21 +++- .../src/Verifier/SAW/TypedTerm.hs | 77 ++++++++---- 3 files changed, 111 insertions(+), 102 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs index e06b5e05b8..b07ec1d3b6 100644 --- a/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs +++ b/cryptol-saw-core/src/Verifier/SAW/Cryptol.hs @@ -54,15 +54,13 @@ import Cryptol.TypeCheck.TypeOf (fastTypeOf, fastSchemaOf) import Cryptol.Utils.PP (pretty) import Verifier.SAW.Cryptol.Panic -import Verifier.SAW.Conversion import Verifier.SAW.FiniteValue (FirstOrderType(..), FirstOrderValue(..)) import qualified Verifier.SAW.Simulator.Concrete as SC import qualified Verifier.SAW.Simulator.Value as SC import Verifier.SAW.Prim (BitVector(..)) -import Verifier.SAW.Rewriter import Verifier.SAW.SharedTerm import Verifier.SAW.Simulator.MonadLazy (force) -import Verifier.SAW.TypedAST (mkSort, mkModuleName, FieldName, LocalName) +import Verifier.SAW.TypedAST (mkSort, FieldName, LocalName) import GHC.Stack @@ -1567,91 +1565,58 @@ pIsNeq ty = case C.tNoUser ty of -------------------------------------------------------------------------------- -- Utilities -asCryptolTypeValue :: SC.TValue SC.Concrete -> Maybe C.Type +asCryptolTypeValue :: SC.TValue SC.Concrete -> Maybe (Either C.Kind C.Type) asCryptolTypeValue v = case v of - SC.VBoolType -> return C.tBit - SC.VIntType -> return C.tInteger - SC.VIntModType n -> return (C.tIntMod (C.tNum n)) + SC.VBoolType -> return (Right C.tBit) + SC.VIntType -> return (Right C.tInteger) + SC.VIntModType n -> return (Right (C.tIntMod (C.tNum n))) SC.VArrayType v1 v2 -> do - t1 <- asCryptolTypeValue v1 - t2 <- asCryptolTypeValue v2 - return $ C.tArray t1 t2 + Right t1 <- asCryptolTypeValue v1 + Right t2 <- asCryptolTypeValue v2 + return (Right (C.tArray t1 t2)) SC.VVecType n v2 -> do - t2 <- asCryptolTypeValue v2 - return (C.tSeq (C.tNum n) t2) - SC.VDataType "Prelude.Stream" [v1] -> - case v1 of - SC.TValue tv -> C.tSeq C.tInf <$> asCryptolTypeValue tv - _ -> Nothing - SC.VUnitType -> return (C.tTuple []) + Right t2 <- asCryptolTypeValue v2 + return (Right (C.tSeq (C.tNum n) t2)) + + SC.VDataType "Prelude.Stream" [SC.TValue v1] -> + do Right t1 <- asCryptolTypeValue v1 + return (Right (C.tSeq C.tInf t1)) + + SC.VDataType "Cryptol.Num" [] -> + return (Left C.KNum) + + SC.VDataType _ _ -> Nothing + + SC.VUnitType -> return (Right (C.tTuple [])) SC.VPairType v1 v2 -> do - t1 <- asCryptolTypeValue v1 - t2 <- asCryptolTypeValue v2 + Right t1 <- asCryptolTypeValue v1 + Right t2 <- asCryptolTypeValue v2 case C.tIsTuple t2 of - Just ts -> return (C.tTuple (t1 : ts)) - Nothing -> return (C.tTuple [t1, t2]) - SC.VPiType _nm v1 (SC.VDependentPi _) -> - case v1 of - -- if we see that the parameter is a Cryptol.Num, it's a - -- pretty good guess that it originally was a - -- polymorphic number type. - SC.VDataType "Cryptol.Num" [] -> - let msg= unwords ["asCryptolTypeValue: can't infer a polymorphic Cryptol" - ,"type. Please, make sure all numeric types are" - ,"specialized before constructing a typed term." - ] - in error msg - -- otherwise we issue a generic error about dependent type inference - _ -> - error $ unwords ["asCryptolTypeValue: can't infer a Cryptol type" - ,"for a dependent SAW-Core type." - ] + Just ts -> return (Right (C.tTuple (t1 : ts))) + Nothing -> return (Right (C.tTuple [t1, t2])) SC.VPiType _nm v1 (SC.VNondependentPi v2) -> - do t1 <- asCryptolTypeValue v1 - t2 <- asCryptolTypeValue v2 - return (C.tFun t1 t2) + do Right t1 <- asCryptolTypeValue v1 + Right t2 <- asCryptolTypeValue v2 + return (Right (C.tFun t1 t2)) - _ -> Nothing + SC.VSort s + | s == mkSort 0 -> return (Left C.KType) + | otherwise -> Nothing --- | Deprecated. -scCryptolType :: SharedContext -> Term -> IO C.Type + -- TODO? + SC.VPiType _nm _v1 (SC.VDependentPi _) -> Nothing + SC.VRecordType{} -> Nothing + SC.VTyTerm{} -> Nothing + + +scCryptolType :: SharedContext -> Term -> IO (Maybe (Either C.Kind C.Type)) scCryptolType sc t = do modmap <- scGetModuleMap sc case SC.evalSharedTerm modmap Map.empty Map.empty t of - SC.TValue (asCryptolTypeValue -> Just ty) -> return ty - _ -> panic "scCryptolType" ["scCryptolType: unsupported type " ++ showTerm t] - --- | Deprecated. -scCryptolEq :: SharedContext -> Term -> Term -> IO Term -scCryptolEq sc x y = - do rules <- concat <$> traverse defRewrites defs - let ss = addConvs natConversions (addRules rules emptySimpset :: Simpset ()) - tx <- scTypeOf sc x >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd - ty <- scTypeOf sc y >>= rewriteSharedTerm sc ss >>= scCryptolType sc . snd - unless (tx == ty) $ - panic "scCryptolEq" - [ "scCryptolEq: type mismatch between" - , pretty tx - , "and" - , pretty ty - ] - - -- Actually apply the equality function, along with the Eq class dictionary - t <- scTypeOf sc x - c <- scCryptolType sc t - k <- importType sc emptyEnv c - eqPrf <- proveProp sc emptyEnv (C.pEq c) - scGlobalApply sc "Cryptol.ecEq" [k, eqPrf, x, y] - - where - defs = map (mkIdent (mkModuleName ["Cryptol"])) ["seq", "ty"] - defRewrites ident = - do maybe_def <- scFindDef sc ident - case maybe_def of - Nothing -> return [] - Just def -> scDefRewriteRules sc def + SC.TValue tv -> return (asCryptolTypeValue tv) + _ -> return Nothing -- | Convert from SAWCore's Value type to Cryptol's, guided by the -- Cryptol type schema. diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 5f3e0b9e5f..813c74d470 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -366,7 +366,7 @@ loadCryptolModule sc env path = do let names = MEx.exported C.NSValue (T.mExports m) -- :: Set T.Name let tm' = Map.filterWithKey (\k _ -> Set.member k names) $ - Map.intersectionWith TypedTerm types newTermEnv + Map.intersectionWith (\t x -> TypedTerm (TypedTermSchema t) x) types newTermEnv let env' = env { eModuleEnv = modEnv'' , eTermEnv = newTermEnv } @@ -375,13 +375,18 @@ loadCryptolModule sc env path = do bindCryptolModule :: (P.ModName, CryptolModule) -> CryptolEnv -> CryptolEnv bindCryptolModule (modName, CryptolModule sm tm) env = - env { eExtraNames = flip (foldr addName) (Map.keys tm) $ + env { eExtraNames = flip (foldr addName) (Map.keys tm') $ flip (foldr addTSyn) (Map.keys sm) $ eExtraNames env , eExtraTSyns = Map.union sm (eExtraTSyns env) - , eExtraTypes = Map.union (fmap (\(TypedTerm s _) -> s) tm) (eExtraTypes env) - , eTermEnv = Map.union (fmap (\(TypedTerm _ t) -> t) tm) (eTermEnv env) + , eExtraTypes = Map.union (fmap fst tm') (eExtraTypes env) + , eTermEnv = Map.union (fmap snd tm') (eTermEnv env) } where + -- select out those typed terms that have Cryptol schemas + tm' = Map.mapMaybe f tm + f (TypedTerm (TypedTermSchema s) x) = Just (s,x) + f _ = Nothing + addName name = MN.shadowing (MN.singletonE (P.mkQual modName (MN.nameIdent name)) name) addTSyn name = MN.shadowing (MN.singletonT (P.mkQual modName (MN.nameIdent name)) name) @@ -435,7 +440,7 @@ bindIdent ident env = (name, env') env' = env { eModuleEnv = modEnv' } bindTypedTerm :: (Ident, TypedTerm) -> CryptolEnv -> CryptolEnv -bindTypedTerm (ident, TypedTerm schema trm) env = +bindTypedTerm (ident, TypedTerm (TypedTermSchema schema) trm) env = env' { eExtraNames = MR.shadowing (MN.singletonE pname name) (eExtraNames env) , eExtraTypes = Map.insert name schema (eExtraTypes env) , eTermEnv = Map.insert name trm (eTermEnv env) @@ -444,6 +449,10 @@ bindTypedTerm (ident, TypedTerm schema trm) env = pname = P.mkUnqual ident (name, env') = bindIdent ident env +-- Only bind terms that have Cryptol schemas +bindTypedTerm _ env = env + + bindType :: (Ident, T.Schema) -> CryptolEnv -> CryptolEnv bindType (ident, T.Forall [] [] ty) env = env' { eExtraNames = MR.shadowing (MN.singletonT pname name) (eExtraNames env) @@ -528,7 +537,7 @@ parseTypedTerm sc env input = do -- Translate trm <- translateExpr sc env' expr - return (TypedTerm schema trm) + return (TypedTerm (TypedTermSchema schema) trm) parseDecls :: (?fileReader :: FilePath -> IO ByteString) => diff --git a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs index 0480ba4ac9..dac3549deb 100644 --- a/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs +++ b/cryptol-saw-core/src/Verifier/SAW/TypedTerm.hs @@ -5,6 +5,7 @@ License : BSD3 Maintainer : huffman Stability : provisional -} +{-# LANGUAGE PatternGuards #-} module Verifier.SAW.TypedTerm where import Control.Monad (foldM) @@ -32,29 +33,50 @@ import Verifier.SAW.SharedTerm data TypedTerm = TypedTerm - { ttSchema :: C.Schema + { ttType :: TypedTermType , ttTerm :: Term } deriving Show + +-- | The different notion of Cryptol types that +-- as SAWCore term might have. +data TypedTermType + = TypedTermSchema C.Schema + | TypedTermKind C.Kind + | TypedTermOther Term + deriving Show + + ttTermLens :: Functor f => (Term -> f Term) -> TypedTerm -> f TypedTerm ttTermLens f tt = tt `seq` fmap (\x -> tt{ttTerm = x}) (f (ttTerm tt)) --- | Deprecated. +ttIsMono :: TypedTermType -> Maybe C.Type +ttIsMono ttp = + case ttp of + TypedTermSchema sch -> C.isMono sch + _ -> Nothing + mkTypedTerm :: SharedContext -> Term -> IO TypedTerm mkTypedTerm sc trm = do ty <- scTypeOf sc trm ct <- scCryptolType sc ty - return $ TypedTerm (C.Forall [] [] ct) trm + let ttt = case ct of + Nothing -> TypedTermOther ty + Just (Left k) -> TypedTermKind k + Just (Right t) -> TypedTermSchema (C.tMono t) + return (TypedTerm ttt trm) -- | Apply a function-typed 'TypedTerm' to an argument. This operation -- fails if the first 'TypedTerm' does not have a monomorphic function -- type. applyTypedTerm :: SharedContext -> TypedTerm -> TypedTerm -> IO TypedTerm -applyTypedTerm sc (TypedTerm schema1 t1) (TypedTerm _schema2 t2) = - case C.tIsFun =<< C.isMono schema1 of - Nothing -> fail "applyTypedTerm: not a function type" - Just (_, cty') -> TypedTerm (C.tMono cty') <$> scApply sc t1 t2 +applyTypedTerm sc (TypedTerm tp t1) (TypedTerm _ t2) + | Just (_,cty') <- C.tIsFun =<< ttIsMono tp + = TypedTerm (TypedTermSchema (C.tMono cty')) <$> scApply sc t1 t2 + +-- TODO? extend this to allow explicit application of types? +applyTypedTerm _ _ _ = fail "applyTypedTerm: not a (monomorphic) function type" -- | Apply a 'TypedTerm' to a list of arguments. This operation fails -- if the first 'TypedTerm' does not have a function type of @@ -72,23 +94,24 @@ defineTypedTerm sc name (TypedTerm schema t) = -- fails if any 'TypedTerm' in the list has a polymorphic type. tupleTypedTerm :: SharedContext -> [TypedTerm] -> IO TypedTerm tupleTypedTerm sc tts = - case traverse (C.isMono . ttSchema) tts of + case traverse (ttIsMono . ttType) tts of Nothing -> fail "tupleTypedTerm: invalid polymorphic term" Just ctys -> - TypedTerm (C.tMono (C.tTuple ctys)) <$> scTuple sc (map ttTerm tts) + TypedTerm (TypedTermSchema (C.tMono (C.tTuple ctys))) <$> + scTuple sc (map ttTerm tts) -- | Given a 'TypedTerm' with a tuple type, return a list of its -- projected components. This operation fails if the 'TypedTerm' does -- not have a tuple type. destTupleTypedTerm :: SharedContext -> TypedTerm -> IO [TypedTerm] -destTupleTypedTerm sc (TypedTerm schema t) = - case C.tIsTuple =<< C.isMono schema of +destTupleTypedTerm sc (TypedTerm tp t) = + case C.tIsTuple =<< ttIsMono tp of Nothing -> fail "asTupleTypedTerm: not a tuple type" Just ctys -> do let len = length ctys let idxs = take len [1 ..] ts <- traverse (\i -> scTupleSelector sc t i len) idxs - pure $ zipWith TypedTerm (map C.tMono ctys) ts + pure $ zipWith TypedTerm (map (TypedTermSchema . C.tMono) ctys) ts -- First order types and values ------------------------------------------------ @@ -117,7 +140,7 @@ typedTermOfFirstOrderValue sc fov = do let fot = firstOrderTypeOf fov let cty = cryptolTypeOfFirstOrderType fot t <- scFirstOrderValue sc fov - pure $ TypedTerm (C.tMono cty) t + pure $ TypedTerm (TypedTermSchema (C.tMono cty)) t -- Typed external constants ---------------------------------------------------- @@ -130,23 +153,32 @@ data TypedExtCns = -- | Recognize 'TypedTerm's that are external constants. asTypedExtCns :: TypedTerm -> Maybe TypedExtCns -asTypedExtCns (TypedTerm schema t) = - do cty <- C.isMono schema +asTypedExtCns (TypedTerm tp t) = + do cty <- ttIsMono tp ec <- asExtCns t pure $ TypedExtCns cty ec -- | Make a 'TypedTerm' from a 'TypedExtCns'. typedTermOfExtCns :: SharedContext -> TypedExtCns -> IO TypedTerm typedTermOfExtCns sc (TypedExtCns cty ec) = - TypedTerm (C.tMono cty) <$> scExtCns sc ec + TypedTerm (TypedTermSchema (C.tMono cty)) <$> scExtCns sc ec abstractTypedExts :: SharedContext -> [TypedExtCns] -> TypedTerm -> IO TypedTerm -abstractTypedExts sc tecs (TypedTerm (C.Forall params props ty) trm) = +abstractTypedExts sc tecs (TypedTerm (TypedTermSchema (C.Forall params props ty)) trm) = do let tys = map tecType tecs let exts = map tecExt tecs let ty' = foldr C.tFun ty tys trm' <- scAbstractExts sc exts trm - pure $ TypedTerm (C.Forall params props ty') trm' + pure $ TypedTerm (TypedTermSchema (C.Forall params props ty')) trm' +abstractTypedExts sc tecs (TypedTerm (TypedTermKind k) trm) = + do let exts = map tecExt tecs + trm' <- scAbstractExts sc exts trm + pure $ TypedTerm (TypedTermKind k) trm' +abstractTypedExts sc tecs (TypedTerm (TypedTermOther _tp) trm) = + do let exts = map tecExt tecs + trm' <- scAbstractExts sc exts trm + tp' <- scTypeOf sc trm' + pure $ TypedTerm (TypedTermOther tp') trm' -- Typed modules --------------------------------------------------------------- @@ -162,9 +194,12 @@ showCryptolModule (CryptolModule sm tm) = unlines $ (if Map.null sm then [] else "Type Synonyms" : "=============" : map showTSyn (Map.elems sm) ++ [""]) ++ - "Symbols" : "=======" : map showBinding (Map.assocs tm) + "Symbols" : "=======" : concatMap showBinding (Map.assocs tm) where showTSyn (C.TySyn name params _props rhs _doc) = " " ++ unwords (pretty (nameIdent name) : map pretty params) ++ " = " ++ pretty rhs - showBinding (name, TypedTerm schema _) = - " " ++ pretty (nameIdent name) ++ " : " ++ pretty schema + + showBinding (name, TypedTerm (TypedTermSchema schema) _) = + [" " ++ pretty (nameIdent name) ++ " : " ++ pretty schema] + showBinding _ = + [] From 81c800afb44440b28b603173cce947bf25d93b84 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Tue, 25 May 2021 15:02:58 -0700 Subject: [PATCH 5/7] Update SAWScript with the new, more permissive, notion of `TypedTerm` --- src/SAWScript/Builtins.hs | 71 ++++++++++++------- src/SAWScript/Crucible/Common/MethodSpec.hs | 10 ++- src/SAWScript/Crucible/JVM/Builtins.hs | 30 +++++--- src/SAWScript/Crucible/JVM/BuiltinsJVM.hs | 4 +- src/SAWScript/Crucible/JVM/Override.hs | 10 +-- .../Crucible/JVM/ResolveSetupValue.hs | 23 ++++-- src/SAWScript/Crucible/LLVM/Builtins.hs | 51 +++++++++---- src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 17 ++--- src/SAWScript/Crucible/LLVM/Override.hs | 32 ++++++--- .../Crucible/LLVM/ResolveSetupValue.hs | 29 ++++---- src/SAWScript/Interpreter.hs | 2 +- src/SAWScript/Prover/Exporter.hs | 4 +- src/SAWScript/Prover/Util.hs | 10 ++- src/SAWScript/Value.hs | 8 ++- 14 files changed, 196 insertions(+), 105 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index ccbe4081f3..a2032c173b 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -115,6 +115,7 @@ import SAWScript.TopLevel import qualified SAWScript.Value as SV import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork) +import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) import SAWScript.Prover.Util(checkBooleanSchema) import SAWScript.Prover.SolverStats import qualified SAWScript.Prover.SBV as Prover @@ -131,11 +132,16 @@ showPrim v = do return (SV.showsPrecValue opts 0 v "") definePrim :: Text -> TypedTerm -> TopLevel TypedTerm -definePrim name (TypedTerm schema rhs) = +definePrim name (TypedTerm (TypedTermSchema schema) rhs) = do sc <- getSharedContext ty <- io $ Cryptol.importSchema sc Cryptol.emptyEnv schema t <- io $ scConstant sc name rhs ty - return $ TypedTerm schema t + return $ TypedTerm (TypedTermSchema schema) t +definePrim _name (TypedTerm tp _) = + fail $ unlines + [ "Expected term with Cryptol schema type, but got" + , show (ppTypedTermType tp) + ] sbvUninterpreted :: String -> Term -> TopLevel Uninterp sbvUninterpreted s t = return $ Uninterp (s, t) @@ -150,7 +156,7 @@ readBytes path = do xs <- io $ mapM (scBvConst sc 8 . toInteger) bytes trm <- io $ scVector sc e xs let schema = C.Forall [] [] (C.tSeq (C.tNum len) (C.tSeq (C.tNum (8::Int)) C.tBit)) - return (TypedTerm schema trm) + return (TypedTerm (TypedTermSchema schema) trm) readSBV :: FilePath -> [Uninterp] -> TopLevel TypedTerm readSBV path unintlst = @@ -166,7 +172,7 @@ readSBV path unintlst = printOutLnTop Error $ unlines $ ("Type error reading " ++ path ++ ":") : prettyTCError err Right _ -> return () -- TODO: check that it matches 'schema'? - return (TypedTerm schema trm) + return (TypedTerm (TypedTermSchema schema) trm) where unintmap = Map.fromList $ map getUninterp unintlst @@ -257,7 +263,7 @@ readAIGPrim f = do et <- io $ readAIG proxy opts sc f case et of Left err -> fail $ "Reading AIG failed: " ++ err - Right (inLen, outLen, t) -> pure $ TypedTerm schema t + Right (inLen, outLen, t) -> pure $ TypedTerm (TypedTermSchema schema) t where t1 = C.tWord (C.tNum inLen) t2 = C.tWord (C.tNum outLen) @@ -508,6 +514,15 @@ hoistIfsInGoalPrim = p <- io $ hoistIfsInGoal sc (goalProp goal) return (p, HoistIfsEvidence) +term_type :: TypedTerm -> TopLevel C.Schema +term_type tt = + case ttType tt of + TypedTermSchema sch -> pure sch + tp -> fail $ unlines + [ "Term does not have a Cryptol type" + , show (ppTypedTermType tp) + ] + goal_eval :: [String] -> ProofScript () goal_eval unints = execTactic $ tacticChange $ \goal -> @@ -818,7 +833,7 @@ provePrim :: TypedTerm -> TopLevel ProofResult provePrim script t = do - io $ checkBooleanSchema (ttSchema t) + io $ checkBooleanSchema (ttType t) sc <- getSharedContext prop <- io $ predicateToProp sc Universal (ttTerm t) let goal = ProofGoal 0 "prove" "prove" prop @@ -855,7 +870,7 @@ satPrim :: TypedTerm -> TopLevel SV.SatResult satPrim script t = - do io $ checkBooleanSchema (ttSchema t) + do io $ checkBooleanSchema (ttType t) sc <- getSharedContext prop <- io $ predicateToProp sc Existential (ttTerm t) let goal = ProofGoal 0 "sat" "sat" prop @@ -1001,7 +1016,7 @@ freshSymbolicPrim x schema@(C.Forall [] [] ct) = do sc <- getSharedContext cty <- io $ Cryptol.importType sc Cryptol.emptyEnv ct tm <- io $ scFreshGlobal sc x cty - return $ TypedTerm schema tm + return $ TypedTerm (TypedTermSchema schema) tm freshSymbolicPrim _ _ = fail "Can't create fresh symbolic variable of non-ground type." @@ -1144,8 +1159,8 @@ failsPrim m = TopLevel $ do eval_bool :: TypedTerm -> TopLevel Bool eval_bool t = do sc <- getSharedContext - case ttSchema t of - C.Forall [] [] (C.tIsBit -> True) -> return () + case ttType t of + TypedTermSchema (C.Forall [] [] (C.tIsBit -> True)) -> return () _ -> fail "eval_bool: not type Bit" unless (null (getAllExts (ttTerm t))) $ fail "eval_bool: term contains symbolic variables" @@ -1161,8 +1176,8 @@ eval_int t = do fail "term contains symbolic variables" opts <- getOptions t' <- io $ defaultTypedTerm opts sc cfg t - case ttSchema t' of - C.Forall [] [] (isInteger -> True) -> return () + case ttType t' of + TypedTermSchema (C.Forall [] [] (isInteger -> True)) -> return () _ -> fail "eval_int: argument is not a finite bitvector" v <- io $ rethrowEvalError $ SV.evaluateTypedTerm sc t' io $ C.runEval mempty (C.bvVal <$> C.fromVWord C.Concrete "eval_int" v) @@ -1177,41 +1192,42 @@ list_term :: [TypedTerm] -> TopLevel TypedTerm list_term [] = fail "list_term: invalid empty list" list_term tts@(tt0 : _) = do sc <- getSharedContext - let schema = ttSchema tt0 - unless (all (schema ==) (map ttSchema tts)) $ + a <- case ttType tt0 of + TypedTermSchema (C.Forall [] [] a) -> return a + _ -> fail "list_term: not a monomorphic element type" + let eqa (TypedTermSchema (C.Forall [] [] x)) = a == x + eqa _ = False + unless (all eqa (map ttType tts)) $ fail "list_term: non-uniform element types" - a <- - case schema of - C.Forall [] [] a -> return a - _ -> fail "list_term: not a monomorphic element type" + a' <- io $ Cryptol.importType sc Cryptol.emptyEnv a trm <- io $ scVectorReduced sc a' (map ttTerm tts) let n = C.tNum (length tts) - return (TypedTerm (C.tMono (C.tSeq n a)) trm) + return (TypedTerm (TypedTermSchema (C.tMono (C.tSeq n a))) trm) eval_list :: TypedTerm -> TopLevel [TypedTerm] eval_list t = do sc <- getSharedContext (n, a) <- - case ttSchema t of - C.Forall [] [] (C.tIsSeq -> Just (C.tIsNum -> Just n, a)) -> return (n, a) + case ttType t of + TypedTermSchema (C.Forall [] [] (C.tIsSeq -> Just (C.tIsNum -> Just n, a))) -> return (n, a) _ -> fail "eval_list: not a monomorphic array type" n' <- io $ scNat sc (fromInteger n) a' <- io $ Cryptol.importType sc Cryptol.emptyEnv a idxs <- io $ traverse (scNat sc) $ map fromInteger [0 .. n - 1] ts <- io $ traverse (scAt sc n' a' (ttTerm t)) idxs - return (map (TypedTerm (C.tMono a)) ts) + return (map (TypedTerm (TypedTermSchema (C.tMono a))) ts) -- | 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 schema trm) +defaultTypedTerm opts sc cfg tt@(TypedTerm (TypedTermSchema schema) trm) | null (C.sVars schema) = return tt | otherwise = do mdefault <- C.withSolver cfg (\s -> C.defaultReplExpr s undefined schema) let inst = do (soln, _) <- mdefault mapM (`lookup` soln) (C.sVars schema) case inst of - Nothing -> return (TypedTerm schema trm) + Nothing -> return (TypedTerm (TypedTermSchema schema) trm) Just tys -> do let vars = C.sVars schema let nms = C.addTNames vars IntMap.empty @@ -1229,7 +1245,7 @@ defaultTypedTerm opts sc cfg tt@(TypedTerm schema trm) let props = map (plainSubst su) (C.sProps schema) trm'' <- foldM dischargeProp trm' props let schema' = C.Forall [] [] (C.apSubst su (C.sType schema)) - return (TypedTerm schema' trm'') + return (TypedTerm (TypedTermSchema schema') trm'') where warnDefault ns (x,t) = printOutLn opts Info $ show $ C.text "Assuming" C.<+> C.ppWithNames ns (x :: C.TParam) C.<+> C.text "=" C.<+> C.pp t @@ -1245,6 +1261,9 @@ defaultTypedTerm opts sc cfg tt@(TypedTerm schema trm) C.TVar x -> C.apSubst s (C.TVar x) C.TNewtype nt ts -> C.TNewtype nt (fmap (plainSubst s) ts) +defaultTypedTerm _opts _sc _cfg tt = return tt + + eval_size :: C.Schema -> TopLevel Integer eval_size s = case s of @@ -1366,7 +1385,7 @@ cryptol_prims = CryptolModule Map.empty <$> Map.fromList <$> traverse parsePrim s' <- io $ CEnv.parseSchema cenv' (noLoc s) t' <- io $ scGlobalDef sc i putTopLevelRW $ rw { rwCryptol = cenv' } - return (n', TypedTerm s' t') + return (n', TypedTerm (TypedTermSchema s') t') cryptol_load :: (FilePath -> IO StrictBS.ByteString) -> FilePath -> TopLevel CryptolModule cryptol_load fileReader path = do diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index cc9fd41d24..28358002a1 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -153,7 +153,15 @@ ppTypedTerm :: TypedTerm -> PP.Doc ann ppTypedTerm (TypedTerm tp tm) = PP.unAnnotate (ppTerm defaultPPOpts tm) PP.<+> PP.pretty ":" PP.<+> - PP.viaShow (Cryptol.ppPrec 0 tp) + ppTypedTermType tp + +ppTypedTermType :: TypedTermType -> PP.Doc ann +ppTypedTermType (TypedTermSchema sch) = + PP.viaShow (Cryptol.ppPrec 0 sch) +ppTypedTermType (TypedTermKind k) = + PP.viaShow (Cryptol.ppPrec 0 k) +ppTypedTermType (TypedTermOther tp) = + PP.unAnnotate (ppTerm defaultPPOpts tp) ppTypedExtCns :: TypedExtCns -> PP.Doc ann ppTypedExtCns (TypedExtCns tp ec) = diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index d65f2797ba..795da169d1 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -864,6 +864,7 @@ data JVMSetupError | JVMArgNumberWrong Int Int -- number expected, number found | JVMReturnUnexpected J.Type -- found | JVMReturnTypeMismatch J.Type J.Type -- expected, found + | JVMNonValueType TypedTermType instance X.Exception JVMSetupError where toException = topLevelExceptionToException @@ -971,6 +972,11 @@ instance Show JVMSetupError where , "Expected type: " ++ show expected , "Given type: " ++ show found ] + JVMNonValueType tp -> + unlines + [ "Expected term with value type, but got" + , show (MS.ppTypedTermType tp) + ] -- | Returns Cryptol type of actual type if it is an array or -- primitive type. @@ -1214,17 +1220,19 @@ generic_array_is ptr mval = case mval of Nothing -> pure () Just val -> - case checkVal of - Nothing -> X.throwM (JVMArrayTypeMismatch len elTy schema) - Just () -> pure () - where - schema = ttSchema val - checkVal = - do ty <- Cryptol.isMono schema - (n, a) <- Cryptol.tIsSeq ty - guard (Cryptol.tIsNum n == Just (toInteger len)) - jty <- toJVMType (Cryptol.evalValType mempty a) - guard (registerCompatible elTy jty) + do schema <- case ttType val of + TypedTermSchema sch -> pure sch + tp -> X.throwM (JVMNonValueType tp) + let checkVal = + do ty <- Cryptol.isMono schema + (n, a) <- Cryptol.tIsSeq ty + guard (Cryptol.tIsNum n == Just (toInteger len)) + jty <- toJVMType (Cryptol.evalValType mempty a) + guard (registerCompatible elTy jty) + case checkVal of + Nothing -> X.throwM (JVMArrayTypeMismatch len elTy schema) + Just () -> pure () + let pt = JVMPointsToArray loc ptr' mval let pts = st ^. Setup.csMethodSpec . MS.csPreState . MS.csPointsTos when (st ^. Setup.csPrePost == PreState && any (overlapPointsTo pt) pts) $ diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs index 96afca77c0..5b12a21b07 100644 --- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs +++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs @@ -67,7 +67,7 @@ import qualified What4.Solver.Yices as Yices import Verifier.SAW.SharedTerm(Term, SharedContext, mkSharedContext, scImplies) -- cryptol-saw-core -import Verifier.SAW.TypedTerm (TypedTerm(..), abstractTypedExts) +import Verifier.SAW.TypedTerm (TypedTerm(..), abstractTypedExts, TypedTermType(..)) -- saw-core-what4 import Verifier.SAW.Simulator.What4.ReturnTrip @@ -183,7 +183,7 @@ jvm_extract c mname = do case baseCryptolType bt of Nothing -> failure Just cty -> return cty - let tt = TypedTerm (Cryptol.tMono cty) t + let tt = TypedTerm (TypedTermSchema (Cryptol.tMono cty)) t abstractTypedExts sc (toList ecs) tt Crucible.AbortedResult _ _ar -> do fail $ unlines [ "Symbolic execution failed." ] diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 5b65315a3d..4d43bcc447 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -550,7 +550,7 @@ matchArg :: OverrideMatcher CJ.JVM w () matchArg opts sc cc cs prepost actual expectedTy expected@(MS.SetupTerm expectedTT) - | Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT + | TypedTermSchema (Cryptol.Forall [] [] tyexpr) <- ttType expectedTT , Right tval <- Cryptol.evalType mempty tyexpr = do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy @@ -694,7 +694,7 @@ learnPointsTo opts sc cc spec prepost pt = do JVMPointsToArray loc ptr (Just tt) -> do (len, ety) <- - case Cryptol.isMono (ttSchema tt) of + case ttIsMono (ttType tt) of Nothing -> fail "jvm_array_is: invalid polymorphic value" Just cty -> case Cryptol.tIsSeq cty of @@ -891,7 +891,7 @@ doEntireArrayStore sym glob ref vs = foldM store glob (zip [0..] vs) -- along with a list of its projected components. Return 'Nothing' if -- the 'TypedTerm' does not have a vector type. destVecTypedTerm :: SharedContext -> TypedTerm -> IO (Maybe (Cryptol.Type, [TypedTerm])) -destVecTypedTerm sc (TypedTerm schema t) = +destVecTypedTerm sc (TypedTerm ttp t) = case asVec of Nothing -> pure Nothing Just (len, ety) -> @@ -899,10 +899,10 @@ destVecTypedTerm sc (TypedTerm schema t) = ty_tm <- Cryptol.importType sc Cryptol.emptyEnv ety idxs <- traverse (scNat sc) (map fromInteger [0 .. len-1]) ts <- traverse (scAt sc len_tm ty_tm t) idxs - pure $ Just (ety, map (TypedTerm (Cryptol.tMono ety)) ts) + pure $ Just (ety, map (TypedTerm (TypedTermSchema (Cryptol.tMono ety))) ts) where asVec = - do ty <- Cryptol.isMono schema + do ty <- ttIsMono ttp (n, a) <- Cryptol.tIsSeq ty n' <- Cryptol.tIsNum n Just (n', a) diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index da2d85894c..c593ad302d 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -89,6 +89,7 @@ type SetupValue = MS.SetupValue CJ.JVM data JVMTypeOfError = JVMPolymorphicType Cryptol.Schema | JVMNonRepresentableType Cryptol.Type + | JVMInvalidTypedTerm TypedTermType instance Show JVMTypeOfError where show (JVMPolymorphicType s) = @@ -102,6 +103,11 @@ instance Show JVMTypeOfError where [ "Type not representable in JVM:" , show (Cryptol.pp ty) ] + show (JVMInvalidTypedTerm tp) = + unlines + [ "Expected typed term with Cryptol represnentable type, but got" + , show (MS.ppTypedTermType tp) + ] instance X.Exception JVMTypeOfError @@ -119,12 +125,13 @@ typeOfSetupValue _cc env _nameEnv val = Nothing -> panic "JVMSetup" ["typeOfSetupValue", "Unresolved prestate variable:" ++ show i] Just (_, alloc) -> return (allocationType alloc) MS.SetupTerm tt -> - case ttSchema tt of - Cryptol.Forall [] [] ty -> + case ttType tt of + TypedTermSchema (Cryptol.Forall [] [] ty) -> case toJVMType (Cryptol.evalValType mempty ty) of Nothing -> X.throwM (JVMNonRepresentableType ty) Just jty -> return jty - s -> X.throwM (JVMPolymorphicType s) + TypedTermSchema s -> X.throwM (JVMPolymorphicType s) + tp -> X.throwM (JVMInvalidTypedTerm tp) MS.SetupNull () -> -- We arbitrarily set the type of NULL to java.lang.Object, @@ -175,10 +182,14 @@ resolveTypedTerm :: TypedTerm -> IO JVMVal resolveTypedTerm cc tm = - case ttSchema tm of - Cryptol.Forall [] [] ty -> + case ttType tm of + TypedTermSchema (Cryptol.Forall [] [] ty) -> resolveSAWTerm cc (Cryptol.evalValType mempty ty) (ttTerm tm) - _ -> fail "resolveSetupVal: expected monomorphic term" + tp -> fail $ unlines + [ "resolveSetupVal: expected monomorphic term" + , "but got a term of type" + , show (MS.ppTypedTermType tp) + ] resolveSAWPred :: JVMCrucibleContext -> diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index ca129de60b..576e8f003c 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -973,7 +973,14 @@ setupPrestateConditions mspec cc mem env = aux [] aux (lp:acc) globals xs aux acc globals (MS.SetupCond_Ghost () _loc var val : xs) = - aux acc (Crucible.insertGlobal var val globals) xs + case val of + TypedTerm (TypedTermSchema sch) tm -> + aux acc (Crucible.insertGlobal var (sch,tm) globals) xs + TypedTerm tp _ -> + fail $ unlines + [ "Setup term for global variable expected to have Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] -------------------------------------------------------------------------------- @@ -1528,11 +1535,11 @@ extractFromLLVMCFG opts sc cc (Crucible.AnyCFG cfg) = do bv <- Crucible.projectLLVM_bv sym rv t <- toSC sym st bv let cty = Cryptol.tWord (Cryptol.tNum (natValue w)) - pure $ TypedTerm (Cryptol.tMono cty) t + pure $ TypedTerm (TypedTermSchema (Cryptol.tMono cty)) t Crucible.BVRepr w -> do t <- toSC sym st rv let cty = Cryptol.tWord (Cryptol.tNum (natValue w)) - pure $ TypedTerm (Cryptol.tMono cty) t + pure $ TypedTerm (TypedTermSchema (Cryptol.tMono cty)) t _ -> fail $ unwords ["Unexpected return type:", show rt] tt' <- abstractTypedExts sc (toList ecs) tt pure tt' @@ -1948,12 +1955,19 @@ llvm_symbolic_alloc ro align_bytes sz = loc <- getW4Position "llvm_symbolic_alloc" sc <- lift getSharedContext sz_ty <- liftIO $ Cryptol.scCryptolType sc =<< scTypeOf sc sz - when (Just 64 /= asCryptolBVType sz_ty) $ - throwCrucibleSetup loc $ unwords - [ "llvm_symbolic_alloc:" - , "unexpected type of size term, expected [64], found" - , Cryptol.pretty sz_ty - ] + case sz_ty of + Just (Right tp) + | Just 64 == asCryptolBVType tp -> return () + | otherwise -> throwCrucibleSetup loc $ unwords + [ "llvm_symbolic_alloc:" + , "unexpected type of size term, expected [64], found" + , Cryptol.pretty tp + ] + _ -> throwCrucibleSetup loc $ unwords + [ "llvm_symbolic_alloc:" + , "unexpected term, expected term of type [64], but got" + , showTerm sz + ] let spec = LLVMAllocSpec { _allocSpecMut = if ro then Crucible.Immutable else Crucible.Mutable , _allocSpecType = Crucible.i8p @@ -2122,15 +2136,22 @@ llvm_points_to_array_prefix (getAllLLVM -> ptr) arr sz = LLVMCrucibleSetupM $ do cc <- getLLVMCrucibleContext loc <- getW4Position "llvm_points_to_array_prefix" - case ttSchema sz of - Cryptol.Forall [] [] ty + case ttType sz of + TypedTermSchema (Cryptol.Forall [] [] ty) | Just 64 == asCryptolBVType ty -> return () + | otherwise -> + throwCrucibleSetup loc $ unwords + [ "llvm_points_to_array_prefix:" + , "unexpected type of size term, expected [64], found" + , Cryptol.pretty ty + ] _ -> throwCrucibleSetup loc $ unwords - [ "llvm_points_to_array_prefix:" - , "unexpected type of size term, expected [64], found" - , Cryptol.pretty (ttSchema sz) - ] + [ "llvm_points_to_array_prefix:" + , "unexpected size term, expected term of type [64], but got" + , showTerm (ttTerm sz) + ] + Crucible.llvmPtrWidth (ccLLVMContext cc) $ \wptr -> Crucible.withPtrWidth wptr $ do let ?lc = ccTypeCtx cc st <- get diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index cd95d600d3..bf85964854 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs @@ -114,6 +114,7 @@ import qualified Text.PrettyPrint.HughesPJ as PP import qualified Data.LLVM.BitCode as LLVM +import qualified Cryptol.TypeCheck.AST as Cryptol import qualified Cryptol.Utils.PP as Cryptol (pp) import Data.Parameterized.All (All(All)) @@ -300,19 +301,19 @@ showLLVMModule (LLVMModule name m _) = -- ** Ghost state instance Crucible.IntrinsicClass Sym MS.GhostValue where - type Intrinsic Sym MS.GhostValue ctx = TypedTerm - muxIntrinsic sym _ _namerep _ctx prd thn els = - do when (ttSchema thn /= ttSchema els) $ fail $ unlines $ + type Intrinsic Sym MS.GhostValue ctx = (Cryptol.Schema, Term) + muxIntrinsic sym _ _namerep _ctx prd (thnSch,thn) (elsSch,els) = + do when (thnSch /= elsSch) $ fail $ unlines $ [ "Attempted to mux ghost variables of different types:" - , show (Cryptol.pp (ttSchema thn)) - , show (Cryptol.pp (ttSchema els)) + , show (Cryptol.pp thnSch) + , show (Cryptol.pp elsSch) ] st <- sawCoreState sym let sc = saw_ctx st prd' <- toSC sym st prd - typ <- scTypeOf sc (ttTerm thn) - res <- scIte sc typ prd' (ttTerm thn) (ttTerm els) - return thn { ttTerm = res } + typ <- scTypeOf sc thn + res <- scIte sc typ prd' thn els + return (thnSch, res) -------------------------------------------------------------------------------- -- ** CrucibleContext diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index 311648a35b..39a9924072 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1071,7 +1071,7 @@ matchArg opts sc cc cs prepost actual expectedTy expected = do Just mem -> pure mem case (actual, expectedTy, expected) of (_, _, SetupTerm expectedTT) - | Cryptol.Forall [] [] tyexpr <- ttSchema expectedTT + | TypedTermSchema (Cryptol.Forall [] [] tyexpr) <- ttType expectedTT , Right tval <- Cryptol.evalType mempty tyexpr -> do sym <- Ov.getSymInterface failMsg <- mkStructuralMismatch opts cc sc cs actual expected expectedTy @@ -1308,14 +1308,20 @@ learnGhost :: MS.GhostGlobal -> TypedTerm -> OverrideMatcher (LLVM arch) md () -learnGhost sc cc loc prepost var expected = - do actual <- readGlobal var - when (ttSchema actual /= ttSchema expected) $ fail $ unlines $ +learnGhost sc cc loc prepost var (TypedTerm (TypedTermSchema schEx) tmEx) = + do (sch,tm) <- readGlobal var + when (sch /= schEx) $ fail $ unlines $ [ "Ghost variable had the wrong type:" - , "- Expected: " ++ show (Cryptol.pp (ttSchema expected)) - , "- Actual: " ++ show (Cryptol.pp (ttSchema actual)) + , "- Expected: " ++ show (Cryptol.pp schEx) + , "- Actual: " ++ show (Cryptol.pp sch) ] - instantiateExtMatchTerm sc cc loc prepost (ttTerm actual) (ttTerm expected) + instantiateExtMatchTerm sc cc loc prepost tm tmEx +learnGhost _sc _cc _loc _prepost _var (TypedTerm tp _) + = fail $ unlines + [ "Ghost variable expected value has improper type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] ------------------------------------------------------------------------ @@ -1634,10 +1640,16 @@ executeGhost :: MS.GhostGlobal -> TypedTerm -> OverrideMatcher (LLVM arch) RW () -executeGhost sc var val = +executeGhost sc var (TypedTerm (TypedTermSchema sch) tm) = do s <- OM (use termSub) - t <- liftIO (ttTermLens (scInstantiateExt sc s) val) - writeGlobal var t + tm' <- liftIO (scInstantiateExt sc s tm) + writeGlobal var (sch,tm') +executeGhost _sc _var (TypedTerm tp _) = + fail $ unlines + [ "executeGhost: improper value type" + , "expected Cryptol schema type, but got" + , show (MS.ppTypedTermType tp) + ] ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index 70e14aeb7e..333347729c 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -46,7 +46,6 @@ import qualified Text.LLVM.AST as L import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType) import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..)) -import qualified Cryptol.Utils.PP as Cryptol (pp) import Data.Parameterized.Some (Some(..)) import Data.Parameterized.NatRepr @@ -70,7 +69,7 @@ import Verifier.SAW.Simulator.What4.ReturnTrip import Text.LLVM.DebugUtils as L import SAWScript.Crucible.Common (Sym, sawCoreState) -import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..)) +import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..), ppTypedTermType) import SAWScript.Crucible.LLVM.MethodSpecIR @@ -182,15 +181,15 @@ typeOfSetupValue' cc env nameEnv val = Just spec -> return (Crucible.PtrType (Crucible.MemType (spec ^. allocSpecType))) SetupTerm tt -> - case ttSchema tt of - Cryptol.Forall [] [] ty -> + case ttType tt of + TypedTermSchema (Cryptol.Forall [] [] ty) -> case toLLVMType dl (Cryptol.evalValType mempty ty) of Left err -> fail (toLLVMTypeErrToString err) Right memTy -> return memTy - s -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term" - , "instead got:" - , show (Cryptol.pp s) - ] + tp -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term" + , "instead got:" + , show (ppTypedTermType tp) + ] SetupStruct () packed vs -> do memTys <- traverse (typeOfSetupValue cc env nameEnv) vs let si = Crucible.mkStructInfo dl packed memTys @@ -359,10 +358,14 @@ resolveTypedTerm :: TypedTerm -> IO LLVMVal resolveTypedTerm cc tm = - case ttSchema tm of - Cryptol.Forall [] [] ty -> + case ttType tm of + TypedTermSchema (Cryptol.Forall [] [] ty) -> resolveSAWTerm cc (Cryptol.evalValType mempty ty) (ttTerm tm) - _ -> fail "resolveSetupVal: expected monomorphic term" + tp -> fail $ unlines + [ "resolveSetupVal: expected monomorphic term" + , "instead got term with type" + , show (ppTypedTermType tp) + ] resolveSAWPred :: LLVMCrucibleContext arch -> @@ -683,8 +686,8 @@ memArrayToSawCoreTerm crucible_context endianess typed_term = do _ -> fail $ "unexpected cryptol type: " ++ show cryptol_type - case ttSchema typed_term of - Cryptol.Forall [] [] cryptol_type -> do + case ttType typed_term of + TypedTermSchema (Cryptol.Forall [] [] cryptol_type) -> do let evaluated_type = Cryptol.evalValType mempty cryptol_type fresh_array_const <- scFreshGlobal saw_context "arr" =<< scArrayType saw_context offset_type_term byte_type_term diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 0bcf909544..db8ec9bdce 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -841,7 +841,7 @@ primitives = Map.fromList [ "Print the type of the given term." ] , prim "type" "Term -> Type" - (pureVal ttSchema) + (funVal1 term_type) Current [ "Return the type of the given term." ] diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index 661ed8a82c..ca1342a9c4 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/src/SAWScript/Prover/Exporter.hs @@ -62,7 +62,6 @@ import Data.Text (pack) import Data.Text.Prettyprint.Doc.Render.Text import Prettyprinter (vcat) -import Cryptol.Utils.PP(pretty) import Lang.JVM.ProcessUtils (readProcessExitIfFailure) import Verifier.SAW.CryptolEnv (initCryptolEnv, loadCryptolModule) @@ -86,6 +85,7 @@ import qualified Verifier.SAW.Simulator.What4 as W import qualified Verifier.SAW.UntypedAST as Un import SAWScript.Crucible.Common +import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) import SAWScript.Proof (Prop, propSize, propToTerm, predicateToSATQuery, propToSATQuery) import SAWScript.Prover.SolverStats import SAWScript.Prover.Util @@ -200,7 +200,7 @@ writeSAIGInferLatches proxy sc file tt = do "writeSAIGInferLatches: " ++ why ++ ":\n" ++ "term must have type of the form '(i, s) -> (o, s)',\n" ++ "where 'i', 's', and 'o' are all fixed-width types,\n" ++ - "but type of term is:\n" ++ (pretty . ttSchema $ tt) + "but type of term is:\n" ++ (show . ppTypedTermType . ttType $ tt) -- Decompose type as '(i, s) -> (o, s)' and return 's'. getStateType :: Term -> TopLevel FiniteType diff --git a/src/SAWScript/Prover/Util.hs b/src/SAWScript/Prover/Util.hs index bc3ee2e0ad..ca7c29bd47 100644 --- a/src/SAWScript/Prover/Util.hs +++ b/src/SAWScript/Prover/Util.hs @@ -2,10 +2,12 @@ module SAWScript.Prover.Util where import Verifier.SAW.SharedTerm import Verifier.SAW.FiniteValue +import Verifier.SAW.TypedTerm import qualified Cryptol.TypeCheck.AST as C import Cryptol.Utils.PP (pretty) +import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType) -- | Is this a bool, or something that returns bool. checkBooleanType :: C.Type -> IO () @@ -16,9 +18,11 @@ checkBooleanType ty -- | Make sure that this schema is monomorphic, and either boolean, -- or something that returns a boolean. -checkBooleanSchema :: C.Schema -> IO () -checkBooleanSchema (C.Forall [] [] t) = checkBooleanType t -checkBooleanSchema s = fail ("Invalid polymorphic type: " ++ pretty s) +checkBooleanSchema :: TypedTermType -> IO () +checkBooleanSchema (TypedTermSchema (C.Forall [] [] t)) = checkBooleanType t +checkBooleanSchema (TypedTermSchema s) = fail ("Invalid polymorphic type: " ++ pretty s) +checkBooleanSchema tp = + fail ("Expected boolean type, but got " ++ show (ppTypedTermType tp)) bindAllExts :: SharedContext -> Term -> IO Term bindAllExts sc body = scAbstractExts sc (getAllExts body) body diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 2dd2a83e89..8f7fa0c5c8 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -341,8 +341,12 @@ evaluate sc t = scGetModuleMap sc evaluateTypedTerm :: SharedContext -> TypedTerm -> IO C.Value -evaluateTypedTerm sc (TypedTerm schema trm) = +evaluateTypedTerm sc (TypedTerm (TypedTermSchema schema) trm) = C.runEval mempty . exportValueWithSchema schema =<< evaluate sc trm +evaluateTypedTerm sc (TypedTerm tp _) = + fail $ unlines [ "Could not evaluate term with type" + , show (CMS.ppTypedTermType tp) + ] applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x @@ -559,7 +563,7 @@ typedTermOfString sc str = let scChar c = scApply sc bvNat8 =<< scNat sc (fromIntegral (fromEnum c)) ts <- traverse scChar str trm <- scVector sc byteT ts - pure (TypedTerm schema trm) + pure (TypedTerm (TypedTermSchema schema) trm) -- Other SAWScript Monads ------------------------------------------------------ From 9a46e6d1bd4881cf8617afb2c195c960b352e334 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 26 May 2021 15:25:30 -0700 Subject: [PATCH 6/7] Update saw-remote-api with TypedTerm changes --- saw-remote-api/src/SAWServer/CryptolExpression.hs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/saw-remote-api/src/SAWServer/CryptolExpression.hs b/saw-remote-api/src/SAWServer/CryptolExpression.hs index a464c7716f..53ad5a220d 100644 --- a/saw-remote-api/src/SAWServer/CryptolExpression.hs +++ b/saw-remote-api/src/SAWServer/CryptolExpression.hs @@ -39,7 +39,7 @@ import Verifier.SAW.CryptolEnv translateExpr, CryptolEnv(eExtraTypes, eExtraTSyns, eModuleEnv) ) import Verifier.SAW.SharedTerm (SharedContext) -import Verifier.SAW.TypedTerm(TypedTerm(..)) +import Verifier.SAW.TypedTerm(TypedTerm(..),TypedTermType(..)) import qualified Argo import CryptolServer.Data.Expression (Expression, getCryptolExpr) @@ -86,7 +86,7 @@ getTypedTermOfCExp fileReader sc cenv expr = (Right ((checkedExpr, schema), modEnv'), ws) -> do let env' = cenv { eModuleEnv = modEnv' } trm <- liftIO $ translateExpr sc env' checkedExpr - return (Right (TypedTerm schema trm, modEnv'), ws) + return (Right (TypedTerm (TypedTermSchema schema) trm, modEnv'), ws) (Left err, ws) -> return (Left err, ws) moduleCmdResult :: ModuleRes a -> Argo.Command SAWState (a, ModuleEnv) From 55e3eb13265eb205955487865028eefc161392d4 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 14 Jun 2021 12:13:18 -0700 Subject: [PATCH 7/7] warning police --- src/SAWScript/Value.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 8f7fa0c5c8..4a8e6f3d8b 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -343,7 +343,7 @@ evaluate sc t = evaluateTypedTerm :: SharedContext -> TypedTerm -> IO C.Value evaluateTypedTerm sc (TypedTerm (TypedTermSchema schema) trm) = C.runEval mempty . exportValueWithSchema schema =<< evaluate sc trm -evaluateTypedTerm sc (TypedTerm tp _) = +evaluateTypedTerm _sc (TypedTerm tp _) = fail $ unlines [ "Could not evaluate term with type" , show (CMS.ppTypedTermType tp) ]