From e8a4fa9bf14c8655f98b06d430b9138d844af8ce Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 8 Jul 2022 18:05:15 +0200
Subject: [PATCH] [Eva] Results: adds a request to allows evaluations in a
given cvalue state.
During the Eva analysis, the Inout and From plugins uses callbacks that gives
access to the computed cvalue states, and they need to evaluate some expressions
in these states.
---
src/plugins/eva/Eva.mli | 4 ++
src/plugins/eva/utils/results.ml | 97 ++++++++++++++++++++-----------
src/plugins/eva/utils/results.mli | 4 ++
3 files changed, 70 insertions(+), 35 deletions(-)
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 6dadf905432..cc3ec581d05 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -212,6 +212,10 @@ module Results: sig
(** Just before a statement or at the start of the analysis. *)
val before_kinstr : Cil_types.kinstr -> request
+ (** Evaluation in a given cvalue state.
+ Callstacks selection are silently ignored on such requests. *)
+ val in_cvalue_state: Cvalue.Model.t -> request
+
(** Callstack selection *)
diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml
index 3ff75868921..c7b44e783a1 100644
--- a/src/plugins/eva/utils/results.ml
+++ b/src/plugins/eva/utils/results.ml
@@ -39,12 +39,16 @@ type control_point =
| Before of Cil_types.stmt
| After of Cil_types.stmt
-type request = {
+type context = {
control_point : control_point;
selector : callstack list option;
filter: (callstack -> bool) list;
}
+type request =
+ | Point of context
+ | Cvalue of Cvalue.Model.t
+
type error = Bottom | Top | DisabledDomain
type 'a result = ('a,error) Result.t
@@ -61,11 +65,8 @@ let pretty_result f fmt r =
(* Building requests *)
-let make control_point = {
- control_point;
- selector = None;
- filter = [];
-}
+let make control_point =
+ Point { control_point; selector = None; filter = []; }
let before stmt = make (Before stmt)
let after stmt = make (After stmt)
@@ -78,9 +79,20 @@ let before_kinstr = function
| Cil_types.Kglobal -> at_start
| Kstmt stmt -> before stmt
-let in_callstacks l req = { req with selector = Some l }
-let in_callstack cs req = { req with selector = Some [cs] }
-let filter_callstack f req = { req with filter = f :: req.filter }
+let change_context f = function
+ | Point ctx -> Point (f ctx)
+ | Cvalue _ as x -> x
+
+let in_callstacks l =
+ change_context (fun ctx -> { ctx with selector = Some l })
+
+let in_callstack cs =
+ change_context (fun ctx -> { ctx with selector = Some [cs] })
+
+let filter_callstack f =
+ change_context (fun ctx -> { ctx with filter = f :: ctx.filter })
+
+let in_cvalue_state cvalue = Cvalue cvalue
(* Manipulating request results *)
@@ -120,7 +132,7 @@ struct
| `Top -> Top
| `Value state -> ByCallstack [cs,state]
- let by_callstack : request ->
+ let by_callstack : context ->
[< `Bottom | `Top | `Value of 'a Value_types.Callstack.Hashtbl.t ] ->
('a, restricted_to_callstack) t =
fun req -> function
@@ -212,49 +224,64 @@ struct
| Address: (EvalTypes.loc, 'c) Response.t * Locations.access ->
(address,'c) evaluation
- let get_by_callstack (req : request) :
+ let get_from_cvalue cvalue =
+ if Cvalue.Model.(equal cvalue bottom)
+ then `Bottom
+ else if Cvalue.Model.(equal cvalue top)
+ then `Top
+ else
+ let state = cvalue, Locals_scoping.bottom () in
+ `Value (A.Dom.set Cvalue_domain.State.key state A.Dom.top)
+
+ let get_by_callstack (ctx : context) :
(_, restricted_to_callstack) Response.t =
let open Response in
- let selection = req.selector in
- match req.control_point with
+ let selection = ctx.selector in
+ match ctx.control_point with
| Before stmt ->
A.get_stmt_state_by_callstack ?selection ~after:false stmt
- |> by_callstack req
+ |> by_callstack ctx
| After stmt ->
A.get_stmt_state_by_callstack ?selection ~after:true stmt
- |> by_callstack req
+ |> by_callstack ctx
| Initial ->
A.get_global_state () |> singleton []
| Start kf ->
- A.get_initial_state_by_callstack ?selection kf |> by_callstack req
+ A.get_initial_state_by_callstack ?selection kf |> by_callstack ctx
let get (req : request) : (_, unrestricted_response) Response.t =
- if req.filter <> [] || Option.is_some req.selector then
- Response.coercion @@ get_by_callstack req
- else
- let open Response in
- let state =
- match req.control_point with
- | Before stmt -> A.get_stmt_state ~after:false stmt
- | After stmt -> A.get_stmt_state ~after:true stmt
- | Start kf -> A.get_initial_state kf
- | Initial -> A.get_global_state ()
- in
- consolidated ~top:A.Dom.top state
+ let open Response in
+ match req with
+ | Cvalue state -> consolidated ~top:A.Dom.top (get_from_cvalue state)
+ | Point req ->
+ if req.filter <> [] || Option.is_some req.selector then
+ Response.coercion @@ get_by_callstack req
+ else
+ let state =
+ match req.control_point with
+ | Before stmt -> A.get_stmt_state ~after:false stmt
+ | After stmt -> A.get_stmt_state ~after:true stmt
+ | Start kf -> A.get_initial_state kf
+ | Initial -> A.get_global_state ()
+ in
+ consolidated ~top:A.Dom.top state
let convert : 'a or_top_bottom -> 'a result = function
| `Top -> Result.error Top
| `Bottom -> Result.error Bottom
| `Value v -> Result.ok v
- let callstacks req =
- get_by_callstack req |> Response.callstacks
+ let callstacks = function
+ | Point ctx -> get_by_callstack ctx |> Response.callstacks
+ | Cvalue _ -> []
- let by_callstack req =
- let f cs _res acc =
- (cs, in_callstack cs req) :: acc
- in
- get_by_callstack req |> Response.fold f []
+ let by_callstack = function
+ | Cvalue _ -> assert false
+ | Point ctx as req ->
+ let f cs _res acc =
+ (cs, in_callstack cs req) :: acc
+ in
+ get_by_callstack ctx |> Response.fold f []
let is_reachable req =
match get req with
diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli
index a28f266db67..68a6d04badc 100644
--- a/src/plugins/eva/utils/results.mli
+++ b/src/plugins/eva/utils/results.mli
@@ -117,6 +117,10 @@ val after : Cil_types.stmt -> request
(** Just before a statement or at the start of the analysis. *)
val before_kinstr : Cil_types.kinstr -> request
+(** Evaluation in a given cvalue state.
+ Callstacks selection are silently ignored on such requests. *)
+val in_cvalue_state: Cvalue.Model.t -> request
+
(** Callstack selection *)
--
GitLab