diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 8dddcc9..eab6112 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -84,7 +84,7 @@ let compile source_f = let modul = Names.modul_of_string modname in Initial.initialize modul; source_f |> Filename.dirname |> add_include; - + check_options (); match Misc.file_extension source_f with | "ept" -> compile_program modname source_f | "epi" -> compile_interface modname source_f @@ -124,6 +124,7 @@ let main () = "-statefuli", Arg.Set stateful_info, doc_stateful_info; "-fname", Arg.Set full_name, doc_full_name; "-itfusion", Arg.Set do_iterator_fusion, doc_itfusion; + "-strict_ssa", Arg.Set strict_ssa, doc_strict_ssa; "-memalloc", Arg.Unit do_mem_alloc_and_typing, doc_memalloc; "-only-memalloc", Arg.Set do_mem_alloc, doc_memalloc_only; "-only-linear", Arg.Set do_linear_typing, doc_linear_only; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index a8bde6d..06e3c19 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -64,7 +64,7 @@ let fresh_for = fresh_for "mls2obc" let op_from_string op = { qual = Pervasives; name = op; } let rec pattern_of_idx_list p l = - let rec aux p l = match p.pat_ty, l with + let rec aux p l = match Modules.unalias_type p.pat_ty, l with | _, [] -> p | Tarray (ty',_), idx :: l -> aux (mk_pattern ty' (Larray (p, idx))) l | _ -> internal_error "mls2obc" @@ -158,7 +158,7 @@ let mk_plus_one e = match e.e_desc with (** Creates the action list that copies [src] to [dest], updating the value at index [idx_list] with the value [v]. *) -let rec update_array dest src idx_list v = match Modules.unalias_type dest.pat_ty, idx_list with +let rec ssa_update_array dest src idx_list v = match Modules.unalias_type dest.pat_ty, idx_list with | Tarray (t, n), idx::idx_list -> (*Body of the copy loops*) let copy i = @@ -171,7 +171,7 @@ let rec update_array dest src idx_list v = match Modules.unalias_type dest.pat_t (* Update the correct element*) let src_idx = array_elt_of_exp idx src in let dest_idx = mk_pattern t (Larray (dest, idx)) in - let a_update = update_array dest_idx src_idx idx_list v in + let a_update = ssa_update_array dest_idx src_idx idx_list v in (*Copy values > idx*) let idx_plus_one = mk_plus_one idx in let a_upper = fresh_for idx_plus_one (mk_exp_static_int n) copy in @@ -181,7 +181,7 @@ let rec update_array dest src idx_list v = match Modules.unalias_type dest.pat_t (** Creates the action list that copies [src] to [dest], updating the value of field [f] with the value [v]. *) -let update_record dest src f v = +let ssa_update_record dest src f v = let assgn_act { f_name = l; f_type = ty } = let dest_l = mk_pattern ty (Lfield(dest, l)) in let src_l = mk_ext_value_exp ty (Wfield(src, l)) in @@ -384,18 +384,29 @@ and translate_act map pat let e1 = translate_extvalue_to_exp map e1 in let e2 = translate_extvalue_to_exp map e2 in let cond = bound_check_expr idx bounds in - let true_act = update_array x e1 idx e2 in - let false_act = Aassgn (x, e1) in - [ mk_ifthenelse cond true_act [false_act] ] + let copy = Aassgn (x, e1) in + if !Compiler_options.strict_ssa + then ( + let ssa_up = ssa_update_array x e1 idx e2 in + [ mk_ifthenelse cond ssa_up [copy] ] + ) else ( + let assgn = Aassgn (pattern_of_idx_list x idx, e2) in + [copy; mk_if cond [assgn]] + ) | Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Efield_update; Minils.a_params = [{ se_desc = Sfield f }] }, [e1; e2], _) -> let x = var_from_name map x in - let e1 = translate_extvalue map e1 in + let e1' = translate_extvalue map e1 in let e2 = translate_extvalue_to_exp map e2 in - update_record x e1 f e2 - + if !Compiler_options.strict_ssa + then ssa_update_record x e1' f e2 + else ( + let copy = Aassgn (x, translate_extvalue_to_exp map e1) in + let action = Aassgn (mk_pattern (Types.Tid (Modules.find_field f)) (Lfield (x, f)), e2) in + [copy; action] + ) | Minils.Evarpat n, _ -> [Aassgn (var_from_name map n, translate map act)] | _ -> @@ -533,20 +544,20 @@ and mk_node_call map call_context app loc (name_list : Obc.pattern list) args ty v @ nd.Minils.n_local, si, j, subst_act_list env s | Minils.Enode f | Minils.Efun f -> - let id = - begin match app.Minils.a_id with - None -> gen_obj_ident f - | Some id -> id - end in + let id = match app.Minils.a_id with + | None -> gen_obj_ident f + | Some id -> id + in let o = mk_obj_call_from_context call_context id in let obj = { o_ident = obj_ref_name o; o_class = f; o_params = app.Minils.a_params; o_size = size_from_call_context call_context; o_loc = loc } in - let si = (match app.Minils.a_op with - | Minils.Efun _ -> [] - | Minils.Enode _ -> [reinit o] - | _ -> assert false) in + let si = match app.Minils.a_op with + | Minils.Efun _ -> [] + | Minils.Enode _ -> [reinit o] + | _ -> assert false + in let s = [Acall (name_list, o, Mstep, args)] in [], si, [obj], s | _ -> assert false diff --git a/compiler/main/mls2seq.ml b/compiler/main/mls2seq.ml index c49ce95..78ee0d0 100644 --- a/compiler/main/mls2seq.ml +++ b/compiler/main/mls2seq.ml @@ -105,7 +105,10 @@ let generate_interface i s = | IMinils convert_fun -> convert_fun i let load_conf () = - List.iter (fun s -> (find_target s).t_load_conf ()) !target_languages + List.iter (fun s -> (find_target s).t_load_conf ()) !target_languages; + try + check_options () + with Arg.Bad m -> raise (Arg.Bad ("After loading target configurations: "^m)) (** Translation into dataflow and sequential languages, defaults to obc. *) let program p = diff --git a/compiler/obc/obc_utils.ml b/compiler/obc/obc_utils.ml index 178bd84..e10a86b 100644 --- a/compiler/obc/obc_utils.ml +++ b/compiler/obc/obc_utils.ml @@ -74,6 +74,9 @@ let mk_block ?(locals=[]) eq_list = let mk_ifthenelse cond true_act false_act = Acase (cond, [ Initial.ptrue, mk_block true_act; Initial.pfalse, mk_block false_act ]) +let mk_if cond true_act = + Acase (cond, [Initial.ptrue, mk_block true_act]) + let rec var_name x = match x.pat_desc with | Lvar x -> x diff --git a/compiler/utilities/global/compiler_options.ml b/compiler/utilities/global/compiler_options.ml index 653ef63..a077957 100644 --- a/compiler/utilities/global/compiler_options.ml +++ b/compiler/utilities/global/compiler_options.ml @@ -66,7 +66,7 @@ let boolean = ref false let target_languages : string list ref = ref [] let add_target_language s = - if s = "z3z" then boolean := true; + if s = "z3z" then boolean := true; (* TODO use load_conf instead *) target_languages := s :: !target_languages (* Optional path for generated files (C or Java) *) @@ -115,14 +115,27 @@ let do_mem_alloc_and_typing () = let use_old_scheduler = ref false +let strict_ssa = ref false + + let optim = ref false let do_optim () = -(* do_iterator_fusion := true; TODO reset when itfusion is fixed *) +(* do_iterator_fusion := true; *)(*TODO reset when itfusion is fixed *) do_mem_alloc_and_typing (); tomato := true; deadcode := true +let check_options () = + let err m = raise (Arg.Bad m) in + if !strict_ssa + then ( + if !do_mem_alloc then err "Unable to activate memory allocation with strict SSA activated."; + if !do_linear_typing then err "Unable to activate linear typing with strict SSA activated." + ) + + + let doc_verbose = "\t\t\tSet verbose mode" and doc_version = "\t\tThe version of the compiler" and doc_print_types = "\t\t\tPrint types" @@ -151,6 +164,7 @@ and doc_assert = "\tInsert run-time assertions for boolean node " and doc_inline = "\tInline node " and doc_itfusion = "\t\tEnable iterator fusion." and doc_tomato = "\t\tEnable automata minimization." +and doc_strict_ssa = "\t\tEnsure that the generated code is SSA, even for array elements." and doc_memalloc = "\t\tEnable memory allocation and linear annotations" and doc_memalloc_only = "\tEnable memory allocation" and doc_linear_only = "\t\tEnable linear annotations"