SV: Improve compilation for complete matches

src/lib/jib_compile.ml

@@ -898,7 +898,7 @@ module Make (C : CONFIG) = struct
           @ on_reached
           @ [idecl l ctyp case_return_id]
           @ List.concat (List.map compile_case cases)
-          @ [imatch_failure l]
+          @ (if Option.is_some (get_attribute "complete" uannot) then [] else [imatch_failure l])
           @ [ilabel finish_match_label],
           (fun clexp -> icopy l clexp (V_id (case_return_id, ctyp))),
           [iclear ctyp case_return_id] @ aval_cleanup

src/lib/smt_exp.ml

@@ -330,6 +330,7 @@ let rec identical x y =
   | Fn (f1, args1), Fn (f2, args2) ->
       String.compare f1 f2 = 0 && List.compare_lengths args1 args2 = 0 && List.for_all2 identical args1 args2
   | Tester (sx, x), Tester (sy, y) -> String.compare sx sy = 0 && identical x y
+  | Ite (ix, tx, ex), Ite (iy, ty, ey) -> identical ix iy && identical tx ty && identical ex ey
   | _ -> false
 
 let simp_eq x y =
@@ -430,6 +431,12 @@ module Simplifier = struct
     | Ite (cond, Ite (cond', x, y), z) when identical y z -> change (Ite (append_to_and cond cond', x, z))
     | _ -> NoChange
 
+  let rule_chain_right_ite =
+    mk_simple_rule __LOC__ @@ function
+    | Ite (cond, Ite (cond', x, y), z) ->
+        change (Ite (Fn ("and", [cond; cond']), x, Ite (Fn ("and", [cond; Fn ("not", [cond'])]), y, z)))
+    | _ -> NoChange
+
   let rule_same_ite =
     mk_simple_rule __LOC__ @@ function
     | Ite (cond, x, y) -> (
@@ -743,8 +750,8 @@ module Simplifier = struct
   let rule_access_ite =
     mk_simple_rule __LOC__ @@ function
     | Field (struct_id, field, Ite (i, t, e)) ->
-        change (Ite (i, Field (struct_id, field, t), Field (struct_id, field, t)))
-    | Unwrap (ctor, b, Ite (i, t, e)) -> change (Ite (i, Unwrap (ctor, b, t), Unwrap (ctor, b, t)))
+        change (Ite (i, Field (struct_id, field, t), Field (struct_id, field, e)))
+    | Unwrap (ctor, b, Ite (i, t, e)) -> change (Ite (i, Unwrap (ctor, b, t), Unwrap (ctor, b, e)))
     | Tester (ctor, Ite (i, t, e)) -> change (Ite (i, Tester (ctor, t), Tester (ctor, e)))
     | Fn ("select", [Ite (i, t, e); ix]) -> change (Ite (i, Fn ("select", [t; ix]), Fn ("select", [e; ix])))
     | _ -> NoChange

test/c/spc_mappings_small.expect

@@ -0,0 +1,3 @@
+ok
+ok
+ok

test/c/spc_mappings_small.sail

@@ -0,0 +1,24 @@
+default Order dec
+
+$include <prelude.sail>
+$include <mapping.sail>
+
+infixl 5 ++
+
+overload operator ++ = concat_str
+
+$[jib_debug]
+function main() -> unit = {
+  match " " {
+    spc() => print_endline("ok"),
+    _ => print_endline("fail 1"),
+  };
+  match "" {
+    spc() => print_endline("fail 2"),
+    _ => print_endline("ok"),
+  };
+  match " not spaces" {
+    spc() => print_endline("fail 3"),
+    _ => print_endline("ok"),
+  };
+}

test/sv/run_tests.py

@@ -15,19 +15,17 @@
 sail = get_sail()
 
 skip_tests = {
-    'all_even_vector_length',
-    'assign_rename_bug',
-    'cheri128_hsb',
-    'for_shadow',
-    'loop_exception',
-    'poly_mapping', # length
-    'poly_mapping2',
-    'read_write_ram',
+    'all_even_vector_length', # loops
+    'assign_rename_bug', # loops
+    'cheri128_hsb', # loops
+    'for_shadow', # loops
+    'loop_exception', # loops
+    'poly_mapping', # bitvector parsing
+    'read_write_ram', # memory
     'real', # reals
     'real_prop', # reals
-    'split', # generic vectors, loops
+    'split', # loops
     'vector_example', # loops
-    'spc_mappings',
     'lib_hex_bits', # bitvector parsing
     'lib_hex_bits_signed', # bitvector parsing
 }