From 299af05bce73c4a4ba0e0dfc700eb979825c2c79 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Mon, 20 Sep 2021 17:33:59 +0200
Subject: [PATCH] [Eva] api: Functions evaluations must now be done in one step
---
src/plugins/value/Eva.mli | 8 ++++-
src/plugins/value/utils/results.ml | 56 ++++++++++++++++-------------
src/plugins/value/utils/results.mli | 8 ++++-
3 files changed, 46 insertions(+), 26 deletions(-)
diff --git a/src/plugins/value/Eva.mli b/src/plugins/value/Eva.mli
index 71b28373ba5..0fc464a048d 100644
--- a/src/plugins/value/Eva.mli
+++ b/src/plugins/value/Eva.mli
@@ -41,6 +41,11 @@ module Results: sig
type error = Bottom | Top | DisabledDomain
type 'a result = ('a,error) Result.t
+ val string_of_error : error -> string
+ val pretty_error : Format.formatter -> error -> unit
+ val pretty_result : (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a result -> unit
+
(* Control point selection *)
val at_start : request
val at_end : request
@@ -72,11 +77,12 @@ module Results: sig
val eval_address : Cil_types.lval -> request -> lvaluation
+ 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 *)
+
(* Value conversion *)
val as_int : evaluation -> int result
val as_integer : evaluation -> Integer.t result
val as_float : evaluation -> float result
- val as_functions : evaluation -> Cil_types.kernel_function list result (* Ignores non-function values *)
val as_ival : evaluation -> Ival.t result
val as_fval : evaluation -> Fval.t result
val as_cvalue : evaluation -> Cvalue.V.t result
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 7871300ab7a..48189f931d4 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -20,12 +20,14 @@
(* *)
(**************************************************************************)
+open Bottom.Type
+
type 'a or_top_bottom = 'a Bottom.Top.or_top_bottom
-let (>>>-) t f = match t with
+let (>>>-:) t f = match t with
| `Top -> `Top
| `Bottom -> `Bottom
- | `Value t -> f t
+ | `Value t -> `Value (f t)
module Callstack = Value_types.Callstack
@@ -49,6 +51,17 @@ type request = {
type error = Bottom | Top | DisabledDomain
type 'a result = ('a,error) Result.t
+let string_of_error = function
+ | Bottom -> "The computed state is bottom"
+ | Top -> "The computed state is Top"
+ | DisabledDomain -> "The required domain is disabled"
+
+let pretty_error fmt error =
+ Format.pp_print_string fmt (string_of_error error)
+let pretty_result f fmt r =
+ Result.fold ~ok:(f fmt) ~error:(pretty_error fmt) r
+
+
(* Building requests *)
let make control_point = {
@@ -338,9 +351,15 @@ struct
let eval state = A.Eval.lvaluate ~for_writing:false state lval in
Response.map eval (get req)
- (* Conversion *)
+ let eval_callee exp req =
+ let join = (@)
+ and extract state =
+ let r,_alarms = A.Eval.eval_function_exp exp state in
+ r >>>-: List.map fst
+ in
+ get req |> Response.map_join' extract join |> convert
- open Bottom.Type
+ (* Conversion *)
let extract_value : type c. c evaluation -> (value or_bottom, c) Response.t =
function
@@ -359,19 +378,10 @@ struct
| Some get ->
let join = Main_values.CVal.join in
let extract value =
- (value >>-: get :> 'a or_top_bottom)
+ value >>>-: get
in
extract_value res |> Response.map_join' extract join |> convert
- let as_functions : type c. c evaluation ->
- Cil_types.kernel_function list result =
- fun res ->
- let join = (@)
- and extract value =
- value >>>- fun v -> (fst (A.Val.resolve_functions v) :> 'a or_top_bottom)
- in
- extract_value res |> Response.map_join' extract join |> convert
-
let extract_loc : type c. c lvaluation -> (location or_bottom, c) Response.t =
fun r ->
let extract (x, _alarms) = x >>-: (fun (_valuation,loc,_typ) -> loc) in
@@ -390,7 +400,7 @@ struct
assert (Int_Base.equal loc2.size size);
make_loc loc size
and extract loc =
- (loc >>-: get >>-: Precise_locs.imprecise_location :> 'a or_top_bottom)
+ loc >>>-: get >>>-: Precise_locs.imprecise_location
in
extract_loc res |> Response.map_join' extract join |> convert
@@ -402,7 +412,7 @@ struct
| Some get ->
let join = Locations.Zone.join
and extract loc =
- (loc >>-: get >>-: Precise_locs.enumerate_valid_bits Read :> 'a or_top_bottom)
+ loc >>>-: get >>>-: Precise_locs.enumerate_valid_bits Read
in
extract_loc res |> Response.map_join' extract join |> convert
@@ -411,7 +421,7 @@ struct
| `LValue r ->
let join = (&&)
and extract (x, _alarms) =
- (x >>-: (fun (_valuation,fv) -> fv.Eval.initialized) :> 'a or_top_bottom)
+ x >>>-: (fun (_valuation,fv) -> fv.Eval.initialized)
in
begin match Response.map_join' extract join r with
| `Bottom | `Top -> false
@@ -442,7 +452,7 @@ struct
let is_bottom : type c. c evaluation -> bool =
fun res ->
- let extract (x,_) = (x >>-: fun _ -> () :> unit or_top_bottom) in
+ let extract (x,_) = x >>>-: fun _ -> () in
let join () () = () in
let r = match res with
| `LValue r ->
@@ -490,8 +500,6 @@ sig
type 'a evaluation
type restriction
val as_cvalue : 'callstack evaluation -> Main_values.CVal.t result
- val as_functions : 'callstack evaluation ->
- Cil_types.kernel_function list result
val as_location : 'callstack lvaluation -> Locations.location result
val as_zone : 'callstack lvaluation -> Locations.Zone.t result
val is_initialized : 'callstack evaluation -> bool
@@ -561,6 +569,10 @@ let eval_address lval req =
let v = lval
end : Lvaluation)
+let eval_callee exp req =
+ let module M = Make () in
+ M.eval_callee exp req
+
(* Value conversion *)
let as_cvalue evaluation =
@@ -589,10 +601,6 @@ let as_float evaluation =
with Fval.Not_Singleton_Float ->
Result.error Top
-let as_functions evaluation =
- let module E = (val evaluation : Evaluation) in
- E.as_functions E.v
-
let as_integer evaluation =
try
Result.map Ival.project_int (as_ival evaluation)
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index 870feaea2b9..17fb9dda5a7 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -39,6 +39,11 @@ type lvaluation
type error = Bottom | Top | DisabledDomain
type 'a result = ('a,error) Result.t
+val string_of_error : error -> string
+val pretty_error : Format.formatter -> error -> unit
+val pretty_result : (Format.formatter -> 'a -> unit) ->
+ Format.formatter -> 'a result -> unit
+
(* Control point selection *)
val at_start : request
val at_end : request
@@ -70,11 +75,12 @@ val eval_exp : Cil_types.exp -> request -> evaluation
val eval_address : Cil_types.lval -> request -> lvaluation
+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 *)
+
(* Value conversion *)
val as_int : evaluation -> int result
val as_integer : evaluation -> Integer.t result
val as_float : evaluation -> float result
-val as_functions : evaluation -> Cil_types.kernel_function list result (* Ignores non-function values *)
val as_ival : evaluation -> Ival.t result
val as_fval : evaluation -> Fval.t result
val as_cvalue : evaluation -> Cvalue.V.t result
--
GitLab