Add a rewrite to remove impossible cases on integer literals

(e.g., for the dual 32/64 bit RISC-V model)
Apply this rewrite in Coq backend.

3 files changed, 41 insertions, 2 deletions

diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml
index 015b615e..c3e00753 100644
--- a/src/constant_propagation.ml
+++ b/src/constant_propagation.ml
@@ -374,7 +374,7 @@ let is_env_inconsistent env ksubsts =
   prove __POS__ env nc_false
 
 
-let const_prop defs ref_vars =
+let const_props defs ref_vars =
   let rec const_prop_exp substs assigns ((E_aux (e,(l,annot))) as exp) =
     (* Functions to treat lists and tuples of subexpressions as possibly
        non-deterministic: that is, we stop making any assumptions about
@@ -822,11 +822,47 @@ let const_prop defs ref_vars =
     let env = Type_check.env_of exp in
     can_match_with_env env exp
 
-in const_prop_exp
+in (const_prop_exp, const_prop_pexp)
 
+let const_prop d r = fst (const_props d r)
+let const_prop_pexp d r = snd (const_props d r)
 
 let referenced_vars exp =
   let open Rewriter in
   fst (fold_exp
          { (compute_exp_alg IdSet.empty IdSet.union) with
            e_ref = (fun id -> IdSet.singleton id, E_ref id) } exp)
+
+(* This is intended to remove impossible cases when a type-level constant has
+   been used to fix a property of the architecture.  In particular, the current
+   version of the RISC-V model uses constructs like
+
+   match (width, sizeof(xlen)) {
+     (BYTE, _)    => ...
+     ...
+     (DOUBLE, 64) => ...
+   };
+
+   and the type checker will replace the sizeof with the literal 32 or 64.  This
+   pass will then remove the DOUBLE case.
+
+   It would be nice to have the full constant propagation above do this kind of
+   thing too...
+*)
+
+let remove_impossible_int_cases _ =
+
+  let must_keep_case exp (Pat_aux ((Pat_exp (p,_) | Pat_when (p,_,_)),_)) =
+    let rec aux (E_aux (exp,_)) (P_aux (p,_)) =
+      match exp, p with
+      | E_tuple exps, P_tup ps -> List.for_all2 aux exps ps
+      | E_lit (L_aux (lit,_)), P_lit (L_aux (lit',_)) -> lit_match (lit, lit')
+      | _ -> true
+    in aux exp p
+  in
+  let rewrite_e_case (exp,cases) =
+    E_case (exp, List.filter (must_keep_case exp) cases)
+  in
+  let open Rewriter in
+  let rewrite_exp _ = fold_exp { id_exp_alg with e_case = rewrite_e_case } in
+  rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp }
diff --git a/src/constant_propagation.mli b/src/constant_propagation.mli
index 1537b927..437492c6 100644
--- a/src/constant_propagation.mli
+++ b/src/constant_propagation.mli
@@ -67,3 +67,5 @@ val const_prop :
   tannot exp * tannot exp Bindings.t
 
 val referenced_vars : tannot exp -> IdSet.t
+
+val remove_impossible_int_cases : 'a -> tannot defs -> tannot defs
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 23e22769..d9bcec04 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -5120,6 +5120,7 @@ let rewrite_defs_coq = [
   ("rewrite_undefined", rewrite_undefined_if_gen true);
   ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
   ("remove_not_pats", rewrite_defs_not_pats);
+  ("remove_impossible_int_cases", Constant_propagation.remove_impossible_int_cases);
   ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem);
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);