removed a bug in reuse for the specific case of early inlined assignments

src/machine_code_common.mli

@@ -33,6 +33,7 @@ val arrow_machine : machine_t
 val new_instance : top_decl -> tag -> ident
 val value_of_dimension : machine_t -> Dimension.t -> value_t
 val dimension_of_value : value_t -> Dimension.t
+val pp_spec : machine_t -> Format.formatter -> (mc_formula_t * bool) list -> unit
 val pp_instr : machine_t -> Format.formatter -> instr_t -> unit
 val pp_instrs : machine_t -> Format.formatter -> instr_t list -> unit
 val pp_machines : Format.formatter -> machine_t list -> unit

src/optimize_machine.ml

@@ -851,8 +851,9 @@ let predicate_spec_replace fvar = function
   | p ->
     p
 
-let rec instr_spec_replace fvar t =
-  let aux t = instr_spec_replace fvar t in
+let rec instr_spec_replace m fvar t =
+  (*Format.eprintf "instr_spec_replace %a@." (fun fmt t -> Machine_code_common.pp_spec m fmt [t, true]) t;*)
+  let aux t = instr_spec_replace m fvar t in
   match t with
   | Equal (e1, e2) ->
     Equal (expr_spec_replace fvar e1, expr_spec_replace fvar e2)
@@ -866,17 +867,17 @@ let rec instr_spec_replace fvar t =
     Imply (aux a, aux b)
   | Exists (xs, a) ->
     let fvar v = if List.mem v xs then v else fvar v in
-    Exists (xs, instr_spec_replace fvar a)
+    Exists (xs, instr_spec_replace m fvar a)
   | Forall (xs, a) ->
     let fvar v = if List.mem v xs then v else fvar v in
-    Forall (xs, instr_spec_replace fvar a)
+    Forall (xs, instr_spec_replace m fvar a)
   | Ternary (e, a, b) ->
     Ternary (expr_spec_replace fvar e, aux a, aux b)
   | Predicate p ->
     Predicate (predicate_spec_replace fvar p)
   | ExistsMem (f, a, b) ->
     ExistsMem (f, aux a, aux b)
-  | f ->
+  | f -> 
     f
 
 let rec instr_replace_var m fvar instrs instr =
@@ -915,7 +916,8 @@ and instrs_replace_var m fvar instrs =
   let instrs = List.fold_left (instr_replace_var m fvar) [] instrs in
   List.rev instrs
 
-let rec add_ghost_assign fvar instr =
+let rec add_ghost_assign m fvar instr =
+  (*Format.eprintf "add_ghost_assign %a @." (Machine_code_common.pp_instr m) instr;*)
   let aux spec i =
     let v = fvar i in
     if (fvar i).var_id = i.var_id then spec
@@ -929,12 +931,12 @@ let rec add_ghost_assign fvar instr =
     let instr_spec = List.fold_left aux instr.instr_spec il in
     { instr with instr_spec }
   | MBranch (e, hl) ->
-    let hl = List.map (fun (h, l) -> h, add_ghost_assigns fvar l) hl in
+    let hl = List.map (fun (h, l) -> h, add_ghost_assigns m fvar l) hl in
     { instr with instr_desc = MBranch (e, hl) }
   | _ ->
     instr
 
-and add_ghost_assigns fvar = List.map (add_ghost_assign fvar)
+and add_ghost_assigns m fvar = List.map (add_ghost_assign m fvar)
 
 let ghost_vd m =
   let used = List.fold_left (fun set v -> ISet.add v.var_id set) ISet.empty m.mstep.step_inputs in
@@ -943,12 +945,12 @@ let ghost_vd m =
   let used = ref used in
   (fun v -> 
     let ghost_name = mk_new_name (fun v -> ISet.mem v !used) ("_" ^ v.var_id) in
-    used := ISet.add ghost_name !used;
+    used := ISet.add v.var_id !used;
     { v with var_id = ghost_name })
 
 module IntS = Set.Make (Int)
 
-let add_ghost_assigns_reassigned ghost_vd_m rasg instrs =
+let add_ghost_assigns_reassigned m ghost_vd_m rasg instrs =
   let rec aux n instr fvar =
     match instr.instr_desc with
     | MLocalAssign (i, _) ->
@@ -1012,9 +1014,16 @@ let add_ghost_assigns_reassigned ghost_vd_m rasg instrs =
     List.fold_left
       (fun (n, instrs, fvar) instr ->
         let n, instr, fvar = aux n instr fvar in
+        (*Format.eprintf "instr_spec_replace %a@." (Machine_code_common.pp_instr m) instr;*)
         let instr_spec =
-          List.map (fun (t, b) -> instr_spec_replace fvar t, b) instr.instr_spec
+          match instr.instr_desc, instr.instr_spec with
+          (* special case for early inlined assignment *)
+          | MComment _, (Predicate (GhostAssign (v, e)), b) :: spec ->
+           (Predicate (GhostAssign (v, value_replace_var fvar e)), b) :: List.map (fun (t, b) -> instr_spec_replace m fvar t, b) spec
+        | _         , spec     ->
+           List.map (fun (t, b) -> instr_spec_replace m fvar t, b) spec
         in
+        (*Format.eprintf "instr_spec_replace -> %a@." (Machine_code_common.pp_spec m) instr_spec;*)
         n, { instr with instr_spec } :: instrs, fvar)
       (0, [], fun v -> v)
       instrs
@@ -1099,7 +1108,7 @@ let step_replace_var m reuse step =
   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
+  let step_instrs = add_ghost_assigns m fvar step_instrs in
   (* register the locations of assignments *)
   let asg = assigned nb_inputs false VMap.empty step_instrs in
   let pp fmt (ns, k, b) =
@@ -1121,7 +1130,7 @@ let step_replace_var m reuse step =
   (*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 ghost_vd_m rasg step_instrs in
+  let step_instrs = add_ghost_assigns_reassigned m ghost_vd_m 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