[Eva] Documents origin.mli.

src/kernel_services/abstract_interp/origin.ml

@@ -45,6 +45,8 @@ type tt =
   | Well
   | Unknown
 
+(* Unique id for each origin. Used to keep the oldest origin when a garbled
+   mix may have several origins. *)
 module Id = State_builder.Counter (struct let name = "Origin.Id" end)
 
 let current kind =
@@ -104,6 +106,8 @@ let descr = function
     | Merge -> "imprecise merge of addresses"
     | Arith -> "arithmetic operation on addresses"
 
+(* Keep the oldest known origin: it is probably the most relevant origin, as
+   subsequent ones may have been created because of the first. *)
 let join t1 t2 =
   if t1 == t2 then t1 else
     match t1, t2 with
@@ -113,10 +117,19 @@ let join t1 t2 =
 
 let is_included = equal
 
-let is_current = function
-  | Unknown | Well -> false
-  | Origin { loc } -> Cil_datatype.Location.equal loc (Cil.CurrentLoc.get ())
 
+(* For each garbled mix origin, keep track of:
+   - the number of writes (according to [register_write] below), i.e. the number
+     of times a garbled mix with this origin has been written in a state during
+     the analysis.
+   - the number of reads (according to [register_read] below), i.e. the number
+     of times a garbled mix with this origin is used by the analysis.
+     Only reads at a different location than that of the origin are counted:
+     if a garbled mix is only used where it has been created, it has no more
+     impact on the analysis precision than any other imprecise value.
+   - the set of bases related to garbled mix with this origin.
+
+   These info are printed at the end of an Eva analysis. *)
 
 module History_Info = struct
   let name = "Origin.History"
@@ -124,24 +137,33 @@ module History_Info = struct
   let size = 32
 end
 
+(* Number of writes, number of reads, related bases. *)
 module History_Data =
   Datatype.Triple (Datatype.Int) (Datatype.Int) (Base.SetLattice)
 module History = State_builder.Hashtbl (Hashtbl) (History_Data) (History_Info)
 
 let clear () = Id.reset (); History.clear ()
 
+let is_current = function
+  | Unknown | Well -> false
+  | Origin { loc } -> Cil_datatype.Location.equal loc (Cil.CurrentLoc.get ())
+
+(* Returns true if the origin has never been registered and is related to the
+   current location. *)
 let register_write bases t =
   if is_unknown t then false else
     let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
     let count, _, _ = History.memo ~change (fun _ -> 1, 0, bases) t in
     count < 2 && is_current t
 
+(* Registers a read only if the current location is not that of the origin. *)
 let register_read bases t =
   if not (is_unknown t || is_current t) then
     let change (w, r, b) = w, r+1, Base.SetLattice.join b bases in
     ignore (History.memo ~change (fun _ -> 0, 1, bases) t)
 
-
+(* Returns the list of recorded origins, sorted by number of reads.
+   Origins with no reads are filtered. *)
 let get_history () =
   let list = List.of_seq (History.to_seq ()) in
   let list = List.filter (fun (_origin, (_, r, _)) -> r > 0) list in

src/kernel_services/abstract_interp/origin.mli

@@ -20,33 +20,35 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** The datastructures of this module can be used to track the origin
-    of a major imprecision in the values of an abstract domain. *)
-
-(** This module is generic, although currently used only by the plugin Value.
-    Within Value, values that have an imprecision origin are "garbled mix",
-    ie. a numeric value that contains bits extracted from at least one
-    pointer, and that are not the result of a translation *)
+(** This module is used to track the origin of very imprecise values
+    (namely "garbled mix", created on imprecise or unsupported operations on
+    addresses) propagated by an Eva analysis. *)
 
 include Datatype.S
 
 type kind =
-  | Misalign_read
-  | Leaf
-  | Merge
-  | Arith
+  | Misalign_read (* Misaligned read of addresses *)
+  | Leaf  (* Interpretation of assigns clause *)
+  | Merge (* Imprecise merge of addresses *)
+  | Arith (* Arithmetic operation on addresses *)
 
+(** Creates an origin of the given kind, associated with the current source
+    location extracted from [Cil.CurrentLoc]. *)
 val current: kind -> t
-(** This is automatically extracted from [Cil.CurrentLoc] *)
 
+(** Origin for garbled mix created in the initial state of the analysis
+    (not associated to a source location). *)
 val well: t
+
+(** Unknown origin. *)
 val unknown: t
 val is_unknown: t -> bool
 
-val pretty_as_reason: Format.formatter -> t -> unit
 (** Pretty-print [because of <origin>] if the origin is not {!Unknown}, or
-    nothing otherwise *)
+    nothing otherwise. *)
+val pretty_as_reason: Format.formatter -> t -> unit
 
+(** Short description of an origin. *)
 val descr: t -> string
 
 val join: t -> t -> t
@@ -56,7 +58,7 @@ val is_included: t -> t -> bool
     with the given origin.
     Returns [true] if the given origin has never been written before,
     and if it is related to the current location — in which case a warning
-    should be emitted. *)
+    should probably be emitted. *)
 val register_write: Base.SetLattice.t -> t -> bool
 
 (** Records the read of an imprecise value of the given bases,