use ghost variables instead of existential variables to avoid read / write...

use ghost variables instead of existential variables to avoid read / write capture problems with variable reuse

src/backends/C/c_backend_spec.ml

@@ -237,7 +237,7 @@ let pp_locals m =
 
 let pp_ptr_decl fmt v = pp_ptr fmt v.var_id
 
-let pp_basic_assign_spec ?(pp_op = pp_equal) pp_l pp_r fmt typ var_name value =
+let pp_basic_assign_spec ?(pp_op = pp_equal) pp_l pp_r fmt (typ, var_name, value) =
   if Types.is_real_type typ && !Options.mpfr then assert false
     (* Mpfr.pp_inject_assign pp_var fmt (var_name, value) *)
   else pp_op pp_l pp_r fmt (var_name, value)
@@ -267,9 +267,7 @@ let pp_assign_spec ?pp_op m self_l pp_var_l indirect_l self_r pp_var_r
            loop_vars
            pp_var_r)
         fmt
-        typ
-        var_name
-        value
+        (typ, var_name, value)
     | (_d, LVar _i) :: _q ->
       assert false
     (* let typ' = Types.array_element_type typ in
@@ -459,6 +457,8 @@ module PrintSpec = struct
     (* fprintf fmt "ResetCleared_%a" pp_print_string f *)
     | Initialization ->
       ()
+    | GhostAssign (v1, v2) ->
+      pp_ghost (pp_assign m mem_in (pp_c_var_read m)) fmt (v1, vdecl_to_val v2)
 
   let reset_flag = dummy_var_decl "_reset" Type_predef.type_bool
 
@@ -1647,7 +1647,9 @@ module SrcMod = struct
          ~pp_prologue:pp_print_cut
          (pp_acsl_line'
             ~ghost
-            (pp_assert (PrintSpec.pp_spec (InstrMode self) m))))
+            (fun fmt (spec, asrt) ->
+               let pp = PrintSpec.pp_spec (InstrMode self) m in
+               (if asrt then pp_assert pp else pp) fmt spec)))
       instr.instr_spec
 
   let pp_ghost_parameter mem fmt inst =
@@ -1686,6 +1688,28 @@ module SrcMod = struct
         c.mc_proof
     | _, _ ->
       ()
+
+  let pp_c_decl_local_spec_var m fmt v =
+    pp_acsl_line'
+      (fun fmt v ->
+         fprintf fmt "%a;"
+           (pp_ghost (pp_c_decl_local_var m))
+           v)
+      fmt v
+
+  let get_spec_locals m =
+    let rec gather vs instr =
+      let vs = List.fold_left (fun vs (spec, _) -> match Spec_common.red spec with
+          | Predicate (GhostAssign (v, _)) -> VSet.add v vs
+          | _ -> vs) vs instr.instr_spec
+      in
+      match instr.instr_desc with
+      | MBranch (_, hl) ->
+        List.fold_left (fun vs (_, il) -> List.fold_left gather vs il) vs hl
+      | _ -> vs
+    in
+    List.fold_left gather VSet.empty m.mstep.step_instrs |> VSet.elements
+
 end
 
 module MainMod = struct
@@ -1891,8 +1915,9 @@ let rec sanitize_formula = function
     Value (sanitize_value v)
   | f ->
     f
+and sanitize_formulae fs = List.map (fun spec -> sanitize_formula spec) fs
 
-and sanitize_formulae fs = List.map sanitize_formula fs
+let sanitize_spec fs = List.map (fun (spec, asrt) -> sanitize_formula spec, asrt) fs
 
 let rec sanitize_instr i =
   let sanitize_instr_desc = function
@@ -1912,7 +1937,7 @@ let rec sanitize_instr i =
   {
     i with
     instr_desc = sanitize_instr_desc i.instr_desc;
-    instr_spec = sanitize_formulae i.instr_spec;
+    instr_spec = sanitize_spec i.instr_spec;
   }
 
 and sanitize_instrs instrs = List.map sanitize_instr instrs

src/backends/C/c_backend_src.ml

@@ -37,6 +37,10 @@ module type MODIFIERS_SRC = sig
 
   val pp_contract :
     formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+
+  val pp_c_decl_local_spec_var: machine_t -> formatter -> var_decl -> unit
+
+  val get_spec_locals: machine_t -> var_decl list
 end
 
 module EmptyMod = struct
@@ -55,6 +59,10 @@ module EmptyMod = struct
   let pp_ghost_parameter _ _ _ = ()
 
   let pp_contract _ _ _ _ _ = ()
