Merge pull request #1891 from GaloisInc/crux-mir-nightly-2023-01-23

`crux-mir-comp`: Support `nightly-2023-01-23`

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -714,6 +714,8 @@ regToSetup bak p eval shp rv = go shp rv
         alloc <- refToAlloc bak p mutbl ty' tpr startRef len
         let offsetSv idx sv = if idx == 0 then sv else MS.SetupElem () sv idx
         return $ offsetSv idx $ MS.SetupVar alloc
+    go (FnPtrShape _ _ _) _ =
+        error "Function pointers not currently supported in overrides"
 
     goFields :: forall ctx. Assignment FieldShape ctx -> Assignment (RegValue' sym) ctx ->
         BuilderT sym t (OverrideSim p sym MIR rtp args ret) [MS.SetupValue MIR]

crucible-mir-comp/src/Mir/Compositional/Clobber.hs

@@ -59,6 +59,8 @@ clobberSymbolic sym loc nameStr 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 (FnPtrShape _ _ _) _rv =
+        error "Function pointers not currently supported in overrides"
     go shp _rv = error $ "clobberSymbolic: " ++ show (shapeType shp) ++ " NYI"
 
     goField :: forall tp. FieldShape tp -> RegValue' sym tp ->
@@ -105,6 +107,8 @@ clobberImmutSymbolic sym loc nameStr 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 (FnPtrShape _ _ _) _rv =
+        error "Function pointers not currently supported in overrides"
 
     goField :: forall tp. FieldShape tp -> RegValue' sym tp ->
         OverrideSim (p sym) sym MIR rtp args ret (RegValue' sym tp)
@@ -133,6 +137,8 @@ freshSymbolic sym loc nameStr shp = go shp
         return expr
     go (ArrayShape (M.TyArray _ len) _ shp) =
         MirVector_Vector <$> V.replicateM len (go shp)
+    go (FnPtrShape _ _ _) =
+        error "Function pointers not currently supported in overrides"
     go shp = error $ "freshSymbolic: " ++ show (shapeType shp) ++ " NYI"
 
 

crucible-mir-comp/src/Mir/Compositional/Convert.hs

@@ -49,7 +49,8 @@ import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW (baseSCType)
 
 import Mir.Intrinsics
 import qualified Mir.Mir as M
-import Mir.TransTy (tyToRepr, canInitialize, isUnsized, reprTransparentFieldTy)
+import Mir.TransTy ( tyListToCtx, tyToRepr, tyToReprCont, canInitialize
+                   , isUnsized, reprTransparentFieldTy )
 
 
 -- | TypeShape is used to classify MIR `Ty`s and their corresponding
@@ -75,6 +76,11 @@ data TypeShape (tp :: CrucibleType) where
     -- 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.
@@ -108,6 +114,7 @@ tyToShape col ty = go ty
             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
@@ -139,10 +146,19 @@ tyToShape col ty = go ty
         False -> Some $ OptField shp
 
     goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape
-    goRef ty (M.TySlice ty') mutbl | Some tpr <- tyToRepr col ty' = Some $
+    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 ty' tpr)
+                :> 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
@@ -155,6 +171,12 @@ tyToShape col ty = go ty
         "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`.
@@ -177,6 +199,7 @@ shapeType shp = go 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
@@ -190,6 +213,7 @@ 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
@@ -536,7 +560,7 @@ shapeToTerm sc shp = go shp
     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 (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

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -407,6 +407,8 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
         goRef refTy tpr ref alloc 0
     go (RefShape refTy _ tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) =
         goRef refTy tpr ref alloc idx
+    go (FnPtrShape _ _ _) _ _ =
+        error "Function pointers not currently supported in overrides"
     go shp _ sv = error $ "matchArg: type error: bad SetupValue " ++
         show (MS.ppSetupValue sv) ++ " for " ++ show (shapeType shp)
 
@@ -528,6 +530,8 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
             Nothing -> error $ "setupToReg: type error: bad reference type for " ++ show alloc ++
                 ": got " ++ show (ptr ^. mpType) ++ " but expected " ++ show tpr
         Nothing -> error $ "setupToReg: no definition for " ++ show alloc
+    go (FnPtrShape _ _ _) _ =
+        error "Function pointers not currently supported in overrides"
     go shp sv = error $ "setupToReg: type error: bad SetupValue for " ++ show (shapeType shp) ++
         ": " ++ show (MS.ppSetupValue sv)
 

crux-mir-comp/DESIGN.md

@@ -19,7 +19,7 @@ fn f(x: (u8, u8)) -> (u8, u8) {
     (x.1, x.0)
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     let x = <(u8, u8)>::symbolic("x");
     crucible_assume!(x.0 > 0);
@@ -45,7 +45,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 

crux-mir-comp/crux-mir-comp.cabal

@@ -21,6 +21,7 @@ library
   default-language: Haskell2010
   build-depends: base >= 4.9 && < 5,
                  text,
+                 extra,
                  crucible,
                  parameterized-utils >= 1.0.8,
                  containers,
@@ -39,6 +40,7 @@ library
   hs-source-dirs: src
   exposed-modules: Mir.Compositional
                    Mir.Cryptol
+  other-modules:   Mir.Compositional.DefId
 
   ghc-options: -Wall -Wno-name-shadowing
 
@@ -104,6 +106,8 @@ test-suite test
                 config-schema,
                 config-value,
                 bytestring,
+                regex-base,
+                regex-posix,
                 utf8-string
 
   default-language: Haskell2010

crux-mir-comp/src/Mir/Compositional.hs

@@ -12,7 +12,6 @@ where
 import Data.Parameterized.Context (pattern Empty, pattern (:>))
 import Data.Parameterized.NatRepr
 import Data.Text (Text)
-import qualified Data.Text as Text
 
 import Lang.Crucible.Backend
 import Lang.Crucible.CFG.Core
@@ -28,6 +27,7 @@ import Mir.Intrinsics
 
 import Mir.Compositional.Builder (builderNew)
 import Mir.Compositional.Clobber (clobberGlobalsOverride)
+import Mir.Compositional.DefId (hasInstPrefix)
 
 
 compositionalOverrides ::
@@ -40,15 +40,15 @@ compositionalOverrides ::
     Maybe (OverrideSim (p sym) sym MIR rtp a r ())
 compositionalOverrides _symOnline cs name cfg
 
-  | (normDefId "crucible::method_spec::raw::builder_new" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "method_spec", "raw", "builder_new"] explodedName
   , Empty <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
     mkOverride' "method_spec_builder_new" MethodSpecBuilderRepr $ do
         msb <- builderNew cs (textId name)
         return $ MethodSpecBuilder msb
 
-  | (normDefId "crucible::method_spec::raw::builder_add_arg" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "method_spec", "raw", "builder_add_arg"] explodedName
   , Empty :> MethodSpecBuilderRepr :> MirReferenceRepr _tpr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -58,7 +58,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbAddArg tpr argRef msb
         return $ MethodSpecBuilder msb'
 
-  | (normDefId "crucible::method_spec::raw::builder_set_return" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "method_spec", "raw", "builder_set_return"] explodedName
   , Empty :> MethodSpecBuilderRepr :> MirReferenceRepr _tpr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -68,7 +68,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbSetReturn tpr argRef msb
         return $ MethodSpecBuilder msb'
 
-  | normDefId "crucible::method_spec::raw::builder_gather_assumes" == name
+  | ["crucible", "method_spec", "raw", "builder_gather_assumes"] == explodedName
   , Empty :> MethodSpecBuilderRepr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -77,7 +77,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbGatherAssumes msb
         return $ MethodSpecBuilder msb'
 
-  | normDefId "crucible::method_spec::raw::builder_gather_asserts" == name
+  | ["crucible", "method_spec", "raw", "builder_gather_asserts"] == explodedName
   , Empty :> MethodSpecBuilderRepr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -86,7 +86,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbGatherAsserts msb
         return $ MethodSpecBuilder msb'
 
-  | normDefId "crucible::method_spec::raw::builder_finish" == name
+  | ["crucible", "method_spec", "raw", "builder_finish"] == explodedName
   , Empty :> MethodSpecBuilderRepr <- cfgArgTypes cfg
   , MethodSpecRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -95,15 +95,15 @@ compositionalOverrides _symOnline cs name cfg
         msbFinish msb
 
 
-  | normDefId "crucible::method_spec::raw::clobber_globals" == name
+  | ["crucible", "method_spec", "raw", "clobber_globals"] == explodedName
   , Empty <- cfgArgTypes cfg
   , UnitRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
     mkOverride' "method_spec_clobber_globals" UnitRepr $ do
         clobberGlobalsOverride cs
 
 
-  | normDefId "crucible::method_spec::raw::spec_pretty_print" == name
+  | ["crucible", "method_spec", "raw", "spec_pretty_print"] == explodedName
   , Empty :> MethodSpecRepr <- cfgArgTypes cfg
   , MirSliceRepr (BVRepr w) <- cfgReturnType cfg
   , Just Refl <- testEquality w (knownNat @8)
@@ -112,7 +112,7 @@ compositionalOverrides _symOnline cs name cfg
         RegMap (Empty :> RegEntry _tpr (MethodSpec ms _)) <- getOverrideArgs
         msPrettyPrint ms
 
-  | normDefId "crucible::method_spec::raw::spec_enable" == name
+  | ["crucible", "method_spec", "raw", "spec_enable"] == explodedName
   , Empty :> MethodSpecRepr <- cfgArgTypes cfg
   , UnitRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -122,4 +122,5 @@ compositionalOverrides _symOnline cs name cfg
 
 
   | otherwise = Nothing
-
+  where
+    explodedName = textIdKey name

crux-mir-comp/src/Mir/Compositional/DefId.hs

@@ -0,0 +1,20 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Mir.Compositional.DefId
+  ( hasInstPrefix
+  ) where
+
+import Data.List.Extra (unsnoc)
+import qualified Data.Text as Text
+import Data.Text (Text)
+
+import Mir.DefId
+
+-- | Check if @edid@ has the same path as @pfxInit@, plus a final path
+-- component that begins with the name @_inst@.
+hasInstPrefix :: [Text] -> ExplodedDefId -> Bool
+hasInstPrefix pfxInit edid =
+  case unsnoc edid of
+    Nothing -> False
+    Just (edidInit, edidLast) ->
+      pfxInit == edidInit &&
+      "_inst" `Text.isPrefixOf` edidLast

crux-mir-comp/src/Mir/Cryptol.hs

@@ -62,6 +62,7 @@ import qualified Verifier.SAW.Recognizer as SAW (asExtCns)
 import qualified Verifier.SAW.TypedTerm as SAW
 
 import Mir.Compositional.Convert
+import Mir.Compositional.DefId (hasInstPrefix)
 
 
 cryptolOverrides ::
@@ -74,7 +75,7 @@ cryptolOverrides ::
     Maybe (OverrideSim (p sym) sym MIR rtp a r ())
 cryptolOverrides _symOnline cs name cfg
 
-  | (normDefId "crucible::cryptol::load" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "cryptol", "load"] explodedName
   , Empty
       :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl))
       :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl))
@@ -90,7 +91,7 @@ cryptolOverrides _symOnline cs name cfg
         RegMap (Empty :> RegEntry _tpr modulePathStr :> RegEntry _tpr' nameStr) <- getOverrideArgs
         cryptolLoad (cs ^. collection) sig (cfgReturnType cfg) modulePathStr nameStr
 
-  | (normDefId "crucible::cryptol::override_" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "cryptol", "override_"] explodedName
   , Empty
       :> UnitRepr
       :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl))
@@ -114,7 +115,7 @@ cryptolOverrides _symOnline cs name cfg
           :> RegEntry _tpr' nameStr) <- getOverrideArgs
         cryptolOverride (cs ^. collection) mh modulePathStr nameStr
 
-  | (normDefId "crucible::cryptol::munge" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "cryptol", "munge"] explodedName
   , Empty :> tpr <- cfgArgTypes cfg
   , tpr' <- cfgReturnType cfg
   , Just Refl <- testEquality tpr tpr'
@@ -131,7 +132,8 @@ cryptolOverrides _symOnline cs name cfg
         liftIO $ munge sym shp rv
 
   | otherwise = Nothing
-
+  where
+    explodedName = textIdKey name
 
 cryptolLoad ::
     forall sym p t st fs rtp a r tp .
@@ -333,6 +335,8 @@ munge sym shp rv = do
                 AnyValue tpr <$> goFields flds rvs
             | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr
         go (TransparentShape _ shp) rv = go shp rv
+        go (FnPtrShape _ _ _) _ =
+            error "Function pointers not currently supported in overrides"
         -- TODO: RefShape
         go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI"