From ae7a94b1a731abed50cf44c0b4e083bc5ced82ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 15 Feb 2024 20:01:04 +0100
Subject: [PATCH] [Eva] Removes previous mechanism to track garbled mix.
---
.../abstract_interp/locations.ml | 62 +++----------------
.../abstract_interp/locations.mli | 11 ----
src/kernel_services/abstract_interp/origin.ml | 7 ---
.../abstract_interp/origin.mli | 2 -
src/plugins/eva/engine/compute_functions.ml | 7 +--
.../eva/engine/transfer_specification.ml | 3 -
src/plugins/eva/engine/transfer_stmt.ml | 9 +--
src/plugins/eva/utils/eva_utils.ml | 11 ----
src/plugins/eva/utils/eva_utils.mli | 3 -
9 files changed, 10 insertions(+), 105 deletions(-)
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index a30181b5f0a..4e951a71e40 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -190,53 +190,9 @@ module Location_Bytes = struct
in
M.fold aux_base m (Some Int.zero)
- (* These two states contain the garbled mix that we track. The list preserves
- the creation order (except it is reversed), while the set is used to test
- inclusion efficiently so far. Only "original" garbled mix are tracked,
- i.e. operations that _transform a garbled mix are not tracked. *)
- module ListGarbledMix = State_builder.List_ref(MapSetLattice)
- (struct
- let name = "Locations.ListGarbledMix"
- let dependencies = [M.self]
- end)
- module SetGarbledMix = State_builder.Set_ref(MapSetLattice.Set)
- (struct
- let name = "Locations.SetGarbledMix"
- let dependencies = [M.self]
- end)
-
- let get_garbled_mix () = List.rev (ListGarbledMix.get ())
- let clear_garbled_mix () =
- ListGarbledMix.clear ();
- SetGarbledMix.clear ();
- ;;
-
- (* We skip imprecise origins: origins that have no location information,
- and leaf origins, because we may create tons of those, that get reduced
- to precise values by the specifications of the function. *)
- let is_gm_to_log = function
- | Top (_, origin) -> Origin.is_precise origin
- | Map _ -> false
-
- let ref_track_garbled_mix = ref true
- let do_track_garbled_mix b = ref_track_garbled_mix := b
-
- (* track a garbled mix if needed, then return it (more convenient for the
- caller). *)
- let track_garbled_mix gm =
- if !ref_track_garbled_mix && is_gm_to_log gm && not (SetGarbledMix.mem gm)
- then begin
- SetGarbledMix.set (MapSetLattice.Set.add gm (SetGarbledMix.get ()));
- ListGarbledMix.set (gm :: ListGarbledMix.get ());
- end;
- gm
-
- let top_with_origin origin =
- track_garbled_mix (Top(Base.SetLattice.top, origin))
-
- (* This internal function builds a garbled mix, but does *not* track its
- creation. This is useful for functions that transform existing GMs. *)
- let inject_top_origin_internal o b =
+ let top_with_origin origin = Top (Base.SetLattice.top, origin)
+
+ let inject_top_origin o b =
if Base.Hptset.(equal b empty || equal b Base.null_set) then
top_int
else begin
@@ -246,15 +202,12 @@ module Location_Bytes = struct
Top (Base.(SetLattice.inject (Hptset.add null b)), o)
end
- let inject_top_origin o b =
- track_garbled_mix (inject_top_origin_internal o b)
-
(** some functions can reduce a garbled mix, make sure to normalize
the result when only NULL remains *)
let normalize_top m =
match m with
| Top (Base.SetLattice.Top, _) | Map _ -> m
- | Top (Base.SetLattice.Set s, o) -> inject_top_origin_internal o s
+ | Top (Base.SetLattice.Set s, o) -> inject_top_origin o s
let narrow m1 m2 = normalize_top (narrow m1 m2)
let meet m1 m2 = normalize_top (meet m1 m2)
@@ -269,8 +222,7 @@ module Location_Bytes = struct
else
match get_keys v with
| Base.SetLattice.Top -> top_with_origin o
- | Base.SetLattice.Set b ->
- track_garbled_mix (inject_top_origin_internal o b)
+ | Base.SetLattice.Set b -> inject_top_origin o b
let topify_with_origin_kind ok v =
let o = Origin.current ok in
@@ -327,7 +279,7 @@ module Location_Bytes = struct
if Base.Hptset.equal garble nonlocals then
false, v
else
- true, inject_top_origin_internal orig nonlocals
+ true, inject_top_origin orig nonlocals
| Map m ->
let nonlocals = M.filter non_local m in
if M.equal nonlocals m then
@@ -366,7 +318,7 @@ module Location_Bytes = struct
match v with
| Top (Base.SetLattice.Top, _) -> false, v
| Top (Base.SetLattice.Set set, origin) ->
- substitute Base.Hptset.replace (inject_top_origin_internal origin) set
+ substitute Base.Hptset.replace (inject_top_origin origin) set
| Map map ->
let decide _key = Ival.join in
substitute (M.replace_key ~decide) (fun m -> Map m) map
diff --git a/src/kernel_services/abstract_interp/locations.mli b/src/kernel_services/abstract_interp/locations.mli
index fe99c8a4a38..c00226fda5c 100644
--- a/src/kernel_services/abstract_interp/locations.mli
+++ b/src/kernel_services/abstract_interp/locations.mli
@@ -216,17 +216,6 @@ module Location_Bytes : sig
val may_reach : Base.t -> t -> bool
(** [may_reach base loc] is true if [base] might be accessed from [loc]. *)
-
- val get_garbled_mix: unit -> t list
- (** All the garbled mix that have been created so far, sorted by "temporal"
- order of emission. *)
-
- val clear_garbled_mix: unit -> unit
- (** Clear the information on created garbled mix. *)
-
- val do_track_garbled_mix: bool -> unit
- val track_garbled_mix: t -> t
-
(**/**)
val pretty_debug: t Pretty_utils.formatter
val clear_caches: unit -> unit
diff --git a/src/kernel_services/abstract_interp/origin.ml b/src/kernel_services/abstract_interp/origin.ml
index 0e198d4b9c2..fb933d6a9ec 100644
--- a/src/kernel_services/abstract_interp/origin.ml
+++ b/src/kernel_services/abstract_interp/origin.ml
@@ -107,13 +107,6 @@ 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. *)
-let is_precise = function
- | Unknown | Well -> false
- | Origin { kind } -> kind <> Leaf
-
module History_Info = struct
let name = "Origin.History"
diff --git a/src/kernel_services/abstract_interp/origin.mli b/src/kernel_services/abstract_interp/origin.mli
index cfc870300db..8aa75691e37 100644
--- a/src/kernel_services/abstract_interp/origin.mli
+++ b/src/kernel_services/abstract_interp/origin.mli
@@ -50,8 +50,6 @@ val pretty_as_reason: Format.formatter -> t -> unit
val join: t -> t -> t
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
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 5904de59dc6..88b6280b2e7 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -101,7 +101,6 @@ let pre_analysis () =
(* We may be resuming Value from a previously crashed analysis. Clear
degeneration states *)
Eva_utils.DegenerationPoints.clear ();
- Cvalue.V.clear_garbled_mix ();
Origin.clear ();
Eva_utils.clear_call_stack ()
@@ -115,7 +114,7 @@ let post_analysis () =
(* Garbled mix must be dumped here -- at least before the call to
mark_green_and_red -- because fresh ones are created when re-evaluating
all the alarms, and we get an unpleasant "ghost effect". *)
- Eva_utils.dump_garbled_mix ();
+ Self.warning ~wkey:Self.wkey_garbled_mix_summary "%t" Origin.pretty_history;
(* Mark unreachable and RTE statuses. Only do this there, not when the
analysis was aborted (hence, not in post_cleanup), because the
propagation is incomplete. Also do not mark unreachable statutes if
@@ -304,13 +303,9 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
Self.feedback ~current:true "Call to builtin %s%s"
name (if kf_name = name then "" else " for function " ^ kf_name);
apply_call_hooks call state `Builtin;
- (* Do not track garbled mixes created when interpreting the specification,
- as the result of the cvalue builtin will overwrite them. *)
- Locations.Location_Bytes.do_track_garbled_mix false;
let states =
Spec.compute_using_specification ~warn:false kinstr call spec state
in
- Locations.Location_Bytes.do_track_garbled_mix true;
let final_state = join_states states in
match final_state with
| `Bottom ->
diff --git a/src/plugins/eva/engine/transfer_specification.ml b/src/plugins/eva/engine/transfer_specification.ml
index 32174a32d2e..8f9c92b08ec 100644
--- a/src/plugins/eva/engine/transfer_specification.ml
+++ b/src/plugins/eva/engine/transfer_specification.ml
@@ -314,7 +314,6 @@ module Make
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
@@ -337,7 +336,6 @@ module Make
and [status] the status of the behaviors. *)
let compute_effects ~warn kf spec result behaviors status states =
States.join states >>- fun pre_state ->
- Locations.Location_Bytes.do_track_garbled_mix false;
let behavior = List.hd behaviors in
let retres_loc = Option.map Location.eval_varinfo result in
let assigns = get_assigns_for_behavior spec behavior in
@@ -355,7 +353,6 @@ module Make
(* Warn on garbled mixes created by specifications, except on builtins. *)
if warn
then check_post_assigns kf retres_loc spec behavior ~pre:pre_state states;
- Locations.Location_Bytes.do_track_garbled_mix true;
states
(* Reduces the [states] by the assumes and requires clauses of the [behavior]
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 13a12c2e300..1bb0994dc6e 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -189,13 +189,8 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
(* Assignment by copying the value of a right lvalue. *)
let assign_by_copy ~subdivnb state valuation lval lloc ltyp =
- (* This code about garbled mix is specific to the Cvalue domain.
- Unfortunately, the current API for abstract_domain does not permit
- distinguishing between an evaluation or a copy. *)
- Locations.Location_Bytes.do_track_garbled_mix false;
- let r = copy_lvalue_and_check ~valuation ~subdivnb state lval in
- Locations.Location_Bytes.do_track_garbled_mix true;
- r >>=: fun (valuation, value) ->
+ copy_lvalue_and_check ~valuation ~subdivnb state lval
+ >>=: fun (valuation, value) ->
Copy ({lval; lloc; ltyp}, value), valuation
(* For an initialization, use for_writing:false for the evaluation of
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 3f1b88be0bf..e1a9d043fec 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -285,17 +285,6 @@ let lval_to_exp =
MemoLvalToExp.memo
(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
- Self.warning ~wkey:Self.wkey_garbled_mix_summary
- "Garbled mix generated during analysis:@.\
- @[<v>%a@]"
- (Pretty_utils.pp_list ~pre:"" ~suf:"" ~sep:"@ " pp_one) l
-
-
type deps = Function_Froms.Deps.deps = {
data: Locations.Zone.t;
indirect: Locations.Zone.t;
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index 2e3ab131c5c..b7c7a84512a 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -112,9 +112,6 @@ val is_value_zero: exp -> bool
val lval_to_exp: lval -> exp
(** This function is memoized to avoid creating too many expressions *)
-val dump_garbled_mix: unit -> unit
-(** print information on the garbled mix created during evaluation *)
-
(** Dependences of expressions and lvalues. *)
--
GitLab