Skip to content
Snippets Groups Projects
Commit f1592187 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[eva/api] EVA proxies

parent e606c07c
No related branches found
No related tags found
No related merge requests found
...@@ -24,6 +24,11 @@ open Server ...@@ -24,6 +24,11 @@ open Server
open Data open Data
open Cil_types open Cil_types
module Md = Markdown 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 = let package =
Package.package Package.package
...@@ -33,334 +38,179 @@ let package = ...@@ -33,334 +38,179 @@ let package =
~readme:"eva.md" ~readme:"eva.md"
() ()
type value = type callstack = Value_types.callstack
{ value: string;
alarm: bool; } type truth = Abstract_interp.truth
type step = [ `Here | `After | `Then of exp | `Else of exp ]
type evaluation =
| Unreachable type probe =
| Evaluation of value | Expr of exp * stmt
| Lval of lval * stmt
type after =
| Unchanged type domain = {
| Reduced of evaluation values: ( step * string ) list ;
alarms: ( truth * string ) list ;
type before_after = }
{ before: evaluation;
after_instr: after option; (* -------------------------------------------------------------------------- *)
after_then: after option; (* --- Domain Utilities --- *)
after_else: after option; } (* -------------------------------------------------------------------------- *)
type values = let next_steps s : step list =
{ values: before_after; match s.skind with
callstack: (Value_util.callstack * before_after) list option; } | If(cond,_,_,_) -> [ `Then cond ; `Else cond ]
| Instr (Set _ | Call _ | Local_init _ | Asm _ | Code_annot _)
let get_value = function | Switch _ | Loop _ | Block _ | UnspecifiedSequence _
| Unreachable -> "Unreachable" | TryCatch _ | TryFinally _ | TryExcept _
| Evaluation { value } -> value -> [ `After ]
| Instr (Skip _) | Return _ | Break _ | Continue _ | Goto _ | Throw _ -> []
let get_alarm = function
| Unreachable -> false (* -------------------------------------------------------------------------- *)
| Evaluation { alarm } -> alarm (* --- EVA Proxy --- *)
(* -------------------------------------------------------------------------- *)
let get_after_value =
Extlib.opt_map module type EvaProxy =
(function Unchanged -> "unchanged" | Reduced eval -> get_value eval) sig
val callstacks : stmt -> callstack list
module CallStackId = val domain : probe -> callstack option -> domain
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
end end
module Make (Eva: Analysis.S) : S = struct module Proxy(A : Analysis.S) : EvaProxy =
struct
let make_before eval before =
let before = open Eval
match before with type dstate = A.Dom.state or_top_or_bottom
| `Bottom -> Unreachable
| `Value state -> Evaluation (eval state) let callstacks stmt =
in match A.get_stmt_state_by_callstack ~after:false stmt with
{ before; after_instr = None; after_then = None; after_else = None; } | `Top | `Bottom -> []
| `Value states ->
let make_callstack stmt eval = CSmap.fold_sorted (fun cs _st css -> cs :: css) states []
let before = Eva.get_stmt_state_by_callstack ~after:false stmt in
match before with let dstate ~after stmt callstack =
| (`Bottom | `Top) -> [] match callstack with
| `Value before -> | None -> (A.get_stmt_state ~after stmt :> dstate)
let aux callstack before acc = | Some cs ->
let before_after = make_before eval (`Value before) in begin match A.get_stmt_state_by_callstack ~after stmt with
(callstack, before_after) :: acc | `Top -> `Top
in | `Bottom -> `Bottom
Value_types.Callstack.Hashtbl.fold aux before [] | `Value cmap ->
try `Value (CSmap.find cmap cs)
let make_before_after eval ~before ~after = with Not_found -> `Bottom
match before with end
| `Bottom ->
{ before = Unreachable; let dbottom = {
after_instr = None; alarms = [] ;
after_then = None; values = [`Here , "Unreachable (bottom)"] ;
after_else = None; } }
| `Value before ->
let before = eval before in let dtop = {
let after_instr = alarms = [] ;
match after with values = [`Here , "Not available (top)"] ;
| `Bottom -> Some (Reduced Unreachable) }
| `Value after ->
let after = eval after in let dalarms alarms =
if String.equal before.value after.value let pool = ref [] in
then Some Unchanged Alarmset.iter
else Some (Reduced (Evaluation after)) (fun alarm status ->
in let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty alarm
{ before = Evaluation before; in pool := (status , descr) :: !pool
after_instr; after_then = None; after_else = None; } ) alarms ;
List.rev !pool
let make_instr_callstack stmt eval =
let before = Eva.get_stmt_state_by_callstack ~after:false stmt in let deval (eval : A.Dom.state -> string * Alarmset.t) stmt callstack =
let after = Eva.get_stmt_state_by_callstack ~after:true stmt in match dstate ~after:false stmt callstack with
match before, after with | `Bottom -> dbottom
| (`Bottom | `Top), _ | `Top -> dtop
| _, (`Bottom | `Top) -> [] | `Value state ->
| `Value before, `Value after -> let value, alarms = eval state in
let aux callstack before acc = let dnext (step : step) vs = function
let before = `Value before in | `Top | `Bottom -> vs
let after = | `Value state -> (step , fst @@ eval state) :: vs in
try `Value (Value_types.Callstack.Hashtbl.find after callstack) let others = List.fold_right
with Not_found -> `Bottom begin fun st vs ->
in match st with
let before_after = make_before_after eval ~before ~after in | `Here -> vs (* absurd *)
(callstack, before_after) :: acc | `After -> dnext st vs @@ dstate ~after:false stmt callstack
in | `Then cond -> dnext st vs @@ A.assume_cond stmt state cond true
Value_types.Callstack.Hashtbl.fold aux before [] | `Else cond -> dnext st vs @@ A.assume_cond stmt state cond false
end (next_steps stmt) []
let make eval kinstr = in {
let before = Eva.get_kinstr_state ~after:false kinstr in values = (`Here,value) :: others ;
let values, callstack = alarms = dalarms alarms ;
match kinstr with }
| Cil_types.Kglobal ->
make_before eval before, None let e_expr expr state =
| Cil_types.Kstmt stmt -> let value, alarms = A.eval_expr state expr in
match stmt.skind with begin
| Instr _ -> Pretty_utils.to_string (Bottom.pretty A.Val.pretty) value,
let after = Eva.get_kinstr_state ~after:true kinstr in alarms
let values = make_before_after eval ~before ~after in end
let callstack = make_instr_callstack stmt eval in
values, Some callstack
| _ ->
make_before eval before, Some (make_callstack stmt eval)
in
{ values; callstack; }
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 domain probe callstack =
let eval state = match probe with
let value, alarms = Eva.eval_expr state expr in | Expr(expr,stmt) -> deval (e_expr expr) stmt callstack
let alarm = not (Alarmset.is_empty alarms) in | Lval(lval,stmt) -> deval (e_lval lval) stmt callstack
let str = Format.asprintf "%a" (Bottom.pretty Eva.Val.pretty) value in
{ value = str; alarm }
in
make eval kinstr
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 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 (* --- Request getCallstackInfos --- *)
ref (module Make (Analyzer) : S) (* -------------------------------------------------------------------------- *)
let hook (module Analyzer: Analysis.S) =
ref_request := (module Make (Analyzer) : S)
let () = Analysis.register_hook hook module Jcallstack = Data.Index(Value_types.Callstack.Map)
(struct let name = "eva-callstack-id" end)
let pretty fmt cs =
let update tag = match cs with
let module Request = (val !ref_request) in | (_, Kstmt _) :: callers ->
match tag with Value_types.Callstack.pretty_hash fmt cs;
| Printer_tag.PExp (_kf, kinstr, expr) -> Pretty_utils.pp_flowlist ~left:"@[" ~sep:" ←@ " ~right:"@]"
update_values (Request.evaluate kinstr expr) (fun fmt (kf, _) -> Kernel_function.pretty fmt kf) fmt callers
| 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 () = let () =
Server.Request.register let getCallstackInfos = Request.signature
~package ~input:(module Jcallstack) () in
~kind:`GET let set_descr = Request.result getCallstackInfos ~name:"descr"
~name:"getValues" ~descr:(Md.plain "Description")
~descr:(Md.plain "Get the abstract values computed for an expression or lvalue") (module Jstring) in
~input:(module Kernel_ast.Marker) let set_calls = Request.result getCallstackInfos ~name:"calls"
~output:(module Junit) ~descr:(Md.plain "Callers site, from last to first")
update (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)
(* -------------------------------------------------------------------------- *)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment