Merge pull request #1931 from GaloisInc/T1859-mir_struct_value

`mir_find_adt`, `mir_struct_value`, and friends

Author: mergify[bot]

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

@@ -694,9 +694,17 @@ regToSetup bak p eval shp rv = go shp rv
                 go shp rv
             MirVector_Array _ -> error $ "regToSetup: MirVector_Array NYI"
         return $ MS.SetupArray elemTy svs
-    go (StructShape _ _ flds) (AnyValue tpr rvs)
+    go (StructShape tyAdt _ flds) (AnyValue tpr rvs)
       | Just Refl <- testEquality tpr shpTpr =
-        MS.SetupStruct () <$> goFields flds rvs
+        case tyAdt of
+          M.TyAdt adtName _ _ -> do
+            mbAdt <- use $ msbCollection . M.adts . at adtName
+            case mbAdt of
+              Just adt -> MS.SetupStruct adt <$> goFields flds rvs
+              Nothing -> error $ "regToSetup: Could not find ADT named: "
+                              ++ show adtName
+          _ -> error $ "regToSetup: Found non-ADT type for struct: "
+                    ++ show (PP.pretty tyAdt)
       | otherwise = error $ "regToSetup: type error: expected " ++ show shpTpr ++
         ", but got Any wrapping " ++ show tpr
       where shpTpr = StructRepr $ fmapFC fieldShapeType flds

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

@@ -397,7 +397,7 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
             rv <- liftIO $ readMaybeType sym "vector element" (shapeType shp) p
             go shp rv sv
         MirVector_Array _ -> error $ "matchArg: MirVector_Array NYI"
-    go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct () svs)
+    go (StructShape _ _ flds) (AnyValue tpr rvs) (MS.SetupStruct _ svs)
       | Just Refl <- testEquality tpr shpTpr = goFields flds rvs svs
       | otherwise = error $ "matchArg: type error: expected " ++ show shpTpr ++
         ", but got Any wrapping " ++ show tpr

doc/manual/manual.md

@@ -2113,7 +2113,7 @@ implemented include the following:
 
 * MIR specifications that use overrides (i.e., the `[MIRSpec]` argument to
   `mir_verify` must always be the empty list at present)
-* The ability to construct MIR `struct` or `enum` values in specifications
+* The ability to construct MIR `enum` values in specifications
 * The ability to specify the layout of slice values
 
 The `String` supplied as an argument to `mir_verify` is expected to be a
@@ -2229,6 +2229,7 @@ Java types are built up using the following functions:
 
 MIR types are built up using the following functions:
 
+* `mir_adt : MIRAdt -> MIRType`
 * `mir_array : Int -> MIRType -> MIRType`
 * `mir_bool : MIRType`
 * `mir_char : MIRType`
@@ -2627,9 +2628,81 @@ construct compound values:
 * `mir_array_value : MIRType -> [MIRValue] -> MIRValue` constructs an array
   of the given type whose elements consist of the given values. Supplying the
   element type is necessary to support length-0 arrays.
+* `mir_struct_value : MIRAdt -> [MIRValue] -> MIRValue` construct a struct
+  with the given list of values as elements. The `MIRAdt` argument determines
+  what struct type to create.
+
+  See the "Finding MIR alegraic data types" section for more information on how
+  to compute a `MIRAdt` value to pass to `mir_struct_value`.
 * `mir_tuple_value : [MIRValue] -> MIRValue` construct a tuple with the given
   list of values as elements.
 
+### Finding MIR alegraic data types
+
+We collectively refer to MIR `struct`s and `enum`s together as _algebraic data
+types_, or ADTs for short. ADTs have identifiers to tell them apart, and a
+single ADT declaration can give rise to multiple identifiers depending on how
+the declaration is used. For example:
+
+~~~~ .rs
+pub struct S<A, B> {
+    pub x: A,
+    pub y: B,
+}
+
+pub fn f() -> S<u8, u16> {
+    S {
+        x: 1,
+        y: 2,
+    }
+}
+
+pub fn g() -> S<u32, u64> {
+    S {
+        x: 3,
+        y: 4,
+    }
+}
+~~~~
+
+This program as a single `struct` declaration `S`, which is used in the
+functions `f` and `g`. Note that `S`'s declaration is _polymorphic_, as it uses
+type parameters, but the uses of `S` in `f` and `g` are _monomorphic_, as `S`'s
+type parameters are fully instantiated. Each unique, monomorphic instantiation
+of an ADT gives rise to its own identifier. In the example above, this might
+mean that the following identifiers are created when this code is compiled with
+`mir-json`:
+
+* `S<u8, u16>` gives rise to `example/abcd123::S::_adt456`
+* `S<u32, u64>` gives rise to `example/abcd123::S::_adt789`
+
+The suffix `_adt<number>` is autogenerated by `mir-json` and is typically
+difficult for humans to guess. For this reason, we offer a command to look up
+an ADT more easily:
+
+* `mir_find_adt : MIRModule -> String -> [MIRType] -> MIRAdt` consults the
+  given `MIRModule` to find an algebraic data type (`MIRAdt`). It uses the given
+  `String` as an identifier and the given MIRTypes as the types to instantiate
+  the type parameters of the ADT. If such a `MIRAdt` cannot be found in the
+  `MIRModule`, this will raise an error.
+
+Note that the `String` argument to `mir_find_adt` does not need to include the
+`_adt<num>` suffix, as `mir_find_adt` will discover this for you. The `String`
+is expected to adhere to the identifier conventions described in the "Running a
+MIR-based verification" section. For instance, the following two lines will
+look up `S<u8, u16>` and `S<u32, u64>` from the example above as `MIRAdt`s:
+
+~~~~
+m <- mir_load_module "example.linked-mir.json";
+
+s_8_16  <- mir_find_adt m "example::S" [mir_u8,  mir_u16];
+s_32_64 <- mir_find_adt m "example::S" [mir_u32, mir_u64];
+~~~~
+
+The `mir_adt` command (for constructing a struct type) and `mir_struct_value`
+(for constructing a struct value) commands in turn take a `MIRAdt` as an
+argument.
+
 ### Bitfields
 
 SAW has experimental support for specifying `struct`s with bitfields, such as