+
+  let pp_c_decl_local_spec_var _ _ _ = ()
+
+  let get_spec_locals _ = []
 end
 
 module Main (Mod : MODIFIERS_SRC) = struct
@@ -546,17 +554,21 @@ module Main (Mod : MODIFIERS_SRC) = struct
       check
 
   let pp_print_function ~pp_prototype ~prototype ?(is_contract = false)
-      ?(pp_spec = pp_print_nothing) ?(pp_local = pp_print_nothing)
-      ?(base_locals = []) ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
+      ?(pp_spec = pp_print_nothing)
+      ?(pp_local = pp_print_nothing)
+      ?(base_locals = [])
+      ?(pp_array_mem = pp_print_nothing) ?(array_mems = [])
       ?(pp_init_mpfr_local = pp_print_nothing)
       ?(pp_clear_mpfr_local = pp_print_nothing) ?(mpfr_locals = [])
+      ?(pp_spec_local = pp_print_nothing)
+      ?(spec_locals = [])
       ?(pp_check = pp_print_nothing) ?(checks = [])
       ?(pp_extra = pp_print_nothing)
       ?(pp_instr = fun fmt _ -> pp_print_nothing fmt ()) ?(instrs = []) fmt =
     if not is_contract then
       fprintf
         fmt
-        "%a@[<v 2>%a {@,%a%a%a%a%a%a%areturn;@]@,}"
+        "%a@[<v 2>%a {@,%a%a%a%a%a%a%a%areturn;@]@,}"
         pp_spec
         ()
         pp_prototype
@@ -578,6 +590,13 @@ module Main (Mod : MODIFIERS_SRC) = struct
         (* locals initialization *)
         (pp_print_list ~pp_epilogue:pp_print_cut pp_init_mpfr_local)
         (mpfr_vars mpfr_locals)
+        (* spec vars *)
+        (pp_print_list
+           ~pp_open_box:pp_open_vbox0
+           ~pp_sep:pp_print_cut
+           ~pp_eol:pp_print_cut
+           pp_spec_local)
+        spec_locals
         (* check assertions *)
         (pp_print_list pp_check)
         checks
@@ -613,6 +632,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
         ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
         ~pp_local:(pp_c_decl_local_var m)
         ~base_locals:m.mstep.step_locals
+        ~pp_spec_local:(Mod.pp_c_decl_local_spec_var m)
+        ~spec_locals:(Mod.get_spec_locals m)
         ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
         ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
         ~mpfr_locals:m.mstep.step_locals
@@ -741,6 +762,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
         ~prototype:(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
         ~pp_local:(pp_c_decl_local_var m)
         ~base_locals:m.mstep.step_locals
+        ~pp_spec_local:(Mod.pp_c_decl_local_spec_var m)
+        ~spec_locals:(Mod.get_spec_locals m)
         ~pp_array_mem:(pp_c_decl_array_mem self)
         ~array_mems:(array_mems m)
         ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
@@ -776,6 +799,8 @@ module Main (Mod : MODIFIERS_SRC) = struct
             m.mstep.step_outputs )
         ~pp_local:(pp_c_decl_local_var m)
         ~base_locals
+        ~pp_spec_local:(Mod.pp_c_decl_local_spec_var m)
+        ~spec_locals:(Mod.get_spec_locals m)
         ~pp_init_mpfr_local:(pp_initialize m self (pp_c_var_read m))
         ~pp_clear_mpfr_local:(pp_clear m self (pp_c_var_read m))
         ~mpfr_locals:m.mstep.step_locals

src/backends/C/c_backend_src.mli

@@ -23,6 +23,10 @@ module type MODIFIERS_SRC = sig
 
   val pp_contract :
     formatter -> machine_t list -> ident -> ident -> machine_t -> unit
+
+  val pp_c_decl_local_spec_var: machine_t -> formatter -> var_decl -> unit
+
+  val get_spec_locals: machine_t -> var_decl list
 end
 
 module EmptyMod : MODIFIERS_SRC

src/corelang.mli

@@ -85,7 +85,7 @@ val mktop : top_decl_desc -> top_decl
 val mkinstr :
   ?lustre_eq:(* ?lustre_expr:expr -> *)
              eq ->
-  ?instr_spec:Machine_code_types.value_t Spec_types.formula_t list ->
+  ?instr_spec:(Machine_code_types.mc_formula_t * bool) list ->
   Machine_code_types.instr_t_desc ->
   Machine_code_types.instr_t
 

src/machine_code.ml

