Fix: Make sure we check Jib types match for operators before optimizing

Insert coercions for AV_cval if neccessary

Simplify any n in 2 ^ n, to make sure we can always evaluate 2 ^ n when
n is a constant before passing it to the SMT solver.

3 files changed, 16 insertions, 11 deletions

diff --git a/src/constraint.ml b/src/constraint.ml
index 1bd6a437..d8241e1d 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -179,10 +179,13 @@ let to_smt l vars constr =
     | Nexp_times (nexp1, nexp2) -> sfun "*" [smt_nexp nexp1; smt_nexp nexp2]
     | Nexp_sum (nexp1, nexp2) -> sfun "+" [smt_nexp nexp1; smt_nexp nexp2]
     | Nexp_minus (nexp1, nexp2) -> sfun "-" [smt_nexp nexp1; smt_nexp nexp2]
-    | Nexp_exp (Nexp_aux (Nexp_constant c, _)) when Big_int.greater c Big_int.zero ->
-       Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c)))
-    | Nexp_exp nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp]
-    | Nexp_exp nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
+    | Nexp_exp nexp ->
+       begin match nexp_simp nexp with
+       | Nexp_aux (Nexp_constant c, _) when Big_int.greater c Big_int.zero ->
+          Atom (Big_int.to_string (Big_int.pow_int_positive 2 (Big_int.to_int c)))
+       | nexp when !opt_solver.uninterpret_power -> sfun "sailexp" [smt_nexp nexp]
+       | nexp -> sfun "^" [Atom "2"; smt_nexp nexp]
+       end
     | Nexp_neg nexp -> sfun "-" [smt_nexp nexp]
   in
   let rec smt_constraint (NC_aux (aux, l) : n_constraint) : sexpr =
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index b98c53c4..c13b7f3b 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -462,19 +462,19 @@ let analyze_primop' ctx id args typ =
   | "not_bits", [AV_cval (v, _)] ->
      AE_val (AV_cval (V_call (Bvnot, [v]), typ))
 
-  | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+  | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
      AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ))
 
-  | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+  | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
      AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ))
 
-  | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+  | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
      AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ))
 
-  | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+  | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
      AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ))
 
-  | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] ->
+  | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
      AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ))
 
   | "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] ->
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 2066021e..e577e53a 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -193,8 +193,10 @@ let rec compile_aval l ctx = function
      let ctyp = cval_ctyp cval in
      let ctyp' = ctyp_of_typ ctx typ in
      if not (ctyp_equal ctyp ctyp') then
-       raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp'));
-     [], cval, []
+       let gs = ngensym () in
+       [iinit ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs]
+     else
+       [], cval, []
 
   | AV_id (id, typ) ->
      begin