Merge pull request #1974 from GaloisInc/T1973

Fix interaction between `mir_fresh_expanded_value` and `repr(transparent)` structs

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

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"]}

intTests/test1973/test.rs

@@ -0,0 +1,6 @@
+#[repr(transparent)]
+pub struct S(u8);
+
+pub fn f(s: &S) -> &S {
+    s
+}

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;

intTests/test1973/test.sh

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

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 ::