intTests/test_mir_verify_structs/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/test_mir_verify_structs/test.linked-mir.json

@@ -0,0 +1,66 @@
+pub struct S1 {
+    pub x1: u32,
+    pub y1: u32,
+}
+
+pub fn f1(s: S1) -> S1 {
+    S1 {
+        x1: s.y1.wrapping_add(1),
+        y1: s.x1.wrapping_add(2),
+    }
+}
+
+pub fn g(s: &S1) -> S1 {
+    S1 {
+        x1: s.y1.wrapping_add(1),
+        y1: s.x1.wrapping_add(2),
+    }
+}
+
+pub fn h(s: &mut S1) {
+    let x1 = s.x1;
+    let y1 = s.y1;
+    s.x1 = y1.wrapping_add(1);
+    s.y1 = x1.wrapping_add(2);
+}
+
+// Polymorphism
+
+pub struct S2<A, B> {
+    pub x2: A,
+    pub y2: B,
+}
+
+pub fn f2(s: S2<u32, u32>) -> S2<u32, u32> {
+    S2 {
+        x2: s.y2.wrapping_add(1),
+        y2: s.x2.wrapping_add(2),
+    }
+}
+
+pub struct S3(u32, u32);
+
+pub fn f3(s: S3) -> S3 {
+    match s {
+        S3(x3, y3) => S3(y3.wrapping_add(1), x3.wrapping_add(2)),
+    }
+}
+
+#[repr(transparent)]
+pub struct S4(u32);
+
+pub fn f4(s: S4) -> S4 {
+    match s {
+        S4(x4) => S4(x4.wrapping_add(2)),
+    }
+}
+
+pub struct Foo<A>(A);
+
+pub fn bar<'a>(f1: &'a mut Foo<[u8; 4]>, f2: &'a mut Foo<S2<u32, u32>>) -> &'a mut Foo<S2<u32, u32>> {
+    f1.0[1] = 42;
+    f2.0.x2 = f2.0.y2;
+    f2
+}
+
+pub fn baz(_: Option<S2<u32, u32>>) {}

intTests/test_mir_verify_structs/test.rs

