From dcc4f9515bc0fab157fd8b9b6aa440465cbb0dae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 21 Sep 2023 16:10:28 +0200
Subject: [PATCH] [Eva] Keeps an history of garbled mix origins.
---
src/kernel_services/abstract_interp/origin.ml | 67 ++++++++++++++++++-
.../abstract_interp/origin.mli | 16 +++++
.../eva/domains/cvalue/cvalue_queries.ml | 6 ++
src/plugins/eva/domains/cvalue/warn.ml | 3 +-
src/plugins/eva/engine/compute_functions.ml | 1 +
.../eva/engine/transfer_specification.ml | 10 +--
src/plugins/eva/utils/eva_utils.ml | 1 +
7 files changed, 98 insertions(+), 6 deletions(-)
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 2b743f0d854..0e198d4b9c2 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/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 ../../.."
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index a739d8dca4c..cfc870300db 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/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 ../../.."
diff --git a/src/plugins/eva/domains/cvalue/cvalue_queries.ml b/src/plugins/eva/domains/cvalue/cvalue_queries.ml
index ae31230b0e8..a39492a4594 100644
--- a/src/plugins/eva/domains/cvalue/cvalue_queries.ml
+++ b/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
diff --git a/src/plugins/eva/domains/cvalue/warn.ml b/src/plugins/eva/domains/cvalue/warn.ml
index 402f79f5702..81c8eede4b2 100644
--- a/src/plugins/eva/domains/cvalue/warn.ml
+++ b/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
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 09a3b4d353b..5904de59dc6 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/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 =
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index bd0b649c6bd..32174a32d2e 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/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
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 73d1517b788..3f1b88be0bf 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/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
--
GitLab