Correct scalarize and java load_conf
This commit is contained in:
parent
be28156de9
commit
efa6b5cf70
4 changed files with 37 additions and 28 deletions
|
@ -54,9 +54,14 @@ let write_obc_file p =
|
|||
close_out obc;
|
||||
comment "Generation of Obc code"
|
||||
|
||||
|
||||
let java_conf () =
|
||||
Compiler_options.do_scalarize := true;
|
||||
()
|
||||
|
||||
let targets =
|
||||
[ mk_target ~interface:(IObc Cmain.interface) "c" (Obc_no_params Cmain.program);
|
||||
mk_target "java" (Obc Java_main.program);
|
||||
mk_target ~load_conf:java_conf "java" (Obc Java_main.program);
|
||||
mk_target "z3z" (Minils_no_params Sigalimain.program);
|
||||
mk_target "obc" (Obc write_obc_file);
|
||||
mk_target "obc_np" (Obc_no_params write_obc_file);
|
||||
|
|
|
@ -12,8 +12,6 @@ let mk_var ty name =
|
|||
|
||||
|
||||
let program p =
|
||||
(*Scalarize*)
|
||||
let p = Compiler_utils.pass "Scalarize" true Scalarize.program p Obc_compiler.pp in
|
||||
let p_java = Obc2java.program p in
|
||||
let dir = Compiler_utils.build_path "java" in
|
||||
Compiler_utils.ensure_dir dir;
|
||||
|
|
|
@ -2,7 +2,7 @@ open Obc
|
|||
open Obc_mapfold
|
||||
|
||||
let is_deadcode = function
|
||||
| Aassgn (lhs, e) ->
|
||||
| Aassgn (lhs, e) -> (* remove x=x equations *)
|
||||
(match e.e_desc with
|
||||
| Eextvalue w -> Obc_compare.compare_lhs_extvalue lhs w = 0
|
||||
| _ -> false
|
||||
|
|
|
@ -20,38 +20,44 @@ open Obc_mapfold
|
|||
(** Scalarize the code : any equation t = e with e_ty an array
|
||||
is transformed into : t_ref = e; for i do t[i] = t_ref[i].
|
||||
This pass assumes that the backend when encountering t_ref = (e : int^n) will NOT COPY the array
|
||||
but set a reference to it. *)
|
||||
but set a reference to it. That's why it is declared as an alias.
|
||||
No t_ref is created if e was an extended value, no calculation is done, so it can be duplicated.
|
||||
*)
|
||||
|
||||
let fresh_for = fresh_for "scalarize"
|
||||
|
||||
let act funs () a = match a with
|
||||
| Aassgn (p,e) ->
|
||||
(match e.e_ty with
|
||||
| Types.Tarray (t, size) ->
|
||||
(* a reference (alias) to the array, since we could have a full expression *)
|
||||
let array_ref = Idents.gen_var "scalarize" "a_ref" in
|
||||
let vd_array_ref = mk_var_dec array_ref p.pat_ty in
|
||||
(* reference initialization *)
|
||||
let pat_array_ref = mk_pattern ~loc:e.e_loc p.pat_ty (Lvar array_ref) in
|
||||
let init_array_ref = Aassgn (pat_array_ref, e) in
|
||||
(* the copy loop *)
|
||||
let array_ref_i i = mk_ext_value_exp t (Warray (ext_value_of_pattern pat_array_ref, i)) in
|
||||
let p_i i = mk_pattern t (Larray (p, i)) in
|
||||
let copy_i i =
|
||||
(* recursive call to deal with multidimensional arrays (go deeper) *)
|
||||
let a = Aassgn (p_i i, array_ref_i i) in
|
||||
let a, _ = act_it funs () a in
|
||||
[a]
|
||||
in
|
||||
let copy_array = fresh_for (mk_exp_const_int 0) (mk_exp_static_int size) copy_i in
|
||||
(* resulting block *)
|
||||
let block = mk_block ~locals:[vd_array_ref] [init_array_ref; copy_array] in
|
||||
Ablock block, ()
|
||||
| _ -> raise Errors.Fallback
|
||||
(match Modules.unalias_type e.e_ty with
|
||||
| Types.Tarray (t, size) ->
|
||||
let new_vd, new_eq, w_from_e = match e.e_desc with
|
||||
| Eextvalue w -> [], [], w
|
||||
| _ ->
|
||||
(* a reference (alias) to the array, since we have a full expression *)
|
||||
let array_ref = Idents.gen_var "scalarize" "a_ref" in
|
||||
let vd_array_ref = mk_var_dec ~alias:true array_ref p.pat_ty in
|
||||
(* reference initialization *)
|
||||
let pat_array_ref = mk_pattern ~loc:e.e_loc p.pat_ty (Lvar array_ref) in
|
||||
let init_array_ref = Aassgn (pat_array_ref, e) in
|
||||
[vd_array_ref], [init_array_ref], ext_value_of_pattern pat_array_ref
|
||||
in
|
||||
(* the copy loop with index [i] *)
|
||||
let array_ref_i i = mk_ext_value_exp t (Warray (w_from_e, i)) in
|
||||
let p_i i = mk_pattern t (Larray (p, i)) in
|
||||
let copy_i i =
|
||||
(* recursive call to deal with multidimensional arrays (go deeper) *)
|
||||
let a = Aassgn (p_i i, array_ref_i i) in
|
||||
let a, _ = act_it funs () a in
|
||||
[a]
|
||||
in
|
||||
let copy_array = fresh_for (mk_exp_const_int 0) (mk_exp_static_int size) copy_i in
|
||||
(* resulting block *)
|
||||
let block = mk_block ~locals:new_vd (new_eq @ [copy_array]) in
|
||||
Ablock block, ()
|
||||
| _ -> raise Errors.Fallback
|
||||
)
|
||||
| _ -> raise Errors.Fallback
|
||||
|
||||
|
||||
let program p =
|
||||
let p, _ = program_it { defaults with act = act } () p in
|
||||
p
|
||||
|
|
Loading…
Reference in a new issue