@@ -0,0 +1,155 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+
+let s1_adt = mir_find_adt m "test::S1" [];
+let s2_adt = mir_find_adt m "test::S2" [mir_u32, mir_u32];
+let s3_adt = mir_find_adt m "test::S3" [];
+let s4_adt = mir_find_adt m "test::S4" [];
+
+let foo_adt_1 = mir_find_adt m "test::Foo" [mir_array 4 mir_u8];
+let foo_adt_2 = mir_find_adt m "test::Foo" [mir_adt s2_adt];
+
+let option_adt = mir_find_adt m "core::option::Option" [mir_adt s2_adt];
+
+let f_spec adt = do {
+    x1 <- mir_fresh_var "x1" mir_u32;
+    y1 <- mir_fresh_var "y1" mir_u32;
+    let s = mir_struct_value
+              adt
+              [ mir_term x1
+              , mir_term y1
+              ];
+
+    mir_execute_func [s];
+
+    let s' = mir_struct_value
+              adt
+              [ mir_term {{ y1 + 1 }}
+              , mir_term {{ x1 + 2 }}
+              ];
+    mir_return s';
+};
+
+
+let f1_spec = f_spec s1_adt;
+let f2_spec = f_spec s2_adt;
+let f3_spec = f_spec s3_adt;
+
+let f4_spec = do {
+    x4 <- mir_fresh_var "x4" mir_u32;
+    let s = mir_struct_value s4_adt [mir_term x4];
+
+    mir_execute_func [s];
+
+    let s' = mir_struct_value s4_adt [mir_term {{ x4 + 2 }}];
+    mir_return s';
+};
+
+let g_spec = do {
+    s_ptr <- mir_alloc (mir_adt s1_adt);
+    x1 <- mir_fresh_var "x1" mir_u32;
+    y1 <- mir_fresh_var "y1" mir_u32;
+    let s = mir_struct_value
+              s1_adt
+              [ mir_term x1
+              , mir_term y1
+              ];
+    mir_points_to s_ptr s;
+
+    mir_execute_func [s_ptr];
+
+    let s' = mir_struct_value
+              s1_adt
+              [ mir_term {{ y1 + 1 }}
+              , mir_term {{ x1 + 2 }}
+              ];
+    mir_return s';
+};
+
+let h_spec = do {
+    s_ptr <- mir_alloc_mut (mir_adt s1_adt);
+    x1 <- mir_fresh_var "x1" mir_u32;
+    y1 <- mir_fresh_var "y1" mir_u32;
+    let s = mir_struct_value
+              s1_adt
+              [ mir_term x1
+              , mir_term y1
+              ];
+    mir_points_to s_ptr s;
+
+    mir_execute_func [s_ptr];
+
+    let s' = mir_struct_value
+              s1_adt
+              [ mir_term {{ y1 + 1 }}
+              , mir_term {{ x1 + 2 }}
+              ];
+    mir_points_to s_ptr s';
+};
+
+let bar_spec = do {
+    f1_ptr <- mir_alloc_mut (mir_adt foo_adt_1);
+    f1_arr_val0 <- mir_fresh_var "f1_arr_val0" mir_u8;
+    f1_arr_val1 <- mir_fresh_var "f1_arr_val1" mir_u8;
+    f1_arr_val2 <- mir_fresh_var "f1_arr_val2" mir_u8;
+    f1_arr_val3 <- mir_fresh_var "f1_arr_val3" mir_u8;
+    let f1_arr_val = mir_array_value
+                       mir_u8
+                       [ mir_term f1_arr_val0
+                       , mir_term f1_arr_val1
+                       , mir_term f1_arr_val2
+                       , mir_term f1_arr_val3
+                       ];
+    let f1_foo_val = mir_struct_value foo_adt_1 [f1_arr_val];
+    mir_points_to f1_ptr f1_foo_val;
+
+    f2_ptr <- mir_alloc_mut (mir_adt foo_adt_2);
+    f2_s2_val0 <- mir_fresh_var "f2_s2_val0" mir_u32;
+    f2_s2_val1 <- mir_fresh_var "f2_s2_val1" mir_u32;
+    let f2_s2_val = mir_struct_value
+                      s2_adt
+                      [ mir_term f2_s2_val0
+                      , mir_term f2_s2_val1
+                      ];
+    let f2_foo_val = mir_struct_value foo_adt_2 [f2_s2_val];
+    mir_points_to f2_ptr f2_foo_val;
+
+    mir_execute_func [f1_ptr, f2_ptr];
+
+    let f1_arr_val' = mir_array_value
+                        mir_u8
+                        [ mir_term f1_arr_val0
+                        , mir_term {{ 42 : [8] }}
+                        , mir_term f1_arr_val2
+                        , mir_term f1_arr_val3
+                        ];
+    let f1_foo_val' = mir_struct_value foo_adt_1 [f1_arr_val'];
+    mir_points_to f1_ptr f1_foo_val';
+
+    let f2_s2_val' = mir_struct_value
+                       s2_adt
+                       [ mir_term f2_s2_val1
+                       , mir_term f2_s2_val1
+                       ];
+    let f2_foo_val' = mir_struct_value foo_adt_2 [f2_s2_val'];
+    mir_points_to f2_ptr f2_foo_val';
+
+    mir_return f2_ptr;
+};
+
+mir_verify m "test::f1" [] false f1_spec z3;
+mir_verify m "test::f2" [] false f2_spec z3;
+mir_verify m "test::f3" [] false f3_spec z3;
+mir_verify m "test::f4" [] false f4_spec z3;
+mir_verify m "test::g" [] false g_spec z3;
+mir_verify m "test::h" [] false h_spec z3;
+
+fails (
+  mir_verify m "test::f1" [] false f2_spec z3
+);
+fails (
+  mir_verify m "test::f2" [] false f1_spec z3
+);
+
+mir_verify m "test::bar" [] false bar_spec z3;

intTests/test_mir_verify_structs/test.saw

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

intTests/test_mir_verify_structs/test.sh

@@ -6,6 +6,8 @@
 
   * The `SAW/MIR/load module` command loads a MIR JSON file into SAW.
   * The `SAW/MIR/verify` command performs verification of a MIR function.
+  * The `SAW/MIR/find ADT` command looks up an algebraic data type (ADT) name in
+    a MIR module.
 
   See the [remote API
   documentation](https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/docs/SAW.rst#sawmirload-module-command)
@@ -20,6 +22,9 @@
 * The old `"tuple"` `setup value` has been renamed to `"struct"`. This better
   reflects its intended purpose of representing struct values. There is now a
   new `"tuple"` `setup value` that is only used to represent MIR tuples.
+* The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For
+  MIR verification, this field is required. For LLVM and JVM verification,
+  this field must be `null`, or else an error will be raised.
 
 ## 1.0.0 -- 2023-06-26