From 07db8151eda519db6592e92922acdd986b344582 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 10 Nov 2023 10:02:01 -0800 Subject: [PATCH] Fix interaction between `mir_fresh_expanded_value` and `repr(transparent)` structs Previously, if `mir_fresh_expanded_value` was asked to generate a value whose type was a struct marked `repr(transparent)`, then SAW would produce a value of the underlying type, not the struct type. This fixes the issue by wrapping the underlying value with `SetupStruct`. Fixes #1973. --- intTests/test1973/Makefile | 13 ++++++ intTests/test1973/test.linked-mir.json | 1 + intTests/test1973/test.rs | 6 +++ intTests/test1973/test.saw | 17 ++++++++ intTests/test1973/test.sh | 3 ++ src/SAWScript/Crucible/MIR/Builtins.hs | 59 ++++++++++++++++++++------ 6 files changed, 86 insertions(+), 13 deletions(-) create mode 100644 intTests/test1973/Makefile create mode 100644 intTests/test1973/test.linked-mir.json create mode 100644 intTests/test1973/test.rs create mode 100644 intTests/test1973/test.saw create mode 100755 intTests/test1973/test.sh diff --git a/intTests/test1973/Makefile b/intTests/test1973/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/intTests/test1973/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/test1973/test.linked-mir.json b/intTests/test1973/test.linked-mir.json new file mode 100644 index 0000000000..04ad287941 --- /dev/null +++ b/intTests/test1973/test.linked-mir.json @@ -0,0 +1 @@ +{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::72fda5b91c47396c"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::72fda5b91c47396c"}},"pos":"test.rs:5:5: 5:6","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Ref::72fda5b91c47396c"}},"kind":"Copy"}}}],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Ref::72fda5b91c47396c"}]},"name":"test/0d75de25::f","return_ty":"ty::Ref::72fda5b91c47396c","spread_arg":null}],"adts":[{"kind":{"kind":"Struct"},"name":"test/0d75de25::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/0d75de25::S","orig_substs":[],"repr_transparent":true,"size":1,"variants":[{"ctor_kind":{"kind":"Fn"},"discr":{"index":0,"kind":"Relative"},"discr_value":null,"fields":[{"name":"test/0d75de25::S::0","ty":"ty::u8"}],"inhabited":true,"name":"test/0d75de25::S"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/0d75de25::f","kind":"Item","substs":[]},"name":"test/0d75de25::f"}],"tys":[{"name":"ty::Adt::a8a1a3466e211b44","ty":{"kind":"Adt","name":"test/0d75de25::S::_adtb7803c2264daf0ec[0]","orig_def_id":"test/0d75de25::S","substs":[]}},{"name":"ty::Ref::72fda5b91c47396c","ty":{"kind":"Ref","mutability":{"kind":"Not"},"ty":"ty::Adt::a8a1a3466e211b44"}},{"name":"ty::u8","ty":{"kind":"Uint","uintkind":{"kind":"U8"}}}],"roots":["test/0d75de25::f"]} \ No newline at end of file diff --git a/intTests/test1973/test.rs b/intTests/test1973/test.rs new file mode 100644 index 0000000000..72e32d3d11 --- /dev/null +++ b/intTests/test1973/test.rs @@ -0,0 +1,6 @@ +#[repr(transparent)] +pub struct S(u8); + +pub fn f(s: &S) -> &S { + s +} diff --git a/intTests/test1973/test.saw b/intTests/test1973/test.saw new file mode 100644 index 0000000000..173e71ba4e --- /dev/null +++ b/intTests/test1973/test.saw @@ -0,0 +1,17 @@ +enable_experimental; + +m <- mir_load_module "test.linked-mir.json"; + +s_adt <- mir_find_adt m "test::S" []; + +let f_spec = do { + s_ref <- mir_alloc (mir_adt s_adt); + s <- mir_fresh_expanded_value "s" (mir_adt s_adt); + mir_points_to s_ref s; + + mir_execute_func [s_ref]; + + mir_return s_ref; +}; + +mir_verify m "test::f" [] false f_spec z3; diff --git a/intTests/test1973/test.sh b/intTests/test1973/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test1973/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index 84aaecbc67..9436a31faf 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -282,24 +282,43 @@ constructExpandedSetupValue cc sc = go , show (PP.pretty ty) ] StructShape ty _ fldShps -> + case ty of + Mir.TyAdt adtName _ _ -> + case col ^. Mir.adts . at adtName of + Just adt@(Mir.Adt _ kind _ _ _ _ _) -> + case kind of + Mir.Struct -> do + flds <- goFlds pfx fldShps + pure $ MS.SetupStruct adt flds + _ -> + panic "constructExpandedSetupValue" + [ "Expected struct, encountered " ++ + show kind + ] + Nothing -> + adt_not_found_panic "StructShape" adtName + _ -> + non_adt_type_panic "StructShape" ty + TransparentShape ty shp' -> case ty of Mir.TyAdt adtName _ _ -> do case col ^. Mir.adts . at adtName of - Just adt -> do - flds <- goFlds pfx fldShps - pure $ MS.SetupStruct adt flds + Just adt@(Mir.Adt _ kind _ _ _ _ _) -> + case kind of + Mir.Struct -> do + val <- go pfx shp' + pure $ MS.SetupStruct adt [val] + Mir.Enum{} -> + fail "`repr(transparent)` enums not currently supported" + Mir.Union -> + panic "constructExpandedSetupValue" + [ "Unexpected `repr(transparent)` union:" + , show adtName + ] Nothing -> - panic "constructExpandedSetupValue" - [ "Could not find ADT in StructShape:" - , show adtName - ] + adt_not_found_panic "TransparentShape" adtName _ -> - panic "constructExpandedSetupValue" - [ "StructShape with non-TyAdt type:" - , show (PP.pretty ty) - ] - TransparentShape _ shp' -> - go pfx shp' + non_adt_type_panic "TransparentShape" ty RefShape ty _ _ _ -> X.throwM $ MIRFreshExpandedValueUnsupportedType ty SliceShape ty _ _ _ -> @@ -320,6 +339,20 @@ constructExpandedSetupValue cc sc = go OptField shp' -> go pfx' shp') fldShps + adt_not_found_panic :: String -> Mir.DefId -> a + adt_not_found_panic shapeName adtName = + panic "constructExpandedSetupValue" + [ "Could not find ADT in " ++ shapeName ++ ":" + , show adtName + ] + + non_adt_type_panic :: String -> Mir.Ty -> a + non_adt_type_panic shapeName ty = + panic "constructExpandedSetupValue" + [ shapeName ++ " with non-TyAdt type:" + , show (PP.pretty ty) + ] + -- | Generate a fresh variable term. The name will be used when -- pretty-printing the variable in debug output. mir_fresh_var ::