[Eva] Comments the interpretation of recursive calls.

src/kernel_services/abstract_interp/base.mli

@@ -225,6 +225,11 @@ val register_memory_var : Cil_types.varinfo -> validity -> t
     They are created only to fill the contents of another variable.
     Their field [vsource] is set to false. *)
 
+
+(** {2 Substituting bases}
+    This is used to efficiently replace some bases by others in locations or
+    in memory states, for instance in {!Locations} or {!Lmap_sig}. *)
+
 type substitution = base Hptmap.Shape(Base).t
 (** Type used for the substitution between bases. *)
 

src/kernel_services/abstract_interp/lmap_sig.mli

@@ -150,6 +150,8 @@ val filter_by_shape: 'a Hptmap.Shape(Base.Base).t -> t -> t
 (** Removes the base if it is present. Does nothing otherwise. *)
 val remove_base : Base.t -> t -> t
 
+(** [replace_bases substitition map] replaces some bases in [map]
+    according to [substitution]. *)
 val replace_base: Base.substitution -> t -> t
 
 

src/libraries/utils/hptset.mli

@@ -89,6 +89,9 @@ module type S = sig
     (** Build a set from another [elt]-indexed map or set. *)
 
     val partition_with_shape: 'a shape -> t -> t * t
+    (** [partition_with_shape shape set] returns two sets [inter, diff] that are
+        respectively the intersection and the difference between [set] and
+        [shape]. *)
 
     val fold2_join_heterogeneous:
       cache:Hptmap_sig.cache_type ->
@@ -101,6 +104,9 @@ module type S = sig
       'b
 
     val replace: elt shape -> t -> bool * t
