[Eva] Fixes the cvalue domain on recursive calls.

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

@@ -230,21 +230,19 @@ module State = struct
     Cvalue_transfer.assume stmt expr positive valuation s >>-: fun s ->
     s, clob
 
+  let is_direct_recursion stmt call =
+    try
+      let kf = Kernel_function.find_englobing_kf stmt in
+      Kernel_function.equal kf call.kf
+    with Not_found -> false (* Should not happen *)
+
   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 direct = is_direct_recursion stmt call in
     let state = Model.remove_variables recursion.withdrawal state in
-    let state = Model.replace_base recursion.base_substitution state in
+    let substitution = recursion.base_substitution in
     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 state = Locals_scoping.substitute substitution clob state in
+    Model.replace_base substitution state
 
   let start_call stmt call recursion valuation (state, clob) =
     let state =
@@ -256,31 +254,26 @@ module State = struct
     >>-: fun state -> state, Locals_scoping.bottom ()
 
   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 direct = is_direct_recursion stmt call in
     let pre, clob = pre in
+    let substitution = recursion.base_substitution in
+    let state = Model.replace_base substitution state in
+    let clob = if direct then clob else Locals_scoping.top () in
+    let state = Locals_scoping.substitute substitution clob state 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
-    let clob = if direct then clob else Locals_scoping.top () in
-    let state, _set =
-      Locals_scoping.substitute recursion.base_substitution clob state
-    in
-    state
+    Cvalue.Model.merge ~into:state inter
 
   let finalize_call stmt call recursion ~pre ~post =
+    let (pre, clob) = pre in
     let (post, post_clob) = post in
+    Locals_scoping.(remember_bases_with_locals clob post_clob.clob);
     let post =
-      Extlib.opt_fold (finalize_recursive_call stmt call ~pre) recursion post
+      Extlib.opt_fold
+        (finalize_recursive_call stmt call ~pre:(pre, clob))
+        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
+    Cvalue_transfer.finalize_call stmt call recursion ~pre ~post
     >>-: fun state ->
     state, clob
 

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

@@ -130,12 +130,12 @@ let make_escaping_fundec fundec clob vars state =
 let substitute substitution clob 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 replace_offsm base offsm state =
     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, set
-    else Cvalue.Model.add_base base offsm' state, Base.Hptset.add base set
+    then state
+    else Cvalue.Model.add_base base offsm' state
   in
   (* Apply the substitution to the offsetmap bound to [base] in [state] *)
   let replace_base base acc =
@@ -144,15 +144,14 @@ let substitute substitution clob state =
     | `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 acc)
+  try Base.SetLattice.fold replace_base clob.clob (replace_base Base.null state)
   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 -> acc
-  | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map acc
+  | Cvalue.Model.Top | Cvalue.Model.Bottom -> state
+  | Cvalue.Model.Map map -> Cvalue.Model.fold replace_offsm map state
 
 (*
 Local Variables:

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

@@ -71,8 +71,9 @@ 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.Hptset.t
+  Base.substitution -> clobbered_set -> Cvalue.Model.t -> Cvalue.Model.t
+(** [substitute substitution clob state] applies [substitution] to all pointer
+    values in the offsetmaps bound to variables in [clob] in [state]. *)
 
 (*
 Local Variables: