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

[region/ivette] report on singleton & typed

parent dec786ea
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ivette/src/frama-c/plugins/region/memory.tsx
+ 4
− 6
View file @ d9fdf572
...@@ -70,7 +70,7 @@ function makeDiagram(regions: readonly Region.region[]): Diagram { ...@@ -70,7 +70,7 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
const id = `n${r.node}`; const id = `n${r.node}`;
// --- Color // --- Color
const color = const color =
r.bytes ? 'red' : !r.typed ? 'red' :
r.pointed !== undefined r.pointed !== undefined
? (r.writes ? 'orange' : 'yellow') ? (r.writes ? 'orange' : 'yellow')
: (r.writes && r.reads) ? 'green' : : (r.writes && r.reads) ? 'green' :
...@@ -81,19 +81,17 @@ function makeDiagram(regions: readonly Region.region[]): Diagram { ...@@ -81,19 +81,17 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
const shape = cells.length > 0 ? cells : undefined; const shape = cells.length > 0 ? cells : undefined;
nodes.push({ id, font, color, label: r.label, title: r.title, shape }); nodes.push({ id, font, color, label: r.label, title: r.title, shape });
// --- Labels // --- Labels
const L: Dot.Node = const L: Dot.Node = { id: '', shape: 'note', font: 'mono' };
{ id: '', shape: 'note', font: 'mono' };
r.labels.forEach(a => { r.labels.forEach(a => {
const lid = `L${a}`; const lid = `L${a}`;
nodes.push({ ...L, id: lid, label: `${a}:` }); nodes.push({ ...L, id: lid, label: `${a}:` });
edges.push({ edges.push({
source: lid, target: id, aligned: true, source: lid, target: id, aligned: true,
headAnchor: 'n', head: 'none', color: 'grey' headAnchor: 's', head: 'none', color: 'grey'
}); });
}); });
// --- Roots // --- Roots
const R: Dot.Node = const R: Dot.Node = { id: '', shape: 'cds', font: 'mono' };
{ id: '', shape: 'cds', font: 'mono' };
r.roots.forEach(x => { r.roots.forEach(x => {
const xid = `X${x}`; const xid = `X${x}`;
nodes.push({ ...R, id: xid, label: x }); nodes.push({ ...R, id: xid, label: x });
......
src/plugins/region/memory.ml
+ 140
− 121
View file @ d9fdf572
...@@ -66,11 +66,11 @@ type map = { ...@@ -66,11 +66,11 @@ type map = {
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_,_) -> s let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_,_) -> s
let ranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs let cranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs
let fields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds let cfields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds
let pointed = function Blob | Compound _ -> None | Cell(_,p) -> p let cpointed = function Blob | Compound _ -> None | Cell(_,p) -> p
let types (m : chunk) : typ list = let ctypes (m : chunk) : typ list =
let pool = ref Typ.Set.empty in let pool = ref Typ.Set.empty in
let add acs = let add acs =
pool := Typ.Set.add (Cil.unrollType @@ Access.typeof acs) !pool in pool := Typ.Set.add (Cil.unrollType @@ Access.typeof acs) !pool in
...@@ -111,7 +111,7 @@ let pp_chunk fmt (n: node) (m: chunk) = ...@@ -111,7 +111,7 @@ let pp_chunk fmt (n: node) (m: chunk) =
let acs r s = if Access.Set.is_empty s then '-' else r in 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 Format.fprintf fmt "@[<hov 2>%a: %c%c%c" pp_node n
(acs 'R' m.creads) (acs 'W' m.cwrites) (acs 'A' m.cshifts) ; (acs 'R' m.creads) (acs 'W' m.cwrites) (acs 'A' m.cshifts) ;
List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (types m) ; List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (ctypes m) ;
Lset.iter (Format.fprintf fmt "@ %s:") m.clabels ; Lset.iter (Format.fprintf fmt "@ %s:") m.clabels ;
Vset.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.croots ; Vset.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.croots ;
if Options.debug_atleast 1 then if Options.debug_atleast 1 then
...@@ -221,117 +221,6 @@ let add_label (m: map) a = ...@@ -221,117 +221,6 @@ let add_label (m: map) a =
(* --- Iterator --- *) (* --- Iterator --- *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
type range = {
label: string ; (* pretty printed fields *)
offset: int ;
length: int ;
cells: int ;
data: node ;
}
type region = {
node: node ;
parents: node list ;
roots: varinfo list ;
labels: string list ;
types: typ list ;
fields: Fields.domain ;
reads: Access.acs list ;
writes: Access.acs list ;
shifts: Access.acs list ;
sizeof: int ;
ranges: range list ;
pointed: node option ;
}
let pp_cells fmt = function
| 1 -> ()
| 0 -> Format.fprintf fmt "[…]"
| n -> Format.fprintf fmt "[%d]" n
type slice =
| Padding of int
| Range of range
let pad p q s =
let n = q - p in
if n > 0 then Padding n :: s else s
let rec span k s = function
| [] -> pad k s []
| r::rs -> pad k r.offset @@ Range r :: span (r.offset + r.length) s rs
let pp_slice fields fmt = function
| Padding n ->
Format.fprintf fmt "@ %a;" Fields.pp_bits n
| Range r ->
Format.fprintf fmt "@ %t: %a%a;"
(Fields.pslice ~fields ~offset:r.offset ~length:r.length)
pp_node r.data
pp_cells r.cells
let pp_range fmt (r: range) =
Format.fprintf fmt "@ %d..%d: %a%a;"
r.offset (r.offset + r.length) pp_node r.data pp_cells r.cells
let pp_region fmt (m: region) =
begin
let acs r s = if s = [] then '-' else r in
Format.fprintf fmt "@[<hov 2>%a: %c%c%c"
pp_node m.node
(acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ;
List.iter (Format.fprintf fmt "@ %s:") m.labels ;
List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ;
List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) m.types ;
Format.fprintf fmt "@ %db" m.sizeof ;
Option.iter (Format.fprintf fmt "@ (*%a)" pp_node) m.pointed ;
if m.ranges <> [] then
begin
Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ;
if Options.debug_atleast 1 then
List.iter (pp_range fmt) m.ranges
else
List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ;
Format.fprintf fmt "@]@ }@]" ;
end ;
if Options.debug_atleast 1 then
begin
List.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ;
List.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ;
List.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ;
end ;
Format.fprintf fmt " ;@]" ;
end
let make_range (m: map) fields Ranges.{ length ; offset ; data } : range =
let s = sizeof (get m data).clayout in
let p = Fields.pslice ~fields ~offset ~length in
{
label = Format.asprintf "%t" p ;
offset ; length ;
cells = if s = 0 then 0 else length / s ;
data = node m data ;
}
let make_region (m: map) (n: node) (r: chunk) : region =
let types = types r in
let sizeof = sizeof r.clayout in
let fields = fields r.clayout in
{
node = n ;
parents = nodes m r.cparents ;
roots = Vset.elements r.croots ;
labels = Lset.elements r.clabels ;
reads = Access.Set.elements r.creads ;
writes = Access.Set.elements r.cwrites ;
shifts = Access.Set.elements r.cshifts ;
types ; sizeof ; fields ;
ranges = List.map (make_range m fields) (ranges r.clayout) ;
pointed = Option.map (node m) (pointed r.clayout) ;
}
let region map n = make_region map n (get map n)
let rec walk h m (f: node -> unit) n = let rec walk h m (f: node -> unit) n =
let n = Ufind.find m.store n in let n = Ufind.find m.store n in
let id = Store.id n in let id = Store.id n in
...@@ -348,11 +237,6 @@ let iter (m:map) (f: node -> unit) = ...@@ -348,11 +237,6 @@ let iter (m:map) (f: node -> unit) =
let h = Hashtbl.create 0 in let h = Hashtbl.create 0 in
Vmap.iter (fun _x n -> walk h m f n) m.roots Vmap.iter (fun _x n -> walk h m f n) m.roots
let regions map =
let pool = ref [] in
iter map (fun r -> pool := region map r :: !pool) ;
List.rev !pool
let size (m: map) (r: node) = let size (m: map) (r: node) =
sizeof (Ufind.get m.store r).clayout sizeof (Ufind.get m.store r).clayout
...@@ -665,6 +549,8 @@ let shifts (m:map) (r:node) = ...@@ -665,6 +549,8 @@ let shifts (m:map) (r:node) =
let node = Ufind.get m.store r in let node = Ufind.get m.store r in
List.map Access.typeof @@ Access.Set.elements node.cshifts List.map Access.typeof @@ Access.Set.elements node.cshifts
let types (m:map) (r:node) = ctypes @@ Ufind.get m.store r
let typed (m:map) (r:node) = let typed (m:map) (r:node) =
let types = ref None in let types = ref None in
let node = Ufind.get m.store r in let node = Ufind.get m.store r in
...@@ -682,3 +568,136 @@ let typed (m:map) (r:node) = ...@@ -682,3 +568,136 @@ let typed (m:map) (r:node) =
Access.Set.iter check node.cshifts ; Access.Set.iter check node.cshifts ;
!types !types
with Exit -> None with Exit -> None
(* -------------------------------------------------------------------------- *)
(* --- High-Level API --- *)
(* -------------------------------------------------------------------------- *)
type range = {
label: string ; (* pretty printed fields *)
offset: int ;
length: int ;
cells: int ;
data: node ;
}
type region = {
node: node ;
parents: node list ;
roots: varinfo list ;
labels: string list ;
types: typ list ;
typed : typ option ;
fields: Fields.domain ;
reads: Access.acs list ;
writes: Access.acs list ;
shifts: Access.acs list ;
sizeof: int ;
singleton : bool ;
ranges: range list ;
pointed: node option ;
}
let make_range (m: map) fields Ranges.{ length ; offset ; data } : range =
let s = sizeof (get m data).clayout in
let p = Fields.pslice ~fields ~offset ~length in
{
label = Format.asprintf "%t" p ;
offset ; length ;
cells = if s = 0 then 0 else length / s ;
data = node m data ;
}
let ranges (m:map) (r:node) =
let node = Ufind.get m.store r in
let fields = cfields node.clayout in
List.map (make_range m fields) (cranges node.clayout)
let make_region (m: map) (n: node) (r: chunk) : region =
let types = ctypes r in
let typed = typed m n in
let sizeof = sizeof r.clayout in
let fields = cfields r.clayout in
let singleton = singleton m n in
{
node = n ;
parents = nodes m r.cparents ;
roots = Vset.elements r.croots ;
labels = Lset.elements r.clabels ;
reads = Access.Set.elements r.creads ;
writes = Access.Set.elements r.cwrites ;
shifts = Access.Set.elements r.cshifts ;
ranges = List.map (make_range m fields) (cranges r.clayout) ;
pointed = Option.map (node m) (cpointed r.clayout) ;
types ; typed ; singleton ; sizeof ; fields ;
}
let region map n = make_region map n (get map n)
let regions map =
let pool = ref [] in
iter map (fun r -> pool := region map r :: !pool) ;
List.rev !pool
(* -------------------------------------------------------------------------- *)
(* --- Pretty Printers --- *)
(* -------------------------------------------------------------------------- *)
let pp_cells fmt = function
| 1 -> ()
| 0 -> Format.fprintf fmt "[…]"
| n -> Format.fprintf fmt "[%d]" n
type slice =
| Padding of int
| Range of range
let pad p q s =
let n = q - p in
if n > 0 then Padding n :: s else s
let rec span k s = function
| [] -> pad k s []
| r::rs -> pad k r.offset @@ Range r :: span (r.offset + r.length) s rs
let pp_slice fields fmt = function
| Padding n ->
Format.fprintf fmt "@ %a;" Fields.pp_bits n
| Range r ->
Format.fprintf fmt "@ %t: %a%a;"
(Fields.pslice ~fields ~offset:r.offset ~length:r.length)
pp_node r.data
pp_cells r.cells
let pp_range fmt (r: range) =
Format.fprintf fmt "@ %d..%d: %a%a;"
r.offset (r.offset + r.length) pp_node r.data pp_cells r.cells
let pp_region fmt (m: region) =
begin
let acs r s = if s = [] then '-' else r in
Format.fprintf fmt "@[<hov 2>%a: %c%c%c"
pp_node m.node
(acs 'R' m.reads) (acs 'W' m.writes) (acs 'A' m.shifts) ;
List.iter (Format.fprintf fmt "@ %s:") m.labels ;
List.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.roots ;
List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) m.types ;
Format.fprintf fmt "@ %db" m.sizeof ;
Option.iter (Format.fprintf fmt "@ (*%a)" pp_node) m.pointed ;
if m.ranges <> [] then
begin
Format.fprintf fmt "@ @[<hv 0>@[<hv 2>{" ;
if Options.debug_atleast 1 then
List.iter (pp_range fmt) m.ranges
else
List.iter (pp_slice m.fields fmt) (span 0 m.sizeof m.ranges) ;
Format.fprintf fmt "@]@ }@]" ;
end ;
if Options.debug_atleast 1 then
begin
List.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.reads ;
List.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.writes ;
List.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.shifts ;
end ;
Format.fprintf fmt " ;@]" ;
end
src/plugins/region/memory.mli
+ 4
− 0
View file @ d9fdf572
...@@ -38,11 +38,13 @@ type region = { ...@@ -38,11 +38,13 @@ type region = {
roots: varinfo list ; roots: varinfo list ;
labels: string list ; labels: string list ;
types: typ list ; types: typ list ;
typed : typ option ;
fields: Fields.domain ; fields: Fields.domain ;
reads: Access.acs list ; reads: Access.acs list ;
writes: Access.acs list ; writes: Access.acs list ;
shifts: Access.acs list ; shifts: Access.acs list ;
sizeof: int ; sizeof: int ;
singleton : bool ;
ranges: range list ; ranges: range list ;
pointed: node option ; pointed: node option ;
} }
...@@ -100,6 +102,7 @@ val index : map -> node -> typ -> node ...@@ -100,6 +102,7 @@ val index : map -> node -> typ -> node
val lval : map -> lval -> node val lval : map -> lval -> node
val exp : map -> exp -> node option val exp : map -> exp -> node option
val ranges : map -> node -> range list
val points_to : map -> node -> node option val points_to : map -> node -> node option
val pointed_by : map -> node -> node list val pointed_by : map -> node -> node list
...@@ -110,4 +113,5 @@ val singleton : map -> node -> bool ...@@ -110,4 +113,5 @@ val singleton : map -> node -> bool
val reads : map -> node -> typ list val reads : map -> node -> typ list
val writes : map -> node -> typ list val writes : map -> node -> typ list
val shifts : map -> node -> typ list val shifts : map -> node -> typ list
val types : map -> node -> typ list
val typed : map -> node -> typ option val typed : map -> node -> typ option
src/plugins/region/services.ml
+ 11
− 4
View file @ d9fdf572
...@@ -114,6 +114,7 @@ struct ...@@ -114,6 +114,7 @@ struct
let label (m: Memory.region) = let label (m: Memory.region) =
let buffer = Buffer.create 4 in let buffer = Buffer.create 4 in
if m.singleton then Buffer.add_string buffer "!" ;
if m.reads <> [] then Buffer.add_char buffer 'R' ; if m.reads <> [] then Buffer.add_char buffer 'R' ;
if m.writes <> [] then Buffer.add_char buffer 'W' ; if m.writes <> [] then Buffer.add_char buffer 'W' ;
if m.pointed <> None then Buffer.add_char buffer '*' if m.pointed <> None then Buffer.add_char buffer '*'
...@@ -133,7 +134,7 @@ struct ...@@ -133,7 +134,7 @@ struct
Typ.pretty fmt ty Typ.pretty fmt ty
let title (m: Memory.region) = let title (m: Memory.region) =
Format.asprintf "%t (%db)" Format.asprintf "%t (%db)%t"
begin fun fmt -> begin fun fmt ->
match m.types with match m.types with
| [] -> Format.pp_print_string fmt "Compound" | [] -> Format.pp_print_string fmt "Compound"
...@@ -141,7 +142,11 @@ struct ...@@ -141,7 +142,11 @@ struct
| ty::ts -> | ty::ts ->
pp_typ_layout 0 fmt ty ; pp_typ_layout 0 fmt ty ;
List.iter (Format.fprintf fmt ", %a" (pp_typ_layout 0)) ts ; List.iter (Format.fprintf fmt ", %a" (pp_typ_layout 0)) ts ;
end m.sizeof end
m.sizeof
begin fun fmt ->
if m.singleton then Format.pp_print_string fmt " (singleton)"
end
let jtype = Data.declare ~package ~name:"region" @@ let jtype = Data.declare ~package ~name:"region" @@
Jrecord [ Jrecord [
...@@ -154,7 +159,8 @@ struct ...@@ -154,7 +159,8 @@ struct
"pointed", NodeOpt.jtype ; "pointed", NodeOpt.jtype ;
"reads", Jboolean ; "reads", Jboolean ;
"writes", Jboolean ; "writes", Jboolean ;
"bytes", Jboolean ; "typed", Jboolean ;
"singleton", Jboolean ;
"label", Jstring ; "label", Jstring ;
"title", Jstring ; "title", Jstring ;
] ]
...@@ -170,7 +176,8 @@ struct ...@@ -170,7 +176,8 @@ struct
"pointed", NodeOpt.to_json @@ m.pointed ; "pointed", NodeOpt.to_json @@ m.pointed ;
"reads", Json.of_bool (m.reads <> []) ; "reads", Json.of_bool (m.reads <> []) ;
"writes", Json.of_bool (m.writes <> []) ; "writes", Json.of_bool (m.writes <> []) ;
"bytes", Json.of_bool (List.length m.types > 1) ; "typed", Json.of_bool (m.typed <> None) ;
"singleton", Json.of_bool m.singleton ;
"label", Json.of_string @@ label m ; "label", Json.of_string @@ label m ;
"title", Json.of_string @@ title m ; "title", Json.of_string @@ title m ;
] ]
......
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