@@ -281,13 +281,14 @@ let translate_eq env ctx nd inputs locals outputs i eq =
           inst with
           instr_spec =
             (if fst (get_stateless_status_node nd) || spec_mp = None then []
-            else [ mk_memory_pack ~i id ])
+            else [ mk_memory_pack ~i id, true ])
             @ [
                 mk_transition
                   ~i
                   stateless
                   id
-                  (vdecls_to_vals (inputs @ locals_i @ outputs_i));
+                  (vdecls_to_vals (inputs @ locals_i @ outputs_i)),
+                true
               ];
         }
         :: ctx.s;
@@ -643,13 +644,14 @@ let translate_decl nd sch =
     mkinstr
       ~instr_spec:
         ((if fst (get_stateless_status_node nd) then []
-         else [ mk_memory_pack ~i:0 nd.node_id ])
+         else [ mk_memory_pack ~i:0 nd.node_id, true ])
         @ [
             mk_transition
               ~i:0
               stateless
               nd.node_id
-              (vdecls_to_vals nd.node_inputs);
+              (vdecls_to_vals nd.node_inputs),
+            true
           ])
       MClearReset
   in

src/machine_code_common.ml

@@ -95,6 +95,8 @@ module PrintSpec = struct
       fprintf fmt "ResetCleared_%a" pp_print_string f
     | Initialization ->
       ()
+    | GhostAssign (v1, v2) ->
+      fprintf fmt "Ghost %s = %s" v1.var_id v2.var_id
 
   let pp_spec m =
     let pp_expr fmt e = pp_expr m fmt e in
@@ -169,7 +171,7 @@ let pp_spec m =
     pp_print_list
       ~pp_open_box:pp_open_vbox0
       ~pp_prologue:pp_print_cut
-      (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
+      (fun fmt (spec, _) -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m) spec)
 
 let rec pp_instr m fmt i =
   let pp_val = pp_val m in

src/machine_code_types.mli

@@ -27,7 +27,7 @@ type instr_t = {
      *) *)
   lustre_eq : eq option;
   (* possible representation as a lustre flow equation *)
-  instr_spec : mc_formula_t list;
+  instr_spec : (mc_formula_t * bool) list; (* spec, where the boolean specifies assert *)
 }
 
 and instr_t_desc =

src/optimize_machine.ml

@@ -120,7 +120,7 @@ let rec eliminate m elim instr =
   let instr =
     {
       instr with
-      instr_spec = List.map (eliminate_formula m elim) instr.instr_spec;
+      instr_spec = List.map (fun (f, asrt) -> eliminate_formula m elim f, asrt) instr.instr_spec;
     }
   in
   match get_instr_desc instr with
@@ -782,19 +782,22 @@ let predicate_spec_replace fvar = function
   | p ->
     p
 
