diff --git a/CHANGES.md b/CHANGES.md index c31d0bebd2..2fe5edfaf6 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1,7 +1,11 @@ -# Nightly +# Nightly -- ????-??-?? ## New Features * SAW now supports loading and reasoning about Cryptol declarations that make use of numeric constraint guards. For more information on numeric constraint guards, see the [relavent section of the Cryptol reference manual](https://galoisinc.github.io/cryptol/master/BasicSyntax.html#numeric-constraint-guards). +* Add an experimental `mir_verify` command, along with related utilities for + constructing specifications for MIR/Rust programs. For more information, see + the `mir_*` commands documented in the [SAW + manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md). # Version 1.0 -- 2023-06-26 diff --git a/crucible-mir-comp/crucible-mir-comp.cabal b/crucible-mir-comp/crucible-mir-comp.cabal index 6e4220cce1..5883a68623 100644 --- a/crucible-mir-comp/crucible-mir-comp.cabal +++ b/crucible-mir-comp/crucible-mir-comp.cabal @@ -41,7 +41,6 @@ library exposed-modules: Mir.Compositional.Builder Mir.Compositional.Clobber Mir.Compositional.Convert - Mir.Compositional.MethodSpec Mir.Compositional.Override ghc-options: -Wall -Wno-name-shadowing diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs index cd3ab2ec70..8c13af7bed 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs @@ -52,6 +52,8 @@ import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.TypedTerm as SAW import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.MIR.MethodSpecIR +import SAWScript.Crucible.MIR.TypeShape import Mir.DefId import Mir.Generator (CollectionState, collection) @@ -61,7 +63,6 @@ import qualified Mir.Mir as M import Mir.Compositional.Clobber import Mir.Compositional.Convert -import Mir.Compositional.MethodSpec import Mir.Compositional.Override (MethodSpec(..)) @@ -686,7 +687,7 @@ regToSetup bak p eval shp rv = go shp rv ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds go (TransparentShape _ shp) rv = go shp rv - go (RefShape refTy ty' tpr) ref = do + go (RefShape refTy ty' _ tpr) ref = do partIdxLen <- lift $ mirRef_indexAndLenSim ref optIdxLen <- liftIO $ readPartExprMaybe sym partIdxLen let (optIdx, optLen) = diff --git a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs index 458d09daac..151d025b98 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs @@ -24,6 +24,8 @@ import Lang.Crucible.Backend import Lang.Crucible.Simulator import Lang.Crucible.Types +import SAWScript.Crucible.MIR.TypeShape + import Mir.Generator (CollectionState, collection, staticMap, StaticVar(..)) import Mir.Intrinsics hiding (MethodSpec, MethodSpecBuilder) import qualified Mir.Mir as M @@ -106,7 +108,7 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv go (TransparentShape _ shp) rv = go shp rv -- Since this ref is in immutable memory, whatever behavior we're -- approximating with this clobber can't possibly modify it. - go (RefShape _ _ _tpr) rv = return rv + go (RefShape _ _ _ _tpr) rv = return rv go (FnPtrShape _ _ _) _rv = error "Function pointers not currently supported in overrides" diff --git a/crucible-mir-comp/src/Mir/Compositional/Convert.hs b/crucible-mir-comp/src/Mir/Compositional/Convert.hs index 157639bf39..bb503e1e74 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Convert.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Convert.hs @@ -13,7 +13,6 @@ module Mir.Compositional.Convert where -import Control.Lens ((^.), (^..), each) import Control.Monad import Control.Monad.IO.Class import Data.Foldable @@ -47,177 +46,10 @@ import Verifier.SAW.Simulator.What4 (SValue) import qualified Verifier.SAW.Simulator.What4 as SAW import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW (baseSCType) +import SAWScript.Crucible.MIR.TypeShape + import Mir.Intrinsics import qualified Mir.Mir as M -import Mir.TransTy ( tyListToCtx, tyToRepr, tyToReprCont, canInitialize - , isUnsized, reprTransparentFieldTy ) - - --- | TypeShape is used to classify MIR `Ty`s and their corresponding --- CrucibleTypes into a few common cases. We don't use `Ty` directly because --- there are some `Ty`s that have identical structure (such as TyRef vs. --- TyRawPtr) or similar enough structure that we'd rather write only one case --- (such as `u8` vs `i8` vs `i32`, all primitives/BaseTypes). And we don't use --- TypeRepr directly because it's lacking information in some cases (notably --- `TyAdt`, which is always AnyRepr, concealing the actual field types of the --- struct). --- --- In each constructor, the first `M.Ty` is the overall MIR type (e.g., for --- ArrayShape, this is the TyArray type). The overall `TypeRepr tp` isn't --- stored directly, but can be computed with `shapeType`. -data TypeShape (tp :: CrucibleType) where - UnitShape :: M.Ty -> TypeShape UnitType - PrimShape :: M.Ty -> BaseTypeRepr btp -> TypeShape (BaseToType btp) - TupleShape :: M.Ty -> [M.Ty] -> Assignment FieldShape ctx -> TypeShape (StructType ctx) - ArrayShape :: M.Ty -> M.Ty -> TypeShape tp -> TypeShape (MirVectorType tp) - StructShape :: M.Ty -> [M.Ty] -> Assignment FieldShape ctx -> TypeShape AnyType - TransparentShape :: M.Ty -> TypeShape tp -> TypeShape tp - -- | Note that RefShape contains only a TypeRepr for the pointee type, not - -- a TypeShape. None of our operations need to recurse inside pointers, - -- and also this saves us from some infinite recursion. - RefShape :: M.Ty -> M.Ty -> TypeRepr tp -> TypeShape (MirReferenceType tp) - -- | Note that 'FnPtrShape' contains only 'TypeRepr's for the argument and - -- result types, not 'TypeShape's, as none of our operations need to recurse - -- inside them. - FnPtrShape :: M.Ty -> CtxRepr args -> TypeRepr ret - -> TypeShape (FunctionHandleType args ret) - --- | The TypeShape of a struct field, which might have a MaybeType wrapper to --- allow for partial initialization. -data FieldShape (tp :: CrucibleType) where - OptField :: TypeShape tp -> FieldShape (MaybeType tp) - ReqField :: TypeShape tp -> FieldShape tp - --- | Return the `TypeShape` of `ty`. --- --- It is guaranteed that the `tp :: CrucibleType` index of the resulting --- `TypeShape` matches that returned by `tyToRepr`. -tyToShape :: M.Collection -> M.Ty -> Some TypeShape -tyToShape col ty = go ty - where - go :: M.Ty -> Some TypeShape - go ty = case ty of - M.TyBool -> goPrim ty - M.TyChar -> goPrim ty - M.TyInt _ -> goPrim ty - M.TyUint _ -> goPrim ty - M.TyTuple [] -> goUnit ty - M.TyTuple tys -> goTuple ty tys - M.TyClosure tys -> goTuple ty tys - M.TyFnDef _ -> goUnit ty - M.TyArray ty' _ | Some shp <- go ty' -> Some $ ArrayShape ty ty' shp - M.TyAdt nm _ _ -> case Map.lookup nm (col ^. M.adts) of - Just adt | Just ty' <- reprTransparentFieldTy col adt -> - mapSome (TransparentShape ty) $ go ty' - Just (M.Adt _ M.Struct [v] _ _ _ _) -> goStruct ty (v ^.. M.vfields . each . M.fty) - Just (M.Adt _ ak _ _ _ _ _) -> error $ "tyToShape: AdtKind " ++ show ak ++ " NYI" - Nothing -> error $ "tyToShape: bad adt: " ++ show ty - M.TyRef ty' mutbl -> goRef ty ty' mutbl - M.TyRawPtr ty' mutbl -> goRef ty ty' mutbl - M.TyFnPtr sig -> goFnPtr ty sig - _ -> error $ "tyToShape: " ++ show ty ++ " NYI" - - goPrim :: M.Ty -> Some TypeShape - goPrim ty | Some tpr <- tyToRepr col ty, AsBaseType btpr <- asBaseType tpr = - Some $ PrimShape ty btpr - goPrim ty | Some tpr <- tyToRepr col ty = - error $ "tyToShape: type " ++ show ty ++ " produced non-primitive type " ++ show tpr - - goUnit :: M.Ty -> Some TypeShape - goUnit ty = Some $ UnitShape ty - - goTuple :: M.Ty -> [M.Ty] -> Some TypeShape - goTuple ty tys | Some flds <- loop tys Empty = Some $ TupleShape ty tys flds - where - loop :: forall ctx. [M.Ty] -> Assignment FieldShape ctx -> Some (Assignment FieldShape) - loop [] flds = Some flds - loop (ty:tys) flds | Some fld <- go ty = loop tys (flds :> OptField fld) - - goStruct :: M.Ty -> [M.Ty] -> Some TypeShape - goStruct ty tys | Some flds <- loop tys Empty = Some $ StructShape ty tys flds - where - loop :: forall ctx. [M.Ty] -> Assignment FieldShape ctx -> Some (Assignment FieldShape) - loop [] flds = Some flds - loop (ty:tys) flds | Some fld <- goField ty = loop tys (flds :> fld) - - goField :: M.Ty -> Some FieldShape - goField ty | Some shp <- go ty = case canInitialize col ty of - True -> Some $ ReqField shp - False -> Some $ OptField shp - - goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape - goRef ty ty' mutbl - | M.TySlice slicedTy <- ty' - , Some tpr <- tyToRepr col slicedTy - = Some $ - TupleShape ty [refTy, usizeTy] - (Empty - :> ReqField (RefShape refTy slicedTy tpr) - :> ReqField (PrimShape usizeTy BaseUsizeRepr)) - | M.TyStr <- ty' - = Some $ - TupleShape ty [refTy, usizeTy] - (Empty - :> ReqField (RefShape refTy (M.TyUint M.B8) (BVRepr (knownNat @8))) - :> ReqField (PrimShape usizeTy BaseUsizeRepr)) - where - -- We use a ref (of the same mutability as `ty`) when possible, to - -- avoid unnecessary clobbering. - refTy = case ty of - M.TyRef _ _ -> M.TyRef ty' mutbl - _ -> M.TyRef ty' mutbl - usizeTy = M.TyUint M.USize - goRef ty ty' _ | isUnsized ty' = error $ - "tyToShape: fat pointer " ++ show ty ++ " NYI" - goRef ty ty' _ | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' tpr - - goFnPtr :: M.Ty -> M.FnSig -> Some TypeShape - goFnPtr ty (M.FnSig args ret _abi _spread) = - tyListToCtx col args $ \argsr -> - tyToReprCont col ret $ \retr -> - Some (FnPtrShape ty argsr retr) - --- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with --- the same index `tp`. Raises an `error` if the `TypeRepr` doesn't match --- `tyToRepr ty`. -tyToShapeEq :: HasCallStack => M.Collection -> M.Ty -> TypeRepr tp -> TypeShape tp -tyToShapeEq col ty tpr | Some shp <- tyToShape col ty = - case testEquality (shapeType shp) tpr of - Just Refl -> shp - Nothing -> error $ "tyToShapeEq: type " ++ show ty ++ - " does not have representation " ++ show tpr ++ - " (got " ++ show (shapeType shp) ++ " instead)" - -shapeType :: TypeShape tp -> TypeRepr tp -shapeType shp = go shp - where - go :: forall tp. TypeShape tp -> TypeRepr tp - go (UnitShape _) = UnitRepr - go (PrimShape _ btpr) = baseToType btpr - go (TupleShape _ _ flds) = StructRepr $ fmapFC fieldShapeType flds - go (ArrayShape _ _ shp) = MirVectorRepr $ shapeType shp - go (StructShape _ _ _flds) = AnyRepr - go (TransparentShape _ shp) = go shp - go (RefShape _ _ tpr) = MirReferenceRepr tpr - go (FnPtrShape _ args ret) = FunctionHandleRepr args ret - -fieldShapeType :: FieldShape tp -> TypeRepr tp -fieldShapeType (ReqField shp) = shapeType shp -fieldShapeType (OptField shp) = MaybeRepr $ shapeType shp - -shapeMirTy :: TypeShape tp -> M.Ty -shapeMirTy (UnitShape ty) = ty -shapeMirTy (PrimShape ty _) = ty -shapeMirTy (TupleShape ty _ _) = ty -shapeMirTy (ArrayShape ty _ _) = ty -shapeMirTy (StructShape ty _ _) = ty -shapeMirTy (TransparentShape ty _) = ty -shapeMirTy (RefShape ty _ _) = ty -shapeMirTy (FnPtrShape ty _ _) = ty - -fieldShapeMirTy :: FieldShape tp -> M.Ty -fieldShapeMirTy (ReqField shp) = shapeMirTy shp -fieldShapeMirTy (OptField shp) = shapeMirTy shp -- | Run `f` on each `SymExpr` in `v`. @@ -549,28 +381,3 @@ regToTerm sym sc name w4VarMapRef shp rv = go shp rv go shp rv' goVector _shp (MirVector_Array _) = fail $ "regToTerm: MirVector_Array not supported" - -shapeToTerm :: forall tp m. - (MonadIO m, MonadFail m) => - SAW.SharedContext -> - TypeShape tp -> - m SAW.Term -shapeToTerm sc shp = go shp - where - go :: forall tp. TypeShape tp -> m SAW.Term - go (UnitShape _) = liftIO $ SAW.scUnitType sc - go (PrimShape _ BaseBoolRepr) = liftIO $ SAW.scBoolType sc - go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w) - go (TupleShape _ _ flds) = do - tys <- toListFC getConst <$> traverseFC (\x -> Const <$> goField x) flds - liftIO $ SAW.scTupleType sc tys - go (ArrayShape (M.TyArray _ n) _ shp) = do - ty <- go shp - n <- liftIO $ SAW.scNat sc (fromIntegral n) - liftIO $ SAW.scVecType sc n ty - go shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp) - - goField :: forall tp. FieldShape tp -> m SAW.Term - goField (OptField shp) = go shp - goField (ReqField shp) = go shp - diff --git a/crucible-mir-comp/src/Mir/Compositional/MethodSpec.hs b/crucible-mir-comp/src/Mir/Compositional/MethodSpec.hs deleted file mode 100644 index 9c5c2c275a..0000000000 --- a/crucible-mir-comp/src/Mir/Compositional/MethodSpec.hs +++ /dev/null @@ -1,79 +0,0 @@ -{-# Language DataKinds #-} -{-# Language TypeFamilies #-} -{-# Language OverloadedStrings #-} -{-# Language TemplateHaskell #-} - -module Mir.Compositional.MethodSpec -where - -import Control.Lens (makeLenses) -import Data.Parameterized.Classes -import Data.Parameterized.Some -import Data.Text (Text) -import qualified Prettyprinter as PP - -import Lang.Crucible.Types - -import qualified SAWScript.Crucible.Common.MethodSpec as MS -import qualified SAWScript.Crucible.Common.Override as MS - -import Mir.DefId -import Mir.Generator -import Mir.Intrinsics -import qualified Mir.Mir as M - - -type instance MS.HasSetupNull MIR = 'False -type instance MS.HasSetupGlobal MIR = 'False -type instance MS.HasSetupStruct MIR = 'True -type instance MS.HasSetupArray MIR = 'True -type instance MS.HasSetupElem MIR = 'True -type instance MS.HasSetupField MIR = 'True -type instance MS.HasSetupCast MIR = 'False -type instance MS.HasSetupUnion MIR = 'False -type instance MS.HasSetupGlobalInitializer MIR = 'False - -type instance MS.HasGhostState MIR = 'False - -type instance MS.TypeName MIR = Text -type instance MS.ExtType MIR = M.Ty - -type instance MS.MethodId MIR = DefId -type instance MS.AllocSpec MIR = Some MirAllocSpec -type instance MS.PointsTo MIR = MirPointsTo -type instance MS.ResolvedState MIR = () -type instance MS.CastType MIR = () - -type instance MS.Codebase MIR = CollectionState - -type instance MS.CrucibleContext MIR = () - -type instance MS.Pointer' MIR sym = Some (MirPointer sym) - - -data MirPointsTo = MirPointsTo MS.AllocIndex [MS.SetupValue MIR] - deriving (Show) - -instance PP.Pretty MirPointsTo where - pretty (MirPointsTo alloc sv) = PP.parens $ - PP.pretty (show alloc) PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) - -data MirAllocSpec tp = MirAllocSpec - { _maType :: TypeRepr tp - , _maMutbl :: M.Mutability - , _maMirType :: M.Ty - , _maLen :: Int - } - deriving (Show) - -instance ShowF MirAllocSpec where - -data MirPointer sym tp = MirPointer - { _mpType :: TypeRepr tp - , _mpRef :: MirReferenceMux sym tp - } - -type MIRMethodSpec = MS.CrucibleMethodSpecIR MIR - -makeLenses ''MirAllocSpec -makeLenses ''MirPointer diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs index 0553c28baf..5658d87b9e 100644 --- a/crucible-mir-comp/src/Mir/Compositional/Override.hs +++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs @@ -53,6 +53,8 @@ import qualified Verifier.SAW.TypedTerm as SAW import qualified SAWScript.Crucible.Common.MethodSpec as MS import qualified SAWScript.Crucible.Common.Override as MS +import SAWScript.Crucible.MIR.MethodSpecIR +import SAWScript.Crucible.MIR.TypeShape import Mir.Generator import Mir.Intrinsics hiding (MethodSpec) @@ -60,7 +62,6 @@ import qualified Mir.Mir as M import Mir.Compositional.Clobber import Mir.Compositional.Convert -import Mir.Compositional.MethodSpec type MirOverrideMatcher sym a = forall p rorw rtp args ret. @@ -288,7 +289,12 @@ runSpec cs mh ms = ovrWithBackend $ \bak -> Map.toList $ ms ^. MS.csPostState . MS.csAllocs postAllocMap <- liftM Map.fromList $ forM postAllocDefs $ \(alloc, Some allocSpec) -> do ref <- newMirRefSim (allocSpec ^. maType) - return (alloc, Some $ MirPointer (allocSpec ^. maType) ref) + return ( alloc + , Some $ MirPointer (allocSpec ^. maType) + (allocSpec ^. maMutbl) + (allocSpec ^. maMirType) + ref + ) let allocMap = preAllocMap <> postAllocMap -- Handle return value and post-state PointsTos @@ -403,10 +409,10 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv ", but got Any wrapping " ++ show tpr where shpTpr = StructRepr $ fmapFC fieldShapeType flds go (TransparentShape _ shp) rv sv = go shp rv sv - go (RefShape refTy _ tpr) ref (MS.SetupVar alloc) = - goRef refTy tpr ref alloc 0 - go (RefShape refTy _ tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) = - goRef refTy tpr ref alloc idx + go (RefShape refTy pointeeTy mutbl tpr) ref (MS.SetupVar alloc) = + goRef refTy pointeeTy mutbl tpr ref alloc 0 + go (RefShape refTy pointeeTy mutbl tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) = + goRef refTy pointeeTy mutbl tpr ref alloc idx go (FnPtrShape _ _ _) _ _ = error "Function pointers not currently supported in overrides" go shp _ sv = error $ "matchArg: type error: bad SetupValue " ++ @@ -432,13 +438,15 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv goRef :: forall tp'. M.Ty -> + M.Ty -> + M.Mutability -> TypeRepr tp' -> MirReferenceMux sym tp' -> MS.AllocIndex -> -- | The expected offset of `ref` past the start of the allocation. Int -> MirOverrideMatcher sym () - goRef refTy tpr ref alloc refOffset = do + goRef refTy pointeeTy mutbl tpr ref alloc refOffset = do partIdxLen <- lift $ mirRef_indexAndLenSim ref optIdxLen <- liftIO $ readPartExprMaybe sym partIdxLen let (optIdx, optLen) = @@ -486,7 +494,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv SimError loc (AssertFailureSimError ("mismatch on " ++ show alloc) "") | otherwise -> error $ "mismatched types for " ++ show alloc ++ ": " ++ show tpr ++ " does not match " ++ show (ptr ^. mpType) - MS.setupValueSub %= Map.insert alloc (Some $ MirPointer tpr ref') + MS.setupValueSub %= Map.insert alloc (Some $ MirPointer tpr mutbl pointeeTy ref') -- | Convert a SetupValue to a RegValue. This is used for MethodSpec outputs, @@ -524,7 +532,7 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv go (StructShape _ _ flds) (MS.SetupStruct _ False svs) = AnyValue (StructRepr $ fmapFC fieldShapeType flds) <$> goFields flds svs go (TransparentShape _ shp) sv = go shp sv - go (RefShape _ _ tpr) (MS.SetupVar alloc) = case Map.lookup alloc allocMap of + go (RefShape _ _ _ tpr) (MS.SetupVar alloc) = case Map.lookup alloc allocMap of Just (Some ptr) -> case testEquality tpr (ptr ^. mpType) of Just Refl -> return $ ptr ^. mpRef Nothing -> error $ "setupToReg: type error: bad reference type for " ++ show alloc ++ diff --git a/crux-mir-comp/crux-mir-comp.cabal b/crux-mir-comp/crux-mir-comp.cabal index 199b7c991d..e51d5feaad 100644 --- a/crux-mir-comp/crux-mir-comp.cabal +++ b/crux-mir-comp/crux-mir-comp.cabal @@ -34,6 +34,7 @@ library crux-mir, saw-core, saw-core-what4, + saw-script, cryptol, cryptol-saw-core diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs index 17bc207a59..ccc45ba518 100644 --- a/crux-mir-comp/src/Mir/Cryptol.hs +++ b/crux-mir-comp/src/Mir/Cryptol.hs @@ -61,6 +61,8 @@ import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW import qualified Verifier.SAW.Recognizer as SAW (asExtCns) import qualified Verifier.SAW.TypedTerm as SAW +import SAWScript.Crucible.MIR.TypeShape + import Mir.Compositional.Convert import Mir.Compositional.DefId (hasInstPrefix) diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 586d06e7c8..645757cbc5 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1737,9 +1737,9 @@ file to the `mir_load_module` function: * `mir_load_module : String -> TopLevel MIRModule` -SAW currently supports Rust code that can be built with a [March 22, 2020 Rust -nightly](https://static.rust-lang.org/dist/2020-03-22/). If you encounter a -Rust feature that SAW does not support, please report it [on +SAW currently supports Rust code that can be built with a [January 23, 2023 +Rust nightly](https://static.rust-lang.org/dist/2023-01-23/). If you encounter +a Rust feature that SAW does not support, please report it [on GitHub](https://github.com/GaloisInc/saw-script/issues). ## Notes on Compiling Code for SAW @@ -1913,7 +1913,7 @@ allocated during execution is allowed). The direct extraction process just discussed automatically introduces symbolic variables and then abstracts over them, yielding a SAWScript -`Term` that reflects the semantics of the original Java or LLVM code. +`Term` that reflects the semantics of the original Java, LLVM, or MIR code. For simple functions, this is often the most convenient interface. For more complex code, however, it can be necessary (or more natural) to specifically introduce fresh variables and indicate what portions of the @@ -2040,7 +2040,7 @@ The built-in functions described so far work by extracting models of code that can then be used for a variety of purposes, including proofs about the properties of the code. -When the goal is to prove equivalence between some LLVM or Java code and +When the goal is to prove equivalence between some LLVM, Java, or MIR code and a specification, however, a more declarative approach is sometimes convenient. The following sections describe an approach that combines model extraction and verification with respect to a specification. A @@ -2072,8 +2072,7 @@ gives the proof script to use for verification. The result is a proved specification that can be used to simplify verification of functions that call this one. -A similar command for JVM programs is available if `enable_experimental` -has been run. +Similar commands are available for JVM programs: ~~~~ jvm_verify : @@ -2086,8 +2085,81 @@ jvm_verify : TopLevel JVMMethodSpec ~~~~ -Now we describe how to construct a value of type `LLVMSetup ()` (or -`JVMSetup ()`). +And for MIR programs: + +~~~~ +mir_verify : + MIRModule -> + String -> + [MIRSpec] -> + Bool -> + MIRSetup () -> + ProofScript () -> + TopLevel MIRSpec +~~~~ + +### Running a MIR-based verification + +`mir_verify` requires `enable_experimental` in order to be used. Moreover, +some parts of `mir_verify` are not currently implemented, so it is possible +that using `mir_verify` on some programs will fail. Features that are not yet +implemented include the following: + +* MIR specifications involving memory allocations (i.e., neither the + `mir_alloc` nor the `mir_points_to` commands are functional) +* MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to + `mir_verify` must always be the empty list at present) +* The ability to construct MIR `struct` or `enum` values in specifications +* The ability to specify the layout of slice values + +The `String` supplied as an argument to `mir_verify` is expected to be a +function _identifier_. An identifier is expected adhere to one of the following +conventions: + +* `/::` +* `::` + +Where: + +* `` is the name of the crate in which the function is defined. (If + you produced your MIR JSON file by compiling a single `.rs` file with + `saw-rustc`, then the crate name is the same as the name of the file, but + without the `.rs` file extension.) +* `` is a hash of the crate and its dependencies. In extreme + cases, it is possible for two different crates to have identical crate names, + in which case the disambiguator must be used to distinguish between the two + crates. In the common case, however, most crate names will correspond to + exactly one disambiguator, and you are allowed to leave out the + `/` part of the `String` in this case. If you supply an + identifier with an ambiguous crate name and omit the disambiguator, then SAW + will raise an error. +* `` is the path to the function within the crate. Sometimes, + this is as simple as the function name itself. In other cases, a function + path may involve multiple _segments_, depending on the module hierarchy for + the program being verified. For instance, a `read` function located in + `core/src/ptr/mod.rs` will have the identifier: + + ``` + core::ptr::read + ``` + + Where `core` is the crate name and `ptr::read` is the function path, which + has two segments `ptr` and `read`. There are also some special forms of + segments that appear for functions defined in certain language constructs. + For instance, if a function is defined in an `impl` block, then it will have + `{impl}` as one of its segments, e.g., + + ``` + core::ptr::const_ptr::{impl}::offset + ``` + + If you are in doubt about what the full identifier for a given function is, + consult the MIR JSON file for your program. + +----- + +Now we describe how to construct a value of type `LLVMSetup ()`, `JVMSetup ()`, +or `MIRSetup ()`. ## Structure of a Specification @@ -2099,32 +2171,32 @@ A specifications for Crucible consists of three logical components: * A specification of the expected final value of the program state. -These three portions of the specification are written in sequence within -a `do` block of `LLVMSetup` (or `JVMSetup`) type. The command -`llvm_execute_func` (or `jvm_execute_func`) separates the -specification of the initial state from the specification of the final -state, and specifies the arguments to the function in terms of the -initial state. Most of the commands available for state description will -work either before or after `llvm_execute_func`, though with -slightly different meaning, as described below. +These three portions of the specification are written in sequence within a `do` +block of type `{LLVM,JVM,MIR}Setup`. The command `{llvm,jvm,mir}_execute_func` +separates the specification of the initial state from the specification of the +final state, and specifies the arguments to the function in terms of the +initial state. Most of the commands available for state description will work +either before or after `{llvm,jvm,mir}_execute_func`, though with slightly +different meaning, as described below. ## Creating Fresh Variables -In any case where you want to prove a property of a function for an -entire class of inputs (perhaps all inputs) rather than concrete values, -the initial values of at least some elements of the program state must -contain fresh variables. These are created in a specification with the -`llvm_fresh_var` and `jvm_fresh_var` commands rather than -`fresh_symbolic`. +In any case where you want to prove a property of a function for an entire +class of inputs (perhaps all inputs) rather than concrete values, the initial +values of at least some elements of the program state must contain fresh +variables. These are created in a specification with the +`{llvm,jvm,mir}_fresh_var` commands rather than `fresh_symbolic`. * `llvm_fresh_var : String -> LLVMType -> LLVMSetup Term` * `jvm_fresh_var : String -> JavaType -> JVMSetup Term` +* `mir_fresh_var : String -> MIRType -> MIRSetup Term` + The first parameter to both functions is a name, used only for presentation. It's possible (though not recommended) to create multiple variables with the same name, but SAW will distinguish between them -internally. The second parameter is the LLVM (or Java) type of the +internally. The second parameter is the LLVM, Java, or MIR type of the variable. The resulting `Term` can be used in various subsequent commands. @@ -2151,6 +2223,31 @@ Java types are built up using the following functions: * `java_class : String -> JavaType` * `java_array : Int -> JavaType -> JavaType` +MIR types are built up using the following functions: + +* `mir_array : Int -> MIRType -> MIRType` +* `mir_bool : MIRType` +* `mir_char : MIRType` +* `mir_i8 : MIRType` +* `mir_i6 : MIRType` +* `mir_i32 : MIRType` +* `mir_i64 : MIRType` +* `mir_i128 : MIRType` +* `mir_isize : MIRType` +* `mir_f32 : MIRType` +* `mir_f64 : MIRType` +* `mir_ref : MIRType -> MIRType` +* `mir_ref_mut : MIRType -> MIRType` +* `mir_slice : MIRType -> MIRType` +* `mir_str : MIRType` +* `mir_tuple : [MIRType] -> MIRType` +* `mir_u8 : MIRType` +* `mir_u6 : MIRType` +* `mir_u32 : MIRType` +* `mir_u64 : MIRType` +* `mir_u128 : MIRType` +* `mir_usize : MIRType` + Most of these types are straightforward mappings to the standard LLVM and Java types. The one key difference is that arrays must have a fixed, concrete size. Therefore, all analysis results are valid only under the @@ -2189,27 +2286,31 @@ values that can occur during symbolic execution, which includes both `Term` values, pointers, and composite types consisting of either of these (both structures and arrays). -The `llvm_term` and `jvm_term` functions create a `SetupValue` or -`JVMValue` from a `Term`: +The `llvm_term`, `jvm_term`, and `mir_term` functions create a `SetupValue`, +`JVMValue`, or `MIRValue`, respectively, from a `Term`: * `llvm_term : Term -> SetupValue` * `jvm_term : Term -> JVMValue` +* `mir_term : Term -> MIRValue` ## Executing -Once the initial state has been configured, the `llvm_execute_func` +Once the initial state has been configured, the `{llvm,jvm,mir}_execute_func` command specifies the parameters of the function being analyzed in terms of the state elements already configured. * `llvm_execute_func : [SetupValue] -> LLVMSetup ()` +* `jvm_execute_func : [JVMValue] -> JVMSetup ()` +* `mir_execute_func : [MIRValue] -> MIRSetup ()` ## Return Values To specify the value that should be returned by the function being -verified use the `llvm_return` or `jvm_return` command. +verified use the `{llvm,jvm,mir}_return` command. * `llvm_return : SetupValue -> LLVMSetup ()` * `jvm_return : JVMValue -> JVMSetup ()` +* `mir_return : MIRValue -> MIRSetup ()` ## A First Simple Example @@ -2252,11 +2353,11 @@ of properties we have already proved about its callees rather than analyzing them anew. This enables us to reason about much larger and more complex systems than otherwise possible. -The `llvm_verify` and `jvm_verify` functions return values of -type `CrucibleMethodSpec` and `JVMMethodSpec`, respectively. These -values are opaque objects that internally contain both the information -provided in the associated `JVMSetup` or `LLVMSetup` blocks and -the results of the verification process. +The `llvm_verify`, `jvm_verify`, and `mir_verify` functions return values of +type `CrucibleMethodSpec`, `JVMMethodSpec`, and `MIRMethodSpec`, respectively. +These values are opaque objects that internally contain both the information +provided in the associated `LLVMSetup`, `JVMSetup`, or `MIRSetup` blocks, +respectively, and the results of the verification process. Any of these `MethodSpec` objects can be passed in via the third argument of the `..._verify` functions. For any function or method @@ -2265,7 +2366,7 @@ calls to the associated target. Instead, it will perform the following steps: * Check that all `llvm_points_to` and `llvm_precond` statements - (or the corresponding JVM statements) in the specification are + (or the corresponding JVM or MIR statements) in the specification are satisfied. * Update the simulator state and optionally construct a return value as @@ -2326,6 +2427,14 @@ array of the given concrete size, with elements of the given type. * `jvm_alloc_object : String -> JVMSetup JVMValue` specifies an object of the given class name. +The experimental MIR implementation also has a `mir_alloc` function, which +behaves similarly to `llvm_alloc`. `mir_alloc` creates an immutable reference, +but there is also a `mir_alloc_mut` function for creating a mutable reference: + +* `mir_alloc : MIRType -> MIRSetup SetupValue` + +* `mir_alloc_mut : MIRType -> MIRSetup SetupValue` + In LLVM, it's also possible to construct fresh pointers that do not point to allocated memory (which can be useful for functions that manipulate pointers but not the values they point to): @@ -2650,6 +2759,9 @@ values in scope at the time. * `jvm_precond : Term -> JVMSetup ()` * `jvm_postcond : Term -> JVMSetup ()` * `jvm_assert : Term -> JVMSetup ()` +* `mir_precond : Term -> MIRSetup ()` +* `mir_postcond : Term -> MIRSetup ()` +* `mir_assert : Term -> MIRSetup ()` These commands take `Term` arguments, and therefore cannot describe the values of pointers. The "assert" variants will work in either pre- @@ -3512,7 +3624,7 @@ N.B: The following commands must first be enabled using `enable_experimental`. s : out std_logic ); end half; - + entity full is port ( a : in std_logic; diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 1d5bba2dc3..228adb1af1 100644 Binary files a/doc/manual/manual.pdf and b/doc/manual/manual.pdf differ diff --git a/intTests/test_mir_load_module/Makefile b/intTests/test_mir_load_module/Makefile index eddd5ee141..bc6297ae15 100644 --- a/intTests/test_mir_load_module/Makefile +++ b/intTests/test_mir_load_module/Makefile @@ -1,8 +1,13 @@ -all: test.json +all: test.linked-mir.json test.linked-mir.json: test.rs saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib .PHONY: clean -clean: +clean: remove-unused-build-artifacts rm -f test.linked-mir.json diff --git a/intTests/test_mir_verify_basic/Makefile b/intTests/test_mir_verify_basic/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_verify_basic/Makefile @@ -0,0 +1,13 @@ +all: test.linked-mir.json + +test.linked-mir.json: test.rs + saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib + +.PHONY: clean +clean: remove-unused-build-artifacts + rm -f test.linked-mir.json diff --git a/intTests/test_mir_verify_basic/test.linked-mir.json b/intTests/test_mir_verify_basic/test.linked-mir.json new file mode 100644 index 0000000000..341daed006 --- /dev/null +++ b/intTests/test_mir_verify_basic/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}},"pos":"test.rs:14:5: 14:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i32"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:15:2: 15:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}]},"name":"test/775505e0::id_i32","return_ty":"ty::i32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":true,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::e93222e871854c41"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:51:2: 51:2"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/775505e0::id_unit","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i16"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i16"}},"pos":"test.rs:10:5: 10:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i16"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:11:2: 11:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i16"}]},"name":"test/775505e0::id_i16","return_ty":"ty::i16","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:1:26: 1:27","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"5"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:26: 1:27"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/775505e0::id_array::{constant#0}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}},"pos":"test.rs:30:5: 30:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u8"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:31:2: 31:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u8"}]},"name":"test/775505e0::id_u8","return_ty":"ty::u8","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::isize"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}},"pos":"test.rs:22:5: 22:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::isize"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:23:2: 23:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::isize"}]},"name":"test/775505e0::id_isize","return_ty":"ty::isize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u16"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u16"}},"pos":"test.rs:34:5: 34:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u16"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:35:2: 35:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u16"}]},"name":"test/775505e0::id_u16","return_ty":"ty::u16","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:38:5: 38:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:39:2: 39:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"test/775505e0::id_u32","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:1:39: 1:40","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"usize","size":8,"val":"5"},"ty":"ty::usize"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:39: 1:40"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/775505e0::id_array::{constant#1}","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}},"pos":"test.rs:26:5: 26:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Tuple::f54c7b3282e27392"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:27:2: 27:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::f54c7b3282e27392"}]},"name":"test/775505e0::id_tuple","return_ty":"ty::Tuple::f54c7b3282e27392","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i64"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i64"}},"pos":"test.rs:18:5: 18:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i64"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:19:2: 19:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i64"}]},"name":"test/775505e0::id_i64","return_ty":"ty::i64","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i8"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i8"}},"pos":"test.rs:6:5: 6:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::i8"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:7:2: 7:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i8"}]},"name":"test/775505e0::id_i8","return_ty":"ty::i8","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u64"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u64"}},"pos":"test.rs:42:5: 42:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u64"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:43:2: 43:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u64"}]},"name":"test/775505e0::id_u64","return_ty":"ty::u64","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::usize"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}},"pos":"test.rs:46:5: 46:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::usize"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:47:2: 47:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::usize"}]},"name":"test/775505e0::id_usize","return_ty":"ty::usize","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::a60250c8af2ca6f4"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::a60250c8af2ca6f4"}},"pos":"test.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Array::a60250c8af2ca6f4"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Array::a60250c8af2ca6f4"}]},"name":"test/775505e0::id_array","return_ty":"ty::Array::a60250c8af2ca6f4","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/775505e0::id_i32","kind":"Item","substs":[]},"name":"test/775505e0::id_i32"},{"inst":{"def_id":"test/775505e0::id_unit","kind":"Item","substs":[]},"name":"test/775505e0::id_unit"},{"inst":{"def_id":"test/775505e0::id_i16","kind":"Item","substs":[]},"name":"test/775505e0::id_i16"},{"inst":{"def_id":"test/775505e0::id_array::{constant#0}","kind":"Item","substs":[]},"name":"test/775505e0::id_array::{constant#0}"},{"inst":{"def_id":"test/775505e0::id_u8","kind":"Item","substs":[]},"name":"test/775505e0::id_u8"},{"inst":{"def_id":"test/775505e0::id_isize","kind":"Item","substs":[]},"name":"test/775505e0::id_isize"},{"inst":{"def_id":"test/775505e0::id_u16","kind":"Item","substs":[]},"name":"test/775505e0::id_u16"},{"inst":{"def_id":"test/775505e0::id_u32","kind":"Item","substs":[]},"name":"test/775505e0::id_u32"},{"inst":{"def_id":"test/775505e0::id_array::{constant#1}","kind":"Item","substs":[]},"name":"test/775505e0::id_array::{constant#1}"},{"inst":{"def_id":"test/775505e0::id_tuple","kind":"Item","substs":[]},"name":"test/775505e0::id_tuple"},{"inst":{"def_id":"test/775505e0::id_i64","kind":"Item","substs":[]},"name":"test/775505e0::id_i64"},{"inst":{"def_id":"test/775505e0::id_i8","kind":"Item","substs":[]},"name":"test/775505e0::id_i8"},{"inst":{"def_id":"test/775505e0::id_u64","kind":"Item","substs":[]},"name":"test/775505e0::id_u64"},{"inst":{"def_id":"test/775505e0::id_usize","kind":"Item","substs":[]},"name":"test/775505e0::id_usize"},{"inst":{"def_id":"test/775505e0::id_array","kind":"Item","substs":[]},"name":"test/775505e0::id_array"}],"tys":[{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::i16","ty":{"intkind":{"kind":"I16"},"kind":"Int"}},{"name":"ty::usize","ty":{"kind":"Uint","uintkind":{"kind":"Usize"}}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::u16","ty":{"kind":"Uint","uintkind":{"kind":"U16"}}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Tuple::f54c7b3282e27392","ty":{"kind":"Tuple","tys":["ty::u32","ty::u32"]}},{"name":"ty::i64","ty":{"intkind":{"kind":"I64"},"kind":"Int"}},{"name":"ty::i8","ty":{"intkind":{"kind":"I8"},"kind":"Int"}},{"name":"ty::u64","ty":{"kind":"Uint","uintkind":{"kind":"U64"}}},{"name":"ty::Array::a60250c8af2ca6f4","ty":{"kind":"Array","size":{"rendered":{"kind":"usize","size":8,"val":"5"},"ty":"ty::usize"},"ty":"ty::u32"}}],"roots":["test/775505e0::id_array","test/775505e0::id_array::{constant#0}","test/775505e0::id_array::{constant#1}","test/775505e0::id_i8","test/775505e0::id_i16","test/775505e0::id_i32","test/775505e0::id_i64","test/775505e0::id_isize","test/775505e0::id_tuple","test/775505e0::id_u8","test/775505e0::id_u16","test/775505e0::id_u32","test/775505e0::id_u64","test/775505e0::id_usize","test/775505e0::id_unit"]} \ No newline at end of file diff --git a/intTests/test_mir_verify_basic/test.rs b/intTests/test_mir_verify_basic/test.rs new file mode 100644 index 0000000000..aba26f5700 --- /dev/null +++ b/intTests/test_mir_verify_basic/test.rs @@ -0,0 +1,51 @@ +pub fn id_array(x: [u32; 5]) -> [u32; 5] { + x +} + +pub fn id_i8(x: i8) -> i8 { + x +} + +pub fn id_i16(x: i16) -> i16 { + x +} + +pub fn id_i32(x: i32) -> i32 { + x +} + +pub fn id_i64(x: i64) -> i64 { + x +} + +pub fn id_isize(x: isize) -> isize { + x +} + +pub fn id_tuple(x: (u32, u32)) -> (u32, u32) { + x +} + +pub fn id_u8(x: u8) -> u8 { + x +} + +pub fn id_u16(x: u16) -> u16 { + x +} + +pub fn id_u32(x: u32) -> u32 { + x +} + +pub fn id_u64(x: u64) -> u64 { + x +} + +pub fn id_usize(x: usize) -> usize { + x +} + +pub fn id_unit(x: ()) -> () { + x +} diff --git a/intTests/test_mir_verify_basic/test.saw b/intTests/test_mir_verify_basic/test.saw new file mode 100644 index 0000000000..5499e61850 --- /dev/null +++ b/intTests/test_mir_verify_basic/test.saw @@ -0,0 +1,87 @@ +enable_experimental; + +// Specifications using `mir_fresh_var` + +let id_spec mty = do { + x <- mir_fresh_var "x" mty; + + mir_execute_func [mir_term x]; + + mir_return (mir_term x); +}; + +let id_u32_wrong = do { + x <- mir_fresh_var "x" (mir_u32); + + mir_execute_func [mir_term x]; + + mir_return (mir_term {{ x + 1 : [32] }}); +}; + +let id_unit = do { + x <- mir_fresh_var "x" (mir_tuple []); + + mir_execute_func [mir_term x]; +}; + +// Specifications using specific Cryptol terms + +let id_array_cryptol_spec = do { + let t = mir_term {{ [42, 27, 100, 27, 42] : [5][32] }}; + + mir_execute_func [t]; + + mir_return t; +}; + +let id_tuple_cryptol_spec = do { + let t = mir_term {{ (42, 27) : ([32], [32]) }}; + + mir_execute_func [t]; + + mir_return t; +}; + +let id_u32_cryptol_spec = do { + let t = mir_term {{ 42 : [32] }}; + + mir_execute_func [t]; + + mir_return t; +}; + +let id_unit_cryptol_spec = do { + mir_execute_func [mir_term {{ () }}]; +}; + +///// + +m <- mir_load_module "test.linked-mir.json"; + +mir_verify m "test::id_array" [] false (id_spec (mir_array 5 mir_u32)) z3; +mir_verify m "test::id_i8" [] false (id_spec mir_i8) z3; +mir_verify m "test::id_i16" [] false (id_spec mir_i16) z3; +mir_verify m "test::id_i32" [] false (id_spec mir_i32) z3; +mir_verify m "test::id_i64" [] false (id_spec mir_i64) z3; +mir_verify m "test::id_isize" [] false (id_spec mir_isize) z3; +mir_verify m "test::id_tuple" [] false (id_spec (mir_tuple [mir_u32, mir_u32])) z3; +mir_verify m "test::id_u8" [] false (id_spec mir_u8) z3; +mir_verify m "test::id_u16" [] false (id_spec mir_u16) z3; +mir_verify m "test::id_u32" [] false (id_spec mir_u32) z3; +mir_verify m "test::id_u64" [] false (id_spec mir_u64) z3; +mir_verify m "test::id_usize" [] false (id_spec mir_usize) z3; +mir_verify m "test::id_unit" [] false id_unit z3; + +// Test using fully disambiguated names +mir_verify m "test/775505e0::id_u8" [] false (id_spec mir_u8) z3; +mir_verify m "test/775505e0::id_u8[0]" [] false (id_spec mir_u8) z3; + +mir_verify m "test::id_array" [] false id_array_cryptol_spec z3; +mir_verify m "test::id_tuple" [] false id_tuple_cryptol_spec z3; +mir_verify m "test::id_u32" [] false id_u32_cryptol_spec z3; +mir_verify m "test::id_unit" [] false id_unit_cryptol_spec z3; + +// A specification that is expected to fail +fails ( + mir_verify m "test::id_u32" [] false id_u32_wrong z3 +); diff --git a/intTests/test_mir_verify_basic/test.sh b/intTests/test_mir_verify_basic/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_verify_basic/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/intTests/test_mir_verify_conds/Makefile b/intTests/test_mir_verify_conds/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_verify_conds/Makefile @@ -0,0 +1,13 @@ +all: test.linked-mir.json + +test.linked-mir.json: test.rs + saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib + +.PHONY: clean +clean: remove-unused-build-artifacts + rm -f test.linked-mir.json diff --git a/intTests/test_mir_verify_conds/test.linked-mir.json b/intTests/test_mir_verify_conds/test.linked-mir.json new file mode 100644 index 0000000000..c1a7cf2328 --- /dev/null +++ b/intTests/test_mir_verify_conds/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:2:5: 2:10","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"1"},"ty":"ty::u32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _2 + const 1_u32`, which would overflow","pos":"test.rs:2:5: 2:10","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:2:5: 2:10","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}}],"terminator":{"kind":"Return","pos":"test.rs:3:2: 3:2"}},"blockid":"bb1"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Tuple::7063e33f0dbc8a58"}]},"name":"test/4ae812d0::add1","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/4ae812d0::add1","kind":"Item","substs":[]},"name":"test/4ae812d0::add1"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}}],"roots":["test/4ae812d0::add1"]} \ No newline at end of file diff --git a/intTests/test_mir_verify_conds/test.rs b/intTests/test_mir_verify_conds/test.rs new file mode 100644 index 0000000000..1161df5eea --- /dev/null +++ b/intTests/test_mir_verify_conds/test.rs @@ -0,0 +1,3 @@ +pub fn add1(x: u32) -> u32 { + x + 1 +} diff --git a/intTests/test_mir_verify_conds/test.saw b/intTests/test_mir_verify_conds/test.saw new file mode 100644 index 0000000000..c35419ea13 --- /dev/null +++ b/intTests/test_mir_verify_conds/test.saw @@ -0,0 +1,56 @@ +enable_experimental; + +// A spec using mir_precond + +let add1_precond_spec = do { + x <- mir_fresh_var "x" mir_u32; + mir_precond {{ x < 0xffffffff }}; + + mir_execute_func [mir_term x]; + + mir_return (mir_term {{ x + 1 }}); +}; + +// A spec using mir_assert in a precondition + +let add1_precond_assert_spec = do { + x <- mir_fresh_var "x" mir_u32; + mir_assert {{ x < 0xffffffff }}; + + mir_execute_func [mir_term x]; + + mir_return (mir_term {{ x + 1 }}); +}; + +// A spec using mir_postcond + +let add1_postcond_spec = do { + x <- mir_fresh_var "x" mir_u32; + mir_precond {{ x < 0xffffffff }}; + + mir_execute_func [mir_term x]; + + x' <- mir_fresh_var "x'" mir_u32; + mir_return (mir_term x'); + mir_postcond {{ x < x' }}; +}; + +// A spec using mir_assert in a postcondition + +let add1_postcond_assert_spec = do { + x <- mir_fresh_var "x" mir_u32; + mir_precond {{ x < 0xffffffff }}; + + mir_execute_func [mir_term x]; + + x' <- mir_fresh_var "x'" mir_u32; + mir_return (mir_term x'); + mir_assert {{ x < x' }}; +}; + +m <- mir_load_module "test.linked-mir.json"; + +mir_verify m "test::add1" [] false add1_precond_spec z3; +mir_verify m "test::add1" [] false add1_precond_assert_spec z3; +mir_verify m "test::add1" [] false add1_postcond_spec z3; +mir_verify m "test::add1" [] false add1_postcond_assert_spec z3; diff --git a/intTests/test_mir_verify_conds/test.sh b/intTests/test_mir_verify_conds/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_verify_conds/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/intTests/test_mir_verify_pop_count/Makefile b/intTests/test_mir_verify_pop_count/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test_mir_verify_pop_count/Makefile @@ -0,0 +1,13 @@ +all: test.linked-mir.json + +test.linked-mir.json: test.rs + saw-rustc $< + $(MAKE) remove-unused-build-artifacts + +.PHONY: remove-unused-build-artifacts +remove-unused-build-artifacts: + rm -f test libtest.mir libtest.rlib + +.PHONY: clean +clean: remove-unused-build-artifacts + rm -f test.linked-mir.json diff --git a/intTests/test_mir_verify_pop_count/test.linked-mir.json b/intTests/test_mir_verify_pop_count/test.linked-mir.json new file mode 100644 index 0000000000..92496ab136 --- /dev/null +++ b/intTests/test_mir_verify_pop_count/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"pos":"test.rs:3:9: 3:10","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"pos":"test.rs:3:15: 3:16","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:3:14: 3:22","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"int","size":4,"val":"1"},"ty":"ty::i32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Shr"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to shift right by `const 1_i32`, which would overflow","pos":"test.rs:3:14: 3:22","target":"bb1"}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"pos":"test.rs:3:14: 3:22","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:3:13: 3:36","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"1431655765"},"ty":"ty::u32"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"BitAnd"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:3:9: 3:36","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Sub"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _2 - move _3`, which would overflow","pos":"test.rs:3:9: 3:36","target":"bb2"}},"blockid":"bb1"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"pos":"test.rs:3:5: 3:36","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::u32"}},"pos":"test.rs:4:10: 4:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::u32"}},"pos":"test.rs:4:9: 4:25","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"858993459"},"ty":"ty::u32"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"BitAnd"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::u32"}},"pos":"test.rs:4:30: 4:31","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:4:29: 4:37","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"int","size":4,"val":"2"},"ty":"ty::i32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Shr"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to shift right by `const 2_i32`, which would overflow","pos":"test.rs:4:29: 4:37","target":"bb3"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::u32"}},"pos":"test.rs:4:29: 4:37","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::u32"}},"pos":"test.rs:4:28: 4:51","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"858993459"},"ty":"ty::u32"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"BitAnd"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:4:9: 4:51","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _8 + move _10`, which would overflow","pos":"test.rs:4:9: 4:51","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"pos":"test.rs:4:5: 4:51","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::u32"}},"pos":"test.rs:5:10: 5:11","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::u32"}},"pos":"test.rs:5:15: 5:16","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:5:14: 5:22","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"int","size":4,"val":"4"},"ty":"ty::i32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Shr"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to shift right by `const 4_i32`, which would overflow","pos":"test.rs:5:14: 5:22","target":"bb5"}},"blockid":"bb4"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::u32"}},"pos":"test.rs:5:14: 5:22","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:5:9: 5:23","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _16 + move _17`, which would overflow","pos":"test.rs:5:9: 5:23","target":"bb6"}},"blockid":"bb5"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::u32"}},"pos":"test.rs:5:9: 5:23","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"pos":"test.rs:5:5: 5:36","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"252645135"},"ty":"ty::u32"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"BitAnd"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::u32"}},"pos":"test.rs:6:9: 6:10","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::u32"}},"pos":"test.rs:6:14: 6:15","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:6:13: 6:21","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"int","size":4,"val":"8"},"ty":"ty::i32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Shr"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to shift right by `const 8_i32`, which would overflow","pos":"test.rs:6:13: 6:21","target":"bb7"}},"blockid":"bb6"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::u32"}},"pos":"test.rs:6:13: 6:21","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:6:9: 6:21","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _21 + move _22`, which would overflow","pos":"test.rs:6:9: 6:21","target":"bb8"}},"blockid":"bb7"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"pos":"test.rs:6:5: 6:21","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::u32"}},"pos":"test.rs:7:9: 7:10","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_28","ty":"ty::u32"}},"pos":"test.rs:7:14: 7:15","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_29","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:7:13: 7:22","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_28","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"rendered":{"kind":"int","size":4,"val":"16"},"ty":"ty::i32"},"kind":"Constant"},"kind":"CheckedBinaryOp","op":{"kind":"Shr"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_29","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to shift right by `const 16_i32`, which would overflow","pos":"test.rs:7:13: 7:22","target":"bb9"}},"blockid":"bb8"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::u32"}},"pos":"test.rs:7:13: 7:22","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_29","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_30","ty":"ty::Tuple::7063e33f0dbc8a58"}},"pos":"test.rs:7:9: 7:22","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::u32"}},"kind":"Copy"},"R":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::u32"}},"kind":"Copy"},"kind":"CheckedBinaryOp","op":{"kind":"Add"}}}],"terminator":{"cleanup":null,"cond":{"data":{"data":[{"field":1,"kind":"Field","ty":"ty::bool"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_30","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"},"expected":false,"kind":"Assert","msg":"attempt to compute `move _26 + move _27`, which would overflow","pos":"test.rs:7:9: 7:22","target":"bb10"}},"blockid":"bb9"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"pos":"test.rs:7:5: 7:22","rhs":{"kind":"Use","usevar":{"data":{"data":[{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_30","ty":"ty::Tuple::7063e33f0dbc8a58"}},"kind":"Move"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_31","ty":"ty::u32"}},"pos":"test.rs:8:5: 8:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:8:5: 8:19","rhs":{"L":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_31","ty":"ty::u32"}},"kind":"Move"},"R":{"data":{"rendered":{"kind":"uint","size":4,"val":"63"},"ty":"ty::u32"},"kind":"Constant"},"kind":"BinaryOp","op":{"kind":"BitAnd"}}}],"terminator":{"kind":"Return","pos":"test.rs:9:2: 9:2"}},"blockid":"bb10"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_4","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_5","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_6","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_7","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_8","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_9","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_10","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_11","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_12","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_13","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_14","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_15","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_16","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_17","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_18","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_19","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_20","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_21","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_22","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_23","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_24","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_25","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_26","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_27","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_28","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_29","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_30","ty":"ty::Tuple::7063e33f0dbc8a58"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_31","ty":"ty::u32"}]},"name":"test/6f0edd4f::pop_count","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/6f0edd4f::pop_count","kind":"Item","substs":[]},"name":"test/6f0edd4f::pop_count"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::7063e33f0dbc8a58","ty":{"kind":"Tuple","tys":["ty::u32","ty::bool"]}},{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}}],"roots":["test/6f0edd4f::pop_count"]} \ No newline at end of file diff --git a/intTests/test_mir_verify_pop_count/test.rs b/intTests/test_mir_verify_pop_count/test.rs new file mode 100644 index 0000000000..5d804221ea --- /dev/null +++ b/intTests/test_mir_verify_pop_count/test.rs @@ -0,0 +1,9 @@ +// From the book "Hacker's Delight" by Henry S. Warren, Jr. +pub fn pop_count(mut x: u32) -> u32 { + x = x - ((x >> 1) & 0x55555555); + x = (x & 0x33333333) + ((x >> 2) & 0x33333333); + x = (x + (x >> 4)) & 0x0F0F0F0F; + x = x + (x >> 8); + x = x + (x >> 16); + x & 0x0000003F +} diff --git a/intTests/test_mir_verify_pop_count/test.saw b/intTests/test_mir_verify_pop_count/test.saw new file mode 100644 index 0000000000..5fd5ac5a56 --- /dev/null +++ b/intTests/test_mir_verify_pop_count/test.saw @@ -0,0 +1,19 @@ +enable_experimental; + +let +{{ +popCount : [32] -> [32] +popCount bs = zext`{32,6} (ic ! 0) where + ic = [0] # [ if elt then prev + 1 else prev | elt <- bs | prev <- ic] +}}; + +let pop_count_spec = do { + x <- mir_fresh_var "x" mir_u32; + + mir_execute_func [mir_term x]; + + mir_return (mir_term {{ popCount x }}); +}; + +m <- mir_load_module "test.linked-mir.json"; +mir_verify m "test::pop_count" [] false pop_count_spec z3; diff --git a/intTests/test_mir_verify_pop_count/test.sh b/intTests/test_mir_verify_pop_count/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_verify_pop_count/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/saw-remote-api/docs/SAW.rst b/saw-remote-api/docs/SAW.rst index 34a12df8a8..bfaecdf7e6 100644 --- a/saw-remote-api/docs/SAW.rst +++ b/saw-remote-api/docs/SAW.rst @@ -433,7 +433,7 @@ Parameter fields -``module name`` +``JSON file`` The file containing the MIR JSON file to load. @@ -445,6 +445,93 @@ No return fields +SAW/MIR/verify (command) +~~~~~~~~~~~~~~~~~~~~~~~~ + +Verify the named MIR method meets its specification. + +Parameter fields +++++++++++++++++ + + +``module`` + The module of the function being verified. + + + +``function`` + The function being verified. + + + +``lemmas`` + The specifications to use for other functions during this verification. + + + +``check sat`` + Whether or not to enable path satisfiability checking. + + + +``contract`` + The specification to verify for the function. + + + +``script`` + The script to use to prove the validity of the resulting verification conditions. + + + +``lemma name`` + The name to refer to this verification/contract by later. + + + +Return fields ++++++++++++++ + +No return fields + + + +SAW/MIR/assume (command) +~~~~~~~~~~~~~~~~~~~~~~~~ + +Assume the named MIR method meets its specification. + +Parameter fields +++++++++++++++++ + + +``module`` + The LLVM module containing the function. + + + +``function`` + The function we are assuming a contract for. + + + +``contract`` + The specification to assume for the function. + + + +``lemma name`` + The name to refer to this assumed contract by later. + + + +Return fields ++++++++++++++ + +No return fields + + + SAW/Yosys/import (command) ~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/saw-remote-api/python/saw_client/__init__.py b/saw-remote-api/python/saw_client/__init__.py index af4b54b61a..0cf9a231de 100644 --- a/saw-remote-api/python/saw_client/__init__.py +++ b/saw-remote-api/python/saw_client/__init__.py @@ -393,7 +393,7 @@ def jvm_load_class(class_name: str) -> JVMClass: __get_designated_connection().jvm_load_class(name, class_name).result() return JVMClass(class_name, name) -# TODO: this is almost identical to llvm_assume. Can we reduce duplication? +# TODO: this is almost identical to llvm_assume and mir_assume. Can we reduce duplication? def jvm_assume(cls: JVMClass, method_name: str, contract: llvm.Contract, @@ -433,7 +433,7 @@ def jvm_assume(cls: JVMClass, return result -# TODO: this is almost identical to llvm_verify. Can we reduce duplication? +# TODO: this is almost identical to llvm_verify and mir_verify. Can we reduce duplication? def jvm_verify(cls: JVMClass, method_name: str, contract: llvm.Contract, @@ -625,6 +625,134 @@ def llvm_verify(module: LLVMModule, return result + +@dataclass +class MIRModule: + json_file: str + server_name: str + + +def mir_load_module(json_file: str) -> MIRModule: + name = __fresh_server_name(json_file) + __get_designated_connection().mir_load_module(name, json_file).result() + return MIRModule(json_file, name) + + +# TODO: this is almost identical to llvm_assume and jvm_assume. Can we reduce duplication? +def mir_assume(module: MIRModule, + function: str, + contract: llvm.Contract, + lemma_name_hint: Optional[str] = None) -> VerificationResult: + """Assume that the given function satisfies the given contract. Returns an + override linking the function and contract that can be passed as an + argument in calls to `mir_verify` + """ + if lemma_name_hint is None: + lemma_name_hint = contract.__class__.__name__ + "_" + function + name = __fresh_server_name(lemma_name_hint) + + result: VerificationResult + try: + conn = __get_designated_connection() + res = conn.mir_assume(module.server_name, + function, + contract.to_json(), + name) + result = AssumptionSucceeded(server_name=name, + contract=contract, + stdout=res.stdout(), + stderr=res.stderr()) + __global_success = True + # If something stopped us from even **assuming**... + except exceptions.VerificationError as err: + __global_success = False + result = AssumptionFailed(server_name=name, + assumptions=[], + contract=contract, + exception=err) + except Exception as err: + __global_success = False + for view in __designated_views: + view.on_python_exception(err) + raise err from None + + return result + + +# TODO: this is almost identical to llvm_verify and jvm_verify. Can we reduce duplication? +def mir_verify(module: MIRModule, + function: str, + contract: llvm.Contract, + lemmas: List[VerificationResult] = [], + check_sat: bool = False, + script: Optional[proofscript.ProofScript] = None, + lemma_name_hint: Optional[str] = None) -> VerificationResult: + """Verify that the given function satisfies the given contract. Returns an + override linking the function and contract that can be passed as an + argument in further calls to `mir_verify` + """ + + if script is None: + script = proofscript.ProofScript([proofscript.z3([])]) + if lemma_name_hint is None: + lemma_name_hint = contract.__class__.__name__ + "_" + function + + name = __fresh_server_name(lemma_name_hint) + + result: VerificationResult + conn = __get_designated_connection() + + global __global_success + global __designated_views + + try: + res = conn.mir_verify(module.server_name, + function, + [l.server_name for l in lemmas], + check_sat, + contract.to_json(), + script.to_json(), + name) + + stdout = res.stdout() + stderr = res.stderr() + result = VerificationSucceeded(server_name=name, + assumptions=lemmas, + contract=contract, + stdout=stdout, + stderr=stderr) + # If the verification did not succeed... + except exceptions.VerificationError as err: + # FIXME add the goal as an assumption if it failed...? + result = VerificationFailed(server_name=name, + assumptions=lemmas, + contract=contract, + exception=err) + # If something else went wrong... + except Exception as err: + __global_success = False + for view in __designated_views: + view.on_python_exception(err) + raise err from None + + # Log or otherwise process the verification result + for view in __designated_views: + if isinstance(result, VerificationSucceeded): + view.on_success(result) + elif isinstance(result, VerificationFailed): + view.on_failure(result) + + # Note when any failure occurs + __global_success = __global_success and result.is_success() + + # Abort the proof if we failed to assume a failed verification, otherwise + # return the result of the verification + if isinstance(result, AssumptionFailed): + raise result.exception from None + + return result + + def prove(goal: cryptoltypes.CryptolJSON, proof_script: proofscript.ProofScript) -> ProofResult: """Atempts to prove that the expression given as the first argument, `goal`, is diff --git a/saw-remote-api/python/saw_client/commands.py b/saw-remote-api/python/saw_client/commands.py index 2d901631e3..2be5907553 100644 --- a/saw-remote-api/python/saw_client/commands.py +++ b/saw-remote-api/python/saw_client/commands.py @@ -251,6 +251,63 @@ def __init__( def process_result(self, res : Any) -> Any: return res +class MIRLoadModule(SAWCommand): + def __init__(self, connection : argo.HasProtocolState, + name : str, + json_file : str, + timeout : Optional[float]) -> None: + super(MIRLoadModule, self).__init__( + 'SAW/MIR/load module', + {'name': name, 'JSON file': json_file}, + connection, + timeout=timeout + ) + + def process_result(self, res : Any) -> Any: + return res + +class MIRAssume(SAWCommand): + def __init__( + self, + connection : argo.HasProtocolState, + module : str, + function : str, + setup : Any, + lemma_name : str, + timeout : Optional[float]) -> None: + params = {'module': module, + 'function': function, + 'contract': setup, + 'lemma name': lemma_name} + super(MIRAssume, self).__init__('SAW/MIR/assume', params, connection, timeout=timeout) + + def process_result(self, _res : Any) -> Any: + return None + +class MIRVerify(SAWCommand): + def __init__( + self, + connection : argo.HasProtocolState, + module : str, + function : str, + lemmas : List[str], + check_sat : bool, + setup : Any, + script : ProofScript, + lemma_name : str, + timeout : Optional[float]) -> None: + params = {'module': module, + 'function': function, + 'lemmas': lemmas, + 'check sat': check_sat, + 'contract': setup, + 'script': script, + 'lemma name': lemma_name} + super(MIRVerify, self).__init__('SAW/MIR/verify', params, connection, timeout=timeout) + + def process_result(self, res : Any) -> Any: + return res + class Prove(SAWCommand): def __init__( self, diff --git a/saw-remote-api/python/saw_client/connection.py b/saw-remote-api/python/saw_client/connection.py index 7d8d33dae1..a8f6ebb0fb 100644 --- a/saw-remote-api/python/saw_client/connection.py +++ b/saw-remote-api/python/saw_client/connection.py @@ -229,6 +229,45 @@ def llvm_assume(self, LLVMAssume(self, module, function, contract, lemma_name, timeout) return self.most_recent_result + def mir_load_module(self, name: str, mir_json_file: str, timeout : Optional[float] = None) -> Command: + """Create an instance of the `MIRLoadClass` command. Documentation on the purpose + and use of this command is associated with the top-level `mir_load_class` + function. + """ + self.most_recent_result = MIRLoadModule(self, name, mir_json_file, timeout) + return self.most_recent_result + + def mir_verify(self, + module: str, + function: str, + lemmas: List[str], + check_sat: bool, + contract: Any, + script: ProofScript, + lemma_name: str, + timeout : Optional[float] = None) -> Command: + """Create an instance of the `MIRVerify` command. Documentation on the purpose + and use of this command is associated with the top-level `mir_verify` + function. + """ + self.most_recent_result = \ + MIRVerify(self, module, function, lemmas, check_sat, contract, script, lemma_name, timeout) + return self.most_recent_result + + def mir_assume(self, + module: str, + function: str, + contract: Any, + lemma_name: str, + timeout : Optional[float] = None) -> Command: + """Create an instance of the `MIRAssume` command. Documentation on the purpose + and use of this command is associated with the top-level `mir_assume` + function. + """ + self.most_recent_result = \ + LLVMAssume(self, module, function, contract, lemma_name, timeout) + return self.most_recent_result + def yosys_import(self, name: str, path: str, timeout : Optional[float] = None) -> Command: self.most_recent_result = YosysImport(self, name, path, timeout) return self.most_recent_result diff --git a/saw-remote-api/python/saw_client/crucible.py b/saw-remote-api/python/saw_client/crucible.py index 5d5ff39a0c..f4c18dfaa5 100644 --- a/saw-remote-api/python/saw_client/crucible.py +++ b/saw-remote-api/python/saw_client/crucible.py @@ -12,6 +12,7 @@ from .llvm_type import * from .jvm_type import * +from .mir_type import * JSON = Union[None, bool, int, float, str, Dict, Tuple, List] @@ -89,7 +90,7 @@ def __to_cryptol_str__(self) -> str: class FreshVar(NamedSetupVal): __name : Optional[str] - def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType'], suggested_name : Optional[str] = None) -> None: + def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType', 'MIRType'], suggested_name : Optional[str] = None) -> None: self.__name = suggested_name self.spec = spec self.type = type @@ -119,7 +120,7 @@ def to_json(self) -> JSON: class Allocated(NamedSetupVal): name : Optional[str] - def __init__(self, spec : 'Contract', type : Union['LLVMType','JVMType'], *, + def __init__(self, spec : 'Contract', type : Union['LLVMType', 'JVMType', 'MIRType'], *, mutable : bool = True, alignment : Optional[int] = None) -> None: self.name = None self.spec = spec @@ -247,7 +248,7 @@ class PointsTo: """The workhorse for ``points_to``. """ def __init__(self, pointer : SetupVal, target : SetupVal, *, - check_target_type : Union[PointerType, 'LLVMType', 'JVMType', None] = PointerType(), + check_target_type : Union[PointerType, 'LLVMType', 'JVMType', 'MIRType', None] = PointerType(), condition : Optional[Condition] = None) -> None: self.pointer = pointer self.target = target @@ -398,7 +399,7 @@ def get_fresh_name(self, hint : str = 'x') -> str: self.__used_names.add(new_name) return new_name - def fresh_var(self, type : Union['LLVMType','JVMType'], suggested_name : Optional[str] = None) -> FreshVar: + def fresh_var(self, type : Union['LLVMType','JVMType', 'MIRType'], suggested_name : Optional[str] = None) -> FreshVar: """Declares a fresh variable of type ``type`` (with name ``suggested_name`` if provided and available).""" fresh_name = self.get_fresh_name('x' if suggested_name is None else self.get_fresh_name(suggested_name)) v = FreshVar(self, type, fresh_name) @@ -410,7 +411,7 @@ def fresh_var(self, type : Union['LLVMType','JVMType'], suggested_name : Optiona raise Exception("wrong state") return v - def alloc(self, type : Union['LLVMType', 'JVMType'], *, read_only : bool = False, + def alloc(self, type : Union['LLVMType', 'JVMType', 'MIRType'], *, read_only : bool = False, alignment : Optional[int] = None, points_to : Optional[SetupVal] = None) -> SetupVal: """Allocates a pointer of type ``type``. @@ -439,7 +440,7 @@ def alloc(self, type : Union['LLVMType', 'JVMType'], *, read_only : bool = False return a def points_to(self, pointer : SetupVal, target : SetupVal, *, - check_target_type : Union[PointerType, 'LLVMType', 'JVMType', None] = PointerType(), + check_target_type : Union[PointerType, 'LLVMType', 'JVMType', 'MIRType', None] = PointerType(), condition : Optional[Condition] = None) -> None: """Declare that the memory location indicated by the ``pointer`` contains the ``target``. @@ -469,7 +470,7 @@ def points_to_bitfield(self, pointer : SetupVal, field_name : str, contains the ``target``. Currently, this function only supports LLVM verification. Attempting to - use this function for JVM verification will result in an error. + use this function for JVM or MIR verification will result in an error. """ pt = PointsToBitfield(pointer, field_name, target) if self.__state == 'pre': @@ -651,7 +652,7 @@ def cry_f(s : str) -> CryptolTerm: ``cry_f('{ {"x": 5, "y": 4} }')`` equals ``cry('{x = 5, y = 4}')`` but ``f'{ {"x": 5, "y": 4} }'`` equals ``'{"x": 5, "y": 4}'``. Only the former is valid Cryptol syntax for a record. - + Note that any conversion or format specifier will always result in the argument being rendered as a Cryptol string literal with the conversion and/or formating applied. For example, `cry('f {5}')` is equal to diff --git a/saw-remote-api/python/saw_client/mir.py b/saw-remote-api/python/saw_client/mir.py new file mode 100644 index 0000000000..f7dc895e58 --- /dev/null +++ b/saw-remote-api/python/saw_client/mir.py @@ -0,0 +1,42 @@ +from cryptol import cryptoltypes +from .utils import deprecated + +from .mir_type import * +from .crucible import * + +################################################## +# Helpers for type construction +################################################## + +bool_ty = MIRBoolType() +char_ty = MIRCharType() +str_ty = MIRStrType() + +i8 = MIRI8Type() +i16 = MIRI16Type() +i32 = MIRI32Type() +i64 = MIRI64Type() +i128 = MIRI128Type() +isize = MIRIsizeType() + +f32 = MIRF32Type() +f64 = MIRF64Type() + +u8 = MIRU8Type() +u16 = MIRU16Type() +u32 = MIRU32Type() +u64 = MIRU64Type() +u128 = MIRU128Type() +usize = MIRUsizeType() + +def array_ty(size : int, ty : 'MIRType') -> 'MIRArrayType': + """``[ty; size]``, i.e. a MIR array of ``size`` elements of type ``ty``.""" + return MIRArrayType(ty, size) + +def slice_ty(ty : MIRType) -> 'MIRSliceType': + """``[ty]``, i.e., a MIR slice to a type ``ty``.""" + return MIRSliceType(ty) + +def tuple_ty(*tuple_types : MIRType) -> 'MIRTupleType': + """A MIR tuple type with fields of type ``tuple_types``.""" + return MIRTupleType(list(tuple_types)) diff --git a/saw-remote-api/python/saw_client/mir_type.py b/saw-remote-api/python/saw_client/mir_type.py new file mode 100644 index 0000000000..60ad41e8a2 --- /dev/null +++ b/saw-remote-api/python/saw_client/mir_type.py @@ -0,0 +1,100 @@ +from abc import ABCMeta, abstractmethod +from typing import Any, Dict, List, Optional, Set, Union, overload + +class MIRType(metaclass=ABCMeta): + @abstractmethod + def to_json(self) -> Any: pass + +class MIRArrayType(MIRType): + def __init__(self, element_type : 'MIRType', size : int) -> None: + self.size = size + self.element_type = element_type + + def to_json(self) -> Any: + return { 'type': 'array', + 'element type': self.element_type.to_json(), + 'size': self.size } + +class MIRBoolType(MIRType): + def to_json(self) -> Any: + return { 'type': 'bool' } + +class MIRCharType(MIRType): + def to_json(self) -> Any: + return { 'type': 'char' } + +class MIRI8Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'i8' } + +class MIRI16Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'i16' } + +class MIRI32Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'i32' } + +class MIRI64Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'i64' } + +class MIRI128Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'i128' } + +class MIRF32Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'f32' } + +class MIRF64Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'f64' } + +class MIRIsizeType(MIRType): + def to_json(self) -> Any: + return { 'type': 'isize' } + +class MIRSliceType(MIRType): + def __init__(self, slice_type : 'MIRType') -> None: + self.slice_type = slice_type + + def to_json(self) -> Any: + return { 'type': 'slice', + 'slice type': self.slice_type.to_json() } + +class MIRStrType(MIRType): + def to_json(self) -> Any: + return { 'type': 'str' } + +class MIRTupleType(MIRType): + def __init__(self, tuple_types : List['MIRType']) -> None: + self.tuple_types = tuple_types + + def to_json(self) -> Any: + return { 'type': 'tuple', + 'tuple types': [ty.to_json() for ty in self.tuple_types] } + +class MIRU8Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'u8' } + +class MIRU16Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'u16' } + +class MIRU32Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'u32' } + +class MIRU64Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'u64' } + +class MIRU128Type(MIRType): + def to_json(self) -> Any: + return { 'type': 'u128' } + +class MIRUsizeType(MIRType): + def to_json(self) -> Any: + return { 'type': 'usize' } diff --git a/saw-remote-api/python/tests/saw/test-files/Makefile b/saw-remote-api/python/tests/saw/test-files/Makefile index f763f03e02..acb9f97702 100644 --- a/saw-remote-api/python/tests/saw/test-files/Makefile +++ b/saw-remote-api/python/tests/saw/test-files/Makefile @@ -1,11 +1,16 @@ -C_FILES := $(wildcard *.c) -BC_FILES := $(C_FILES:.c=.bc) +C_FILES := $(wildcard *.c) +BC_FILES := $(C_FILES:.c=.bc) +RS_FILES := $(wildcard *.rs) +JSON_FILES := $(RS_FILES:.rs=.linked-mir.json) -all: $(BC_FILES) +all: $(BC_FILES) $(JSON_FILES) %.bc: %.c clang -g -c -emit-llvm -o $@ $< +%.linked-mir.json: %.rs + saw-rustc $< + # This test case crucially relies on the use of -O2. llvm_lax_pointer_ordering.bc: llvm_lax_pointer_ordering.c clang -O2 -g -c -emit-llvm -o $@ $< diff --git a/saw-remote-api/python/tests/saw/test-files/basic_mir.linked-mir.json b/saw-remote-api/python/tests/saw/test-files/basic_mir.linked-mir.json new file mode 100644 index 0000000000..e03338d039 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/basic_mir.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"basic_mir.rs:2:5: 2:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"basic_mir.rs:3:2: 3:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}]},"name":"basic_mir/ce9b627a::basic","return_ty":"ty::u32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"basic_mir/ce9b627a::basic","kind":"Item","substs":[]},"name":"basic_mir/ce9b627a::basic"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}}],"roots":["basic_mir/ce9b627a::basic"]} \ No newline at end of file diff --git a/saw-remote-api/python/tests/saw/test-files/basic_mir.rs b/saw-remote-api/python/tests/saw/test-files/basic_mir.rs new file mode 100644 index 0000000000..1957583bee --- /dev/null +++ b/saw-remote-api/python/tests/saw/test-files/basic_mir.rs @@ -0,0 +1,3 @@ +pub fn basic(x: u32) -> u32 { + x +} diff --git a/saw-remote-api/python/tests/saw/test_basic_mir.py b/saw-remote-api/python/tests/saw/test_basic_mir.py new file mode 100644 index 0000000000..338ebdecf0 --- /dev/null +++ b/saw-remote-api/python/tests/saw/test_basic_mir.py @@ -0,0 +1,32 @@ +import unittest +from pathlib import Path + +import saw_client as saw + +from saw_client.crucible import cry, cry_f +from saw_client.mir import Contract, u32 + +class Basic(Contract): + def __init__(self) -> None: + super().__init__() + + def specification(self) -> None: + x = self.fresh_var(u32, "x") + + self.execute_func(x) + + self.returns_f("{x}") + +class BasicTest(unittest.TestCase): + def test_basic(self): + saw.connect(reset_server=True) + if __name__ == "__main__": saw.view(saw.LogResults()) + json_name = str(Path('tests', 'saw', 'test-files', 'basic_mir.linked-mir.json')) + mod = saw.mir_load_module(json_name) + + basic_result = saw.mir_verify(mod, 'basic_mir::basic', Basic()) + self.assertIs(basic_result.is_success(), True) + + +if __name__ == "__main__": + unittest.main() diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index 6c10c6e724..58fee4b9d8 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -74,6 +74,7 @@ library SAWServer.Data.Contract, SAWServer.Data.JVMType, SAWServer.Data.LLVMType, + SAWServer.Data.MIRType, SAWServer.Data.SetupValue, SAWServer.Eval, SAWServer.Exceptions, @@ -83,6 +84,7 @@ library SAWServer.LLVMCrucibleSetup, SAWServer.LLVMVerify, SAWServer.MIRCrucibleSetup, + SAWServer.MIRVerify, SAWServer.NoParams, SAWServer.OK, SAWServer.ProofScript, diff --git a/saw-remote-api/saw-remote-api/Main.hs b/saw-remote-api/saw-remote-api/Main.hs index 68234bcfc4..e71de047b5 100644 --- a/saw-remote-api/saw-remote-api/Main.hs +++ b/saw-remote-api/saw-remote-api/Main.hs @@ -38,6 +38,9 @@ import SAWServer.LLVMVerify llvmVerifyX86 ) import SAWServer.MIRCrucibleSetup ( mirLoadModuleDescr, mirLoadModule ) +import SAWServer.MIRVerify + ( mirAssumeDescr, mirAssume, + mirVerifyDescr, mirVerify ) import SAWServer.ProofScript ( makeSimpsetDescr, makeSimpset, proveDescr, prove ) import SAWServer.SaveTerm ( saveTermDescr, saveTerm ) @@ -121,6 +124,14 @@ sawMethods = "SAW/MIR/load module" mirLoadModuleDescr mirLoadModule + , Argo.command + "SAW/MIR/verify" + mirVerifyDescr + mirVerify + , Argo.command + "SAW/MIR/assume" + mirAssumeDescr + mirAssume -- Yosys , Argo.command "SAW/Yosys/import" diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 5ec7c5882c..7fb8729e84 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -40,6 +40,7 @@ import qualified Data.AIG as AIG import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator, newHandleAllocator) import qualified Lang.Crucible.JVM as CJ import qualified Lang.JVM.Codebase as JSS +import Mir.Intrinsics (MIR) import Mir.Generator (RustModule) --import qualified Verifier.SAW.CryptolEnv as CryptolEnv import Verifier.SAW.Module (emptyModule) @@ -83,7 +84,7 @@ import SAWServer.Exceptions notAJVMMethodSpecIR, notAYosysImport, notAYosysTheorem, notAYosysSequential, - notAMIRModule + notAMIRModule, notAMIRMethodSpecIR ) type SAWCont = (SAWEnv, SAWTask) @@ -94,11 +95,13 @@ data SAWTask = ProofScriptTask | LLVMCrucibleSetup ServerName | JVMSetup ServerName + | MIRSetup ServerName instance Show SAWTask where show ProofScriptTask = "ProofScript" show (LLVMCrucibleSetup n) = "(LLVMCrucibleSetup" ++ show n ++ ")" show (JVMSetup n) = "(JVMSetup" ++ show n ++ ")" + show (MIRSetup n) = "(MIRSetup" ++ show n ++ ")" data CrucibleSetupVal ty e @@ -328,6 +331,7 @@ data ServerVal | VMIRModule RustModule | VJVMMethodSpecIR (CMS.ProvedSpec CJ.JVM) | VLLVMMethodSpecIR (CMS.SomeLLVM CMS.ProvedSpec) + | VMIRMethodSpecIR (CMS.ProvedSpec MIR) | VGhostVar CMS.GhostGlobal | VYosysImport YosysImport | VYosysTheorem YosysTheorem @@ -345,6 +349,7 @@ instance Show ServerVal where show (VMIRModule _) = "VMIRModule" show (VLLVMMethodSpecIR _) = "VLLVMMethodSpecIR" show (VJVMMethodSpecIR _) = "VJVMMethodSpecIR" + show (VMIRMethodSpecIR _) = "VMIRMethodSpecIR" show (VGhostVar x) = "(VGhostVar " ++ show x ++ ")" show (VYosysImport _) = "VYosysImport" show (VYosysTheorem _) = "VYosysTheorem" @@ -371,6 +376,9 @@ instance IsServerVal (CMS.ProvedSpec CJ.JVM) where instance IsServerVal (CMS.SomeLLVM CMS.ProvedSpec) where toServerVal = VLLVMMethodSpecIR +instance IsServerVal (CMS.ProvedSpec MIR) where + toServerVal = VMIRMethodSpecIR + instance IsServerVal JSS.Class where toServerVal = VJVMClass @@ -451,6 +459,13 @@ getLLVMModule n = VLLVMModule m -> return m _other -> Argo.raise (notAnLLVMModule n) +getMIRMethodSpecIR :: ServerName -> Argo.Command SAWState (CMS.ProvedSpec MIR) +getMIRMethodSpecIR n = + do v <- getServerVal n + case v of + VMIRMethodSpecIR ir -> return ir + _other -> Argo.raise (notAMIRMethodSpecIR n) + getMIRModule :: ServerName -> Argo.Command SAWState RustModule getMIRModule n = do v <- getServerVal n diff --git a/saw-remote-api/src/SAWServer/Data/MIRType.hs b/saw-remote-api/src/SAWServer/Data/MIRType.hs new file mode 100644 index 0000000000..c84af365ca --- /dev/null +++ b/saw-remote-api/src/SAWServer/Data/MIRType.hs @@ -0,0 +1,89 @@ +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +module SAWServer.Data.MIRType (JSONMIRType, mirType) where + +import Control.Applicative +import qualified Data.Aeson as JSON +import Data.Aeson (withObject, withText, (.:)) + +import Mir.Mir (BaseSize(..), FloatKind(..), Ty(..)) + +data MIRTypeTag + = TagArray + | TagBool + | TagI8 + | TagI16 + | TagI32 + | TagI64 + | TagI128 + | TagIsize + | TagF32 + | TagF64 + | TagSlice + | TagStr + | TagTuple + | TagU8 + | TagU16 + | TagU32 + | TagU64 + | TagU128 + | TagUsize + +instance JSON.FromJSON MIRTypeTag where + parseJSON = + withText "MIR type tag" $ + \case + "array" -> pure TagArray + "bool" -> pure TagBool + "i8" -> pure TagI8 + "i16" -> pure TagI16 + "i32" -> pure TagI32 + "i64" -> pure TagI64 + "i128" -> pure TagI128 + "isize" -> pure TagIsize + "f32" -> pure TagF32 + "f64" -> pure TagF64 + "slice" -> pure TagSlice + "str" -> pure TagStr + "tuple" -> pure TagTuple + "u8" -> pure TagU8 + "u16" -> pure TagU16 + "u32" -> pure TagU32 + "u64" -> pure TagU64 + "u128" -> pure TagU128 + "usize" -> pure TagUsize + _ -> empty + +newtype JSONMIRType = JSONMIRType { getMIRType :: Ty } + +instance JSON.FromJSON JSONMIRType where + parseJSON = + primType + + where + primType = + withObject "MIR type" $ \o -> fmap JSONMIRType $ + o .: "type" >>= + \case + TagArray -> TyArray <$> (getMIRType <$> o .: "element type") <*> o .: "size" + TagBool -> pure TyBool + TagI8 -> pure $ TyInt B8 + TagI16 -> pure $ TyInt B16 + TagI32 -> pure $ TyInt B32 + TagI64 -> pure $ TyInt B64 + TagI128 -> pure $ TyInt B128 + TagIsize -> pure $ TyInt USize + TagF32 -> pure $ TyFloat F32 + TagF64 -> pure $ TyFloat F64 + TagSlice -> TySlice <$> (getMIRType <$> o .: "slice type") + TagStr -> pure TyStr + TagTuple -> TyTuple <$> (fmap getMIRType <$> o .: "tuple types") + TagU8 -> pure $ TyUint B8 + TagU16 -> pure $ TyUint B16 + TagU32 -> pure $ TyUint B32 + TagU64 -> pure $ TyUint B64 + TagU128 -> pure $ TyUint B128 + TagUsize -> pure $ TyUint USize + +mirType :: JSONMIRType -> Ty +mirType = getMIRType diff --git a/saw-remote-api/src/SAWServer/Exceptions.hs b/saw-remote-api/src/SAWServer/Exceptions.hs index f1584c0139..a34fd22f1c 100644 --- a/saw-remote-api/src/SAWServer/Exceptions.hs +++ b/saw-remote-api/src/SAWServer/Exceptions.hs @@ -15,6 +15,7 @@ module SAWServer.Exceptions ( , notAYosysImport , notAYosysSequential , notAMIRModule + , notAMIRMethodSpecIR -- * Wrong monad errors , notSettingUpCryptol , notSettingUpLLVMCrucible @@ -204,6 +205,17 @@ notAMIRModule name = " is not a MIR module") (Just $ object ["name" .= name]) +notAMIRMethodSpecIR :: + (ToJSON name, Show name) => + name {- ^ the name that should have been mapped to a method specification IR -}-> + JSONRPCException +notAMIRMethodSpecIR name = + makeJSONRPCException 10150 + ("The server value with name " <> + T.pack (show name) <> + " is not a MIR method specification") + (Just $ object ["name" .= name]) + cantLoadLLVMModule :: String -> JSONRPCException cantLoadLLVMModule err = makeJSONRPCException diff --git a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs index a96da3bb4e..e0f16f83f9 100644 --- a/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs +++ b/saw-remote-api/src/SAWServer/MIRCrucibleSetup.hs @@ -1,41 +1,185 @@ +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} -- | Support for interfacing with MIR-related commands in SAW. module SAWServer.MIRCrucibleSetup ( mirLoadModule , mirLoadModuleDescr + , compileMIRContract ) where +import Control.Exception (throw) import Control.Lens ( view ) +import Control.Monad.IO.Class ( MonadIO(liftIO) ) import Data.Aeson ( FromJSON(..), withObject, (.:) ) +import Data.ByteString (ByteString) +import Data.Map (Map) +import qualified Data.Map as Map -import SAWScript.Crucible.MIR.Builtins ( mir_load_module ) +import Mir.Intrinsics (MIR) + +import qualified Cryptol.Parser.AST as P +import Cryptol.Utils.Ident (mkIdent) +import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..)) +import SAWScript.Crucible.MIR.Builtins + ( mir_alloc, + mir_alloc_mut, + mir_fresh_var, + mir_execute_func, + mir_load_module, + mir_postcond, + mir_precond, + mir_return ) +import SAWScript.Value (BuiltinContext, MIRSetupM(..), biSharedContext) +import qualified Verifier.SAW.CryptolEnv as CEnv +import Verifier.SAW.CryptolEnv (CryptolEnv) +import Verifier.SAW.TypedTerm (TypedTerm) import qualified Argo import qualified Argo.Doc as Doc -import SAWServer as Server +import SAWServer ( ServerName(..), SAWState, + CrucibleSetupVal(..), sawTask, setServerVal ) +import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp) +import SAWServer.Data.Contract + ( PointsTo, + PointsToBitfield, + Allocated(Allocated), + ContractVar(ContractVar), + Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields, + argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields, + returnVal) ) +import SAWServer.Data.MIRType (JSONMIRType, mirType) import SAWServer.Exceptions ( notAtTopLevel ) import SAWServer.OK ( OK, ok ) import SAWServer.TopLevel ( tl ) import SAWServer.TrackFile ( trackFile ) +newtype ServerSetupVal = Val (SetupValue MIR) + +compileMIRContract :: + (FilePath -> IO ByteString) -> + BuiltinContext -> + CryptolEnv -> + Contract JSONMIRType (P.Expr P.PName) -> + MIRSetupM () +compileMIRContract fileReader bic cenv0 c = + do allocsPre <- mapM setupAlloc (preAllocated c) + (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c) + mapM_ (\p -> getTypedTerm cenvPre p >>= mir_precond) (preConds c) + mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c) + mapM_ setupPointsToBitfields (prePointsToBitfields c) + --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c) + traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= mir_execute_func + allocsPost <- mapM setupAlloc (postAllocated c) + (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c) + mapM_ (\p -> getTypedTerm cenvPost p >>= mir_postcond) (postConds c) + mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c) + mapM_ setupPointsToBitfields (postPointsToBitfields c) + --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c) + case returnVal c of + Just v -> getSetupVal (envPost, cenvPost) v >>= mir_return + Nothing -> return () + where + setupFresh :: ContractVar JSONMIRType -> MIRSetupM (ServerName, TypedTerm) + setupFresh (ContractVar n dn ty) = + do t <- mir_fresh_var dn (mirType ty) + return (n, t) + setupState allocs (env, cenv) vars = + do freshTerms <- mapM setupFresh vars + let cenv' = foldr (\(ServerName n, t) -> CEnv.bindTypedTerm (mkIdent n, t)) cenv freshTerms + let env' = Map.union env $ Map.fromList $ + [ (n, Val (MS.SetupTerm t)) | (n, t) <- freshTerms ] ++ + [ (n, Val v) | (n, v) <- allocs ] + return (env', cenv') + + setupAlloc :: Allocated JSONMIRType -> MIRSetupM (ServerName, MS.SetupValue MIR) + setupAlloc (Allocated _ _ _ (Just _)) = + MIRSetupM $ fail "Alignment not supported in the MIR API." + setupAlloc (Allocated n ty mut Nothing) + | mut = (n,) <$> mir_alloc_mut ty' + | otherwise = (n,) <$> mir_alloc ty' + where + ty' = mirType ty + + setupPointsTo :: + (Map ServerName ServerSetupVal, CryptolEnv) -> + PointsTo JSONMIRType (P.Expr P.PName) -> + MIRSetupM () + setupPointsTo _env _pt = + MIRSetupM $ fail "Points-to not currently implemented in the MIR API." + + setupPointsToBitfields :: PointsToBitfield JSONMIRType (P.Expr P.PName) -> MIRSetupM () + setupPointsToBitfields _ = + MIRSetupM $ fail "Points-to-bitfield not supported in the MIR API." + + --setupGhostValue _ _ _ = fail "Ghost values not supported yet in the MIR API." + + resolve :: Map ServerName a -> ServerName -> MIRSetupM a + resolve env name = + MIRSetupM $ + case Map.lookup name env of + Just v -> return v + Nothing -> fail $ unlines + [ "Server value " ++ show name ++ " not found - impossible!" -- rule out elsewhere + , show (Map.keys env) + ] + + getTypedTerm :: + CryptolEnv -> + P.Expr P.PName -> + MIRSetupM TypedTerm + getTypedTerm cenv expr = MIRSetupM $ + do (res, warnings) <- liftIO $ getTypedTermOfCExp fileReader (biSharedContext bic) cenv expr + case res of + Right (t, _) -> return t + Left err -> throw $ CryptolModuleException err warnings + + getSetupVal :: + (Map ServerName ServerSetupVal, CryptolEnv) -> + CrucibleSetupVal JSONMIRType (P.Expr P.PName) -> + MIRSetupM (MS.SetupValue MIR) + getSetupVal (env, _) (NamedValue n) = + resolve env n >>= \case Val x -> return x + getSetupVal (_, cenv) (CryptolExpr expr) = + MS.SetupTerm <$> getTypedTerm cenv expr + getSetupVal _ NullValue = + MIRSetupM $ fail "Null setup values unsupported in the MIR API." + getSetupVal env (ArrayValue elts) = + do elts' <- mapM (getSetupVal env) elts + MIRSetupM $ return $ MS.SetupArray () elts' + getSetupVal _ (TupleValue _) = + MIRSetupM $ fail "Tuple setup values unsupported in the MIR API." + getSetupVal _ (FieldLValue _ _) = + MIRSetupM $ fail "Field l-values unsupported in the MIR API." + getSetupVal _ (CastLValue _ _) = + MIRSetupM $ fail "Cast l-values unsupported in the MIR API." + getSetupVal _ (UnionLValue _ _) = + MIRSetupM $ fail "Union l-values unsupported in the MIR API." + getSetupVal _ (ElementLValue _ _) = + MIRSetupM $ fail "Element l-values unsupported in the MIR API." + getSetupVal _ (GlobalInitializer _) = + MIRSetupM $ fail "Global initializers unsupported in the MIR API." + getSetupVal _ (GlobalLValue _) = + MIRSetupM $ fail "Global l-values unsupported in the MIR API." + data MIRLoadModuleParams = MIRLoadModuleParams ServerName FilePath instance FromJSON MIRLoadModuleParams where parseJSON = withObject "params for \"SAW/MIR/load module\"" $ \o -> - MIRLoadModuleParams <$> o .: "name" <*> o .: "module name" + MIRLoadModuleParams <$> o .: "name" <*> o .: "JSON file" instance Doc.DescribedMethod MIRLoadModuleParams OK where parameterFieldDescription = [ ("name", Doc.Paragraph [Doc.Text "The name to refer to the loaded module by later."]) - , ("module name", + , ("JSON file", Doc.Paragraph [Doc.Text "The file containing the MIR JSON file to load."]) ] resultFieldDescription = [] diff --git a/saw-remote-api/src/SAWServer/MIRVerify.hs b/saw-remote-api/src/SAWServer/MIRVerify.hs new file mode 100644 index 0000000000..9f72addfcf --- /dev/null +++ b/saw-remote-api/src/SAWServer/MIRVerify.hs @@ -0,0 +1,80 @@ +{-# LANGUAGE OverloadedStrings #-} +-- | Support for the MIR @verify@ and @assume@ commands. +module SAWServer.MIRVerify + ( mirVerify + , mirVerifyDescr + , mirAssume + , mirAssumeDescr + ) where + +import Prelude hiding (mod) +import Control.Lens + +import SAWScript.Crucible.MIR.Builtins + ( mir_verify ) +import SAWScript.Value (rwCryptol) + +import qualified Argo +import qualified Argo.Doc as Doc +import SAWServer + ( SAWState, + SAWTask(MIRSetup), + sawBIC, + sawTask, + sawTopLevelRW, + pushTask, + dropTask, + setServerVal, + getMIRModule, + getMIRMethodSpecIR ) +import SAWServer.CryptolExpression (getCryptolExpr) +import SAWServer.Data.Contract ( ContractMode(..) ) +import SAWServer.Data.MIRType ( JSONMIRType ) +import SAWServer.Exceptions ( notAtTopLevel ) +import SAWServer.MIRCrucibleSetup ( compileMIRContract ) +import SAWServer.OK ( OK, ok ) +import SAWServer.ProofScript + ( ProofScript(ProofScript), interpretProofScript ) +import SAWServer.TopLevel ( tl ) +import SAWServer.VerifyCommon + ( AssumeParams(AssumeParams), VerifyParams(VerifyParams) ) + +mirVerifyAssume :: ContractMode -> VerifyParams JSONMIRType -> Argo.Command SAWState OK +mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract script lemmaName) = + do tasks <- view sawTask <$> Argo.getState + case tasks of + (_:_) -> Argo.raise $ notAtTopLevel $ map fst tasks + [] -> + do pushTask (MIRSetup lemmaName) + state <- Argo.getState + rm <- getMIRModule modName + let bic = view sawBIC state + cenv = rwCryptol (view sawTopLevelRW state) + fileReader <- Argo.getFileReader + setup <- compileMIRContract fileReader bic cenv <$> + traverse getCryptolExpr contract + res <- case mode of + VerifyContract -> do + lemmas <- mapM getMIRMethodSpecIR lemmaNames + proofScript <- interpretProofScript script + tl $ mir_verify rm fun lemmas checkSat setup proofScript + AssumeContract -> + tl $ error "mir_unsafe_assume_spec not yet supported" + dropTask + setServerVal lemmaName res + ok + +mirVerify :: VerifyParams JSONMIRType -> Argo.Command SAWState OK +mirVerify = mirVerifyAssume VerifyContract + +mirVerifyDescr :: Doc.Block +mirVerifyDescr = + Doc.Paragraph [Doc.Text "Verify the named MIR method meets its specification."] + +mirAssume :: AssumeParams JSONMIRType -> Argo.Command SAWState OK +mirAssume (AssumeParams modName fun contract lemmaName) = + mirVerifyAssume AssumeContract (VerifyParams modName fun [] False contract (ProofScript []) lemmaName) + +mirAssumeDescr :: Doc.Block +mirAssumeDescr = + Doc.Paragraph [Doc.Text "Assume the named MIR method meets its specification."] diff --git a/saw-script.cabal b/saw-script.cabal index 56617e75f7..fdbaf42c9d 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -143,6 +143,7 @@ library SAWScript.Crucible.Common SAWScript.Crucible.Common.MethodSpec SAWScript.Crucible.Common.Override + SAWScript.Crucible.Common.ResolveSetupValue SAWScript.Crucible.Common.Setup.Builtins SAWScript.Crucible.Common.Setup.Type @@ -163,6 +164,10 @@ library SAWScript.Crucible.JVM.ResolveSetupValue SAWScript.Crucible.MIR.Builtins + SAWScript.Crucible.MIR.MethodSpecIR + SAWScript.Crucible.MIR.Override + SAWScript.Crucible.MIR.ResolveSetupValue + SAWScript.Crucible.MIR.TypeShape SAWScript.Prover.Mode SAWScript.Prover.Rewrite diff --git a/src/SAWScript/AST.hs b/src/SAWScript/AST.hs index 4f47dbb7bb..6ad51b80d2 100644 --- a/src/SAWScript/AST.hs +++ b/src/SAWScript/AST.hs @@ -32,7 +32,7 @@ module SAWScript.AST , toLName , tMono, tForall, tTuple, tRecord, tArray, tFun , tString, tTerm, tType, tBool, tInt, tAIG, tCFG - , tJVMSpec, tLLVMSpec + , tJVMSpec, tLLVMSpec, tMIRSpec , tBlock, tContext, tVar , PrettyPrint(..), pShow, commaSepAll, prettyWholeModule @@ -178,6 +178,7 @@ data Context = CryptolSetup | JavaSetup | LLVMSetup + | MIRSetup | ProofScript | TopLevel | CrucibleSetup @@ -212,6 +213,7 @@ data TyCon | CFGCon | JVMSpecCon | LLVMSpecCon + | MIRSpecCon | ContextCon Context deriving (Eq, Show) @@ -394,6 +396,7 @@ instance PrettyPrint TyCon where CFGCon -> "CFG" JVMSpecCon -> "JVMSpec" LLVMSpecCon -> "LLVMSpec" + MIRSpecCon -> "MIRSpec" BlockCon -> "" ContextCon cxt -> pretty par cxt @@ -402,6 +405,7 @@ instance PrettyPrint Context where CryptolSetup -> "CryptolSetup" JavaSetup -> "JavaSetup" LLVMSetup -> "LLVMSetup" + MIRSetup -> "MIRSetup" ProofScript -> "ProofScript" TopLevel -> "TopLevel" CrucibleSetup-> "CrucibleSetup" @@ -471,6 +475,9 @@ tJVMSpec = TyCon JVMSpecCon [] tLLVMSpec :: Type tLLVMSpec = TyCon LLVMSpecCon [] +tMIRSpec :: Type +tMIRSpec = TyCon MIRSpecCon [] + tBlock :: Type -> Type -> Type tBlock c t = TyCon BlockCon [c,t] diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs index f80c3c24e0..551b7376f3 100644 --- a/src/SAWScript/Crucible/Common/MethodSpec.hs +++ b/src/SAWScript/Crucible/Common/MethodSpec.hs @@ -67,6 +67,10 @@ data PrePost = PreState | PostState deriving (Eq, Ord, Show) +stateCond :: PrePost -> String +stateCond PreState = "precondition" +stateCond PostState = "postcondition" + -------------------------------------------------------------------------------- -- *** Extension-specific information diff --git a/src/SAWScript/Crucible/Common/Override.hs b/src/SAWScript/Crucible/Common/Override.hs index de65b19d79..c02ad8baca 100644 --- a/src/SAWScript/Crucible/Common/Override.hs +++ b/src/SAWScript/Crucible/Common/Override.hs @@ -51,6 +51,7 @@ module SAWScript.Crucible.Common.Override , writeGlobal , failure , getSymInterface + , enforceCompleteSubstitution -- , assignmentToList , MetadataMap @@ -58,6 +59,7 @@ module SAWScript.Crucible.Common.Override import qualified Control.Exception as X import Control.Lens +import Control.Monad (unless) import Control.Monad.Trans.State hiding (get, put) import Control.Monad.State.Class (MonadState(..)) import Control.Monad.Error.Class (MonadError) @@ -67,6 +69,7 @@ import Control.Monad.Trans.Except import Control.Monad.Trans.Class import Control.Monad.IO.Class import Data.Kind (Type) +import qualified Data.Map as Map import Data.Map (Map) import Data.Set (Set) import Data.Typeable (Typeable) @@ -273,7 +276,7 @@ instance ( PP.Pretty (ExtType ext) instance ( PP.Pretty (ExtType ext) , PP.Pretty (MS.PointsTo ext) - , Typeable ext + , Typeable ext ) => X.Exception (OverrideFailure ext) -------------------------------------------------------------------------------- @@ -376,6 +379,26 @@ failure loc e = OM (lift (throwE (OF loc e))) getSymInterface :: Monad m => OverrideMatcher' sym ext md m sym getSymInterface = OM (use syminterface) +-- | Verify that all of the fresh variables for the given +-- state spec have been "learned". If not, throws +-- 'AmbiguousVars' exception. +enforceCompleteSubstitution :: + W4.ProgramLoc -> + MS.StateSpec ext -> + OverrideMatcher ext w () +enforceCompleteSubstitution loc ss = + + do sub <- OM (use termSub) + + let -- predicate matches terms that are not covered by the computed + -- term substitution + isMissing tt = ecVarIndex (tecExt tt) `Map.notMember` sub + + -- list of all terms not covered by substitution + missing = filter isMissing (view MS.csFreshVars ss) + + unless (null missing) (failure loc (AmbiguousVars missing)) + ------------------------------------------------------------------------ -- | Forget the type indexes and length of the arguments. diff --git a/src/SAWScript/Crucible/Common/ResolveSetupValue.hs b/src/SAWScript/Crucible/Common/ResolveSetupValue.hs new file mode 100644 index 0000000000..253aa430af --- /dev/null +++ b/src/SAWScript/Crucible/Common/ResolveSetupValue.hs @@ -0,0 +1,32 @@ +-- | Utilities for resolving 'SetupValue's that are used across language +-- backends. +module SAWScript.Crucible.Common.ResolveSetupValue + ( resolveBoolTerm + ) where + +import qualified What4.BaseTypes as W4 +import qualified What4.Interface as W4 + +import Verifier.SAW.SharedTerm + +import qualified Verifier.SAW.Simulator.Concrete as Concrete + +import Verifier.SAW.Simulator.What4.ReturnTrip + +import SAWScript.Crucible.Common + +-- | Resolve a SAWCore 'Term' into a What4 'W4.Pred'. +resolveBoolTerm :: Sym -> Term -> IO (W4.Pred Sym) +resolveBoolTerm sym tm = + do st <- sawCoreState sym + let sc = saw_ctx st + mx <- case getAllExts tm of + -- concretely evaluate if it is a closed term + [] -> + do modmap <- scGetModuleMap sc + let v = Concrete.evalSharedTerm modmap mempty mempty tm + pure (Just (Concrete.toBool v)) + _ -> return Nothing + case mx of + Just x -> return (W4.backendPred sym x) + Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index e38b41555d..a3920359f6 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -620,6 +620,8 @@ registerOverride opts cc _ctx top_loc mdMap cs = -------------------------------------------------------------------------------- +-- | Simulate a JVM function with Crucible as part of a 'jvm_verify' command, +-- making sure to install any overrides that the user supplies. verifySimulate :: Options -> JVMCrucibleContext -> diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index 4fe4f7bce6..c9e53b4b30 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -354,24 +354,6 @@ learnCond opts sc cc cs prepost ss = enforceCompleteSubstitution loc ss --- | Verify that all of the fresh variables for the given --- state spec have been "learned". If not, throws --- 'AmbiguousVars' exception. -enforceCompleteSubstitution :: W4.ProgramLoc -> StateSpec -> OverrideMatcher CJ.JVM w () -enforceCompleteSubstitution loc ss = - - do sub <- OM (use termSub) - - let -- predicate matches terms that are not covered by the computed - -- term substitution - isMissing tt = ecVarIndex (tecExt tt) `Map.notMember` sub - - -- list of all terms not covered by substitution - missing = filter isMissing (view MS.csFreshVars ss) - - unless (null missing) (failure loc (AmbiguousVars missing)) - - -- execute a pre/post condition executeCond :: Options -> @@ -590,7 +572,7 @@ matchArg opts sc cc cs prepost md actual@(RVal ref) expectedTy setupval = MS.SetupNull () -> do sym <- Ov.getSymInterface p <- liftIO (CJ.refIsNull sym ref) - addAssert p md (Crucible.SimError (cs ^. MS.csLoc) (Crucible.AssertFailureSimError ("null-equality " ++ stateCond prepost) "")) + addAssert p md (Crucible.SimError (cs ^. MS.csLoc) (Crucible.AssertFailureSimError ("null-equality " ++ MS.stateCond prepost) "")) MS.SetupGlobal empty _ -> absurd empty @@ -659,7 +641,7 @@ matchTerm sc cc md prepost real expect = _ -> do t <- liftIO $ scEq sc real expect p <- liftIO $ resolveBoolTerm (cc ^. jccSym) t - addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError ("literal equality " ++ stateCond prepost) "")) + addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost) "")) ------------------------------------------------------------------------ @@ -756,10 +738,6 @@ learnPointsTo opts sc cc spec prepost pt = ------------------------------------------------------------------------ -stateCond :: PrePost -> String -stateCond PreState = "precondition" -stateCond PostState = "postcondition" - -- | Process a "crucible_equal" statement from the precondition -- section of the CrucibleSetup block. learnEqual :: @@ -776,7 +754,7 @@ learnEqual opts sc cc spec md prepost v1 v2 = do val1 <- resolveSetupValueJVM opts cc sc spec v1 val2 <- resolveSetupValueJVM opts cc sc spec v2 p <- liftIO (equalValsPred cc val1 val2) - let name = "equality " ++ stateCond prepost + let name = "equality " ++ MS.stateCond prepost let loc = MS.conditionLoc md addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError name "")) @@ -794,7 +772,7 @@ learnPred sc cc md prepost t = u <- liftIO $ scInstantiateExt sc s t p <- liftIO $ resolveBoolTerm (cc ^. jccSym) u let loc = MS.conditionLoc md - addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (stateCond prepost) "")) + addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) "")) ------------------------------------------------------------------------ diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 253269eda4..c0db25d7c6 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -69,6 +69,7 @@ import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..)) import SAWScript.Panic import SAWScript.Crucible.JVM.MethodSpecIR import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.ResolveSetupValue (resolveBoolTerm) data JVMVal @@ -273,21 +274,6 @@ resolveBitvectorTerm sym w tm = Just x -> W4.bvLit sym w (BV.mkBV w x) Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm -resolveBoolTerm :: Sym -> Term -> IO (W4.Pred Sym) -resolveBoolTerm sym tm = - do st <- sawCoreState sym - let sc = saw_ctx st - mx <- case getAllExts tm of - -- concretely evaluate if it is a closed term - [] -> - do modmap <- scGetModuleMap sc - let v = Concrete.evalSharedTerm modmap mempty mempty tm - pure (Just (Concrete.toBool v)) - _ -> return Nothing - case mx of - Just x -> return (W4.backendPred sym x) - Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm - toJVMType :: Cryptol.TValue -> Maybe J.Type toJVMType tp = case tp of diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 3ddc66f29b..65413e40a2 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1407,6 +1407,8 @@ withBreakpointCfgAndBlockId opts context name parent k = Just (Some breakpoint_block_id) -> k cfg breakpoint_block_id Nothing -> fail $ "Unexpected breakpoint name: " ++ name +-- | Simulate an LLVM function with Crucible as part of a 'llvm_verify' command, +-- making sure to install any overrides that the user supplies. verifySimulate :: ( ?lc :: Crucible.TypeContext , ?memOpts::Crucible.MemOptions diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index d193f73864..f132747f2c 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -247,7 +247,7 @@ notEqual cond opts loc cc sc spec expected actual = do prettyLLVMVal <- ppLLVMVal cc actual prettySetupLLVMVal <- ppSetupValueAsLLVMVal opts cc sc spec expected let msg = unlines - [ "Equality " ++ stateCond cond + [ "Equality " ++ MS.stateCond cond , "Expected value (as a SAW value): " , show (MS.ppSetupValue expected) , "Expected value (as a Crucible value): " @@ -810,27 +810,6 @@ assertTermEqualities sc cc = do traverse_ assertTermEquality =<< OM (use termEqs) --- | Verify that all of the fresh variables for the given --- state spec have been "learned". If not, throws --- 'AmbiguousVars' exception. -enforceCompleteSubstitution :: - W4.ProgramLoc -> - MS.StateSpec (LLVM arch) -> - OverrideMatcher (LLVM arch) md () -enforceCompleteSubstitution loc ss = - - do sub <- OM (use termSub) - - let -- predicate matches terms that are not covered by the computed - -- term substitution - isMissing tt = ecVarIndex (tecExt tt) `Map.notMember` sub - - -- list of all terms not covered by substitution - missing = filter isMissing (view MS.csFreshVars ss) - - unless (null missing) (failure loc (AmbiguousVars missing)) - - -- execute a pre/post condition executeCond :: ( ?lc :: Crucible.TypeContext , ?memOpts :: Crucible.MemOptions @@ -1219,7 +1198,7 @@ assignTerm sc cc md prepost var val = -- do t <- liftIO $ scEq sc old val -- p <- liftIO $ resolveSAWPred cc t --- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ stateCond prepost)) +-- addAssert p (Crucible.AssertFailureSimError ("literal equality " ++ MS.stateCond prepost)) ------------------------------------------------------------------------ @@ -1504,7 +1483,7 @@ matchTerm sc cc md prepost real expect = _ -> do t <- liftIO $ scEq sc real expect let msg = unlines $ - [ "Literal equality " ++ stateCond prepost + [ "Literal equality " ++ MS.stateCond prepost -- , "Expected term: " ++ prettyTerm expect -- , "Actual term: " ++ prettyTerm real ] @@ -1642,7 +1621,7 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val = Crucible.asMemAllocationArrayStore sym Crucible.PtrWidth ptr (Crucible.memImplHeap mem) let errMsg = PP.vcat $ map (PP.pretty . unwords) [ [ "When reading through pointer:", show (Crucible.ppPtr ptr) ] - , [ "in the ", stateCond prepost, "of an override" ] + , [ "in the ", MS.stateCond prepost, "of an override" ] , [ "Tried to read an array prefix of size:", show (MS.ppTypedTerm expected_sz_tm) ] ] case maybe_allocation_array of @@ -1816,7 +1795,7 @@ summarizeBadLoad cc memTy prepost ptr = sz = Crucible.memTypeSize dataLayout memTy in map (PP.pretty . unwords) [ [ "When reading through pointer:", show (Crucible.ppPtr ptr) ] - , [ "in the ", stateCond prepost, "of an override" ] + , [ "in the ", MS.stateCond prepost, "of an override" ] , [ "Tried to read something of size:" , show (Crucible.bytesToInteger sz) ] @@ -1856,10 +1835,6 @@ describeConcreteMemoryLoadFailure mem badLoadSummary ptr = do ------------------------------------------------------------------------ -stateCond :: PrePost -> String -stateCond PreState = "precondition" -stateCond PostState = "postcondition" - -- | Process an @llvm_equal@ statement from the precondition -- section of the CrucibleSetup block. learnEqual :: @@ -1877,7 +1852,7 @@ learnEqual opts sc cc spec md prepost v1 v2 = do (_, val1) <- resolveSetupValueLLVM opts cc sc spec v1 (_, val2) <- resolveSetupValueLLVM opts cc sc spec v2 p <- liftIO (equalValsPred cc val1 val2) - let name = "equality " ++ stateCond prepost + let name = "equality " ++ MS.stateCond prepost let loc = MS.conditionLoc md addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError name "")) @@ -1894,7 +1869,7 @@ learnPred :: learnPred sc cc md prepost t = do p <- instantiateExtResolveSAWPred sc cc t let loc = MS.conditionLoc md - addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (stateCond prepost) "")) + addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) "")) instantiateExtResolveSAWPred :: (?w4EvalTactic :: W4EvalTactic) => diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 293e88f965..b86d209739 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -1,20 +1,204 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} {-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} -- | Implementations of Crucible-related SAWScript primitives for MIR. module SAWScript.Crucible.MIR.Builtins - ( mir_load_module + ( -- * Commands + -- ** Setup + mir_alloc + , mir_alloc_mut + , mir_assert + , mir_execute_func + , mir_fresh_var + , mir_load_module + , mir_postcond + , mir_precond + , mir_return + , mir_verify + -- ** MIR types + , mir_array + , mir_bool + , mir_char + , mir_i8 + , mir_i16 + , mir_i32 + , mir_i64 + , mir_i128 + , mir_isize + , mir_f32 + , mir_f64 + , mir_ref + , mir_ref_mut + , mir_slice + , mir_str + , mir_tuple + , mir_u8 + , mir_u16 + , mir_u32 + , mir_u64 + , mir_u128 + , mir_usize ) where +import Control.Lens +import Control.Monad (foldM, forM, forM_, unless, when) +import qualified Control.Monad.Catch as X +import Control.Monad.IO.Class (MonadIO(..)) +import Control.Monad.Reader (runReaderT) +import Control.Monad.State (MonadState(..), StateT(..), execStateT, gets) +import Control.Monad.Trans.Class (MonadTrans(..)) import qualified Data.ByteString.Lazy as BSL +import qualified Data.Foldable as F +import Data.Foldable (for_) +import Data.IORef +import qualified Data.List.Extra as List (groupOn) +import Data.List.NonEmpty (NonEmpty(..)) +import qualified Data.Map as Map +import Data.Map (Map) +import Data.Maybe (fromMaybe) +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.NatRepr (knownNat, natValue) +import Data.Parameterized.Some (Some(..)) +import qualified Data.Set as Set +import qualified Data.Text as Text +import Data.Text (Text) +import Data.Time.Clock (diffUTCTime, getCurrentTime) +import Data.Type.Equality (TestEquality(..)) +import Data.Void (absurd) +import Numeric.Natural (Natural) +import qualified Prettyprinter as PP +import System.IO (stdout) -import Mir.Generator -import Mir.ParseTranslate +import qualified Cryptol.TypeCheck.Type as Cryptol +import qualified Lang.Crucible.Analysis.Postdom as Crucible +import qualified Lang.Crucible.Backend as Crucible +import qualified Lang.Crucible.CFG.Core as Crucible +import qualified Lang.Crucible.FunctionHandle as Crucible +import qualified Lang.Crucible.Simulator as Crucible +import qualified Lang.Crucible.Simulator.SimError as Crucible + +import qualified Mir.DefId as Mir +import qualified Mir.Mir as Mir +import qualified Mir.Generator as Mir +import Mir.Intrinsics (MIR) +import qualified Mir.Intrinsics as Mir +import qualified Mir.ParseTranslate as Mir +import qualified Mir.Trans as Mir +import Mir.TransCustom (customOps) +import qualified Mir.TransTy as Mir + +import qualified What4.Config as W4 +import qualified What4.Interface as W4 +import qualified What4.ProgramLoc as W4 + +import Verifier.SAW.FiniteValue (ppFirstOrderValue) +import Verifier.SAW.Name (toShortName) +import Verifier.SAW.SharedTerm +import Verifier.SAW.Simulator.What4.ReturnTrip +import Verifier.SAW.TypedTerm + +import SAWScript.Crucible.Common +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.Override +import qualified SAWScript.Crucible.Common.Setup.Builtins as Setup +import qualified SAWScript.Crucible.Common.Setup.Type as Setup +import SAWScript.Crucible.MIR.MethodSpecIR +import SAWScript.Crucible.MIR.Override +import SAWScript.Crucible.MIR.ResolveSetupValue +import SAWScript.Crucible.MIR.TypeShape +import SAWScript.Exceptions import SAWScript.Options +import SAWScript.Panic +import qualified SAWScript.Position as SS +import SAWScript.Proof +import SAWScript.Prover.SolverStats import SAWScript.Value +type AssumptionReason = (MS.ConditionMetadata, String) +type SetupValue = MS.SetupValue MIR +type Lemma = MS.ProvedSpec MIR +type MethodSpec = MS.CrucibleMethodSpecIR MIR +type SetupCondition = MS.SetupCondition MIR + +-- TODO: something useful with the global pair? +ppMIRAbortedResult :: MIRCrucibleContext + -> Crucible.AbortedResult Sym a + -> PP.Doc ann +ppMIRAbortedResult _cc = ppAbortedResult (\_gp -> mempty) + +----- +-- Commands +----- + +mir_alloc :: Mir.Ty -> MIRSetupM SetupValue +mir_alloc = mir_alloc_internal Mir.Immut + +mir_alloc_mut :: Mir.Ty -> MIRSetupM SetupValue +mir_alloc_mut = mir_alloc_internal Mir.Mut + +-- | The workhorse for 'mir_alloc' and 'mir_alloc_mut'. +mir_alloc_internal :: Mir.Mutability -> Mir.Ty -> MIRSetupM SetupValue +mir_alloc_internal mut mty = + MIRSetupM $ + do st <- get + let mcc = st ^. Setup.csCrucibleContext + let col = mcc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection + Some tpr <- pure $ Mir.tyToRepr col mty + n <- Setup.csVarCounter <<%= MS.nextAllocIndex + Setup.currentState . MS.csAllocs . at n ?= + Some (MirAllocSpec { _maType = tpr + , _maMutbl = mut + , _maMirType = mty + , _maLen = 1 + }) + return (MS.SetupVar n) + +mir_execute_func :: [SetupValue] -> MIRSetupM () +mir_execute_func args = + MIRSetupM $ + do st <- get + let cc = st ^. Setup.csCrucibleContext + let mspec = st ^. Setup.csMethodSpec + let env = MS.csAllocations mspec + let nameEnv = MS.csTypeNames mspec + let argTys = mspec ^. MS.csArgs + let + checkArg i expectedTy val = + do valTy <- typeOfSetupValue cc env nameEnv val + unless (checkCompatibleTys expectedTy valTy) $ + X.throwM (MIRArgTypeMismatch i expectedTy valTy) + let + checkArgs _ [] [] = pure () + checkArgs i [] vals = + X.throwM (MIRArgNumberWrong i (i + length vals)) + checkArgs i tys [] = + X.throwM (MIRArgNumberWrong (i + length tys) i) + checkArgs i (ty : tys) (val : vals) = + do checkArg i ty val + checkArgs (i + 1) tys vals + checkArgs 0 argTys args + Setup.crucible_execute_func args + +-- | Generate a fresh variable term. The name will be used when +-- pretty-printing the variable in debug output. +mir_fresh_var :: + Text {- ^ variable name -} -> + Mir.Ty {- ^ variable type -} -> + MIRSetupM TypedTerm {- ^ fresh typed term -} +mir_fresh_var name mty = + MIRSetupM $ + do sc <- lift $ lift getSharedContext + case cryptolTypeOfActual mty of + Nothing -> X.throwM $ MIRFreshVarInvalidType mty + Just cty -> Setup.freshVariable sc name cty + -- | Load a MIR JSON file and return a handle to it. -mir_load_module :: String -> TopLevel RustModule +mir_load_module :: String -> TopLevel Mir.RustModule mir_load_module inputFile = do b <- io $ BSL.readFile inputFile @@ -26,5 +210,954 @@ mir_load_module inputFile = do let ?printCrucible = False halloc <- getHandleAlloc - col <- io $ parseMIR inputFile b - io $ translateMIR mempty col halloc + col <- io $ Mir.parseMIR inputFile b + io $ Mir.translateMIR mempty col halloc + +mir_return :: SetupValue -> MIRSetupM () +mir_return retVal = + MIRSetupM $ + do st <- get + let cc = st ^. Setup.csCrucibleContext + let mspec = st ^. Setup.csMethodSpec + let env = MS.csAllocations mspec + let nameEnv = MS.csTypeNames mspec + valTy <- typeOfSetupValue cc env nameEnv retVal + case mspec ^. MS.csRet of + Nothing -> + X.throwM (MIRReturnUnexpected valTy) + Just retTy -> + unless (checkCompatibleTys retTy valTy) $ + X.throwM (MIRReturnTypeMismatch retTy valTy) + Setup.crucible_return retVal + +mir_assert :: TypedTerm -> MIRSetupM () +mir_assert term = MIRSetupM $ do + loc <- SS.toW4Loc "mir_assert" <$> lift (lift getPosition) + tags <- view Setup.croTags + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = tags + , MS.conditionType = "specification assertion" + , MS.conditionContext = "" + } + Setup.addCondition (MS.SetupCond_Pred md term) + +mir_precond :: TypedTerm -> MIRSetupM () +mir_precond term = MIRSetupM $ do + loc <- SS.toW4Loc "mir_precond" <$> lift (lift getPosition) + Setup.crucible_precond loc term + +mir_postcond :: TypedTerm -> MIRSetupM () +mir_postcond term = MIRSetupM $ do + loc <- SS.toW4Loc "mir_postcond" <$> lift (lift getPosition) + Setup.crucible_postcond loc term + +mir_verify :: + Mir.RustModule -> + String {- ^ method name -} -> + [Lemma] {- ^ overrides -} -> + Bool {- ^ path sat checking -} -> + MIRSetupM () -> + ProofScript () -> + TopLevel Lemma +mir_verify rm nm lemmas checkSat setup tactic = + do start <- io getCurrentTime + opts <- getOptions + + -- set up the metadata map for tracking proof obligation metadata + mdMap <- io $ newIORef mempty + + cc <- setupCrucibleContext rm + SomeOnlineBackend bak <- pure (cc^.mccBackend) + let sym = cc^.mccSym + + pos <- getPosition + let loc = SS.toW4Loc "_SAW_verify_prestate" pos + + profFile <- rwProfilingFile <$> getTopLevelRW + (writeFinalProfile, pfs) <- io $ setupProfiling sym "mir_verify" profFile + + let cs = rm ^. Mir.rmCS + col = cs ^. Mir.collection + crateDisambigs = cs ^. Mir.crateHashesMap + did <- findDefId crateDisambigs (Text.pack nm) + fn <- case Map.lookup did (col ^. Mir.functions) of + Just x -> return x + Nothing -> fail $ "Couldn't find MIR function named: " ++ nm + let st0 = initialCrucibleSetupState cc fn loc + + -- execute commands of the method spec + io $ W4.setCurrentProgramLoc sym loc + methodSpec <- view Setup.csMethodSpec <$> + execStateT + (runReaderT (runMIRSetupM setup) Setup.makeCrucibleSetupRO) + st0 + + printOutLnTop Info $ + unwords ["Verifying", show (methodSpec ^. MS.csMethod), "..."] + + -- construct the initial state for verifications + (args, assumes, env, globals1) <- io $ verifyPrestate cc methodSpec Crucible.emptyGlobals + + -- save initial path conditions + frameIdent <- io $ Crucible.pushAssumptionFrame bak + + -- run the symbolic execution + printOutLnTop Info $ + unwords ["Simulating", show (methodSpec ^. MS.csMethod), "..."] + top_loc <- SS.toW4Loc "mir_verify" <$> getPosition + (ret, globals2) <- + io $ verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals1 checkSat mdMap + + -- collect the proof obligations + asserts <- verifyPoststate cc + methodSpec env globals2 ret mdMap + + -- restore previous assumption state + _ <- io $ Crucible.popAssumptionFrame bak frameIdent + + -- attempt to verify the proof obligations + printOutLnTop Info $ + unwords ["Checking proof obligations", show (methodSpec ^. MS.csMethod), "..."] + (stats,vcstats) <- verifyObligations cc methodSpec tactic assumes asserts + io $ writeFinalProfile + + let lemmaSet = Set.fromList (map (view MS.psSpecIdent) lemmas) + end <- io getCurrentTime + let diff = diffUTCTime end start + ps <- io (MS.mkProvedSpec MS.SpecProved methodSpec stats vcstats lemmaSet diff) + returnProof ps + +----- +-- Mir.Types +----- + +mir_array :: Int -> Mir.Ty -> Mir.Ty +mir_array n t = Mir.TyArray t n + +mir_bool :: Mir.Ty +mir_bool = Mir.TyBool + +mir_char :: Mir.Ty +mir_char = Mir.TyChar + +mir_i8 :: Mir.Ty +mir_i8 = Mir.TyInt Mir.B8 + +mir_i16 :: Mir.Ty +mir_i16 = Mir.TyInt Mir.B16 + +mir_i32 :: Mir.Ty +mir_i32 = Mir.TyInt Mir.B32 + +mir_i64 :: Mir.Ty +mir_i64 = Mir.TyInt Mir.B64 + +mir_i128 :: Mir.Ty +mir_i128 = Mir.TyInt Mir.B128 + +mir_isize :: Mir.Ty +mir_isize = Mir.TyInt Mir.USize + +mir_f32 :: Mir.Ty +mir_f32 = Mir.TyFloat Mir.F32 + +mir_f64 :: Mir.Ty +mir_f64 = Mir.TyFloat Mir.F64 + +mir_ref :: Mir.Ty -> Mir.Ty +mir_ref ty = Mir.TyRef ty Mir.Immut + +mir_ref_mut :: Mir.Ty -> Mir.Ty +mir_ref_mut ty = Mir.TyRef ty Mir.Mut + +mir_slice :: Mir.Ty -> Mir.Ty +mir_slice = Mir.TySlice + +mir_str :: Mir.Ty +mir_str = Mir.TyStr + +mir_tuple :: [Mir.Ty] -> Mir.Ty +mir_tuple = Mir.TyTuple + +mir_u8 :: Mir.Ty +mir_u8 = Mir.TyUint Mir.B8 + +mir_u16 :: Mir.Ty +mir_u16 = Mir.TyUint Mir.B16 + +mir_u32 :: Mir.Ty +mir_u32 = Mir.TyUint Mir.B32 + +mir_u64 :: Mir.Ty +mir_u64 = Mir.TyUint Mir.B64 + +mir_u128 :: Mir.Ty +mir_u128 = Mir.TyUint Mir.B128 + +mir_usize :: Mir.Ty +mir_usize = Mir.TyUint Mir.USize + +-------------------------------------------------------------------------------- +-- mir_verify +-------------------------------------------------------------------------------- + +-- | Create a SAWCore formula asserting that two 'MIRVal's are equal. +assertEqualVals :: + MIRCrucibleContext -> + MIRVal -> + MIRVal -> + IO Term +assertEqualVals cc v1 v2 = + do let sym = cc^.mccSym + st <- sawCoreState sym + toSC sym st =<< equalValsPred cc v1 v2 + +registerOverride :: + Options -> + MIRCrucibleContext -> + Crucible.SimContext (SAWCruciblePersonality Sym) Sym MIR -> + W4.ProgramLoc -> + IORef MetadataMap {- ^ metadata map -} -> + [MethodSpec] -> + Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym MIR rtp args ret () +registerOverride _opts cc _ctx _top_loc _mdMap cs = + do let c0 = head cs + let method = c0 ^. MS.csMethod + let rm = cc^.mccRustModule + + Crucible.AnyCFG cfg <- lookupDefIdCFG rm method + let h = Crucible.cfgHandle cfg + let retTy = Crucible.handleReturnType h + + Crucible.bindFnHandle h + $ Crucible.UseOverride + $ Crucible.mkOverride' + (Crucible.handleName h) + retTy + (panic "registerOverride.methodSpecHandler" ["not yet implemented"]) + +resolveArguments :: + MIRCrucibleContext -> + MethodSpec -> + Map MS.AllocIndex (Some (MirPointer Sym)) -> + IO [(Mir.Ty, MIRVal)] +resolveArguments cc mspec env = mapM resolveArg [0..(nArgs-1)] + where + nArgs = toInteger (length (mspec ^. MS.csArgs)) + tyenv = MS.csAllocations mspec + nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames + nm = mspec ^. MS.csMethod + + checkArgTy i mt mt' = + unless (checkCompatibleTys mt mt') $ + fail $ unlines [ "Type mismatch in argument " ++ show i ++ " when verifying " ++ show nm + , "Argument is declared with type: " ++ show mt + , "but provided argument has incompatible type: " ++ show mt' + , "Note: this may be because the signature of your " ++ + "function changed during compilation." + ] + resolveArg i = + case Map.lookup i (mspec ^. MS.csArgBindings) of + Just (mt, sv) -> do + mt' <- typeOfSetupValue cc tyenv nameEnv sv + checkArgTy i mt mt' + v <- resolveSetupVal cc env tyenv nameEnv sv + return (mt, v) + Nothing -> fail $ unwords ["Argument", show i, "unspecified when verifying", show nm] + +-- | For each points-to constraint in the pre-state section of the +-- function spec, write the given value to the address of the given +-- pointer. +setupPrePointsTos :: + MethodSpec -> + MIRCrucibleContext -> + Map MS.AllocIndex (Some (MirPointer Sym)) -> + [MirPointsTo] -> + Crucible.SymGlobalState Sym -> + IO (Crucible.SymGlobalState Sym) +setupPrePointsTos _mspec _cc _env pts mem0 = foldM doPointsTo mem0 pts + where + doPointsTo :: Crucible.SymGlobalState Sym -> MirPointsTo -> IO (Crucible.SymGlobalState Sym) + doPointsTo _mem _pt = + panic "setupPrePointsTo" ["not yet implemented"] + +-- | Collects boolean terms that should be assumed to be true. +setupPrestateConditions :: + MethodSpec -> + MIRCrucibleContext -> + Map MS.AllocIndex (Some (MirPointer Sym)) -> + [SetupCondition] -> + IO [Crucible.LabeledPred Term AssumptionReason] +setupPrestateConditions mspec cc env = aux [] + where + tyenv = MS.csAllocations mspec + nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames + + aux acc [] = return acc + + aux acc (MS.SetupCond_Equal loc val1 val2 : xs) = + do val1' <- resolveSetupVal cc env tyenv nameEnv val1 + val2' <- resolveSetupVal cc env tyenv nameEnv val2 + t <- assertEqualVals cc val1' val2' + let lp = Crucible.LabeledPred t (loc, "equality precondition") + aux (lp:acc) xs + + aux acc (MS.SetupCond_Pred loc tm : xs) = + let lp = Crucible.LabeledPred (ttTerm tm) (loc, "precondition") in + aux (lp:acc) xs + + aux _ (MS.SetupCond_Ghost empty_ _ _ _ : _) = absurd empty_ + +verifyObligations :: + MIRCrucibleContext -> + MethodSpec -> + ProofScript () -> + [Crucible.LabeledPred Term AssumptionReason] -> + [(String, MS.ConditionMetadata, Term)] -> + TopLevel (SolverStats, [MS.VCStats]) +verifyObligations cc mspec tactic assumes asserts = + do let sym = cc^.mccSym + st <- io $ sawCoreState sym + let sc = saw_ctx st + assume <- io $ scAndList sc (toListOf (folded . Crucible.labeledPred) assumes) + let nm = show $ mspec ^. MS.csMethod + outs <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, md, assert)) -> do + goal <- io $ scImplies sc assume assert + goal' <- io $ boolToProp sc [] goal -- TODO, generalize over inputs + let ploc = MS.conditionLoc md + let gloc = (unwords [show (W4.plSourceLoc ploc) + ,"in" + , show (W4.plFunction ploc)]) ++ + (if Prelude.null (MS.conditionContext md) then [] else + "\n" ++ MS.conditionContext md) + let goalname = concat [nm, " (", takeWhile (/= '\n') msg, ")"] + let proofgoal = ProofGoal + { goalNum = n + , goalType = MS.conditionType md + , goalName = nm + , goalLoc = gloc + , goalDesc = msg + , goalSequent = propToSequent goal' + , goalTags = MS.conditionTags md + } + res <- runProofScript tactic goal' proofgoal (Just ploc) + (Text.unwords + ["MIR verification condition:", Text.pack (show n), Text.pack goalname]) + False -- do not record in the theorem database + False -- TODO, useSequentGoals... + case res of + ValidProof stats thm -> + return (stats, MS.VCStats md stats (thmSummary thm) (thmNonce thm) (thmDepends thm) (thmElapsedTime thm)) + InvalidProof stats vals _pst -> do + printOutLnTop Info $ unwords ["Subgoal failed:", nm, msg] + printOutLnTop Info (show stats) + printOutLnTop OnlyCounterExamples "----------Counterexample----------" + opts <- sawPPOpts <$> rwPPOpts <$> getTopLevelRW + let showEC ec = Text.unpack (toShortName (ecName ec)) + let showAssignment (name, val) = " " ++ showEC name ++ ": " ++ show (ppFirstOrderValue opts val) + mapM_ (printOutLnTop OnlyCounterExamples . showAssignment) vals + io $ fail "Proof failed." -- Mirroring behavior of llvm_verify + UnfinishedProof pst -> + io $ fail $ "Proof failed " ++ show (length (psGoals pst)) ++ " goals remaining." + + printOutLnTop Info $ unwords ["Proof succeeded!", nm] + + let stats = mconcat (map fst outs) + let vcstats = map snd outs + return (stats, vcstats) + +verifyPoststate :: + MIRCrucibleContext {- ^ crucible context -} -> + MethodSpec {- ^ specification -} -> + Map MS.AllocIndex (Some (MirPointer Sym)) {- ^ allocation substitution -} -> + Crucible.SymGlobalState Sym {- ^ global variables -} -> + Maybe (Mir.Ty, MIRVal) {- ^ optional return value -} -> + IORef MetadataMap {- ^ metadata map -} -> + TopLevel [(String, MS.ConditionMetadata, Term)] {- ^ generated labels and verification conditions -} +verifyPoststate cc mspec env0 globals ret mdMap = + mccWithBackend cc $ \bak -> + do opts <- getOptions + sc <- getSharedContext + poststateLoc <- SS.toW4Loc "_SAW_verify_poststate" <$> getPosition + io $ W4.setCurrentProgramLoc sym poststateLoc + + -- This discards all the obligations generated during + -- symbolic execution itself, i.e., which are not directly + -- generated from specification postconditions. This + -- is, in general, unsound. + skipSafetyProofs <- gets rwSkipSafetyProofs + when skipSafetyProofs (io (Crucible.clearProofObligations bak)) + + let ecs0 = Map.fromList + [ (ecVarIndex ec, ec) + | tt <- mspec ^. MS.csPreState . MS.csFreshVars + , let ec = tecExt tt ] + terms0 <- io $ traverse (scExtCns sc) ecs0 + + let initialFree = Set.fromList (map (ecVarIndex . tecExt) + (view (MS.csPostState . MS.csFreshVars) mspec)) + matchPost <- io $ + runOverrideMatcher sym globals env0 terms0 initialFree poststateLoc $ + do matchResult opts sc + learnCond opts sc cc mspec MS.PostState (mspec ^. MS.csPostState) + + st <- case matchPost of + Left err -> fail (show err) + Right (_, st) -> return st + io $ forM_ (view osAsserts st) $ \(md, Crucible.LabeledPred p r) -> + do (ann,p') <- W4.annotateTerm sym p + modifyIORef mdMap (Map.insert ann md) + Crucible.addAssertion bak (Crucible.LabeledPred p' r) + + finalMdMap <- io $ readIORef mdMap + obligations <- io $ Crucible.getProofObligations bak + io $ Crucible.clearProofObligations bak + io $ mapM (verifyObligation sc finalMdMap) (maybe [] Crucible.goalsToList obligations) + + where + sym = cc^.mccSym + + verifyObligation sc finalMdMap + (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError loc err))) = + do st <- sawCoreState sym + hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps + conclTerm <- toSC sym st concl + obligation <- scImplies sc hypTerm conclTerm + let defaultMd = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = mempty + , MS.conditionType = "safety assertion" + , MS.conditionContext = "" + } + let md = fromMaybe defaultMd $ + do ann <- W4.getAnnotation sym concl + Map.lookup ann finalMdMap + return (Crucible.simErrorReasonMsg err, md, obligation) + + matchResult opts sc = + case (ret, mspec ^. MS.csRetValue) of + (Just (rty,r), Just expect) -> + let md = MS.ConditionMetadata + { MS.conditionLoc = mspec ^. MS.csLoc + , MS.conditionTags = mempty + , MS.conditionType = "return value matching" + , MS.conditionContext = "" + } in + matchArg opts sc cc mspec MS.PostState md r rty expect + (Nothing , Just _ ) -> fail "verifyPoststate: unexpected mir_return specification" + _ -> return () + +-- | Evaluate the precondition part of a Crucible method spec: +-- +-- * Allocate heap space for each 'mir_alloc' statement. +-- +-- * Record an equality precondition for each 'mir_equal' +-- statement. +-- +-- * Write to memory for each 'mir_points_to' statement. (Writes +-- to already-initialized locations are transformed into equality +-- preconditions.) +-- +-- * Evaluate the function arguments from the 'mir_execute_func' +-- statement. +-- +-- Returns a tuple of (arguments, preconditions, pointer values, +-- memory). +verifyPrestate :: + MIRCrucibleContext -> + MS.CrucibleMethodSpecIR MIR -> + Crucible.SymGlobalState Sym -> + IO ([(Mir.Ty, MIRVal)], + [Crucible.LabeledPred Term AssumptionReason], + Map MS.AllocIndex (Some (MirPointer Sym)), + Crucible.SymGlobalState Sym) +verifyPrestate cc mspec globals0 = + do let sym = cc^.mccSym + let tyenv = MS.csAllocations mspec + let nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames + + let prestateLoc = W4.mkProgramLoc "_SAW_verify_prestate" W4.InternalPos + liftIO $ W4.setCurrentProgramLoc sym prestateLoc + + -- Allocate memory for each 'mir_alloc' + let doAlloc = panic "verifyPrestate.doAlloc" ["not yet implemented"] + (env, globals1) <- runStateT + (Map.traverseWithKey (doAlloc cc) (mspec ^. MS.csPreState . MS.csAllocs)) + globals0 + + globals2 <- setupPrePointsTos mspec cc env (mspec ^. MS.csPreState . MS.csPointsTos) globals1 + cs <- setupPrestateConditions mspec cc env (mspec ^. MS.csPreState . MS.csConditions) + args <- resolveArguments cc mspec env + + -- Check the type of the return setup value + let methodStr = show (mspec ^. MS.csMethod) + case (mspec ^. MS.csRetValue, mspec ^. MS.csRet) of + (Just _, Nothing) -> + fail $ unlines + [ "Return value specified, but method " ++ methodStr ++ + " has void return type" + ] + (Just sv, Just retTy) -> + do retTy' <- typeOfSetupValue cc tyenv nameEnv sv + unless (checkCompatibleTys retTy retTy') $ + fail $ unlines + [ "Incompatible types for return value when verifying " ++ methodStr + , "Expected: " ++ show retTy + , "but given value of type: " ++ show retTy' + ] + (Nothing, _) -> return () + + return (args, cs, env, globals2) + +-- | Simulate a MIR function with Crucible as part of a 'mir_verify' command, +-- making sure to install any overrides that the user supplies. +verifySimulate :: + Options -> + MIRCrucibleContext -> + [Crucible.GenericExecutionFeature Sym] -> + MethodSpec -> + [(a, MIRVal)] -> + [Crucible.LabeledPred Term AssumptionReason] -> + W4.ProgramLoc -> + [Lemma] -> + Crucible.SymGlobalState Sym -> + Bool {- ^ path sat checking -} -> + IORef MetadataMap {- ^ metadata map -} -> + IO (Maybe (Mir.Ty, MIRVal), Crucible.SymGlobalState Sym) +verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat mdMap = + mccWithBackend cc $ \bak -> + do let rm = cc^.mccRustModule + let cfgMap = rm ^. Mir.rmCFGs + let cs = rm ^. Mir.rmCS + let col = cs ^. Mir.collection + let method = mspec ^. MS.csMethod + let verbosity = simVerbose opts + let halloc = cc^.mccHandleAllocator + + when (verbosity > 2) $ + putStrLn "starting executeCrucibleMIR" + + -- Translate the static initializer function + let ?debug = simVerbose opts + -- For now, we use the same default settings for implicit parameters as in + -- crux-mir. We may want to add options later that allow configuring these. + let ?assertFalseOnError = True + let ?customOps = customOps + Crucible.AnyCFG staticInitCfg <- Mir.transStatics cs halloc + let staticInitHndl = Crucible.cfgHandle staticInitCfg + Refl <- case testEquality (Crucible.handleArgTypes staticInitHndl) Ctx.Empty of + Just e -> pure e + Nothing -> fail "mir_verify: static initializer should not require arguments" + + -- Find and run the target function + Crucible.AnyCFG methodCfg <- lookupDefIdCFG rm method + let methodHndl = Crucible.cfgHandle methodCfg + let methodArgTys = Crucible.handleArgTypes methodHndl + let methodRetTy = Crucible.handleReturnType methodHndl + + regmap <- prepareArgs methodArgTys (map snd args) + res <- + do let feats = pfs + let simctx = Crucible.initSimContext bak Mir.mirIntrinsicTypes halloc stdout + (Crucible.FnBindings Crucible.emptyHandleMap) Mir.mirExtImpl + SAWCruciblePersonality + let simSt = Crucible.InitialState simctx globals Crucible.defaultAbortHandler methodRetTy + let fnCall = Crucible.regValue <$> Crucible.callCFG methodCfg regmap + let overrideSim = + do forM_ cfgMap $ \(Crucible.AnyCFG cfg) -> + Crucible.bindFnHandle (Crucible.cfgHandle cfg) $ + Crucible.UseCFG cfg (Crucible.postdomInfo cfg) + _ <- Crucible.callCFG staticInitCfg Crucible.emptyRegMap + + mapM_ (registerOverride opts cc simctx top_loc mdMap) + (List.groupOn (view MS.csMethod) (map (view MS.psSpec) lemmas)) + liftIO $ + for_ assumes $ \(Crucible.LabeledPred p (md, reason)) -> + do expr <- resolveSAWPred cc p + let loc = MS.conditionLoc md + Crucible.addAssumption bak (Crucible.GenericAssumption loc reason expr) + fnCall + Crucible.executeCrucible (map Crucible.genericToExecutionFeature feats) + (simSt (Crucible.runOverrideSim methodRetTy overrideSim)) + + case res of + Crucible.FinishedResult _ pr -> + do Crucible.GlobalPair retval globals1 <- + case pr of + Crucible.TotalRes gp -> return gp + Crucible.PartialRes _ _ gp _ -> + do printOutLn opts Info "Symbolic simulation completed with side conditions." + return gp + let ret_ty = mspec ^. MS.csRet + retval' <- + case ret_ty of + Nothing -> return Nothing + Just ret_mt -> + case retval of + Crucible.RegEntry ty val -> + case decodeMIRVal col ret_mt (Crucible.AnyValue ty val) of + Nothing -> error $ "FIXME: Unsupported return type: " ++ show ret_ty + Just v -> return (Just (ret_mt, v)) + return (retval', globals1) + + Crucible.AbortedResult _ ar -> + do let resultDoc = ppMIRAbortedResult cc ar + fail $ unlines [ "Symbolic execution failed." + , show resultDoc + ] + + Crucible.TimeoutResult _cxt -> fail "Symbolic execution timed out." + + where + prepareArg :: forall tp. Crucible.TypeRepr tp -> MIRVal -> IO (Crucible.RegValue Sym tp) + prepareArg ty (MIRVal vTy vVal) = + case testEquality ty (shapeType vTy) of + Just Refl -> pure vVal + Nothing -> fail $ unlines + [ "argument type mismatch" + , show ty + , show (shapeType vTy) + ] + + prepareArgs :: + forall xs. + Ctx.Assignment Crucible.TypeRepr xs -> + [MIRVal] -> + IO (Crucible.RegMap Sym xs) + prepareArgs ctx xs | length xs /= Ctx.sizeInt (Ctx.size ctx) = + fail $ "Wrong number of arguments: found " ++ show (length xs) ++ ", expected " ++ show (Ctx.sizeInt (Ctx.size ctx)) + prepareArgs ctx xs = + Crucible.RegMap <$> + Ctx.traverseWithIndex (\idx tr -> + do v <- prepareArg tr (xs !! Ctx.indexVal idx) + return (Crucible.RegEntry tr v)) + ctx + +-------------------------------------------------------------------------------- +-- Utilities +-------------------------------------------------------------------------------- + +-- | Check if two 'Mir.Ty's are compatible in SAW. This is a slightly coarser +-- notion of equality to reflect the fact that MIR's type system is richer than +-- Cryptol's type system, and some types which would be distinct in MIR are in +-- fact equal when converted to the equivalent Cryptol types. In particular: +-- +-- 1. A @u@ type is always compatible with an @i@ type. For instance, @u8@ +-- is compatible with @i8@, and @u16@ is compatible with @i16@. Note that the +-- bit sizes of both types must be the same. For instance, @u8@ is /not/ +-- compatible with @i16@. +-- +-- 2. The @usize@/@isize@ types are always compatible with @u@/@i@, where +-- @N@ is the number of bits corresponding to the 'Mir.SizeBits' type in +-- "Mir.Intrinsics". (This is a bit unsavory, as the actual size of +-- @usize@/@isize@ is platform-dependent, but this is the current approach.) +-- +-- 3. Compatibility applies recursively. For instance, @[ty_1; N]@ is compatible +-- with @[ty_2; N]@ iff @ty_1@ and @ty_2@ are compatibile. Similarly, a tuple +-- typle @(ty_1_a, ..., ty_n_a)@ is compatible with @(ty_1_b, ..., ty_n_b)@ +-- iff @ty_1_a@ is compatible with @ty_1_b@, ..., and @ty_n_a@ is compatible +-- with @ty_n_b@. +-- +-- See also @checkRegisterCompatibility@ in "SAWScript.Crucible.LLVM.Builtins" +-- and @registerCompatible@ in "SAWScript.Crucible.JVM.Builtins", which fill a +-- similar niche in the LLVM and JVM backends, respectively. +checkCompatibleTys :: Mir.Ty -> Mir.Ty -> Bool +checkCompatibleTys ty1 ty2 = tyView ty1 == tyView ty2 + +-- | Like 'Mir.Ty', but where: +-- +-- * The 'TyInt' and 'TyUint' constructors have been collapsed into a single +-- 'TyViewInt' constructor. +-- +-- * 'TyViewInt' uses 'BaseSizeView' instead of 'Mir.BaseSize'. +-- +-- * Recursive occurrences of 'Mir.Ty' use 'TyView' instead. This also applies +-- to fields of type 'SubstsView' and 'FnSigView', which also replace 'Mir.Ty' +-- with 'TyView' in their definitions. +-- +-- This provides a coarser notion of equality than what the 'Eq' instance for +-- 'Mir.Ty' provides, which distinguishes the two sorts of integer types. +-- +-- This is an internal data type that is used to power the 'checkCompatibleTys' +-- function. Refer to the Haddocks for that function for more information on why +-- this is needed. +data TyView + = TyViewBool + | TyViewChar + -- | The sole integer type. Both 'TyInt' and 'TyUint' are mapped to + -- 'TyViewInt', and 'BaseSizeView' is used instead of 'Mir.BaseSize'. + | TyViewInt !BaseSizeView + | TyViewTuple ![TyView] + | TyViewSlice !TyView + | TyViewArray !TyView !Int + | TyViewRef !TyView !Mir.Mutability + | TyViewAdt !Mir.DefId !Mir.DefId !SubstsView + | TyViewFnDef !Mir.DefId + | TyViewClosure [TyView] + | TyViewStr + | TyViewFnPtr !FnSigView + | TyViewDynamic !Mir.TraitName + | TyViewRawPtr !TyView !Mir.Mutability + | TyViewFloat !Mir.FloatKind + | TyViewDowncast !TyView !Integer + | TyViewNever + | TyViewForeign + | TyViewLifetime + | TyViewConst + | TyViewErased + | TyViewInterned Mir.TyName + deriving Eq + +-- | Like 'Mir.BaseSize', but without a special case for @usize@/@isize@. +-- Instead, these are mapped to their actual size, which is determined by the +-- number of bits in the 'Mir.SizeBits' type in "Mir.Intrinsics". (This is a bit +-- unsavory, as the actual size of @usize@/@isize@ is platform-dependent, but +-- this is the current approach.) +data BaseSizeView + = B8View + | B16View + | B32View + | B64View + | B128View + deriving Eq + +-- | Like 'Mir.Substs', but using 'TyView's instead of 'Mir.Ty'. +-- +-- This is an internal data type that is used to power the 'checkCompatibleTys' +-- function. Refer to the Haddocks for that function for more information on why +-- this is needed. +newtype SubstsView = SubstsView [TyView] + deriving Eq + +-- | Like 'Mir.FnSig', but using 'TyView's instead of 'Mir.Ty'. +-- +-- This is an internal data type that is used to power the 'checkCompatibleTys' +-- function. Refer to the Haddocks for that function for more information on why +-- this is needed. +data FnSigView = FnSigView { + _fsvarg_tys :: ![TyView] + , _fsvreturn_ty :: !TyView + , _fsvabi :: Mir.Abi + , _fsvspreadarg :: Maybe Int + } + deriving Eq + +-- | Convert a 'Mir.Ty' value to a 'TyView' value. +tyView :: Mir.Ty -> TyView +-- The two most important cases. Both sorts of integers are mapped to TyViewInt. +tyView (Mir.TyInt bs) = TyViewInt (baseSizeView bs) +tyView (Mir.TyUint bs) = TyViewInt (baseSizeView bs) +-- All other cases are straightforward. +tyView Mir.TyBool = TyViewBool +tyView Mir.TyChar = TyViewChar +tyView (Mir.TyTuple tys) = TyViewTuple (map tyView tys) +tyView (Mir.TySlice ty) = TyViewSlice (tyView ty) +tyView (Mir.TyArray ty n) = TyViewArray (tyView ty) n +tyView (Mir.TyRef ty mut) = TyViewRef (tyView ty) mut +tyView (Mir.TyAdt monoDid origDid substs) = + TyViewAdt monoDid origDid (substsView substs) +tyView (Mir.TyFnDef did) = TyViewFnDef did +tyView (Mir.TyClosure tys) = TyViewClosure (map tyView tys) +tyView Mir.TyStr = TyViewStr +tyView (Mir.TyFnPtr sig) = TyViewFnPtr (fnSigView sig) +tyView (Mir.TyDynamic trait) = TyViewDynamic trait +tyView (Mir.TyRawPtr ty mut) = TyViewRawPtr (tyView ty) mut +tyView (Mir.TyFloat fk) = TyViewFloat fk +tyView (Mir.TyDowncast ty n) = TyViewDowncast (tyView ty) n +tyView Mir.TyNever = TyViewNever +tyView Mir.TyForeign = TyViewForeign +tyView Mir.TyLifetime = TyViewLifetime +tyView Mir.TyConst = TyViewConst +tyView Mir.TyErased = TyViewErased +tyView (Mir.TyInterned nm) = TyViewInterned nm + +-- | Convert a 'Mir.BaseSize' value to a 'BaseSizeView' value. +baseSizeView :: Mir.BaseSize -> BaseSizeView +baseSizeView Mir.B8 = B8View +baseSizeView Mir.B16 = B16View +baseSizeView Mir.B32 = B32View +baseSizeView Mir.B64 = B64View +baseSizeView Mir.B128 = B128View +baseSizeView Mir.USize = + case Map.lookup (natValue sizeBitsRepr) bitSizesMap of + Just bsv -> bsv + Nothing -> + error $ "Mir.Intrinsics.BaseSize bit size not supported: " ++ show sizeBitsRepr + where + sizeBitsRepr = knownNat @Mir.SizeBits + + bitSizesMap :: Map Natural BaseSizeView + bitSizesMap = Map.fromList + [ (natValue (knownNat @8), B8View) + , (natValue (knownNat @16), B16View) + , (natValue (knownNat @32), B32View) + , (natValue (knownNat @64), B64View) + , (natValue (knownNat @128), B128View) + ] + +-- | Convert a 'Mir.Substs' value to a 'SubstsView' value. +substsView :: Mir.Substs -> SubstsView +substsView (Mir.Substs tys) = SubstsView (map tyView tys) + +-- | Convert a 'Mir.FnSig' value to a 'FnSigView' value. +fnSigView :: Mir.FnSig -> FnSigView +fnSigView (Mir.FnSig argTys retTy abi spreadarg) = + FnSigView (map tyView argTys) (tyView retTy) abi spreadarg + +-- | Returns the Cryptol type of a MIR type, returning 'Nothing' if it is not +-- easily expressible in Cryptol's type system or if it is not currently +-- supported. +cryptolTypeOfActual :: Mir.Ty -> Maybe Cryptol.Type +cryptolTypeOfActual mty = + case mty of + Mir.TyBool -> Just Cryptol.tBit + Mir.TyChar -> Just $ Cryptol.tWord $ Cryptol.tNum (32 :: Integer) + Mir.TyUint bs -> baseSizeType bs + Mir.TyInt bs -> baseSizeType bs + Mir.TyArray t n -> Cryptol.tSeq (Cryptol.tNum n) <$> cryptolTypeOfActual t + Mir.TyTuple tys -> Cryptol.tTuple <$> traverse cryptolTypeOfActual tys + + Mir.TyFloat _ -> Nothing + Mir.TyStr -> Nothing + Mir.TyAdt _ _ _ -> Nothing + Mir.TyRef _ _ -> Nothing + Mir.TyFnDef _ -> Nothing + Mir.TyFnPtr _ -> Nothing + Mir.TyRawPtr _ _ -> Nothing + Mir.TyClosure _ -> Nothing + Mir.TySlice _ -> Nothing + Mir.TyDowncast _ _ -> Nothing + Mir.TyNever -> Nothing + Mir.TyForeign -> Nothing + Mir.TyLifetime -> Nothing + Mir.TyConst -> Nothing + Mir.TyErased -> Nothing + Mir.TyInterned _ -> Nothing + Mir.TyDynamic _ -> Nothing + where + baseSizeType :: Mir.BaseSize -> Maybe Cryptol.Type + baseSizeType Mir.B8 = Just $ Cryptol.tWord $ Cryptol.tNum (8 :: Integer) + baseSizeType Mir.B16 = Just $ Cryptol.tWord $ Cryptol.tNum (16 :: Integer) + baseSizeType Mir.B32 = Just $ Cryptol.tWord $ Cryptol.tNum (32 :: Integer) + baseSizeType Mir.B64 = Just $ Cryptol.tWord $ Cryptol.tNum (64 :: Integer) + baseSizeType Mir.B128 = Just $ Cryptol.tWord $ Cryptol.tNum (128 :: Integer) + baseSizeType Mir.USize = Just $ Cryptol.tWord $ Cryptol.tNum $ natValue $ knownNat @Mir.SizeBits + +-- | Given a function name @fnName@, attempt to look up its corresponding +-- 'Mir.DefId'. Currently, the following types of function names are permittd: +-- +-- * @/::: A fully disambiguated name. +-- +-- * @::: A name without a disambiguator. In this +-- case, SAW will attempt to look up a disambiguator from the @crateDisambigs@ +-- map. If none can be found, or if there are multiple disambiguators for the +-- given @@, then this will fail. +findDefId :: Map Text (NonEmpty Text) -> Text -> TopLevel Mir.DefId +findDefId crateDisambigs fnName = do + (crate, path) <- + case edid of + crate:path -> pure (crate, path) + [] -> fail $ unlines + [ "The function `" ++ fnNameStr ++ "` lacks a crate." + , "Consider providing one, e.g., `::" ++ fnNameStr ++ "`." + ] + let crateStr = Text.unpack crate + case Text.splitOn "/" crate of + [crateNoDisambig, disambig] -> + pure $ Mir.textId $ Text.intercalate "::" + $ (crateNoDisambig <> "/" <> disambig) : path + [_] -> + case Map.lookup crate crateDisambigs of + Just allDisambigs@(disambig :| otherDisambigs) + | F.null otherDisambigs + -> pure $ Mir.textId $ Text.intercalate "::" + $ (crate <> "/" <> disambig) : path + | otherwise + -> fail $ unlines $ + [ "ambiguous crate " ++ crateStr + , "crate disambiguators:" + ] ++ F.toList (Text.unpack <$> allDisambigs) + Nothing -> fail $ "unknown crate " ++ crateStr + _ -> fail $ "Malformed crate name: " ++ show crateStr + where + fnNameStr = Text.unpack fnName + edid = Text.splitOn "::" fnName + +-- | Look up the control-flow graph (CFG) for a 'Mir.DefId', failing if a CFG +-- cannot be found. +lookupDefIdCFG :: + MonadFail m + => Mir.RustModule + -> Mir.DefId + -> m (Crucible.AnyCFG MIR) +lookupDefIdCFG rm method = + case Map.lookup (Mir.idText method) (rm ^. Mir.rmCFGs) of + Just x -> return x + Nothing -> fail $ "Couldn't find CFG for MIR function: " ++ show method + +setupCrucibleContext :: Mir.RustModule -> TopLevel MIRCrucibleContext +setupCrucibleContext rm = + do halloc <- getHandleAlloc + sc <- getSharedContext + pathSatSolver <- gets rwPathSatSolver + sym <- io $ newSAWCoreExprBuilder sc + bak <- io $ newSAWCoreBackend pathSatSolver sym + opts <- getOptions + io $ do let cfg = W4.getConfiguration sym + verbSetting <- W4.getOptionSetting W4.verbosity cfg + _ <- W4.setOpt verbSetting $ toInteger $ simVerbose opts + return () + + -- TODO! there's a lot of options setup we need to replicate + -- from SAWScript.Crucible.LLVM.Builtins + + return MIRCrucibleContext { _mccRustModule = rm + , _mccBackend = bak + , _mccHandleAllocator = halloc + } + +-------------------------------------------------------------------------------- +-- Errors +-------------------------------------------------------------------------------- + +data MIRSetupError + = MIRFreshVarInvalidType Mir.Ty + | MIRArgTypeMismatch Int Mir.Ty Mir.Ty -- argument position, expected, found + | MIRArgNumberWrong Int Int -- number expected, number found + | MIRReturnUnexpected Mir.Ty -- found + | MIRReturnTypeMismatch Mir.Ty Mir.Ty -- expected, found + +instance X.Exception MIRSetupError where + toException = topLevelExceptionToException + fromException = topLevelExceptionFromException + +instance Show MIRSetupError where + show err = + case err of + MIRFreshVarInvalidType jty -> + "mir_fresh_var: Invalid type: " ++ show jty + MIRArgTypeMismatch i expected found -> + unlines + [ "mir_execute_func: Argument type mismatch" + , "Argument position: " ++ show i + , "Expected type: " ++ show expected + , "Given type: " ++ show found + ] + MIRArgNumberWrong expected found -> + unlines + [ "mir_execute_func: Wrong number of arguments" + , "Expected: " ++ show expected + , "Given: " ++ show found + ] + MIRReturnUnexpected found -> + unlines + [ "mir_return: Unexpected return value for void method" + , "Given type: " ++ show found + ] + MIRReturnTypeMismatch expected found -> + unlines + [ "mir_return: Return type mismatch" + , "Expected type: " ++ show expected + , "Given type: " ++ show found + ] diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs new file mode 100644 index 0000000000..21895c7ee7 --- /dev/null +++ b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs @@ -0,0 +1,162 @@ +{-# Language DataKinds #-} +{-# Language OverloadedStrings #-} +{-# Language RankNTypes #-} +{-# Language TemplateHaskell #-} +{-# Language TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} + +-- | Provides type-checked representations for Rust/MIR function specifications +-- and functions for creating them from ASTs. +module SAWScript.Crucible.MIR.MethodSpecIR + ( -- * @MIRCrucibleContext@ + MIRCrucibleContext(..) + , mccRustModule + , mccBackend + , mccHandleAllocator + , mccWithBackend + , mccSym + + -- * @MirPointsTo@ + , MirPointsTo(..) + + -- * @MirAllocSpec@ + , MirAllocSpec(..) + , maType + , maMutbl + , maMirType + , maLen + + -- * @MirPointer@ + , MirPointer(..) + , mpType + , mpMutbl + , mpMirType + , mpRef + + -- * @MIRMethodSpec@ + , MIRMethodSpec + + -- * Initial CrucibleSetupMethodSpec + , initialDefCrucibleMethodSpecIR + , initialCrucibleSetupState + ) where + +import Control.Lens (Getter, (^.), makeLenses, to) +import Data.Parameterized.Classes +import Data.Parameterized.Some +import Data.Text (Text) +import qualified Prettyprinter as PP + +import Lang.Crucible.FunctionHandle (HandleAllocator) +import Lang.Crucible.Types +import Mir.DefId +import Mir.Generator +import Mir.Intrinsics +import qualified Mir.Mir as M +import What4.ProgramLoc (ProgramLoc) + +import SAWScript.Crucible.Common +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import qualified SAWScript.Crucible.Common.Override as MS +import qualified SAWScript.Crucible.Common.Setup.Type as Setup + +type instance MS.HasSetupNull MIR = 'False +type instance MS.HasSetupGlobal MIR = 'False +type instance MS.HasSetupStruct MIR = 'True +type instance MS.HasSetupArray MIR = 'True +type instance MS.HasSetupElem MIR = 'True +type instance MS.HasSetupField MIR = 'True +type instance MS.HasSetupCast MIR = 'False +type instance MS.HasSetupUnion MIR = 'False +type instance MS.HasSetupGlobalInitializer MIR = 'False + +type instance MS.HasGhostState MIR = 'False + +type instance MS.TypeName MIR = Text +type instance MS.ExtType MIR = M.Ty + +type instance MS.MethodId MIR = DefId +type instance MS.AllocSpec MIR = Some MirAllocSpec +type instance MS.PointsTo MIR = MirPointsTo +type instance MS.ResolvedState MIR = () +type instance MS.CastType MIR = () + +type instance MS.Codebase MIR = CollectionState + +data MIRCrucibleContext = + MIRCrucibleContext + { _mccRustModule :: RustModule + , _mccBackend :: SomeOnlineBackend + , _mccHandleAllocator :: HandleAllocator + } + +type instance MS.CrucibleContext MIR = MIRCrucibleContext + +mccWithBackend :: + MIRCrucibleContext -> + (forall solver. OnlineSolver solver => Backend solver -> a) -> + a +mccWithBackend cc k = + case _mccBackend cc of SomeOnlineBackend bak -> k bak + +mccSym :: Getter MIRCrucibleContext Sym +mccSym = to (\mcc -> mccWithBackend mcc backendGetSym) + +type instance MS.Pointer' MIR sym = Some (MirPointer sym) + + +data MirPointsTo = MirPointsTo MS.AllocIndex [MS.SetupValue MIR] + deriving (Show) + +instance PP.Pretty MirPointsTo where + pretty (MirPointsTo alloc sv) = PP.parens $ + PP.pretty (show alloc) PP.<+> "->" PP.<+> PP.list (map MS.ppSetupValue sv) + +data MirAllocSpec tp = MirAllocSpec + { _maType :: TypeRepr tp + , _maMutbl :: M.Mutability + , _maMirType :: M.Ty + , _maLen :: Int + } + deriving (Show) + +instance ShowF MirAllocSpec where + +data MirPointer sym tp = MirPointer + { _mpType :: TypeRepr tp + , _mpMutbl :: M.Mutability + , _mpMirType :: M.Ty + , _mpRef :: MirReferenceMux sym tp + } + +type MIRMethodSpec = MS.CrucibleMethodSpecIR MIR + +makeLenses ''MIRCrucibleContext +makeLenses ''MirAllocSpec +makeLenses ''MirPointer + +initialDefCrucibleMethodSpecIR :: + CollectionState -> + M.Fn -> + ProgramLoc -> + MS.CrucibleMethodSpecIR MIR +initialDefCrucibleMethodSpecIR rm fn loc = + let fname = fn ^. M.fname + fsig = fn ^. M.fsig + argTys = fsig ^. M.fsarg_tys + retTy = case fsig ^. M.fsreturn_ty of + M.TyTuple [] -> Nothing + ty -> Just ty in + MS.makeCrucibleMethodSpecIR fname argTys retTy loc rm + +initialCrucibleSetupState :: + MIRCrucibleContext -> + M.Fn -> + ProgramLoc -> + Setup.CrucibleSetupState MIR +initialCrucibleSetupState cc fn loc = + Setup.makeCrucibleSetupState () cc $ + initialDefCrucibleMethodSpecIR + (cc ^. mccRustModule ^. rmCS) + fn + loc diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs new file mode 100644 index 0000000000..93939e22e2 --- /dev/null +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -0,0 +1,503 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeApplications #-} + +-- | Override matching and application for MIR. +module SAWScript.Crucible.MIR.Override + ( OverrideMatcher + , OverrideMatcher'(..) + , runOverrideMatcher + + , setupValueSub + , osAsserts + , termSub + + , learnCond + , matchArg + , decodeMIRVal + ) where + +import qualified Control.Exception as X +import Control.Lens +import Control.Monad.IO.Class (MonadIO(..)) +import Data.Foldable (for_, traverse_) +import qualified Data.Functor.Product as Functor +import Data.List (tails) +import qualified Data.Map as Map +import Data.Map (Map) +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(..)) +import qualified Data.Parameterized.TraversableFC as FC +import qualified Data.Set as Set +import qualified Data.Vector as V +import Data.Void (absurd) +import qualified Prettyprinter as PP + +import qualified Cryptol.TypeCheck.AST as Cryptol +import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalType) +import qualified Lang.Crucible.Backend as Crucible +import qualified Lang.Crucible.Simulator as Crucible +import qualified Lang.Crucible.Types as Crucible +import qualified Mir.Intrinsics as Mir +import Mir.Intrinsics (MIR) +import qualified Mir.Mir as Mir +import qualified What4.Expr as W4 +import qualified What4.Interface as W4 +import qualified What4.Partial as W4 +import qualified What4.ProgramLoc as W4 + +import Verifier.SAW.Prelude (scEq) +import Verifier.SAW.SharedTerm +import Verifier.SAW.Simulator.What4.ReturnTrip (saw_ctx, toSC) +import Verifier.SAW.TypedAST +import Verifier.SAW.TypedTerm + +import SAWScript.Crucible.Common +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..)) +import qualified SAWScript.Crucible.Common.Override as Ov (getSymInterface) +import SAWScript.Crucible.Common.Override hiding (getSymInterface) +import SAWScript.Crucible.MIR.MethodSpecIR +import SAWScript.Crucible.MIR.ResolveSetupValue +import SAWScript.Crucible.MIR.TypeShape +import SAWScript.Options +import SAWScript.Panic +import SAWScript.Utils (handleException) + +-- A few convenient synonyms +type SetupValue = MS.SetupValue MIR +type CrucibleMethodSpecIR = MS.CrucibleMethodSpecIR MIR +type StateSpec = MS.StateSpec MIR +type SetupCondition = MS.SetupCondition MIR + +assertTermEqualities :: + SharedContext -> + MIRCrucibleContext -> + OverrideMatcher MIR md () +assertTermEqualities sc cc = do + let assertTermEquality (t, md, e) = do + p <- instantiateExtResolveSAWPred sc cc t + addAssert p md e + traverse_ assertTermEquality =<< OM (use termEqs) + +-- | Assign the given reference value to the given allocation index in +-- the current substitution. If there is already a binding for this +-- index, then add a reference-equality constraint. +assignVar :: + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + MS.ConditionMetadata -> + AllocIndex {- ^ variable index -} -> + Some (MirPointer Sym) {- ^ concrete value -} -> + OverrideMatcher MIR w () + +assignVar cc md var sref@(Some ref) = + do old <- OM (setupValueSub . at var <<.= Just sref) + let loc = MS.conditionLoc md + for_ old $ \(Some ref') -> + do p <- liftIO (equalRefsPred cc ref ref') + addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError "equality of aliased references" "")) + +assignTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + MS.ConditionMetadata -> + MS.PrePost -> + VarIndex {- ^ external constant index -} -> + Term {- ^ value -} -> + OverrideMatcher MIR w () + +assignTerm sc cc md prepost var val = + do mb <- OM (use (termSub . at var)) + case mb of + Nothing -> OM (termSub . at var ?= val) + Just old -> + matchTerm sc cc md prepost val old + +decodeMIRVal :: Mir.Collection -> Mir.Ty -> Crucible.AnyValue Sym -> Maybe MIRVal +decodeMIRVal col ty (Crucible.AnyValue repr rv) + | Some shp <- tyToShape col ty + = case W4.testEquality repr (shapeType shp) of + Just Refl -> Just (MIRVal shp rv) + Nothing -> Nothing + +-- | Generate assertions that all of the memory allocations matched by +-- an override's precondition are disjoint. +enforceDisjointness :: + MIRCrucibleContext -> W4.ProgramLoc -> StateSpec -> OverrideMatcher MIR w () +enforceDisjointness cc loc ss = + do let sym = cc^.mccSym + sub <- OM (use setupValueSub) + let mems = Map.elems $ Map.intersectionWith (,) (view MS.csAllocs ss) sub + + let md = MS.ConditionMetadata + { MS.conditionLoc = loc + , MS.conditionTags = mempty + , MS.conditionType = "memory region disjointness" + , MS.conditionContext = "" + } + -- Ensure that all regions are disjoint from each other. + sequence_ + [ do c <- liftIO $ W4.notPred sym =<< equalRefsPred cc p q + addAssert c md a + + | let a = Crucible.SimError loc $ + Crucible.AssertFailureSimError "Memory regions not disjoint" "" + , (_, Some p) : ps <- tails mems + , (_, Some q) <- ps + ] + +instantiateExtResolveSAWPred :: + SharedContext -> + MIRCrucibleContext -> + Term -> + OverrideMatcher MIR md (W4.Pred Sym) +instantiateExtResolveSAWPred sc cc cond = do + sub <- OM (use termSub) + liftIO $ resolveSAWPred cc =<< scInstantiateExt sc sub cond + +-- | Map the given substitution over all 'SetupTerm' constructors in +-- the given 'SetupValue'. +instantiateSetupValue :: + SharedContext -> + Map VarIndex Term -> + SetupValue -> + IO SetupValue +instantiateSetupValue sc s v = + case v of + MS.SetupVar _ -> return v + MS.SetupTerm tt -> MS.SetupTerm <$> doTerm tt + MS.SetupNull empty -> absurd empty + MS.SetupGlobal empty _ -> absurd empty + MS.SetupStruct _ _ _ -> return v + MS.SetupArray _ _ -> return v + MS.SetupElem _ _ _ -> return v + MS.SetupField _ _ _ -> return v + MS.SetupCast empty _ _ -> absurd empty + MS.SetupUnion empty _ _ -> absurd empty + MS.SetupGlobalInitializer empty _ -> absurd empty + where + doTerm (TypedTerm schema t) = TypedTerm schema <$> scInstantiateExt sc s t + +-- learn pre/post condition +learnCond :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + MS.PrePost -> + StateSpec -> + OverrideMatcher MIR w () +learnCond opts sc cc cs prepost ss = + do let loc = cs ^. MS.csLoc + matchPointsTos opts sc cc cs prepost (ss ^. MS.csPointsTos) + traverse_ (learnSetupCondition opts sc cc cs prepost) (ss ^. MS.csConditions) + assertTermEqualities sc cc + enforceDisjointness cc loc ss + enforceCompleteSubstitution loc ss + +-- | Process a "crucible_equal" statement from the precondition +-- section of the CrucibleSetup block. +learnEqual :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + MS.ConditionMetadata -> + MS.PrePost -> + SetupValue {- ^ first value to compare -} -> + SetupValue {- ^ second value to compare -} -> + OverrideMatcher MIR w () +learnEqual opts sc cc spec md prepost v1 v2 = + do val1 <- resolveSetupValueMIR opts cc sc spec v1 + val2 <- resolveSetupValueMIR opts cc sc spec v2 + p <- liftIO (equalValsPred cc val1 val2) + let name = "equality " ++ MS.stateCond prepost + let loc = MS.conditionLoc md + addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError name "")) + +-- | Process a "points_to" statement from the precondition section of +-- the CrucibleSetup block. First, load the value from the address +-- indicated by 'ptr', and then match it against the pattern 'val'. +learnPointsTo :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + MS.PrePost -> + MirPointsTo -> + OverrideMatcher MIR w () +learnPointsTo _opts _sc _cc _spec _prepost _pt = + panic "learnPointsTo" ["not yet implemented"] + +-- | Process a "crucible_precond" statement from the precondition +-- section of the CrucibleSetup block. +learnPred :: + SharedContext -> + MIRCrucibleContext -> + MS.ConditionMetadata -> + MS.PrePost -> + Term {- ^ the precondition to learn -} -> + OverrideMatcher MIR w () +learnPred sc cc md prepost t = + do s <- OM (use termSub) + u <- liftIO $ scInstantiateExt sc s t + p <- liftIO $ resolveBoolTerm (cc ^. mccSym) u + let loc = MS.conditionLoc md + addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) "")) + +-- | Use the current state to learn about variable assignments based on +-- preconditions for a procedure specification. +learnSetupCondition :: + Options -> + SharedContext -> + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + MS.PrePost -> + SetupCondition -> + OverrideMatcher MIR w () +learnSetupCondition opts sc cc spec prepost (MS.SetupCond_Equal md val1 val2) = learnEqual opts sc cc spec md prepost val1 val2 +learnSetupCondition _opts sc cc _ prepost (MS.SetupCond_Pred md tm) = learnPred sc cc md prepost (ttTerm tm) +learnSetupCondition _opts _ _ _ _ (MS.SetupCond_Ghost empty _ _ _) = absurd empty + +-- | Match the value of a function argument with a symbolic 'SetupValue'. +matchArg :: + Options {- ^ saw script print out opts -} -> + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + CrucibleMethodSpecIR {- ^ specification for current function override -} -> + MS.PrePost -> + MS.ConditionMetadata -> + MIRVal {- ^ concrete simulation value -} -> + Mir.Ty {- ^ expected memory type -} -> + SetupValue {- ^ expected specification value -} -> + OverrideMatcher MIR w () + +matchArg opts sc cc cs prepost md actual expectedTy expected@(MS.SetupTerm 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 + realTerm <- valueToSC sym md failMsg tval actual + matchTerm sc cc md prepost realTerm (ttTerm expectedTT) + +matchArg opts sc cc cs _prepost md actual@(MIRVal (RefShape _refTy pointeeTy mutbl tpr) ref) expectedTy setupval = + case setupval of + MS.SetupVar var -> + do assignVar cc md var (Some (MirPointer tpr mutbl pointeeTy ref)) + + MS.SetupNull empty -> absurd empty + MS.SetupGlobal empty _ -> absurd empty + MS.SetupCast empty _ _ -> absurd empty + MS.SetupUnion empty _ _ -> absurd empty + MS.SetupGlobalInitializer empty _ -> absurd empty + + _ -> failure (cs ^. MS.csLoc) =<< + mkStructuralMismatch opts cc sc cs actual setupval expectedTy + +matchArg opts sc cc cs _prepost md actual expectedTy expected = + failure (MS.conditionLoc md) =<< + mkStructuralMismatch opts cc sc cs actual expected expectedTy + +-- | For each points-to statement read the memory value through the +-- given pointer (lhs) and match the value against the given pattern +-- (rhs). Statements are processed in dependency order: a points-to +-- statement cannot be executed until bindings for any/all lhs +-- variables exist. +matchPointsTos :: + Options {- ^ saw script print out opts -} -> + SharedContext {- ^ term construction context -} -> + MIRCrucibleContext {- ^ simulator context -} -> + CrucibleMethodSpecIR -> + MS.PrePost -> + [MirPointsTo] {- ^ points-tos -} -> + OverrideMatcher MIR w () +matchPointsTos opts sc cc spec prepost = go False [] + where + go :: + Bool {- progress indicator -} -> + [MirPointsTo] {- delayed conditions -} -> + [MirPointsTo] {- queued conditions -} -> + OverrideMatcher MIR w () + + -- all conditions processed, success + go _ [] [] = return () + + -- not all conditions processed, no progress, failure + go False delayed [] = failure (spec ^. MS.csLoc) (AmbiguousPointsTos delayed) + + -- not all conditions processed, progress made, resume delayed conditions + go True delayed [] = go False [] delayed + + -- progress the next points-to in the work queue + go progress delayed (c:cs) = + do ready <- checkPointsTo c + if ready then + do learnPointsTo opts sc cc spec prepost c + go True delayed cs + else + do go progress (c:delayed) cs + + -- determine if a precondition is ready to be checked + checkPointsTo :: MirPointsTo -> OverrideMatcher MIR w Bool + checkPointsTo = panic "matchPointsTos" ["not yet implemented"] + +matchTerm :: + SharedContext {- ^ context for constructing SAW terms -} -> + MIRCrucibleContext {- ^ context for interacting with Crucible -} -> + MS.ConditionMetadata -> + MS.PrePost -> + Term {- ^ exported concrete term -} -> + Term {- ^ expected specification term -} -> + OverrideMatcher MIR md () + +matchTerm _ _ _ _ real expect | real == expect = return () +matchTerm sc cc md prepost real expect = + do let loc = MS.conditionLoc md + free <- OM (use osFree) + case unwrapTermF expect of + FTermF (ExtCns ec) + | Set.member (ecVarIndex ec) free -> + do assignTerm sc cc md prepost (ecVarIndex ec) real + + _ -> + do t <- liftIO $ scEq sc real expect + let msg = unlines $ + [ "Literal equality " ++ MS.stateCond prepost +-- , "Expected term: " ++ prettyTerm expect +-- , "Actual term: " ++ prettyTerm real + ] + addTermEq t md $ Crucible.SimError loc $ Crucible.AssertFailureSimError msg "" + +-- | Try to translate the spec\'s 'SetupValue' into a 'MIRVal', pretty-print +-- the 'MIRVal'. +mkStructuralMismatch :: + Options {- ^ output/verbosity options -} -> + MIRCrucibleContext -> + SharedContext {- ^ context for constructing SAW terms -} -> + CrucibleMethodSpecIR {- ^ for name and typing environments -} -> + MIRVal {- ^ the value from the simulator -} -> + SetupValue {- ^ the value from the spec -} -> + Mir.Ty {- ^ the expected type -} -> + OverrideMatcher MIR w (OverrideFailureReason MIR) +mkStructuralMismatch _opts cc _sc spec (MIRVal shp _) setupval mty = do + setupTy <- typeOfSetupValueMIR cc spec setupval + pure $ StructuralMismatch + (PP.pretty shp) -- TODO: Print the entire value, not just the type shape + (MS.ppSetupValue setupval) + (Just setupTy) + mty + +readMaybeType :: + Crucible.IsSymInterface sym + => sym + -> String + -> Crucible.TypeRepr tp + -> Crucible.RegValue sym (Crucible.MaybeType tp) + -> IO (Crucible.RegValue sym tp) +readMaybeType sym desc tpr rv = + case readPartExprMaybe sym rv of + Just x -> return x + Nothing -> error $ "readMaybeType: accessed possibly-uninitialized " ++ desc ++ + " of type " ++ show tpr + +readPartExprMaybe :: + Crucible.IsSymInterface sym + => sym + -> W4.PartExpr (W4.Pred sym) a + -> Maybe a +readPartExprMaybe _sym W4.Unassigned = Nothing +readPartExprMaybe _sym (W4.PE p v) + | Just True <- W4.asConstantPred p = Just v + | otherwise = Nothing + +resolveSetupValueMIR :: + Options -> + MIRCrucibleContext -> + SharedContext -> + CrucibleMethodSpecIR -> + SetupValue -> + OverrideMatcher MIR w MIRVal +resolveSetupValueMIR opts cc sc spec sval = + do m <- OM (use setupValueSub) + s <- OM (use termSub) + let tyenv = MS.csAllocations spec + nameEnv = MS.csTypeNames spec + sval' <- liftIO $ instantiateSetupValue sc s sval + liftIO $ resolveSetupVal cc m tyenv nameEnv sval' `X.catch` handleException opts + +typeOfSetupValueMIR :: + MIRCrucibleContext -> + CrucibleMethodSpecIR -> + SetupValue -> + OverrideMatcher MIR w Mir.Ty +typeOfSetupValueMIR cc spec sval = + do let tyenv = MS.csAllocations spec + nameEnv = MS.csTypeNames spec + liftIO $ typeOfSetupValue cc tyenv nameEnv sval + +valueToSC :: + Sym -> + MS.ConditionMetadata -> + OverrideFailureReason MIR -> + Cryptol.TValue -> + MIRVal -> + OverrideMatcher MIR w Term +valueToSC sym md failMsg tval (MIRVal shp val) = + case (tval, shp) of + (Cryptol.TVBit, PrimShape _ W4.BaseBoolRepr) -> + liftIO (toSC sym st val) + (Cryptol.TVSeq n Cryptol.TVBit, PrimShape _ (W4.BaseBVRepr w)) + | n == 8, Just _ <- W4.testEquality w (W4.knownNat @8) + -> liftIO (toSC sym st val) + | n == 16, Just _ <- W4.testEquality w (W4.knownNat @16) + -> liftIO (toSC sym st val) + | n == 32, Just _ <- W4.testEquality w (W4.knownNat @32) + -> liftIO (toSC sym st val) + | n == 64, Just _ <- W4.testEquality w (W4.knownNat @64) + -> liftIO (toSC sym st val) + | n == 128, Just _ <- W4.testEquality w (W4.knownNat @128) + -> liftIO (toSC sym st val) + (Cryptol.TVTuple [], UnitShape _) -> + liftIO (scUnitValue sc) + (Cryptol.TVTuple tys, TupleShape _ _ flds) + | length tys == Ctx.sizeInt (Ctx.size flds) + -> do terms <- + traverse + fieldToSC + (zip tys (FC.toListFC Some (Ctx.zipWith Functor.Pair flds val))) + liftIO (scTupleReduced sc terms) + (Cryptol.TVSeq n cryty, ArrayShape _ _ arrShp) + | Mir.MirVector_Vector vals <- val + , toInteger (V.length vals) == n + -> do terms <- V.toList <$> + traverse (\v -> valueToSC sym md failMsg cryty (MIRVal arrShp v)) vals + t <- shapeToTerm sc arrShp + liftIO (scVectorReduced sc t terms) + | Mir.MirVector_PartialVector vals <- val + , toInteger (V.length vals) == n + -> do vals' <- liftIO $ V.toList <$> + traverse (readMaybeType sym "vector element" (shapeType arrShp)) vals + terms <- + traverse (\v -> valueToSC sym md failMsg cryty (MIRVal arrShp v)) vals' + t <- shapeToTerm sc arrShp + liftIO (scVectorReduced sc t terms) + | Mir.MirVector_Array{} <- val + -> fail "valueToSC: Symbolic arrays not supported" + _ -> + failure (MS.conditionLoc md) failMsg + where + st = sym ^. W4.userState + sc = saw_ctx st + + fieldToSC :: + (Cryptol.TValue, Some (Functor.Product FieldShape (Crucible.RegValue' Sym))) + -> OverrideMatcher MIR w Term + fieldToSC (ty, Some (Functor.Pair fldShp (Crucible.RV tm))) = do + mirVal <- + case fldShp of + ReqField shp' -> + pure $ MIRVal shp' tm + OptField shp' -> do + tm' <- liftIO $ readMaybeType sym "field" (shapeType shp') tm + pure $ MIRVal shp' tm' + valueToSC sym md failMsg ty mirVal diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs new file mode 100644 index 0000000000..e1327ae6c5 --- /dev/null +++ b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs @@ -0,0 +1,397 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +-- | Turns 'SetupValue's back into 'MIRVal's. +module SAWScript.Crucible.MIR.ResolveSetupValue + ( MIRVal(..) + , resolveSetupVal + , typeOfSetupValue + , lookupAllocIndex + , toMIRType + , resolveTypedTerm + , resolveBoolTerm + , resolveSAWPred + , equalRefsPred + , equalValsPred + , MIRTypeOfError(..) + ) where + +import Control.Lens +import Control.Monad (zipWithM) +import qualified Control.Monad.Catch as X +import qualified Data.BitVector.Sized as BV +import qualified Data.Functor.Product as Functor +import Data.Map (Map) +import qualified Data.Map as Map +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Some (Some(..)) +import Data.Text (Text) +import qualified Data.Vector as V +import Data.Vector (Vector) +import Data.Void (absurd) + +import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType) +import qualified Cryptol.TypeCheck.AST as Cryptol (Type, Schema(..)) +import qualified Cryptol.Utils.PP as Cryptol (pp) +import Lang.Crucible.Simulator (RegValue, RegValue'(..)) +import qualified Mir.Generator as Mir +import qualified Mir.Intrinsics as Mir +import Mir.Intrinsics (MIR) +import qualified Mir.Mir as Mir + +import qualified What4.BaseTypes as W4 +import qualified What4.Interface as W4 +import qualified What4.Partial as W4 + +import Verifier.SAW.Cryptol (importType, emptyEnv) +import Verifier.SAW.SharedTerm +import qualified Verifier.SAW.Prim as Prim +import qualified Verifier.SAW.Simulator.Concrete as Concrete +import Verifier.SAW.Simulator.What4.ReturnTrip +import Verifier.SAW.TypedTerm + +import SAWScript.Crucible.Common +import qualified SAWScript.Crucible.Common.MethodSpec as MS +import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..)) +import SAWScript.Crucible.Common.ResolveSetupValue (resolveBoolTerm) +import SAWScript.Crucible.MIR.MethodSpecIR +import SAWScript.Crucible.MIR.TypeShape +import SAWScript.Panic + +-- | A pair of a simulation-time MIR value ('RegValue') and its corresponding +-- type ('TypeShape'), where the @tp@ type parameter is closed over +-- existentially. SAW's MIR backend passes around 'MIRVal's at simulation time. +data MIRVal where + MIRVal :: TypeShape tp -> RegValue Sym tp -> MIRVal + +type SetupValue = MS.SetupValue MIR + +data MIRTypeOfError + = MIRPolymorphicType Cryptol.Schema + | MIRNonRepresentableType Cryptol.Type ToMIRTypeErr + | MIRInvalidTypedTerm TypedTermType + +instance Show MIRTypeOfError where + show (MIRPolymorphicType s) = + unlines + [ "Expected monomorphic term" + , "instead got:" + , show (Cryptol.pp s) + ] + show (MIRNonRepresentableType ty err) = + unlines + [ "Type not representable in MIR:" + , show (Cryptol.pp ty) + , toMIRTypeErrToString err + ] + show (MIRInvalidTypedTerm tp) = + unlines + [ "Expected typed term with Cryptol-representable type, but got" + , show (MS.ppTypedTermType tp) + ] + +instance X.Exception MIRTypeOfError + +typeOfSetupValue :: + X.MonadThrow m => + MIRCrucibleContext -> + Map AllocIndex (Some MirAllocSpec) -> + Map AllocIndex Text -> + SetupValue -> + m Mir.Ty +typeOfSetupValue _mcc env _nameEnv val = + case val of + MS.SetupVar i -> + case Map.lookup i env of + Nothing -> panic "MIRSetup" ["typeOfSetupValue", "Unresolved prestate variable:" ++ show i] + Just (Some alloc) -> + return $ Mir.TyRef (alloc^.maMirType) (alloc^.maMutbl) + MS.SetupTerm tt -> + case ttType tt of + TypedTermSchema (Cryptol.Forall [] [] ty) -> + case toMIRType (Cryptol.evalValType mempty ty) of + Left err -> X.throwM (MIRNonRepresentableType ty err) + Right mirTy -> return mirTy + TypedTermSchema s -> X.throwM (MIRPolymorphicType s) + tp -> X.throwM (MIRInvalidTypedTerm tp) + + MS.SetupNull empty -> absurd empty + MS.SetupGlobal empty _ -> absurd empty + MS.SetupStruct _ _ _ -> panic "typeOfSetupValue" ["structs not yet implemented"] + MS.SetupArray _ _ -> panic "typeOfSetupValue" ["arrays not yet implemented"] + MS.SetupElem _ _ _ -> panic "typeOfSetupValue" ["elems not yet implemented"] + MS.SetupField _ _ _ -> panic "typeOfSetupValue" ["fields not yet implemented"] + MS.SetupCast empty _ _ -> absurd empty + MS.SetupUnion empty _ _ -> absurd empty + MS.SetupGlobalInitializer empty _ -> absurd empty + +lookupAllocIndex :: Map AllocIndex a -> AllocIndex -> a +lookupAllocIndex env i = + case Map.lookup i env of + Nothing -> panic "MIRSetup" ["Unresolved prestate variable:" ++ show i] + Just x -> x + +-- | Translate a SetupValue into a Crucible MIR value, resolving +-- references +resolveSetupVal :: + MIRCrucibleContext -> + Map AllocIndex (Some (MirPointer Sym)) -> + Map AllocIndex (Some MirAllocSpec) -> + Map AllocIndex Text -> + SetupValue -> + IO MIRVal +resolveSetupVal mcc env tyenv nameEnv val = + case val of + MS.SetupVar i -> do + Some ptr <- pure $ lookupAllocIndex env i + let pointeeType = ptr ^. mpMirType + pure $ MIRVal (RefShape + (Mir.TyRef pointeeType (ptr ^. mpMutbl)) + pointeeType + (ptr ^. mpMutbl) + (ptr ^. mpType)) + (ptr ^. mpRef) + MS.SetupTerm tm -> resolveTypedTerm mcc tm + MS.SetupNull empty -> absurd empty + MS.SetupGlobal empty _ -> absurd empty + MS.SetupStruct _ _ _ -> panic "resolveSetupValue" ["structs not yet implemented"] + MS.SetupArray () [] -> fail "resolveSetupVal: invalid empty array" + MS.SetupArray () vs -> do + vals <- V.mapM (resolveSetupVal mcc env tyenv nameEnv) (V.fromList vs) + + Some (shp :: TypeShape tp) <- + case V.head vals of + MIRVal shp _ -> pure (Some shp) + + let mirTy :: Mir.Ty + mirTy = shapeMirTy shp + + vals' :: Vector (RegValue Sym tp) + vals' = V.map (\(MIRVal shp' val') -> + case W4.testEquality shp shp' of + Just Refl -> val' + Nothing -> error $ unlines + [ "resolveSetupVal: internal error" + , show shp + , show shp' + ]) + vals + return $ MIRVal (ArrayShape (Mir.TyArray mirTy (V.length vals)) mirTy shp) + (Mir.MirVector_Vector vals') + MS.SetupElem _ _ _ -> panic "resolveSetupValue" ["elems not yet implemented"] + MS.SetupField _ _ _ -> panic "resolveSetupValue" ["fields not yet implemented"] + MS.SetupCast empty _ _ -> absurd empty + MS.SetupUnion empty _ _ -> absurd empty + MS.SetupGlobalInitializer empty _ -> absurd empty + +resolveTypedTerm :: + MIRCrucibleContext -> + TypedTerm -> + IO MIRVal +resolveTypedTerm mcc tm = + case ttType tm of + TypedTermSchema (Cryptol.Forall [] [] ty) -> + resolveSAWTerm mcc (Cryptol.evalValType mempty ty) (ttTerm tm) + tp -> fail $ unlines + [ "resolveTypedTerm: expected monomorphic term" + , "but got a term of type" + , show (MS.ppTypedTermType tp) + ] + +resolveSAWPred :: + MIRCrucibleContext -> + Term -> + IO (W4.Pred Sym) +resolveSAWPred cc tm = + do let sym = cc^.mccSym + st <- sawCoreState sym + bindSAWTerm sym st W4.BaseBoolRepr tm + +resolveSAWTerm :: + MIRCrucibleContext -> + Cryptol.TValue -> + Term -> + IO MIRVal +resolveSAWTerm mcc tp tm = + case tp of + Cryptol.TVBit -> + do b <- resolveBoolTerm sym tm + pure $ MIRVal (PrimShape Mir.TyBool W4.BaseBoolRepr) b + Cryptol.TVInteger -> + fail "resolveSAWTerm: unimplemented type Integer (FIXME)" + Cryptol.TVIntMod _ -> + fail "resolveSAWTerm: unimplemented type Z n (FIXME)" + Cryptol.TVFloat{} -> + fail "resolveSAWTerm: unimplemented type Float e p (FIXME)" + Cryptol.TVArray{} -> + fail "resolveSAWTerm: unimplemented type Array a b (FIXME)" + Cryptol.TVRational -> + fail "resolveSAWTerm: unimplemented type Rational (FIXME)" + Cryptol.TVSeq sz Cryptol.TVBit -> + case sz of + 8 -> bv_term Mir.B8 $ W4.knownNat @8 + 16 -> bv_term Mir.B16 $ W4.knownNat @16 + 32 -> bv_term Mir.B32 $ W4.knownNat @32 + 64 -> bv_term Mir.B64 $ W4.knownNat @64 + 128 -> bv_term Mir.B128 $ W4.knownNat @128 + _ -> fail ("Invalid bitvector width: " ++ show sz) + where + bv_term :: forall w. 1 W4.<= w + => Mir.BaseSize -> W4.NatRepr w -> IO MIRVal + bv_term b n = + MIRVal (PrimShape (Mir.TyUint b) (W4.BaseBVRepr n)) <$> + resolveBitvectorTerm sym n tm + Cryptol.TVSeq sz tp' -> do + st <- sawCoreState sym + let sc = saw_ctx st + sz_tm <- scNat sc (fromIntegral sz) + tp_tm <- importType sc emptyEnv (Cryptol.tValTy tp') + case toMIRType tp' of + Left e -> fail ("In resolveSAWTerm: " ++ toMIRTypeErrToString e) + Right mirTy -> do + Some (shp :: TypeShape tp) <- pure $ tyToShape col mirTy + + let sz' = fromInteger sz + + f :: Int -> IO (RegValue Sym tp) + f i = do + i_tm <- scNat sc (fromIntegral i) + tm' <- scAt sc sz_tm tp_tm tm i_tm + MIRVal shp' val <- resolveSAWTerm mcc tp' tm' + Refl <- case W4.testEquality shp shp' of + Just r -> pure r + Nothing -> fail $ unlines + [ "resolveSAWTerm: internal error" + , show shp + , show shp' + ] + pure val + + vals <- V.generateM sz' f + pure $ MIRVal (ArrayShape (Mir.TyArray mirTy sz') mirTy shp) + $ Mir.MirVector_Vector vals + Cryptol.TVStream _tp' -> + fail "resolveSAWTerm: unsupported infinite stream type" + Cryptol.TVTuple tps -> do + st <- sawCoreState sym + let sc = saw_ctx st + tms <- traverse (\i -> scTupleSelector sc tm i (length tps)) [1 .. length tps] + vals <- zipWithM (resolveSAWTerm mcc) tps tms + if null vals + then pure $ MIRVal (UnitShape (Mir.TyTuple [])) () + else do + let mirTys = map (\(MIRVal shp _) -> shapeMirTy shp) vals + let mirTupleTy = Mir.TyTuple mirTys + Some fldAssn <- + pure $ Ctx.fromList $ + map (\(MIRVal shp val) -> + Some $ Functor.Pair (OptField shp) (RV (W4.justPartExpr sym val))) + vals + let (fldShpAssn, valAssn) = Ctx.unzip fldAssn + pure $ MIRVal (TupleShape mirTupleTy mirTys fldShpAssn) valAssn + Cryptol.TVRec _flds -> + fail "resolveSAWTerm: unsupported record type" + Cryptol.TVFun _ _ -> + fail "resolveSAWTerm: unsupported function type" + Cryptol.TVAbstract _ _ -> + fail "resolveSAWTerm: unsupported abstract type" + Cryptol.TVNewtype{} -> + fail "resolveSAWTerm: unsupported newtype" + where + sym = mcc ^. mccSym + col = mcc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection + +resolveBitvectorTerm :: + forall w. + (1 W4.<= w) => + Sym -> + W4.NatRepr w -> + Term -> + IO (W4.SymBV Sym w) +resolveBitvectorTerm sym w tm = + do st <- sawCoreState sym + let sc = saw_ctx st + mx <- case getAllExts tm of + -- concretely evaluate if it is a closed term + [] -> + do modmap <- scGetModuleMap sc + let v = Concrete.evalSharedTerm modmap mempty mempty tm + pure (Just (Prim.unsigned (Concrete.toWord v))) + _ -> return Nothing + case mx of + Just x -> W4.bvLit sym w (BV.mkBV w x) + Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm + +data ToMIRTypeErr = NotYetSupported String | Impossible String + +toMIRTypeErrToString :: ToMIRTypeErr -> String +toMIRTypeErrToString = + \case + NotYetSupported ty -> + unwords [ "SAW doesn't yet support translating Cryptol's" + , ty + , "type(s) into crucible-mir's type system." + ] + Impossible ty -> + unwords [ "User error: It's impossible to store Cryptol" + , ty + , "values in crucible-mir's memory model." + ] + +toMIRType :: + Cryptol.TValue -> + Either ToMIRTypeErr Mir.Ty +toMIRType tp = + case tp of + Cryptol.TVBit -> Right Mir.TyBool + Cryptol.TVInteger -> Left (NotYetSupported "integer") + Cryptol.TVIntMod _ -> Left (Impossible "integer (mod n)") + Cryptol.TVFloat{} -> Left (NotYetSupported "float e p") + Cryptol.TVArray{} -> Left (NotYetSupported "array a b") + Cryptol.TVRational -> Left (NotYetSupported "rational") + Cryptol.TVSeq n Cryptol.TVBit -> + case n of + 8 -> Right $ Mir.TyUint Mir.B8 + 16 -> Right $ Mir.TyUint Mir.B16 + 32 -> Right $ Mir.TyUint Mir.B32 + 64 -> Right $ Mir.TyUint Mir.B64 + 128 -> Right $ Mir.TyUint Mir.B128 + _ -> Left (Impossible ("unsupported bitvector size: " ++ show n)) + Cryptol.TVSeq n t -> do + t' <- toMIRType t + let n' = fromIntegral n + Right $ Mir.TyArray t' n' + Cryptol.TVStream _tp' -> Left (Impossible "stream") + Cryptol.TVTuple tps -> do + tps' <- traverse toMIRType tps + Right $ Mir.TyTuple tps' + Cryptol.TVRec _flds -> Left (NotYetSupported "record") + Cryptol.TVFun _ _ -> Left (Impossible "function") + Cryptol.TVAbstract _ _ -> Left (Impossible "abstract") + Cryptol.TVNewtype{} -> Left (Impossible "newtype") + +-- | Check if two MIR references are equal. +equalRefsPred :: + MIRCrucibleContext -> + MirPointer Sym tp1 -> + MirPointer Sym tp2 -> + IO (W4.Pred Sym) +equalRefsPred cc mp1 mp2 = + mccWithBackend cc $ \bak -> + let sym = backendGetSym bak in + case W4.testEquality (mp1^.mpType) (mp2^.mpType) of + Nothing -> pure $ W4.falsePred sym + Just Refl -> Mir.mirRef_eqIO bak (mp1^.mpRef) (mp2^.mpRef) + +equalValsPred :: + MIRCrucibleContext -> + MIRVal -> + MIRVal -> + IO (W4.Pred Sym) +equalValsPred = panic "equalValsPred" ["not yet implemented"] diff --git a/src/SAWScript/Crucible/MIR/TypeShape.hs b/src/SAWScript/Crucible/MIR/TypeShape.hs new file mode 100644 index 0000000000..5fed734473 --- /dev/null +++ b/src/SAWScript/Crucible/MIR/TypeShape.hs @@ -0,0 +1,272 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +-- | The 'TypeShape' data type and related utilities. +module SAWScript.Crucible.MIR.TypeShape + ( TypeShape(..) + , FieldShape(..) + , tyToShape + , tyToShapeEq + , shapeType + , fieldShapeType + , shapeMirTy + , fieldShapeMirTy + , shapeToTerm + ) where + +import Control.Lens ((^.), (^..), each) +import Control.Monad.IO.Class (MonadIO(..)) +import Data.Functor.Const (Const(..)) +import qualified Data.Map as Map +import Data.Parameterized.Classes (ShowF) +import Data.Parameterized.Context (pattern Empty, pattern (:>), Assignment) +import Data.Parameterized.Some +import Data.Parameterized.TH.GADT +import Data.Parameterized.TraversableFC +import GHC.Stack (HasCallStack) +import qualified Prettyprinter as PP + +import Lang.Crucible.Types + +import Mir.Intrinsics +import qualified Mir.Mir as M +import Mir.TransTy ( tyListToCtx, tyToRepr, tyToReprCont, canInitialize + , isUnsized, reprTransparentFieldTy ) + +import qualified Verifier.SAW.SharedTerm as SAW + +-- | TypeShape is used to classify MIR `Ty`s and their corresponding +-- CrucibleTypes into a few common cases. We don't use `Ty` directly because +-- there are some `Ty`s that have identical structure (such as TyRef vs. +-- TyRawPtr) or similar enough structure that we'd rather write only one case +-- (such as `u8` vs `i8` vs `i32`, all primitives/BaseTypes). And we don't use +-- TypeRepr directly because it's lacking information in some cases (notably +-- `TyAdt`, which is always AnyRepr, concealing the actual field types of the +-- struct). +-- +-- In each constructor, the first `M.Ty` is the overall MIR type (e.g., for +-- ArrayShape, this is the TyArray type). The overall `TypeRepr tp` isn't +-- stored directly, but can be computed with `shapeType`. +data TypeShape (tp :: CrucibleType) where + UnitShape :: M.Ty -> TypeShape UnitType + PrimShape :: M.Ty -> BaseTypeRepr btp -> TypeShape (BaseToType btp) + TupleShape :: M.Ty -> [M.Ty] -> Assignment FieldShape ctx -> TypeShape (StructType ctx) + ArrayShape :: M.Ty -> M.Ty -> TypeShape tp -> TypeShape (MirVectorType tp) + StructShape :: M.Ty -> [M.Ty] -> Assignment FieldShape ctx -> TypeShape AnyType + TransparentShape :: M.Ty -> TypeShape tp -> TypeShape tp + -- | Note that RefShape contains only a TypeRepr for the pointee type, not + -- a TypeShape. None of our operations need to recurse inside pointers, + -- and also this saves us from some infinite recursion. + RefShape :: M.Ty + -- ^ The reference type + -> M.Ty + -- ^ The pointee type + -> M.Mutability + -- ^ Is the reference mutable or immutable? + -> TypeRepr tp + -- ^ The Crucible representation of the pointee type + -> TypeShape (MirReferenceType tp) + -- | Note that 'FnPtrShape' contains only 'TypeRepr's for the argument and + -- result types, not 'TypeShape's, as none of our operations need to recurse + -- inside them. + FnPtrShape :: M.Ty -> CtxRepr args -> TypeRepr ret + -> TypeShape (FunctionHandleType args ret) + +-- TODO: Improve? +instance PP.Pretty (TypeShape tp) where + pretty = PP.viaShow + +deriving instance Show (TypeShape tp) +instance ShowF TypeShape + +-- | The TypeShape of a struct field, which might have a MaybeType wrapper to +-- allow for partial initialization. +data FieldShape (tp :: CrucibleType) where + OptField :: TypeShape tp -> FieldShape (MaybeType tp) + ReqField :: TypeShape tp -> FieldShape tp + +-- TODO: Improve? +instance PP.Pretty (FieldShape tp) where + pretty = PP.viaShow + +deriving instance Show (FieldShape tp) +instance ShowF FieldShape + +-- | Return the `TypeShape` of `ty`. +-- +-- It is guaranteed that the `tp :: CrucibleType` index of the resulting +-- `TypeShape` matches that returned by `tyToRepr`. +tyToShape :: M.Collection -> M.Ty -> Some TypeShape +tyToShape col = go + where + go :: M.Ty -> Some TypeShape + go ty = case ty of + M.TyBool -> goPrim ty + M.TyChar -> goPrim ty + M.TyInt _ -> goPrim ty + M.TyUint _ -> goPrim ty + M.TyTuple [] -> goUnit ty + M.TyTuple tys -> goTuple ty tys + M.TyClosure tys -> goTuple ty tys + M.TyFnDef _ -> goUnit ty + M.TyArray ty' _ | Some shp <- go ty' -> Some $ ArrayShape ty ty' shp + M.TyAdt nm _ _ -> case Map.lookup nm (col ^. M.adts) of + Just adt | Just ty' <- reprTransparentFieldTy col adt -> + mapSome (TransparentShape ty) $ go ty' + Just (M.Adt _ M.Struct [v] _ _ _ _) -> goStruct ty (v ^.. M.vfields . each . M.fty) + Just (M.Adt _ ak _ _ _ _ _) -> error $ "tyToShape: AdtKind " ++ show ak ++ " NYI" + Nothing -> error $ "tyToShape: bad adt: " ++ show ty + M.TyRef ty' mutbl -> goRef ty ty' mutbl + M.TyRawPtr ty' mutbl -> goRef ty ty' mutbl + M.TyFnPtr sig -> goFnPtr ty sig + _ -> error $ "tyToShape: " ++ show ty ++ " NYI" + + goPrim :: M.Ty -> Some TypeShape + goPrim ty | Some tpr <- tyToRepr col ty, AsBaseType btpr <- asBaseType tpr = + Some $ PrimShape ty btpr + goPrim ty | Some tpr <- tyToRepr col ty = + error $ "tyToShape: type " ++ show ty ++ " produced non-primitive type " ++ show tpr + + goUnit :: M.Ty -> Some TypeShape + goUnit ty = Some $ UnitShape ty + + goTuple :: M.Ty -> [M.Ty] -> Some TypeShape + goTuple ty tys | Some flds <- loop tys Empty = Some $ TupleShape ty tys flds + where + loop :: forall ctx. [M.Ty] -> Assignment FieldShape ctx -> Some (Assignment FieldShape) + loop [] flds = Some flds + loop (ty':tys') flds | Some fld <- go ty' = loop tys' (flds :> OptField fld) + + goStruct :: M.Ty -> [M.Ty] -> Some TypeShape + goStruct ty tys | Some flds <- loop tys Empty = Some $ StructShape ty tys flds + where + loop :: forall ctx. [M.Ty] -> Assignment FieldShape ctx -> Some (Assignment FieldShape) + loop [] flds = Some flds + loop (ty':tys') flds | Some fld <- goField ty' = loop tys' (flds :> fld) + + goField :: M.Ty -> Some FieldShape + goField ty | Some shp <- go ty = case canInitialize col ty of + True -> Some $ ReqField shp + False -> Some $ OptField shp + + goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape + goRef ty ty' mutbl + | M.TySlice slicedTy <- ty' + , Some tpr <- tyToRepr col slicedTy + = Some $ + TupleShape ty [refTy, usizeTy] + (Empty + :> ReqField (RefShape refTy slicedTy mutbl tpr) + :> ReqField (PrimShape usizeTy BaseUsizeRepr)) + | M.TyStr <- ty' + = Some $ + TupleShape ty [refTy, usizeTy] + (Empty + :> ReqField (RefShape refTy (M.TyUint M.B8) mutbl (BVRepr (knownNat @8))) + :> ReqField (PrimShape usizeTy BaseUsizeRepr)) + where + -- We use a ref (of the same mutability as `ty`) when possible, to + -- avoid unnecessary clobbering. + refTy = M.TyRef ty' mutbl + usizeTy = M.TyUint M.USize + goRef ty ty' _ | isUnsized ty' = error $ + "tyToShape: fat pointer " ++ show ty ++ " NYI" + goRef ty ty' mutbl | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' mutbl tpr + + goFnPtr :: M.Ty -> M.FnSig -> Some TypeShape + goFnPtr ty (M.FnSig args ret _abi _spread) = + tyListToCtx col args $ \argsr -> + tyToReprCont col ret $ \retr -> + Some (FnPtrShape ty argsr retr) + +-- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with +-- the same index `tp`. Raises an `error` if the `TypeRepr` doesn't match +-- `tyToRepr ty`. +tyToShapeEq :: HasCallStack => M.Collection -> M.Ty -> TypeRepr tp -> TypeShape tp +tyToShapeEq col ty tpr | Some shp <- tyToShape col ty = + case testEquality (shapeType shp) tpr of + Just Refl -> shp + Nothing -> error $ "tyToShapeEq: type " ++ show ty ++ + " does not have representation " ++ show tpr ++ + " (got " ++ show (shapeType shp) ++ " instead)" + +shapeType :: TypeShape tp -> TypeRepr tp +shapeType = go + where + go :: forall tp. TypeShape tp -> TypeRepr tp + go (UnitShape _) = UnitRepr + go (PrimShape _ btpr) = baseToType btpr + go (TupleShape _ _ flds) = StructRepr $ fmapFC fieldShapeType flds + go (ArrayShape _ _ shp) = MirVectorRepr $ shapeType shp + go (StructShape _ _ _flds) = AnyRepr + go (TransparentShape _ shp) = go shp + go (RefShape _ _ _ tpr) = MirReferenceRepr tpr + go (FnPtrShape _ args ret) = FunctionHandleRepr args ret + +fieldShapeType :: FieldShape tp -> TypeRepr tp +fieldShapeType (ReqField shp) = shapeType shp +fieldShapeType (OptField shp) = MaybeRepr $ shapeType shp + +shapeMirTy :: TypeShape tp -> M.Ty +shapeMirTy (UnitShape ty) = ty +shapeMirTy (PrimShape ty _) = ty +shapeMirTy (TupleShape ty _ _) = ty +shapeMirTy (ArrayShape ty _ _) = ty +shapeMirTy (StructShape ty _ _) = ty +shapeMirTy (TransparentShape ty _) = ty +shapeMirTy (RefShape ty _ _ _) = ty +shapeMirTy (FnPtrShape ty _ _) = ty + +fieldShapeMirTy :: FieldShape tp -> M.Ty +fieldShapeMirTy (ReqField shp) = shapeMirTy shp +fieldShapeMirTy (OptField shp) = shapeMirTy shp + +shapeToTerm :: forall tp m. + (MonadIO m, MonadFail m) => + SAW.SharedContext -> + TypeShape tp -> + m SAW.Term +shapeToTerm sc = go + where + go :: forall tp'. TypeShape tp' -> m SAW.Term + go (UnitShape _) = liftIO $ SAW.scUnitType sc + go (PrimShape _ BaseBoolRepr) = liftIO $ SAW.scBoolType sc + go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w) + go (TupleShape _ _ flds) = do + tys <- toListFC getConst <$> traverseFC (\x -> Const <$> goField x) flds + liftIO $ SAW.scTupleType sc tys + go (ArrayShape (M.TyArray _ n) _ shp) = do + ty <- go shp + n' <- liftIO $ SAW.scNat sc (fromIntegral n) + liftIO $ SAW.scVecType sc n' ty + go shp = fail $ "shapeToTerm: unsupported type " ++ show (shapeType shp) + + goField :: forall tp'. FieldShape tp' -> m SAW.Term + goField (OptField shp) = go shp + goField (ReqField shp) = go shp + +$(pure []) + +instance TestEquality TypeShape where + testEquality = + $(structuralTypeEquality + [t|TypeShape|] + [ (TypeApp (ConType [t|TypeShape|]) AnyType, [|testEquality|]) + , (TypeApp (ConType [t|BaseTypeRepr|]) AnyType, [|testEquality|]) + , (TypeApp (TypeApp (ConType [t|Assignment|]) AnyType) AnyType, [|testEquality|]) + , (TypeApp (ConType [t|TypeRepr|]) AnyType, [|testEquality|]) + , (TypeApp (ConType [t|CtxRepr|]) AnyType, [|testEquality|]) + ]) + +instance TestEquality FieldShape where + testEquality = + $(structuralTypeEquality + [t|FieldShape|] + [ (TypeApp (ConType [t|TypeShape|]) AnyType, [|testEquality|]) + ]) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index b96ddf79b6..758f9d2ba9 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -92,6 +92,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW -- Crucible import qualified Lang.Crucible.JVM as CJ +import Mir.Intrinsics (MIR) import qualified SAWScript.Crucible.Common as CC import qualified SAWScript.Crucible.Common.MethodSpec as CMS import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ @@ -1093,7 +1094,7 @@ primitives = Map.fromList , "caching has yet to actually be used, then the value of the environment" , "variable is ignored." ] - + , prim "clean_solver_cache" "TopLevel ()" (pureVal clean_solver_cache) Current @@ -3195,7 +3196,7 @@ primitives = Map.fromList Current [ "State that the given predicate must hold. Acts as `llvm_precond`" , "or `llvm_postcond` depending on the phase of specification in which" - , "it appears (i.e., before or after `llvm_execute_func`." + , "it appears (i.e., before or after `llvm_execute_func`)." ] , prim "llvm_setup_with_tag" "String -> LLVMSetup () -> LLVMSetup ()" @@ -3763,7 +3764,7 @@ primitives = Map.fromList Current [ "State that the given predicate must hold. Acts as `jvm_precond`" , "or `jvm_postcond` depending on the phase of specification in which" - , "it appears (i.e., before or after `jvm_execute_func`." + , "it appears (i.e., before or after `jvm_execute_func`)." ] , prim "jvm_postcond" "Term -> JVMSetup ()" @@ -3836,11 +3837,212 @@ primitives = Map.fromList --------------------------------------------------------------------- -- Crucible/MIR commands + , prim "mir_alloc" "MIRType -> MIRSetup SetupValue" + (pureVal mir_alloc) + Experimental + [ "Declare that an immutable reference to the given type should be allocated" + , "in a MIR specification. Before `mir_execute_func`, this states that" + , "the function expects the object to be allocated before it runs." + , "After `mir_execute_func`, it states that the function being" + , "verified is expected to perform the allocation." + ] + + , prim "mir_alloc_mut" "MIRType -> MIRSetup SetupValue" + (pureVal mir_alloc_mut) + Experimental + [ "Declare that a mutable reference to the given type should be allocated" + , "in a MIR specification. Before `mir_execute_func`, this states that" + , "the function expects the object to be allocated before it runs." + , "After `mir_execute_func`, it states that the function being" + , "verified is expected to perform the allocation." + ] + + , prim "mir_assert" "Term -> MIRSetup ()" + (pureVal mir_assert) + Experimental + [ "State that the given predicate must hold. Acts as `mir_precond`" + , "or `mir_postcond` depending on the phase of specification in which" + , "it appears (i.e., before or after `mir_execute_func`)." + ] + + , prim "mir_execute_func" "[MIRValue] -> MIRSetup ()" + (pureVal mir_execute_func) + Experimental + [ "Specify the given list of values as the arguments of the method." + , "" + , "The mir_execute_func statement also serves to separate the pre-state" + , "section of the spec (before mir_execute_func) from the post-state" + , "section (after mir_execute_func). The effects of some MIRSetup" + , "statements depend on whether they occur in the pre-state or post-state" + , "section." + ] + + , prim "mir_fresh_var" "String -> MIRType -> MIRSetup Term" + (pureVal mir_fresh_var) + Experimental + [ "Create a fresh symbolic variable for use within a MIR" + , "specification. The name is used only for pretty-printing." + ] + , prim "mir_load_module" "String -> TopLevel MIRModule" (pureVal mir_load_module) Experimental [ "Load a MIR JSON file and return a handle to it." ] + , prim "mir_postcond" "Term -> MIRSetup ()" + (pureVal mir_postcond) + Experimental + [ "State that the given predicate is a post-condition of execution of the" + , "method being verified." + ] + + , prim "mir_precond" "Term -> MIRSetup ()" + (pureVal mir_precond) + Experimental + [ "State that the given predicate is a pre-condition on execution of the" + , "method being verified." + ] + + , prim "mir_return" "MIRValue -> MIRSetup ()" + (pureVal mir_return) + Experimental + [ "Specify the given value as the return value of the method. A" + , "mir_return statement is required if and only if the method" + , "has a non-() return type." ] + + , prim "mir_term" + "Term -> MIRValue" + (pureVal (CMS.SetupTerm :: TypedTerm -> CMS.SetupValue MIR)) + Experimental + [ "Construct a `MIRValue` from a `Term`." ] + + , prim "mir_verify" + "MIRModule -> String -> [MIRSpec] -> Bool -> MIRSetup () -> ProofScript () -> TopLevel MIRSpec" + (pureVal mir_verify) + Experimental + [ "Verify the MIR function named by the second parameter in the module" + , "specified by the first. The third parameter lists the MIRSpec" + , "values returned by previous calls to use as overrides. The fourth (Bool)" + , "parameter enables or disables path satisfiability checking. The fifth" + , "describes how to set up the symbolic execution engine before verification." + , "And the last gives the script to use to prove the validity of the resulting" + , "verification conditions." + ] + + , prim "mir_array" "Int -> MIRType -> MIRType" + (pureVal mir_array) + Experimental + [ "The type of MIR arrays with the given number of elements of the" + , "given type." ] + + , prim "mir_bool" "MIRType" + (pureVal mir_bool) + Experimental + [ "The type of MIR booleans." ] + + , prim "mir_char" "MIRType" + (pureVal mir_char) + Experimental + [ "The type of MIR characters." ] + + , prim "mir_i8" "MIRType" + (pureVal mir_i8) + Experimental + [ "The type of MIR 8-bit signed integers." ] + + , prim "mir_i16" "MIRType" + (pureVal mir_i16) + Experimental + [ "The type of MIR 16-bit signed integers." ] + + , prim "mir_i32" "MIRType" + (pureVal mir_i32) + Experimental + [ "The type of MIR 32-bit signed integers." ] + + , prim "mir_i64" "MIRType" + (pureVal mir_i64) + Experimental + [ "The type of MIR 64-bit signed integers." ] + + , prim "mir_i128" "MIRType" + (pureVal mir_i128) + Experimental + [ "The type of MIR 128-bit signed integers." ] + + , prim "mir_isize" "MIRType" + (pureVal mir_isize) + Experimental + [ "The type of MIR pointer-sized signed integers." ] + + , prim "mir_f32" "MIRType" + (pureVal mir_f32) + Experimental + [ "The type of MIR single-precision floating-point values." ] + + , prim "mir_f64" "MIRType" + (pureVal mir_f64) + Experimental + [ "The type of MIR double-precision floating-point values." ] + + , prim "mir_ref" "MIRType -> MIRType" + (pureVal mir_ref) + Experimental + [ "The type of MIR immutable references." ] + + , prim "mir_ref_mut" "MIRType -> MIRType" + (pureVal mir_ref_mut) + Experimental + [ "The type of MIR mutable references." ] + + , prim "mir_slice" "MIRType -> MIRType" + (pureVal mir_slice) + Experimental + [ "The type of MIR slices, i.e., dynamically sized views into a" + , "contiguous sequence of the given type. Currently, SAW can only" + , "handle references to slices (&[T])." ] + + , prim "mir_str" "MIRType" + (pureVal mir_str) + Experimental + [ "The type of MIR strings, which are a particular kind of slice." + , "Currently, SAW can only handle references to strings (&str)." ] + + , prim "mir_tuple" "[MIRType] -> MIRType" + (pureVal mir_tuple) + Experimental + [ "The type of MIR tuples of the given types." ] + + , prim "mir_u8" "MIRType" + (pureVal mir_u8) + Experimental + [ "The type of MIR 8-bit unsigned integers." ] + + , prim "mir_u16" "MIRType" + (pureVal mir_u16) + Experimental + [ "The type of MIR 16-bit unsigned integers." ] + + , prim "mir_u32" "MIRType" + (pureVal mir_u32) + Experimental + [ "The type of MIR 32-bit unsigned integers." ] + + , prim "mir_u64" "MIRType" + (pureVal mir_u64) + Experimental + [ "The type of MIR 64-bit unsigned integers." ] + + , prim "mir_u128" "MIRType" + (pureVal mir_u128) + Experimental + [ "The type of MIR 128-bit unsigned integers." ] + + , prim "mir_usize" "MIRType" + (pureVal mir_usize) + Experimental + [ "The type of MIR pointer-sized unsigned integers." ] + --------------------------------------------------------------------- , prim "yosys_import" "String -> TopLevel Term" diff --git a/src/SAWScript/Lexer.x b/src/SAWScript/Lexer.x index 23a02cc3f4..11b42f4386 100644 --- a/src/SAWScript/Lexer.x +++ b/src/SAWScript/Lexer.x @@ -41,9 +41,9 @@ $idchar = [$alpha $digit \' \_] $codechar = [$graphic $whitechar] @reservedid = import|and|let|rec|in|do|if|then|else|as|hiding|typedef - |CryptolSetup|JavaSetup|LLVMSetup|ProofScript|TopLevel|CrucibleSetup + |CryptolSetup|JavaSetup|LLVMSetup|MIRSetup|ProofScript|TopLevel|CrucibleSetup |Int|String|Term|Type|Bool|AIG|CFG - |CrucibleMethodSpec|LLVMSpec|JVMMethodSpec|JVMSpec + |CrucibleMethodSpec|LLVMSpec|JVMMethodSpec|JVMSpec|MIRSpec @punct = "," | ";" | "(" | ")" | ":" | "::" | "[" | "]" | "<-" | "->" | "=" | "{" | "}" | "." | "\" diff --git a/src/SAWScript/Parser.y b/src/SAWScript/Parser.y index 6a28a05cee..9494deb1fd 100644 --- a/src/SAWScript/Parser.y +++ b/src/SAWScript/Parser.y @@ -59,6 +59,7 @@ import Control.Exception 'CryptolSetup' { TReserved _ "CryptolSetup" } 'JavaSetup' { TReserved _ "JavaSetup" } 'LLVMSetup' { TReserved _ "LLVMSetup" } + 'MIRSetup' { TReserved _ "MIRSetup" } 'ProofScript' { TReserved _ "ProofScript" } 'TopLevel' { TReserved _ "TopLevel" } 'CrucibleSetup'{ TReserved _ "CrucibleSetup" } @@ -66,6 +67,7 @@ import Control.Exception 'LLVMSpec' { TReserved _ "LLVMSpec" } 'JVMMethodSpec'{ TReserved _ "JVMMethodSpec" } 'JVMSpec' { TReserved _ "JVMSpec" } + 'MIRSpec' { TReserved _ "MIRSpec" } 'Bool' { TReserved _ "Bool" } 'Int' { TReserved _ "Int" } 'String' { TReserved _ "String" } @@ -229,6 +231,7 @@ BaseType :: { Type } | 'LLVMSpec' { LType (getPos $1) tLLVMSpec } | 'JVMMethodSpec' { LType (getPos $1) tJVMSpec } | 'JVMSpec' { LType (getPos $1) tJVMSpec } + | 'MIRSpec' { LType (getPos $1) tMIRSpec } | '(' Type ')' { LType (maxSpan [$1, $3]) $2 } | '(' commas2(Type) ')' { LType (maxSpan [$1, $3]) (tTuple $2) } | '[' Type ']' { LType (maxSpan [$1, $3]) (tArray $2) } @@ -238,6 +241,7 @@ Context :: { Type } : 'CryptolSetup' { tContext CryptolSetup } | 'JavaSetup' { tContext JavaSetup } | 'LLVMSetup' { tContext LLVMSetup } + | 'MIRSetup' { tContext MIRSetup } | 'ProofScript' { tContext ProofScript } | 'TopLevel' { tContext TopLevel } | 'CrucibleSetup' { tContext LLVMSetup } diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index c5b597c687..e890402aac 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -70,6 +70,7 @@ import qualified SAWScript.Crucible.Common.MethodSpec as CMS import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMSLLVM import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible import qualified SAWScript.Crucible.JVM.MethodSpecIR () +import qualified SAWScript.Crucible.MIR.MethodSpecIR () import qualified Lang.JVM.Codebase as JSS import qualified Text.LLVM.AST as LLVM (Type) import qualified Text.LLVM.PP as LLVM (ppType) @@ -116,6 +117,8 @@ import Lang.Crucible.Utils.StateContT import Lang.Crucible.LLVM.ArraySizeProfile import Mir.Generator +import Mir.Intrinsics (MIR) +import qualified Mir.Mir as MIR import What4.ProgramLoc (ProgramLoc(..)) @@ -152,6 +155,10 @@ data Value | VJVMMethodSpec !(CMS.ProvedSpec CJ.JVM) | VJVMSetupValue !(CMS.SetupValue CJ.JVM) ----- + | VMIRSetup !(MIRSetupM Value) + | VMIRMethodSpec !(CMS.ProvedSpec MIR) + | VMIRSetupValue !(CMS.SetupValue MIR) + ----- | VLLVMModuleSkeleton ModuleSkeleton | VLLVMFunctionSkeleton FunctionSkeleton | VLLVMSkeletonState SkeletonState @@ -159,6 +166,7 @@ data Value ----- | VJavaType JavaType | VLLVMType LLVM.Type + | VMIRType MIR.Ty | VCryptolModule CryptolModule | VJavaClass JSS.Class | VLLVMModule (Some CMSLLVM.LLVMModule) @@ -340,6 +348,7 @@ showsPrecValue opts nenv p v = VLLVMFunctionProfile _ -> showString "<>" VJavaType {} -> showString "<>" VLLVMType t -> showString (show (LLVM.ppType t)) + VMIRType t -> showString (show (PP.pretty t)) VCryptolModule m -> showString (showCryptolModule m) VLLVMModule (Some m) -> showString (CMSLLVM.showLLVMModule m) VMIRModule m -> shows (PP.pretty (m^.rmCS^.collection)) @@ -360,6 +369,9 @@ showsPrecValue opts nenv p v = VJVMSetup _ -> showString "<>" VJVMMethodSpec _ -> showString "<>" VJVMSetupValue x -> shows x + VMIRSetup{} -> showString "<>" + VMIRMethodSpec{} -> showString "<>" + VMIRSetupValue x -> shows x where opts' = sawPPOpts opts @@ -876,6 +888,13 @@ type JVMSetup = CrucibleSetup CJ.JVM newtype JVMSetupM a = JVMSetupM { runJVMSetupM :: JVMSetup a } deriving (Applicative, Functor, Monad) +-- + +type MIRSetup = CrucibleSetup MIR + +newtype MIRSetupM a = MIRSetupM { runMIRSetupM :: MIRSetup a } + deriving (Applicative, Functor, Monad) + -- newtype ProofScript a = ProofScript { unProofScript :: ExceptT (SolverStats, CEX) (StateT ProofState TopLevel) a } deriving (Functor, Applicative, Monad) @@ -1040,6 +1059,19 @@ instance FromValue a => FromValue (JVMSetupM a) where runJVMSetupM (fromValue m2) fromValue _ = error "fromValue JVMSetup" +instance IsValue a => IsValue (MIRSetupM a) where + toValue m = VMIRSetup (fmap toValue m) + +instance FromValue a => FromValue (MIRSetupM a) where + fromValue (VMIRSetup m) = fmap fromValue m + fromValue (VReturn v) = return (fromValue v) + fromValue (VBind pos m1 v2) = MIRSetupM $ do + v1 <- underReaderT (underStateT (withPosition pos)) + (runMIRSetupM (fromValue m1)) + m2 <- lift $ lift $ applyValue v2 v1 + runMIRSetupM (fromValue m2) + fromValue _ = error "fromValue MIRSetup" + instance IsValue (CMSLLVM.AllLLVM CMS.SetupValue) where toValue = VLLVMCrucibleSetupValue @@ -1054,6 +1086,13 @@ instance FromValue (CMS.SetupValue CJ.JVM) where fromValue (VJVMSetupValue v) = v fromValue _ = error "fromValue Crucible.SetupValue" +instance IsValue (CMS.SetupValue MIR) where + toValue v = VMIRSetupValue v + +instance FromValue (CMS.SetupValue MIR) where + fromValue (VMIRSetupValue v) = v + fromValue _ = error "fromValue Crucible.SetupValue" + instance IsValue SAW_CFG where toValue t = VCFG t @@ -1075,6 +1114,13 @@ instance FromValue (CMS.ProvedSpec CJ.JVM) where fromValue (VJVMMethodSpec t) = t fromValue _ = error "fromValue ProvedSpec JVM" +instance IsValue (CMS.ProvedSpec MIR) where + toValue t = VMIRMethodSpec t + +instance FromValue (CMS.ProvedSpec MIR) where + fromValue (VMIRMethodSpec t) = t + fromValue _ = error "fromValue ProvedSpec MIR" + instance IsValue ModuleSkeleton where toValue s = VLLVMModuleSkeleton s @@ -1196,6 +1242,13 @@ instance FromValue LLVM.Type where fromValue (VLLVMType t) = t fromValue _ = error "fromValue LLVMType" +instance IsValue MIR.Ty where + toValue t = VMIRType t + +instance FromValue MIR.Ty where + fromValue (VMIRType t) = t + fromValue _ = error "fromValue MIRType" + instance IsValue Uninterp where toValue me = VUninterp me