From a62fe77357dc6041b85a116e73daa5838da60421 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 5 Jun 2024 16:35:33 +0200
Subject: [PATCH] [region] dump results & access
---
src/plugins/region/analysis.ml | 14 ++++++++--
src/plugins/region/code.ml | 2 +-
src/plugins/region/memory.ml | 48 ++++++++++++++++++++++++++++------
src/plugins/region/memory.mli | 2 ++
src/plugins/region/services.ml | 11 ++++++++
5 files changed, 66 insertions(+), 11 deletions(-)
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
index 0a1ca081d49..58d131f5b4f 100644
--- a/src/plugins/region/analysis.ml
+++ b/src/plugins/region/analysis.ml
@@ -53,9 +53,19 @@ let find = STATE.find
let get kf =
try STATE.find kf with Not_found ->
- Options.feedback ~ontty:`Transient "Function %a" Kernel_function.pretty kf ;
+ Options.feedback ~ontty:`Transient "Function %a…" Kernel_function.pretty kf ;
let domain = Code.domain kf in
- STATE.add kf domain ; domain
+ STATE.add kf domain ;
+ Options.result "@[<v 2>Function %a:%t@]@."
+ Kernel_function.pretty kf
+ begin fun fmt ->
+ Memory.iter domain.map
+ begin fun r m ->
+ Format.pp_print_newline fmt () ;
+ Memory.pp_region fmt r m ;
+ end
+ end ;
+ domain
let compute kf = ignore @@ get kf
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
index 1a39ee97ab0..2c1b468afd1 100644
--- a/src/plugins/region/code.ml
+++ b/src/plugins/region/code.ml
@@ -83,7 +83,7 @@ and exp (m: map) (s:stmt) (e:exp) : node option =
| BinOp((PlusPI|MinusPI),p,k,_) ->
value m s k ;
let r = pointer m s p in
- Memory.shift m r (Exp(s,e)) ;
+ Memory.shift m r (Exp(s,p)) ;
Some r
| BinOp(_,a,b,_) ->
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index f430fea6630..4ecd531ad66 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -54,6 +54,26 @@ type map = {
mutable index: node Vmap.t ;
}
+(* -------------------------------------------------------------------------- *)
+(* --- Accessors --- *)
+(* -------------------------------------------------------------------------- *)
+
+let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_) -> s
+let points_to = function Blob | Compound _ -> None | Cell(_,p) -> p
+let ranges = function Blob | Cell _ -> [] | Compound(_,R rs) -> rs
+
+let types (m : region) : typ list =
+ let pool = ref Typ.Set.empty in
+ let add acs =
+ pool := Typ.Set.add (Cil.unrollType @@ Access.typeof acs) !pool in
+ Access.Set.iter add m.reads ;
+ Access.Set.iter add m.writes ;
+ Typ.Set.elements !pool
+
+(* -------------------------------------------------------------------------- *)
+(* --- Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
let pp_node fmt (n : node) = Format.fprintf fmt "R%04x" @@ Store.id n
let pp_layout fmt = function
@@ -61,12 +81,28 @@ let pp_layout fmt = function
| Cell(s,None) -> Format.fprintf fmt "<%04d>" s
| Cell(s,Some n) -> Format.fprintf fmt "<%04d>(*%a)" s pp_node n
| Compound(s,rg) ->
- Format.fprintf fmt "@[<hov 2>{%04d" s ;
+ Format.fprintf fmt "@[<hv 0>{%04d" s ;
Ranges.iteri
(fun (rg : range) ->
Format.fprintf fmt "@ | %a: %a" Ranges.pp_range rg pp_node rg.data
) rg ;
- Format.fprintf fmt " }@]"
+ Format.fprintf fmt "@ }@]"
+
+let pp_region fmt (n: node) (m: region) =
+ begin
+ let acs r s = if Access.Set.is_empty s then '-' else r in
+ Format.fprintf fmt "@[<hov 2>%a: %c%c%c" pp_node n
+ (acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ;
+ List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (types m) ;
+ List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ;
+ if Options.debug_atleast 1 then
+ begin
+ Access.Set.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ;
+ Access.Set.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ;
+ Access.Set.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ;
+ end ;
+ Format.fprintf fmt "@ %a ;@]" pp_layout m.layout ;
+ end
(* -------------------------------------------------------------------------- *)
(* --- Constructors --- *)
@@ -82,10 +118,6 @@ let copy m = {
index = m.index ;
}
-let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_) -> s
-let points_to = function Blob | Compound _ -> None | Cell(_,p) -> p
-let ranges = function Blob | Cell _ -> [] | Compound(_,R rs) -> rs
-
let empty = {
parents = [] ;
roots = [] ;
@@ -242,8 +274,8 @@ let merge_region (m: map) (q: queue) (a : region) (b : region) : region = {
parents = nodes m (Store.bag a.parents b.parents) ;
roots = Store.bag a.roots b.roots ;
reads = Access.Set.union a.reads b.reads ;
- writes = Access.Set.union a.reads b.writes ;
- shifts = Access.Set.union a.reads b.shifts ;
+ writes = Access.Set.union a.writes b.writes ;
+ shifts = Access.Set.union a.shifts b.shifts ;
layout = merge_layout m q a.layout b.layout ;
}
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 01d1f63e3af..f3a03a5417c 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -41,9 +41,11 @@ type region = private {
val sizeof : layout -> int
val points_to : layout -> node option
val ranges : layout -> node Ranges.range list
+val types : region -> typ list
val pp_node : Format.formatter -> node -> unit
val pp_layout : Format.formatter -> layout -> unit
+val pp_region : Format.formatter -> node -> region -> unit
type map
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 8f1e8f634a9..b14918e442d 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -71,12 +71,19 @@ struct
"sizeof", Jnumber ;
"ranges", Ranges.jtype ;
"pointsTo", NodeOpt.jtype ;
+ "reads", Jboolean ;
+ "writes", Jboolean ;
+ "shifts", Jboolean ;
+ "types", Jarray Kernel_ast.Marker.jtype ;
]
let roots_to_json vs =
let open Cil_types in
Json.of_list @@ List.map (fun v -> Json.of_string v.vname) vs
+ let typ_to_json typ =
+ Kernel_ast.Marker.to_json @@ Printer_tag.PType typ
+
let to_json (m: Memory.region) =
Json.of_fields [
"roots", roots_to_json m.roots ;
@@ -84,6 +91,10 @@ struct
"sizeof", Json.of_int @@ Memory.sizeof m.layout ;
"ranges", Ranges.to_json @@ Memory.ranges m.layout ;
"pointsTo", NodeOpt.to_json @@ Memory.points_to m.layout ;
+ "reads", Json.of_bool @@ not @@ Access.Set.is_empty m.reads ;
+ "writes", Json.of_bool @@ not @@ Access.Set.is_empty m.writes ;
+ "shifts", Json.of_bool @@ not @@ Access.Set.is_empty m.shifts ;
+ "types", Json.of_list @@ List.map typ_to_json @@ Memory.types m ;
]
let of_json _ = failwith "Region.Layout.of_json"
end
--
GitLab