-let is_reassigned v asg =
-  try IMap.find v asg > 1 with Not_found -> false
+let is_reused_reassigned m fvar asg v =
+  let r_asg = IMap.filter (fun _ n -> n > 1) asg in
+  List.exists (fun v' -> v.var_id = v'.var_id) m.mstep.step_locals
+  && List.exists (fun v' -> fvar v' = v && v <> v') m.mstep.step_locals
+  && IMap.mem v.var_id r_asg
+
+let ghost_vd v =
+  { v with var_id = "__" ^ v.var_id }
 
 let rec instr_spec_replace m fvar asg t =
   let aux instr = instr_spec_replace m fvar asg instr in
-  (* quantify existentially reused vars that appears freely in the formula before substitution, *)
+  (* rename reused vars that appears freely in the formula before substitution, *)
   (* to handle the fact that those vars can be modified in a way that the formula does not hold anymore *)
-  let r_asg = IMap.filter (fun _ n -> n > 1) asg in
   let fv_m = VSet.fold (fun v fv_m ->
-      if List.exists (fun v' -> v.var_id = v'.var_id) m.mstep.step_locals
-      && List.exists (fun v' -> fvar v' = v && v <> v') m.mstep.step_locals
-      && IMap.mem v.var_id r_asg
-      then IMap.add v.var_id { v with var_id = "__" ^ v.var_id} fv_m
+      if is_reused_reassigned m fvar asg v
+      then IMap.add v.var_id (ghost_vd v) fv_m
       else fv_m)  (fv_formula m VSet.empty t) IMap.empty
   in
   let fvar v = try IMap.find v.var_id fv_m with Not_found -> fvar v in
@@ -824,9 +827,10 @@ let rec instr_spec_replace m fvar asg t =
   | f ->
     f
   in
-  let fv_t = VSet.of_list (IMap.bindings fv_m |> List.split |> snd) in
-  let fv = VSet.(elements (inter fv_t (fv_formula m empty t'))) in
-  Exists (fv, t')
+  (* let fv_t = VSet.of_list (IMap.bindings fv_m |> List.split |> snd) in *)
+  (* let fv = VSet.(elements (inter fv_t (fv_formula m empty t'))) in *)
+  (* Exists (fv, t') *)
+  t'
 
 let add_assigned v =
   IMap.update v.var_id (function
@@ -869,13 +873,45 @@ let rec instr_replace_var m fvar (asg, instrs) instr =
     | MComment _ ->
       asg, instr.instr_desc
   in
-  let instr_spec = List.map (instr_spec_replace m fvar asg) instr.instr_spec in
+  let instr_spec = List.map (fun (f, asrt) -> instr_spec_replace m fvar asg f, asrt) instr.instr_spec in
   asg, instr_cons { instr with instr_desc; instr_spec } instrs
 
 and instrs_replace_var m fvar asg instrs =
   let asg, instrs = List.fold_left (instr_replace_var m fvar) (asg, []) instrs in
   asg, List.rev instrs
 
+let add_ghost_assign (firsts, spec) v =
+  ISet.add v.var_id firsts, (Predicate (GhostAssign (ghost_vd v, v)), false) :: spec
+
+let add_ghost_assigns m fvar asg instrs =
+  let rec aux (firsts, instrs) instr =
+    let firsts, instr = match instr.instr_desc with
+      | MLocalAssign (i, _)
+        when is_reused_reassigned m fvar asg i && not (ISet.mem i.var_id firsts) ->
+        let firsts, instr_spec = add_ghost_assign (firsts, instr.instr_spec) i in
+        firsts, { instr with instr_spec }
+      | MStep (il, _, _) ->
+        let firsts, instr_spec = List.fold_left (fun (firsts, _ as acc) i ->
+            if is_reused_reassigned m fvar asg i && not (ISet.mem i.var_id firsts)
+            then add_ghost_assign acc i else acc) (firsts, instr.instr_spec) il
+        in
+        firsts, { instr with instr_spec }
+      | MBranch (g, hl) ->
+        let firsts, hl = List.fold_left (fun (firsts', hl) (h, il) ->
+            let firsts, il = aux' firsts il in
+            ISet.union firsts firsts', ((h, il) :: hl))
+            (ISet.empty, []) hl
+        in
+        firsts, { instr with instr_desc = MBranch (g, List.rev hl) }
+      | _ -> firsts, instr
+    in
+    firsts, instr :: instrs
+  and aux' firsts instrs =
+    let firsts, instrs = List.fold_left aux (firsts, []) instrs in
+    firsts, List.rev instrs
+  in
+  aux' ISet.empty instrs |> snd
+
 let step_replace_var m fvar step =
   let step_locals =
     List.fold_left
@@ -889,7 +925,8 @@ let step_replace_var m fvar step =
   let step_checks =
     List.map (fun (l, v) -> l, value_replace_var fvar v) step.step_checks
   in
-  let _, step_instrs = instrs_replace_var m fvar IMap.empty step.step_instrs in
+  let asg, step_instrs = instrs_replace_var m fvar IMap.empty step.step_instrs in
+  let step_instrs = add_ghost_assigns m fvar asg step_instrs in
   {
     step with
     step_checks;
@@ -999,9 +1036,9 @@ let machine_fusion m =
   let rec filter_instrs instrs =
     List.filter_map (fun instr ->
         let instr = { instr with
-                      instr_spec = List.map (fun t ->
+                      instr_spec = List.map (fun (t, asrt) ->
                           let fv = VSet.(elements (filter is_unused (fv_formula m empty t))) in
-                          Exists (fv, t)) instr.instr_spec }
+                          Exists (fv, t), asrt) instr.instr_spec }
         in
         match get_instr_desc instr with
         | MLocalAssign (v, _) ->

src/spec_types.ml

@@ -28,6 +28,7 @@ type 'a predicate_t =
   | MemoryPack of ident * ident option * int option
   | Initialization
   | ResetCleared of ident
+  | GhostAssign of var_decl * var_decl
 
 type 'a formula_t =
   | True

src/spec_types.mli

@@ -28,6 +28,7 @@ type 'a predicate_t =
   | MemoryPack of ident * ident option * int option
   | Initialization
   | ResetCleared of ident
+  | GhostAssign of var_decl * var_decl
 
 type 'a formula_t =
   | True