machine optimization now supports input reuse

src/optimize_machine.ml

@@ -966,7 +966,7 @@ let add_ghost_assigns_reassigned rasg instrs =
           (fun i ->
             match VMap.find_opt i rasg with
             | Some ns ->
-              IntS.exists (( = ) n) ns
+              IntS.is_empty ns || IntS.exists (( = ) n) ns
             | _ ->
               false)
           il
@@ -1056,19 +1056,19 @@ let step_replace_var m reuse step =
   let step_checks =
     List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks
   in
-  let rec asg_instr rasg k (n, asg) instr =
+  let rec asg_instr rank_input rasg k (n, asg) instr =
     (* k: instruction block index (equation index)
      * n: instruction index (absolute) *)
     match instr.instr_desc with
     | MLocalAssign (i, v) ->
-      n + 1, if silly_asg i v then asg else add_assigned rasg n k i asg
+      n + 1, if n >= rank_input && silly_asg i v then asg else add_assigned rasg n k i asg
     | MStep (il, _, _) ->
       n + 1, List.fold_right (add_assigned rasg n k) il asg
     | MBranch (_, hl) ->
       let n, asg =
         List.fold_left
           (fun (n, asg) (_, il) ->
-            let n, asg = List.fold_left (asg_instr rasg k) (n, asg) il in
+            let n, asg = List.fold_left (asg_instr rank_input rasg k) (n, asg) il in
             n, asg)
           (n, asg)
           hl
@@ -1077,39 +1077,44 @@ let step_replace_var m reuse step =
     | _ ->
       n + 1, asg
   in
-  let assigned rasg asg instrs =
+  let assigned rank_input rasg asg instrs =
     let _, (_, asg) =
       List.fold_left
-        (fun (k, acc) i -> k + 1, asg_instr rasg k acc i)
+        (fun (k, acc) i -> k + 1, asg_instr rank_input rasg k acc i)
         (0, (0, asg))
         instrs
     in
     asg
   in
   (* SSA *)
-  let step_instrs = add_ghost_assigns fvar step.step_instrs in
+  let input_instrs = List.map Machine_code_common.(fun v -> mk_assign v (vdecl_to_val v)) step.step_inputs in
+  let nb_inputs = List.length input_instrs in
+  let step_instrs  = input_instrs @ step.step_instrs in
+  let step_instrs = add_ghost_assigns fvar step_instrs in
   (* register the locations of assignments *)
-  let asg = assigned false VMap.empty step_instrs in
-  (* let pp fmt (ns, k, b) = *)
-  (*   Format.( *)
-  (*     fprintf fmt "[%a]%n:%a" *)
-  (*       (pp_comma_list pp_print_int) (IntS.elements ns) *)
-  (*       k *)
-  (*       pp_print_bool b) *)
-  (* in *)
-  (* Format.printf "AVANT %a@." (VMap.pp pp) asg; *)
+  let asg = assigned nb_inputs false VMap.empty step_instrs in
+  let pp fmt (ns, k, b) =
+    Format.(
+      fprintf fmt "[%a]%n:%a"
+        (pp_comma_list pp_print_int) (IntS.elements ns)
+        k
+        pp_print_bool b)
+  in
+  (*Format.printf "AVANT %a@." (VMap.pp pp) asg;*)
   (* SSA *)
   let step_instrs = instrs_replace_var m fvar step_instrs in
   (* update the locations of assignments, consider as reassignments only the
      ones appearing *after* the original one *)
-  let asg = assigned true asg step_instrs in
+  let asg = assigned nb_inputs true asg step_instrs in
   let rasg =
     VMap.filter_map (fun _ (ns, _, b) -> if b then Some ns else None) asg
   in
-  (* Format.printf "APRES %a@." (VMap.pp pp) asg; *)
+  (*Format.printf "APRES %a@." (VMap.pp pp) asg;*)
   (* not SSA anymore *)
+  (*Format.eprintf "step instrs before ghost reassign@.%a@." (pp_instrs m) step_instrs;*)
   let step_instrs = add_ghost_assigns_reassigned rasg step_instrs in
   (* not SSA anymore *)
+  (*Format.eprintf "step instrs after ghost reassign@.%a@." (pp_instrs m) step_instrs;*)
   let step_instrs = remove_skips_instrs step_instrs in
   { step with step_checks; step_locals; step_instrs }