Strict-SSA option to switch array encoding.

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;

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

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 =

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

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 = "<node>\tInsert run-time assertions for boolean node <node>"
 and doc_inline = "<node>\tInline node <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"