From f1592187688843e19601e12a748869f76aad3cb5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 3 Dec 2020 16:05:40 +0100
Subject: [PATCH] [eva/api] EVA proxies
---
src/plugins/value/api/values_request.ml | 488 ++++++++----------------
1 file changed, 169 insertions(+), 319 deletions(-)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index 85d2df413cd..25c4f4626a2 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -24,6 +24,11 @@ open Server
open Data
open Cil_types
module Md = Markdown
+module Jkf = Kernel_ast.Kf
+module Jki = Kernel_ast.Ki
+module Jstmt = Kernel_ast.Stmt
+module CS = Value_types.Callstack
+module CSmap = CS.Hashtbl
let package =
Package.package
@@ -33,334 +38,179 @@ let package =
~readme:"eva.md"
()
-type value =
- { value: string;
- alarm: bool; }
-
-type evaluation =
- | Unreachable
- | Evaluation of value
-
-type after =
- | Unchanged
- | Reduced of evaluation
-
-type before_after =
- { before: evaluation;
- after_instr: after option;
- after_then: after option;
- after_else: after option; }
-
-type values =
- { values: before_after;
- callstack: (Value_util.callstack * before_after) list option; }
-
-let get_value = function
- | Unreachable -> "Unreachable"
- | Evaluation { value } -> value
-
-let get_alarm = function
- | Unreachable -> false
- | Evaluation { alarm } -> alarm
-
-let get_after_value =
- Extlib.opt_map
- (function Unchanged -> "unchanged" | Reduced eval -> get_value eval)
-
-module CallStackId =
- Data.Index
- (Value_types.Callstack.Map)
- (struct
- let name = "eva-callstack-id"
- end)
-
-(* This pretty-printer drops the toplevel kf, which is always the function
- in which we are pretty-printing the expression/term *)
-let pretty_callstack fmt cs =
- match cs with
- | [_, Kglobal] -> ()
- | (_kf_cur, Kstmt callsite) :: q -> begin
- let rec aux callsite = function
- | (kf, callsite') :: q -> begin
- Format.fprintf fmt "%a (%a)"
- Kernel_function.pretty kf
- Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc callsite);
- match callsite' with
- | Kglobal -> ()
- | Kstmt callsite' ->
- Format.fprintf fmt " â†@ ";
- aux callsite' q
- end
- | _ -> assert false
- in
- Format.fprintf fmt "@[<hv>%a" Value_types.Callstack.pretty_hash cs;
- aux callsite q;
- Format.fprintf fmt "@]"
- end
- | _ -> assert false
-
-(* This pretty-printer prints only the lists of the functions, not
- the locations. *)
-let pretty_callstack_short fmt cs =
- match cs with
- | [_, Kglobal] -> ()
- | (_kf_cur, Kstmt _callsite) :: q ->
- Format.fprintf fmt "%a" Value_types.Callstack.pretty_hash cs;
- Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
- (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt q
- | _ -> assert false
-
-module CallStack = struct
- type record
-
- let record: record Record.signature = Record.signature ()
-
- let id = Record.field record ~name:"id"
- ~descr:(Md.plain "Callstack id") (module Jint)
- let short = Record.field record ~name:"short"
- ~descr:(Md.plain "Short name for the callstack") (module Jstring)
- let full = Record.field record ~name:"full"
- ~descr:(Md.plain "Full name for the callstack") (module Jstring)
-
- module R =
- (val
- (Record.publish
- ~package
- ~name:"callstack"
- ~descr:(Md.plain "CallStack")
- record) : Record.S with type r = record)
-
- type t = Value_types.callstack option
-
- let jtype = R.jtype
-
- let pp_callstack ~short = function
- | None -> if short then "all" else ""
- | Some callstack ->
- let pp_text =
- if short
- then Pretty_utils.to_string ~margin:50 pretty_callstack_short
- else Pretty_utils.to_string pretty_callstack
- in
- (pp_text callstack)
-
- let id_callstack = function
- | None -> -1
- | Some callstack -> CallStackId.get callstack
-
- let to_json callstack =
- R.default |>
- R.set id (id_callstack callstack) |>
- R.set short (pp_callstack ~short:true callstack) |>
- R.set full (pp_callstack ~short:false callstack) |>
- R.to_json
-
- let key = function
- | None -> "all"
- | Some callstack -> string_of_int (CallStackId.get callstack)
-end
-
-
-let consolidated = ref None
-let table = Hashtbl.create 100
-
-let iter f =
- if Hashtbl.length table > 1
- then Extlib.may (fun values -> f (None, values)) !consolidated;
- Hashtbl.iter (fun key data -> f (Some key, data)) table
-
-let array =
- let model = States.model () in
- let () =
- States.column
- ~name:"callstack"
- ~descr:(Md.plain "CallStack")
- ~data:(module CallStack)
- ~get:fst
- model
- in
- let () =
- States.column
- ~name:"value_before"
- ~descr:(Md.plain "Value inferred just before the selected point")
- ~data:(module Jstring)
- ~get:(fun (_, e) -> get_value e.before)
- model
- in
- let () =
- States.column
- ~name:"alarm"
- ~descr:(Md.plain "Did the evaluation led to an alarm?")
- ~data:(module Jbool)
- ~get:(fun (_, e) -> get_alarm e.before)
- model
- in
- let () =
- States.column
- ~name:"value_after"
- ~descr:(Md.plain "Value inferred just after the selected point")
- ~data:(module Joption(Jstring))
- ~get:(fun (_, e) -> get_after_value e.after_instr)
- model
- in
- States.register_array
- ~package
- ~name:"values"
- ~descr:(Md.plain "Abstract values inferred by the Eva analysis")
- ~key:(fun (cs, _) -> CallStack.key cs)
- ~iter
- model
-
-let update_values values =
- Hashtbl.clear table;
- consolidated := Some values.values;
- let () =
- match values.callstack with
- | None -> ()
- | Some by_callstack ->
- List.iter
- (fun (callstack, before_after) ->
- Hashtbl.add table callstack before_after)
- by_callstack
- in
- States.reload array
-
-module type S = sig
- val evaluate: kinstr -> exp -> values
- val lvaluate: kinstr -> lval -> values
+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 domain = {
+ values: ( step * string ) list ;
+ alarms: ( truth * string ) list ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Domain Utilities --- *)
+(* -------------------------------------------------------------------------- *)
+
+let next_steps s : step list =
+ match s.skind with
+ | If(cond,_,_,_) -> [ `Then cond ; `Else cond ]
+ | Instr (Set _ | Call _ | Local_init _ | Asm _ | Code_annot _)
+ | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
+ | TryCatch _ | TryFinally _ | TryExcept _
+ -> [ `After ]
+ | Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
+
+(* -------------------------------------------------------------------------- *)
+(* --- EVA Proxy --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type EvaProxy =
+sig
+ val callstacks : stmt -> callstack list
+ val domain : probe -> callstack option -> domain
end
-module Make (Eva: Analysis.S) : S = struct
-
- let make_before eval before =
- let before =
- match before with
- | `Bottom -> Unreachable
- | `Value state -> Evaluation (eval state)
- in
- { before; after_instr = None; after_then = None; after_else = None; }
-
- let make_callstack stmt eval =
- let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
- match before with
- | (`Bottom | `Top) -> []
- | `Value before ->
- let aux callstack before acc =
- let before_after = make_before eval (`Value before) in
- (callstack, before_after) :: acc
- in
- Value_types.Callstack.Hashtbl.fold aux before []
-
- let make_before_after eval ~before ~after =
- match before with
- | `Bottom ->
- { before = Unreachable;
- after_instr = None;
- after_then = None;
- after_else = None; }
- | `Value before ->
- let before = eval before in
- let after_instr =
- match after with
- | `Bottom -> Some (Reduced Unreachable)
- | `Value after ->
- let after = eval after in
- if String.equal before.value after.value
- then Some Unchanged
- else Some (Reduced (Evaluation after))
- in
- { before = Evaluation before;
- after_instr; after_then = None; after_else = None; }
-
- let make_instr_callstack stmt eval =
- let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
- let after = Eva.get_stmt_state_by_callstack ~after:true stmt in
- match before, after with
- | (`Bottom | `Top), _
- | _, (`Bottom | `Top) -> []
- | `Value before, `Value after ->
- let aux callstack before acc =
- let before = `Value before in
- let after =
- try `Value (Value_types.Callstack.Hashtbl.find after callstack)
- with Not_found -> `Bottom
- in
- let before_after = make_before_after eval ~before ~after in
- (callstack, before_after) :: acc
- in
- Value_types.Callstack.Hashtbl.fold aux before []
-
- let make eval kinstr =
- let before = Eva.get_kinstr_state ~after:false kinstr in
- let values, callstack =
- match kinstr with
- | Cil_types.Kglobal ->
- make_before eval before, None
- | Cil_types.Kstmt stmt ->
- match stmt.skind with
- | Instr _ ->
- let after = Eva.get_kinstr_state ~after:true kinstr in
- let values = make_before_after eval ~before ~after in
- let callstack = make_instr_callstack stmt eval in
- values, Some callstack
- | _ ->
- make_before eval before, Some (make_callstack stmt eval)
- in
- { values; callstack; }
+module Proxy(A : Analysis.S) : EvaProxy =
+struct
+
+ open Eval
+ type dstate = A.Dom.state or_top_or_bottom
+
+ let callstacks stmt =
+ match A.get_stmt_state_by_callstack ~after:false stmt with
+ | `Top | `Bottom -> []
+ | `Value states ->
+ CSmap.fold_sorted (fun cs _st css -> cs :: css) states []
+
+ let dstate ~after stmt callstack =
+ match callstack with
+ | None -> (A.get_stmt_state ~after stmt :> dstate)
+ | Some cs ->
+ 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
+ end
+
+ let dbottom = {
+ alarms = [] ;
+ values = [`Here , "Unreachable (bottom)"] ;
+ }
+
+ let dtop = {
+ alarms = [] ;
+ values = [`Here , "Not available (top)"] ;
+ }
+
+ let dalarms alarms =
+ let pool = ref [] in
+ Alarmset.iter
+ (fun alarm status ->
+ let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty alarm
+ in pool := (status , descr) :: !pool
+ ) alarms ;
+ List.rev !pool
+
+ let deval (eval : A.Dom.state -> string * Alarmset.t) stmt callstack =
+ match dstate ~after:false stmt callstack with
+ | `Bottom -> dbottom
+ | `Top -> dtop
+ | `Value state ->
+ let value, alarms = eval state in
+ let dnext (step : step) vs = function
+ | `Top | `Bottom -> vs
+ | `Value state -> (step , fst @@ eval state) :: vs in
+ let others = List.fold_right
+ begin fun st vs ->
+ match st with
+ | `Here -> vs (* absurd *)
+ | `After -> dnext st vs @@ dstate ~after:false stmt callstack
+ | `Then cond -> dnext st vs @@ A.assume_cond stmt state cond true
+ | `Else cond -> dnext st vs @@ A.assume_cond stmt state cond false
+ end (next_steps stmt) []
+ in {
+ values = (`Here,value) :: others ;
+ alarms = dalarms alarms ;
+ }
+
+ let e_expr expr state =
+ let value, alarms = A.eval_expr state expr in
+ begin
+ Pretty_utils.to_string (Bottom.pretty A.Val.pretty) value,
+ alarms
+ end
+ let e_lval lval state =
+ let value, alarms = A.copy_lvalue state lval in
+ let flagged = match value with
+ | `Bottom -> Eval.Flagged_Value.bottom
+ | `Value v -> v in
+ begin
+ Pretty_utils.to_string (Eval.Flagged_Value.pretty A.Val.pretty) flagged,
+ alarms
+ end
- let evaluate kinstr expr =
- let eval state =
- let value, alarms = Eva.eval_expr state expr in
- let alarm = not (Alarmset.is_empty alarms) in
- let str = Format.asprintf "%a" (Bottom.pretty Eva.Val.pretty) value in
- { value = str; alarm }
- in
- make eval kinstr
+ 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 lvaluate kinstr lval =
- let eval state =
- let value, alarms = Eva.copy_lvalue state lval in
- let alarm = not (Alarmset.is_empty alarms) in
- let flagged_value = match value with
- | `Bottom -> Eval.Flagged_Value.bottom
- | `Value v -> v
- in
- let pretty = Eval.Flagged_Value.pretty Eva.Val.pretty in
- let str = Format.asprintf "%a" pretty flagged_value in
- { value = str; alarm }
- in
- make eval kinstr
end
+let proxy =
+ let make (a : (module Analysis.S)) = (module Proxy(val a) : EvaProxy) in
+ let current = ref (make @@ Analysis.current_analyzer ()) in
+ let () = Analysis.register_hook (fun a -> current := make a) in
+ current
-let ref_request =
- let module Analyzer = (val Analysis.current_analyzer ()) in
- ref (module Make (Analyzer) : S)
-
-let hook (module Analyzer: Analysis.S) =
- ref_request := (module Make (Analyzer) : S)
+(* -------------------------------------------------------------------------- *)
+(* --- Request getCallstackInfos --- *)
+(* -------------------------------------------------------------------------- *)
-let () = Analysis.register_hook hook
+module Jcallstack = Data.Index(Value_types.Callstack.Map)
+ (struct let name = "eva-callstack-id" end)
-
-let update tag =
- let module Request = (val !ref_request) in
- match tag with
- | Printer_tag.PExp (_kf, kinstr, expr) ->
- update_values (Request.evaluate kinstr expr)
- | Printer_tag.PLval (_kf, kinstr, lval) ->
- update_values (Request.lvaluate kinstr lval)
- | PVDecl (_kf, kinstr, varinfo) ->
- update_values (Request.lvaluate kinstr (Var varinfo, NoOffset))
- | _ -> ()
+let pretty fmt cs =
+ match cs with
+ | (_, Kstmt _) :: callers ->
+ Value_types.Callstack.pretty_hash fmt cs;
+ Pretty_utils.pp_flowlist ~left:"@[" ~sep:" â†@ " ~right:"@]"
+ (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt callers
+ | _ -> ()
let () =
- Server.Request.register
- ~package
- ~kind:`GET
- ~name:"getValues"
- ~descr:(Md.plain "Get the abstract values computed for an expression or lvalue")
- ~input:(module Kernel_ast.Marker)
- ~output:(module Junit)
- update
+ let getCallstackInfos = Request.signature
+ ~input:(module Jcallstack) () in
+ let set_descr = Request.result getCallstackInfos ~name:"descr"
+ ~descr:(Md.plain "Description")
+ (module Jstring) in
+ let set_calls = Request.result getCallstackInfos ~name:"calls"
+ ~descr:(Md.plain "Callers site, from last to first")
+ (module Jlist(Jpair(Jkf)(Jki))) in
+ Request.register_sig ~package getCallstackInfos
+ ~kind:`GET ~name:"getCallstackInfos"
+ ~descr:(Md.plain "Callstack Description")
+ begin fun rq cs ->
+ set_calls rq cs ;
+ set_descr rq (Pretty_utils.to_string pretty cs) ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request getCallstacks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getCallstacks"
+ ~descr:(Md.plain "Callstacks to a statement")
+ ~input:(module Jstmt)
+ ~output:(module Jlist(Jcallstack))
+ (fun stmt -> let module A = (val !proxy) in A.callstacks stmt)
+
+(* -------------------------------------------------------------------------- *)
--
GitLab