From 88b25e94c9266a481af6704423c321fb18f2ac31 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Fri, 28 Sep 2018 17:19:13 +0100 Subject: 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. --- src/anf.ml | 2 +- src/ast_util.ml | 2 +- src/ast_util.mli | 2 +- src/c_backend.ml | 6 ++++++ src/rewrites.ml | 2 +- src/type_check.ml | 4 ++++ 6 files changed, 14 insertions(+), 4 deletions(-) (limited to 'src') 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 -- cgit v1.2.3