diff --git a/src/lib/anf.ml b/src/lib/anf.ml index e759750e7..928673a8f 100644 --- a/src/lib/anf.ml +++ b/src/lib/anf.ml @@ -78,7 +78,9 @@ module Big_int = Nat_big_num (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) -type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l +type aexp_annot = { loc : l; env : Env.t; uannot : uannot } + +type 'a aexp = AE_aux of 'a aexp_aux * aexp_annot and 'a aexp_aux = | AE_val of 'a aval @@ -126,7 +128,7 @@ and 'a aval = and 'a alexp = AL_id of id * 'a | AL_addr of id * 'a | AL_field of 'a alexp * id -let aexp_loc (AE_aux (_, _, l)) = l +let aexp_loc (AE_aux (_, { loc = l; _ })) = l (* Renaming variables in ANF expressions *) @@ -194,7 +196,7 @@ let rec aval_typ = function | AV_record (_, typ) -> typ | AV_cval (_, typ) -> typ -let aexp_typ (AE_aux (aux, _, _)) = +let aexp_typ (AE_aux (aux, _)) = match aux with | AE_val aval -> aval_typ aval | AE_app (_, _, typ) -> typ @@ -233,7 +235,7 @@ let rec alexp_rename from_id to_id = function | AL_addr (id, typ) -> AL_id (id, typ) | AL_field (alexp, field_id) -> AL_field (alexp_rename from_id to_id alexp, field_id) -let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = +let rec aexp_rename from_id to_id (AE_aux (aexp, annot)) = let recur = aexp_rename from_id to_id in let aexp = match aexp with @@ -264,13 +266,13 @@ let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, recur aexp1, recur aexp2) | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval_rename from_id to_id aval, recur aexp) in - AE_aux (aexp, env, l) + AE_aux (aexp, annot) and apexp_rename from_id to_id (apat, aexp1, aexp2) = if IdSet.mem from_id (apat_bindings apat) then (apat, aexp1, aexp2) else (apat, aexp_rename from_id to_id aexp1, aexp_rename from_id to_id aexp2) -let rec fold_aexp f (AE_aux (aexp, env, l)) = +let rec fold_aexp f (AE_aux (aexp, annot)) = let aexp = match aexp with | AE_app (id, vs, typ) -> AE_app (id, vs, typ) @@ -293,12 +295,12 @@ let rec fold_aexp f (AE_aux (aexp, env, l)) = ) | (AE_field _ | AE_struct_update _ | AE_val _ | AE_return _ | AE_exit _ | AE_throw _) as v -> v in - f (AE_aux (aexp, env, l)) + f (AE_aux (aexp, annot)) let aexp_bindings aexp = let ids = ref IdSet.empty in let collect_lets = function - | AE_aux (AE_let (_, id, _, _, _, _), _, _) as aexp -> + | AE_aux (AE_let (_, id, _, _, _, _), _) as aexp -> ids := IdSet.add id !ids; aexp | aexp -> aexp @@ -313,7 +315,7 @@ let new_shadow id = incr shadow_counter; shadow_id -let rec no_shadow ids (AE_aux (aexp, env, l)) = +let rec no_shadow ids (AE_aux (aexp, annot)) = let aexp = match aexp with | AE_val aval -> AE_val aval @@ -349,7 +351,7 @@ let rec no_shadow ids (AE_aux (aexp, env, l)) = | AE_loop (loop, aexp1, aexp2) -> AE_loop (loop, no_shadow ids aexp1, no_shadow ids aexp2) | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, no_shadow ids aexp) in - AE_aux (aexp, env, l) + AE_aux (aexp, annot) and no_shadow_apexp ids (apat, aexp1, aexp2) = let shadows = IdSet.inter (apat_bindings apat) ids in @@ -361,39 +363,39 @@ and no_shadow_apexp ids (apat, aexp1, aexp2) = (rename_apat apat, new_guard, no_shadow (IdSet.union ids (aexp_bindings new_guard)) (rename aexp2)) (* Map over all the avals in an aexp. *) -let rec map_aval f (AE_aux (aexp, env, l)) = +let rec map_aval f (AE_aux (aexp, annot)) = let aexp = match aexp with - | AE_val v -> AE_val (f env l v) + | AE_val v -> AE_val (f annot v) | AE_typ (aexp, typ) -> AE_typ (map_aval f aexp, typ) | AE_assign (alexp, aexp) -> AE_assign (alexp, map_aval f aexp) - | AE_app (id, vs, typ) -> AE_app (id, List.map (f env l) vs, typ) + | AE_app (id, vs, typ) -> AE_app (id, List.map (f annot) vs, typ) | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> AE_let (mut, id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_aval f) aexps, map_aval f aexp, typ) - | AE_return (aval, typ) -> AE_return (f env l aval, typ) - | AE_exit (aval, typ) -> AE_exit (f env l aval, typ) - | AE_throw (aval, typ) -> AE_throw (f env l aval, typ) - | AE_if (aval, aexp1, aexp2, typ2) -> AE_if (f env l aval, map_aval f aexp1, map_aval f aexp2, typ2) + | AE_return (aval, typ) -> AE_return (f annot aval, typ) + | AE_exit (aval, typ) -> AE_exit (f annot aval, typ) + | AE_throw (aval, typ) -> AE_throw (f annot aval, typ) + | AE_if (aval, aexp1, aexp2, typ2) -> AE_if (f annot aval, map_aval f aexp1, map_aval f aexp2, typ2) | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, map_aval f aexp1, map_aval f aexp2) | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> AE_for (id, map_aval f aexp1, map_aval f aexp2, map_aval f aexp3, order, map_aval f aexp4) - | AE_struct_update (aval, updates, typ) -> AE_struct_update (f env l aval, Bindings.map (f env l) updates, typ) - | AE_field (aval, field, typ) -> AE_field (f env l aval, field, typ) + | AE_struct_update (aval, updates, typ) -> AE_struct_update (f annot aval, Bindings.map (f annot) updates, typ) + | AE_field (aval, field, typ) -> AE_field (f annot aval, field, typ) | AE_match (aval, cases, typ) -> AE_match - (f env l aval, List.map (fun (pat, aexp1, aexp2) -> (pat, map_aval f aexp1, map_aval f aexp2)) cases, typ) + (f annot aval, List.map (fun (pat, aexp1, aexp2) -> (pat, map_aval f aexp1, map_aval f aexp2)) cases, typ) | AE_try (aexp, cases, typ) -> AE_try (map_aval f aexp, List.map (fun (pat, aexp1, aexp2) -> (pat, map_aval f aexp1, map_aval f aexp2)) cases, typ) - | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f env l aval, map_aval f aexp) + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, f annot aval, map_aval f aexp) in - AE_aux (aexp, env, l) + AE_aux (aexp, annot) (* Map over all the functions in an aexp. *) -let rec map_functions f (AE_aux (aexp, env, l)) = +let rec map_functions f (AE_aux (aexp, annot)) = let aexp = match aexp with - | AE_app (id, vs, typ) -> f env l id vs typ + | AE_app (id, vs, typ) -> f annot id vs typ | AE_typ (aexp, typ) -> AE_typ (map_functions f aexp, typ) | AE_assign (alexp, aexp) -> AE_assign (alexp, map_functions f aexp) | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) @@ -415,7 +417,7 @@ let rec map_functions f (AE_aux (aexp, env, l)) = ) | (AE_field _ | AE_struct_update _ | AE_val _ | AE_return _ | AE_exit _ | AE_throw _) as v -> v in - AE_aux (aexp, env, l) + AE_aux (aexp, annot) (* For debugging we provide a pretty printer for ANF expressions. *) @@ -441,7 +443,7 @@ let rec pp_alexp = function | AL_addr (id, typ) -> string "*" ^^ parens (pp_annot typ (pp_id id)) | AL_field (alexp, field) -> pp_alexp alexp ^^ dot ^^ pp_id field -let rec pp_aexp (AE_aux (aexp, _, _)) = +let rec pp_aexp (AE_aux (aexp, _)) = match aexp with | AE_val v -> pp_aval v | AE_typ (aexp, typ) -> pp_annot typ (string "$" ^^ pp_aexp aexp) @@ -453,7 +455,7 @@ let rec pp_aexp (AE_aux (aexp, _, _)) = group begin match binding with - | AE_aux (AE_let _, _, _) -> + | AE_aux (AE_let _, _) -> (pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="]) ^^ hardline ^^ nest 2 (pp_aexp binding) @@ -549,7 +551,7 @@ and pp_aval = function let ae_lit lit typ = AE_val (AV_lit (lit, typ)) -let is_dead_aexp (AE_aux (_, env, _)) = prove __POS__ env nc_false +let is_dead_aexp (AE_aux (_, { env; _ })) = prove __POS__ env nc_false let gensym, reset_anf_counter = symbol_generator "ga" @@ -596,8 +598,8 @@ let rec apat_globals (AP_aux (aux, _, _)) = | AP_as (apat, _, _) -> apat_globals apat | AP_struct (afpats, _) -> List.concat (List.map (fun (_, apat) -> apat_globals apat) afpats) -let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = - let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in +let rec anf (E_aux (e_aux, (l, tannot)) as exp) = + let mk_aexp aexp = AE_aux (aexp, { loc = l; env = env_of_tannot tannot; uannot = untyped_annot tannot }) in let rec anf_lexp env (LE_aux (aux, (l, _)) as lexp) = match aux with @@ -613,8 +615,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") [@coverage off] in - let to_aval (AE_aux (aexp_aux, env, _) as aexp) = - let mk_aexp (AE_aux (_, _, l)) aexp = AE_aux (aexp, env, l) in + let to_aval (AE_aux (aexp_aux, { env; uannot }) as aexp) = + let mk_aexp (AE_aux (_, { loc = l; _ })) aexp = AE_aux (aexp, { env; loc = l; uannot }) in match aexp_aux with | AE_val v -> (v, fun x -> x) | AE_short_circuit (_, _, _) -> @@ -670,8 +672,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = 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 exp))) - | E_app_infix (x, Id_aux (Id op, l), y) -> anf (E_aux (E_app (Id_aux (Operator op, l), [x; y]), exp_annot)) - | E_app_infix (x, Id_aux (Operator op, l), y) -> anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot)) + | E_app_infix (x, Id_aux (Id op, l), y) -> anf (E_aux (E_app (Id_aux (Operator op, l), [x; y]), (l, tannot))) + | E_app_infix (x, Id_aux (Operator op, l), y) -> anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), (l, tannot))) | E_vector exps -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in @@ -769,7 +771,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = Reporting.unreachable l __POS__ ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") [@coverage off] | E_let (LB_aux (LB_val (pat, binding), _), body) -> - anf (E_aux (E_match (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), exp_annot)) + anf (E_aux (E_match (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, empty_tannot))]), (l, tannot))) | E_tuple exps -> let aexps = List.map anf exps in let avals = List.map to_aval aexps in diff --git a/src/lib/anf.mli b/src/lib/anf.mli index 1a355359c..cb9eb0d7f 100644 --- a/src/lib/anf.mli +++ b/src/lib/anf.mli @@ -98,7 +98,9 @@ open Type_check See Flanagan et al's {e The Essence of Compiling with Continuations}. *) -type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l +type aexp_annot = { loc : l; env : Env.t; uannot : uannot } + +type 'a aexp = AE_aux of 'a aexp_aux * aexp_annot and 'a aexp_aux = | AE_val of 'a aval @@ -161,10 +163,10 @@ val aval_typ : typ aval -> typ val aexp_typ : typ aexp -> typ (** Map over all values in an ANF expression *) -val map_aval : (Env.t -> Ast.l -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp +val map_aval : (aexp_annot -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp (** Map over all function calls in an ANF expression *) -val map_functions : (Env.t -> Ast.l -> id -> 'a aval list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp +val map_functions : (aexp_annot -> id -> 'a aval list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp val fold_aexp : ('a aexp -> 'a aexp) -> 'a aexp -> 'a aexp diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index 74b6496bd..08729f099 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -303,7 +303,7 @@ module Make (C : CONFIG) = struct let append_into_block instrs instr = match instrs with [] -> instr | _ -> iblock (instrs @ [instr]) - let rec find_aexp_loc (AE_aux (e, _, l)) = + let rec find_aexp_loc (AE_aux (e, { loc = l; _ })) = match Reporting.simp_loc l with | Some _ -> l | None -> ( @@ -726,10 +726,10 @@ module Make (C : CONFIG) = struct CL_addr (CL_id (name id, ctyp)) | AL_field (alexp, field_id) -> CL_field (compile_alexp ctx alexp, field_id) - let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = + let rec compile_aexp ctx (AE_aux (aexp_aux, { env; loc = l; _ })) = let ctx = { ctx with local_env = env } in match aexp_aux with - | AE_let (mut, id, binding_typ, binding, (AE_aux (_, body_env, _) as body), body_typ) -> + | AE_let (mut, id, binding_typ, binding, (AE_aux (_, { env = body_env; _ }) as body), body_typ) -> let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in let setup, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = @@ -760,8 +760,8 @@ module Make (C : CONFIG) = struct else ( let trivial_guard = match guard with - | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) - | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _, _) -> + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _) + | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _) -> true | _ -> false in @@ -808,8 +808,8 @@ module Make (C : CONFIG) = struct let compile_case (apat, guard, body) = let trivial_guard = match guard with - | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) - | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _, _) -> + | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _) + | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _) -> true | _ -> false in @@ -930,7 +930,7 @@ module Make (C : CONFIG) = struct ) (* This is a faster assignment rule for updating fields of a struct. *) - | AE_assign (AL_id (id, assign_typ), AE_aux (AE_struct_update (AV_id (rid, _), fields, typ), _, _)) + | AE_assign (AL_id (id, assign_typ), AE_aux (AE_struct_update (AV_id (rid, _), fields, typ), _)) when Id.compare id rid = 0 -> let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in @@ -1112,7 +1112,7 @@ module Make (C : CONFIG) = struct and compile_block ctx = function | [] -> [] - | (AE_aux (_, _, l) as exp) :: exps -> + | (AE_aux (_, { loc = l; _ }) as exp) :: exps -> let setup, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in let gs = ngensym () in @@ -1405,7 +1405,7 @@ module Make (C : CONFIG) = struct let guard_instrs = match guard with | Some guard -> - let (AE_aux (_, _, l) as guard) = anf guard in + let (AE_aux (_, { loc = l; _ }) as guard) = anf guard in guard_bindings := aexp_bindings guard; let guard_aexp = C.optimize_anf ctx (no_shadow known_ids guard) in let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in diff --git a/src/lib/type_env.ml b/src/lib/type_env.ml index 050e497b1..c34d90b0b 100644 --- a/src/lib/type_env.ml +++ b/src/lib/type_env.ml @@ -1251,7 +1251,7 @@ let add_enum' is_scattered id ids env = id_loc member ) ) - ("Enum member " ^ string_of_id member ^ " is already part of another enum") + ("Enumeration member " ^ string_of_id member ^ " is already part of another enumeration") | None -> () ) ) diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 2dbf6b1c8..59d187159 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -294,11 +294,11 @@ end) : CONFIG = struct (**************************************************************************) let c_literals ctx = - let rec c_literal env l = function - | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) -> begin + let rec c_literal annot = function + | AV_lit (lit, typ) as v when is_stack_ctyp (convert_typ { ctx with local_env = annot.env } typ) -> begin match literal_to_fragment lit with Some cval -> AV_cval (cval, typ) | None -> v end - | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals) + | AV_tuple avals -> AV_tuple (List.map (c_literal annot) avals) | v -> v in map_aval c_literal @@ -356,7 +356,7 @@ end) : CONFIG = struct | aval -> aval (* Map over all the functions in an aexp. *) - let rec analyze_functions ctx f (AE_aux (aexp, env, l)) = + let rec analyze_functions ctx f (AE_aux (aexp, ({ env; loc = l; _ } as annot))) = let ctx = { ctx with local_env = env } in let aexp = match aexp with @@ -364,7 +364,7 @@ end) : CONFIG = struct | AE_typ (aexp, typ) -> AE_typ (analyze_functions ctx f aexp, typ) | AE_assign (alexp, aexp) -> AE_assign (alexp, analyze_functions ctx f aexp) | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp) - | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) -> + | AE_let (mut, id, typ1, aexp1, (AE_aux (_, { env = env2; _ }) as aexp2), typ2) -> let aexp1 = analyze_functions ctx f aexp1 in (* Use aexp2's environment because it will contain constraints for id *) let ctyp1 = convert_typ { ctx with local_env = env2 } typ1 in @@ -406,7 +406,7 @@ end) : CONFIG = struct ) | (AE_field _ | AE_struct_update _ | AE_val _ | AE_return _ | AE_exit _ | AE_throw _) as v -> v in - AE_aux (aexp, env, l) + AE_aux (aexp, annot) let analyze_primop' ctx id args typ = let no_change = AE_app (id, args, typ) in diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 314f819ec..5afd2a3c1 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -1503,19 +1503,19 @@ end) : Jib_compile.CONFIG = struct | L_false -> Some (V_lit (VL_bool false, CT_bool)) | _ -> None - let c_literals ctx = - let rec c_literal env l = function + let smt_literals ctx = + let rec smt_literal annot = function | AV_lit (lit, typ) as v -> begin match literal_to_cval lit with Some cval -> AV_cval (cval, typ) | None -> v end - | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals) + | AV_tuple avals -> AV_tuple (List.map (smt_literal annot) avals) | v -> v in - map_aval c_literal + map_aval smt_literal (* If we know the loop variables exactly (especially after specialization), we can unroll the exact number of times required, and omit any comparisons. *) let unroll_static_foreach ctx = function - | AE_aux (AE_for (id, from_aexp, to_aexp, by_aexp, order, body), env, l) as aexp -> begin + | AE_aux (AE_for (id, from_aexp, to_aexp, by_aexp, order, body), annot) as aexp -> begin match ( convert_typ ctx (aexp_typ from_aexp), convert_typ ctx (aexp_typ to_aexp), @@ -1524,28 +1524,30 @@ end) : Jib_compile.CONFIG = struct ) with | CT_constant f, CT_constant t, CT_constant b, Ord_aux (Ord_inc, _) -> + let new_annot = { annot with loc = gen_loc annot.loc; uannot = empty_uannot } in let i = ref f in let unrolled = ref [] in while Big_int.less_equal !i t do let current_index = - AE_aux (AE_val (AV_lit (L_aux (L_num !i, gen_loc l), atom_typ (nconstant !i))), env, gen_loc l) + AE_aux (AE_val (AV_lit (L_aux (L_num !i, gen_loc annot.loc), atom_typ (nconstant !i))), new_annot) in let iteration = - AE_aux (AE_let (Immutable, id, atom_typ (nconstant !i), current_index, body, unit_typ), env, gen_loc l) + AE_aux (AE_let (Immutable, id, atom_typ (nconstant !i), current_index, body, unit_typ), new_annot) in unrolled := iteration :: !unrolled; i := Big_int.add !i b done; begin match !unrolled with - | last :: iterations -> AE_aux (AE_block (List.rev iterations, last, unit_typ), env, gen_loc l) - | [] -> AE_aux (AE_val (AV_lit (L_aux (L_unit, gen_loc l), unit_typ)), env, gen_loc l) + | last :: iterations -> + AE_aux (AE_block (List.rev iterations, last, unit_typ), { annot with loc = gen_loc annot.loc }) + | [] -> AE_aux (AE_val (AV_lit (L_aux (L_unit, gen_loc annot.loc), unit_typ)), new_annot) end | _ -> aexp end | aexp -> aexp - let optimize_anf ctx aexp = aexp |> c_literals ctx |> fold_aexp (unroll_static_foreach ctx) + let optimize_anf ctx aexp = aexp |> smt_literals ctx |> fold_aexp (unroll_static_foreach ctx) let make_call_precise _ _ = false let ignore_64 = true