+    (** [replace shape set] replaces the elements of [set] according to [shape].
+        The returned boolean indicates whether the set has been modified; it is
+        false when the intersection between [shape] and [set] is empty. *)
 
     (** Clear all the caches used internally by the functions of this module.
         Those caches are not project-aware, so this function must be called

src/plugins/value/domains/abstract_domain.mli

@@ -251,11 +251,13 @@ module type Transfer = sig
     stmt -> exp -> bool ->
     (value, location, origin) valuation -> state -> state or_bottom
 
-  (** [start_call stmt call valuation state] returns an initial state
+  (** [start_call stmt call recursion valuation state] returns an initial state
       for the analysis of a called function. In particular, this function
       should introduce the formal parameters in the state, if necessary.
       - [stmt] is the statement of the call site;
       - [call] represents the call: the called function and the arguments;
+      - [recursion] is the information needed to interpret a recursive call.
+        It is None if the call is not recursive.
       - [state] is the abstract state at the call site, before the call;
       - [valuation] is a cache for all values and locations computed during
         the evaluation of the function and its arguments. *)
@@ -268,6 +270,8 @@ module type Transfer = sig
       end of the called function.
       - [stmt] is the statement of the call site;
       - [call] represents the function call and its arguments.
+      - [recursion] is the information needed to interpret a recursive call.
+        It is None if the call is not recursive.
       - [pre] and [post] are the states before and at the end of the call
         respectively. *)
   val finalize_call:

src/plugins/value/domains/simple_memory.ml

@@ -53,7 +53,7 @@ module Make_Memory (Value: Value) = struct
   module Deps = struct let l = [Ast.self] end
 
   include Hptmap.Make
-      (Base.Base) (Value)(Hptmap.Comp_unused) (Initial_Values) (Deps)
+      (Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
 
   let cache_name s =
     Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)

src/plugins/value/engine/compute_functions.ml

@@ -174,7 +174,7 @@ module Make (Abstract: Abstractions.Eva) = struct
     let use_spec =
       match recursion with
       | Some { depth } when depth >= Value_parameters.RecursiveUnroll.get () ->
-        `Spec (Recursion.recursive_spec call_kinstr kf)
+        `Spec (Recursion.get_spec call_kinstr kf)
       | _ ->
         match kf.fundec with
         | Declaration (_,_,_,_) -> `Spec (Annotations.funspec kf)

src/plugins/value/engine/recursion.ml

@@ -44,7 +44,7 @@ let mark_unknown_requires kinstr kf funspec =
   in
   List.iter emit_behavior funspec.spec_behavior
 
-let recursive_spec kinstr kf =
+let get_spec kinstr kf =
   let funspec = Annotations.funspec ~populate:false kf in
   if Cil.is_empty_funspec funspec then
     Value_parameters.abort ~current:true
@@ -174,7 +174,7 @@ let make_recursion call depth =
   let base_withdrawal = Base.Hptset.of_list list_withdrawal in
   { depth; substitution; base_substitution; withdrawal; base_withdrawal; }
 
-let get_recursion call =
+let make call =
   let call_stack = Value_util.call_stack () in
   let previous_calls = List.filter (fun (f, _) -> f == call.kf) call_stack in
   let depth = List.length previous_calls in
@@ -182,7 +182,7 @@ let get_recursion call =
   then Some (make_recursion call depth)
   else None
 
-let revert_recursion recursion =
+let revert recursion =
   let revert (v1, v2) = v2, v1 in
   let substitution = List.map revert recursion.substitution in
   let base_of_varinfo (v1, v2) = Base.of_varinfo v1, Base.of_varinfo v2 in

src/plugins/value/engine/recursion.mli

@@ -25,9 +25,14 @@
 open Cil_types
 open Eval
 
-val recursive_spec: kinstr -> kernel_function -> funspec
+(* Returns the specification for a recursive call to the given function. Fails
+   if the function has no specification. Marks the preconditions of the call
+   as unknowns. *)
+val get_spec: kinstr -> kernel_function -> funspec
 
-(** TODO *)
-val get_recursion: ('v, 'loc) call -> recursion option
+(** Creates the information about a recursive call. *)
+val make: ('v, 'loc) call -> recursion option
 
-val revert_recursion: recursion -> recursion
+(** Changes the information about a recursive call to be used at the end
+    of the call. *)
+val revert: recursion -> recursion

src/plugins/value/engine/transfer_stmt.ml

@@ -113,7 +113,7 @@ let substitution_visitor table = object
   method! vvrbl varinfo =
     match VarHashtbl.find_opt table varinfo with
     | None -> Cil.JustCopy
-    | Some lval -> Cil.ChangeTo lval
+    | Some vi -> Cil.ChangeTo vi
 end
 
 module Make (Abstract: Abstractions.Eva) = struct
@@ -483,7 +483,7 @@ module Make (Abstract: Abstractions.Eva) = struct
       >>- fun reductions ->
       (* The formals (and the locals) of the called function leave scope. *)
       let post = Domain.leave_scope kf_callee leaving_vars state in
-      let recursion = Option.map Recursion.revert_recursion recursion in
+      let recursion = Option.map Recursion.revert recursion in
       (* Computes the state after the call, from the post state at the end of
          the called function, and the pre state at the call site. *)
       Domain.finalize_call stmt call recursion ~pre ~post >>- fun state ->
@@ -582,7 +582,7 @@ module Make (Abstract: Abstractions.Eva) = struct
     compute_actuals ~subdivnb ~determinate valuation state arguments
     >>=: fun (args, valuation) ->
     let call = create_call kf args in
-    let recursion = Recursion.get_recursion call in
+    let recursion = Recursion.make call in
     let call = Extlib.opt_fold replace_recursive_call recursion call in
     call, recursion, valuation
 

src/plugins/value/eval.mli

@@ -236,13 +236,25 @@ type ('loc, 'value) call = {
 (** Information needed to interpret a recursive call.
     The local variables and formal parameters of different recursive calls
     should not be mixed up. Those of the current call must be temporary withdraw
-    or replaced from the domain states before starting the new recursive call. *)
+    or replaced from the domain states before starting the new recursive call,
+    and the inverse transformation must be made at the end of the call. *)
 type recursion = {
   depth: int;
+  (** Depth of the recursive call, i.e. the number of previous call to the
+      called function in the current callstack. *)
   substitution: (varinfo * varinfo) list;
+  (** List of variables substitutions to be performed by the domains: for each
+      pair, the first variable must be replaced by the second one in the domain
+      state. *)
   base_substitution: Base.substitution;
+  (** Same substitution as the previous field, for bases. *)
   withdrawal: varinfo list;
+  (** List of variables to be temporary removed from the state at the start of a
+      new recursive call (by the function [start_call] of the abstract domains),
+      or to be put back in the state at the end of a recursive call (by the
+      function [finalize_call] of the abstract domains).  *)
   base_withdrawal: Base.Hptset.t;
+  (** Same withdrawal as the previous field, for bases. *)
 }
 
 (** Can the results of a function call be cached with memexec? *)

src/plugins/value/values/abstract_location.mli

@@ -44,6 +44,8 @@ module type S = sig
   val to_value : location -> value
   val size : location -> Int_Base.t
 
+  (** [replace_base substitution location] replaces the variables represented
+      by the [location] according to [substitution]. *)
   val replace_base: Base.substitution -> location -> location
 
   (** {3 Alarms } *)

src/plugins/value/values/abstract_value.mli

@@ -190,6 +190,9 @@ module type S = sig
       boolean must be [true] if some of the values represented by [v] do not
       correspond to functions. It is always safe to return [`Top, true]. *)
 
+  (** For pointer values, [replace_base substitution value] replaces the bases
+      pointed to by [value] according to [substitution]. For arithmetic values,
+      this function returns the [value] unchanged.  *)
   val replace_base: Base.substitution -> t -> t
 end