From 242f82719d069d2de5eef0361130fb4dd9c288d6 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Tue, 16 Nov 2021 15:38:47 +0100
Subject: [PATCH] [Eva] api: Add evaluation of callee directly from call
statements
---
src/plugins/value/Eva.mli | 22 +++++++++++++++++++---
src/plugins/value/utils/results.ml | 26 +++++++++++++++++++++++---
src/plugins/value/utils/results.mli | 22 +++++++++++++++++++---
3 files changed, 61 insertions(+), 9 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index a61c219bf21..1b42840150a 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -79,7 +79,15 @@ module Results: sig
val eval_address : Cil_types.lval -> request -> address evaluation
- val eval_callee : Cil_types.exp -> request -> Cil_types.kernel_function list result (* Ignores non-function values; exp must come from Cil Call constructor and are restricted to lvalues with no offset *)
+ (* Returns the kernel functions into which the given expression may evaluate.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+ without offset.
+ Also see [callee] for a function which applies directly on Call
+ statements *)
+ val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
(* Value conversion *)
val as_int : value evaluation -> int result
@@ -103,11 +111,19 @@ module Results: sig
val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *)
val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
- (* Callers / callsites *)
+ (* Callers / Callees / Callsites *)
val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
val callsites : Cil_types.kernel_function -> Cil_types.stmt list
val callsites_per_caller : Cil_types.kernel_function ->
- (Cil_types.kernel_function * Cil_types.stmt list) list
+ (Cil_types.kernel_function * Cil_types.stmt list) list
+
+ (* Returns the kernel functions called in the given statement.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+ instruction or a [Local_init] with [ConsInit] initializer. *)
+ val callee : Cil_types.stmt -> Kernel_function.t list
end
module Value_results: sig
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 397e6fce5bb..9a9a4a23e2e 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -376,7 +376,9 @@ struct
let r,_alarms = A.Eval.eval_function_exp exp state in
r >>>-: List.map fst
in
- get req |> Response.map_join' extract join |> convert
+ get req |> Response.map_join' extract join |> convert |>
+ Result.map (List.sort_uniq Kernel_function.compare)
+
(* Conversion *)
@@ -429,7 +431,7 @@ struct
let response_loc, lv = extract_loc res in
let is_const_lv = Value_util.is_const_write_invalid (Cil.typeOfLval lv) in
(* No write effect if [lv] is const *)
- if access=Locations.Write && is_const_lv
+ if access=Locations.Write && is_const_lv
then Result.ok Locations.Zone.bottom
else
match A.Loc.get Main_locations.PLoc.key with
@@ -620,9 +622,27 @@ let eval_address lval req =
end : Lvaluation)
let eval_callee exp req =
+ (* Check the validity of exp *)
+ begin match exp with
+ | Cil_types.({ enode = Lval (_, NoOffset) }) -> ()
+ | _ ->
+ invalid_arg "The callee must be an lvalue with no offset"
+ end;
let module M = Make () in
M.eval_callee exp req
+let callee stmt =
+ let callee_exp =
+ match stmt.Cil_types.skind with
+ | Instr (Call (_lval, callee_exp, _args, _loc)) ->
+ callee_exp
+ | Instr (Local_init (_vi, ConsInit (f, _, _), _loc)) ->
+ Cil.evar f
+ | _ ->
+ invalid_arg "Can only evaluate the callee on a statement which is a Call"
+ in
+ before stmt |> eval_callee callee_exp |> Result.value ~default:[]
+
(* Value conversion *)
let as_cvalue (Value evaluation) =
@@ -733,7 +753,7 @@ let callsites_per_caller kf =
let module Map = Kernel_function.Map in
let f acc = function
| [] | (_,Cil_types.Kglobal) :: _ -> acc
- | (kf,Kstmt stmt) :: _->
+ | (kf,Kstmt stmt) :: _->
Map.update kf (fun old -> Some (stmt :: Option.value ~default:[] old)) acc
in
at_start_of kf |> callstacks |>
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index eecc8c1b6f6..d200cddfd41 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -82,7 +82,15 @@ val eval_exp : Cil_types.exp -> request -> value evaluation
val eval_address : Cil_types.lval -> request -> address evaluation
-val eval_callee : Cil_types.exp -> request -> Cil_types.kernel_function list result (* Ignores non-function values; exp must come from Cil Call constructor and are restricted to lvalues with no offset *)
+(* Returns the kernel functions into which the given expression may evaluate.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the callee expression is not an lvalue
+ without offset.
+ Also see [callee] for a function which applies directly on Call
+ statements *)
+val eval_callee : Cil_types.exp -> request -> Kernel_function.t list result
(* Value conversion *)
val as_int : value evaluation -> int result
@@ -106,9 +114,17 @@ val is_bottom : 'a evaluation -> bool
val is_called : Cil_types.kernel_function -> bool (* called during the analysis, not by the actual program *)
val is_reachable : Cil_types.stmt -> bool (* reachable by the analysis, not by the actual program *)
-(* Callers / callsites *)
+(* Callers / Callees / Callsites *)
val callers : Cil_types.kernel_function -> Cil_types.kernel_function list
val callsites : Cil_types.kernel_function -> Cil_types.stmt list
val callsites_per_caller : Cil_types.kernel_function ->
- (Cil_types.kernel_function * Cil_types.stmt list) list
+ (Cil_types.kernel_function * Cil_types.stmt list) list
+
+(* Returns the kernel functions called in the given statement.
+ If the callee expression doesn't always evaluate to a function, those
+ spurious values are ignored. If it always evaluate to a non-function value
+ then the returned list is empty.
+ Raises [Stdlib.Invalid_argument] if the statement is not a [Call]
+ instruction or a [Local_init] with [ConsInit] initializer. *)
+val callee : Cil_types.stmt -> Kernel_function.t list
[@@@ api_end]
--
GitLab