[crux-mir-comp] struct support for munge

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

@@ -326,7 +326,11 @@ munge sym shp rv = do
                     W4.justPartExpr sym <$> go shp rv
                 return $ MirVector_PartialVector pv'
             MirVector_Array _ -> error $ "munge: MirVector_Array NYI"
-        -- TODO: StructShape
+        go (StructShape _ _ flds) (AnyValue tpr rvs)
+            | StructRepr ctx <- tpr
+            , Just Refl <- testEquality (fmapFC fieldShapeType flds) ctx =
+                AnyValue tpr <$> goFields flds rvs
+            | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr
         go (TransparentShape _ shp) rv = go shp rv
         -- TODO: RefShape
         go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI"

crux-mir-comp/test/symb_eval/comp/munge_struct.good

@@ -0,0 +1,3 @@
+test munge_struct/3a1fbbbh::munge_struct_equiv_test[0]: ok
+
+[Crux] Overall status: Valid.

crux-mir-comp/test/symb_eval/comp/munge_struct.rs

@@ -0,0 +1,20 @@
+extern crate crucible;
+use crucible::*;
+use crucible::cryptol::munge;
+
+#[derive(Clone)]
+struct Point{
+    x: u32,
+    y: u32,
+}
+
+fn reflect(p: Point) -> Point {
+    Point{x: p.y, y: p.x}
+}
+
+#[crux_test]
+fn munge_struct_equiv_test() {
+    let (x, y) = <(u32, u32)>::symbolic("p");
+    let p2 = reflect(munge(Point{x, y}));
+    crucible_assert!(p2.x == y);
+}