Merge pull request #1904 from GaloisInc/T1859-basic-mir-verify

Prototype `mir_verify` command

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
 

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

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) =

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"
 

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
-