From c2fed1b99f605958f1e5b9c11bad4b5bffe19efa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 4 Dec 2020 13:46:36 +0100
Subject: [PATCH] [eva/server] merging callstacks
---
src/plugins/value/api/values_request.ml | 83 +++++++++++++++++++------
1 file changed, 64 insertions(+), 19 deletions(-)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 25c4f4626a2..39960918fbe 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -39,13 +39,9 @@ let package =
()
type callstack = Value_types.callstack
-
type truth = Abstract_interp.truth
type step = [ `Here | `After | `Then of exp | `Else of exp ]
-
-type probe =
- | Expr of exp * stmt
- | Lval of lval * stmt
+type probe = Pexpr of exp * stmt | Plval of lval
type domain = {
values: ( step * string ) list ;
@@ -65,6 +61,18 @@ let next_steps s : step list =
-> [ `After ]
| Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
+module CS = Value_types.Callstack
+module CSmap = CS.Hashtbl
+module CSlist =
+struct
+ type t = callstack list
+ let rec hash = function [] -> 1 | a::q -> CS.hash a + 31 * hash q
+ let rec equal ca cb = match ca , cb with
+ | [] , [] -> true
+ | a::p , b::q -> Callstack.equal a b && equal p q
+ | _ -> false
+end
+
(* -------------------------------------------------------------------------- *)
(* --- EVA Proxy --- *)
(* -------------------------------------------------------------------------- *)
@@ -72,7 +80,7 @@ let next_steps s : step list =
module type EvaProxy =
sig
val callstacks : stmt -> callstack list
- val domain : probe -> callstack option -> domain
+ val domain : Printer_tag.localizable -> callstack list -> domain
end
module Proxy(A : Analysis.S) : EvaProxy =
@@ -81,6 +89,17 @@ struct
open Eval
type dstate = A.Dom.state or_top_or_bottom
+ module CSSmap = Hashtbl.Make
+ (struct
+ type t = bool * stmt * callstack list
+ let hash (after,stmt,cs) =
+ Hashtbl.hash (after,Cil_datatype.Stmt.hash stmt,CSlist.hash cs)
+ let equal (a1,s1,cs1) (a2,s2,cs2) =
+ a1 = a2 && Cil_datatype.Stmt.equal s1 s2 && CSlist.equal cs1 cs2
+ end)
+
+ let stackcache = CSSmap.create 0
+
let callstacks stmt =
match A.get_stmt_state_by_callstack ~after:false stmt with
| `Top | `Bottom -> []
@@ -89,24 +108,47 @@ struct
let dstate ~after stmt callstack =
match callstack with
- | None -> (A.get_stmt_state ~after stmt :> dstate)
- | Some cs ->
+ | [] -> (A.get_stmt_state ~after stmt :> dstate)
+ | css ->
begin match A.get_stmt_state_by_callstack ~after stmt with
| `Top -> `Top
- | `Bottom -> `Bottom
- | `Value cmap ->
- try `Value (CSmap.find cmap cs)
- with Not_found -> `Bottom
+ | `Bottom -> `Bottom
+ | `Value cmap ->
+ match css with
+ | [cs] ->
+ begin
+ try `Value (CSmap.find cmap cs)
+ with Not_found -> `Bottom
+ end
+ | css ->
+ begin
+ try CSSmap.find stackcache (after,stmt,css)
+ with Not_found ->
+ (List.fold_left
+ (fun d cs ->
+ try
+ let s = CSmap.find cmap cs in
+ match d with
+ | `Bottom -> d
+ | `Value s0 -> `Value (A.Dom.join s0 s)
+ with Not_found -> d
+ ) `Bottom css :> dstate)
+ end
end
- let dbottom = {
+ let dnone = {
alarms = [] ;
- values = [`Here , "Unreachable (bottom)"] ;
+ values = [] ;
}
let dtop = {
alarms = [] ;
- values = [`Here , "Not available (top)"] ;
+ values = [`Here , "Not available."] ;
+ }
+
+ let dbottom = {
+ alarms = [] ;
+ values = [`Here , "Unreachable."] ;
}
let dalarms alarms =
@@ -157,10 +199,13 @@ struct
alarms
end
- let domain probe callstack =
- match probe with
- | Expr(expr,stmt) -> deval (e_expr expr) stmt callstack
- | Lval(lval,stmt) -> deval (e_lval lval) stmt callstack
+ let dexpr e s css = deval (e_expr e) s css
+ let dlval l s css = deval (e_lval l) s css
+
+ let domain marker _callstacks =
+ let open Printer_tag in
+ match marker with
+ | _ -> dnone
end
--
GitLab