diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/anf.ml | 59 | ||||
| -rw-r--r-- | src/anf.mli | 12 | ||||
| -rw-r--r-- | src/ast_util.ml | 7 | ||||
| -rw-r--r-- | src/ast_util.mli | 5 | ||||
| -rw-r--r-- | src/bytecode_util.ml | 48 | ||||
| -rw-r--r-- | src/c_backend.ml | 802 | ||||
| -rw-r--r-- | src/monomorphise.ml | 90 | ||||
| -rw-r--r-- | src/monomorphise.mli | 21 | ||||
| -rw-r--r-- | src/pattern_completeness.ml | 2 | ||||
| -rw-r--r-- | src/pattern_completeness.mli | 2 | ||||
| -rw-r--r-- | src/process_file.ml | 21 | ||||
| -rw-r--r-- | src/process_file.mli | 8 | ||||
| -rw-r--r-- | src/rewrites.ml | 52 | ||||
| -rw-r--r-- | src/rewrites.mli | 9 | ||||
| -rw-r--r-- | src/sail.ml | 43 | ||||
| -rw-r--r-- | src/type_check.ml | 9 | ||||
| -rw-r--r-- | src/type_check.mli | 5 |
17 files changed, 656 insertions, 539 deletions
@@ -54,6 +54,7 @@ open Bytecode open Bytecode_util open Type_check open PPrint + module Big_int = Nat_big_num let anf_error ?loc:(l=Parse_ast.Unknown) message = @@ -95,7 +96,7 @@ and 'a aexp_aux = | AE_app of id * ('a aval) list * 'a | AE_cast of 'a aexp * 'a | AE_assign of id * 'a * 'a aexp - | AE_let of id * 'a * 'a aexp * 'a aexp * 'a + | AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a | AE_block of ('a aexp) list * 'a aexp * 'a | AE_return of 'a aval * 'a | AE_throw of 'a aval * 'a @@ -123,8 +124,8 @@ and 'a apat_aux = and 'a aval = | AV_lit of lit * 'a - | AV_id of id * lvar - | AV_ref of id * lvar + | AV_id of id * 'a lvar + | AV_ref of id * 'a lvar | AV_tuple of ('a aval) list | AV_list of ('a aval) list * 'a | AV_vector of ('a aval) list * 'a @@ -132,7 +133,7 @@ and 'a aval = | AV_C_fragment of fragment * 'a (* Renaming variables in ANF expressions *) - + let rec apat_bindings (AP_aux (apat_aux, _, _)) = match apat_aux with | AP_tup apats -> List.fold_left IdSet.union IdSet.empty (List.map apat_bindings apats) @@ -143,6 +144,23 @@ let rec apat_bindings (AP_aux (apat_aux, _, _)) = | AP_nil -> IdSet.empty | AP_wild -> IdSet.empty +let rec apat_types (AP_aux (apat_aux, _, _)) = + let merge id b1 b2 = + match b1, b2 with + | None, None -> None + | Some v, None -> Some v + | None, Some v -> Some v + | Some _, Some _ -> assert false + in + match apat_aux with + | AP_tup apats -> List.fold_left (Bindings.merge merge) Bindings.empty (List.map apat_types apats) + | AP_id (id, typ) -> Bindings.singleton id typ + | AP_global (id, _) -> Bindings.empty + | AP_app (id, apat) -> apat_types apat + | AP_cons (apat1, apat2) -> (Bindings.merge merge) (apat_types apat1) (apat_types apat2) + | AP_nil -> Bindings.empty + | AP_wild -> Bindings.empty + let rec apat_rename from_id to_id (AP_aux (apat_aux, env, l)) = let apat_aux = match apat_aux with | AP_tup apats -> AP_tup (List.map (apat_rename from_id to_id) apats) @@ -176,8 +194,8 @@ let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) = | AE_cast (aexp, typ) -> AE_cast (recur aexp, typ) | AE_assign (id, typ, aexp) when Id.compare from_id id = 0 -> AE_assign (to_id, typ, aexp_rename from_id to_id aexp) | AE_assign (id, typ, aexp) -> AE_assign (id, typ, aexp_rename from_id to_id aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (id, typ1, aexp1, aexp2, typ2) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, recur aexp1, recur aexp2, typ2) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) when Id.compare from_id id = 0 -> AE_let (mut, id, typ1, aexp1, aexp2, typ2) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> AE_let (mut, id, typ1, recur aexp1, recur aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map recur aexps, recur aexp, typ) | AE_return (aval, typ) -> AE_return (aval_rename from_id to_id aval, typ) | AE_throw (aval, typ) -> AE_throw (aval_rename from_id to_id aval, typ) @@ -212,13 +230,13 @@ let rec no_shadow ids (AE_aux (aexp, env, l)) = | AE_app (id, avals, typ) -> AE_app (id, avals, typ) | AE_cast (aexp, typ) -> AE_cast (no_shadow ids aexp, typ) | AE_assign (id, typ, aexp) -> AE_assign (id, typ, no_shadow ids aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) when IdSet.mem id ids -> let shadow_id = new_shadow id in let aexp1 = no_shadow ids aexp1 in let ids = IdSet.add shadow_id ids in - AE_let (shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> - AE_let (id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) + AE_let (mut, shadow_id, typ1, aexp1, no_shadow ids (aexp_rename id shadow_id aexp2), typ2) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> + AE_let (mut, id, typ1, no_shadow ids aexp1, no_shadow (IdSet.add id ids) aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map (no_shadow ids) aexps, no_shadow ids aexp, typ) | AE_return (aval, typ) -> AE_return (aval, typ) | AE_throw (aval, typ) -> AE_throw (aval, typ) @@ -257,8 +275,8 @@ let rec map_aval f (AE_aux (aexp, env, l)) = | AE_cast (aexp, typ) -> AE_cast (map_aval f aexp, typ) | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_aval f aexp) | AE_app (id, vs, typ) -> AE_app (id, List.map (f env l) vs, typ) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> - AE_let (id, typ1, map_aval f aexp1, map_aval f aexp2, typ2) + | 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_throw (aval, typ) -> AE_throw (f env l aval, typ) @@ -286,7 +304,7 @@ let rec map_functions f (AE_aux (aexp, env, l)) = | AE_cast (aexp, typ) -> AE_cast (map_functions f aexp, typ) | AE_assign (id, typ, aexp) -> AE_assign (id, typ, map_functions f aexp) | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, map_functions f aexp) - | AE_let (id, typ1, aexp1, aexp2, typ2) -> AE_let (id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> AE_let (mut, id, typ1, map_functions f aexp1, map_functions f aexp2, typ2) | AE_block (aexps, aexp, typ) -> AE_block (List.map (map_functions f) aexps, map_functions f aexp, typ) | AE_if (aval, aexp1, aexp2, typ) -> AE_if (aval, map_functions f aexp1, map_functions f aexp2, typ) @@ -336,8 +354,9 @@ let rec pp_aexp (AE_aux (aexp, _, _)) = pp_aval aval ^^ string " || " ^^ pp_aexp aexp | AE_short_circuit (SC_and, aval, aexp) -> pp_aval aval ^^ string " && " ^^ pp_aexp aexp - | AE_let (id, id_typ, binding, body, typ) -> group + | AE_let (mut, id, id_typ, binding, body, typ) -> group begin + let let_doc = string (match mut with Immutable -> "let" | Mutable -> "let mut") in match binding with | AE_aux (AE_let _, _, _) -> (pp_annot typ (separate space [string "let"; pp_annot id_typ (pp_id id); string "="]) @@ -466,9 +485,9 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | AE_val v -> (v, fun x -> x) | AE_short_circuit (_, _, _) -> let id = gensym () in - (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (id, bool_typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, bool_typ)), fun x -> mk_aexp (AE_let (Immutable, id, bool_typ, aexp, x, typ_of exp))) | AE_app (_, _, typ) - | AE_let (_, _, _, _, typ) + | AE_let (_, _, _, _, _, typ) | AE_return (_, typ) | AE_throw (_, typ) | AE_cast (_, typ) @@ -478,10 +497,10 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | AE_try (_, _, typ) | AE_record_update (_, _, typ) -> let id = gensym () in - (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (id, typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, typ)), fun x -> mk_aexp (AE_let (Immutable, id, typ, aexp, x, typ_of exp))) | AE_assign _ | AE_block _ | AE_for _ | AE_loop _ -> let id = gensym () in - (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (id, unit_typ, aexp, x, typ_of exp))) + (AV_id (id, Local (Immutable, unit_typ)), fun x -> mk_aexp (AE_let (Immutable, id, unit_typ, aexp, x, typ_of exp))) in match e_aux with | E_lit lit -> mk_aexp (ae_lit lit (typ_of exp)) @@ -494,7 +513,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_assign (LEXP_aux (LEXP_deref dexp, _), exp) -> let gs = gensym () in - mk_aexp (AE_let (gs, typ_of dexp, anf dexp, mk_aexp (AE_assign (gs, typ_of dexp, anf exp)), unit_typ)) + mk_aexp (AE_let (Mutable, gs, typ_of dexp, anf dexp, mk_aexp (AE_assign (gs, typ_of dexp, anf exp)), unit_typ)) | E_assign (LEXP_aux (LEXP_id id, _), exp) | E_assign (LEXP_aux (LEXP_cast (_, id), _), exp) -> @@ -635,7 +654,7 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) = | E_let (LB_aux (LB_val (P_aux (P_id id, _), binding), _), body) -> let env = env_of body in let lvar = Env.lookup_id id env in - mk_aexp (AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp)) + mk_aexp (AE_let (Mutable, id, lvar_typ lvar, anf binding, anf body, typ_of exp)) | E_var (lexp, _, _) -> failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF") diff --git a/src/anf.mli b/src/anf.mli index ad345667..8ba83ccd 100644 --- a/src/anf.mli +++ b/src/anf.mli @@ -54,7 +54,7 @@ open Bytecode open Type_check (* The A-normal form (ANF) grammar *) - + type 'a aexp = AE_aux of 'a aexp_aux * Env.t * l and 'a aexp_aux = @@ -62,7 +62,7 @@ and 'a aexp_aux = | AE_app of id * ('a aval) list * 'a | AE_cast of 'a aexp * 'a | AE_assign of id * 'a * 'a aexp - | AE_let of id * 'a * 'a aexp * 'a aexp * 'a + | AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a | AE_block of ('a aexp) list * 'a aexp * 'a | AE_return of 'a aval * 'a | AE_throw of 'a aval * 'a @@ -90,8 +90,8 @@ and 'a apat_aux = and 'a aval = | AV_lit of lit * 'a - | AV_id of id * lvar - | AV_ref of id * lvar + | AV_id of id * 'a lvar + | AV_ref of id * 'a lvar | AV_tuple of ('a aval) list | AV_list of ('a aval) list * 'a | AV_vector of ('a aval) list * 'a @@ -109,7 +109,9 @@ val map_functions : (Env.t -> Ast.l -> id -> ('a aval) list -> 'a -> 'a aexp_aux val no_shadow : IdSet.t -> 'a aexp -> 'a aexp val apat_globals : 'a apat -> (id * 'a) list - + +val apat_types : 'a apat -> 'a Bindings.t + (* Compiling to ANF expressions *) val anf_pat : ?global:bool -> tannot pat -> typ apat diff --git a/src/ast_util.ml b/src/ast_util.ml index 78a34a33..86457e8f 100644 --- a/src/ast_util.ml +++ b/src/ast_util.ml @@ -54,7 +54,12 @@ module Big_int = Nat_big_num type mut = Immutable | Mutable -type lvar = Register of effect * effect * typ | Enum of typ | Local of mut * typ | Unbound +type 'a lvar = Register of effect * effect * 'a | Enum of 'a | Local of mut * 'a | Unbound + +let lvar_typ = function + | Local (_, typ) -> typ + | Register (_, _, typ) -> typ + | Enum typ -> typ let no_annot = (Parse_ast.Unknown, ()) diff --git a/src/ast_util.mli b/src/ast_util.mli index b4ef27ee..083b81e0 100644 --- a/src/ast_util.mli +++ b/src/ast_util.mli @@ -58,7 +58,10 @@ type mut = Immutable | Mutable (** [lvar] is the type of variables - they can either be registers, local mutable or immutable variables, nullary union constructors (i.e. None in option), or unbound identifiers *) -type lvar = Register of effect * effect * typ | Enum of typ | Local of mut * typ | Unbound +type 'a lvar = Register of effect * effect * 'a | Enum of 'a | Local of mut * 'a | Unbound + +(** Note: Partial function -- fails for Unknown lvars *) +val lvar_typ : 'a lvar -> 'a val no_annot : unit annot val gen_loc : Parse_ast.l -> Parse_ast.l diff --git a/src/bytecode_util.ml b/src/bytecode_util.ml index 139763b1..b11b70d0 100644 --- a/src/bytecode_util.ml +++ b/src/bytecode_util.ml @@ -73,18 +73,15 @@ let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval = let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp = I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l)) -let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = - I_aux (I_funcall (clexp, false, id, cvals, ctyp), (instr_number (), l)) +let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals = + I_aux (I_funcall (clexp, false, id, cvals), (instr_number (), l)) -let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals ctyp = - I_aux (I_funcall (clexp, true, id, cvals, ctyp), (instr_number (), l)) +let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals = + I_aux (I_funcall (clexp, true, id, cvals), (instr_number (), l)) let icopy ?loc:(l=Parse_ast.Unknown) clexp cval = I_aux (I_copy (clexp, cval), (instr_number (), l)) -let iconvert ?loc:(l=Parse_ast.Unknown) clexp ctyp1 id ctyp2 = - I_aux (I_convert (clexp, ctyp1, id, ctyp2), (instr_number (), l)) - let iclear ?loc:(l=Parse_ast.Unknown) ctyp id = I_aux (I_clear (ctyp, id), (instr_number (), l)) @@ -107,6 +104,9 @@ let ilabel ?loc:(l=Parse_ast.Unknown) label = let igoto ?loc:(l=Parse_ast.Unknown) label = I_aux (I_goto label, (instr_number (), l)) +let iundefined ?loc:(l=Parse_ast.Unknown) ctyp = + I_aux (I_undefined ctyp, (instr_number (), l)) + let imatch_failure ?loc:(l=Parse_ast.Unknown) () = I_aux (I_match_failure, (instr_number (), l)) @@ -203,11 +203,11 @@ let pp_cval (frag, ctyp) = string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp let rec pp_clexp = function - | CL_id id -> pp_id id - | CL_field (id, field) -> pp_id id ^^ string "." ^^ string field - | CL_addr id -> string "*" ^^ pp_id id - | CL_addr_field (id, field) -> pp_id id ^^ string "->" ^^ string field - | CL_current_exception -> string "current_exception" + | CL_id (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | CL_field (id, field, ctyp) -> pp_id id ^^ string "." ^^ string field ^^ string " : " ^^ pp_ctyp ctyp + | CL_addr (id, ctyp) -> string "*" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp + | CL_addr_field (id, field, ctyp) -> pp_id id ^^ string "->" ^^ string field ^^ string " : " ^^ pp_ctyp ctyp + | CL_current_exception _ -> string "current_exception" | CL_have_exception -> string "have_exception" let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = @@ -238,13 +238,9 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval | I_reinit (ctyp, id, cval) -> pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval - | I_funcall (x, _, f, args, ctyp2) -> + | I_funcall (x, _, f, args) -> separate space [ pp_clexp x; string "="; - string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args); - string ":"; pp_ctyp ctyp2 ] - | I_convert (x, ctyp1, y, ctyp2) -> - separate space [ pp_clexp x; colon; pp_ctyp ctyp1; string "="; - pp_keyword "convert" ^^ pp_id y; colon; pp_ctyp ctyp2 ] + string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args) ] | I_copy (clexp, cval) -> separate space [pp_clexp clexp; string "="; pp_cval cval] | I_clear (ctyp, id) -> @@ -261,6 +257,8 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) = pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear) | I_match_failure -> pp_keyword "match_failure" + | I_undefined ctyp -> + pp_keyword "undefined" ^^ pp_ctyp ctyp | I_raw str -> pp_keyword "C" ^^ string (str |> Util.cyan |> Util.clear) @@ -355,12 +353,12 @@ let rec fragment_deps = function let cval_deps = function (frag, _) -> fragment_deps frag let rec clexp_deps = function - | CL_id id -> NS.singleton (G_id id) - | CL_field (id, _) -> NS.singleton (G_id id) - | CL_addr id -> NS.singleton (G_id id) - | CL_addr_field (id, _) -> NS.singleton (G_id id) + | CL_id (id, _) -> NS.singleton (G_id id) + | CL_field (id, _, _) -> NS.singleton (G_id id) + | CL_addr (id, _) -> NS.singleton (G_id id) + | CL_addr_field (id, _, _) -> NS.singleton (G_id id) | CL_have_exception -> NS.empty - | CL_current_exception -> NS.empty + | CL_current_exception _ -> NS.empty (** Return the direct, non program-order dependencies of a single instruction **) @@ -370,8 +368,7 @@ let instr_deps = function | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NS.singleton (G_id id) | I_if (cval, _, _, _) -> cval_deps cval, NS.empty | I_jump (cval, label) -> cval_deps cval, NS.singleton (G_label label) - | I_funcall (clexp, _, _, cvals, _) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp - | I_convert (clexp, _, id, _) -> NS.singleton (G_id id), clexp_deps clexp + | I_funcall (clexp, _, _, cvals) -> List.fold_left NS.union NS.empty (List.map cval_deps cvals), clexp_deps clexp | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp | I_clear (_, id) -> NS.singleton (G_id id), NS.singleton (G_id id) | I_throw cval | I_return cval -> cval_deps cval, NS.empty @@ -379,6 +376,7 @@ let instr_deps = function | I_comment _ | I_raw _ -> NS.empty, NS.empty | I_label label -> NS.singleton (G_label label), NS.empty | I_goto label -> NS.empty, NS.singleton (G_label label) + | I_undefined _ -> NS.empty, NS.empty | I_match_failure -> NS.empty, NS.empty let add_link from_node to_node graph = diff --git a/src/c_backend.ml b/src/c_backend.ml index cb732e2d..433e3d85 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -67,7 +67,6 @@ let opt_static = ref false (* Optimization flags *) let optimize_primops = ref false -let optimize_z3 = ref false let optimize_hoist_allocations = ref false let optimize_struct_updates = ref false @@ -94,9 +93,11 @@ type ctx = variants : (ctyp Bindings.t) Bindings.t; tc_env : Env.t; local_env : Env.t; + locals : (mut * ctyp) Bindings.t; letbinds : int list; recursive_functions : IdSet.t; no_raw : bool; + optimize_z3 : bool; } let initial_ctx env = @@ -105,9 +106,11 @@ let initial_ctx env = variants = Bindings.empty; tc_env = env; local_env = env; + locals = Bindings.empty; letbinds = []; recursive_functions = IdSet.empty; no_raw = false; + optimize_z3 = true; } let rec ctyp_equal ctyp1 ctyp2 = @@ -148,12 +151,11 @@ let rec ctyp_of_typ ctx typ = | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 -> CT_int64 - | n, m when !optimize_z3 -> - prerr_endline ("optimize atom " ^ string_of_nexp n ^ ", " ^ string_of_nexp m ^ " in context " ^ (Util.string_of_list ", " string_of_n_constraint (Env.get_constraints ctx.local_env))); + | n, m when ctx.optimize_z3 -> if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then - (prerr_endline "yes"; CT_int64) + CT_int64 else - (prerr_endline "no"; CT_int) + CT_int | _ -> CT_int end @@ -168,7 +170,13 @@ let rec ctyp_of_typ ctx typ = let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction) + | _ when not ctx.optimize_z3 -> CT_bits direction | _ -> CT_bits direction + (* This is extremely slow :( + match solve ctx.local_env n with + | Some n when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction) + | _ -> CT_bits direction + *) end | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_order ord, _); @@ -190,13 +198,11 @@ let rec ctyp_of_typ ctx typ = | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs) - | Typ_exist _ when !optimize_z3 -> + | Typ_exist _ when ctx.optimize_z3 -> (* Use Type_check.destruct_exist when optimising with z3, to ensure that we don't cause any type variable clashes in local_env. *) begin match destruct_exist ctx.local_env typ with | Some (kids, nc, typ) -> - c_debug (lazy ("optimize existential: " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ - ^ " in context " ^ (Util.string_of_list ", " string_of_n_constraint (Env.get_constraints ctx.local_env)))); let env = add_existential l kids nc ctx.local_env in ctyp_of_typ { ctx with local_env = env } typ | None -> c_error "Existential cannot be destructured. This should be impossible!" @@ -298,12 +304,24 @@ let rec c_aval ctx = function | None -> v end | AV_C_fragment (str, typ) -> AV_C_fragment (str, typ) - (* An id can be converted to a C fragment if it's type can be stack-allocated. *) + (* An id can be converted to a C fragment if it's type can be + stack-allocated. *) | AV_id (id, lvar) as v -> begin match lvar with | Local (_, typ) when is_stack_typ ctx typ -> - AV_C_fragment (F_id id, typ) + begin + try + (* We need to check that id's type hasn't changed due to flow typing *) + let _, ctyp = Bindings.find id ctx.locals in + if is_stack_ctyp ctyp then + AV_C_fragment (F_id id, typ) + else + (prerr_endline (string_of_id id ^ " : " ^ string_of_ctyp ctyp ^ " -> " ^ string_of_ctyp (ctyp_of_typ ctx typ)); + v) (* id's type went from heap -> stack due to flow typing, so it's really still heap allocated! *) + with + Not_found -> failwith ("could not find " ^ string_of_id id ^ " in local variables") + end | Register (_, _, typ) when is_stack_typ ctx typ -> AV_C_fragment (F_id id, typ) | _ -> v @@ -324,16 +342,65 @@ let c_fragment = function let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail2_values.B1))) -let analyze_primop' ctx env l id args typ = +(* Map over all the functions in an aexp. *) +let rec analyze_functions ctx f (AE_aux (aexp, env, l)) = let ctx = { ctx with local_env = env } in + let aexp = match aexp with + | AE_app (id, vs, typ) -> f ctx id vs typ + + | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ) + + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, 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, aexp2, typ2) -> + let aexp1 = analyze_functions ctx f aexp1 in + let ctyp1 = ctyp_of_typ ctx typ1 in + let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in + AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2) + + | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ) + + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ) + + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) + + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let aexp1 = analyze_functions ctx f aexp1 in + let aexp2 = analyze_functions ctx f aexp2 in + let aexp3 = analyze_functions ctx f aexp3 in + let aexp4 = analyze_functions ctx f aexp4 in + AE_for (id, aexp1, aexp2, aexp3, order, aexp4) + + | AE_case (aval, cases, typ) -> + let analyze_case (pat, aexp1, aexp2) = + let pat_bindings = Bindings.bindings (apat_types pat) in + let ctx = + List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, ctyp_of_typ ctx typ) ctx.locals }) ctx pat_bindings + in + pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2 + in + AE_case (aval, List.map analyze_case cases, typ) + + | AE_try (aexp, cases, typ) -> + AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ) + + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v + in + AE_aux (aexp, env, l) + +let analyze_primop' ctx id args typ = let no_change = AE_app (id, args, typ) in let args = List.map (c_aval ctx) args in let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in - (* prerr_endline ("Analysing: " ^ string_of_typ typ ^ " " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); *) let v_one = F_lit (V_int (Big_int.of_int 1)) in let v_int n = F_lit (V_int (Big_int.of_int n)) in + c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")")); + match extern, args with | "eq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ)) @@ -352,6 +419,9 @@ let analyze_primop' ctx env l id args typ = | _ -> no_change end + | "gteq", [AV_C_fragment (v1, _); AV_C_fragment (v2, _)] -> + AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ)) + | "xor_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "^", v2), typ)) @@ -369,7 +439,7 @@ let analyze_primop' ctx env l id args typ = | _ -> no_change end - | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> + | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] when is_stack_typ ctx typ -> let len = F_op (f, "-", F_op (t, "-", v_one)) in AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ)) @@ -413,13 +483,17 @@ let analyze_primop' ctx env l id args typ = | "undefined_bool", _ -> AE_val (AV_C_fragment (F_lit (V_bool false), typ)) - | _, _ -> no_change + | _, _ -> + c_debug (lazy ("No optimization routine found")); + no_change -let analyze_primop ctx env l id args typ = +let analyze_primop ctx id args typ = let no_change = AE_app (id, args, typ) in if !optimize_primops then - try analyze_primop' ctx env l id args typ with - | Failure _ -> no_change + try analyze_primop' ctx id args typ with + | Failure str -> + (c_debug (lazy ("Analyze primop failed for id " ^ string_of_id id ^ " reason: " ^ str))); + no_change else no_change @@ -456,15 +530,23 @@ let ctype_def_ctyps = function let cval_ctyp = function (_, ctyp) -> ctyp +let clexp_ctyp = function + | CL_id (_, ctyp) -> ctyp + | CL_field (_, _, ctyp) -> ctyp + | CL_addr (_, ctyp) -> ctyp + | CL_addr_field (_, _, ctyp) -> ctyp + | CL_have_exception -> CT_bool + | CL_current_exception ctyp -> ctyp + let rec map_instrs f (I_aux (instr, aux)) = let instr = match instr with | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr | I_if (cval, instrs1, instrs2, ctyp) -> I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp) - | I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr + | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr | I_block instrs -> I_block (f (List.map (map_instrs f) instrs)) | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs)) - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr in I_aux (instr, aux) @@ -472,14 +554,13 @@ let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ct let rec instr_ctyps (I_aux (instr, aux)) = match instr with - | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp] + | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> [ctyp] | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> [ctyp; cval_ctyp cval] | I_if (cval, instrs1, instrs2, ctyp) -> ctyp :: cval_ctyp cval :: List.concat (List.map instr_ctyps instrs1 @ List.map instr_ctyps instrs2) - | I_funcall (_, _, _, cvals, ctyp) -> - ctyp :: List.map cval_ctyp cvals - | I_convert (_, ctyp1, _, ctyp2) -> [ctyp1; ctyp2] - | I_copy (_, cval) -> [cval_ctyp cval] + | I_funcall (clexp, _, _, cvals) -> + clexp_ctyp clexp :: List.map cval_ctyp cvals + | I_copy (clexp, cval) -> [clexp_ctyp clexp; cval_ctyp cval] | I_block instrs | I_try_block instrs -> List.concat (List.map instr_ctyps instrs) | I_throw cval | I_jump (cval, _) | I_return cval -> [cval_ctyp cval] | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> [] @@ -546,7 +627,14 @@ let rec compile_aval ctx = function [], (frag, ctyp_of_typ ctx typ), [] | AV_id (id, typ) -> - [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] + begin + try + let _, ctyp = Bindings.find id ctx.locals in + [], (F_id id, ctyp), [] + with + | Not_found -> + [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] + end | AV_ref (id, typ) -> [], (F_ref id, CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] @@ -590,7 +678,7 @@ let rec compile_aval ctx = function let gs = gensym () in setup @ [idecl tup_ctyp gs] - @ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n)) cval) cvals, + @ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n, cval_ctyp cval)) cval) cvals, (F_id gs, CT_tup (List.map cval_ctyp cvals)), [iclear tup_ctyp gs] @ cleanup @@ -601,7 +689,7 @@ let rec compile_aval ctx = function let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup - @ [icopy (CL_field (gs, string_of_id id)) cval] + @ [icopy (CL_field (gs, string_of_id id, cval_ctyp cval)) cval] @ field_cleanup in [idecl ctyp gs] @@ -637,10 +725,9 @@ let rec compile_aval ctx = function let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in let gs = gensym () in [iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))] - @ List.map (fun chunk -> ifuncall (CL_id gs) + @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_bits true)) (mk_id "append_64") - [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))] - (CT_bits true)) chunks, + [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))]) chunks, (F_id gs, CT_bits true), [iclear (CT_bits true) gs] @@ -661,12 +748,12 @@ let rec compile_aval ctx = function match cval with | (F_lit (V_bit Sail2_values.B0), _) -> [] | (F_lit (V_bit Sail2_values.B1), _) -> - [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] + [icopy (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] | _ -> - setup @ [iif cval [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup + setup @ [iif cval [icopy (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup in [idecl ctyp gs; - icopy (CL_id gs) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] + icopy (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] @ List.concat (List.mapi aval_mask (List.rev avals)), (F_id gs, ctyp), [] @@ -685,13 +772,13 @@ let rec compile_aval ctx = function let aval_set i aval = let setup, cval, cleanup = compile_aval ctx aval in setup - @ [iextern (CL_id gs) + @ [iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_update") - [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval] vector_ctyp] + [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval]] @ cleanup in [idecl vector_ctyp gs; - iextern (CL_id gs) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)] vector_ctyp] + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)]] @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), (F_id gs, vector_ctyp), [iclear vector_ctyp gs] @@ -707,7 +794,7 @@ let rec compile_aval ctx = function let gs = gensym () in let mk_cons aval = let setup, cval, cleanup = compile_aval ctx aval in - setup @ [ifuncall (CL_id gs) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)] (CT_list ctyp)] @ cleanup + setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup in [idecl (CT_list ctyp) gs] @ List.concat (List.map mk_cons (List.rev avals)), @@ -728,125 +815,103 @@ let compile_funcall l ctx id args typ = | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ | _ -> assert false in - let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in let final_ctyp = ctyp_of_typ ctx typ in let setup_arg ctyp aval = let arg_setup, cval, arg_cleanup = compile_aval ctx aval in - setup := List.rev arg_setup @ !setup; + setup := List.rev arg_setup @ [icomment (string_of_ctyp (cval_ctyp cval))] @ !setup; cleanup := arg_cleanup @ !cleanup; let have_ctyp = cval_ctyp cval in if ctyp_equal ctyp have_ctyp then cval - else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then + else let gs = gensym () in setup := iinit ctyp gs cval :: !setup; cleanup := iclear ctyp gs :: !cleanup; (F_id gs, ctyp) - else if not (is_stack_ctyp have_ctyp) && is_stack_ctyp ctyp then - (* This is inefficient. FIXME: Remove id restriction on iconvert - instruction. Fortunatly only happens when flow typing makes a - length-polymorphic bitvector monomorphic. *) - let gs1 = gensym () in - let gs2 = gensym () in - setup := idecl have_ctyp gs1 :: !setup; - setup := icopy (CL_id gs1) cval :: !setup; - setup := idecl ctyp gs2 :: !setup; - setup := iconvert (CL_id gs2) ctyp gs1 have_ctyp :: !setup; - cleanup := iclear have_ctyp gs1 :: !cleanup; - (F_id gs2, ctyp) - else - c_error ~loc:l - (Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp)) in assert (List.length arg_ctyps = List.length args); - let sargs = List.map2 setup_arg arg_ctyps args in + let setup_args = List.map2 setup_arg arg_ctyps args in - let call = - if ctyp_equal final_ctyp ret_ctyp then - fun ret -> ifuncall ret id sargs ret_ctyp - else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then - let gs = gensym () in - setup := idecl ret_ctyp gs :: !setup; - setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; - cleanup := iclear ret_ctyp gs :: !cleanup; - fun ret -> iconvert ret final_ctyp gs ret_ctyp - else if is_stack_ctyp ret_ctyp && not (is_stack_ctyp final_ctyp) then - let gs = gensym () in - setup := idecl ret_ctyp gs :: !setup; - setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; - fun ret -> iconvert ret final_ctyp gs ret_ctyp - else - c_error (Printf.sprintf "Funcall call type mismatch between %s and %s" (string_of_ctyp ret_ctyp) (string_of_ctyp final_ctyp)) - in - - (List.rev !setup, final_ctyp, call, !cleanup) + List.rev !setup, + begin fun clexp -> + if ctyp_equal (clexp_ctyp clexp) ret_ctyp then + ifuncall clexp id setup_args + else + let gs = gensym () in + iblock [idecl ret_ctyp gs; + ifuncall (CL_id (gs, ret_ctyp)) id setup_args; + icopy clexp (F_id gs, ret_ctyp); + iclear ret_ctyp gs] + end, + !cleanup let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = let ctx = { ctx with local_env = env } in match apat_aux, cval with | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env -> [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label], - [] + [], + ctx + | AP_global (pid, typ), (frag, ctyp) -> let global_ctyp = ctyp_of_typ ctx typ in - if ctyp_equal global_ctyp ctyp then - [icopy (CL_id pid) cval], [] - else - begin match frag with - | F_id id -> - [iconvert (CL_id pid) global_ctyp id ctyp], [] - | _ -> c_error "Cannot compile global letbinding" - end + [icopy (CL_id (pid, global_ctyp)) cval], [], ctx + | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with - | Unbound -> [idecl ctyp pid; icopy (CL_id pid) (frag, ctyp)], [] - | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [] + | Unbound -> [idecl ctyp pid; icopy (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx + | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx end + | AP_id (pid, typ), _ -> let ctyp = cval_ctyp cval in let id_ctyp = ctyp_of_typ ctx typ in - if ctyp_equal id_ctyp ctyp then - [idecl ctyp pid; icopy (CL_id pid) cval], [iclear id_ctyp pid] - else - let gs = gensym () in - [idecl id_ctyp pid; idecl ctyp gs; icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp; iclear ctyp gs], [iclear id_ctyp pid] + c_debug (lazy ("Adding local " ^ string_of_id pid ^ " : " ^ string_of_ctyp id_ctyp)); + let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in + [idecl ctyp pid; icopy (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx + | AP_tup apats, (frag, ctyp) -> begin let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in - let fold (instrs, cleanup, n) apat ctyp = - let instrs', cleanup' = compile_match ctx apat (get_tup n ctyp) case_label in - instrs @ instrs', cleanup' @ cleanup, n + 1 + let fold (instrs, cleanup, n, ctx) apat ctyp = + let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in + instrs @ instrs', cleanup' @ cleanup, n + 1, ctx in match ctyp with | CT_tup ctyps -> - let instrs, cleanup, _ = List.fold_left2 fold ([], [], 0) apats ctyps in - instrs, cleanup + let instrs, cleanup, _, ctx = List.fold_left2 fold ([], [], 0, ctx) apats ctyps in + instrs, cleanup, ctx | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp) end + | AP_app (ctor, apat), (frag, ctyp) -> begin match ctyp with | CT_variant (_, ctors) -> let ctor_c_id = string_of_id ctor in let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in - let instrs, cleanup = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in + let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label] @ instrs, - cleanup + cleanup, + ctx | _ -> failwith "AP_app constructor with non-variant type" end - | AP_wild, _ -> [], [] + + | AP_wild, _ -> [], [], ctx | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> - let hd_setup, hd_cleanup = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in - let tl_setup, tl_cleanup = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in - [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup + let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in + let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in + [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx + | AP_cons _, (_, _) -> c_error "Tried to pattern match cons on non list type" - | AP_nil, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [] + | AP_nil, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx let unit_fragment = (F_lit V_unit, CT_unit) @@ -860,34 +925,34 @@ let label str = incr label_counter; str +let pointer_assign ctyp1 ctyp2 = + match ctyp1 with + | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true + | CT_ref ctyp1 -> + c_error (Printf.sprintf "Incompatible type in pointer assignment between %s and %s" + (string_of_ctyp ctyp1) + (string_of_ctyp ctyp2)) + | _ -> false + let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctx = { ctx with local_env = env } in match aexp_aux with - | AE_let (id, _, binding, body, typ) -> - let setup, ctyp, call, cleanup = compile_aexp ctx binding in + | AE_let (mut, id, binding_typ, binding, body, body_typ) -> + let binding_ctyp = ctyp_of_typ ctx binding_typ in + let setup, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = - [idecl ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [iclear ctyp id] + [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] in - let setup, ctyp, call, cleanup = compile_aexp ctx body in - let body_ctyp = ctyp_of_typ ctx typ in - if ctyp_equal body_ctyp ctyp then - letb_setup @ setup, ctyp, call, cleanup @ letb_cleanup - else - begin - prerr_endline ("Mismatch: " ^ string_of_ctyp body_ctyp ^ " and " ^ string_of_ctyp ctyp); - let gs = gensym () in - letb_setup @ setup @ [idecl ctyp gs; call (CL_id gs)], - body_ctyp, - (fun clexp -> iconvert clexp body_ctyp gs ctyp), - [iclear ctyp gs] @ cleanup @ letb_cleanup - end + let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in + let setup, call, cleanup = compile_aexp ctx body in + letb_setup @ setup, call, cleanup @ letb_cleanup | AE_app (id, vs, typ) -> compile_funcall l ctx id vs typ | AE_val aval -> let setup, cval, cleanup = compile_aval ctx aval in - setup, cval_ctyp cval, (fun clexp -> icopy clexp cval), cleanup + setup, (fun clexp -> icopy clexp cval), cleanup (* Compile case statements *) | AE_case (aval, cases, typ) -> @@ -903,19 +968,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = in let case_label = label "case_" in c_debug (lazy ("Compiling match")); - let destructure, destructure_cleanup = compile_match ctx apat cval case_label in + let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in c_debug (lazy ("Compiled match")); - let guard_setup, _, guard_call, guard_cleanup = compile_aexp ctx guard in - let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let case_instrs = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then - guard_setup @ [idecl CT_bool gs; guard_call (CL_id gs)] @ guard_cleanup + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit] @ [icomment "end guard"] else []) - @ body_setup @ [body_call (CL_id case_return_id)] @ body_cleanup @ destructure_cleanup + @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in [iblock case_instrs; ilabel case_label] @@ -925,15 +990,15 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], - ctyp, (fun clexp -> icopy clexp (F_id case_return_id, ctyp)), - (if is_stack_ctyp ctyp then [] else [iclear ctyp case_return_id]) + [iclear ctyp case_return_id] @ aval_cleanup @ [icomment "end match"] (* Compile try statement *) | AE_try (aexp, cases, typ) -> - let aexp_setup, ctyp, aexp_call, aexp_cleanup = compile_aexp ctx aexp in + let ctyp = ctyp_of_typ ctx typ in + let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in let try_return_id = gensym () in let handled_exception_label = label "handled_exception_" in let compile_case (apat, guard, body) = @@ -944,18 +1009,18 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = in let try_label = label "try_" in let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in - let destructure, destructure_cleanup = compile_match ctx apat exn_cval try_label in - let guard_setup, _, guard_call, guard_cleanup = compile_aexp ctx guard in - let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let case_instrs = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then - guard_setup @ [idecl CT_bool gs; guard_call (CL_id gs)] @ guard_cleanup + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label] @ [icomment "end guard"] else []) - @ body_setup @ [body_call (CL_id try_return_id)] @ body_cleanup @ destructure_cleanup + @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto handled_exception_label] in [iblock case_instrs; ilabel try_label] @@ -963,35 +1028,23 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [icomment "begin try catch"; idecl ctyp try_return_id; - itry_block (aexp_setup @ [aexp_call (CL_id try_return_id)] @ aexp_cleanup); + itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); ijump (F_unary ("!", F_have_exception), CT_bool) handled_exception_label] @ List.concat (List.map compile_case cases) @ [imatch_failure (); ilabel handled_exception_label; icopy CL_have_exception (F_lit (V_bool false), CT_bool)], - ctyp, (fun clexp -> icopy clexp (F_id try_return_id, ctyp)), [] | AE_if (aval, then_aexp, else_aexp, if_typ) -> let if_ctyp = ctyp_of_typ ctx if_typ in let compile_branch aexp = - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - if ctyp_equal if_ctyp ctyp then - fun clexp -> setup @ [call clexp] @ cleanup - else - fun clexp -> - let gs = gensym () in - setup - @ [idecl ctyp gs; - call (CL_id gs); - iconvert clexp if_ctyp gs ctyp; - iclear ctyp gs] - @ cleanup + let setup, call, cleanup = compile_aexp ctx aexp in + fun clexp -> setup @ [call clexp] @ cleanup in let setup, cval, cleanup = compile_aval ctx aval in setup, - if_ctyp, (fun clexp -> iif cval (compile_branch then_aexp clexp) (compile_branch else_aexp clexp) @@ -1001,43 +1054,51 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) | AE_record_update (aval, fields, typ) -> let ctyp = ctyp_of_typ ctx typ in + let ctors = match ctyp with + | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors + | _ -> c_error "Cannot perform record update for non-record type" + in let gs = gensym () in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup - @ [icopy (CL_field (gs, string_of_id id)) cval] + @ [icomment (string_of_ctyp ctyp)] + @ [icopy (CL_field (gs, string_of_id id, Bindings.find id ctors)) cval] @ field_cleanup in let setup, cval, cleanup = compile_aval ctx aval in [idecl ctyp gs] @ setup - @ [icopy (CL_id gs) cval] + @ [icopy (CL_id (gs, ctyp)) cval] @ cleanup @ List.concat (List.map compile_fields (Bindings.bindings fields)), - ctyp, (fun clexp -> icopy clexp (F_id gs, ctyp)), [iclear ctyp gs] | AE_short_circuit (SC_and, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval ctx aval in - let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in let gs = gensym () in left_setup @ [ idecl CT_bool gs; - iif cval (right_setup @ [call (CL_id gs)] @ right_cleanup) [icopy (CL_id gs) (F_lit (V_bool false), CT_bool)] CT_bool ] + iif cval + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + [icopy (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)] + CT_bool ] @ left_cleanup, - CT_bool, (fun clexp -> icopy clexp (F_id gs, CT_bool)), [] | AE_short_circuit (SC_or, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval ctx aval in - let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in let gs = gensym () in left_setup @ [ idecl CT_bool gs; - iif cval [icopy (CL_id gs) (F_lit (V_bool true), CT_bool)] (right_setup @ [call (CL_id gs)] @ right_cleanup) CT_bool ] + iif cval + [icopy (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)] + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + CT_bool ] @ left_cleanup, - CT_bool, (fun clexp -> icopy clexp (F_id gs, CT_bool)), [] @@ -1049,91 +1110,64 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup - @ [icopy (CL_field (id, string_of_id field_id)) cval] + @ [icopy (CL_field (id, string_of_id field_id, cval_ctyp cval)) cval] @ field_cleanup in List.concat (List.map compile_fields (Bindings.bindings fields)), - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] | AE_assign (id, assign_typ, aexp) -> - (* assign_ctyp is the type of the C variable we are assigning to, - ctyp is the type of the C expression being assigned. These may - be different. *) - let pointer_assign ctyp1 ctyp2 = - match ctyp1 with - | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true - | CT_ref ctyp1 -> c_error ~loc:l "Incompatible type in pointer assignment" - | _ -> false - in let assign_ctyp = ctyp_of_typ ctx assign_typ in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - let comment = "assign " ^ string_of_ctyp assign_ctyp ^ " := " ^ string_of_ctyp ctyp in - if ctyp_equal assign_ctyp ctyp then - setup @ [call (CL_id id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup - else if pointer_assign assign_ctyp ctyp then - setup @ [call (CL_addr id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup - else - let gs = gensym () in - setup @ [ icomment comment; - idecl ctyp gs; - call (CL_id gs); - iconvert (CL_id id) assign_ctyp gs ctyp; - iclear ctyp gs - ], - CT_unit, - (fun clexp -> icopy clexp unit_fragment), - cleanup + let setup, call, cleanup = compile_aexp ctx aexp in + setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy clexp unit_fragment), cleanup | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - block @ setup, ctyp, call, cleanup + let setup, call, cleanup = compile_aexp ctx aexp in + block @ setup, call, cleanup | AE_loop (While, cond, body) -> let loop_start_label = label "while_" in let loop_end_label = label "wend_" in - let cond_setup, _, cond_call, cond_cleanup = compile_aexp ctx cond in - let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let unit_gs = gensym () in let loop_test = (F_unary ("!", F_id gs), CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (cond_setup - @ [cond_call (CL_id gs)] + @ [cond_call (CL_id (gs, CT_bool))] @ cond_cleanup @ [ijump loop_test loop_end_label] @ body_setup - @ [body_call (CL_id unit_gs)] + @ [body_call (CL_id (unit_gs, CT_unit))] @ body_cleanup @ [igoto loop_start_label])] @ [ilabel loop_end_label], - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] | AE_loop (Until, cond, body) -> let loop_start_label = label "repeat_" in let loop_end_label = label "until_" in - let cond_setup, _, cond_call, cond_cleanup = compile_aexp ctx cond in - let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = gensym () in let unit_gs = gensym () in let loop_test = (F_id gs, CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (body_setup - @ [body_call (CL_id unit_gs)] + @ [body_call (CL_id (unit_gs, CT_unit))] @ body_cleanup @ cond_setup - @ [cond_call (CL_id gs)] + @ [cond_call (CL_id (gs, CT_bool))] @ cond_cleanup @ [ijump loop_test loop_end_label] @ [igoto loop_start_label])] @ [ilabel loop_end_label], - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] @@ -1149,19 +1183,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let creturn = if ctyp_equal fn_return_ctyp (cval_ctyp cval) then [ireturn cval] - else if is_stack_ctyp (cval_ctyp cval) && not (is_stack_ctyp fn_return_ctyp) then - let gs1 = gensym () in - let gs2 = gensym () in - [idecl (cval_ctyp cval) gs1; - icopy (CL_id gs1) cval; - idecl fn_return_ctyp gs2; - iconvert (CL_id gs2) fn_return_ctyp gs1 (cval_ctyp cval); - ireturn (F_id gs2, fn_return_ctyp)] else - c_error ~loc:l "Can only do return type conversion from stack to heap" + let gs = gensym () in + [idecl fn_return_ctyp gs; + icopy (CL_id (gs, fn_return_ctyp)) cval; + ireturn (F_id gs, fn_return_ctyp)] in return_setup @ creturn, - ctyp_of_typ ctx typ, (fun clexp -> icomment "unreachable after return"), [] @@ -1169,7 +1197,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* Cleanup info will be handled by fix_exceptions *) let throw_setup, cval, _ = compile_aval ctx aval in throw_setup @ [ithrow cval], - ctyp_of_typ ctx typ, (fun clexp -> icomment "unreachable after throw"), [] @@ -1177,7 +1204,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctyp = ctyp_of_typ ctx typ in let setup, cval, cleanup = compile_aval ctx aval in setup, - ctyp, (fun clexp -> icopy clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), cleanup @@ -1198,43 +1224,37 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = in (* Loop variables *) - let from_setup, from_ctyp, from_call, from_cleanup = compile_aexp ctx loop_from in + let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in let from_gs = gensym () in - let to_setup, to_ctyp, to_call, to_cleanup = compile_aexp ctx loop_to in + let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in let to_gs = gensym () in - let step_setup, step_ctyp, step_call, step_cleanup = compile_aexp ctx loop_step in + let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in let step_gs = gensym () in - let variable_init gs setup ctyp call cleanup = + let variable_init gs setup call cleanup = [idecl CT_int64 gs; - if is_stack_ctyp ctyp then - iblock (setup @ [call (CL_id gs)] @ cleanup) - else - let gs' = gensym () in - iblock (setup - @ [idecl ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs'] - @ cleanup)] + iblock (setup @ [call (CL_id (gs, CT_int64))] @ cleanup)] in let loop_start_label = label "for_start_" in let loop_end_label = label "for_end_" in - let body_setup, _, body_call, body_cleanup = compile_aexp ctx body in + let body_setup, body_call, body_cleanup = compile_aexp ctx body in let body_gs = gensym () in - variable_init from_gs from_setup from_ctyp from_call from_cleanup - @ variable_init to_gs to_setup to_ctyp to_call to_cleanup - @ variable_init step_gs step_setup step_ctyp step_call step_cleanup + variable_init from_gs from_setup from_call from_cleanup + @ variable_init to_gs to_setup to_call to_cleanup + @ variable_init step_gs step_setup step_call step_cleanup @ [iblock ([idecl CT_int64 loop_var; - icopy (CL_id loop_var) (F_id from_gs, CT_int64); + icopy (CL_id (loop_var, CT_int64)) (F_id from_gs, CT_int64); idecl CT_unit body_gs; iblock ([ilabel loop_start_label] @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label] @ body_setup - @ [body_call (CL_id body_gs)] + @ [body_call (CL_id (body_gs, CT_unit))] @ body_cleanup - @ [icopy (CL_id loop_var) (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)] + @ [icopy (CL_id (loop_var, CT_int64)) + (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)] @ [igoto loop_start_label]); ilabel loop_end_label])], - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] @@ -1245,10 +1265,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = and compile_block ctx = function | [] -> [] | exp :: exps -> - let setup, _, call, cleanup = compile_aexp ctx exp in + let setup, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in let gs = gensym () in - iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest + iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest (** Compile a sail type definition into a IR one. Most of the actual work of translating the typedefs into C is done by the code @@ -1384,7 +1404,7 @@ let fix_early_stack_return ctx instrs = in rewrite_return [] instrs -let fix_exception_block ctx instrs = +let fix_exception_block ?return:(return=None) ctx instrs = let end_block_label = label "end_block_exception_" in let is_exception_stop (I_aux (instr, _)) = match instr with @@ -1409,12 +1429,12 @@ let fix_exception_block ctx instrs = @ rewrite_exception historic after | before, I_aux (I_throw cval, _) :: after -> before - @ [icopy CL_current_exception cval; + @ [icopy (CL_current_exception (cval_ctyp cval)) cval; icopy CL_have_exception (F_lit (V_bool true), CT_bool)] @ generate_cleanup (historic @ before) @ [igoto end_block_label] @ rewrite_exception (historic @ before) after - | before, (I_aux (I_funcall (x, _, f, args, ctyp), _) as funcall) :: after -> + | before, (I_aux (I_funcall (x, _, f, args), _) as funcall) :: after -> let effects = match Env.get_val_spec f ctx.tc_env with | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *) @@ -1429,24 +1449,27 @@ let fix_exception_block ctx instrs = before @ funcall :: rewrite_exception (historic @ before) after | _, _ -> assert false (* unreachable *) in - rewrite_exception [] instrs - @ [ilabel end_block_label] - + match return with + | None -> + rewrite_exception [] instrs @ [ilabel end_block_label] + | Some ctyp -> + rewrite_exception [] instrs @ [ilabel end_block_label; iundefined ctyp] + let rec map_try_block f (I_aux (instr, aux)) = let instr = match instr with | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr | I_if (cval, instrs1, instrs2, ctyp) -> I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp) - | I_funcall _ | I_convert _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr + | I_funcall _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr | I_block instrs -> I_block (List.map (map_try_block f) instrs) | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs)) - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ -> instr in I_aux (instr, aux) -let fix_exception ctx instrs = +let fix_exception ?return:(return=None) ctx instrs = let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in - fix_exception_block ctx instrs + fix_exception_block ~return:return ctx instrs let rec arg_pats ctx (Typ_aux (arg_typ_aux, _) as arg_typ) (P_aux (p_aux, (l, _)) as pat) = match p_aux, arg_typ_aux with @@ -1466,7 +1489,7 @@ let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat, ctyp) = | _ -> let apat = anf_pat pat in let gs = gensym () in - let destructure, cleanup = compile_match ctx apat (F_id gs, ctyp) label in + let destructure, cleanup, _ = compile_match ctx apat (F_id gs, ctyp) label in (gs, (destructure, cleanup)) let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs)) @@ -1484,9 +1507,9 @@ let rec compile_def ctx = function | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) -> [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> - let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id id)] @ cleanup in + let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in + let setup, call, cleanup = compile_aexp ctx aexp in + let instrs = setup @ [call (CL_id (id, ctyp_of_typ ctx typ))] @ cleanup in [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> @@ -1503,30 +1526,57 @@ let rec compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> c_debug (lazy ("Compiling function " ^ string_of_id id)); - let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - c_debug (lazy "Compiled aexp"); - let fundef_label = label "fundef_fail_" in - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + (* Find the function's type *) + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env + with Type_error _ -> + c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env + in let arg_typ, ret_typ = match fn_typ with | Typ_fn (arg_typ, ret_typ, _) -> arg_typ, ret_typ | _ -> assert false in - let compiled_args = List.map (compile_arg_pat ctx fundef_label) (arg_pats ctx arg_typ pat) in + + (* Handle the argument pattern *) + let fundef_label = label "fundef_fail_" in + let orig_ctx = ctx in + let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + let compiled_args' = arg_pats ctx arg_typ pat in + let compiled_args = List.map (compile_arg_pat ctx fundef_label) compiled_args' in + let ctx = + (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) + List.fold_left2 (fun ctx (id, _) (_, ctyp) -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args compiled_args' + in + + if string_of_id id = "TLBTranslateC" then c_verbosity := 1 else (); + + (* Optimize and compile the expression *) + let aexp = no_shadow (pat_ids pat) (anf exp) in + c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); + let aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) in + c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); + let setup, call, cleanup = compile_aexp ctx aexp in + c_debug (lazy "Compiled aexp"); let gs = gensym () in let destructure, destructure_cleanup = compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label in - if is_stack_ctyp ctyp then - let instrs = destructure @ [idecl ctyp gs] @ setup @ [call (CL_id gs)] @ cleanup @ destructure_cleanup @ [ireturn (F_id gs, ctyp)] in + + c_verbosity := 0; + + (* This better be true or something has gone badly wrong. *) + let ret_ctyp = ctyp_of_typ ctx ret_typ in + + if is_stack_ctyp ret_ctyp then + let instrs = destructure @ [idecl ret_ctyp gs] @ setup @ [call (CL_id (gs, ret_ctyp))] @ cleanup @ destructure_cleanup @ [ireturn (F_id gs, ret_ctyp)] in let instrs = fix_early_stack_return ctx instrs in - let instrs = fix_exception ctx instrs in - [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], ctx + let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx else - let instrs = destructure @ setup @ [call (CL_addr gs)] @ cleanup @ destructure_cleanup in - let instrs = fix_early_return (CL_addr gs) ctx instrs in + let instrs = destructure @ setup @ [call (CL_addr (gs, ret_ctyp))] @ cleanup @ destructure_cleanup in + let instrs = fix_early_return (CL_addr (gs, ret_ctyp)) ctx instrs in let instrs = fix_exception ctx instrs in - [CDEF_fundef (id, Some gs, List.map fst compiled_args, instrs)], ctx + [CDEF_fundef (id, Some gs, List.map fst compiled_args, instrs)], orig_ctx | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> c_error ~loc:l "Encountered function with no clauses" @@ -1543,14 +1593,15 @@ let rec compile_def ctx = function | DEF_val (LB_aux (LB_val (pat, exp), _)) -> c_debug (lazy ("Compiling letbind " ^ string_of_pat pat)); - let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in + let ctyp = ctyp_of_typ ctx (pat_typ_of pat) in + let aexp = analyze_functions ctx analyze_primop (c_literals ctx (no_shadow IdSet.empty (anf exp))) in + let setup, call, cleanup = compile_aexp ctx aexp in let apat = anf_pat ~global:true pat in let gs = gensym () in let end_label = label "let_end_" in - let destructure, destructure_cleanup = compile_match ctx apat (F_id gs, ctyp) end_label in + let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in let gs_setup, gs_cleanup = - [idecl ctyp gs], [iclear ctyp gs] + [idecl ctyp gs], [iclear ctyp gs] in let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in let n = !letdef_count in @@ -1558,7 +1609,7 @@ let rec compile_def ctx = function let instrs = [icomment "gs_setup"] @ gs_setup @ [icomment "setup"] @ setup @ [icomment "call"] - @ [call (CL_id gs)] + @ [call (CL_id (gs, ctyp))] @ [icomment "cleanup"] @ cleanup @ [icomment "destructure"] @@ -1618,11 +1669,11 @@ let add_local_labels instrs = let clexp_rename from_id to_id = let rename id = if Id.compare id from_id = 0 then to_id else id in function - | CL_id id -> CL_id (rename id) - | CL_field (id, field) -> CL_field (rename id, field) - | CL_addr id -> CL_addr (rename id) - | CL_addr_field (id, field) -> CL_addr_field (rename id, field) - | CL_current_exception -> CL_current_exception + | CL_id (id, ctyp) -> CL_id (rename id, ctyp) + | CL_field (id, field, ctyp) -> CL_field (rename id, field, ctyp) + | CL_addr (id, ctyp) -> CL_addr (rename id, ctyp) + | CL_addr_field (id, field, ctyp) -> CL_addr_field (rename id, field, ctyp) + | CL_current_exception ctyp -> CL_current_exception ctyp | CL_have_exception -> CL_have_exception let rec instrs_rename from_id to_id = @@ -1639,17 +1690,15 @@ let rec instrs_rename from_id to_id = | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs -> I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs - | I_aux (I_funcall (clexp, extern, id, cvals, ctyp), aux) :: instrs -> - I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals, ctyp), aux) :: irename instrs + | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs -> + I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs - | I_aux (I_convert (clexp, ctyp1, id, ctyp2), aux) :: instrs -> - I_aux (I_convert (lrename clexp, ctyp1, rename id, ctyp2), aux) :: irename instrs | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs - | (I_aux ((I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure), _) as instr) :: instrs -> instr :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs | [] -> [] let hoist_ctyp = function @@ -1750,6 +1799,7 @@ let flatten_instrs ctx = | cdef -> [cdef] + (* (* When this optimization fires we know we have bytecode of the form recreate x : S; x = y; ... @@ -1762,18 +1812,18 @@ let flatten_instrs ctx = let fix_struct_updates ctx = (* FIXME need to check no remaining references *) let rec fix_updates struct_id id = function - | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs + | I_aux (I_copy (CL_field (struct_id', field, ctyp), cval), aux) :: instrs when Id.compare struct_id struct_id' = 0 -> - Util.option_map (fun instrs -> I_aux (I_copy (CL_field (id, field), cval), aux) :: instrs) (fix_updates struct_id id instrs) + Util.option_map (fun instrs -> I_aux (I_copy (CL_field (id, field, ctyp), cval), aux) :: instrs) (fix_updates struct_id id instrs) | I_aux (I_copy (CL_id id', (F_id struct_id', ctyp)), aux) :: instrs when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0-> Some instrs | _ -> None in let rec fix_updates_ret struct_id id = function - | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs + | I_aux (I_copy (CL_field (struct_id', field, ctyp), cval), aux) :: instrs when Id.compare struct_id struct_id' = 0 -> - Util.option_map (fun instrs -> I_aux (I_copy (CL_addr_field (id, field), cval), aux) :: instrs) (fix_updates_ret struct_id id instrs) + Util.option_map (fun instrs -> I_aux (I_copy (CL_addr_field (id, field, ctyp), cval), aux) :: instrs) (fix_updates_ret struct_id id instrs) | I_aux (I_copy (CL_addr id', (F_id struct_id', ctyp)), aux) :: instrs when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0-> Some instrs @@ -1781,10 +1831,9 @@ let fix_struct_updates ctx = in let rec opt hr = function | (I_aux (I_reset (ctyp, struct_id), _) as instr1) - :: (I_aux (I_copy (CL_id struct_id', (F_id id, ctyp')), _) as instr2) + :: (I_aux (I_copy (CL_id (struct_id', _), (F_id id, ctyp')), _) as instr2) :: instrs when is_ct_struct ctyp && ctyp_equal ctyp ctyp' && Id.compare struct_id struct_id' = 0 -> - prerr_endline ("Potential struct update " ^ string_of_id struct_id); begin match fix_updates struct_id id instrs with | None -> instr1 :: instr2 :: opt hr instrs | Some updated -> opt hr updated @@ -1793,7 +1842,6 @@ let fix_struct_updates ctx = | (I_aux (I_reset (ctyp, struct_id), _) as instr) :: instrs when is_ct_struct ctyp && Util.is_some hr -> let id = match hr with Some id -> id | None -> assert false in - prerr_endline ("Potential struct return " ^ string_of_id struct_id ^ " to " ^ string_of_id id); begin match fix_updates_ret struct_id id instrs with | None -> instr :: opt hr instrs | Some updated -> opt hr updated @@ -1811,6 +1859,7 @@ let fix_struct_updates ctx = | CDEF_fundef (function_id, heap_return, args, body) -> [CDEF_fundef (function_id, heap_return, args, opt heap_return body)] | cdef -> [cdef] + *) let concatMap f xs = List.concat (List.map f xs) @@ -1818,7 +1867,7 @@ let optimize ctx cdefs = let nothing cdefs = cdefs in cdefs |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing) - |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing) +(* |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing) *) (**************************************************************************) (* 6. Code generation *) @@ -1878,22 +1927,22 @@ let sgen_cval_param (frag, ctyp) = let sgen_cval = function (frag, _) -> string_of_fragment frag let sgen_clexp = function - | CL_id id -> "&" ^ sgen_id id - | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ Util.zencode_string field ^ ")" - | CL_addr id -> sgen_id id - | CL_addr_field (id, field) -> "&(" ^ sgen_id id ^ "->" ^ Util.zencode_string field ^ ")" + | CL_id (id, _) -> "&" ^ sgen_id id + | CL_field (id, field, _) -> "&(" ^ sgen_id id ^ "." ^ Util.zencode_string field ^ ")" + | CL_addr (id, _) -> sgen_id id + | CL_addr_field (id, field, _) -> "&(" ^ sgen_id id ^ "->" ^ Util.zencode_string field ^ ")" | CL_have_exception -> "have_exception" - | CL_current_exception -> "current_exception" + | CL_current_exception _ -> "current_exception" let sgen_clexp_pure = function - | CL_id id -> sgen_id id - | CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field - | CL_addr id -> "*" ^ sgen_id id - | CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field + | CL_id (id, _) -> sgen_id id + | CL_field (id, field, _) -> sgen_id id ^ "." ^ Util.zencode_string field + | CL_addr (id, _) -> "*" ^ sgen_id id + | CL_addr_field (id, field, _) -> sgen_id id ^ "->" ^ Util.zencode_string field | CL_have_exception -> "have_exception" - | CL_current_exception -> "current_exception" + | CL_current_exception _ -> "current_exception" -let rec codegen_instr fid ctx (I_aux (instr, _)) = +let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = match instr with | I_decl (ctyp, id) when is_stack_ctyp ctyp -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) @@ -1902,11 +1951,30 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = ^^ string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) | I_copy (clexp, cval) -> - let ctyp = cval_ctyp cval in - if is_stack_ctyp ctyp then - string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) + let lctyp = clexp_ctyp clexp in + let rctyp = cval_ctyp cval in + if ctyp_equal lctyp rctyp then + if is_stack_ctyp lctyp then + string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) + else + string (Printf.sprintf " COPY(%s)(%s, %s);" (sgen_ctyp_name lctyp) (sgen_clexp clexp) (sgen_cval cval)) + else if pointer_assign lctyp rctyp then + let lctyp = match lctyp with + | CT_ref lctyp -> lctyp + | _ -> assert false + in + if is_stack_ctyp lctyp then + string (Printf.sprintf " *(%s) = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) + else + string (Printf.sprintf " COPY(%s)(*(%s), %s);" (sgen_ctyp_name lctyp) (sgen_clexp clexp) (sgen_cval cval)) else - string (Printf.sprintf " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval)) + if is_stack_ctyp lctyp then + string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" + (sgen_clexp_pure clexp) (sgen_ctyp_name lctyp) (sgen_ctyp_name rctyp) (sgen_cval cval)) + else + string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s);" + (sgen_ctyp_name lctyp) (sgen_ctyp_name rctyp) (sgen_clexp clexp) (sgen_cval cval)) + | I_jump (cval, label) -> string (Printf.sprintf " if (%s) goto %s;" (sgen_cval cval) label) | I_if (cval, [then_instr], [], ctyp) -> @@ -1928,8 +1996,9 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string " { /* try */" ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline ^^ string " }" - | I_funcall (x, extern, f, args, ctyp) -> + | I_funcall (x, extern, f, args) -> let c_args = Util.string_of_list ", " sgen_cval args in + let ctyp = clexp_ctyp x in let fname = if Env.is_extern f ctx.tc_env "c" then Env.get_extern f ctx.tc_env "c" @@ -1975,10 +2044,11 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args) else string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) - else if is_stack_ctyp ctyp then - string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) else - string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) + if is_stack_ctyp ctyp then + string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) + else + string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) | I_clear (ctyp, id) when is_stack_ctyp ctyp -> empty @@ -2009,70 +2079,54 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = | I_reset (ctyp, id) -> string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) - (* FIXME: This just covers the cases we see in our specs, need a - special conversion code-generator for full generality *) - | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> - let convert i (ctyp1, ctyp2) = - if ctyp_equal ctyp1 ctyp2 then - string (Printf.sprintf " %s.ztup%i = %s.ztup%i;" (sgen_clexp_pure x) i (sgen_id y) i) - else if ctyp_equal ctyp1 ctyp2 then - c_error "heap tuple type conversion" - else if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s.ztup%i = CONVERT_OF(%s, %s)(%s.ztup%i);" - (sgen_clexp_pure x) - i - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_id y) - i) - else - string (Printf.sprintf " CONVERT_OF(%s, %s)(%s.ztup%i, %s.ztup%i);" - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_clexp x) - i - (sgen_id y) - i) - in - separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2)) - (* If we're converting from a bits type with a known compile time - length, pass it as an extra parameter to the conversion. *) - | I_convert (x, ctyp1, y, (CT_bits64 (n, _) as ctyp2)) -> - if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s, %d);" - (sgen_clexp_pure x) - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_id y) - n) - else - string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s, %d);" - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_clexp x) - (sgen_id y) - n) - | I_convert (x, ctyp1, y, ctyp2) -> - if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" - (sgen_clexp_pure x) - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_id y)) - else - string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s);" - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_clexp x) - (sgen_id y)) | I_return cval -> string (Printf.sprintf " return %s;" (sgen_cval cval)) + | I_throw cval -> c_error "I_throw reached code generator" + + | I_undefined ctyp -> + let rec codegen_exn_return ctyp = + match ctyp with + | CT_unit -> "UNIT", [] + | CT_bit -> "UINT64_C(0)", [] + | CT_int64 -> "INT64_C(0xdeadc0de)", [] + | CT_bits64 _ -> "UINT64_C(0xdeadc0de)", [] + | CT_bool -> "false", [] + | CT_enum (_, ctor :: _) -> sgen_id ctor, [] + | CT_tup ctyps when is_stack_ctyp ctyp -> + let gs = gensym () in + let fold (inits, prev) (n, ctyp) = + let init, prev' = codegen_exn_return ctyp in + Printf.sprintf ".ztup%d = %s" n init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in + sgen_id gs, + [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | CT_struct (id, ctors) when is_stack_ctyp ctyp -> + let gs = gensym () in + let fold (inits, prev) (id, ctyp) = + let init, prev' = codegen_exn_return ctyp in + Printf.sprintf ".%s = %s" (sgen_id id) init :: inits, prev @ prev' + in + let inits, prev = List.fold_left fold ([], []) ctors in + sgen_id gs, + [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | ctyp -> c_error ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp) + in + let ret, prev = codegen_exn_return ctyp in + separate_map hardline (fun str -> string (" " ^ str)) (List.rev prev) + ^^ hardline + ^^ string (Printf.sprintf " return %s;" ret) + | I_comment str -> string (" /* " ^ str ^ " */") + | I_label str -> string (str ^ ": ;") + | I_goto str -> string (Printf.sprintf " goto %s;" str) @@ -2084,17 +2138,26 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") let codegen_type_def ctx = function - | CTD_enum (id, ids) -> + | CTD_enum (id, ((first_id :: _) as ids)) -> let codegen_eq = let name = sgen_id id in string (Printf.sprintf "static bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name) in + let codegen_undefined = + let name = sgen_id id in + string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (upper_sgen_id first_id)) + in string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id ids; rbrace ^^ semi] ^^ twice hardline ^^ codegen_eq + ^^ twice hardline + ^^ codegen_undefined + + | CTD_enum (id, []) -> c_error ("Cannot compile empty enum " ^ string_of_id id) | CTD_struct (id, ctors) -> + let struct_ctyp = CT_struct (id, ctors) in (* Generate a set_T function for every struct T *) let codegen_set (id, ctyp) = if is_stack_ctyp ctyp then @@ -2143,12 +2206,14 @@ let codegen_type_def ctx = function rbrace ^^ semi ^^ twice hardline ^^ codegen_setter id (ctor_bindings ctors) - ^^ twice hardline - ^^ codegen_init "CREATE" id (ctor_bindings ctors) - ^^ twice hardline - ^^ codegen_init "RECREATE" id (ctor_bindings ctors) - ^^ twice hardline - ^^ codegen_init "KILL" id (ctor_bindings ctors) + ^^ (if not (is_stack_ctyp struct_ctyp) then + twice hardline + ^^ codegen_init "CREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "RECREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "KILL" id (ctor_bindings ctors) + else empty) ^^ twice hardline ^^ codegen_eq @@ -2209,7 +2274,10 @@ let codegen_type_def ctx = function | CT_tup ctyps -> String.concat ", " (List.mapi (fun i ctyp -> Printf.sprintf "%s op%d" (sgen_ctyp ctyp) i) ctyps), string (Printf.sprintf "%s op;" (sgen_ctyp ctyp)) ^^ hardline - ^^ string (Printf.sprintf "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline + ^^ if not (is_stack_ctyp ctyp) then + string (Printf.sprintf "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline + else + empty ^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline | ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty in @@ -2651,12 +2719,12 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false + (* let instrument_tracing ctx = let module StringSet = Set.Make(String) in let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in let rec instrument = function - | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs when not (Env.is_extern id ctx.tc_env "c") -> - + | (I_aux (I_funcall (clexp, _, id, args), _) as instr) :: instrs -> let trace_start = iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id))) in @@ -2702,6 +2770,7 @@ let instrument_tracing ctx = | CDEF_fundef (function_id, heap_return, args, body) -> CDEF_fundef (function_id, heap_return, args, instrument body) | cdef -> cdef + *) let bytecode_ast ctx rewrites (Defs defs) = let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in @@ -2753,8 +2822,9 @@ let compile_ast ctx (Defs defs) = let cdefs = List.concat (List.rev chunks) in let cdefs = optimize ctx cdefs in + (* let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in - + *) let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline diff --git a/src/monomorphise.ml b/src/monomorphise.ml index f4f28c41..7886fe6b 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -1591,6 +1591,31 @@ let split_defs all_errors splits defs = (Reporting_basic.print_err false true l' "Monomorphisation" "Unexpected kind of pattern for literal"; GiveUp) in findpat_generic checkpat "literal" assigns cases + | E_vector es when List.for_all (function (E_aux (E_lit _,_)) -> true | _ -> false) es -> + let checkpat = function + | P_aux (P_vector ps,_) -> + let matches = List.map2 (fun e p -> + match e, p with + | E_aux (E_lit (L_aux (lit,_)),_), P_aux (P_lit (L_aux (lit',_)),_) -> + if lit_match (lit,lit') then DoesMatch ([],[]) else DoesNotMatch + | E_aux (E_lit l,_), P_aux (P_id var,_) when pat_id_is_variable env var -> + DoesMatch ([var, e],[]) + | _ -> GiveUp) es ps in + let final = List.fold_left (fun acc m -> match acc, m with + | _, GiveUp -> GiveUp + | GiveUp, _ -> GiveUp + | DoesMatch (sub,ksub), DoesMatch(sub',ksub') -> DoesMatch(sub@sub',ksub@ksub') + | _ -> DoesNotMatch) (DoesMatch ([],[])) matches in + (match final with + | GiveUp -> + (Reporting_basic.print_err false true l "Monomorphisation" + "Unexpected kind of pattern for vector literal"; GiveUp) + | _ -> final) + | _ -> + (Reporting_basic.print_err false true l "Monomorphisation" + "Unexpected kind of pattern for vector literal"; GiveUp) + in findpat_generic checkpat "vector literal" assigns cases + | E_cast (undef_typ, (E_aux (E_lit (L_aux (L_undef, lit_l)),_) as e_undef)) -> let checkpat = function | P_aux (P_lit (L_aux (lit_p, _)),_) -> DoesNotMatch @@ -1780,21 +1805,31 @@ let split_defs all_errors splits defs = otherwise *) | Some (Some (pats,l)) -> let max = List.length pats - 1 in + let lit_like = function + | P_lit _ -> true + | P_vector ps -> List.for_all (function P_aux (P_lit _,_) -> true | _ -> false) ps + | _ -> false + in + let rec to_exp = function + | P_aux (P_lit lit,(l,ann)) -> E_aux (E_lit lit,(Generated l,ann)) + | P_aux (P_vector ps,(l,ann)) -> E_aux (E_vector (List.map to_exp ps),(Generated l,ann)) + | _ -> assert false + in Some (List.mapi (fun i p -> match p with - | P_aux (P_lit lit,(pl,pannot)) - when (match lit with L_aux (L_undef,_) -> false | _ -> true) -> + | P_aux (P_lit (L_aux (L_num j,_) as lit),(pl,pannot)) -> let orig_typ = Env.base_typ_of (env_of_annot (l,annot)) (typ_of_annot (l,annot)) in - let kid_subst = match lit, orig_typ with - | L_aux (L_num i,_), - Typ_aux + let kid_subst = match orig_typ with + | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var var,_)),_)]),_) -> - [var,nconstant i] + [var,nconstant j] | _ -> [] in p,[id,E_aux (E_lit lit,(Generated pl,pannot))],[l,(i,max,[])],kid_subst + | P_aux (p',(pl,pannot)) when lit_like p' -> + p,[id,to_exp p],[l,(i,max,[])],[] | _ -> let p',subst = freshen_pat_bindings p in match p' with @@ -4193,12 +4228,8 @@ let rewrite_toplevel_nexps (Defs defs) = type options = { auto : bool; debug_analysis : int; - rewrites : bool; - rewrite_toplevel_nexps : bool; - rewrite_size_parameters : bool; all_split_errors : bool; - continue_anyway : bool; - dump_raw: bool + continue_anyway : bool } let recheck defs = @@ -4208,18 +4239,10 @@ let recheck defs = let () = Util.opt_warnings := w in r -let monomorphise opts splits env defs = - let (defs,env) = - if opts.rewrites then - let defs = MonoRewrites.mono_rewrite defs in - recheck defs - else defs,env - in - let defs,env = - if opts.rewrite_toplevel_nexps - then recheck (rewrite_toplevel_nexps defs) - else defs,env - in +let mono_rewrites = MonoRewrites.mono_rewrite + +let monomorphise opts splits defs = + let defs, env = Type_check.check Type_check.initial_env defs in let ok_analysis, new_splits, extra_splits = if opts.auto then @@ -4239,18 +4262,9 @@ let monomorphise opts splits env defs = let () = if (ok_analysis && ok_extras && ok_split) || opts.continue_anyway then () else raise (Reporting_basic.err_general Unknown "Unable to monomorphise program") - in - let defs,env = recheck defs in - let defs = BitvectorSizeCasts.add_bitvector_casts defs in - (* TODO: currently doing this because constant propagation leaves numeric literals as - int, try to avoid this later; also use final env for DEF_spec case above, because the - type checker doesn't store the env at that point :( *) - let defs = if opts.rewrite_size_parameters then - let (defs,env) = recheck defs in - let defs = AtomToItself.rewrite_size_parameters env defs in - defs - else - defs - in - let () = if opts.dump_raw then Pretty_print_sail.pp_defs stdout defs else () in - recheck defs + in defs + +let add_bitvector_casts = BitvectorSizeCasts.add_bitvector_casts +let rewrite_atoms_to_singletons defs = + let defs, env = Type_check.check Type_check.initial_env defs in + AtomToItself.rewrite_size_parameters env defs diff --git a/src/monomorphise.mli b/src/monomorphise.mli index 3baa7d12..1a82c8d0 100644 --- a/src/monomorphise.mli +++ b/src/monomorphise.mli @@ -51,17 +51,24 @@ type options = { auto : bool; (* Analyse ast to find splits for monomorphisation *) debug_analysis : int; (* Debug output level for the automatic analysis *) - rewrites : bool; (* Experimental rewrites for variable-sized operations *) - rewrite_toplevel_nexps : bool; (* Move complex nexps in function signatures into constraints *) - rewrite_size_parameters : bool; (* Make implicit type parameters explicit for (e.g.) lem *) all_split_errors : bool; - continue_anyway : bool; - dump_raw: bool + continue_anyway : bool } val monomorphise : options -> ((string * int) * string) list -> (* List of splits from the command line *) - Type_check.Env.t -> Type_check.tannot Ast.defs -> - Type_check.tannot Ast.defs * Type_check.Env.t + Type_check.tannot Ast.defs + +(* Rewrite (combinations of) variable-sized operations into fixed-sized operations *) +val mono_rewrites : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs + +(* Move complex nexps in function signatures into constraints *) +val rewrite_toplevel_nexps : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs + +(* Add casts across case splits *) +val add_bitvector_casts : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs + +(* Replace atom arguments which are fixed by a type parameter for a size with a singleton type *) +val rewrite_atoms_to_singletons : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs diff --git a/src/pattern_completeness.ml b/src/pattern_completeness.ml index 2372ea82..acd925bf 100644 --- a/src/pattern_completeness.ml +++ b/src/pattern_completeness.ml @@ -53,7 +53,7 @@ open Ast_util module Big_int = Nat_big_num type ctx = - { lookup_id : id -> lvar; + { lookup_id : id -> typ lvar; enums : IdSet.t Bindings.t; variants : IdSet.t Bindings.t } diff --git a/src/pattern_completeness.mli b/src/pattern_completeness.mli index c26a63a8..83d6d54c 100644 --- a/src/pattern_completeness.mli +++ b/src/pattern_completeness.mli @@ -52,7 +52,7 @@ open Ast open Ast_util type ctx = - { lookup_id : id -> lvar; + { lookup_id : id -> typ lvar; enums : IdSet.t Bindings.t; variants : IdSet.t Bindings.t } diff --git a/src/process_file.ml b/src/process_file.ml index c3e1b510..6afbae3d 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -232,27 +232,6 @@ let check_ast (env : Type_check.Env.t) (defs : unit Ast.defs) : Type_check.tanno let () = if !opt_just_check then exit 0 else () in (ast, env) -let opt_ddump_raw_mono_ast = ref false -let opt_dmono_analysis = ref 0 -let opt_auto_mono = ref false -let opt_mono_rewrites = ref false -let opt_mono_complex_nexps = ref true -let opt_dall_split_errors = ref false -let opt_dmono_continue = ref false - -let monomorphise_ast locs type_env ast = - let open Monomorphise in - let opts = { - auto = !opt_auto_mono; - debug_analysis = !opt_dmono_analysis; - rewrites = !opt_mono_rewrites; - rewrite_toplevel_nexps = !opt_mono_complex_nexps; - rewrite_size_parameters = !Pretty_print_lem.opt_mwords; - all_split_errors = !opt_dall_split_errors; - continue_anyway = !opt_dmono_continue; - dump_raw = !opt_ddump_raw_mono_ast - } in - monomorphise opts locs type_env ast let open_output_with_check file_name = let (temp_file_name, o) = Filename.open_temp_file "ll_temp" "" in diff --git a/src/process_file.mli b/src/process_file.mli index 0fec4064..a4e31890 100644 --- a/src/process_file.mli +++ b/src/process_file.mli @@ -52,7 +52,6 @@ val parse_file : string -> Parse_ast.defs val convert_ast : Ast.order -> Parse_ast.defs -> unit Ast.defs val preprocess_ast : Parse_ast.defs -> Parse_ast.defs val check_ast: Type_check.Env.t -> unit Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t -val monomorphise_ast : ((string * int) * string) list -> Type_check.Env.t -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs * Type_check.Env.t val rewrite_ast: Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_undefined: bool -> Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs val rewrite_ast_lem : Type_check.tannot Ast.defs -> Type_check.tannot Ast.defs @@ -69,13 +68,6 @@ val opt_just_check : bool ref val opt_ddump_tc_ast : bool ref val opt_ddump_rewrite_ast : ((string * int) option) ref val opt_dno_cast : bool ref -val opt_ddump_raw_mono_ast : bool ref -val opt_dmono_analysis : int ref -val opt_dmono_continue : bool ref -val opt_auto_mono : bool ref -val opt_mono_rewrites : bool ref -val opt_mono_complex_nexps : bool ref -val opt_dall_split_errors : bool ref type out_type = | Lem_ast_out diff --git a/src/rewrites.ml b/src/rewrites.ml index 246a2670..2faebf9c 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2336,6 +2336,11 @@ let rewrite_undefined mwords = let rewrite_exp_undefined = { id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux (E_aux (exp, annot))) } in rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp rewrite_exp_undefined) } +let rewrite_undefined_if_gen always_bitvector defs = + if !Initial_check.opt_undefined_gen + then rewrite_undefined (always_bitvector || !Pretty_print_lem.opt_mwords) defs + else defs + let rec simple_typ (Typ_aux (typ_aux, l) as typ) = Typ_aux (simple_typ_aux typ_aux, l) and simple_typ_aux = function | Typ_id id -> Typ_id id @@ -4269,11 +4274,54 @@ let remove_mapping_valspecs (Defs defs) = Defs (List.filter allowed_def defs) +let opt_mono_rewrites = ref false +let opt_mono_complex_nexps = ref true + +let mono_rewrites defs = + if !opt_mono_rewrites then + Monomorphise.mono_rewrites defs + else defs + +let rewrite_toplevel_nexps defs = + if !opt_mono_complex_nexps then + Monomorphise.rewrite_toplevel_nexps defs + else defs + +let opt_mono_split = ref ([]:((string * int) * string) list) +let opt_dmono_analysis = ref 0 +let opt_auto_mono = ref false +let opt_dall_split_errors = ref false +let opt_dmono_continue = ref false + +let monomorphise defs = + let open Monomorphise in + monomorphise + { auto = !opt_auto_mono; + debug_analysis = !opt_dmono_analysis; + all_split_errors = !opt_dall_split_errors; + continue_anyway = !opt_dmono_continue } + !opt_mono_split + defs + +let if_mono f defs = + match !opt_mono_split, !opt_auto_mono with + | [], false -> defs + | _, _ -> f defs + let rewrite_defs_lem = [ ("realise_mappings", rewrite_defs_realise_mappings); ("remove_mapping_valspecs", remove_mapping_valspecs); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("mono_rewrites", mono_rewrites); + ("recheck_defs", if_mono recheck_defs); + ("rewrite_toplevel_nexps", if_mono rewrite_toplevel_nexps); + ("monomorphise", if_mono monomorphise); + ("recheck_defs", if_mono recheck_defs); + ("add_bitvector_casts", if_mono Monomorphise.add_bitvector_casts); + ("rewrite_atoms_to_singletons", if_mono Monomorphise.rewrite_atoms_to_singletons); + ("recheck_defs", if_mono recheck_defs); + ("rewrite_undefined", rewrite_undefined_if_gen false); ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4311,6 +4359,7 @@ let rewrite_defs_coq = [ ("remove_mapping_valspecs", remove_mapping_valspecs); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("rewrite_undefined", rewrite_undefined_if_gen true); ("pat_lits", rewrite_defs_pat_lits rewrite_lit_lem); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4351,6 +4400,7 @@ let rewrite_defs_ocaml = [ ("realise_mappings", rewrite_defs_realise_mappings); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("rewrite_undefined", rewrite_undefined_if_gen false); ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4373,6 +4423,7 @@ let rewrite_defs_c = [ ("realise_mappings", rewrite_defs_realise_mappings); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("rewrite_undefined", rewrite_undefined_if_gen false); ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); @@ -4393,6 +4444,7 @@ let rewrite_defs_interpreter = [ ("realise_mappings", rewrite_defs_realise_mappings); ("pat_string_append", rewrite_defs_pat_string_append); ("mapping_builtins", rewrite_defs_mapping_patterns); + ("rewrite_undefined", rewrite_undefined_if_gen false); ("vector_concat_assignments", rewrite_vector_concat_assignments); ("tuple_assignments", rewrite_tuple_assignments); ("simple_assignments", rewrite_simple_assignments); diff --git a/src/rewrites.mli b/src/rewrites.mli index 7d6bc0b2..aa793cb4 100644 --- a/src/rewrites.mli +++ b/src/rewrites.mli @@ -51,6 +51,15 @@ open Ast open Type_check +(* Monomorphisation options *) +val opt_mono_rewrites : bool ref +val opt_mono_complex_nexps : bool ref +val opt_mono_split : ((string * int) * string) list ref +val opt_dmono_analysis : int ref +val opt_auto_mono : bool ref +val opt_dall_split_errors : bool ref +val opt_dmono_continue : bool ref + (* Generate a fresh id with the given prefix *) val fresh_id : string -> l -> id diff --git a/src/sail.ml b/src/sail.ml index f0903146..8cc60e2c 100644 --- a/src/sail.ml +++ b/src/sail.ml @@ -70,7 +70,6 @@ let opt_sanity = ref false let opt_libs_lem = ref ([]:string list) let opt_libs_coq = ref ([]:string list) let opt_file_arguments = ref ([]:string list) -let opt_mono_split = ref ([]:((string * int) * string) list) let opt_process_elf : string option ref = ref None let options = Arg.align ([ @@ -115,9 +114,6 @@ let options = Arg.align ([ Arg.Set Type_check.opt_no_effects; Arg.Set C_backend.optimize_struct_updates ], " turn on optimizations for C compilation"); - ( "-Oz3", - Arg.Set C_backend.optimize_z3, - " use z3 analysis for optimization (experimental)"); ( "-Oconstant_fold", Arg.Set Constant_fold.optimize_constant_fold, " Apply constant folding optimizations"); @@ -161,19 +157,10 @@ let options = Arg.align ([ Arg.String (fun s -> let l = Util.split_on_char ':' s in match l with - | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split + | [fname;line;var] -> + Rewrites.opt_mono_split := ((fname,int_of_string line),var)::!Rewrites.opt_mono_split | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), "<filename>:<line>:<variable> to case split for monomorphisation"); - (* AA: Should use _ to be consistent with other options, but I keep - this case to make sure nothing breaks immediately. *) - ( "-mono-split", - Arg.String (fun s -> - prerr_endline (("Warning" |> Util.yellow |> Util.clear) ^ ": use -mono_split instead"); - let l = Util.split_on_char ':' s in - match l with - | [fname;line;var] -> opt_mono_split := ((fname,int_of_string line),var)::!opt_mono_split - | _ -> raise (Arg.Bad (s ^ " not of form <filename>:<line>:<variable>"))), - "<filename>:<line>:<variable> to case split for monomorphisation"); ( "-memo_z3", Arg.Set opt_memo_z3, " memoize calls to z3, improving performance when typechecking repeatedly"); @@ -192,26 +179,23 @@ let options = Arg.align ([ ( "-just_check", Arg.Set opt_just_check, " (experimental) terminate immediately after typechecking"); - ( "-ddump_raw_mono_ast", - Arg.Set opt_ddump_raw_mono_ast, - " (debug) dump the monomorphised ast before type-checking"); ( "-dmono_analysis", - Arg.Set_int opt_dmono_analysis, + Arg.Set_int Rewrites.opt_dmono_analysis, " (debug) dump information about monomorphisation analysis: 0 silent, 3 max"); ( "-auto_mono", - Arg.Set opt_auto_mono, + Arg.Set Rewrites.opt_auto_mono, " automatically infer how to monomorphise code"); ( "-mono_rewrites", - Arg.Set Process_file.opt_mono_rewrites, + Arg.Set Rewrites.opt_mono_rewrites, " turn on rewrites for combining bitvector operations"); ( "-dno_complex_nexps_rewrite", - Arg.Clear Process_file.opt_mono_complex_nexps, + Arg.Clear Rewrites.opt_mono_complex_nexps, " do not move complex size expressions in function signatures into constraints (monomorphisation)"); ( "-dall_split_errors", - Arg.Set Process_file.opt_dall_split_errors, + Arg.Set Rewrites.opt_dall_split_errors, " display all case split errors from monomorphisation, rather than one"); ( "-dmono_continue", - Arg.Set Process_file.opt_dmono_continue, + Arg.Set Rewrites.opt_dmono_continue, " continue despite monomorphisation errors"); ( "-verbose", Arg.Set opt_print_verbose, @@ -268,16 +252,7 @@ let load_files type_envs files = let (ast, type_envs) = check_ast type_envs ast in - let (ast, type_envs) = - match !opt_mono_split, !opt_auto_mono with - | [], false -> ast, type_envs - | locs, _ -> monomorphise_ast locs type_envs ast - in - - let ast = - if !Initial_check.opt_undefined_gen then - rewrite_undefined (!Pretty_print_lem.opt_mwords || !opt_print_coq) (rewrite_ast ast) - else rewrite_ast ast in + let ast = rewrite_ast ast in let out_name = match !opt_file_out with | None when parsed = [] -> "out.sail" diff --git a/src/type_check.ml b/src/type_check.ml index 2d1241b9..c73c7000 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -80,11 +80,6 @@ let typ_debug m = if !opt_tc_debug > 1 then prerr_endline (indent !depth ^ Lazy. let typ_print m = if !opt_tc_debug > 0 then prerr_endline (indent !depth ^ Lazy.force m) else () -let lvar_typ = function - | Local (_, typ) -> typ - | Register (_, _, typ) -> typ - | Enum typ -> typ - type type_error = (* First parameter is the error that caused us to start doing type coercions, the second is the errors encountered by all possible @@ -401,7 +396,7 @@ module Env : sig val add_cast : id -> t -> t val allow_polymorphic_undefineds : t -> t val polymorphic_undefineds : t -> bool - val lookup_id : ?raw:bool -> id -> t -> lvar + val lookup_id : ?raw:bool -> id -> t -> typ lvar val fresh_kid : ?kid:kid -> t -> kid val expand_synonyms : t -> typ -> typ val canonicalize : t -> typ -> typ @@ -2543,7 +2538,7 @@ and type_coercion env (E_aux (_, (l, _)) as annotated_exp) typ = begin try typ_debug (lazy ("PERFORMING TYPE COERCION: from " ^ string_of_typ (typ_of annotated_exp) ^ " to " ^ string_of_typ typ)); - subtyp l env (typ_of annotated_exp) typ; switch_typ annotated_exp typ + subtyp l env (typ_of annotated_exp) typ; annotated_exp (* ; switch_typ annotated_exp typ *) with | Type_error (_, trigger) when Env.allow_casts env -> let casts = filter_casts env (typ_of annotated_exp) typ (Env.get_casts env) in diff --git a/src/type_check.mli b/src/type_check.mli index 31a5a8dd..286c2be9 100644 --- a/src/type_check.mli +++ b/src/type_check.mli @@ -67,9 +67,6 @@ val opt_no_effects : bool ref assignments in l-expressions. *) val opt_no_lexp_bounds_check : bool ref -(** Note: Partial function -- fails for Unknown lvars *) -val lvar_typ : lvar -> typ - (** {2 Type errors} *) type type_error = @@ -163,7 +160,7 @@ module Env : sig lvar type. Returns Unbound if the identifier is unbound, and won't throw any exceptions. If the raw option is true, then look up the type without any flow typing modifiers. *) - val lookup_id : ?raw:bool -> id -> t -> lvar + val lookup_id : ?raw:bool -> id -> t -> typ lvar val is_union_constructor : id -> t -> bool |