Fix optimisation bug for certain if statements

When converting to A-normal form I just used the type of the then
branch of if statements to get the type of the whole if statement -
usually they'd be the same, but with flow typing one of the branches
can have a false constraint, which then allows the optimizer to fit
any integer into a 64-bit integer causing an overflow. The fix is to
correctly use the type the typechecker gives for the whole if
statement.

Also add decimal_string_of_bits to the C output.

Rename is_reftyp to is_ref_typ to be more consistent with other
is_X_typ functions in Ast_util.

6 files changed, 14 insertions, 4 deletions

diff --git a/src/anf.ml b/src/anf.ml
index 051c586f..0f98caff 100644
--- a/src/anf.ml
+++ b/src/anf.ml
@@ -544,7 +544,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      let cond_val, wrap = to_aval (anf cond) in
      let then_aexp = anf then_exp in
      let else_aexp = anf else_exp in
-     wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of then_exp)))
+     wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp)))
 
   | E_app_infix (x, Id_aux (Id op, l), y) ->
      anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot))
diff --git a/src/ast_util.ml b/src/ast_util.ml
index e69b4399..b9ab21b2 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -985,7 +985,7 @@ let rec is_number (Typ_aux (t,_)) =
   | Typ_app (Id_aux (Id "atom", _),_) -> true
   | _ -> false
 
-let is_reftyp (Typ_aux (typ_aux, _)) = match typ_aux with
+let is_ref_typ (Typ_aux (typ_aux, _)) = match typ_aux with
   | Typ_app (id, _) -> string_of_id id = "register" || string_of_id id = "reg"
   | _ -> false
 
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 429320cf..9dafbcd8 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -298,7 +298,7 @@ val lexp_to_exp : 'a lexp -> 'a exp
 
 val is_unit_typ : typ -> bool
 val is_number : typ -> bool
-val is_reftyp : typ -> bool
+val is_ref_typ : typ -> bool
 val is_vector_typ : typ -> bool
 val is_bit_typ : typ -> bool
 val is_bitvector_typ : typ -> bool
diff --git a/src/c_backend.ml b/src/c_backend.ml
index e61886b7..d58094ca 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -2211,6 +2211,12 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
           | CT_bits _ -> "string_of_sail_bits"
           | _ -> assert false
           end
+       | "decimal_string_of_bits", _ ->
+          begin match cval_ctyp (List.nth args 0) with
+          | CT_bits64 _ -> "decimal_string_of_mach_bits"
+          | CT_bits _ -> "decimal_string_of_sail_bits"
+          | _ -> assert false
+          end
        | "internal_vector_update", _ -> Printf.sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp)
        | "internal_vector_init", _ -> Printf.sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp)
        | "undefined_vector", CT_bits64 _ -> "UNDEFINED(mach_bits)"
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 9c26e69a..49409d1b 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -1855,7 +1855,7 @@ let rewrite_register_ref_writes (Defs defs) =
   let lexp_ref_exp (LEXP_aux (_, annot) as lexp) =
     try
       let exp = infer_exp (env_of_annot annot) (strip_exp (lexp_to_exp lexp)) in
-      if is_reftyp (typ_of exp) then Some exp else None
+      if is_ref_typ (typ_of exp) then Some exp else None
     with | _ -> None in
   let e_assign (lexp, exp) =
     let (lhs, rhs) = rewrite_lexp_to_rhs lexp in
diff --git a/src/type_check.ml b/src/type_check.ml
index 1742d518..6db08006 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -2197,6 +2197,10 @@ let rec add_opt_constraint constr env =
 let rec add_constraints constrs env =
   List.fold_left (fun env constr -> Env.add_constraint constr env) env constrs
 
+let solve_quant env = function
+  | QI_aux (QI_id _, _) -> false
+  | QI_aux (QI_const nc, _) -> prove env nc
+
 (* When doing implicit type coercion, for performance reasons we want
    to filter out the possible casts to only those that could
    reasonably apply. We don't mind if we try some coercions that are