[Eva] Keeps an history of garbled mix origins.

src/kernel_services/abstract_interp/origin.ml

@@ -88,7 +88,7 @@ module Prototype = struct
       Format.fprintf fmt "%s@ {%a}" (kind_label kind) pretty_loc loc
 end
 
-include Datatype.Make (Prototype)
+include Datatype.Make_with_collections (Prototype)
 
 let pretty_as_reason fmt org =
   if not (is_unknown org)
@@ -103,6 +103,10 @@ 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 ())
+
 (* Well and Unknown origins have no location information.
    Leaf origins are also imprecise, because we may create tons of those,
    that get reduced to precise values by the specifications of the function. *)
@@ -110,6 +114,67 @@ let is_precise = function
   | Unknown | Well -> false
   | Origin { kind } -> kind <> Leaf
 
+
+module History_Info = struct
+  let name = "Origin.History"
+  let dependencies = []
+  let size = 32
+end
+
+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 register_write bases t =
+  if not (is_unknown t) then
+    let change (w, r, b) = w+1, r, Base.SetLattice.join b bases in
+    ignore (History.memo ~change (fun _ -> 1, 0, bases) t)
+
+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)
+
+
+let get_history () =
+  let list = List.of_seq (History.to_seq ()) in
+  let list = List.filter (fun (_origin, (_, r, _)) -> r > 0) list in
+  let cmp (origin1, (_, r1, _)) (origin2, (_, r2, _)) =
+    let r = r2 - r1 in
+    if r <> 0 then r else compare origin1 origin2
+  in
+  List.sort cmp list
+
+let pretty_origin fmt origin =
+  match origin with
+  | Unknown -> Format.fprintf fmt "Unknown origin"
+  | Well -> Format.fprintf fmt "Initial state"
+  | Origin { kind; loc; } ->
+    let kind =
+      match kind with
+      | Misalign_read -> "misaligned read of addresses"
+      | Leaf -> "interpretation of assigns clause"
+      | Merge -> "imprecise merge of addresses"
+      | Arith -> "arithmetic operation on addresses"
+    in
+    Format.fprintf fmt "%a: %s" Cil_datatype.Location.pretty loc kind
+
+let pretty_history fmt =
+  let list = get_history () in
+  let pp_origin fmt (origin, (w, r, bases)) =
+    let bases = Base.SetLattice.filter (fun b -> not (Base.is_null b)) bases in
+    Format.fprintf fmt
+      "@[<hov 2>%a@ (read %i times, propagated %i times)@ \
+       garbled mix of &%a@]"
+      pretty_origin origin r w Base.SetLattice.pretty bases
+  in
+  if list <> [] then
+    Format.fprintf fmt
+      "@[<v 2>Origins of garbled mix generated during analysis:@,%a@]"
+      (Pretty_utils.pp_list ~sep:"@," pp_origin) list
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."

src/kernel_services/abstract_interp/origin.mli

@@ -52,6 +52,22 @@ val is_included: t -> t -> bool
 
 val is_precise: t -> bool
 
+(** Records the write of an imprecise value of the given bases,
+    with the given origin. *)
+val register_write: Base.SetLattice.t -> t -> unit
+
+(** Records the read of an imprecise value of the given bases,
+    with the given origin. *)
+val register_read: Base.SetLattice.t -> t -> unit
+
+(** Pretty-print a summary of the origins of imprecise values recorded
+    by [register_write] and [register_read] above. *)
+val pretty_history: Format.formatter -> unit
+
+(** Clears the history of origins saved by [register_write] and
+    [register_read] above. *)
+val clear: unit -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."

src/plugins/eva/domains/cvalue/cvalue_queries.ml

@@ -76,6 +76,10 @@ module Queries = struct
   let is_float v =
     Cvalue.V.(is_included v top_float) && Cvalue.V.contains_non_zero v
 
+  let read_garbled_mix = function
+    | Cvalue.V.Top (bases, origin) -> Origin.register_read bases origin
+    | _ -> ()
+
   let extract_scalar_lval state lval typ loc =
     let process_one_loc = eval_one_loc state lval typ in
     let acc = Cvalue.V.bottom, None in
@@ -88,6 +92,7 @@ module Queries = struct
     let incompatible_type = is_float value <> Cil.isFloatingType typ in
     let origin = if incompatible_type then Some value else None in
     let value = Cvalue_forward.reinterpret typ value in
+    read_garbled_mix value;
     if Cvalue.V.is_bottom value
     then `Bottom, alarms
     else `Value (value, origin), alarms
@@ -106,6 +111,7 @@ module Queries = struct
         let value = Cvalue.V_Offsetmap.find_imprecise_everywhere offsm in
         let alarms = indeterminate_alarms lval value in
         let v = Cvalue.V_Or_Uninitialized.get_v value in
+        read_garbled_mix v;
         let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
         v, alarms
 

src/plugins/eva/domains/cvalue/warn.ml

@@ -99,7 +99,8 @@ let warn_imprecise_lval_read lv loc contents =
    [exp_val] is the part of the evaluation of [exp] that is imprecise. *)
 let warn_right_exp_imprecision lv loc_lv exp_val =
   match exp_val with
-  | Location_Bytes.Top(_topparam,origin) ->
+  | Location_Bytes.Top(topparam, origin) ->
+    Origin.register_write topparam origin;
     Self.warning ~wkey:Self.wkey_garbled_mix_write ~once:true ~current:true
       "@[<v>@[Assigning imprecise value to %a%t.@]%a%t@]"
       Printer.pp_lval lv

src/plugins/eva/engine/compute_functions.ml

@@ -102,6 +102,7 @@ let pre_analysis () =
      degeneration states *)
   Eva_utils.DegenerationPoints.clear ();
   Cvalue.V.clear_garbled_mix ();
+  Origin.clear ();
   Eva_utils.clear_call_stack ()
 
 let post_analysis_cleanup ~aborted =

src/plugins/eva/engine/transfer_specification.ml

@@ -311,16 +311,18 @@ module Make
       | Some location ->
         let loc = Precise_locs.imprecise_location (get_ploc location) in
         let cvalue = Cvalue.Model.find cvalue_state loc in
-        if Cvalue.V.is_imprecise cvalue
-        then
-          begin
+        begin
+          match cvalue with
+          | Top (bases, origin) ->
             ignore (Locations.Location_Bytes.track_garbled_mix cvalue);
+            Origin.register_write bases origin;
             Self.warning ~current:true ~once:true
               ~wkey:Self.wkey_garbled_mix_assigns
               "The specification of function %a has generated a garbled mix \
                for %a."
               Kernel_function.pretty kf pp_assign_clause (Assign, assign)
-          end
+          | _ -> ()
+        end
     in
     let check_one_state state =
       let cvalue_state = get_cvalue_or_top state in

src/plugins/eva/utils/eva_utils.ml

@@ -286,6 +286,7 @@ let lval_to_exp =
     (fun lv -> Cil.new_exp ~loc:Cil_datatype.Location.unknown (Lval lv))
 
 let dump_garbled_mix () =
+  Self.warning ~wkey:Self.wkey_garbled_mix_summary "%t" Origin.pretty_history;
   let l = Cvalue.V.get_garbled_mix () in
   if l <> [] then
     let pp_one fmt v = Format.fprintf fmt "@[<hov 2>%a@]" Cvalue.V.pretty v in