Skip to content
Snippets Groups Projects
Commit b2440bae authored by David Bühler's avatar David Bühler Committed by Maxime Jacquemin
Browse files

[Eva] Values_request: renames and reorders some types and functions. 

Adds a few comments.
parent 779a1fad
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/value/api/values_request.ml
+ 163
− 136
View file @ b2440bae
......@@ -51,20 +51,26 @@ type probe =
type callstack = Value_types.callstack
type truth = Abstract_interp.truth
type value = {
(* The result of an evaluation:
- the resulting value as a text to be printed;
- the alarms emitted for the evaluation;
- the variables pointed by the resulting value, if any. *)
type evaluation = {
value: string;
alarms: ( truth * string ) list ;
pointed_vars: (string * Printer_tag.localizable) list;
}
(* Evaluations after the given statement. If the statement is a conditional
branch, evaluations in the [then] and [else] branch. *)
type 'v next =
| After of 'v
| Cond of 'v * 'v
| Nothing
type domain = {
here: value;
next: value next;
type evaluations = {
here: evaluation;
next: evaluation next;
}
let signal = Request.signal ~package ~name:"changed"
......@@ -242,13 +248,92 @@ module Jtruth : Data.S with type t = truth = struct
| _ -> Abstract_interp.Unknown
end
(* -------------------------------------------------------------------------- *)
(* --- Utility functions for cvalue and offsetmaps --- *)
(* -------------------------------------------------------------------------- *)
type offsetmap =
| Offsetmap of Cvalue.V_Offsetmap.t
| Bottom | Empty | Top | InvalidLoc
let pp_offsetmap typ fmt = function
| Bottom -> Format.fprintf fmt "<BOTTOM>"
| Empty -> Format.fprintf fmt "<EMPTY>"
| Top -> Format.fprintf fmt "<NO INFORMATION>"
| InvalidLoc -> Format.fprintf fmt "<INVALID LOCATION>"
| Offsetmap offsm ->
Cvalue.V_Offsetmap.pretty_generic ~typ () fmt offsm ;
Eval_op.pretty_stitched_offsetmap fmt typ offsm
let extract_single_var vi state =
let b = Base.of_varinfo vi in
try
match Cvalue.Model.find_base b state with
| `Bottom -> Bottom
| `Value m -> Offsetmap m
| `Top -> Top
with Not_found -> InvalidLoc
let reduce_loc_and_eval state loc =
if Cvalue.Model.is_top state then Top
else if not (Cvalue.Model.is_reachable state) then Bottom
else if Int_Base.(equal loc.Locations.size zero) then Empty
else
let loc' = Locations.(valid_part Read loc) in
if Locations.is_bottom_loc loc' then InvalidLoc
else
try
let size = Int_Base.project loc'.Locations.size in
match Cvalue.Model.copy_offsetmap loc'.Locations.loc size state with
| `Bottom -> InvalidLoc
| `Value offsm -> Offsetmap offsm
with Abstract_interp.Error_Top -> Top
let find_offsetmap cvalue_state precise_loc =
let f loc acc =
match acc, reduce_loc_and_eval cvalue_state loc with
| Offsetmap o1, Offsetmap o2 -> Offsetmap (Cvalue.V_Offsetmap.join o1 o2)
| Bottom, v | v, Bottom -> v
| Empty, v | v, Empty -> v
| Top, Top -> Top
| InvalidLoc, InvalidLoc -> InvalidLoc
| InvalidLoc, (Offsetmap _ as res) -> res
| Offsetmap _, InvalidLoc -> acc
| Top, r | r, Top -> r (* cannot happen, we should get Top everywhere *)
in
Precise_locs.fold f precise_loc Bottom
(* Get pointed bases from a cvalue. *)
let get_bases cvalue =
try Base.SetLattice.project (Cvalue.V.get_bases cvalue)
with Abstract_interp.Error_Top -> Base.Hptset.empty
(* Get pointed bases from an offsetmap. *)
let get_pointed_bases = function
| Offsetmap offsm ->
Cvalue.V_Offsetmap.fold_on_values
(fun v acc ->
let v = Cvalue.V_Or_Uninitialized.get_v v in
Base.Hptset.union acc (get_bases v))
offsm Base.Hptset.empty
| Bottom | Empty | Top | InvalidLoc -> Base.Hptset.empty
(* Only keep a list of C variables from both previous functions. *)
let filter_variables bases =
let add_var base acc =
try Base.to_varinfo base :: acc
with Base.Not_a_C_variable -> acc
in
let vars = List.rev (Base.Hptset.fold add_var bases []) in
List.filter (fun vi -> not (Cil.isFunctionType vi.vtype)) vars
(* -------------------------------------------------------------------------- *)
(* --- EVA Proxy --- *)
(* -------------------------------------------------------------------------- *)
module type EvaProxy = sig
val callstacks : stmt -> callstack list
val domain : probe -> callstack option -> domain
val evaluate : probe -> callstack option -> evaluations
end
module Proxy(A : Analysis.S) : EvaProxy = struct
......@@ -256,6 +341,15 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
open Eval
type dstate = A.Dom.state or_top_or_bottom
let get_precise_loc =
match A.Loc.get Main_locations.PLoc.key with
| None -> fun _ -> Precise_locs.loc_top
| Some get -> get
let get_cvalue =
let default = fun _ -> Cvalue.V.top in
Option.value ~default (A.Val.get Main_values.CVal.key)
let callstacks stmt =
match A.get_stmt_state_by_callstack ~after:false stmt with
| `Top | `Bottom -> []
......@@ -270,88 +364,75 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
try `Value (CSmap.find cmap cs)
with Not_found -> `Bottom
type to_offsetmap =
| Bottom
| Offsetmap of Cvalue.V_Offsetmap.t
| Empty
| Top
| InvalidLoc
let extract_single_var vi state =
let b = Base.of_varinfo vi in
try
match Cvalue.Model.find_base b state with
| `Bottom -> Bottom
| `Value m -> Offsetmap m
| `Top -> Top
with Not_found -> InvalidLoc
let reduce_loc_and_eval loc state =
if Cvalue.Model.is_top state then Top
else if not (Cvalue.Model.is_reachable state) then Bottom
else if Int_Base.(equal loc.Locations.size zero) then Empty
else
let loc' = Locations.(valid_part Read loc) in
if Locations.is_bottom_loc loc' then InvalidLoc
else
try
let size = Int_Base.project loc'.Locations.size in
match Cvalue.Model.copy_offsetmap loc'.Locations.loc size state with
| `Bottom -> InvalidLoc
| `Value offsm -> Offsetmap offsm
with Abstract_interp.Error_Top -> Top
(* --- Converts an evaluation [result] into an exported [value]. ---------- *)
let get_precise_loc =
match A.Loc.get Main_locations.PLoc.key with
| None -> fun _ -> Precise_locs.loc_top
| Some get -> get
(* Result of an evaluation: a generic value for scalar types, or an offsetmap
for struct and arrays. *)
type result =
| Value of A.Val.t
| Offsetmap of offsetmap
let pp_result typ fmt = function
| Value v -> A.Val.pretty fmt v
| Offsetmap offsm -> pp_offsetmap typ fmt offsm
let get_pointed_bases = function
| Value v -> get_bases (get_cvalue v)
| Offsetmap offsm -> get_pointed_bases offsm
let get_pointed_markers stmt result =
let bases = get_pointed_bases result in
let vars = filter_variables bases in
let kf =
try Some (Kernel_function.find_englobing_kf stmt)
with Not_found -> None
in
let to_marker vi =
let text = Pretty_utils.to_string Printer.pp_varinfo vi in
let marker = Printer_tag.PLval (kf, Kstmt stmt, Cil.var vi) in
text, marker
in
List.map to_marker vars
(* Creates an exported [value] from an evaluation result. *)
let make_value typ stmt (result, alarms) =
let alarms =
let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty in
let f alarm status acc = (status, descr alarm) :: acc in
Alarmset.fold f [] alarms |> List.rev
in
let pretty_eval = Bottom.pretty (pp_result typ) in
let value = Pretty_utils.to_string pretty_eval result in
let pointed_vars =
Bottom.fold ~bottom:[] (get_pointed_markers stmt) result
in
{ value; alarms; pointed_vars }
(* --- Evaluates an expression or lvalue into an evaluation [result]. ----- *)
let lval_to_offsetmap lval state =
let cvalue = A.Dom.get_cvalue_or_top state in
let cvalue_state = A.Dom.get_cvalue_or_top state in
match lval with
| Var vi, NoOffset ->
let r = extract_single_var vi cvalue in
let r = extract_single_var vi cvalue_state in
`Value r, Alarmset.none
| _ ->
A.eval_lval_to_loc state lval >>=: fun loc ->
let precise_loc = get_precise_loc loc in
let f loc acc =
match acc, reduce_loc_and_eval loc cvalue with
| Offsetmap o1, Offsetmap o2 -> Offsetmap (Cvalue.V_Offsetmap.join o1 o2)
| Bottom, v | v, Bottom -> v
| Empty, v | v, Empty -> v
| Top, Top -> Top
| InvalidLoc, InvalidLoc -> InvalidLoc
| InvalidLoc, (Offsetmap _ as res) -> res
| Offsetmap _, InvalidLoc -> acc
| Top, r | r, Top -> r (* cannot happen, we should get Top everywhere *)
in
Precise_locs.fold f precise_loc Bottom
type evaluation =
| ToValue of A.Val.t
| ToOffsetmap of to_offsetmap
let pp_evaluation typ fmt = function
| ToValue v -> A.Val.pretty fmt v
| ToOffsetmap Bottom -> Format.fprintf fmt "<BOTTOM>"
| ToOffsetmap Empty -> Format.fprintf fmt "<EMPTY>"
| ToOffsetmap Top -> Format.fprintf fmt "<NO INFORMATION>"
| ToOffsetmap InvalidLoc -> Format.fprintf fmt "<INVALID LOCATION>"
| ToOffsetmap (Offsetmap o) ->
Cvalue.V_Offsetmap.pretty_generic ~typ () fmt o ;
Eval_op.pretty_stitched_offsetmap fmt typ o
find_offsetmap cvalue_state precise_loc
let eval_lval lval state =
match Cil.(unrollType (typeOfLval lval)) with
| TInt _ | TEnum _ | TPtr _ | TFloat _ ->
A.copy_lvalue state lval >>=. fun value ->
value.v >>-: fun v -> ToValue v
value.v >>-: fun v -> Value v
| _ ->
lval_to_offsetmap lval state >>=: fun offsm -> ToOffsetmap offsm
lval_to_offsetmap lval state >>=: fun offsm -> Offsetmap offsm
let eval_expr expr state =
A.eval_expr state expr >>=: fun value -> ToValue value
A.eval_expr state expr >>=: fun value -> Value value
(* --- Evaluates all steps (before/after the statement). ------------------ *)
let do_next eval state stmt callstack =
match stmt.skind with
......@@ -364,7 +445,13 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
After (eval after_state)
| _ -> Nothing
let eval_steps eval stmt callstack =
let eval_steps typ eval stmt callstack =
let default value = { value; alarms = []; pointed_vars = []; } in
let eval = function
| `Bottom -> default "Unreachable"
| `Top -> default "No information"
| `Value state -> make_value typ stmt (eval state)
in
let before = dstate ~after:false stmt callstack in
let here = eval before in
let next =
......@@ -374,72 +461,12 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
in
{ here; next; }
let get_cvalue =
let default = fun _ -> Cvalue.V.top in
Option.value ~default (A.Val.get Main_values.CVal.key)
let get_bases cvalue =
try Base.SetLattice.project (Cvalue.V.get_bases cvalue)
with Abstract_interp.Error_Top -> Base.Hptset.empty
let get_pointed_bases = function
| ToValue v -> get_bases (get_cvalue v)
| ToOffsetmap (Offsetmap offsm) ->
Cvalue.V_Offsetmap.fold_on_values
(fun v acc ->
let v = Cvalue.V_Or_Uninitialized.get_v v in
Base.Hptset.union acc (get_bases v))
offsm Base.Hptset.empty
| ToOffsetmap (Bottom | Empty | Top | InvalidLoc) -> Base.Hptset.empty
let get_pointed_vars evaluation =
let bases = get_pointed_bases evaluation in
let add_var base acc =
try Base.to_varinfo base :: acc
with Base.Not_a_C_variable -> acc
in
let vars = Base.Hptset.fold add_var bases [] in
List.filter (fun vi -> not (Cil.isFunctionType vi.vtype)) vars
let make_value typ stmt (evaluation, alarms) =
let alarms =
let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty in
let f alarm status acc = (status, descr alarm) :: acc in
Alarmset.fold f [] alarms |> List.rev
in
let pretty_eval = Bottom.pretty (pp_evaluation typ) in
let value = Pretty_utils.to_string pretty_eval evaluation in
let pointed_vars =
let vars = Bottom.fold ~bottom:[] get_pointed_vars evaluation in
let kf =
try Some (Kernel_function.find_englobing_kf stmt)
with Not_found -> None
in
let to_marker vi =
let text = Pretty_utils.to_string Printer.pp_varinfo vi in
let marker = Printer_tag.PLval (kf, Kstmt stmt, Cil.var vi) in
text, marker
in
List.map to_marker vars
in
{ value; alarms; pointed_vars }
let domain_eval typ eval stmt callstack =
let default value = { value; alarms = []; pointed_vars = []; } in
let eval = function
| `Bottom -> default "Unreachable"
| `Top -> default "No information"
| `Value state -> make_value typ stmt (eval state)
in
eval_steps eval stmt callstack
let domain p callstack =
let evaluate p callstack =
match p with
| Plval (lval, stmt) ->
domain_eval (Cil.typeOfLval lval) (eval_lval lval) stmt callstack
eval_steps (Cil.typeOfLval lval) (eval_lval lval) stmt callstack
| Pexpr (expr, stmt) ->
domain_eval (Cil.typeOf expr) (eval_expr expr) stmt callstack
eval_steps (Cil.typeOf expr) (eval_expr expr) stmt callstack
| Pnone -> assert false
end
......@@ -571,7 +598,7 @@ module JEvaluation = struct
~descr:(Markdown.plain "Evaluation of an expression or lvalue")
module R: Record.S with type r = record = (val data)
type t = value
type t = evaluation
let jtype = R.jtype
let to_json t =
......@@ -609,7 +636,7 @@ let () =
begin fun rq () ->
let module A : EvaProxy = (val proxy ()) in
let marker = get_tgt rq and callstack = get_cs rq in
let domain = A.domain (probe marker) callstack in
let domain = A.evaluate (probe marker) callstack in
set_before rq domain.here;
match domain.next with
| After value -> set_after rq (Some value)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment