Draft: Some progress on symbolic enum values

TODO RGS: Investigate why using `mir_fresh_expanded_value` in an override
doesn't work

TODO RGS: Copy over test case to saw-remote-api

Author: RyanGlScott

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

@@ -648,7 +648,7 @@ substMethodSpec sc sm ms = do
     goSetupEnum (MirSetupEnumVariant adt variant discr variantIdx svs) =
       MirSetupEnumVariant adt variant discr variantIdx <$>
       mapM goSetupValue svs
-    goSetupEnum sv@(MirSetupEnumSymbolic _) =
+    goSetupEnum sv@(MirSetupEnumSymbolic _ _ _) =
       return sv
 
     goSetupSlice (MirSetupSliceRaw ref len) =
@@ -749,7 +749,7 @@ regToSetup bak p eval shp rv = go shp rv
         refSV <- go refShp refRV
         lenSV <- go lenShp lenRV
         pure $ MS.SetupSlice $ MirSetupSliceRaw refSV lenSV
-    go (EnumShape _ _ _ _) _ =
+    go (EnumShape _ _ _ _ _) _ =
       error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"

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

@@ -62,7 +62,7 @@ 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 (EnumShape _ _ _ _) _rv =
+    go (EnumShape _ _ _ _ _) _rv =
       error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"
@@ -122,7 +122,7 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
         ref' <- go refShp ref
         len' <- go lenShp len
         pure $ Ctx.Empty Ctx.:> RV ref' Ctx.:> RV len'
-    go (EnumShape _ _ _ _) _rv =
+    go (EnumShape _ _ _ _ _) _rv =
       error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _rv =
         error "Function pointers not currently supported in overrides"

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

@@ -544,7 +544,7 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
         refRV <- go refShp refSV
         lenRV <- go lenShp lenSV
         pure $ Ctx.Empty Ctx.:> RV refRV Ctx.:> RV lenRV
-    go (EnumShape _ _ _ _) _ =
+    go (EnumShape _ _ _ _ _) _ =
       error "Enums not currently supported in overrides"
     go (FnPtrShape _ _ _) _ =
         error "Function pointers not currently supported in overrides"

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

@@ -337,7 +337,7 @@ 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 (EnumShape _ _ _ _) _ =
+        go (EnumShape _ _ _ _ _) _ =
             error "Enums not currently supported in overrides"
         go (FnPtrShape _ _ _) _ =
             error "Function pointers not currently supported in overrides"

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

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"pos":"test.rs:2:11: 2:12","rhs":{"kind":"Discriminant","ty":"ty::isize","val":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"}},"kind":"Move"},"discr_span":"test.rs:3:9: 3:16","kind":"SwitchInt","pos":"test.rs:2:5: 2:12","switch_ty":"ty::isize","targets":["bb1","bb3","bb2"],"values":["0","1"]}},"blockid":"bb0"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:4:17: 4:19","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}}}],"terminator":{"kind":"Goto","pos":"test.rs:4:17: 4:19","target":"bb4"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"kind":"Unreachable","pos":"test.rs:2:11: 2:12"}},"blockid":"bb2"},{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"pos":"test.rs:3:14: 3:15","rhs":{"kind":"Use","usevar":{"data":{"data":[{"kind":"Downcast","variant":1},{"field":0,"kind":"Field","ty":"ty::u32"}],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}},{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"}},"pos":"test.rs:3:20: 3:21","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}},"kind":"Copy"}}}],"terminator":{"kind":"Goto","pos":"test.rs:3:20: 3:21","target":"bb4"}},"blockid":"bb3"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:6:2: 6:2"}},"blockid":"bb4"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::isize"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_3","ty":"ty::u32"}]},"name":"test/b38ac280::f","return_ty":"ty::u32","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:13:7: 13:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Tuple::e93222e871854c41"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::779a68152b60006a"},"kind":"Constant"},"kind":"Call","pos":"test.rs:13:5: 13:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:14:2: 14:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":true,"mut":{"kind":"Not"},"name":"_2","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/b38ac280::gg","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"pos":"test.rs:9:7: 9:8","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Copy"}}}],"terminator":{"args":[{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}},"kind":"Move"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"}},"bb1"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::946bbc4c46985e3c"},"kind":"Constant"},"kind":"Call","pos":"test.rs:9:5: 9:9"}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:2: 10:2"}},"blockid":"bb1"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Not"},"name":"_2","ty":"ty::u32"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_3","ty":"ty::Adt::3fa7c2d95c7fce06"}]},"name":"test/b38ac280::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[{"kind":{"discr_ty":"ty::isize","kind":"Enum"},"name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","orig_substs":["ty::u32"],"repr_transparent":false,"size":8,"variants":[{"ctor_kind":{"kind":"Const"},"discr":{"index":0,"kind":"Relative"},"discr_value":"0","fields":[],"inhabited":true,"name":"core/73237d41::option::Option::None"},{"ctor_kind":{"kind":"Fn"},"discr":{"index":1,"kind":"Relative"},"discr_value":"1","fields":[{"name":"core/73237d41::option::Option::Some::0","ty":"ty::u32"}],"inhabited":true,"name":"core/73237d41::option::Option::Some"}]}],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/b38ac280::f","kind":"Item","substs":[]},"name":"test/b38ac280::f"},{"inst":{"def_id":"test/b38ac280::gg","kind":"Item","substs":[]},"name":"test/b38ac280::gg"},{"inst":{"def_id":"test/b38ac280::g","kind":"Item","substs":[]},"name":"test/b38ac280::g"}],"tys":[{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}},{"name":"ty::Adt::3fa7c2d95c7fce06","ty":{"kind":"Adt","name":"core/73237d41::option::Option::_adtc5e93708b8ca6e2a[0]","orig_def_id":"core/73237d41::option::Option","substs":["ty::u32"]}},{"name":"ty::isize","ty":{"intkind":{"kind":"Isize"},"kind":"Int"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::779a68152b60006a","ty":{"defid":"test/b38ac280::g","kind":"FnDef"}},{"name":"ty::FnDef::946bbc4c46985e3c","ty":{"defid":"test/b38ac280::f","kind":"FnDef"}}],"roots":["test/b38ac280::f","test/b38ac280::g","test/b38ac280::gg"]}

intTests/test_mir_fresh_expanded_value_enum/test.rs

@@ -0,0 +1,14 @@
+pub fn f(x: Option<u32>) -> u32 {
+    match x {
+        Some(x) => x,
+        None => 27,
+    }
+}
+
+pub fn g(x: Option<u32>) {
+    f(x);
+}
+
+pub fn gg(x: Option<u32>) {
+    g(x);
+}

intTests/test_mir_fresh_expanded_value_enum/test.saw

@@ -0,0 +1,44 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+
+let option_u32_adt = mir_find_adt m "core::option::Option" [mir_u32];
+
+let f_none_spec = do {
+  let x = mir_enum_value option_u32_adt "None" [];
+
+  mir_execute_func [x];
+
+  mir_return (mir_term {{ 27 : [32] }});
+};
+
+let f_some_spec = do {
+  ret <- mir_fresh_var "ret" mir_u32;
+  let x = mir_enum_value option_u32_adt "Some" [mir_term ret];
+
+  mir_execute_func [x];
+
+  mir_return (mir_term ret);
+};
+
+let g_spec = do {
+  x <- mir_fresh_expanded_value "x" (mir_adt option_u32_adt);
+
+  mir_execute_func [x];
+};
+
+let gg_spec = do {
+  xx <- mir_fresh_expanded_value "xx" (mir_adt option_u32_adt);
+
+  mir_execute_func [xx];
+};
+
+f_none_ov <- mir_verify m "test::f" [] false f_none_spec z3;
+f_some_ov <- mir_verify m "test::f" [] false f_some_spec z3;
+
+mir_verify m "test::g" [] false g_spec z3;
+g_ov <- mir_verify m "test::g" [f_none_ov, f_some_ov] false g_spec z3;
+
+mir_verify m "test::gg" [] false gg_spec z3;
+// TODO RGS: Investigate why this doesn't work
+// mir_verify m "test::gg" [g_ov] false gg_spec z3;

intTests/test_mir_fresh_expanded_value_enum/test.sh

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

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -267,7 +267,7 @@ ppSetupValue setupval = case setupval of
     ppMirSetupEnum :: MirSetupEnum -> PP.Doc ann
     ppMirSetupEnum (MirSetupEnumVariant _defId variantName _discr _varIdx fields) =
       PP.pretty variantName PP.<+> ppSetupStructDefault fields
-    ppMirSetupEnum (MirSetupEnumSymbolic _defId) =
+    ppMirSetupEnum (MirSetupEnumSymbolic _defId _discr _variants) =
       PP.pretty "<symbolic enum>"
 
     ppMirSetupSlice :: MirSetupSlice -> PP.Doc ann