summaryrefslogtreecommitdiff
path: root/src/jib
diff options
context:
space:
mode:
Diffstat (limited to 'src/jib')
-rw-r--r--src/jib/anf.ml14
-rw-r--r--src/jib/anf.mli1
-rw-r--r--src/jib/c_backend.ml239
-rw-r--r--src/jib/c_backend.mli1
-rw-r--r--src/jib/jib_compile.ml242
-rw-r--r--src/jib/jib_compile.mli2
-rw-r--r--src/jib/jib_optimize.ml162
-rw-r--r--src/jib/jib_optimize.mli3
-rw-r--r--src/jib/jib_ssa.ml209
-rw-r--r--src/jib/jib_ssa.mli18
-rw-r--r--src/jib/jib_util.ml253
11 files changed, 716 insertions, 428 deletions
diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 025138d0..0a410249 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -91,6 +91,7 @@ and 'a apat_aux =
| AP_global of id * 'a
| AP_app of id * 'a apat * 'a
| AP_cons of 'a apat * 'a apat
+ | AP_as of 'a apat * id * 'a
| AP_nil of 'a
| AP_wild of 'a
@@ -113,6 +114,7 @@ let rec apat_bindings (AP_aux (apat_aux, _, _)) =
| AP_global (id, _) -> IdSet.empty
| AP_app (id, apat, _) -> apat_bindings apat
| AP_cons (apat1, apat2) -> IdSet.union (apat_bindings apat1) (apat_bindings apat2)
+ | AP_as (apat, id, _) -> IdSet.add id (apat_bindings apat)
| AP_nil _ -> IdSet.empty
| AP_wild _ -> IdSet.empty
@@ -132,6 +134,7 @@ let rec apat_types (AP_aux (apat_aux, _, _)) =
| 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_as (apat, id, typ) -> Bindings.add id typ (apat_types apat)
| AP_nil _ -> Bindings.empty
| AP_wild _ -> Bindings.empty
@@ -143,6 +146,8 @@ let rec apat_rename from_id to_id (AP_aux (apat_aux, env, l)) =
| AP_global (id, typ) -> AP_global (id, typ)
| AP_app (ctor, apat, typ) -> AP_app (ctor, apat_rename from_id to_id apat, typ)
| AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2)
+ | AP_as (apat, id, typ) when Id.compare id from_id = 0 -> AP_as (apat, to_id, typ)
+ | AP_as (apat, id, typ) -> AP_as (apat, id, typ)
| AP_nil typ -> AP_nil typ
| AP_wild typ -> AP_wild typ
in
@@ -158,7 +163,7 @@ let rec aval_rename from_id to_id = function
| AV_list (avals, typ) -> AV_list (List.map (aval_rename from_id to_id) avals, typ)
| AV_vector (avals, typ) -> AV_vector (List.map (aval_rename from_id to_id) avals, typ)
| AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ)
- | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename from_id to_id fragment, typ, ctyp)
+ | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename (name from_id) (name to_id) fragment, typ, ctyp)
let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) =
let recur = aexp_rename from_id to_id in
@@ -382,6 +387,7 @@ and pp_apat (AP_aux (apat_aux, _, _)) =
| AP_app (id, apat, typ) -> pp_annot typ (pp_id id ^^ parens (pp_apat apat))
| AP_nil _ -> string "[||]"
| AP_cons (hd_apat, tl_apat) -> pp_apat hd_apat ^^ string " :: " ^^ pp_apat tl_apat
+ | AP_as (apat, id, ctyp) -> pp_apat apat ^^ string " as " ^^ pp_id id
and pp_cases cases = surround 2 0 lbrace (separate_map (comma ^^ hardline) pp_case cases) rbrace
@@ -445,6 +451,7 @@ let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) =
| P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat))
| P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat)))
| P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat))
+ | P_as (pat, id) -> mk_apat (AP_as (anf_pat ~global:global pat, id, typ_of_pat pat))
| _ ->
raise (Reporting.err_unreachable (fst annot) __POS__
("Could not convert pattern to ANF: " ^ string_of_pat pat))
@@ -456,6 +463,7 @@ let rec apat_globals (AP_aux (aux, _, _)) =
| AP_tup apats -> List.concat (List.map apat_globals apats)
| AP_app (_, apat, _) -> apat_globals apat
| AP_cons (hd_apat, tl_apat) -> apat_globals hd_apat @ apat_globals tl_apat
+ | AP_as (apat, _, _) -> apat_globals apat
let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in
@@ -526,8 +534,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp)))
| E_app_infix (x, Id_aux (Id op, l), y) ->
- anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot))
- | E_app_infix (x, Id_aux (DeIid op, l), y) ->
+ anf (E_aux (E_app (Id_aux (Operator op, l), [x; y]), exp_annot))
+ | E_app_infix (x, Id_aux (Operator op, l), y) ->
anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot))
| E_vector exps ->
diff --git a/src/jib/anf.mli b/src/jib/anf.mli
index 79fb35ca..26b847e2 100644
--- a/src/jib/anf.mli
+++ b/src/jib/anf.mli
@@ -111,6 +111,7 @@ and 'a apat_aux =
| AP_global of id * 'a
| AP_app of id * 'a apat * 'a
| AP_cons of 'a apat * 'a apat
+ | AP_as of 'a apat * id * 'a
| AP_nil of 'a
| AP_wild of 'a
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 846b619f..ee16e2e6 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -86,7 +86,6 @@ let optimize_primops = ref false
let optimize_hoist_allocations = ref false
let optimize_struct_updates = ref false
let optimize_alias = ref false
-let optimize_experimental = ref false
let c_debug str =
if !c_verbosity > 0 then prerr_endline (Lazy.force str) else ()
@@ -96,7 +95,7 @@ let c_error ?loc:(l=Parse_ast.Unknown) message =
let zencode_id = function
| Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
- | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
+ | Id_aux (Operator str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
(**************************************************************************)
(* 2. Converting sail types to C types *)
@@ -310,21 +309,21 @@ let rec c_aval ctx = function
(* We need to check that id's type hasn't changed due to flow typing *)
let _, ctyp' = Bindings.find id ctx.locals in
if ctyp_equal ctyp ctyp' then
- AV_C_fragment (F_id id, typ, ctyp)
+ AV_C_fragment (F_id (name id), typ, ctyp)
else
(* id's type changed due to flow
typing, so it's really still heap allocated! *)
v
with
(* Hack: Assuming global letbindings don't change from flow typing... *)
- Not_found -> AV_C_fragment (F_id id, typ, ctyp)
+ Not_found -> AV_C_fragment (F_id (name id), typ, ctyp)
end
else
v
| Register (_, _, typ) when is_stack_typ ctx typ ->
let ctyp = ctyp_of_typ ctx typ in
if is_stack_ctyp ctyp then
- AV_C_fragment (F_id id, typ, ctyp)
+ AV_C_fragment (F_id (name id), typ, ctyp)
else
v
| _ -> v
@@ -612,24 +611,6 @@ let analyze_primop ctx id args typ =
else
no_change
-let generate_cleanup instrs =
- let generate_cleanup' (I_aux (instr, _)) =
- match instr with
- | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)]
- | I_decl (ctyp, id) -> [(id, iclear ctyp id)]
- | instr -> []
- in
- let is_clear ids = function
- | I_aux (I_clear (_, id), _) -> IdSet.add id ids
- | _ -> ids
- in
- let cleaned = List.fold_left is_clear IdSet.empty instrs in
- instrs
- |> List.map generate_cleanup'
- |> List.concat
- |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned))
- |> List.map snd
-
(** Functions that have heap-allocated return types are implemented by
passing a pointer a location where the return value should be
stored. The ANF -> Sail IR pass for expressions simply outputs an
@@ -643,7 +624,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
let end_function_label = label "end_function_" in
let is_return_recur (I_aux (instr, _)) =
match instr with
- | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ | I_undefined _ -> true
+ | I_if _ | I_block _ | I_end _ | I_funcall _ | I_copy _ | I_undefined _ -> true
| _ -> false
in
let rec rewrite_return instrs =
@@ -657,15 +638,15 @@ let fix_early_heap_return ret ret_ctyp instrs =
before
@ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
@ rewrite_return after
- | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after ->
+ | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
before
@ [I_aux (I_funcall (CL_addr (CL_id (ret, CT_ref ctyp)), extern, fid, args), aux)]
@ rewrite_return after
- | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after ->
+ | before, I_aux (I_copy (CL_id (Return _, ctyp), cval), aux) :: after ->
before
@ [I_aux (I_copy (CL_addr (CL_id (ret, CT_ref ctyp)), cval), aux)]
@ rewrite_return after
- | before, I_aux ((I_end | I_undefined _), _) :: after ->
+ | before, I_aux ((I_end _ | I_undefined _), _) :: after ->
before
@ [igoto end_function_label]
@ rewrite_return after
@@ -680,7 +661,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
let fix_early_stack_return ret ret_ctyp instrs =
let is_return_recur (I_aux (instr, _)) =
match instr with
- | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ -> true
+ | I_if _ | I_block _ | I_end _ | I_funcall _ | I_copy _ -> true
| _ -> false
in
let rec rewrite_return instrs =
@@ -694,15 +675,15 @@ let fix_early_stack_return ret ret_ctyp instrs =
before
@ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
@ rewrite_return after
- | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after ->
+ | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
before
@ [I_aux (I_funcall (CL_id (ret, ctyp), extern, fid, args), aux)]
@ rewrite_return after
- | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after ->
+ | before, I_aux (I_copy (CL_id (Return _, ctyp), cval), aux) :: after ->
before
@ [I_aux (I_copy (CL_id (ret, ctyp), cval), aux)]
@ rewrite_return after
- | before, I_aux (I_end, _) :: after ->
+ | before, I_aux (I_end _, _) :: after ->
before
@ [ireturn (F_id ret, ret_ctyp)]
@ rewrite_return after
@@ -722,10 +703,10 @@ let rec insert_heap_returns ret_ctyps = function
| None ->
raise (Reporting.err_general (id_loc id) ("Cannot find return type for function " ^ string_of_id id))
| Some ret_ctyp when not (is_stack_ctyp ret_ctyp) ->
- CDEF_fundef (id, Some gs, args, fix_early_heap_return gs ret_ctyp body)
+ CDEF_fundef (id, Some gs, args, fix_early_heap_return (name gs) ret_ctyp body)
:: insert_heap_returns ret_ctyps cdefs
| Some ret_ctyp ->
- CDEF_fundef (id, None, args, fix_early_stack_return gs ret_ctyp (idecl ret_ctyp gs :: body))
+ CDEF_fundef (id, None, args, fix_early_stack_return (name gs) ret_ctyp (idecl ret_ctyp (name gs) :: body))
:: insert_heap_returns ret_ctyps cdefs
end
@@ -766,32 +747,6 @@ let add_local_labels instrs =
(* 5. Optimizations *)
(**************************************************************************)
-let rec instrs_rename from_id to_id =
- let rename id = if Id.compare id from_id = 0 then to_id else id in
- let crename = cval_rename from_id to_id in
- let irename instrs = instrs_rename from_id to_id instrs in
- let lrename = clexp_rename from_id to_id in
- function
- | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs
- | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs
- | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs
- | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs
- | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs
- | 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), 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_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), 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_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
- | [] -> []
-
let hoist_ctyp = function
| CT_lint | CT_lbits _ | CT_struct _ -> true
| _ -> false
@@ -800,7 +755,7 @@ let hoist_counter = ref 0
let hoist_id () =
let id = mk_id ("gh#" ^ string_of_int !hoist_counter) in
incr hoist_counter;
- id
+ name id
let hoist_allocations recursive_functions = function
| CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id recursive_functions ->
@@ -871,7 +826,7 @@ let rec specialize_variants ctx prior =
if ctyp_equal ctyp suprema then
[], (unpoly frag, ctyp), []
else
- let gs = gensym () in
+ let gs = ngensym () in
[idecl suprema gs;
icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)],
(F_id gs, suprema),
@@ -997,26 +952,26 @@ let remove_alias =
let rec scan ctyp id n instrs =
match n, !alias, instrs with
| 0, None, I_aux (I_copy (CL_id (id', ctyp'), (F_id a, ctyp'')), _) :: instrs
- when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
+ when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
alias := Some a;
scan ctyp id 1 instrs
| 1, Some a, I_aux (I_copy (CL_id (a', ctyp'), (F_id id', ctyp'')), _) :: instrs
- when Id.compare a a' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
+ when Name.compare a a' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
scan ctyp id 2 instrs
| 1, Some a, instr :: instrs ->
- if IdSet.mem a (instr_ids instr) then
+ if NameSet.mem a (instr_ids instr) then
None
else
scan ctyp id 1 instrs
| 2, Some a, I_aux (I_clear (ctyp', id'), _) :: instrs
- when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' ->
+ when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' ->
scan ctyp id 2 instrs
| 2, Some a, instr :: instrs ->
- if IdSet.mem id (instr_ids instr) then
+ if NameSet.mem id (instr_ids instr) then
None
else
scan ctyp id 2 instrs
@@ -1031,9 +986,9 @@ let remove_alias =
in
let remove_alias id alias = function
| I_aux (I_copy (CL_id (id', _), (F_id alias', _)), _)
- when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed
+ when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed
| I_aux (I_copy (CL_id (alias', _), (F_id id', _)), _)
- when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed
+ when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed
| I_aux (I_clear (_, id'), _) -> removed
| instr -> instr
in
@@ -1066,17 +1021,17 @@ let unique_names =
let unique_id () =
let id = mk_id ("u#" ^ string_of_int !unique_counter) in
incr unique_counter;
- id
+ name id
in
let rec opt seen = function
- | I_aux (I_decl (ctyp, id), aux) :: instrs when IdSet.mem id seen ->
+ | I_aux (I_decl (ctyp, id), aux) :: instrs when NameSet.mem id seen ->
let id' = unique_id () in
let instrs', seen = opt seen instrs in
I_aux (I_decl (ctyp, id'), aux) :: instrs_rename id id' instrs', seen
| I_aux (I_decl (ctyp, id), aux) :: instrs ->
- let instrs', seen = opt (IdSet.add id seen) instrs in
+ let instrs', seen = opt (NameSet.add id seen) instrs in
I_aux (I_decl (ctyp, id), aux) :: instrs', seen
| I_aux (I_block block, aux) :: instrs ->
@@ -1103,11 +1058,11 @@ let unique_names =
in
function
| CDEF_fundef (function_id, heap_return, args, body) ->
- [CDEF_fundef (function_id, heap_return, args, fst (opt IdSet.empty body))]
+ [CDEF_fundef (function_id, heap_return, args, fst (opt NameSet.empty body))]
| CDEF_reg_dec (id, ctyp, instrs) ->
- [CDEF_reg_dec (id, ctyp, fst (opt IdSet.empty instrs))]
+ [CDEF_reg_dec (id, ctyp, fst (opt NameSet.empty instrs))]
| CDEF_let (n, bindings, instrs) ->
- [CDEF_let (n, bindings, fst (opt IdSet.empty instrs))]
+ [CDEF_let (n, bindings, fst (opt NameSet.empty instrs))]
| cdef -> [cdef]
(** This optimization looks for patterns of the form
@@ -1135,26 +1090,26 @@ let combine_variables =
scan id 1 instrs
| 1, Some c, I_aux (I_copy (CL_id (id', ctyp'), (F_id c', ctyp'')), _) :: instrs
- when Id.compare c c' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
+ when Name.compare c c' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
scan id 2 instrs
(* Ignore seemingly early clears of x, as this can happen along exception paths *)
| 1, Some c, I_aux (I_clear (_, id'), _) :: instrs
- when Id.compare id id' = 0 ->
+ when Name.compare id id' = 0 ->
scan id 1 instrs
| 1, Some c, instr :: instrs ->
- if IdSet.mem id (instr_ids instr) then
+ if NameSet.mem id (instr_ids instr) then
None
else
scan id 1 instrs
| 2, Some c, I_aux (I_clear (ctyp', c'), _) :: instrs
- when Id.compare c c' = 0 && ctyp_equal ctyp ctyp' ->
+ when Name.compare c c' = 0 && ctyp_equal ctyp ctyp' ->
!combine
| 2, Some c, instr :: instrs ->
- if IdSet.mem c (instr_ids instr) then
+ if NameSet.mem c (instr_ids instr) then
None
else
scan id 2 instrs
@@ -1167,12 +1122,12 @@ let combine_variables =
scan id 0
in
let remove_variable id = function
- | I_aux (I_decl (_, id'), _) when Id.compare id id' = 0 -> removed
- | I_aux (I_clear (_, id'), _) when Id.compare id id' = 0 -> removed
+ | I_aux (I_decl (_, id'), _) when Name.compare id id' = 0 -> removed
+ | I_aux (I_clear (_, id'), _) when Name.compare id id' = 0 -> removed
| instr -> instr
in
let is_not_self_assignment = function
- | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Id.compare id id' = 0 -> false
+ | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Name.compare id id' = 0 -> false
| _ -> true
in
let rec opt = function
@@ -1200,63 +1155,6 @@ let combine_variables =
[CDEF_fundef (function_id, heap_return, args, opt body)]
| cdef -> [cdef]
-(** hoist_alias looks for patterns like
-
- recreate x; y = x; // no furthner mentions of x
-
- Provided x has a certain type, then we can make y an alias to x
- (denoted in the IR as 'alias y = x'). This only works if y also has
- a lifespan that also spans the entire function body. It's possible
- we may need to do a more thorough lifetime evaluation to get this
- to be 100% correct - so it's behind the -Oexperimental flag
- for now. Some benchmarking shows that this kind of optimization
- is very valuable however! *)
-let hoist_alias =
- (* Must return true for a subset of the types hoist_ctyp would return true for. *)
- let is_struct = function
- | CT_struct _ -> true
- | _ -> false
- in
- let pattern heap_return id ctyp instrs =
- let rec scan instrs =
- match instrs with
- (* The only thing that has a longer lifetime than id is the
- function return, so we want to make sure we avoid that
- case. *)
- | (I_aux (I_copy (clexp, (F_id id', ctyp')), aux) as instr) :: instrs
- when not (IdSet.mem heap_return (instr_writes instr)) && Id.compare id id' = 0
- && ctyp_equal (clexp_ctyp clexp) ctyp && ctyp_equal ctyp ctyp' ->
- if List.exists (IdSet.mem id) (List.map instr_ids instrs) then
- instr :: scan instrs
- else
- I_aux (I_alias (clexp, (F_id id', ctyp')), aux) :: instrs
-
- | instr :: instrs -> instr :: scan instrs
- | [] -> []
- in
- scan instrs
- in
- let optimize heap_return =
- let rec opt = function
- | (I_aux (I_reset (ctyp, id), _) as instr) :: instrs when not (is_stack_ctyp ctyp) && is_struct ctyp ->
- instr :: opt (pattern heap_return id ctyp instrs)
-
- | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt block), aux) :: opt instrs
- | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt block), aux) :: opt instrs
- | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
- I_aux (I_if (cval, opt then_instrs, opt else_instrs, ctyp), aux) :: opt instrs
-
- | instr :: instrs ->
- instr :: opt instrs
- | [] -> []
- in
- opt
- in
- function
- | CDEF_fundef (function_id, Some heap_return, args, body) ->
- [CDEF_fundef (function_id, Some heap_return, args, optimize heap_return body)]
- | cdef -> [cdef]
-
let concatMap f xs = List.concat (List.map f xs)
let optimize recursive_functions cdefs =
@@ -1267,13 +1165,13 @@ let optimize recursive_functions cdefs =
|> (if !optimize_alias then concatMap combine_variables else nothing)
(* We need the runtime to initialize hoisted allocations *)
|> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations recursive_functions) else nothing)
- |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap hoist_alias else nothing)
(**************************************************************************)
(* 6. Code generation *)
(**************************************************************************)
let sgen_id id = Util.zencode_string (string_of_id id)
+let sgen_name id = string_of_name id
let codegen_id id = string (sgen_id id)
let sgen_function_id id =
@@ -1286,9 +1184,9 @@ let rec sgen_ctyp = function
| CT_unit -> "unit"
| CT_bit -> "fbits"
| CT_bool -> "bool"
- | CT_fbits _ -> "fbits"
+ | CT_fbits _ -> "uint64_t"
| CT_sbits _ -> "sbits"
- | CT_fint _ -> "mach_int"
+ | CT_fint _ -> "int64_t"
| CT_lint -> "sail_int"
| CT_lbits _ -> "lbits"
| CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
@@ -1336,23 +1234,23 @@ let sgen_cval_param (frag, ctyp) =
let sgen_cval = function (frag, _) -> string_of_fragment frag
let rec sgen_clexp = function
- | CL_id (id, _) -> "&" ^ sgen_id id
+ | CL_id (Have_exception _, _) -> "have_exception"
+ | CL_id (Current_exception _, _) -> "current_exception"
+ | CL_id (Return _, _) -> assert false
+ | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
| CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ Util.zencode_string field ^ ")"
| CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")"
| CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))"
- | CL_have_exception -> "have_exception"
- | CL_current_exception _ -> "current_exception"
- | CL_return _ -> assert false
| CL_void -> assert false
let rec sgen_clexp_pure = function
- | CL_id (id, _) -> sgen_id id
+ | CL_id (Have_exception _, _) -> "have_exception"
+ | CL_id (Current_exception _, _) -> "current_exception"
+ | CL_id (Return _, _) -> assert false
+ | CL_id (Name (id, _), _) -> sgen_id id
| CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ Util.zencode_string field
| CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n
| CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))"
- | CL_have_exception -> "have_exception"
- | CL_current_exception _ -> "current_exception"
- | CL_return _ -> assert false
| CL_void -> assert false
(** Generate instructions to copy from a cval to a clexp. This will
@@ -1397,16 +1295,13 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
let open Printf in
match instr with
| I_decl (ctyp, id) when is_stack_ctyp ctyp ->
- ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id)
+ ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id)
| I_decl (ctyp, id) ->
- ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
- ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)
+ ksprintf string " %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline
+ ^^ ksprintf string " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
| I_copy (clexp, cval) -> codegen_conversion l clexp cval
- | I_alias (clexp, cval) ->
- ksprintf string " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)
-
| I_jump (cval, label) ->
ksprintf string " if (%s) goto %s;" (sgen_cval cval) label
@@ -1488,9 +1383,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
| "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
| fname, _ -> fname
in
- if fname = "sail_assert" && !optimize_experimental then
- empty
- else if fname = "reg_deref" then
+ if fname = "reg_deref" then
if is_stack_ctyp ctyp then
string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args)
else
@@ -1504,7 +1397,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
| I_clear (ctyp, id) when is_stack_ctyp ctyp ->
empty
| I_clear (ctyp, id) ->
- string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ string (Printf.sprintf " KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
| I_init (ctyp, id, cval) ->
codegen_instr fid ctx (idecl ctyp id) ^^ hardline
@@ -1515,9 +1408,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval
| I_reset (ctyp, id) when is_stack_ctyp ctyp ->
- string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id))
+ string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_name id))
| I_reset (ctyp, id) ->
- string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
| I_return cval ->
string (Printf.sprintf " return %s;" (sgen_cval cval))
@@ -1536,24 +1429,24 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
| CT_bool -> "false", []
| CT_enum (_, ctor :: _) -> sgen_id ctor, []
| CT_tup ctyps when is_stack_ctyp ctyp ->
- let gs = gensym () in
+ let gs = ngensym () 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)
+ sgen_name gs,
+ [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
| CT_struct (id, ctors) when is_stack_ctyp ctyp ->
- let gs = gensym () in
+ let gs = ngensym () 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)
+ sgen_name gs,
+ [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
| ctyp -> c_error ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp)
in
@@ -1575,7 +1468,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
| I_raw str ->
string (" " ^ str)
- | I_end -> assert false
+ | I_end _ -> assert false
| I_match_failure ->
string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");")
@@ -2014,13 +1907,13 @@ let is_decl = function
let codegen_decl = function
| I_aux (I_decl (ctyp, id), _) ->
- string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
+ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id))
| _ -> assert false
let codegen_alloc = function
| I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty
| I_aux (I_decl (ctyp, id), _) ->
- string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+ string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
| _ -> assert false
let codegen_def' ctx = function
@@ -2101,10 +1994,10 @@ let codegen_def' ctx = function
| CDEF_let (number, bindings, instrs) ->
let instrs = add_local_labels instrs in
let setup =
- List.concat (List.map (fun (id, ctyp) -> [idecl ctyp id]) bindings)
+ List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (name id)]) bindings)
in
let cleanup =
- List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings)
+ List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings)
in
separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings
^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number)
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 7314eb5a..3e8c426b 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -100,7 +100,6 @@ val optimize_primops : bool ref
val optimize_hoist_allocations : bool ref
val optimize_struct_updates : bool ref
val optimize_alias : bool ref
-val optimize_experimental : bool ref
(** Convert a typ to a IR ctyp *)
val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 27f833d8..4a72ffff 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -61,6 +61,8 @@ let opt_debug_function = ref ""
let opt_debug_flow_graphs = ref false
let opt_memo_cache = ref false
+let ngensym () = name (gensym ())
+
(**************************************************************************)
(* 4. Conversion to low-level AST *)
(**************************************************************************)
@@ -183,26 +185,26 @@ let rec compile_aval l ctx = function
begin
try
let _, ctyp = Bindings.find id ctx.locals in
- [], (F_id id, ctyp), []
+ [], (F_id (name id), ctyp), []
with
| Not_found ->
- [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), []
+ [], (F_id (name 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))), []
+ [], (F_ref (name id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), []
| AV_lit (L_aux (L_string str, _), typ) ->
[], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), []
| AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
- let gs = gensym () in
+ let gs = ngensym () in
[iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
(F_id gs, CT_lint),
[iclear CT_lint gs]
| AV_lit (L_aux (L_num n, _), typ) ->
- let gs = gensym () in
+ let gs = ngensym () in
[iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
(F_id gs, CT_lint),
[iclear CT_lint gs]
@@ -214,7 +216,7 @@ let rec compile_aval l ctx = function
| AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), []
| AV_lit (L_aux (L_real str, _), _) ->
- let gs = gensym () in
+ let gs = ngensym () in
[iinit CT_real gs (F_lit (V_string str), CT_string)],
(F_id gs, CT_real),
[iclear CT_real gs]
@@ -230,7 +232,7 @@ let rec compile_aval l ctx = function
let setup = List.concat (List.map (fun (setup, _, _) -> setup) elements) in
let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in
let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in
- let gs = gensym () in
+ let gs = ngensym () in
setup
@ [idecl tup_ctyp gs]
@ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals,
@@ -240,7 +242,7 @@ let rec compile_aval l ctx = function
| AV_record (fields, typ) ->
let ctyp = ctyp_of_typ ctx typ in
- let gs = gensym () in
+ let gs = ngensym () in
let compile_fields (id, aval) =
let field_setup, cval, field_cleanup = compile_aval l ctx aval in
field_setup
@@ -278,7 +280,7 @@ let rec compile_aval l ctx = function
let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in
let first_chunk = bitstring (Util.take (len mod 64) avals) in
let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
- let gs = gensym () in
+ let gs = ngensym () in
[iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))]
@ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true))
(mk_id "append_64")
@@ -295,7 +297,7 @@ let rec compile_aval l ctx = function
| Ord_aux (Ord_dec, _) -> true
| Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found")
in
- let gs = gensym () in
+ let gs = ngensym () in
let ctyp = CT_fbits (len, direction) in
let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in
let aval_mask i aval =
@@ -323,7 +325,7 @@ let rec compile_aval l ctx = function
| Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found")
in
let vector_ctyp = CT_vector (direction, ctyp_of_typ ctx typ) in
- let gs = gensym () in
+ let gs = ngensym () in
let aval_set i aval =
let setup, cval, cleanup = compile_aval l ctx aval in
setup
@@ -346,7 +348,7 @@ let rec compile_aval l ctx = function
| Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ
| _ -> raise (Reporting.err_general l "Invalid list type")
in
- let gs = gensym () in
+ let gs = ngensym () in
let mk_cons aval =
let setup, cval, cleanup = compile_aval l ctx aval in
setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup
@@ -384,7 +386,7 @@ let compile_funcall l ctx id args typ =
else if ctyp_equal ctyp have_ctyp then
cval
else
- let gs = gensym () in
+ let gs = ngensym () in
setup := iinit ctyp gs cval :: !setup;
cleanup := iclear ctyp gs :: !cleanup;
(F_id gs, ctyp)
@@ -399,7 +401,7 @@ let compile_funcall l ctx id args typ =
if ctyp_equal (clexp_ctyp clexp) ret_ctyp then
ifuncall clexp id setup_args
else
- let gs = gensym () in
+ let gs = ngensym () in
iblock [idecl ret_ctyp gs;
ifuncall (CL_id (gs, ret_ctyp)) id setup_args;
icopy l clexp (F_id gs, ret_ctyp);
@@ -414,30 +416,37 @@ let rec apat_ctyp ctx (AP_aux (apat, _, _)) =
| AP_cons (apat, _) -> CT_list (apat_ctyp ctx apat)
| AP_wild typ | AP_nil typ | AP_id (_, typ) -> ctyp_of_typ ctx typ
| AP_app (_, _, typ) -> ctyp_of_typ ctx typ
+ | AP_as (_, _, typ) -> ctyp_of_typ ctx typ
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],
+ [ijump (F_ctor_kind (frag, pid, [], ctyp), CT_bool) case_label],
[],
ctx
| AP_global (pid, typ), (frag, ctyp) ->
let global_ctyp = ctyp_of_typ ctx typ in
- [icopy l (CL_id (pid, global_ctyp)) cval], [], ctx
+ [icopy l (CL_id (name 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 l (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx
- | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx
+ | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) (frag, ctyp)], [], ctx
+ | _ -> [ijump (F_op (F_id (name 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
let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in
- [idecl id_ctyp pid; icopy l (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx
+ [idecl id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx
+
+ | AP_as (apat, id, typ), _ ->
+ let id_ctyp = ctyp_of_typ ctx typ in
+ let instrs, cleanup, ctx = compile_match ctx apat cval case_label in
+ let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in
+ instrs @ [idecl id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], iclear id_ctyp (name id) :: cleanup, ctx
| AP_tup apats, (frag, ctyp) ->
begin
@@ -456,25 +465,21 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
| AP_app (ctor, apat, variant_typ), (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 pat_ctyp = apat_ctyp ctx apat in
(* These should really be the same, something has gone wrong if they are not. *)
if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then
raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ))))
else ();
- let ctor_c_id, ctor_ctyp =
+ let unifiers, ctor_ctyp =
if is_polymorphic ctor_ctyp then
- let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in
- (if List.length unification > 0 then
- ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification
- else
- ctor_c_id),
- ctyp_suprema (apat_ctyp ctx apat)
+ let unifiers = List.map ctyp_suprema (ctyp_unify ctor_ctyp pat_ctyp) in
+ unifiers, ctyp_suprema (apat_ctyp ctx apat)
else
- ctor_c_id, ctor_ctyp
+ [], ctor_ctyp
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]
+ let instrs, cleanup, ctx = compile_match ctx apat (F_ctor_unwrap (ctor, unifiers, frag), ctor_ctyp) case_label in
+ [ijump (F_ctor_kind (frag, ctor, unifiers, pat_ctyp), CT_bool) case_label]
@ instrs,
cleanup,
ctx
@@ -507,7 +512,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in
let setup, call, cleanup = compile_aexp ctx binding in
let letb_setup, letb_cleanup =
- [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id]
+ [idecl binding_ctyp (name id);
+ iblock (setup @ [call (CL_id (name id, binding_ctyp))] @ cleanup)],
+ [iclear binding_ctyp (name id)]
in
let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in
let setup, call, cleanup = compile_aexp ctx body in
@@ -524,7 +531,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_case (aval, cases, typ) ->
let ctyp = ctyp_of_typ ctx typ in
let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in
- let case_return_id = gensym () in
+ let case_return_id = ngensym () in
let finish_match_label = label "finish_match_" in
let compile_case (apat, guard, body) =
let trivial_guard = match guard with
@@ -536,13 +543,12 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_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 gs = ngensym () in
let case_instrs =
- destructure @ [icomment "end destructuring"]
+ destructure
@ (if not trivial_guard then
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, ctyp))] @ body_cleanup @ destructure_cleanup
@ [igoto finish_match_label]
@@ -552,21 +558,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
else
[iblock case_instrs; ilabel case_label]
in
- [icomment "begin match"]
- @ aval_setup @ [idecl ctyp case_return_id]
+ aval_setup @ [idecl ctyp case_return_id]
@ List.concat (List.map compile_case cases)
@ [imatch_failure ()]
@ [ilabel finish_match_label],
(fun clexp -> icopy l clexp (F_id case_return_id, ctyp)),
[iclear ctyp case_return_id]
@ aval_cleanup
- @ [icomment "end match"]
(* Compile try statement *)
| AE_try (aexp, cases, typ) ->
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 try_return_id = ngensym () in
let handled_exception_label = label "handled_exception_" in
let fallthrough_label = label "fallthrough_exception_" in
let compile_case (apat, guard, body) =
@@ -576,11 +580,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| _ -> false
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 exn_cval = (F_id current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) 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 gs = ngensym () in
let case_instrs =
destructure @ [icomment "end destructuring"]
@ (if not trivial_guard then
@@ -596,11 +600,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
[idecl ctyp try_return_id;
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]
+ ijump (F_unary ("!", F_id have_exception), CT_bool) handled_exception_label]
@ List.concat (List.map compile_case cases)
@ [igoto fallthrough_label;
ilabel handled_exception_label;
- icopy l CL_have_exception (F_lit (V_bool false), CT_bool);
+ icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool false), CT_bool);
ilabel fallthrough_label],
(fun clexp -> icopy l clexp (F_id try_return_id, ctyp)),
[]
@@ -631,7 +635,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors
| _ -> raise (Reporting.err_general l "Cannot perform record update for non-record type")
in
- let gs = gensym () in
+ let gs = ngensym () in
let compile_fields (id, aval) =
let field_setup, cval, field_cleanup = compile_aval l ctx aval in
field_setup
@@ -650,7 +654,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_short_circuit (SC_and, aval, aexp) ->
let left_setup, cval, left_cleanup = compile_aval l ctx aval in
let right_setup, call, right_cleanup = compile_aexp ctx aexp in
- let gs = gensym () in
+ let gs = ngensym () in
left_setup
@ [ idecl CT_bool gs;
iif cval
@@ -663,7 +667,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| AE_short_circuit (SC_or, aval, aexp) ->
let left_setup, cval, left_cleanup = compile_aval l ctx aval in
let right_setup, call, right_cleanup = compile_aexp ctx aexp in
- let gs = gensym () in
+ let gs = ngensym () in
left_setup
@ [ idecl CT_bool gs;
iif cval
@@ -681,7 +685,7 @@ 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 l ctx aval in
field_setup
- @ [icopy l (CL_field (CL_id (id, ctyp_of_typ ctx typ), string_of_id field_id)) cval]
+ @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), string_of_id field_id)) cval]
@ field_cleanup
in
List.concat (List.map compile_fields (Bindings.bindings fields)),
@@ -695,7 +699,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| None -> ctyp_of_typ ctx assign_typ
in
let setup, call, cleanup = compile_aexp ctx aexp in
- setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup
+ setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup
| AE_block (aexps, aexp, _) ->
let block = compile_block ctx aexps in
@@ -707,8 +711,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
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 gs = gensym () in
- let unit_gs = gensym () in
+ let gs = ngensym () in
+ let unit_gs = ngensym () 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]
@@ -729,8 +733,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
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 gs = gensym () in
- let unit_gs = gensym () in
+ let gs = ngensym () in
+ let unit_gs = ngensym () in
let loop_test = (F_id gs, CT_bool) in
[idecl CT_bool gs; idecl CT_unit unit_gs]
@ [ilabel loop_start_label]
@@ -759,7 +763,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
if ctyp_equal fn_return_ctyp (cval_ctyp cval) then
[ireturn cval]
else
- let gs = gensym () in
+ let gs = ngensym () in
[idecl fn_return_ctyp gs;
icopy l (CL_id (gs, fn_return_ctyp)) cval;
ireturn (F_id gs, fn_return_ctyp)]
@@ -775,7 +779,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
(fun clexp -> icomment "unreachable after throw"),
[]
- | AE_field (aval, id, _) ->
+ | AE_field (aval, id, typ) ->
+ let aval_ctyp = ctyp_of_typ ctx typ in
let setup, cval, cleanup = compile_aval l ctx aval in
let ctyp = match cval_ctyp cval with
| CT_struct (struct_id, fields) ->
@@ -788,8 +793,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
| _ ->
raise (Reporting.err_unreachable l __POS__ "Field access on non-struct type in ANF representation!")
in
+ let unifiers, ctyp =
+ if is_polymorphic ctyp then
+ let unifiers = List.map ctyp_suprema (ctyp_unify ctyp aval_ctyp) in
+ unifiers, ctyp_suprema aval_ctyp
+ else
+ [], ctyp
+ in
+ let field_str = match unifiers with
+ | [] -> Util.zencode_string (string_of_id id)
+ | _ -> Util.zencode_string (string_of_id id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+ in
setup,
- (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)),
+ (fun clexp -> icopy l clexp (F_field (fst cval, field_str), ctyp)),
cleanup
| AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
@@ -804,11 +820,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
(* Loop variables *)
let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in
- let from_gs = gensym () in
+ let from_gs = ngensym () in
let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in
- let to_gs = gensym () in
+ let to_gs = ngensym () in
let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in
- let step_gs = gensym () in
+ let step_gs = ngensym () in
let variable_init gs setup call cleanup =
[idecl (CT_fint 64) gs;
iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)]
@@ -817,7 +833,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
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_gs = gensym () in
+ let body_gs = ngensym () in
+
+ let loop_var = name loop_var in
variable_init from_gs from_setup from_call from_cleanup
@ variable_init to_gs to_setup to_call to_cleanup
@@ -842,7 +860,7 @@ and compile_block ctx = function
| exp :: exps ->
let setup, call, cleanup = compile_aexp ctx exp in
let rest = compile_block ctx exps in
- let gs = gensym () in
+ let gs = ngensym () in
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
@@ -892,14 +910,14 @@ let generate_cleanup instrs =
| instr -> []
in
let is_clear ids = function
- | I_aux (I_clear (_, id), _) -> IdSet.add id ids
+ | I_aux (I_clear (_, id), _) -> NameSet.add id ids
| _ -> ids
in
- let cleaned = List.fold_left is_clear IdSet.empty instrs in
+ let cleaned = List.fold_left is_clear NameSet.empty instrs in
instrs
|> List.map generate_cleanup'
|> List.concat
- |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned))
+ |> List.filter (fun (id, _) -> not (NameSet.mem id cleaned))
|> List.map snd
let fix_exception_block ?return:(return=None) ctx instrs =
@@ -927,8 +945,8 @@ let fix_exception_block ?return:(return=None) ctx instrs =
@ rewrite_exception historic after
| before, I_aux (I_throw cval, (_, l)) :: after ->
before
- @ [icopy l (CL_current_exception (cval_ctyp cval)) cval;
- icopy l CL_have_exception (F_lit (V_bool true), CT_bool)]
+ @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval;
+ icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool true), CT_bool)]
@ generate_cleanup (historic @ before)
@ [igoto end_block_label]
@ rewrite_exception (historic @ before) after
@@ -941,7 +959,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
if has_effect effects BE_escape then
before
@ [funcall;
- iif (F_have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
+ iif (F_id have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
@ rewrite_exception (historic @ before) after
else
before @ funcall :: rewrite_exception (historic @ before) after
@@ -958,10 +976,10 @@ let rec map_try_block f (I_aux (instr, aux)) =
| 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_copy _ | I_alias _ | 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 | I_undefined _ | I_end -> instr
+ | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end _ -> instr
in
I_aux (instr, aux)
@@ -979,7 +997,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 (name gs), ctyp) label in
(gs, (destructure, cleanup))
let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
@@ -994,10 +1012,10 @@ let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in
let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in
destructure
- @ [idecl (CT_tup ctyps) arg_id]
- @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (arg_id, CT_tup ctyps), i)) (F_id id, ctyp)) new_ids,
+ @ [idecl (CT_tup ctyps) (name arg_id)]
+ @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (F_id (name id), ctyp)) new_ids,
List.map (fun (id, _) -> id, ([], [])) new_ids,
- [iclear (CT_tup ctyps) arg_id]
+ [iclear (CT_tup ctyps) (name arg_id)]
@ cleanup
let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs))
@@ -1108,7 +1126,7 @@ and compile_def' n total ctx = function
| DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
let aexp = ctx.optimize_anf 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
+ let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in
[CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx
| DEF_reg_dec (DEC_aux (_, (l, _))) ->
@@ -1161,8 +1179,8 @@ and compile_def' n total ctx = function
compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label
in
- let instrs = arg_setup @ destructure @ setup @ [call (CL_return ret_ctyp)] @ cleanup @ destructure_cleanup @ arg_cleanup in
- let instrs = fix_early_return (CL_return ret_ctyp) instrs in
+ let instrs = arg_setup @ destructure @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in
+ let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in
let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
if Id.compare (mk_id !opt_debug_function) id = 0 then
@@ -1179,10 +1197,15 @@ and compile_def' n total ctx = function
if !opt_debug_flow_graphs then
begin
let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
- let cfg = Jib_ssa.ssa instrs in
+ let root, _, cfg = Jib_ssa.control_flow_graph instrs in
+ let idom = Jib_ssa.immediate_dominators cfg root in
+ let _, cfg = Jib_ssa.ssa instrs in
let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
Jib_ssa.make_dot out_chan cfg;
close_out out_chan;
+ let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in
+ Jib_ssa.make_dominators_dot out_chan idom cfg;
+ close_out out_chan;
end;
[CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
@@ -1206,7 +1229,7 @@ and compile_def' n total ctx = function
let aexp = ctx.optimize_anf 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 gs = ngensym () in
let end_label = label "let_end_" in
let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in
let gs_setup, gs_cleanup =
@@ -1257,13 +1280,19 @@ let rec specialize_variants ctx prior =
| CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors)
| ctyp -> ctyp
in
+ let fix_struct_ctyp struct_id new_fields = function
+ | CT_struct (id, ctors) when Id.compare id struct_id = 0 -> CT_struct (id, new_fields)
+ | ctyp -> ctyp
+ in
- let specialize_constructor ctx ctor_id ctyp =
- function
+ (* specialize_constructor is called on all instructions when we find
+ a constructor in a union type that is polymorphic. It's job is to
+ record all uses of that constructor so we can monomorphise it. *)
+ let specialize_constructor ctx ctor_id ctyp = function
| I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
(* Work out how each call to a constructor in instantiated and add that to unifications *)
- let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
- let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in
+ let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+ let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
(* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *)
@@ -1273,7 +1302,7 @@ let rec specialize_variants ctx prior =
if ctyp_equal ctyp suprema then
[], (unpoly frag, ctyp), []
else
- let gs = gensym () in
+ let gs = ngensym () in
[idecl suprema gs;
icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)],
(F_id gs, suprema),
@@ -1297,17 +1326,36 @@ let rec specialize_variants ctx prior =
| I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
Reporting.unreachable l __POS__ "Multiple argument constructor found"
+ (* We have to be careful this is the only place where an F_ctor_kind can appear before calling specialize variants *)
+ | I_aux (I_jump ((F_ctor_kind (_, id, unifiers, pat_ctyp), CT_bool), _), _) as instr when Id.compare id ctor_id = 0 ->
+ let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+ unifications := Bindings.add mono_id (ctyp_suprema pat_ctyp) !unifications;
+ instr
+
| instr -> instr
in
+ (* specialize_field performs the same job as specialize_constructor,
+ but for struct fields rather than union constructors. *)
+ let specialize_field ctx field_id ctyp = function
+ | I_aux (I_copy (CL_field (clexp, field_str), cval), aux) when string_of_id field_id = field_str ->
+ let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+ let mono_id = append_id field_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+ unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
+ I_aux (I_copy (CL_field (clexp, string_of_id mono_id), cval), aux)
+
+ | instr -> instr
+ in
+
function
| (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs ->
let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in
let cdefs =
- List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
- cdefs
- polymorphic_ctors
+ List.fold_left
+ (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
+ cdefs
+ polymorphic_ctors
in
let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in
@@ -1324,6 +1372,30 @@ let rec specialize_variants ctx prior =
let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in
specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs
+ | (CDEF_type (CTD_struct (struct_id, fields)) as cdef) :: cdefs ->
+ let polymorphic_fields = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) fields in
+
+ let cdefs =
+ List.fold_left
+ (fun cdefs (field_id, ctyp) -> List.map (cdef_map_instr (specialize_field ctx field_id ctyp)) cdefs)
+ cdefs
+ polymorphic_fields
+ in
+
+ let monomorphic_fields = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) fields in
+ let specialized_fields = Bindings.bindings !unifications in
+ let new_fields = monomorphic_fields @ specialized_fields in
+
+ let ctx = {
+ ctx with records = Bindings.add struct_id
+ (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_fields)
+ ctx.records
+ } in
+
+ let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) cdefs in
+ let prior = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) prior in
+ specialize_variants ctx (CDEF_type (CTD_struct (struct_id, new_fields)) :: prior) cdefs
+
| cdef :: cdefs ->
let remove_poly (I_aux (instr, aux)) =
match instr with
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index f3bd8c76..a0cacc3c 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -63,6 +63,8 @@ val opt_debug_flow_graphs : bool ref
(** Print the IR representation of a specific function. *)
val opt_debug_function : string ref
+val ngensym : unit -> name
+
(** {2 Jib context} *)
(** Context for compiling Sail to Jib. We need to pass a (global)
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index 889e650e..73b175a1 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -71,12 +71,6 @@ let optimize_unit instrs =
I_aux (I_copy (CL_void, unit_cval cval), annot)
| _ -> instr
end
- | I_aux (I_alias (clexp, cval), annot) as instr ->
- begin match clexp_ctyp clexp with
- | CT_unit ->
- I_aux (I_alias (CL_void, unit_cval cval), annot)
- | _ -> instr
- end
| instr -> instr
in
let non_pointless_copy (I_aux (aux, annot)) =
@@ -90,7 +84,7 @@ let flat_counter = ref 0
let flat_id () =
let id = mk_id ("local#" ^ string_of_int !flat_counter) in
incr flat_counter;
- id
+ name id
let rec flatten_instrs = function
| I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
@@ -127,3 +121,157 @@ let flatten_cdef =
CDEF_let (n, bindings, flatten_instrs instrs)
| cdef -> cdef
+
+let unique_per_function_ids cdefs =
+ let unique_id i = function
+ | Name (id, ssa_num) -> Name (append_id id ("#u" ^ string_of_int i), ssa_num)
+ | name -> name
+ in
+ let rec unique_instrs i = function
+ | I_aux (I_decl (ctyp, id), aux) :: rest ->
+ I_aux (I_decl (ctyp, unique_id i id), aux) :: unique_instrs i (instrs_rename id (unique_id i id) rest)
+ | I_aux (I_init (ctyp, id, cval), aux) :: rest ->
+ I_aux (I_init (ctyp, unique_id i id, cval), aux) :: unique_instrs i (instrs_rename id (unique_id i id) rest)
+ | I_aux (I_block instrs, aux) :: rest ->
+ I_aux (I_block (unique_instrs i instrs), aux) :: unique_instrs i rest
+ | I_aux (I_try_block instrs, aux) :: rest ->
+ I_aux (I_try_block (unique_instrs i instrs), aux) :: unique_instrs i rest
+ | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: rest ->
+ I_aux (I_if (cval, unique_instrs i then_instrs, unique_instrs i else_instrs, ctyp), aux) :: unique_instrs i rest
+ | instr :: instrs -> instr :: unique_instrs i instrs
+ | [] -> []
+ in
+ let unique_cdef i = function
+ | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, unique_instrs i instrs)
+ | CDEF_type ctd -> CDEF_type ctd
+ | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, unique_instrs i instrs)
+ | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+ | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, unique_instrs i instrs)
+ | CDEF_startup (id, instrs) -> CDEF_startup (id, unique_instrs i instrs)
+ | CDEF_finish (id, instrs) -> CDEF_finish (id, unique_instrs i instrs)
+ in
+ List.mapi unique_cdef cdefs
+
+let rec frag_subst id subst = function
+ | F_id id' -> if Name.compare id id' = 0 then subst else F_id id'
+ | F_ref reg_id -> F_ref reg_id
+ | F_lit vl -> F_lit vl
+ | F_op (frag1, op, frag2) -> F_op (frag_subst id subst frag1, op, frag_subst id subst frag2)
+ | F_unary (op, frag) -> F_unary (op, frag_subst id subst frag)
+ | F_call (op, frags) -> F_call (op, List.map (frag_subst id subst) frags)
+ | F_field (frag, field) -> F_field (frag_subst id subst frag, field)
+ | F_raw str -> F_raw str
+ | F_ctor_kind (frag, ctor, unifiers, ctyp) -> F_ctor_kind (frag_subst id subst frag, ctor, unifiers, ctyp)
+ | F_ctor_unwrap (ctor, unifiers, frag) -> F_ctor_unwrap (ctor, unifiers, frag_subst id subst frag)
+ | F_poly frag -> F_poly (frag_subst id subst frag)
+
+let cval_subst id subst (frag, ctyp) = frag_subst id subst frag, ctyp
+
+let rec instrs_subst id subst =
+ function
+ | (I_aux (I_decl (_, id'), _) :: _) as instrs when Name.compare id id' = 0 ->
+ instrs
+
+ | I_aux (I_init (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
+ I_aux (I_init (ctyp, id', cval_subst id subst cval), aux) :: rest
+
+ | (I_aux (I_reset (_, id'), _) :: _) as instrs when Name.compare id id' = 0 ->
+ instrs
+
+ | I_aux (I_reinit (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
+ I_aux (I_reinit (ctyp, id', cval_subst id subst cval), aux) :: rest
+
+ | I_aux (instr, aux) :: instrs ->
+ let instrs = instrs_subst id subst instrs in
+ let instr = match instr with
+ | I_decl (ctyp, id') -> I_decl (ctyp, id')
+ | I_init (ctyp, id', cval) -> I_init (ctyp, id', cval_subst id subst cval)
+ | I_jump (cval, label) -> I_jump (cval_subst id subst cval, label)
+ | I_goto label -> I_goto label
+ | I_label label -> I_label label
+ | I_funcall (clexp, extern, fid, args) -> I_funcall (clexp, extern, fid, List.map (cval_subst id subst) args)
+ | I_copy (clexp, cval) -> I_copy (clexp, cval_subst id subst cval)
+ | I_clear (clexp, id') -> I_clear (clexp, id')
+ | I_undefined ctyp -> I_undefined ctyp
+ | I_match_failure -> I_match_failure
+ | I_end id' -> I_end id'
+ | I_if (cval, then_instrs, else_instrs, ctyp) ->
+ I_if (cval_subst id subst cval, instrs_subst id subst then_instrs, instrs_subst id subst else_instrs, ctyp)
+ | I_block instrs -> I_block (instrs_subst id subst instrs)
+ | I_try_block instrs -> I_try_block (instrs_subst id subst instrs)
+ | I_throw cval -> I_throw (cval_subst id subst cval)
+ | I_comment str -> I_comment str
+ | I_raw str -> I_raw str
+ | I_return cval -> I_return cval
+ | I_reset (ctyp, id') -> I_reset (ctyp, id')
+ | I_reinit (ctyp, id', cval) -> I_reinit (ctyp, id', cval_subst id subst cval)
+ in
+ I_aux (instr, aux) :: instrs
+
+ | [] -> []
+
+let rec clexp_subst id subst = function
+ | CL_id (id', ctyp) when Name.compare id id' = 0 ->
+ assert (ctyp_equal ctyp (clexp_ctyp subst));
+ subst
+ | CL_id (id', ctyp) -> CL_id (id', ctyp)
+ | CL_field (clexp, field) -> CL_field (clexp_subst id subst clexp, field)
+ | CL_addr clexp -> CL_addr (clexp_subst id subst clexp)
+ | CL_tuple (clexp, n) -> CL_tuple (clexp_subst id subst clexp, n)
+ | CL_void -> CL_void
+
+let rec find_function fid = function
+ | CDEF_fundef (fid', heap_return, args, body) :: _ when Id.compare fid fid' = 0 ->
+ Some (heap_return, args, body)
+
+ | cdef :: cdefs -> find_function fid cdefs
+
+ | [] -> None
+
+let inline cdefs should_inline instrs =
+ let inlines = ref (-1) in
+
+ let replace_return subst = function
+ | I_aux (I_funcall (clexp, extern, fid, args), aux) ->
+ I_aux (I_funcall (clexp_subst return subst clexp, extern, fid, args), aux)
+ | I_aux (I_copy (clexp, cval), aux) ->
+ I_aux (I_copy (clexp_subst return subst clexp, cval), aux)
+ | instr -> instr
+ in
+
+ let replace_end label = function
+ | I_aux (I_end _, aux) -> I_aux (I_goto label, aux)
+ | I_aux (I_undefined _, aux) -> I_aux (I_goto label, aux)
+ | instr -> instr
+ in
+
+ let rec inline_instr = function
+ | I_aux (I_funcall (clexp, false, function_id, args), aux) as instr when should_inline function_id ->
+ begin match find_function function_id cdefs with
+ | Some (None, ids, body) ->
+ incr inlines;
+ let inline_label = label "end_inline_" in
+ let body = List.fold_right2 instrs_subst (List.map name ids) (List.map fst args) body in
+ let body = List.map (map_instr (replace_end inline_label)) body in
+ let body = List.map (map_instr (replace_return clexp)) body in
+ I_aux (I_block (body @ [ilabel inline_label]), aux)
+ | Some (Some _, ids, body) ->
+ (* Some _ is only introduced by C backend, so we don't
+ expect it at this point. *)
+ raise (Reporting.err_general (snd aux) "Unexpected return method in IR")
+ | None -> instr
+ end
+ | instr -> instr
+ in
+
+ let rec go instrs =
+ if !inlines <> 0 then
+ begin
+ inlines := 0;
+ let instrs = List.map (map_instr inline_instr) instrs in
+ go instrs
+ end
+ else
+ instrs
+ in
+ go instrs
diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli
index beffa81e..78759d08 100644
--- a/src/jib/jib_optimize.mli
+++ b/src/jib/jib_optimize.mli
@@ -61,3 +61,6 @@ val optimize_unit : instr list -> instr list
val flatten_instrs : instr list -> instr list
val flatten_cdef : cdef -> cdef
+val unique_per_function_ids : cdef list -> cdef list
+
+val inline : cdef list -> (Ast.id -> bool) -> instr list -> instr list
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 1f477696..a086f0b9 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -68,6 +68,15 @@ let make ~initial_size () = {
nodes = Array.make initial_size None
}
+let get_vertex graph n = graph.nodes.(n)
+
+let iter_graph f graph =
+ for n = 0 to graph.next - 1 do
+ match graph.nodes.(n) with
+ | Some (x, y, z) -> f x y z
+ | None -> ()
+ done
+
(** Add a vertex to a graph, returning the node index *)
let add_vertex data graph =
let n = graph.next in
@@ -133,8 +142,11 @@ let prune visited graph =
type cf_node =
| CF_label of string
| CF_block of instr list
+ | CF_guard of cval
| CF_start
+let cval_not (f, ctyp) = (F_unary ("!", f), ctyp)
+
let control_flow_graph instrs =
let module StringMap = Map.Make(String) in
let labels = ref StringMap.empty in
@@ -150,14 +162,14 @@ let control_flow_graph instrs =
let cf_split (I_aux (aux, _)) =
match aux with
- | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end | I_match_failure | I_undefined _ -> true
+ | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end _ | I_match_failure | I_undefined _ -> true
| _ -> false
in
let rec cfg preds instrs =
let before, after = instr_split_at cf_split instrs in
let last = match after with
- | I_aux (I_label _, _) :: _ -> []
+ | I_aux ((I_label _ | I_goto _ | I_jump _), _) :: _ -> []
| instr :: _ -> [instr]
| _ -> []
in
@@ -174,7 +186,7 @@ let control_flow_graph instrs =
let e = cfg preds else_instrs in
cfg (t @ e) after
- | I_aux ((I_end | I_match_failure | I_undefined _), _) :: after ->
+ | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
cfg [] after
| I_aux (I_goto label, _) :: after ->
@@ -182,8 +194,11 @@ let control_flow_graph instrs =
cfg [] after
| I_aux (I_jump (cval, label), _) :: after ->
- List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
- cfg preds after
+ let t = add_vertex ([], CF_guard cval) graph in
+ let f = add_vertex ([], CF_guard (cval_not cval)) graph in
+ List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds;
+ add_edge t (StringMap.find label !labels) graph;
+ cfg [f] after
| I_aux (I_label label, _) :: after ->
cfg (StringMap.find label !labels :: preds) after
@@ -351,55 +366,56 @@ let dominance_frontiers graph root idom children =
(**************************************************************************)
type ssa_elem =
- | Phi of Ast.id * Ast.id list
+ | Phi of Jib.name * Jib.ctyp * Jib.name list
+ | Pi of Jib.cval list
let place_phi_functions graph df =
- let defsites = ref Bindings.empty in
+ let defsites = ref NameCTMap.empty in
- let all_vars = ref IdSet.empty in
+ let all_vars = ref NameCTSet.empty in
let rec all_decls = function
- | I_aux (I_decl (_, id), _) :: instrs ->
- IdSet.add id (all_decls instrs)
+ | I_aux ((I_init (ctyp, id, _) | I_decl (ctyp, id)), _) :: instrs ->
+ NameCTSet.add (id, ctyp) (all_decls instrs)
| _ :: instrs -> all_decls instrs
- | [] -> IdSet.empty
+ | [] -> NameCTSet.empty
in
let orig_A n =
match graph.nodes.(n) with
| Some ((_, CF_block instrs), _, _) ->
- let vars = List.fold_left IdSet.union IdSet.empty (List.map instr_writes instrs) in
- let vars = IdSet.diff vars (all_decls instrs) in
- all_vars := IdSet.union vars !all_vars;
+ let vars = List.fold_left NameCTSet.union NameCTSet.empty (List.map instr_typed_writes instrs) in
+ let vars = NameCTSet.diff vars (all_decls instrs) in
+ all_vars := NameCTSet.union vars !all_vars;
vars
- | Some _ -> IdSet.empty
- | None -> IdSet.empty
+ | Some _ -> NameCTSet.empty
+ | None -> NameCTSet.empty
in
- let phi_A = ref Bindings.empty in
+ let phi_A = ref NameCTMap.empty in
for n = 0 to graph.next - 1 do
- IdSet.iter (fun a ->
- let ds = match Bindings.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
- defsites := Bindings.add a (IntSet.add n ds) !defsites
+ NameCTSet.iter (fun a ->
+ let ds = match NameCTMap.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
+ defsites := NameCTMap.add a (IntSet.add n ds) !defsites
) (orig_A n)
done;
- IdSet.iter (fun a ->
- let workset = ref (Bindings.find a !defsites) in
+ NameCTSet.iter (fun a ->
+ let workset = ref (NameCTMap.find a !defsites) in
while not (IntSet.is_empty !workset) do
let n = IntSet.choose !workset in
workset := IntSet.remove n !workset;
IntSet.iter (fun y ->
- let phi_A_a = match Bindings.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in
+ let phi_A_a = match NameCTMap.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in
if not (IntSet.mem y phi_A_a) then
begin
begin match graph.nodes.(y) with
| Some ((phis, cfnode), preds, succs) ->
- graph.nodes.(y) <- Some ((Phi (a, Util.list_init (IntSet.cardinal preds) (fun _ -> a)) :: phis, cfnode), preds, succs)
+ graph.nodes.(y) <- Some ((Phi (fst a, snd a, Util.list_init (IntSet.cardinal preds) (fun _ -> fst a)) :: phis, cfnode), preds, succs)
| None -> assert false
end;
- phi_A := Bindings.add a (IntSet.add y phi_A_a) !phi_A;
- if not (IdSet.mem a (orig_A y)) then
+ phi_A := NameCTMap.add a (IntSet.add y phi_A_a) !phi_A;
+ if not (NameCTSet.mem a (orig_A y)) then
workset := IntSet.add y !workset
end
) df.(n)
@@ -407,49 +423,53 @@ let place_phi_functions graph df =
) !all_vars
let rename_variables graph root children =
- let counts = ref Bindings.empty in
- let stacks = ref Bindings.empty in
+ let counts = ref NameMap.empty in
+ let stacks = ref NameMap.empty in
let get_count id =
- match Bindings.find_opt id !counts with Some n -> n | None -> 0
+ match NameMap.find_opt id !counts with Some n -> n | None -> 0
in
let top_stack id =
- match Bindings.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0
+ match NameMap.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0
in
let push_stack id n =
- stacks := Bindings.add id (n :: match Bindings.find_opt id !stacks with Some s -> s | None -> []) !stacks
+ stacks := NameMap.add id (n :: match NameMap.find_opt id !stacks with Some s -> s | None -> []) !stacks
+ in
+
+ let ssa_name i = function
+ | Name (id, _) -> Name (id, i)
+ | Have_exception _ -> Have_exception i
+ | Current_exception _ -> Current_exception i
+ | Return _ -> Return i
in
let rec fold_frag = function
| F_id id ->
let i = top_stack id in
- F_id (append_id id ("_" ^ string_of_int i))
+ F_id (ssa_name i id)
| F_ref id ->
let i = top_stack id in
- F_ref (append_id id ("_" ^ string_of_int i))
+ F_ref (ssa_name i id)
| F_lit vl -> F_lit vl
- | F_have_exception -> F_have_exception
- | F_current_exception -> F_current_exception
| F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2)
| F_unary (op, f) -> F_unary (op, fold_frag f)
| F_call (id, fs) -> F_call (id, List.map fold_frag fs)
| F_field (f, field) -> F_field (fold_frag f, field)
| F_raw str -> F_raw str
+ | F_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (fold_frag f, ctor, unifiers, ctyp)
+ | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, fold_frag f)
| F_poly f -> F_poly (fold_frag f)
in
let rec fold_clexp = function
| CL_id (id, ctyp) ->
let i = get_count id + 1 in
- counts := Bindings.add id i !counts;
+ counts := NameMap.add id i !counts;
push_stack id i;
- CL_id (append_id id ("_" ^ string_of_int i), ctyp)
+ CL_id (ssa_name i id, ctyp)
| CL_field (clexp, field) -> CL_field (fold_clexp clexp, field)
| CL_addr clexp -> CL_addr (fold_clexp clexp)
| CL_tuple (clexp, n) -> CL_tuple (fold_clexp clexp, n)
- | CL_current_exception ctyp -> CL_current_exception ctyp
- | CL_have_exception -> CL_have_exception
- | CL_return ctyp -> CL_return ctyp
| CL_void -> CL_void
in
@@ -465,15 +485,20 @@ let rename_variables graph root children =
I_copy (fold_clexp clexp, cval)
| I_decl (ctyp, id) ->
let i = get_count id + 1 in
- counts := Bindings.add id i !counts;
+ counts := NameMap.add id i !counts;
push_stack id i;
- I_decl (ctyp, append_id id ("_" ^ string_of_int i))
+ I_decl (ctyp, ssa_name i id)
| I_init (ctyp, id, cval) ->
let cval = fold_cval cval in
let i = get_count id + 1 in
- counts := Bindings.add id i !counts;
+ counts := NameMap.add id i !counts;
push_stack id i;
- I_init (ctyp, append_id id ("_" ^ string_of_int i), cval)
+ I_init (ctyp, ssa_name i id, cval)
+ | I_jump (cval, label) ->
+ I_jump (fold_cval cval, label)
+ | I_end id ->
+ let i = top_stack id in
+ I_end (ssa_name i id)
| instr -> instr
in
I_aux (aux, annot)
@@ -483,24 +508,28 @@ let rename_variables graph root children =
| CF_start -> CF_start
| CF_block instrs -> CF_block (List.map ssa_instr instrs)
| CF_label label -> CF_label label
+ | CF_guard cval -> CF_guard (fold_cval cval)
in
let ssa_ssanode = function
- | Phi (id, args) ->
+ | Phi (id, ctyp, args) ->
let i = get_count id + 1 in
- counts := Bindings.add id i !counts;
+ counts := NameMap.add id i !counts;
push_stack id i;
- Phi (append_id id ("_" ^ string_of_int i), args)
+ Phi (ssa_name i id, ctyp, args)
+ | Pi _ -> assert false (* Should not be introduced at this point *)
in
let fix_phi j = function
- | Phi (id, ids) ->
- Phi (id, List.mapi (fun k a ->
- if k = j then
- let i = top_stack a in
- append_id a ("_" ^ string_of_int i)
- else a)
- ids)
+ | Phi (id, ctyp, ids) ->
+ let fix_arg k a =
+ if k = j then
+ let i = top_stack a in
+ ssa_name i a
+ else a
+ in
+ Phi (id, ctyp, List.mapi fix_arg ids)
+ | Pi _ -> assert false (* Should not be introduced at this point *)
in
let rec rename n =
@@ -529,6 +558,53 @@ let rename_variables graph root children =
in
rename root
+let place_pi_functions graph start idom children =
+ let get_guard = function
+ | CF_guard guard -> [guard]
+ | _ -> []
+ in
+ let get_pi_contents ssanodes =
+ List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
+ in
+
+ let rec go n =
+ begin match graph.nodes.(n) with
+ | Some ((ssa, cfnode), preds, succs) ->
+ let p = idom.(n) in
+ if p <> -1 then
+ begin match graph.nodes.(p) with
+ | Some ((dom_ssa, _), _, _) ->
+ let args = get_guard cfnode @ get_pi_contents dom_ssa in
+ graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs)
+ | None -> assert false
+ end
+ | None -> assert false
+ end;
+ IntSet.iter go children.(n)
+ in
+ go start
+
+(** Remove p nodes. Assumes the graph is acyclic. *)
+let remove_nodes remove_cf graph =
+ for n = 0 to graph.next - 1 do
+ match graph.nodes.(n) with
+ | Some ((_, cfnode), preds, succs) when remove_cf cfnode ->
+ IntSet.iter (fun pred ->
+ match graph.nodes.(pred) with
+ | Some (content, preds', succs') ->
+ graph.nodes.(pred) <- Some (content, preds', IntSet.remove n (IntSet.union succs succs'))
+ | None -> assert false
+ ) preds;
+ IntSet.iter (fun succ ->
+ match graph.nodes.(succ) with
+ | Some (content, preds', succs') ->
+ graph.nodes.(succ) <- Some (content, IntSet.remove n (IntSet.union preds preds'), succs')
+ | None -> assert false
+ ) succs;
+ graph.nodes.(n) <- None
+ | _ -> ()
+ done
+
let ssa instrs =
let start, finish, cfg = control_flow_graph instrs in
let idom = immediate_dominators cfg start in
@@ -536,36 +612,39 @@ let ssa instrs =
let df = dominance_frontiers cfg start idom children in
place_phi_functions cfg df;
rename_variables cfg start children;
- cfg
+ place_pi_functions cfg start idom children;
+ (* remove_guard_nodes (function CF_guard _ -> true | CF_label _ -> true | _ -> false) cfg; *)
+ start, cfg
(* Debugging utilities for outputing Graphviz files. *)
+let string_of_ssainstr = function
+ | Phi (id, ctyp, args) ->
+ string_of_name id ^ " : " ^ string_of_ctyp ctyp ^ " = &phi;(" ^ Util.string_of_list ", " string_of_name args ^ ")"
+ | Pi cvals ->
+ "&pi;(" ^ Util.string_of_list ", " (fun (f, _) -> String.escaped (string_of_fragment ~zencode:false f)) cvals ^ ")"
+
let string_of_phis = function
| [] -> ""
- | phis -> Util.string_of_list "\\l" (fun (Phi (id, args)) -> string_of_id id ^ " = phi(" ^ Util.string_of_list ", " string_of_id args ^ ")") phis ^ "\\l"
+ | phis -> Util.string_of_list "\\l" string_of_ssainstr phis ^ "\\l"
let string_of_node = function
| (phis, CF_label label) -> string_of_phis phis ^ label
| (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
| (phis, CF_start) -> string_of_phis phis ^ "START"
+ | (phis, CF_guard cval) -> string_of_phis phis ^ (String.escaped (Pretty_print_sail.to_string (pp_cval cval)))
let vertex_color = function
| (_, CF_start) -> "peachpuff"
| (_, CF_block _) -> "white"
| (_, CF_label _) -> "springgreen"
-
-let edge_color node_from node_to =
- match node_from, node_to with
- | CF_block _, CF_block _ -> "black"
- | CF_label _, CF_block _ -> "red"
- | CF_block _, CF_label _ -> "blue"
- | _, _ -> "deeppink"
+ | (_, CF_guard _) -> "yellow"
let make_dot out_chan graph =
Util.opt_colors := false;
output_string out_chan "digraph DEPS {\n";
let make_node i n =
- output_string out_chan (Printf.sprintf " n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n))
+ output_string out_chan (Printf.sprintf " n%i [label=\"%i\\n%s\\l\";shape=box;style=filled;fillcolor=%s];\n" i i (string_of_node n) (vertex_color n))
in
let make_line i s =
output_string out_chan (Printf.sprintf " n%i -> n%i [color=black];\n" i s)
@@ -584,7 +663,7 @@ let make_dominators_dot out_chan idom graph =
Util.opt_colors := false;
output_string out_chan "digraph DOMS {\n";
let make_node i n =
- output_string out_chan (Printf.sprintf " n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n))
+ output_string out_chan (Printf.sprintf " n%i [label=\"%i\\n%s\\l\";shape=box;style=filled;fillcolor=%s];\n" i i (string_of_node n) (vertex_color n))
in
let make_line i s =
output_string out_chan (Printf.sprintf " n%i -> n%i [color=black];\n" i s)
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 3796a114..b146861c 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -57,6 +57,12 @@ type 'a array_graph
underlying array. *)
val make : initial_size:int -> unit -> 'a array_graph
+module IntSet : Set.S with type elt = int
+
+val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
+
+val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit
+
(** Add a vertex to a graph, returning the index of the inserted
vertex. If the number of vertices exceeds the size of the
underlying array, then it is dynamically resized. *)
@@ -69,17 +75,25 @@ val add_edge : int -> int -> 'a array_graph -> unit
type cf_node =
| CF_label of string
| CF_block of Jib.instr list
+ | CF_guard of Jib.cval
| CF_start
val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph
+(** [immediate_dominators graph root] will calculate the immediate
+ dominators for a control flow graph with a specified root node. *)
+val immediate_dominators : 'a array_graph -> int -> int array
+
type ssa_elem =
- | Phi of Ast.id * Ast.id list
+ | Phi of Jib.name * Jib.ctyp * Jib.name list
+ | Pi of Jib.cval list
(** Convert a list of instructions into SSA form *)
-val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph
+val ssa : Jib.instr list -> int * (ssa_elem list * cf_node) array_graph
(** Output the control-flow graph in graphviz format for
debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png
image of the graph. *)
val make_dot : out_channel -> (ssa_elem list * cf_node) array_graph -> unit
+
+val make_dominators_dot : out_channel -> int array -> (ssa_elem list * cf_node) array_graph -> unit
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 81cd07ef..904e0209 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -82,12 +82,12 @@ let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals =
let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals =
I_aux (I_funcall (clexp, true, id, cvals), (instr_number (), l))
+let icall ?loc:(l=Parse_ast.Unknown) clexp extern id cvals =
+ I_aux (I_funcall (clexp, extern, id, cvals), (instr_number (), l))
+
let icopy l clexp cval =
I_aux (I_copy (clexp, cval), (instr_number (), l))
-let ialias l clexp cval =
- I_aux (I_alias (clexp, cval), (instr_number (), l))
-
let iclear ?loc:(l=Parse_ast.Unknown) ctyp id =
I_aux (I_clear (ctyp, id), (instr_number (), l))
@@ -95,7 +95,7 @@ let ireturn ?loc:(l=Parse_ast.Unknown) cval =
I_aux (I_return cval, (instr_number (), l))
let iend ?loc:(l=Parse_ast.Unknown) () =
- I_aux (I_end, (instr_number (), l))
+ I_aux (I_end (Return (-1)), (instr_number (), l))
let iblock ?loc:(l=Parse_ast.Unknown) instrs =
I_aux (I_block instrs, (instr_number (), l))
@@ -105,11 +105,13 @@ let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
let ithrow ?loc:(l=Parse_ast.Unknown) cval =
I_aux (I_throw cval, (instr_number (), l))
+
let icomment ?loc:(l=Parse_ast.Unknown) str =
I_aux (I_comment str, (instr_number (), l))
let ilabel ?loc:(l=Parse_ast.Unknown) label =
I_aux (I_label label, (instr_number (), l))
+
let igoto ?loc:(l=Parse_ast.Unknown) label =
I_aux (I_goto label, (instr_number (), l))
@@ -125,25 +127,52 @@ let iraw ?loc:(l=Parse_ast.Unknown) str =
let ijump ?loc:(l=Parse_ast.Unknown) cval label =
I_aux (I_jump (cval, label), (instr_number (), l))
+module Name = struct
+ type t = name
+ let compare id1 id2 =
+ match id1, id2 with
+ | Name (x, n), Name (y, m) ->
+ let c1 = Id.compare x y in
+ if c1 = 0 then compare n m else c1
+ | Have_exception n, Have_exception m -> compare n m
+ | Current_exception n, Current_exception m -> compare n m
+ | Return n, Return m -> compare n m
+ | Name _, _ -> 1
+ | _, Name _ -> -1
+ | Have_exception _, _ -> 1
+ | _, Have_exception _ -> -1
+ | Current_exception _, _ -> 1
+ | _, Current_exception _ -> -1
+end
+
+module NameSet = Set.Make(Name)
+module NameMap = Map.Make(Name)
+
+let current_exception = Current_exception (-1)
+let have_exception = Have_exception (-1)
+let return = Return (-1)
+
+let name id = Name (id, -1)
+
let rec frag_rename from_id to_id = function
- | F_id id when Id.compare id from_id = 0 -> F_id to_id
+ | F_id id when Name.compare id from_id = 0 -> F_id to_id
| F_id id -> F_id id
- | F_ref id when Id.compare id from_id = 0 -> F_ref to_id
+ | F_ref id when Name.compare id from_id = 0 -> F_ref to_id
| F_ref id -> F_ref id
| F_lit v -> F_lit v
- | F_have_exception -> F_have_exception
- | F_current_exception -> F_current_exception
| F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags)
| F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2)
| F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f)
| F_field (f, field) -> F_field (frag_rename from_id to_id f, field)
| F_raw raw -> F_raw raw
+ | F_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (frag_rename from_id to_id f, ctor, unifiers, ctyp)
+ | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, frag_rename from_id to_id f)
| F_poly f -> F_poly (frag_rename from_id to_id f)
let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
let rec clexp_rename from_id to_id = function
- | CL_id (id, ctyp) when Id.compare id from_id = 0 -> CL_id (to_id, ctyp)
+ | CL_id (id, ctyp) when Name.compare id from_id = 0 -> CL_id (to_id, ctyp)
| CL_id (id, ctyp) -> CL_id (id, ctyp)
| CL_field (clexp, field) ->
CL_field (clexp_rename from_id to_id clexp, field)
@@ -151,17 +180,14 @@ let rec clexp_rename from_id to_id = function
CL_addr (clexp_rename from_id to_id clexp)
| CL_tuple (clexp, n) ->
CL_tuple (clexp_rename from_id to_id clexp, n)
- | CL_current_exception ctyp -> CL_current_exception ctyp
- | CL_have_exception -> CL_have_exception
- | CL_return ctyp -> CL_return ctyp
| CL_void -> CL_void
let rec instr_rename from_id to_id (I_aux (instr, aux)) =
let instr = match instr with
- | I_decl (ctyp, id) when Id.compare id from_id = 0 -> I_decl (ctyp, to_id)
+ | I_decl (ctyp, id) when Name.compare id from_id = 0 -> I_decl (ctyp, to_id)
| I_decl (ctyp, id) -> I_decl (ctyp, id)
- | I_init (ctyp, id, cval) when Id.compare id from_id = 0 ->
+ | I_init (ctyp, id, cval) when Name.compare id from_id = 0 ->
I_init (ctyp, to_id, cval_rename from_id to_id cval)
| I_init (ctyp, id, cval) ->
I_init (ctyp, id, cval_rename from_id to_id cval)
@@ -178,9 +204,8 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
I_funcall (clexp_rename from_id to_id clexp, extern, id, List.map (cval_rename from_id to_id) args)
| I_copy (clexp, cval) -> I_copy (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
- | I_alias (clexp, cval) -> I_alias (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
- | I_clear (ctyp, id) when Id.compare id from_id = 0 -> I_clear (ctyp, to_id)
+ | I_clear (ctyp, id) when Name.compare id from_id = 0 -> I_clear (ctyp, to_id)
| I_clear (ctyp, id) -> I_clear (ctyp, id)
| I_return cval -> I_return (cval_rename from_id to_id cval)
@@ -203,12 +228,13 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
| I_match_failure -> I_match_failure
- | I_end -> I_end
+ | I_end id when Name.compare id from_id = 0 -> I_end to_id
+ | I_end id -> I_end id
- | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id)
+ | I_reset (ctyp, id) when Name.compare id from_id = 0 -> I_reset (ctyp, to_id)
| I_reset (ctyp, id) -> I_reset (ctyp, id)
- | I_reinit (ctyp, id, cval) when Id.compare id from_id = 0 ->
+ | I_reinit (ctyp, id, cval) when Name.compare id from_id = 0 ->
I_reinit (ctyp, to_id, cval_rename from_id to_id cval)
| I_reinit (ctyp, id, cval) ->
I_reinit (ctyp, id, cval_rename from_id to_id cval)
@@ -229,15 +255,24 @@ let string_of_value = function
| V_unit -> "UNIT"
| V_bit Sail2_values.B0 -> "UINT64_C(0)"
| V_bit Sail2_values.B1 -> "UINT64_C(1)"
+ | V_bit Sail2_values.BU -> failwith "Undefined bit found in value"
| V_string str -> "\"" ^ str ^ "\""
- | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
- | _ -> failwith "Cannot convert value to string"
+
+let string_of_name ?zencode:(zencode=true) =
+ let ssa_num n = if n < 0 then "" else ("/" ^ string_of_int n) in
+ function
+ | Name (id, n) ->
+ (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n
+ | Have_exception n ->
+ "have_exception" ^ ssa_num n
+ | Return n ->
+ "return" ^ ssa_num n
+ | Current_exception n ->
+ "(*current_exception)" ^ ssa_num n
let rec string_of_fragment ?zencode:(zencode=true) = function
- | F_id id when zencode -> Util.zencode_string (string_of_id id)
- | F_id id -> string_of_id id
- | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id)
- | F_ref id -> "&" ^ string_of_id id
+ | F_id id -> string_of_name ~zencode:zencode id
+ | F_ref id -> "&" ^ string_of_name ~zencode:zencode id
| F_lit v -> string_of_value v
| F_call (str, frags) ->
Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags)
@@ -247,9 +282,21 @@ let rec string_of_fragment ?zencode:(zencode=true) = function
Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2)
| F_unary (op, f) ->
op ^ string_of_fragment' ~zencode:zencode f
- | F_have_exception -> "have_exception"
- | F_current_exception -> "(*current_exception)"
| F_raw raw -> raw
+ | F_ctor_kind (f, ctor, [], _) ->
+ string_of_fragment' ~zencode:zencode f ^ ".kind"
+ ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor)
+ | F_ctor_kind (f, ctor, unifiers, _) ->
+ string_of_fragment' ~zencode:zencode f ^ ".kind"
+ ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+ | F_ctor_unwrap (ctor, [], f) ->
+ Printf.sprintf "%s.%s"
+ (string_of_fragment' ~zencode:zencode f)
+ (Util.zencode_string (string_of_id ctor))
+ | F_ctor_unwrap (ctor, unifiers, f) ->
+ Printf.sprintf "%s.%s"
+ (string_of_fragment' ~zencode:zencode f)
+ (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers))
| F_poly f -> string_of_fragment ~zencode:zencode f
and string_of_fragment' ?zencode:(zencode=true) f =
match f with
@@ -284,9 +331,14 @@ and string_of_ctyp = function
constructors in variants and structs. Used for debug output. *)
and full_string_of_ctyp = function
| CT_tup ctyps -> "(" ^ Util.string_of_list ", " full_string_of_ctyp ctyps ^ ")"
- | CT_struct (id, ctors) | CT_variant (id, ctors) ->
+ | CT_struct (id, ctors) ->
"struct " ^ string_of_id id
- ^ "{ "
+ ^ "{"
+ ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
+ ^ "}"
+ | CT_variant (id, ctors) ->
+ "union " ^ string_of_id id
+ ^ "{"
^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
^ "}"
| CT_vector (true, ctyp) -> "vector(dec, " ^ full_string_of_ctyp ctyp ^ ")"
@@ -407,6 +459,13 @@ let rec ctyp_unify ctyp1 ctyp2 =
| CT_list ctyp1, CT_list ctyp2 -> ctyp_unify ctyp1 ctyp2
+ | CT_struct (id1, fields1), CT_struct (id2, fields2)
+ when Id.compare id1 id2 = 0 && List.length fields1 == List.length fields2 ->
+ if List.for_all2 (fun x y -> x = y) (List.map fst fields1) (List.map fst fields2) then
+ List.concat (List.map2 ctyp_unify (List.map snd fields1) (List.map snd fields2))
+ else
+ raise (Invalid_argument "ctyp_unify")
+
| CT_ref ctyp1, CT_ref ctyp2 -> ctyp_unify ctyp1 ctyp2
| CT_poly, _ -> [ctyp2]
@@ -466,6 +525,9 @@ let rec is_polymorphic = function
let pp_id id =
string (string_of_id id)
+let pp_name id =
+ string (string_of_name ~zencode:false id)
+
let pp_ctyp ctyp =
string (full_string_of_ctyp ctyp |> Util.yellow |> Util.clear)
@@ -476,19 +538,16 @@ let pp_cval (frag, ctyp) =
string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp
let rec pp_clexp = function
- | CL_id (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+ | CL_id (id, ctyp) -> pp_name id ^^ string " : " ^^ pp_ctyp ctyp
| CL_field (clexp, field) -> parens (pp_clexp clexp) ^^ string "." ^^ string field
| CL_tuple (clexp, n) -> parens (pp_clexp clexp) ^^ string "." ^^ string (string_of_int n)
| CL_addr clexp -> string "*" ^^ pp_clexp clexp
- | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp
- | CL_have_exception -> string "have_exception"
- | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp
| CL_void -> string "void"
let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
match instr with
| I_decl (ctyp, id) ->
- pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+ pp_keyword "var" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp
| I_if (cval, then_instrs, else_instrs, ctyp) ->
let pp_if_block = function
| [] -> string "{}"
@@ -508,20 +567,18 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
| I_try_block instrs ->
pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
| I_reset (ctyp, id) ->
- pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+ pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp
| I_init (ctyp, id, cval) ->
- pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
+ pp_keyword "create" ^^ pp_name 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
+ pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
| 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) ]
| I_copy (clexp, cval) ->
separate space [pp_clexp clexp; string "="; pp_cval cval]
- | I_alias (clexp, cval) ->
- pp_keyword "alias" ^^ separate space [pp_clexp clexp; string "="; pp_cval cval]
| I_clear (ctyp, id) ->
- pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+ pp_keyword "kill" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp
| I_return cval ->
pp_keyword "return" ^^ pp_cval cval
| I_throw cval ->
@@ -534,7 +591,7 @@ 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_end ->
+ | I_end _ ->
pp_keyword "end"
| I_undefined ctyp ->
pp_keyword "undefined" ^^ pp_ctyp ctyp
@@ -584,55 +641,72 @@ let pp_cdef = function
^^ hardline
let rec fragment_deps = function
- | F_id id | F_ref id -> IdSet.singleton id
- | F_lit _ -> IdSet.empty
+ | F_id id | F_ref id -> NameSet.singleton id
+ | F_lit _ -> NameSet.empty
| F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag
- | F_call (_, frags) -> List.fold_left IdSet.union IdSet.empty (List.map fragment_deps frags)
- | F_op (frag1, _, frag2) -> IdSet.union (fragment_deps frag1) (fragment_deps frag2)
- | F_current_exception -> IdSet.empty
- | F_have_exception -> IdSet.empty
- | F_raw _ -> IdSet.empty
+ | F_call (_, frags) -> List.fold_left NameSet.union NameSet.empty (List.map fragment_deps frags)
+ | F_op (frag1, _, frag2) -> NameSet.union (fragment_deps frag1) (fragment_deps frag2)
+ | F_ctor_kind (frag, _, _, _) -> fragment_deps frag
+ | F_ctor_unwrap (_, _, frag) -> fragment_deps frag
+ | F_raw _ -> NameSet.empty
let cval_deps = function (frag, _) -> fragment_deps frag
let rec clexp_deps = function
- | CL_id (id, _) -> IdSet.singleton id
+ | CL_id (id, _) -> NameSet.singleton id
| CL_field (clexp, _) -> clexp_deps clexp
| CL_tuple (clexp, _) -> clexp_deps clexp
| CL_addr clexp -> clexp_deps clexp
- | CL_have_exception -> IdSet.empty
- | CL_current_exception _ -> IdSet.empty
- | CL_return _ -> IdSet.empty
- | CL_void -> IdSet.empty
+ | CL_void -> NameSet.empty
(* Return the direct, read/write dependencies of a single instruction *)
let instr_deps = function
- | I_decl (ctyp, id) -> IdSet.empty, IdSet.singleton id
- | I_reset (ctyp, id) -> IdSet.empty, IdSet.singleton id
- | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, IdSet.singleton id
- | I_if (cval, _, _, _) -> cval_deps cval, IdSet.empty
- | I_jump (cval, label) -> cval_deps cval, IdSet.empty
- | I_funcall (clexp, _, _, cvals) -> List.fold_left IdSet.union IdSet.empty (List.map cval_deps cvals), clexp_deps clexp
+ | I_decl (ctyp, id) -> NameSet.empty, NameSet.singleton id
+ | I_reset (ctyp, id) -> NameSet.empty, NameSet.singleton id
+ | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NameSet.singleton id
+ | I_if (cval, _, _, _) -> cval_deps cval, NameSet.empty
+ | I_jump (cval, label) -> cval_deps cval, NameSet.empty
+ | I_funcall (clexp, _, _, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals), clexp_deps clexp
| I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp
- | I_alias (clexp, cval) -> cval_deps cval, clexp_deps clexp
- | I_clear (_, id) -> IdSet.singleton id, IdSet.empty
- | I_throw cval | I_return cval -> cval_deps cval, IdSet.empty
- | I_block _ | I_try_block _ -> IdSet.empty, IdSet.empty
- | I_comment _ | I_raw _ -> IdSet.empty, IdSet.empty
- | I_label label -> IdSet.empty, IdSet.empty
- | I_goto label -> IdSet.empty, IdSet.empty
- | I_undefined _ -> IdSet.empty, IdSet.empty
- | I_match_failure -> IdSet.empty, IdSet.empty
- | I_end -> IdSet.empty, IdSet.empty
+ | I_clear (_, id) -> NameSet.singleton id, NameSet.empty
+ | I_throw cval | I_return cval -> cval_deps cval, NameSet.empty
+ | I_block _ | I_try_block _ -> NameSet.empty, NameSet.empty
+ | I_comment _ | I_raw _ -> NameSet.empty, NameSet.empty
+ | I_label label -> NameSet.empty, NameSet.empty
+ | I_goto label -> NameSet.empty, NameSet.empty
+ | I_undefined _ -> NameSet.empty, NameSet.empty
+ | I_match_failure -> NameSet.empty, NameSet.empty
+ | I_end id -> NameSet.singleton id, NameSet.empty
+
+module NameCT = struct
+ type t = name * ctyp
+ let compare (n1, ctyp1) (n2, ctyp2) =
+ let c = Name.compare n1 n2 in
+ if c = 0 then CT.compare ctyp1 ctyp2 else c
+end
+
+module NameCTSet = Set.Make(NameCT)
+module NameCTMap = Map.Make(NameCT)
+
+let rec clexp_typed_writes = function
+ | CL_id (id, ctyp) -> NameCTSet.singleton (id, ctyp)
+ | CL_field (clexp, _) -> clexp_typed_writes clexp
+ | CL_tuple (clexp, _) -> clexp_typed_writes clexp
+ | CL_addr clexp -> clexp_typed_writes clexp
+ | CL_void -> NameCTSet.empty
+
+let instr_typed_writes (I_aux (aux, _)) =
+ match aux with
+ | I_decl (ctyp, id) | I_reset (ctyp, id) -> NameCTSet.singleton (id, ctyp)
+ | I_init (ctyp, id, _) | I_reinit (ctyp, id, _) -> NameCTSet.singleton (id, ctyp)
+ | I_funcall (clexp, _, _, _) | I_copy (clexp, _) -> clexp_typed_writes clexp
+ | _ -> NameCTSet.empty
let rec map_clexp_ctyp f = function
| CL_id (id, ctyp) -> CL_id (id, f ctyp)
| CL_field (clexp, field) -> CL_field (map_clexp_ctyp f clexp, field)
| CL_tuple (clexp, n) -> CL_tuple (map_clexp_ctyp f clexp, n)
| CL_addr clexp -> CL_addr (map_clexp_ctyp f clexp)
- | CL_current_exception ctyp -> CL_current_exception (f ctyp)
- | CL_have_exception -> CL_have_exception
- | CL_return ctyp -> CL_return (f ctyp)
| CL_void -> CL_void
let rec map_instr_ctyp f (I_aux (instr, aux)) =
@@ -645,7 +719,6 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
| I_funcall (clexp, extern, id, cvals) ->
I_funcall (map_clexp_ctyp f clexp, extern, id, List.map (fun (frag, ctyp) -> frag, f ctyp) cvals)
| I_copy (clexp, (frag, ctyp)) -> I_copy (map_clexp_ctyp f clexp, (frag, f ctyp))
- | I_alias (clexp, (frag, ctyp)) -> I_alias (map_clexp_ctyp f clexp, (frag, f ctyp))
| I_clear (ctyp, id) -> I_clear (f ctyp, id)
| I_return (frag, ctyp) -> I_return (frag, f ctyp)
| I_block instrs -> I_block (List.map (map_instr_ctyp f) instrs)
@@ -654,7 +727,7 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
| I_undefined ctyp -> I_undefined (f ctyp)
| I_reset (ctyp, id) -> I_reset (f ctyp, id)
| I_reinit (ctyp1, id, (frag, ctyp2)) -> I_reinit (f ctyp1, id, (frag, f ctyp2))
- | I_end -> I_end
+ | I_end id -> I_end id
| (I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr
in
I_aux (instr, aux)
@@ -663,8 +736,8 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
let rec map_instr f (I_aux (instr, aux)) =
let instr = match instr with
| I_decl _ | I_init _ | I_reset _ | I_reinit _
- | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _
- | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> instr
+ | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _
+ | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end _ -> instr
| I_if (cval, instrs1, instrs2, ctyp) ->
I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp)
| I_block instrs ->
@@ -678,8 +751,8 @@ let rec map_instr f (I_aux (instr, aux)) =
let rec iter_instr f (I_aux (instr, aux)) =
match instr with
| I_decl _ | I_init _ | I_reset _ | I_reinit _
- | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _
- | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> f (I_aux (instr, aux))
+ | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _
+ | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end _ -> f (I_aux (instr, aux))
| I_if (cval, instrs1, instrs2, ctyp) ->
List.iter (iter_instr f) instrs1;
List.iter (iter_instr f) instrs2
@@ -717,10 +790,10 @@ let rec map_instrs f (I_aux (instr, aux)) =
| 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_copy _ | I_alias _ | 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 | I_undefined _ | I_end -> instr
+ | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end _ -> instr
in
I_aux (instr, aux)
@@ -732,7 +805,7 @@ let map_instrs_list f instrs =
let rec instr_ids (I_aux (instr, _)) =
let reads, writes = instr_deps instr in
- IdSet.union reads writes
+ NameSet.union reads writes
let rec instr_reads (I_aux (instr, _)) =
fst (instr_deps instr)
@@ -764,7 +837,6 @@ let cval_ctyp = function (_, ctyp) -> ctyp
let rec clexp_ctyp = function
| CL_id (_, ctyp) -> ctyp
- | CL_return ctyp -> ctyp
| CL_field (clexp, field) ->
begin match clexp_ctyp clexp with
| CT_struct (id, ctors) ->
@@ -788,8 +860,6 @@ let rec clexp_ctyp = function
end
| ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp)
end
- | CL_have_exception -> CT_bool
- | CL_current_exception ctyp -> ctyp
| CL_void -> CT_unit
let rec instr_ctyps (I_aux (instr, aux)) =
@@ -805,13 +875,13 @@ let rec instr_ctyps (I_aux (instr, aux)) =
| I_funcall (clexp, _, _, cvals) ->
List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty (List.map cval_ctyp cvals)
|> CTSet.add (clexp_ctyp clexp)
- | I_copy (clexp, cval) | I_alias (clexp, cval) ->
+ | I_copy (clexp, cval) ->
CTSet.add (clexp_ctyp clexp) (CTSet.singleton (cval_ctyp cval))
| I_block instrs | I_try_block instrs ->
instrs_ctyps instrs
| I_throw cval | I_jump (cval, _) | I_return cval ->
CTSet.singleton (cval_ctyp cval)
- | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end ->
+ | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end _ ->
CTSet.empty
and instrs_ctyps instrs = List.fold_left CTSet.union CTSet.empty (List.map instr_ctyps instrs)
@@ -848,12 +918,12 @@ let instr_split_at f =
instr_split_at' f []
let rec instrs_rename from_id to_id =
- let rename id = if Id.compare id from_id = 0 then to_id else id in
+ let rename id = if Name.compare id from_id = 0 then to_id else id in
let crename = cval_rename from_id to_id in
let irename instrs = instrs_rename from_id to_id instrs in
let lrename = clexp_rename from_id to_id in
function
- | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs
+ | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Name.compare from_id new_id = 0 -> instrs
| I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs
| I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs
| I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs
@@ -861,14 +931,13 @@ 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), aux) :: instrs ->
- I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs
+ | I_aux (I_funcall (clexp, extern, function_id, cvals), aux) :: instrs ->
+ I_aux (I_funcall (lrename clexp, extern, function_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_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), 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_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
+ | (I_aux ((I_comment _ | I_raw _ | I_end _ | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
| [] -> []
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 11:27:50 +0000