diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/anf.ml | 2 | ||||
| -rw-r--r-- | src/ast_util.ml | 2 | ||||
| -rw-r--r-- | src/ast_util.mli | 2 | ||||
| -rw-r--r-- | src/c_backend.ml | 6 | ||||
| -rw-r--r-- | src/rewrites.ml | 2 | ||||
| -rw-r--r-- | src/type_check.ml | 4 |
6 files changed, 14 insertions, 4 deletions
@@ -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 |