From 1386790e8f292ef0666210aded7e5ff7e2735baa Mon Sep 17 00:00:00 2001 From: David Holland Date: Wed, 21 Aug 2024 14:55:45 -0400 Subject: [PATCH 1/9] Rearrange the way constant references are handled in crucible-mir. Instead of sending them as blobs with values, mir-json now encodes them as references to static definitions. The values appear as separate bodies as static allocations. The new input kinds "slicebody" and "strbody" are used to ship the bodies in the JSON. Change our internal representation of the input MIR to split the ConstSlice and ConstStr cases accordingly. Kill off the ConstByteStr case as it's no longer needed; byte strings come through as ordinary references now. Adjust the translation step to handle the bodies and references separately. The critical part of this is that it produces globalMirRef instead of constMirRef; this avoids using constMirRef for cases it can't support that lead to "Cannot compare Const_RefRoots". See saw-script #2064. Note that the handling of slice and string slice bodies is probably now the same as the handling for ordinary arrays and could be simplified away. It is also possible that Const_RefRoots can be killed off entirely. One thing at a time though. Requires corresponding update to mir-json. --- crucible-mir/src/Mir/Generator.hs | 2 +- crucible-mir/src/Mir/JSON.hs | 26 +++++---- crucible-mir/src/Mir/Mir.hs | 7 ++- crucible-mir/src/Mir/PP.hs | 7 ++- crucible-mir/src/Mir/Trans.hs | 93 +++++++++++++++++++++++++------ 5 files changed, 99 insertions(+), 36 deletions(-) diff --git a/crucible-mir/src/Mir/Generator.hs b/crucible-mir/src/Mir/Generator.hs index 6fb25f626..e2affecde 100644 --- a/crucible-mir/src/Mir/Generator.hs +++ b/crucible-mir/src/Mir/Generator.hs @@ -167,7 +167,7 @@ data PtrMetadata s = instance Show (PtrMetadata s) where show NoMeta = "NoMeta" - show (SliceMeta _) = "SliceMeta" + show (SliceMeta len) = "SliceMeta " ++ show len --------------------------------------------------------------------------------- diff --git a/crucible-mir/src/Mir/JSON.hs b/crucible-mir/src/Mir/JSON.hs index 3006838c2..d01a5aa25 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -491,23 +491,25 @@ instance FromJSON ConstVal where pure $ ConstFloat $ FloatLit fk (T.unpack val) Just (String "slice") -> do - ConstSlice <$> v .: "elements" + def_id <- v .: "def_id" + len <- v.: "len" + return $ ConstSliceRef def_id len + + Just (String "slicebody") -> + ConstSliceBody <$> v .: "elements" Just (String "str") -> do - val <- v .: "val" - let f sci = case Scientific.toBoundedInteger sci of - Just b -> pure (b :: Word8) - Nothing -> fail $ "cannot read " ++ show sci - bytes <- mapM (withScientific "byte" f) val - return $ ConstStr $ BS.pack bytes + def_id <- v .: "def_id" + len <- v.: "len" + return $ ConstStrRef def_id len - Just (String "bstr") -> do - val <- v .: "val" + Just (String "strbody") -> do + elements <- v .: "elements" let f sci = case Scientific.toBoundedInteger sci of - Just b -> pure (ConstInt $ U8 $ toInteger (b :: Int)) + Just b -> pure (b :: Word8) Nothing -> fail $ "cannot read " ++ show sci - bytes <- mapM (withScientific "byte" f) val - return $ ConstArray $ V.toList bytes + bytes <- mapM (withScientific "byte" f) elements + return $ ConstStrBody $ BS.pack bytes Just (String "struct") -> ConstStruct <$> v .: "fields" diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs index 95b25fff5..2f3d2fb5f 100644 --- a/crucible-mir/src/Mir/Mir.hs +++ b/crucible-mir/src/Mir/Mir.hs @@ -496,9 +496,10 @@ data FloatLit data ConstVal = ConstFloat FloatLit | ConstInt IntLit - | ConstSlice [ConstVal] - | ConstStr B.ByteString - | ConstByteStr B.ByteString + | ConstSliceBody [ConstVal] + | ConstSliceRef DefId Int + | ConstStrBody B.ByteString + | ConstStrRef DefId Int | ConstBool Bool | ConstChar Char | ConstVariant DefId diff --git a/crucible-mir/src/Mir/PP.hs b/crucible-mir/src/Mir/PP.hs index fce38a1ad..f45ec9011 100644 --- a/crucible-mir/src/Mir/PP.hs +++ b/crucible-mir/src/Mir/PP.hs @@ -312,8 +312,8 @@ instance Pretty Substs where instance Pretty ConstVal where pretty (ConstFloat i) = pretty i pretty (ConstInt i) = pretty i - pretty (ConstStr i) = dquotes (viaShow i) - pretty (ConstByteStr i) = viaShow i + pretty (ConstStrBody i) = dquotes (viaShow i) + pretty (ConstStrRef a len) = pretty "&" <> pr_id a <> (viaShow len) pretty (ConstBool i) = pretty i pretty (ConstChar i) = pretty i pretty (ConstVariant i) = pr_id i @@ -328,7 +328,8 @@ instance Pretty ConstVal where pretty (ConstRawPtr a) = pretty a pretty (ConstStruct fs) = pretty "struct" <> list (map pretty fs) pretty (ConstEnum v fs) = pretty "enum" <> list ((pretty "variant" <+> pretty v) : map pretty fs) - pretty (ConstSlice cs) = list (map pretty cs) + pretty (ConstSliceBody cs) = list (map pretty cs) + pretty (ConstSliceRef a len) = pretty "&" <> pr_id a <> (viaShow len) pretty (ConstFnPtr i) = pretty "fn_ptr" <> brackets (pretty i) instance Pretty AggregateKind where diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index 092a2bf63..b744e5201 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -149,7 +149,8 @@ transConstVal _ty (Some (UsizeRepr)) (M.ConstInt i) = return $ MirExp UsizeRepr (S.app $ usizeLit n) transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = return $ MirExp IsizeRepr (S.app $ isizeLit (fromIntegerLit i)) -transConstVal (M.TyRef (M.TySlice ty) _) (Some (MirSliceRepr tpr)) (M.ConstSlice cs) = do + +transConstVal (M.TyArray ty _sz) (Some (MirVectorRepr tpr)) (M.ConstSliceBody cs) = do cs' <- Trav.for cs $ \c -> do MirExp tpr' c' <- transConstVal ty (Some tpr) c Refl <- testEqualityOrFail tpr tpr' $ @@ -157,25 +158,63 @@ transConstVal (M.TyRef (M.TySlice ty) _) (Some (MirSliceRepr tpr)) (M.ConstSlice show tpr ++ ", got " ++ show tpr' pure c' vec <- mirVector_fromVector tpr $ R.App $ E.VectorLit tpr $ V.fromList cs' - vecRef <- constMirRef (MirVectorRepr tpr) vec - ref <- subindexRef tpr vecRef (R.App $ usizeLit 0) - let len = R.App $ usizeLit $ fromIntegral $ length cs - let struct = S.mkStruct - (mirSliceCtxRepr tpr) - (Ctx.Empty Ctx.:> ref Ctx.:> len) - return $ MirExp (MirSliceRepr tpr) struct -transConstVal _ty (Some (MirSliceRepr u8Repr@(C.BVRepr w))) (M.ConstStr bs) + let vec_tpr = MirVectorRepr tpr + return $ MirExp vec_tpr vec +-- +-- This is what we did (instead of returning) before this logic +-- got split into separate body and reference steps. +-- +--vecRef <- constMirRef vec_tpr vec +--ref <- subindexRef tpr vecRef (R.App $ usizeLit 0) +--let len = R.App $ usizeLit $ fromIntegral $ length cs +--let struct = S.mkStruct (mirSliceCtxRepr tpr) (Ctx.Empty Ctx.:> ref Ctx.:> len) +--return $ MirExp (MirSliceRepr tpr) struct +-- +-- Therefore, after looking up the defid, the reference step needs to: +-- * extract the type from the global variable it finds +-- (note that it'll be a MirVectorRepr that it needs to unwrap) +-- * construct a reference to the global variable +-- (with globalMirRef rather than constMirRef, that's the point of +-- all this) +-- * apply subindexRef as above +-- * cons up the length +-- * call mkStruct +-- * cons up the final MirExp +-- +-- staticPlaces does the first four of these actions; addrOfPlace +-- does the last two. Note that addrOfPlace uses mkSlice instead +-- of mkStruct as above, but as far as I can tell it's equivalent. +-- +transConstVal (M.TyRef (M.TySlice _ty) _) (Some (MirSliceRepr tpr)) (M.ConstSliceRef defid len) = do + place <- staticPlaces tpr len defid + addr <- addrOfPlace place + return addr + +transConstVal _ty (Some (MirVectorRepr u8Repr@(C.BVRepr w))) (M.ConstStrBody bs) | Just Refl <- testEquality w (knownNat @8) = do let bytes = map (\b -> R.App (eBVLit (knownNat @8) (toInteger b))) (BS.unpack bs) let vec = R.App $ E.VectorLit u8Repr (V.fromList bytes) mirVec <- mirVector_fromVector u8Repr vec - vecRef <- constMirRef (MirVectorRepr u8Repr) mirVec - ref <- subindexRef u8Repr vecRef (R.App $ usizeLit 0) - let len = R.App $ usizeLit $ fromIntegral $ BS.length bs - let struct = S.mkStruct - knownRepr - (Ctx.Empty Ctx.:> ref Ctx.:> len) - return $ MirExp (MirSliceRepr u8Repr) struct + let vec_tpr = MirVectorRepr u8Repr + return $ MirExp vec_tpr mirVec +-- +-- This is the code from before splitting into separate body and +-- reference steps: +-- +--vecRef <- constMirRef vec_tpr mirVec +--ref <- subindexRef u8Repr vecRef (R.App $ usizeLit 0) +--let len = R.App $ usizeLit $ fromIntegral $ BS.length bs +--let struct = S.mkStruct knownRepr (Ctx.Empty Ctx.:> ref Ctx.:> len) +--return $ MirExp (MirSliceRepr u8Repr) struct +-- +-- which is exactly analogous to the non-string slice case. +-- +transConstVal _ty (Some (MirSliceRepr u8Repr@(C.BVRepr w))) (M.ConstStrRef defid len) + | Just Refl <- testEquality w (knownNat @8) = do + place <- staticPlaces u8Repr len defid + addr <- addrOfPlace place + return addr + transConstVal (M.TyArray ty _sz) (Some (MirVectorRepr tpr)) (M.ConstArray arr) = do arr' <- Trav.for arr $ \e -> do MirExp tpr' e' <- transConstVal ty (Some tpr) e @@ -185,6 +224,7 @@ transConstVal (M.TyArray ty _sz) (Some (MirVectorRepr tpr)) (M.ConstArray arr) = pure e' vec <- mirVector_fromVector tpr $ R.App $ E.VectorLit tpr $ V.fromList arr' return $ MirExp (MirVectorRepr tpr) vec + transConstVal _ty (Some (C.BVRepr w)) (M.ConstChar c) = do let i = toInteger (Char.ord c) return $ MirExp (C.BVRepr w) (S.app $ eBVLit w i) @@ -359,6 +399,26 @@ staticPlace did = do MirPlace (G.globalType gv) <$> globalMirRef gv <*> pure NoMeta Nothing -> mirFail $ "cannot find static variable " ++ fmt did +-- variant of staticPlace for slices +-- tpr is the element type; len is the length +staticPlaces :: HasCallStack => C.TypeRepr tp -> Int -> M.DefId -> MirGenerator h s ret (MirPlace s) +staticPlaces tpr len did = do + sm <- use $ cs.staticMap + case Map.lookup did sm of + Just (StaticVar gv) -> do + let tpr_found = G.globalType gv + Refl <- testEqualityOrFail (MirVectorRepr tpr) tpr_found $ + "staticPlaces: wrong type: expected vector of " ++ + show tpr ++ ", found " ++ show tpr_found + ref <- globalMirRef gv + ref' <- subindexRef tpr ref (R.App $ usizeLit 0) + -- XXX we seem to need to cons up a Crucible Atom (see + -- crucible/src/Lang/Crucible/CFG/Reg.hs) from len to put in here. + --let len' = error "oops" + let len' = R.App $ usizeLit $ fromIntegral len + return $ MirPlace tpr ref' (SliceMeta len') + Nothing -> mirFail $ "cannot find static variable " ++ fmt did + -- NOTE: The return var in the MIR output is always "_0" getReturnExp :: HasCallStack => C.TypeRepr ret -> MirGenerator h s ret (R.Expr MIR s ret) getReturnExp tpr = do @@ -403,7 +463,6 @@ addrOfPlace (MirPlaceDynRef dynRef) = return $ MirExp DynRefRepr dynRef - -- Given two bitvectors, extend the length of the shorter one so that they -- have the same length -- Use the sign of the first bitvector to determine how to sign extend From b7f95f43de4212cc48dc3da6226c250cdb9777b5 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 22 Aug 2024 21:24:27 -0400 Subject: [PATCH 2/9] Simplify previous: ConstSliceBody can just be ConstArray. --- crucible-mir/src/Mir/JSON.hs | 3 ++- crucible-mir/src/Mir/Mir.hs | 1 - crucible-mir/src/Mir/PP.hs | 1 - crucible-mir/src/Mir/Trans.hs | 22 +++++++--------------- 4 files changed, 9 insertions(+), 18 deletions(-) diff --git a/crucible-mir/src/Mir/JSON.hs b/crucible-mir/src/Mir/JSON.hs index d01a5aa25..6ff274b8f 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -495,8 +495,9 @@ instance FromJSON ConstVal where len <- v.: "len" return $ ConstSliceRef def_id len + -- FUTURE: this is the same as "array" and can be removed Just (String "slicebody") -> - ConstSliceBody <$> v .: "elements" + ConstArray <$> v .: "elements" Just (String "str") -> do def_id <- v .: "def_id" diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs index 2f3d2fb5f..ae6c92bee 100644 --- a/crucible-mir/src/Mir/Mir.hs +++ b/crucible-mir/src/Mir/Mir.hs @@ -496,7 +496,6 @@ data FloatLit data ConstVal = ConstFloat FloatLit | ConstInt IntLit - | ConstSliceBody [ConstVal] | ConstSliceRef DefId Int | ConstStrBody B.ByteString | ConstStrRef DefId Int diff --git a/crucible-mir/src/Mir/PP.hs b/crucible-mir/src/Mir/PP.hs index f45ec9011..6b6985694 100644 --- a/crucible-mir/src/Mir/PP.hs +++ b/crucible-mir/src/Mir/PP.hs @@ -328,7 +328,6 @@ instance Pretty ConstVal where pretty (ConstRawPtr a) = pretty a pretty (ConstStruct fs) = pretty "struct" <> list (map pretty fs) pretty (ConstEnum v fs) = pretty "enum" <> list ((pretty "variant" <+> pretty v) : map pretty fs) - pretty (ConstSliceBody cs) = list (map pretty cs) pretty (ConstSliceRef a len) = pretty "&" <> pr_id a <> (viaShow len) pretty (ConstFnPtr i) = pretty "fn_ptr" <> brackets (pretty i) diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index b744e5201..cc6d0e21d 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -150,19 +150,10 @@ transConstVal _ty (Some (UsizeRepr)) (M.ConstInt i) = transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = return $ MirExp IsizeRepr (S.app $ isizeLit (fromIntegerLit i)) -transConstVal (M.TyArray ty _sz) (Some (MirVectorRepr tpr)) (M.ConstSliceBody cs) = do - cs' <- Trav.for cs $ \c -> do - MirExp tpr' c' <- transConstVal ty (Some tpr) c - Refl <- testEqualityOrFail tpr tpr' $ - "transConstVal (ConstSlice): returned wrong type: expected " ++ - show tpr ++ ", got " ++ show tpr' - pure c' - vec <- mirVector_fromVector tpr $ R.App $ E.VectorLit tpr $ V.fromList cs' - let vec_tpr = MirVectorRepr tpr - return $ MirExp vec_tpr vec -- --- This is what we did (instead of returning) before this logic --- got split into separate body and reference steps. +-- Before the slice code got split into separate body and reference steps, +-- it did the following after the code that's equivalent to the ConstArray +-- case (which is where constant slice bodies get handled now): -- --vecRef <- constMirRef vec_tpr vec --ref <- subindexRef tpr vecRef (R.App $ usizeLit 0) @@ -198,8 +189,8 @@ transConstVal _ty (Some (MirVectorRepr u8Repr@(C.BVRepr w))) (M.ConstStrBody bs) let vec_tpr = MirVectorRepr u8Repr return $ MirExp vec_tpr mirVec -- --- This is the code from before splitting into separate body and --- reference steps: +-- This is the rest of the code that was here before the reference and +-- body steps got split: -- --vecRef <- constMirRef vec_tpr mirVec --ref <- subindexRef u8Repr vecRef (R.App $ usizeLit 0) @@ -207,7 +198,8 @@ transConstVal _ty (Some (MirVectorRepr u8Repr@(C.BVRepr w))) (M.ConstStrBody bs) --let struct = S.mkStruct knownRepr (Ctx.Empty Ctx.:> ref Ctx.:> len) --return $ MirExp (MirSliceRepr u8Repr) struct -- --- which is exactly analogous to the non-string slice case. +-- which is exactly analogous to the non-string slice case above, so +-- we can do the same thing. -- transConstVal _ty (Some (MirSliceRepr u8Repr@(C.BVRepr w))) (M.ConstStrRef defid len) | Just Refl <- testEquality w (knownNat @8) = do From 5ad42f85ca440ed1f174c4d73504d27654e16961 Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 22 Aug 2024 21:38:37 -0400 Subject: [PATCH 3/9] Drop the "slicebody" input kind. It's just "array" now. --- crucible-mir/src/Mir/JSON.hs | 4 ---- 1 file changed, 4 deletions(-) diff --git a/crucible-mir/src/Mir/JSON.hs b/crucible-mir/src/Mir/JSON.hs index 6ff274b8f..cc97d1dce 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -495,10 +495,6 @@ instance FromJSON ConstVal where len <- v.: "len" return $ ConstSliceRef def_id len - -- FUTURE: this is the same as "array" and can be removed - Just (String "slicebody") -> - ConstArray <$> v .: "elements" - Just (String "str") -> do def_id <- v .: "def_id" len <- v.: "len" From bca9f81da5688484e4e146eba570f05ce655ed0f Mon Sep 17 00:00:00 2001 From: David Holland Date: Thu, 22 Aug 2024 22:13:53 -0400 Subject: [PATCH 4/9] Typo in comment --- crucible-mir/src/Mir/Trans.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index cc6d0e21d..505d7655e 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -372,7 +372,7 @@ varPlace (M.Var vname _ vty _) = do vi <- typedVarInfo vname tpr r <- case vi of VarReference reg -> G.readReg reg - -- TODO: these cases won't be needed once immutabe ref support is done + -- TODO: these cases won't be needed once immutable ref support is done -- - make them report an error instead VarRegister reg -> do x <- G.readReg reg From d31d869a0e3fed26b1dc555ae8962feeb9e90e28 Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 23 Aug 2024 18:32:34 -0400 Subject: [PATCH 5/9] Conclusion is that ConstStrRef and ConstSliceRef can be the same. Kill off ConstStrRef. --- crucible-mir/src/Mir/JSON.hs | 5 ----- crucible-mir/src/Mir/Mir.hs | 1 - crucible-mir/src/Mir/PP.hs | 1 - crucible-mir/src/Mir/Trans.hs | 20 +------------------- 4 files changed, 1 insertion(+), 26 deletions(-) diff --git a/crucible-mir/src/Mir/JSON.hs b/crucible-mir/src/Mir/JSON.hs index cc97d1dce..8332abebd 100644 --- a/crucible-mir/src/Mir/JSON.hs +++ b/crucible-mir/src/Mir/JSON.hs @@ -495,11 +495,6 @@ instance FromJSON ConstVal where len <- v.: "len" return $ ConstSliceRef def_id len - Just (String "str") -> do - def_id <- v .: "def_id" - len <- v.: "len" - return $ ConstStrRef def_id len - Just (String "strbody") -> do elements <- v .: "elements" let f sci = case Scientific.toBoundedInteger sci of diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs index ae6c92bee..144a93fce 100644 --- a/crucible-mir/src/Mir/Mir.hs +++ b/crucible-mir/src/Mir/Mir.hs @@ -498,7 +498,6 @@ data ConstVal = | ConstInt IntLit | ConstSliceRef DefId Int | ConstStrBody B.ByteString - | ConstStrRef DefId Int | ConstBool Bool | ConstChar Char | ConstVariant DefId diff --git a/crucible-mir/src/Mir/PP.hs b/crucible-mir/src/Mir/PP.hs index 6b6985694..4f40f4b76 100644 --- a/crucible-mir/src/Mir/PP.hs +++ b/crucible-mir/src/Mir/PP.hs @@ -313,7 +313,6 @@ instance Pretty ConstVal where pretty (ConstFloat i) = pretty i pretty (ConstInt i) = pretty i pretty (ConstStrBody i) = dquotes (viaShow i) - pretty (ConstStrRef a len) = pretty "&" <> pr_id a <> (viaShow len) pretty (ConstBool i) = pretty i pretty (ConstChar i) = pretty i pretty (ConstVariant i) = pr_id i diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index 505d7655e..65c2c4153 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -176,7 +176,7 @@ transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = -- does the last two. Note that addrOfPlace uses mkSlice instead -- of mkStruct as above, but as far as I can tell it's equivalent. -- -transConstVal (M.TyRef (M.TySlice _ty) _) (Some (MirSliceRepr tpr)) (M.ConstSliceRef defid len) = do +transConstVal (M.TyRef _ _) (Some (MirSliceRepr tpr)) (M.ConstSliceRef defid len) = do place <- staticPlaces tpr len defid addr <- addrOfPlace place return addr @@ -188,24 +188,6 @@ transConstVal _ty (Some (MirVectorRepr u8Repr@(C.BVRepr w))) (M.ConstStrBody bs) mirVec <- mirVector_fromVector u8Repr vec let vec_tpr = MirVectorRepr u8Repr return $ MirExp vec_tpr mirVec --- --- This is the rest of the code that was here before the reference and --- body steps got split: --- ---vecRef <- constMirRef vec_tpr mirVec ---ref <- subindexRef u8Repr vecRef (R.App $ usizeLit 0) ---let len = R.App $ usizeLit $ fromIntegral $ BS.length bs ---let struct = S.mkStruct knownRepr (Ctx.Empty Ctx.:> ref Ctx.:> len) ---return $ MirExp (MirSliceRepr u8Repr) struct --- --- which is exactly analogous to the non-string slice case above, so --- we can do the same thing. --- -transConstVal _ty (Some (MirSliceRepr u8Repr@(C.BVRepr w))) (M.ConstStrRef defid len) - | Just Refl <- testEquality w (knownNat @8) = do - place <- staticPlaces u8Repr len defid - addr <- addrOfPlace place - return addr transConstVal (M.TyArray ty _sz) (Some (MirVectorRepr tpr)) (M.ConstArray arr) = do arr' <- Trav.for arr $ \e -> do From d4bd0cd0ff03b11e463ef51b795d004c8eaa802e Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 23 Aug 2024 18:36:17 -0400 Subject: [PATCH 6/9] Replace handwritten Show instance with now-equivalent derived one. Pointed out by Ryan Scott --- crucible-mir/src/Mir/Generator.hs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/crucible-mir/src/Mir/Generator.hs b/crucible-mir/src/Mir/Generator.hs index e2affecde..e902543e8 100644 --- a/crucible-mir/src/Mir/Generator.hs +++ b/crucible-mir/src/Mir/Generator.hs @@ -164,10 +164,7 @@ data MirPlace s where data PtrMetadata s = NoMeta | SliceMeta (R.Expr MIR s UsizeType) - -instance Show (PtrMetadata s) where - show NoMeta = "NoMeta" - show (SliceMeta len) = "SliceMeta " ++ show len + deriving Show --------------------------------------------------------------------------------- From 3444637b455edf15c14963403aa69cd2f4192f5e Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 23 Aug 2024 19:21:04 -0400 Subject: [PATCH 7/9] Tidyups from review comments. - don't output rubbish when prettyprinting - clarify some comments - remove obsolete comments - update some names - remove separate binding of vec_tpr in the ConstStrBody case which no longer serves its original illustrative purpose --- crucible-mir/src/Mir/PP.hs | 2 +- crucible-mir/src/Mir/Trans.hs | 21 ++++++++++----------- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/crucible-mir/src/Mir/PP.hs b/crucible-mir/src/Mir/PP.hs index 4f40f4b76..04418970a 100644 --- a/crucible-mir/src/Mir/PP.hs +++ b/crucible-mir/src/Mir/PP.hs @@ -327,7 +327,7 @@ instance Pretty ConstVal where pretty (ConstRawPtr a) = pretty a pretty (ConstStruct fs) = pretty "struct" <> list (map pretty fs) pretty (ConstEnum v fs) = pretty "enum" <> list ((pretty "variant" <+> pretty v) : map pretty fs) - pretty (ConstSliceRef a len) = pretty "&" <> pr_id a <> (viaShow len) + pretty (ConstSliceRef a _len) = pretty "&" <> pr_id a pretty (ConstFnPtr i) = pretty "fn_ptr" <> brackets (pretty i) instance Pretty AggregateKind where diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index 65c2c4153..a38b55bf6 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -155,7 +155,10 @@ transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = -- it did the following after the code that's equivalent to the ConstArray -- case (which is where constant slice bodies get handled now): -- ---vecRef <- constMirRef vec_tpr vec +-- (vec is the vector produced in the ConstArray case and tpr is the type +-- representation of its element type) +-- +--vecRef <- constMirRef (MirVectorRepr tpr) vec --ref <- subindexRef tpr vecRef (R.App $ usizeLit 0) --let len = R.App $ usizeLit $ fromIntegral $ length cs --let struct = S.mkStruct (mirSliceCtxRepr tpr) (Ctx.Empty Ctx.:> ref Ctx.:> len) @@ -172,12 +175,12 @@ transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = -- * call mkStruct -- * cons up the final MirExp -- --- staticPlaces does the first four of these actions; addrOfPlace +-- staticSlicePlace does the first four of these actions; addrOfPlace -- does the last two. Note that addrOfPlace uses mkSlice instead -- of mkStruct as above, but as far as I can tell it's equivalent. -- transConstVal (M.TyRef _ _) (Some (MirSliceRepr tpr)) (M.ConstSliceRef defid len) = do - place <- staticPlaces tpr len defid + place <- staticSlicePlace tpr len defid addr <- addrOfPlace place return addr @@ -186,8 +189,7 @@ transConstVal _ty (Some (MirVectorRepr u8Repr@(C.BVRepr w))) (M.ConstStrBody bs) let bytes = map (\b -> R.App (eBVLit (knownNat @8) (toInteger b))) (BS.unpack bs) let vec = R.App $ E.VectorLit u8Repr (V.fromList bytes) mirVec <- mirVector_fromVector u8Repr vec - let vec_tpr = MirVectorRepr u8Repr - return $ MirExp vec_tpr mirVec + return $ MirExp (MirVectorRepr u8Repr) mirVec transConstVal (M.TyArray ty _sz) (Some (MirVectorRepr tpr)) (M.ConstArray arr) = do arr' <- Trav.for arr $ \e -> do @@ -375,20 +377,17 @@ staticPlace did = do -- variant of staticPlace for slices -- tpr is the element type; len is the length -staticPlaces :: HasCallStack => C.TypeRepr tp -> Int -> M.DefId -> MirGenerator h s ret (MirPlace s) -staticPlaces tpr len did = do +staticSlicePlace :: HasCallStack => C.TypeRepr tp -> Int -> M.DefId -> MirGenerator h s ret (MirPlace s) +staticSlicePlace tpr len did = do sm <- use $ cs.staticMap case Map.lookup did sm of Just (StaticVar gv) -> do let tpr_found = G.globalType gv Refl <- testEqualityOrFail (MirVectorRepr tpr) tpr_found $ - "staticPlaces: wrong type: expected vector of " ++ + "staticSlicePlace: wrong type: expected vector of " ++ show tpr ++ ", found " ++ show tpr_found ref <- globalMirRef gv ref' <- subindexRef tpr ref (R.App $ usizeLit 0) - -- XXX we seem to need to cons up a Crucible Atom (see - -- crucible/src/Lang/Crucible/CFG/Reg.hs) from len to put in here. - --let len' = error "oops" let len' = R.App $ usizeLit $ fromIntegral len return $ MirPlace tpr ref' (SliceMeta len') Nothing -> mirFail $ "cannot find static variable " ++ fmt did From f39206120600597ad2c6de161c6045afe0f2b643 Mon Sep 17 00:00:00 2001 From: David Holland Date: Mon, 26 Aug 2024 16:59:52 -0400 Subject: [PATCH 8/9] Improve some comments per further discussion --- crucible-mir/src/Mir/Mir.hs | 4 ++++ crucible-mir/src/Mir/Trans.hs | 20 ++++---------------- 2 files changed, 8 insertions(+), 16 deletions(-) diff --git a/crucible-mir/src/Mir/Mir.hs b/crucible-mir/src/Mir/Mir.hs index 144a93fce..27b9a953e 100644 --- a/crucible-mir/src/Mir/Mir.hs +++ b/crucible-mir/src/Mir/Mir.hs @@ -496,7 +496,11 @@ data FloatLit data ConstVal = ConstFloat FloatLit | ConstInt IntLit + -- | A reference to a static allocation for a slice (type is `&[T]` or `&str`) + -- The DefId can lead to either a ConstArray or a ConstStrBody. | ConstSliceRef DefId Int + -- | A string body, of type [u8]. Currently only arises from string literals, + -- but might in the future be used for all [u8]s. | ConstStrBody B.ByteString | ConstBool Bool | ConstChar Char diff --git a/crucible-mir/src/Mir/Trans.hs b/crucible-mir/src/Mir/Trans.hs index a38b55bf6..f71d76b3c 100644 --- a/crucible-mir/src/Mir/Trans.hs +++ b/crucible-mir/src/Mir/Trans.hs @@ -151,20 +151,9 @@ transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = return $ MirExp IsizeRepr (S.app $ isizeLit (fromIntegerLit i)) -- --- Before the slice code got split into separate body and reference steps, --- it did the following after the code that's equivalent to the ConstArray --- case (which is where constant slice bodies get handled now): --- --- (vec is the vector produced in the ConstArray case and tpr is the type --- representation of its element type) --- ---vecRef <- constMirRef (MirVectorRepr tpr) vec ---ref <- subindexRef tpr vecRef (R.App $ usizeLit 0) ---let len = R.App $ usizeLit $ fromIntegral $ length cs ---let struct = S.mkStruct (mirSliceCtxRepr tpr) (Ctx.Empty Ctx.:> ref Ctx.:> len) ---return $ MirExp (MirSliceRepr tpr) struct --- --- Therefore, after looking up the defid, the reference step needs to: +-- This code handles slice references, both for ordinary array slices +-- and string slices. (These differ from ordinary references in having +-- a length.) It needs to look up the definition ID, and then: -- * extract the type from the global variable it finds -- (note that it'll be a MirVectorRepr that it needs to unwrap) -- * construct a reference to the global variable @@ -176,8 +165,7 @@ transConstVal _ty (Some (IsizeRepr)) (ConstInt i) = -- * cons up the final MirExp -- -- staticSlicePlace does the first four of these actions; addrOfPlace --- does the last two. Note that addrOfPlace uses mkSlice instead --- of mkStruct as above, but as far as I can tell it's equivalent. +-- does the last two. -- transConstVal (M.TyRef _ _) (Some (MirSliceRepr tpr)) (M.ConstSliceRef defid len) = do place <- staticSlicePlace tpr len defid From 45bdefcab726245379366b364437d9ae68e3d2bc Mon Sep 17 00:00:00 2001 From: David Holland Date: Fri, 23 Aug 2024 19:35:21 -0400 Subject: [PATCH 9/9] Bump mir-json to include the corresponding changes. --- dependencies/mir-json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dependencies/mir-json b/dependencies/mir-json index 64dff1bb5..131980a17 160000 --- a/dependencies/mir-json +++ b/dependencies/mir-json @@ -1 +1 @@ -Subproject commit 64dff1bb538640bf61616e9ac3c2d87e2da8a1ff +Subproject commit 131980a17bb27c2c3c616a1e8bfb4253a528c328