From 5b9138e2c71fd0697c4998a6b967c44c49f38c59 Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Sat, 18 Sep 2021 14:24:45 +0200
Subject: [PATCH] [Eva] api: Add results folding by callstack
---
src/plugins/value/utils/results.ml | 38 ++++++++++++++++++++++++++---
src/plugins/value/utils/results.mli | 6 ++++-
2 files changed, 40 insertions(+), 4 deletions(-)
diff --git a/src/plugins/value/utils/results.ml b/src/plugins/value/utils/results.ml
index 278822ec43f..3d3beffa9c0 100644
--- a/src/plugins/value/utils/results.ml
+++ b/src/plugins/value/utils/results.ml
@@ -159,8 +159,16 @@ struct
(* Accessors *)
let callstacks : ('a, restricted_to_callstack) t -> callstack list = function
- | ByCallstack l -> List.map fst l
| Top | Bottom -> [] (* What else to do when Top is given ? *)
+ | ByCallstack l -> List.map fst l
+
+ (* Fold *)
+
+ let fold (f : callstack -> 'a -> 'b -> 'b) (acc : 'b) :
+ ('a, restricted_to_callstack) t -> 'b =
+ function
+ | Top | Bottom -> acc (* What else to do when Top is given ? *)
+ | ByCallstack l -> List.fold_left (fun acc (cs,x) -> f cs x acc) acc l
(* Map *)
@@ -255,7 +263,19 @@ struct
| `Value v -> Result.ok v
let callstacks req =
- Response.callstacks (get_by_callstack req)
+ get_by_callstack req |> Response.callstacks
+
+ let fold_callstacks f acc req =
+ let f' cs _res acc =
+ f cs (in_callstack cs req) acc
+ in
+ get_by_callstack req |> Response.fold f' acc
+
+ let by_callstack req =
+ let f cs _res acc =
+ (cs, in_callstack cs req) :: acc
+ in
+ get_by_callstack req |> Response.fold f []
let is_reachable req =
match get req with
@@ -428,12 +448,23 @@ struct
end
-(* State requests *)
+(* Working with callstacks *)
let callstacks req =
let module E = Make () in
E.callstacks req
+let fold_callstacks f acc req =
+ let module E = Make () in
+ E.fold_callstacks f acc req
+
+let by_callstack req =
+ let module E = Make () in
+ E.by_callstack req
+
+
+(* State requests *)
+
let equality_class exp req =
let module E = Make () in
E.equality_class exp req
@@ -442,6 +473,7 @@ let as_cvalue_model req =
let module E = Make () in
E.as_cvalue_model req
+
(* Evaluation *)
module type Evaluator =
diff --git a/src/plugins/value/utils/results.mli b/src/plugins/value/utils/results.mli
index f3444b2c722..0e0a0c69391 100644
--- a/src/plugins/value/utils/results.mli
+++ b/src/plugins/value/utils/results.mli
@@ -53,8 +53,12 @@ val in_callstack : callstack -> request -> request
val in_callstacks : callstack list -> request -> request
val filter_callstack : (callstack -> bool) -> request -> request
-(* State requests *)
+(* Working with callstacks *)
val callstacks : request -> callstack list
+val fold_callstacks : (callstack -> request -> 'a -> 'a) -> 'a -> request -> 'a
+val by_callstack : request -> (callstack * request) list
+
+(* State requests *)
val equality_class : Cil_types.exp -> request -> Cil_types.exp list result
val as_cvalue_model : request -> Cvalue.Model.t result
--
GitLab