From c8c45ee928d5c72bb587c77507706c06f15ac805 Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Thu, 4 Nov 2021 13:31:52 +0100
Subject: [PATCH] [ivette] Displaying Offsetmap for structures and arrays
We have the same behavior as in the previous GUI. We are going to
discuss about potential improvements.
---
src/plugins/value/api/values_request.ml | 107 +++++++++++++++++++++---
1 file changed, 94 insertions(+), 13 deletions(-)
diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml
index b94f43d4b1e..6701e807f55 100644
--- a/src/plugins/value/api/values_request.ml
+++ b/src/plugins/value/api/values_request.ml
@@ -276,12 +276,90 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
| (`Top | `Bottom) as res -> res
| `Value cmap -> try `Value (CSmap.find cmap cs) with Not_found -> `Bottom
- let eval_lval lval state =
- let value, alarms = A.copy_lvalue state lval in
- let default = Eval.Flagged_Value.bottom in
- (Bottom.default ~default value).v, alarms
+ 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 -> InvalidLoc
+ | `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 -> Bottom
+ | `Value offsm -> Offsetmap offsm
+ with Abstract_interp.Error_Top -> Top
+
+ let extract_or_reduce_lval lval state =
+ match lval with
+ | Var vi, NoOffset -> let r = extract_single_var vi state in fun _ -> r
+ | _ -> fun loc -> reduce_loc_and_eval loc state
+
+ let lval_to_offsetmap lval state =
+ let loc, alarms = A.eval_lval_to_loc state lval in
+ let state = A.Dom.get_cvalue_or_top state in
+ let extract = extract_or_reduce_lval lval state in
+ let precise_loc =
+ match A.Loc.get Main_locations.PLoc.key with
+ | None -> `Value (Precise_locs.loc_top)
+ | Some get -> loc >>-: get
+ and f loc acc =
+ match acc, extract 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_loc >>-: (fun loc -> Precise_locs.fold f loc Bottom), alarms
+
+ 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:(Some typ) () fmt o ;
+ Eval_op.pretty_stitched_offsetmap fmt typ o
- let eval_expr expr state = A.eval_expr state expr
+ let eval_lval lval state =
+ match Cil.(unrollType @@ typeOfLval lval) with
+ | TInt _ | TEnum _ | TPtr _ | TFloat _ ->
+ let value, alarms = A.copy_lvalue state lval in
+ let _ = lval_to_offsetmap lval state in
+ let default = Eval.Flagged_Value.bottom in
+ (Bottom.default ~default value).v >>-: (fun v -> ToValue v), alarms
+ | _ ->
+ let offsetmap, alarms = lval_to_offsetmap lval state in
+ offsetmap >>-: (fun r -> ToOffsetmap r), alarms
+
+ let eval_expr expr state =
+ let value, alarms = A.eval_expr state expr in
+ value >>-: (fun v -> ToValue v), alarms
let dalarms alarms =
let descr = Format.asprintf "@[<hov 2>%a@]" Alarms.pretty in
@@ -297,15 +375,15 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
| `Else cond -> (A.assume_cond stmt state cond false :> dstate)
in List.fold_left (fun acc step -> f acc step @@ add_state step) acc steps
- let domain_step eval ((values, alarms) as acc) step =
- let to_string = Pretty_utils.to_string (Bottom.pretty A.Val.pretty) in
+ let domain_step typ eval ((values, alarms) as acc) step =
+ let to_str = Pretty_utils.to_string (Bottom.pretty (pp_evaluation typ)) in
handle_top_or_bottom ~top:acc ~bottom:acc @@ fun state ->
let step_value, step_alarms = eval state in
let alarms = match step with `Here -> step_alarms | _ -> alarms in
- (step, to_string step_value) :: values, alarms
+ (step, to_str step_value) :: values, alarms
- let domain_eval eval stmt callstack =
- let fold = fold_steps (domain_step eval) stmt callstack in
+ let domain_eval typ eval stmt callstack =
+ let fold = fold_steps (domain_step typ eval) stmt callstack in
let build (vs, als) = { values = List.rev vs ; alarms = dalarms als } in
let compute_domain state = fold state ([], Alarmset.none) |> build in
handle_top_or_bottom ~top:dtop ~bottom:dbottom compute_domain @@
@@ -313,8 +391,10 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let domain p callstack =
match p with
- | Plval (lval, stmt) -> domain_eval (eval_lval lval) stmt callstack
- | Pexpr (expr, stmt) -> domain_eval (eval_expr expr) stmt callstack
+ | Plval (lval, stmt) ->
+ domain_eval (Cil.typeOfLval lval) (eval_lval lval) stmt callstack
+ | Pexpr (expr, stmt) ->
+ domain_eval (Cil.typeOf expr) (eval_expr expr) stmt callstack
| Pnone -> dnone
let var_of_base base acc =
@@ -323,7 +403,8 @@ module Proxy(A : Analysis.S) : EvaProxy = struct
let compute_pointed_lvalues eval_lval stmt callstack =
Option.(bind (A.Val.get Main_values.CVal.key)) @@ fun get ->
- let loc state = eval_lval state |> fst >>-: get in
+ let get_eval = function ToValue v -> `Value (get v) | _ -> `Bottom in
+ let loc state = eval_lval state |> fst >>- get_eval in
let bases value = Cvalue.V.fold_bases var_of_base value [] in
let lvalues state = loc state >>-: bases >>-: List.map Cil.var in
let compute state = lvalues state |> Bottom.to_option in
--
GitLab