[Eva] Fixes locals_scoping and the cvalue domain on mutually recursive calls.

src/plugins/value/domains/cvalue/cvalue_domain.ml

@@ -230,31 +230,55 @@ module State = struct
     Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
     s, clob
 
-  let start_recursive_call recursion (state, clob) =
+  let start_recursive_call stmt call recursion (state, clob) =
+    let direct =
+      try
+        let kf = Kernel_function.find_englobing_kf stmt in
+        Kernel_function.equal kf call.kf
+      with Not_found -> false (* Should not happen *)
+    in
     let state = Model.remove_variables recursion.withdrawal state in
     let state = Model.replace_base recursion.base_substitution state in
-    Locals_scoping.substitute recursion.base_substitution clob state
+    let clob = if direct then clob else Locals_scoping.top () in
+    let state, set =
+      Locals_scoping.substitute recursion.base_substitution clob state
+    in
+    Locals_scoping.remember_bases_with_locals clob (Base.SetLattice.inject set);
+    state
 
   let start_call stmt call recursion valuation (state, clob) =
     let state =
       match recursion with
       | None -> state
-      | Some recursion -> start_recursive_call recursion (state, clob)
+      | Some recursion -> start_recursive_call stmt call recursion (state, clob)
     in
     Cvalue_transfer.start_call stmt call recursion valuation state
     >>-: fun state -> state, Locals_scoping.bottom ()
 
-  let finalize_recursive_call ~pre recursion (state, clob) =
+  let finalize_recursive_call stmt call ~pre recursion state =
+    let direct =
+      try
+        let kf = Kernel_function.find_englobing_kf stmt in
+        Kernel_function.equal kf call.kf
+      with Not_found -> false (* Should not happen *)
+    in
+    let pre, clob = pre in
     let shape = Base.Hptset.shape recursion.base_withdrawal in
     let inter = Cvalue.Model.filter_by_shape shape pre in
     let state = Cvalue.Model.merge ~into:state inter in
     let state = Model.replace_base recursion.base_substitution state in
-    Locals_scoping.substitute recursion.base_substitution clob state, clob
+    let clob = if direct then clob else Locals_scoping.top () in
+    let state, _set =
+      Locals_scoping.substitute recursion.base_substitution clob state
+    in
+    state
 
   let finalize_call stmt call recursion ~pre ~post =
-    let pre, clob = pre in
-    let post = Extlib.opt_fold (finalize_recursive_call ~pre) recursion post in
     let (post, post_clob) = post in
+    let post =
+      Extlib.opt_fold (finalize_recursive_call stmt call ~pre) recursion post
+    in
+    let (pre, clob) = pre in
     Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
     Cvalue_transfer.finalize_call stmt call recursion  ~pre ~post
     >>-: fun state ->

src/plugins/value/domains/cvalue/locals_scoping.ml

@@ -127,32 +127,32 @@ let make_escaping_fundec fundec clob vars state =
     in
     make_escaping ~exact:true ~escaping ~on_escaping ~within:clob.clob state
 
-
 let substitute substitution clob state =
-  (* Clean [offsm], and bind it to [base] if it is modified. *)
-  let replace_offsm base offsm state =
+  (* Apply the [substitution] to [offsm]. If it is modified, bind the new
+     offsetmap to [base] in [state], and add the [base] to [set]. *)
+  let replace_offsm base offsm (state, set) =
     let f v = snd (Cvalue.V_Or_Uninitialized.replace_base substitution v) in
     let offsm' = Cvalue.V_Offsetmap.map_on_values f offsm in
     if Cvalue.V_Offsetmap.equal offsm' offsm
-    then state
-    else Cvalue.Model.add_base base offsm' state
+    then state, set
+    else Cvalue.Model.add_base base offsm' state, Base.Hptset.add base set
   in
-  (* Clean the offsetmap bound to [base] in [state] *)
-  let replace_base base state =
-    try
-      match Cvalue.Model.find_base base state with
-      | `Top | `Bottom -> state
-      | `Value offsm -> replace_offsm base offsm state
-    with Not_found -> state
+  (* Apply the substitution to the offsetmap bound to [base] in [state] *)
+  let replace_base base acc =
+    match Cvalue.Model.find_base base state with
+    | `Value offsm -> replace_offsm base offsm acc
+    | `Top | `Bottom -> acc
+    | exception Not_found -> acc
   in
+  let acc = state, Base.Hptset.empty in
   (* Iterate on all the bases that might contain a variable to substitute *)
-  try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null state)
+  try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null acc)
   with Abstract_interp.Error_Top ->
   (* [clob] is too imprecise. Iterate on the entire memory state instead,
      which is much slower. *)
   match state with
-  | Cvalue.Model.Top | Cvalue.Model.Bottom -> state
-  | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map state
+  | Cvalue.Model.Top | Cvalue.Model.Bottom -> acc
+  | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map acc
 
 (*
 Local Variables:

src/plugins/value/domains/cvalue/locals_scoping.mli

@@ -71,7 +71,8 @@ val make_escaping_fundec:
     function, in which case a different warning is emitted. *)
 
 val substitute:
-  Base.substitution -> clobbered_set -> Cvalue.Model.t -> Cvalue.Model.t
+  Base.substitution -> clobbered_set -> Cvalue.Model.t ->
+  Cvalue.Model.t * Base.Hptset.t
 
 (*
 Local Variables: