From 2b1a9d7aeac87ed7bc11113939c91128ad3c5db2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 11 Feb 2022 12:03:57 +0100
Subject: [PATCH] [Eva] Results: as_zone converts error cases into bottom or
top zone accordingly.
Adds function [as_zone_result] that returns a zone result, without converting
error cases.
---
src/plugins/dive/build.ml | 3 +--
src/plugins/inout/outputs.ml | 2 +-
src/plugins/occurrence/register.ml | 26 ++++++++++++--------------
src/plugins/scope/datascope.ml | 4 +---
src/plugins/scope/defs.ml | 6 ++----
src/plugins/slicing/slicingCmds.ml | 1 -
src/plugins/studia/studia_request.ml | 4 +---
src/plugins/studia/writes.ml | 2 +-
src/plugins/value/Eva.mli | 8 ++++++--
src/plugins/value/utils/results.ml | 8 +++++++-
src/plugins/value/utils/results.mli | 8 ++++++--
11 files changed, 38 insertions(+), 34 deletions(-)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index c17ab76acb1..af26fe2d1f8 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -90,8 +90,7 @@ struct
Result.value ~default:Locations.loc_bottom
let to_zone kinstr lval =
- before_kinstr kinstr |> eval_address lval |> as_zone |>
- Result.value ~default:Locations.Zone.bottom
+ before_kinstr kinstr |> eval_address lval |> as_zone
let to_callstacks stmt =
before stmt |> callstacks
diff --git a/src/plugins/inout/outputs.ml b/src/plugins/inout/outputs.ml
index f7bec37f39e..5976c3b6f0f 100644
--- a/src/plugins/inout/outputs.ml
+++ b/src/plugins/inout/outputs.ml
@@ -52,7 +52,7 @@ class virtual do_it_ = object(self)
let bits_loc = Eva.Results.(
before_kinstr self#current_kinstr |> eval_address lv |>
as_zone ~access) in
- Result.iter self#join bits_loc
+ self#join bits_loc
method! vinst i =
if Db.Value.is_reachable (Db.Value.noassert_get_state self#current_kinstr)
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index cbf6feb7084..5e6922a3562 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -107,20 +107,18 @@ class occurrence = object (self)
method! vlval lv =
let ki = self#current_kinstr in
begin
- match Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) with
- | Result.Error _ -> (* ignore *) ()
- | Ok z ->
- try
- Locations.Zone.fold_topset_ok
- (fun b _ () ->
- match b with
- | Base.Var (vi, _) | Base.Allocated (vi, _, _) ->
- Occurrences.add vi self#current_kf ki lv
- | _ -> ()
- ) z ()
- with Abstract_interp.Error_Top ->
- error ~current:true "Found completely imprecise value (%a). Ignoring@."
- Printer.pp_lval lv
+ let z = Eva.Results.(before_kinstr ki |> eval_address lv |> as_zone) in
+ try
+ Locations.Zone.fold_topset_ok
+ (fun b _ () ->
+ match b with
+ | Base.Var (vi, _) | Base.Allocated (vi, _, _) ->
+ Occurrences.add vi self#current_kf ki lv
+ | _ -> ()
+ ) z ()
+ with Abstract_interp.Error_Top ->
+ error ~current:true "Found completely imprecise value (%a). Ignoring@."
+ Printer.pp_lval lv
end;
DoChildren
diff --git a/src/plugins/scope/datascope.ml b/src/plugins/scope/datascope.ml
index b3782a1a193..6bc2734636b 100644
--- a/src/plugins/scope/datascope.ml
+++ b/src/plugins/scope/datascope.ml
@@ -81,9 +81,7 @@ module InitSid = struct
end
let get_writes stmt lval =
- Eva.Results.(
- before stmt |> eval_address lval |> as_zone ~access:Write |>
- default Locations.Zone.bottom)
+ Eva.Results.(before stmt |> eval_address lval |> as_zone ~access:Write)
(** Add to [stmt] to [lmap] for all the locations modified by the statement.
* Something to do only for calls and assignments.
diff --git a/src/plugins/scope/defs.ml b/src/plugins/scope/defs.ml
index 0aede3dd05e..af1e23d7838 100644
--- a/src/plugins/scope/defs.ml
+++ b/src/plugins/scope/defs.ml
@@ -168,8 +168,7 @@ let compute kf stmt lval =
in
Eva.Analysis.compute ();
let zone = Eva.Results.(before stmt |> eval_address lval |> as_zone) in
- Option.bind (Result.to_option zone) (compute_aux kf stmt) |>
- Option.map extract
+ compute_aux kf stmt zone |> Option.map extract
(* Variation of the function above. For each PDG node that has been found,
we find whether it directly modifies [zone] through an affectation
@@ -220,8 +219,7 @@ let compute_with_def_type_zone kf stmt zone =
let compute_with_def_type kf stmt lval =
Eva.Analysis.compute ();
let zone =
- Eva.Results.(before stmt |> eval_address lval |> as_zone) |>
- Result.value ~default:Locations.Zone.bottom
+ Eva.Results.(before stmt |> eval_address lval |> as_zone)
in
compute_with_def_type_zone kf stmt zone
diff --git a/src/plugins/slicing/slicingCmds.ml b/src/plugins/slicing/slicingCmds.ml
index cdfb8be1be9..8340d52e18c 100644
--- a/src/plugins/slicing/slicingCmds.ml
+++ b/src/plugins/slicing/slicingCmds.ml
@@ -58,7 +58,6 @@ let get_select_kf (fvar, _select) = Globals.Functions.get fvar
let get_lval_zone ?(access=Locations.Read) stmt lval =
let open Eva.Results in
before stmt |> eval_address lval |> as_zone ~access
- |> default Locations.Zone.bottom
(** Utilities for [kinstr]. *)
module Kinstr: sig
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
index f1a94a67bd2..2e44a1b8e8f 100644
--- a/src/plugins/studia/studia_request.ml
+++ b/src/plugins/studia/studia_request.ml
@@ -82,9 +82,7 @@ let compute kind zone =
List.fold_left add empty stmts
let lval_location kinstr lval =
- Eva.Results.(
- before_kinstr kinstr |> eval_address lval |> as_zone |>
- default Locations.Zone.bottom)
+ Eva.Results.(before_kinstr kinstr |> eval_address lval |> as_zone)
let () = Request.register ~package
~kind:`GET ~name:"getReadsLval"
diff --git a/src/plugins/studia/writes.ml b/src/plugins/studia/writes.ml
index d323327d03b..dbcbcfc04ce 100644
--- a/src/plugins/studia/writes.ml
+++ b/src/plugins/studia/writes.ml
@@ -66,7 +66,7 @@ class find_write zlval = object (self)
let direct_write = match lvopt with
| None -> false
| Some lv ->
- Eva.Results.(before stmt |> eval_address lv |> as_zone) |>
+ Eva.Results.(before stmt |> eval_address lv |> as_zone_result) |>
Result.fold ~ok:(Zone.intersects zlval) ~error:(fun _ -> false)
in
let effects =
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 75e6e742e82..d6281ebcd41 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -203,8 +203,12 @@ module Results: sig
(** Converts into a C location abstraction. *)
val as_location : address evaluation -> Locations.location result
- (** Converts into a Zone. *)
- val as_zone : ?access:Locations.access -> address evaluation ->
+ (** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+ val as_zone: ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t
+ (** Converts into a Zone result. *)
+ val as_zone_result : ?access:Locations.access -> address evaluation ->
Locations.Zone.t result
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index ea5c066bf7a..3bcf3b4da4d 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -695,10 +695,16 @@ let as_location (Address lvaluation) =
let module E = (val lvaluation : Lvaluation) in
E.as_location E.v
-let as_zone ?(access=Locations.Read) (Address lvaluation) =
+let as_zone_result ?(access=Locations.Read) (Address lvaluation) =
let module E = (val lvaluation : Lvaluation) in
E.as_zone ~access E.v
+let as_zone ?access address =
+ match as_zone_result ?access address with
+ | Ok zone -> zone
+ | Error Bottom -> Locations.Zone.bottom
+ | Error (Top | DisabledDomain) -> Locations.Zone.top
+
(* Evaluation properties *)
let is_initialized (Value evaluation) =
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 74e9b67936b..b3580445ded 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -191,8 +191,12 @@ val as_cvalue : value evaluation -> Cvalue.V.t result
(** Converts into a C location abstraction. *)
val as_location : address evaluation -> Locations.location result
-(** Converts into a Zone. *)
-val as_zone : ?access:Locations.access -> address evaluation ->
+(** Converts into a Zone. Error cases are converted into bottom or top zones
+ accordingly. *)
+val as_zone: ?access:Locations.access -> address evaluation ->
+ Locations.Zone.t
+(** Converts into a Zone result. *)
+val as_zone_result : ?access:Locations.access -> address evaluation ->
Locations.Zone.t result
--
GitLab