diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 43c783b2d54858680544ee538a36f4d8b63d72ac..c1520c9d3baaac926b2c658815c19c86866c3729 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/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
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index 5cf9f85698374cc848950d7abd8af4813e72fd49..506c020b29df8a5c42bcb7ca7e8a780c285c0be4 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/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,