diff --git a/ivette/src/dome/renderer/graph/diagram.tsx b/ivette/src/dome/renderer/graph/diagram.tsx
index ec0325a9dcc403b3da70add407567c299832114e..291f0a79f4f7bedce638fdcdd7fc7c85ae838d08 100644
--- a/ivette/src/dome/renderer/graph/diagram.tsx
+++ b/ivette/src/dome/renderer/graph/diagram.tsx
@@ -310,7 +310,7 @@ class Builder {
// --- Attributes
escaped(a: string): Builder {
- return this.print(a.split('"').join('\\"'));
+ return this.print(a.replace(/["{}|]/g, '\\$&'));
}
value(a: string | number | boolean): Builder {
diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index 5d01bdbe22ac529ecefaa43e5a11963c12441397..b673d00679bc0bbb0f86d4783451aa7409a0062b 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -66,11 +66,13 @@ export const byNode: Compare.Order<node> = Compare.number;
export const nodeDefault: node = Json.jIndex<'#node'>('#node')(-1);
export type range =
- { offset: number, length: number, cells: number, data: node };
+ { label: string, offset: number, length: number, cells: number, data: node
+ };
/** Decoder for `range` */
export const jRange: Json.Decoder<range> =
Json.jObject({
+ label: Json.jString,
offset: Json.jNumber,
length: Json.jNumber,
cells: Json.jNumber,
@@ -80,7 +82,9 @@ export const jRange: Json.Decoder<range> =
/** Natural order for `range` */
export const byRange: Compare.Order<range> =
Compare.byFields
- <{ offset: number, length: number, cells: number, data: node }>({
+ <{ label: string, offset: number, length: number, cells: number,
+ data: node }>({
+ label: Compare.string,
offset: Compare.number,
length: Compare.number,
cells: Compare.number,
@@ -89,7 +93,7 @@ export const byRange: Compare.Order<range> =
/** Default value for `range` */
export const rangeDefault: range =
- { offset: 0, length: 0, cells: 0, data: nodeDefault };
+ { label: '', offset: 0, length: 0, cells: 0, data: nodeDefault };
export type region =
{ node: node, roots: string[], labels: string[], parents: node[],
@@ -166,34 +170,26 @@ const regions_internal: Server.GetRequest<decl,region[]> = {
/** Returns computed regions for the given declaration */
export const regions: Server.GetRequest<decl,region[]>= regions_internal;
-const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = {
+const regionsAt_internal: Server.GetRequest<marker,region[]> = {
kind: Server.RqKind.GET,
name: 'plugins.region.regionsAt',
- input: Json.jPair( jMarker, Json.jBoolean,),
+ input: jMarker,
output: Json.jArray(jRegion),
fallback: [],
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Compute regions at the given marker */
-export const regionsAt: Server.GetRequest<[ marker, boolean ],region[]>= regionsAt_internal;
-
-const localize_internal: Server.GetRequest<
- [ marker, boolean ],
- node |
- undefined
- > = {
+/** Compute regions at the given marker program point */
+export const regionsAt: Server.GetRequest<marker,region[]>= regionsAt_internal;
+
+const localize_internal: Server.GetRequest<marker,node | undefined> = {
kind: Server.RqKind.GET,
name: 'plugins.region.localize',
- input: Json.jPair( jMarker, Json.jBoolean,),
+ input: jMarker,
output: Json.jOption(jNode),
fallback: undefined,
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Localize in the local (true) or global map (false) */
-export const localize: Server.GetRequest<
- [ marker, boolean ],
- node |
- undefined
- >= localize_internal;
+/** Localize the marker in its map */
+export const localize: Server.GetRequest<marker,node | undefined>= localize_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx
index eed8bea5b81bb105826aaab9a9c1e05b85593f5a..b5faa2a37f188475eda35a31e74a5f6aead76ef9 100644
--- a/ivette/src/frama-c/plugins/region/index.tsx
+++ b/ivette/src/frama-c/plugins/region/index.tsx
@@ -43,9 +43,11 @@ function RegionAnalys(): JSX.Element {
const [pinned, setPinned] = React.useState(false);
const [running, setRunning] = React.useState(false);
const setComputing = Dome.useProtected(setRunning);
- const scope = States.useCurrentScope();
+ const { scope, marker } = States.useCurrentLocation();
const { kind, name } = States.useDeclaration(scope);
const regions = States.useRequestStable(Region.regions, kf);
+ const node = States.useRequestStable(Region.localize, marker);
+ const { descr: label } = States.useMarker(marker);
React.useEffect(() => {
if (!pinned && kind === 'FUNCTION' && scope !== kf) {
setKf(scope);
@@ -84,7 +86,7 @@ function RegionAnalys(): JSX.Element {
onClick={() => setPinned(!pinned)}
/>
</Tools.ToolBar>
- <MemoryView regions={regions} />
+ <MemoryView regions={regions} node={node} label={label} />
</>
);
}
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index a59a4adac95021d3e17cd48d6e10cb0e9aceb15f..2b38fe1acbe532113a27f458bb0a43fe2a30c023 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -40,23 +40,27 @@ function makeRecord(
ranges.forEach((rg, i) => {
const port = `r${i}`;
const target = `n${rg.data}`;
- edges.push({ source, sourcePort: port, target });
+ edges.push({
+ source, sourcePort: port, target,
+ head: 'none', line: 'dashed'
+ });
if (offset !== rg.offset)
- cells.push(`${offset}..${rg.offset - 1} ##`);
+ cells.push(`#${rg.offset - offset}b`);
offset = rg.offset + rg.length;
- cells.push({
- label: `${rg.offset}..${offset - 1} [${rg.cells}]`,
- port,
- });
+ const label =
+ rg.cells < 1 ? `${rg.label} […]` :
+ rg.cells > 1 ? `${rg.label} [${rg.cells}]` :
+ rg.label;
+ cells.push({ label, port });
});
if (offset !== sizeof)
- cells.push(`${offset}..${sizeof - 1} ##`);
+ cells.push(`#${sizeof-offset}b`);
return cells;
}
interface Diagram {
- nodes: Dot.Node[];
- edges: Dot.Edge[];
+ nodes: readonly Dot.Node[];
+ edges: readonly Dot.Edge[];
}
function makeDiagram(regions: readonly Region.region[]): Diagram {
@@ -82,7 +86,10 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
r.labels.forEach(a => {
const lid = `L${a}`;
nodes.push({ ...L, id: lid, label: `${a}:` });
- edges.push({ source: lid, aligned: true, head: 'tee', target: id });
+ edges.push({
+ source: lid, target: id, aligned: true,
+ headAnchor: 'n', head: 'none', color: 'grey'
+ });
});
// --- Roots
const R: Dot.Node =
@@ -90,22 +97,37 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
r.roots.forEach(x => {
const xid = `X${x}`;
nodes.push({ ...R, id: xid, label: x });
- edges.push({ source: xid, headAnchor: "e", target: id });
+ edges.push({
+ source: xid, target: id,
+ headAnchor: "e", head: 'none', color: 'grey'
+ });
});
// --- Pointed
if (r.pointed !== undefined) {
const pid = `n${r.pointed}`;
- edges.push({ source: id, target: pid, head: 'dot', color: 'orange' });
+ edges.push({ source: id, target: pid });
}
});
return { nodes, edges };
}
-function addSelected(d: Diagram, label: string, node: Region.node): void {
- d.nodes.push({
- id: 'Selected', label, title: "Selected Marker", shape: 'note'
- });
- d.edges.push({ source: 'Selected', target: `n${node}` });
+function addSelected(
+ diag: Diagram,
+ node: Region.node | undefined,
+ label: string | undefined
+): Diagram {
+ if (node && label) {
+ const nodes = diag.nodes.concat({
+ id: 'Selected', label, title: "Selected Marker",
+ shape: 'note', color: 'selected'
+ });
+ const edges = diag.edges.concat({
+ source: 'Selected', target: `n${node}`, aligned: true,
+ headAnchor: 's', tailAnchor: 'n',
+ });
+ return { nodes, edges };
+ } else
+ return diag;
}
export interface MemoryViewProps {
@@ -116,9 +138,12 @@ export interface MemoryViewProps {
export function MemoryView(props: MemoryViewProps): JSX.Element {
const { regions = [], label, node } = props;
- const diagram = React.useMemo(() => makeDiagram(regions), [regions]);
- if (label && node) addSelected(diagram, label, node);
- return <Dot.Diagram {...diagram} />;
+ const baseDiagram = React.useMemo(() => makeDiagram(regions), [regions]);
+ const fullDiagram = React.useMemo(
+ () => addSelected(baseDiagram, node, label),
+ [baseDiagram, node, label]
+ );
+ return <Dot.Diagram {...fullDiagram} />;
}
// --------------------------------------------------------------------------
diff --git a/src/libraries/utils/json.mli b/src/libraries/utils/json.mli
index 228b4bdf3f3f1817c9841400f58f219a38471786..2525c0cfd4558aa490462565e51286a4c877b4c3 100644
--- a/src/libraries/utils/json.mli
+++ b/src/libraries/utils/json.mli
@@ -64,7 +64,8 @@ val of_string : string -> t
val of_float : float -> t
val of_list : t list -> t
val of_array : t array -> t
-val of_fields : (string * t) list -> t
+val of_fields : (string * t) list -> t (** Filers out null fields *)
+val of_option : ('a -> t) -> 'a option -> t (** Maps none to null *)
(** {2 Parsers} *)
diff --git a/src/libraries/utils/json.mll b/src/libraries/utils/json.mll
index f5edcc2b636728c81b59b92c8e57a6a63e5d0b0e..fd68888480113a1ec35238250fbb8b49f830d90f 100644
--- a/src/libraries/utils/json.mll
+++ b/src/libraries/utils/json.mll
@@ -288,14 +288,17 @@ let fold f v w = match v with
| `Assoc fs -> List.fold_left (fun w (e,v) -> f e v w) w fs
| _ -> invalid "fold"
+let is_defined = function `Null -> false | _ -> true
+let is_field (_,v) = is_defined v
+
let of_bool b = `Bool b
let of_int k = `Int k
let of_string s = `String s
let of_float f = `Float f
let of_list xs = `List xs
let of_array xs = `List (Array.to_list xs)
-let of_fields m = `Assoc m
-
+let of_fields m = `Assoc (List.filter is_field m)
+let of_option f = function None -> `Null | Some v -> f v
(* JSON file cache and merging *)
diff --git a/src/plugins/region/fields.ml b/src/plugins/region/fields.ml
new file mode 100644
index 0000000000000000000000000000000000000000..baab8fda06ecfc8bd85fe293dcbf165c12cfd60b
--- /dev/null
+++ b/src/plugins/region/fields.ml
@@ -0,0 +1,97 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Ranges
+open Cil_types
+module Domain = Cil_datatype.Compinfo.Set
+
+type field = fieldinfo range
+
+type domain = Domain.t (* support for associating offsets to field name *)
+let iter = Domain.iter
+let union = Domain.union
+let empty = Domain.empty
+let singleton (fd : fieldinfo) = Domain.singleton fd.fcomp
+
+(* minimal offset first, then minimal length, then largest struct *)
+let compare (a : field) (b : field) =
+ let cmp = a.offset - b.offset in
+ if cmp <> 0 then cmp else
+ let cmp = a.length - b.length in
+ if cmp <> 0 then cmp else
+ let sa = Cil.bitsSizeOf (TComp(a.data.fcomp,[])) in
+ let sb = Cil.bitsSizeOf (TComp(b.data.fcomp,[])) in
+ sb - sa
+
+let find_all (fields: domain) (rg : _ range) =
+ List.sort compare @@
+ Domain.fold
+ (fun c fds ->
+ List.fold_left
+ (fun fds fd ->
+ let ofs,len = Cil.fieldBitsOffset fd in
+ if rg.offset <= ofs && ofs + len <= rg.offset + rg.length then
+ { offset = ofs ; length = len ; data = fd } :: fds
+ else
+ fds
+ ) fds @@
+ Option.value ~default:[] c.cfields
+ ) fields []
+
+let find fields rg =
+ match find_all fields rg with
+ | [] -> None
+ | fr::_ -> Some fr
+
+type slice = Bits of int | Field of fieldinfo
+
+let pp_bits fmt n =
+ if n <> 0 then Format.fprintf fmt "#%db" n
+
+let pp_slice fmt = function
+ | Bits n -> pp_bits fmt n
+ | Field fd -> Format.fprintf fmt ".%s" fd.fname
+
+let pad p q s =
+ let n = q - p in
+ if n > 0 then Bits n :: s else s
+
+let last (rg : _ range) = rg.offset + rg.length
+
+let span fields rg =
+ match find_all fields rg with
+ | [] -> [Bits rg.length]
+ | fr :: frs ->
+ pad rg.offset fr.offset @@
+ Field fr.data ::
+ let p = last fr in
+ let q = last rg in
+ match List.rev @@ List.filter (fun r -> p <= r.offset) frs with
+ | [] -> pad p q []
+ | lr :: _ ->
+ pad p lr.offset @@ Field lr.data :: pad (last lr) q []
+
+let pretty fields fmt rg =
+ List.iter (pp_slice fmt) @@ span fields rg
+
+let pslice fmt ~fields ~offset ~length =
+ List.iter (pp_slice fmt) @@ span fields { offset ; length ; data = () }
diff --git a/src/plugins/region/fields.mli b/src/plugins/region/fields.mli
new file mode 100644
index 0000000000000000000000000000000000000000..4e1bbdd73092c2dd843125300dca0ca736753566
--- /dev/null
+++ b/src/plugins/region/fields.mli
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Ranges
+open Cil_types
+
+type domain
+type field = fieldinfo range
+type slice = Bits of int | Field of fieldinfo
+
+val empty : domain
+val singleton : fieldinfo -> domain
+val union : domain -> domain -> domain
+val iter : (compinfo -> unit) -> domain -> unit
+val compare : field -> field -> int
+val find_all : domain -> 'a range -> field list
+val find : domain -> 'a range -> field option
+val span : domain -> 'a range -> slice list
+
+val pp_bits : Format.formatter -> int -> unit
+val pp_slice : Format.formatter -> slice -> unit
+
+val pretty : domain -> Format.formatter -> 'a range -> unit
+val pslice : Format.formatter -> fields:domain -> offset:int -> length:int -> unit
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
index 2ceca06655fada23fd1b4a5925b939e328c98113..48729ec3b6745770588ece376239f05b9ce9d628 100644
--- a/src/plugins/region/memory.ml
+++ b/src/plugins/region/memory.ml
@@ -39,7 +39,7 @@ type node = chunk Ufind.rref
and layout =
| Blob
| Cell of int * node option
- | Compound of int * node Ranges.t
+ | Compound of int * Fields.domain * node Ranges.t
and chunk = {
cparents: node list ;
@@ -64,8 +64,9 @@ type map = {
(* --- Accessors --- *)
(* -------------------------------------------------------------------------- *)
-let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_) -> s
-let ranges = function Blob | Cell _ -> [] | Compound(_,R rs) -> rs
+let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_,_) -> s
+let ranges = function Blob | Cell _ -> [] | Compound(_,_,R rs) -> rs
+let fields = function Blob | Cell _ -> Fields.empty | Compound(_,fds,_) -> fds
let pointed = function Blob | Compound _ -> None | Cell(_,p) -> p
let types (m : chunk) : typ list =
@@ -88,15 +89,19 @@ let unlock m = m.locked <- false
let pp_node fmt (n : node) = Format.fprintf fmt "R%04x" @@ Store.id n
+let pp_field fields fmt fd =
+ if Options.debug_atleast 1 then Ranges.pp_range fmt fd else
+ Fields.pretty fields fmt fd
+
let pp_layout fmt = function
| Blob -> Format.pp_print_string fmt "<blob>"
| Cell(s,None) -> Format.fprintf fmt "<%04d>" s
| Cell(s,Some n) -> Format.fprintf fmt "<%04d>(*%a)" s pp_node n
- | Compound(s,rg) ->
+ | Compound(s,fields,rg) ->
Format.fprintf fmt "@[<hv 0>{%04d" s ;
Ranges.iteri
(fun (rg : rg) ->
- Format.fprintf fmt "@ | %a: %a" Ranges.pp_range rg pp_node rg.data
+ Format.fprintf fmt "@ | %a: %a" (pp_field fields) rg pp_node rg.data
) rg ;
Format.fprintf fmt "@ }@]"
@@ -179,12 +184,13 @@ let new_chunk (m: map) ?(size=0) ?ptr () =
| Some _ -> Cell(Ranges.gcd size Cil.(bitsSizeOf voidPtrType), ptr)
in Ufind.make m.store { empty with clayout }
-let new_range (m: map) ~size ~offset ~length ~data : node =
+let new_range (m: map) ?(fields=Fields.empty) ~size ~offset ~length data : node =
failwith_locked m "Region.Memory.new_range" ;
let last = offset + length in
if not (0 <= offset && offset < last && last <= size) then
raise (Invalid_argument "Region.Memory.add_range") ;
- let clayout = Compound(size, Ranges.singleton { offset ; length ; data }) in
+ let ranges = Ranges.singleton { offset ; length ; data } in
+ let clayout = Compound(size, fields, ranges) in
let n = Ufind.make m.store { empty with clayout } in
update m data (fun r -> { r with cparents = nodes m @@ n :: r.cparents }) ; n
@@ -207,6 +213,7 @@ let add_label (m: map) a =
(* -------------------------------------------------------------------------- *)
type range = {
+ label: string ; (* pretty printed fields *)
offset: int ;
length: int ;
cells: int ;
@@ -219,6 +226,7 @@ type region = {
roots: varinfo list ;
labels: string list ;
types: typ list ;
+ fields: Fields.domain ;
reads: Access.acs list ;
writes: Access.acs list ;
shifts: Access.acs list ;
@@ -227,9 +235,35 @@ type region = {
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 [%d]: %a"
- r.offset (r.offset + r.length) r.cells pp_node r.data
+ 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
@@ -242,9 +276,15 @@ let pp_region fmt (m: region) =
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 ;
- Format.fprintf fmt "@[<hv 0>" ;
- List.iter (Format.fprintf fmt "@ %a" pp_range) m.ranges ;
- Format.fprintf fmt "@]" ;
+ 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 ;
@@ -254,28 +294,31 @@ let pp_region fmt (m: region) =
Format.fprintf fmt " ;@]" ;
end
-let make_range (m: map) (rg: rg) : range =
- let s = sizeof (get m rg.data).clayout in
+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
{
- offset = rg.offset ;
- length = rg.length ;
- cells = if s = 0 then 0 else rg.length / s ;
- data = node m rg.data ;
+ 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 = {
- 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 = types r ;
- sizeof = sizeof r.clayout ;
- ranges = List.map (make_range m) @@ ranges r.clayout ;
- pointed = Option.map (node m) (pointed r.clayout) ;
-}
+let make_region (m: map) (n: node) (r: chunk) : region =
+ 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 = types r ;
+ sizeof = sizeof r.clayout ;
+ 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)
@@ -289,7 +332,7 @@ let rec walk h m f n =
match r.clayout with
| Blob -> ()
| Cell(_,p) -> Option.iter (walk h m f) p
- | Compound(_,rg) -> Ranges.iter (walk h m f) rg
+ | Compound(_,_,rg) -> Ranges.iter (walk h m f) rg
let iter (m:map) (f: region -> unit) =
let h = Hashtbl.create 0 in
@@ -335,16 +378,17 @@ let merge_range (m: map) (q: queue) (ra : rg) (rb : rg) : node =
merge_node m q (new_chunk m ~size ()) data
let merge_ranges (m: map) (q: queue)
- (sa : int) (wa : node Ranges.t)
- (sb : int) (wb : node Ranges.t)
+ (sa : int) (fa : Fields.domain) (wa : node Ranges.t)
+ (sb : int) (fb : Fields.domain) (wb : node Ranges.t)
: layout =
+ let fields = Fields.union fa fb in
if sa = sb then
- Compound(sa, Ranges.merge (merge_range m q) wa wb)
+ Compound(sa, fields, Ranges.merge (merge_range m q) wa wb)
else
let size = Ranges.gcd sa sb in
let ra = Ranges.squash (merge_node m q) wa in
let rb = Ranges.squash (merge_node m q) wb in
- Compound(size, singleton ~size @@ merge_opt m q ra rb)
+ Compound(size, fields, singleton ~size @@ merge_opt m q ra rb)
let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
match a, b with
@@ -352,16 +396,20 @@ let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
| Cell(sa,pa) , Cell(sb,pb) -> Cell(Ranges.gcd sa sb, merge_opt m q pa pb)
- | Compound(sa,wa), Compound(sb,wb) -> merge_ranges m q sa wa sb wb
+ | Compound(sa,fa,wa), Compound(sb,fb,wb) ->
+ merge_ranges m q sa fa wa sb fb wb
- | Compound(sr,wr), Cell(sx,None) | Cell(sx,None), Compound(sr,wr) ->
+ | Compound(sr,fr,wr), Cell(sx,None)
+ | Cell(sx,None), Compound(sr,fr,wr) ->
let size = Ranges.gcd sx sr in
- Compound(size, singleton ~size @@ Ranges.squash (merge_node m q) wr)
+ Compound(size, fr, singleton ~size @@ Ranges.squash (merge_node m q) wr)
- | Compound(sr,wr), Cell(sx,Some ptr) | Cell(sx,Some ptr), Compound(sr,wr) ->
+ | Compound(sr,fr,wr), Cell(sx,Some ptr)
+ | Cell(sx,Some ptr), Compound(sr,fr,wr) ->
let rp = new_chunk m ~size:sx ~ptr () in
+ let fx = Fields.empty in
let wx = Ranges.range ~length:sx rp in
- merge_ranges m q sx wx sr wr
+ merge_ranges m q sx fx wx sr fr wr
let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = {
cparents = nodes m @@ Store.bag a.cparents b.cparents ;
@@ -406,14 +454,15 @@ let add_field (m:map) (r:node) (fd:fieldinfo) : node =
let size = Cil.bitsSizeOf (TComp(ci,[])) in
let offset, length = Cil.fieldBitsOffset fd in
let rf = new_chunk m () in
- let rc = new_range m ~size ~offset ~length ~data:rf in
+ let fields = Fields.singleton fd in
+ let rc = new_range m ~fields ~size ~offset ~length rf in
ignore @@ merge m r rc ; rf
else r
let add_index (m:map) (r:node) (ty:typ) (n:int) : node =
let s = Cil.bitsSizeOf ty * n in
let re = new_chunk m () in
- let rc = new_range m ~size:s ~offset:0 ~length:s ~data:re in
+ let rc = new_range m ~size:s ~offset:0 ~length:s re in
ignore @@ merge m r rc ; re
let add_points_to (m: map) (a: node) (b : node) =
@@ -463,7 +512,7 @@ let cranges m r =
let rg = Ufind.get m.store r in
match rg.clayout with
| Blob | Cell _ -> raise Not_found
- | Compound(s,rgs) -> s, rgs
+ | Compound(s,_,rgs) -> s, rgs
let cpointed m r =
let rg = Ufind.get m.store r in
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
index 2b2f948d436a879d103e927d32a49c54cbb5919c..e15853e9530b642cef5d9dbb5ad2e6ace8314dcb 100644
--- a/src/plugins/region/memory.mli
+++ b/src/plugins/region/memory.mli
@@ -25,6 +25,7 @@ open Cil_types
type node
type range = {
+ label: string ;
offset: int ;
length: int ;
cells: int ;
@@ -37,6 +38,7 @@ type region = {
roots: varinfo list ;
labels: string list ;
types: typ list ;
+ fields: Fields.domain ;
reads: Access.acs list ;
writes: Access.acs list ;
shifts: Access.acs list ;
@@ -48,7 +50,6 @@ type region = {
type map
val pp_node : Format.formatter -> node -> unit
-val pp_range : Format.formatter -> range -> unit
val pp_region : Format.formatter -> region -> unit
(** Initially unlocked. *)
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 0b5ab56eeec696b105255e42145de87b0b25027d..243f1975703242f4c9a0158b96c5467f842d8fcd 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -46,13 +46,16 @@ struct
type t = Memory.range
let jtype = Data.declare ~package ~name:"range" @@
Jrecord [
+ "label", Jstring ;
"offset", Jnumber ;
"length", Jnumber ;
"cells", Jnumber ;
"data", Node.jtype ;
]
+
let to_json (rg : Memory.range) =
Json.of_fields [
+ "label", Json.of_string rg.label ;
"offset", Json.of_int rg.offset ;
"length", Json.of_int rg.length ;
"cells", Json.of_int rg.cells ;
@@ -181,13 +184,13 @@ module Regions = Data.Jlist(Region)
(* --- Server API --- *)
(* -------------------------------------------------------------------------- *)
-let map_of_localizable ~local (loc : Printer_tag.localizable) =
+let map_of_localizable ?(atStmt=false) (loc : Printer_tag.localizable) =
let open Printer_tag in
match kf_of_localizable loc with
| None -> raise Not_found
| Some kf ->
let domain = Analysis.find kf in
- if local then
+ if atStmt then
match ki_of_localizable loc with
| Kglobal -> domain.map
| Kstmt s -> Stmt.Map.find s domain.body
@@ -236,25 +239,25 @@ let () =
let () =
Request.register
~package ~kind:`GET ~name:"regionsAt"
- ~descr:(Md.plain "Compute regions at the given marker")
- ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~descr:(Md.plain "Compute regions at the given marker program point")
+ ~input:(module Kernel_ast.Marker)
~output:(module Regions)
~signals:[signal]
- begin fun (loc,local) ->
- try Memory.regions @@ map_of_localizable ~local loc
+ begin fun loc ->
+ try Memory.regions @@ map_of_localizable ~atStmt:true loc
with Not_found -> []
end
let () =
Request.register
~package ~kind:`GET ~name:"localize"
- ~descr:(Md.plain "Localize in the local (true) or global map (false)")
- ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~descr:(Md.plain "Localize the marker in its map")
+ ~input:(module Kernel_ast.Marker)
~output:(module NodeOpt)
~signals:[signal]
- begin fun (loc,local) ->
+ begin fun loc ->
try
- let map = map_of_localizable ~local loc in
+ let map = map_of_localizable loc in
region_of_localizable map loc
with Not_found -> None
end
diff --git a/src/plugins/region/tests/region/oracle/blob.res.oracle b/src/plugins/region/tests/region/oracle/blob.res.oracle
index 7231ade0c087fd04d00f93ec9432404752374529..f18edf72e524a8a5f91a20925399ee9dd6ddbfb7 100644
--- a/src/plugins/region/tests/region/oracle/blob.res.oracle
+++ b/src/plugins/region/tests/region/oracle/blob.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing blob.i (no preprocessing)
[region] Analyzing regions
[region] Function array_blob:
- R0003: --- arr 96b 0..96 [0]: R0004 ;
+ R0003: --- arr 96b { #96b: R0004[…]; } ;
R0004: --- 0b ;
R0001: -W- p (int *) 64b (*R0004) ;
[region] Function struct_blob:
- R0003: --- y 64b 0..32 [0]: R0004 ;
+ R0003: --- y 64b { .f: R0004[…]; #32b; } ;
R0004: --- 0b ;
R0001: -W- p (int *) 64b (*R0004) ;
[region] Function var_blob:
diff --git a/src/plugins/region/tests/region/oracle/comp.res.oracle b/src/plugins/region/tests/region/oracle/comp.res.oracle
index 760fd5d9552fcb878dbec0a41fa24cb100aad212..11ade26af7604de77361f0715a788f2355f7b9be 100644
--- a/src/plugins/region/tests/region/oracle/comp.res.oracle
+++ b/src/plugins/region/tests/region/oracle/comp.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing comp.c (with preprocessing)
[region] Analyzing regions
[region] Function f:
- R0003: --- s 192b 0..32 [1]: R0004 64..128 [1]: R0007 128..192 [1]: R000b ;
+ R0003: --- s 192b { .x: R0004; #32b; .z: R0007; .arr: R000b; } ;
R0004: -W- (int) 32b ;
R0007: -W- (int *) 64b (*R0001) ;
R0001: RW- a (int) 32b ;
- R000b: --- 64b 0..64 [4]: R000d ;
+ R000b: --- 64b { #64b: R000d[4]; } ;
R000d: -W- (short) 16b ;
diff --git a/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
index 84e4fe84a136c3e51118270f99079d75072b4153..429d4837db73a9eba55a647242e7e77861de6f3d 100644
--- a/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
+++ b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
@@ -2,12 +2,12 @@
[region] Analyzing regions
[region] Function job:
R0001: R-- fb (FB *) 64b (*R0003) ;
- R0003: --- 704b 256..320 [1]: R0005 320..384 [1]: R0018 ;
+ R0003: --- 704b { #256b; .out1: R0005; .out2: R0018; #320b; } ;
R0005: R-- (struct N *) 64b (*R0008) ;
- R0008: --- 128b 0..64 [1]: R000a 64..96 [1]: R0027 ;
+ R0008: --- 128b { .v: R000a; .s: R0027; #32b; } ;
R000a: RW- (double) 64b ;
R0027: RW- (int) 32b ;
R0018: R-- (struct N *) 64b (*R001b) ;
- R001b: --- 128b 0..64 [1]: R001d 64..96 [1]: R003a ;
+ R001b: --- 128b { .v: R001d; .s: R003a; #32b; } ;
R001d: R-- (double) 64b ;
R003a: R-- (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
index 912201cee70ff9cb9ad26b705ce0a1674f0ab3e1..66f3883ad46b3b4827cb09b10c92c78b6276ff60 100644
--- a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -2,29 +2,32 @@
[region] Analyzing regions
[region] Function job:
R0003: R-- fb (FB *) 64b (*R0005) ;
- R0005: ---
- 704b
- 0..128 [2]: R0007
- 256..320 [1]: R000e
- 320..384 [1]: R0066
- 384..512 [2]: R0015
- 640..704 [1]: R0053 ;
+ R0005: --- 704b
+ {
+ .prm.inp1: R0007[2];
+ #128b;
+ .out1: R000e;
+ .out2: R0066;
+ .out3.idx1: R0015[2];
+ #128b;
+ .sum: R0053;
+ } ;
R0007: R-- (struct N *) 64b (*R0024) ;
- R0024: --- 128b 0..64 [1]: R0026 64..96 [1]: R0046 ;
+ R0024: --- 128b { .v: R0026; .s: R0046; #32b; } ;
R0026: R-- (double) 64b ;
R0046: R-- (int) 32b ;
R000e: R-- (struct N *) 64b (*R001d) ;
- R001d: --- 128b 0..64 [1]: R001f 64..96 [1]: R0038 ;
+ R001d: --- 128b { .v: R001f; .s: R0038; #32b; } ;
R001f: RW- (double) 64b ;
R0038: -W- (int) 32b ;
R0066: R-- (struct N *) 64b (*R0069) ;
- R0069: --- 128b 0..64 [1]: R006b ;
+ R0069: --- 128b { .v: R006b; #64b; } ;
R006b: R-- (double) 64b ;
R0015: R-- (struct N *) (struct L *) 64b (*R003e) ;
- R003e: --- 64b 0..64 [2]: R0040 ;
+ R003e: --- 64b { .v.s: R0040[2]; } ;
R0040: RW- (int) (double) 32b ;
R0053: R-- (struct N *) 64b (*R0056) ;
- R0056: --- 128b 0..64 [1]: R0058 64..96 [1]: R007f ;
+ R0056: --- 128b { .v: R0058; .s: R007f; #32b; } ;
R0058: -W- (double) 64b ;
R007f: -W- (int) 32b ;
R0001: RWA inp (SN *) 64b (*R0007) ;