diff --git a/ivette/src/dome/renderer/graph/diagram.tsx b/ivette/src/dome/renderer/graph/diagram.tsx
index f2c2c732aff6a8b1d98bca85ed4c2dcc589fc3b3..ec0325a9dcc403b3da70add407567c299832114e 100644
--- a/ivette/src/dome/renderer/graph/diagram.tsx
+++ b/ivette/src/dome/renderer/graph/diagram.tsx
@@ -35,6 +35,8 @@ import './style.css';
export type Direction = 'LR' | 'TD';
+export type Font = 'serif' | 'sans' | 'mono';
+
export type Color =
| 'white' | 'grey' | 'dark'
| 'primary' | 'selected'
@@ -45,7 +47,10 @@ export type Shape =
| 'point' | 'box'
| 'diamond' | 'hexagon'
| 'circle' | 'ellipse'
- | 'note' | 'tab' | 'folder';
+ | 'note' | 'tab' | 'folder' | 'cds';
+
+export type Anchor =
+ 'n' | 'ne' | 'e' | 'se' | 's' | 'sw' | 'w' | 'nw' | 'c' | '_';
export type Arrow = 'none' | 'arrow' | 'tee' | 'box' | 'dot';
@@ -64,6 +69,8 @@ export interface Node {
label?: string;
/** Node tooltip */
title?: string;
+ /** Node font (label) */
+ font?: Font;
/** Node color (filled background) */
color?: Color;
/**
@@ -90,18 +97,19 @@ export interface Edge {
line?: Line;
/** Default is `dark` */
color?: Color;
- /** Default is `arrow` */
head?: Arrow;
- /** Default is `none` */
+ headLabel?: string,
+ headAnchor?: Anchor;
tail?: Arrow;
- /** Label */
+ tailLabel?: string,
+ tailAnchor?: Anchor;
+ font?: Font;
label?: string;
- /** Tooltip */
title?: string;
- /** Head label */
- headLabel?: string,
- /** Tail label */
- tailLabel?: string,
+ /** Edge constraints node placement (default: true). */
+ constraint?: boolean;
+ /** Node placement on the same rank (default: false). */
+ aligned?: boolean;
}
export interface Cluster {
@@ -148,9 +156,15 @@ export interface DiagramProps {
}
/* -------------------------------------------------------------------------- */
-/* --- Color Model --- */
+/* --- CSS Model --- */
/* -------------------------------------------------------------------------- */
+const FONTNAME = {
+ 'serif': 'Times',
+ 'sans': 'sans-serif',
+ 'mono': 'Courier',
+};
+
// node background colors
const BGCOLOR = {
'white': '#fff',
@@ -307,7 +321,10 @@ class Builder {
}
attr(a: string, v: string | number | boolean | undefined): Builder {
- return v ? this.print(' ', a, '=').value(v).print(';') : this;
+ if (v !== undefined && v !== '')
+ return this.print(' ', a, '=').value(v).print(';');
+ else
+ return this;
}
// --- Node Table Shape
@@ -340,7 +357,8 @@ class Builder {
.print(' ')
.port(n.id)
.print(' [')
- .attr('id', n.id);
+ .attr('id', n.id)
+ .attr('fontname', n.font ? FONTNAME[n.font] : undefined);
if (typeof n.shape === 'object') {
this
.attr('shape', 'record')
@@ -392,6 +410,11 @@ class Builder {
edge(e: Edge): void {
const { line = 'solid', head = 'arrow', tail = 'none' } = e;
const tooltip = e.title ?? e.label ?? `${e.source} -> ${e.target}`;
+ if (e.aligned === true)
+ this
+ .print('{ rank=same; ')
+ .port(e.source).print(' ')
+ .port(e.target).println(' };');
this
.print(' ')
.port(e.source, e.sourcePort)
@@ -399,8 +422,12 @@ class Builder {
.port(e.target, e.targetPort)
.print(' [')
.attr('label', e.label)
+ .attr('fontname', e.font ? FONTNAME[e.font] : undefined)
+ .attr('headport', e.tailAnchor)
+ .attr('tailport', e.headAnchor)
.attr('headlabel', e.headLabel)
.attr('taillabel', e.tailLabel)
+ .attr('constraint', e.constraint === false ? false : undefined)
.attr('labeltooltip', e.label ? tooltip : undefined)
.attr('headtooltip', e.headLabel ? tooltip : undefined)
.attr('tailtooltip', e.tailLabel ? tooltip : undefined)
@@ -476,7 +503,7 @@ function GraphvizView(props: GraphvizProps): JSX.Element {
setError(undefined);
graphviz(href, {
useWorker: false,
- fit: true, zoom: true, width, height,
+ fit: false, zoom: true, width, height,
}).onerror(setError)
.renderDot(model).on('end', function () {
if (onSelection) {
diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
new file mode 100644
index 0000000000000000000000000000000000000000..5d01bdbe22ac529ecefaa43e5a11963c12441397
--- /dev/null
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -0,0 +1,199 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+/* --- Generated Frama-C Server API --- */
+
+/**
+ Region Analysis
+ @packageDocumentation
+ @module frama-c/plugins/region/api
+*/
+
+//@ts-ignore
+import * as Json from 'dome/data/json';
+//@ts-ignore
+import * as Compare from 'dome/data/compare';
+//@ts-ignore
+import * as Server from 'frama-c/server';
+//@ts-ignore
+import * as State from 'frama-c/states';
+
+//@ts-ignore
+import { byDecl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { byMarker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { decl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { declDefault } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jDecl } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { jMarker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { marker } from 'frama-c/kernel/api/ast';
+//@ts-ignore
+import { markerDefault } from 'frama-c/kernel/api/ast';
+
+export type node = Json.index<'#node'>;
+
+/** Decoder for `node` */
+export const jNode: Json.Decoder<node> = Json.jIndex<'#node'>('#node');
+
+/** Natural order for `node` */
+export const byNode: Compare.Order<node> = Compare.number;
+
+/** Default value for `node` */
+export const nodeDefault: node = Json.jIndex<'#node'>('#node')(-1);
+
+export type range =
+ { offset: number, length: number, cells: number, data: node };
+
+/** Decoder for `range` */
+export const jRange: Json.Decoder<range> =
+ Json.jObject({
+ offset: Json.jNumber,
+ length: Json.jNumber,
+ cells: Json.jNumber,
+ data: jNode,
+ });
+
+/** Natural order for `range` */
+export const byRange: Compare.Order<range> =
+ Compare.byFields
+ <{ offset: number, length: number, cells: number, data: node }>({
+ offset: Compare.number,
+ length: Compare.number,
+ cells: Compare.number,
+ data: byNode,
+ });
+
+/** Default value for `range` */
+export const rangeDefault: range =
+ { offset: 0, length: 0, cells: 0, data: nodeDefault };
+
+export type region =
+ { node: node, roots: string[], labels: string[], parents: node[],
+ sizeof: number, ranges: range[], pointed?: node, reads: boolean,
+ writes: boolean, bytes: boolean, label: string, title: string };
+
+/** Decoder for `region` */
+export const jRegion: Json.Decoder<region> =
+ Json.jObject({
+ node: jNode,
+ roots: Json.jArray(Json.jString),
+ labels: Json.jArray(Json.jString),
+ parents: Json.jArray(jNode),
+ sizeof: Json.jNumber,
+ ranges: Json.jArray(jRange),
+ pointed: Json.jOption(jNode),
+ reads: Json.jBoolean,
+ writes: Json.jBoolean,
+ bytes: Json.jBoolean,
+ label: Json.jString,
+ title: Json.jString,
+ });
+
+/** Natural order for `region` */
+export const byRegion: Compare.Order<region> =
+ Compare.byFields
+ <{ node: node, roots: string[], labels: string[], parents: node[],
+ sizeof: number, ranges: range[], pointed?: node, reads: boolean,
+ writes: boolean, bytes: boolean, label: string, title: string }>({
+ node: byNode,
+ roots: Compare.array(Compare.alpha),
+ labels: Compare.array(Compare.alpha),
+ parents: Compare.array(byNode),
+ sizeof: Compare.number,
+ ranges: Compare.array(byRange),
+ pointed: Compare.defined(byNode),
+ reads: Compare.boolean,
+ writes: Compare.boolean,
+ bytes: Compare.boolean,
+ label: Compare.string,
+ title: Compare.string,
+ });
+
+/** Default value for `region` */
+export const regionDefault: region =
+ { node: nodeDefault, roots: [], labels: [], parents: [], sizeof: 0,
+ ranges: [], pointed: undefined, reads: false, writes: false,
+ bytes: false, label: '', title: '' };
+
+/** Region Analysis Updated */
+export const updated: Server.Signal = {
+ name: 'plugins.region.updated',
+};
+
+const compute_internal: Server.ExecRequest<decl,null> = {
+ kind: Server.RqKind.EXEC,
+ name: 'plugins.region.compute',
+ input: jDecl,
+ output: Json.jNull,
+ fallback: null,
+ signals: [],
+};
+/** Compute regions for the given declaration */
+export const compute: Server.ExecRequest<decl,null>= compute_internal;
+
+const regions_internal: Server.GetRequest<decl,region[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.region.regions',
+ input: jDecl,
+ output: Json.jArray(jRegion),
+ fallback: [],
+ signals: [ { name: 'plugins.region.updated' } ],
+};
+/** Returns computed regions for the given declaration */
+export const regions: Server.GetRequest<decl,region[]>= regions_internal;
+
+const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.region.regionsAt',
+ input: Json.jPair( jMarker, Json.jBoolean,),
+ 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
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.region.localize',
+ input: Json.jPair( jMarker, Json.jBoolean,),
+ 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;
+
+/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..eed8bea5b81bb105826aaab9a9c1e05b85593f5a
--- /dev/null
+++ b/ivette/src/frama-c/plugins/region/index.tsx
@@ -0,0 +1,99 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+// --------------------------------------------------------------------------
+// --- Regions
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import { Label } from 'dome/controls/labels';
+import { LCD } from 'dome/controls/displays';
+import { IconButton } from 'dome/controls/buttons';
+import * as Dome from 'dome';
+import * as Tools from 'dome/frame/toolbars';
+import * as Ivette from 'ivette';
+import * as Server from 'frama-c/server';
+import * as States from 'frama-c/states';
+import * as Region from './api';
+import { MemoryView } from './memory';
+import './style.css';
+
+function RegionAnalys(): JSX.Element {
+ const [kf, setKf] = React.useState<States.Scope>();
+ const [kfName, setName] = React.useState<string>();
+ const [pinned, setPinned] = React.useState(false);
+ const [running, setRunning] = React.useState(false);
+ const setComputing = Dome.useProtected(setRunning);
+ const scope = States.useCurrentScope();
+ const { kind, name } = States.useDeclaration(scope);
+ const regions = States.useRequestStable(Region.regions, kf);
+ React.useEffect(() => {
+ if (!pinned && kind === 'FUNCTION' && scope !== kf) {
+ setKf(scope);
+ setName(name);
+ } else if (!Server.isRunning()) {
+ setKf(undefined);
+ setName(undefined);
+ setPinned(false);
+ }
+ }, [pinned, kind, name, scope, kf]);
+ async function compute(): Promise<void> {
+ try {
+ setComputing(true);
+ await Server.send(Region.compute, kf);
+ } finally {
+ setComputing(false);
+ }
+ }
+ return (
+ <>
+ <Tools.ToolBar>
+ <Label label='Function' />
+ <LCD className='region-lcd' label={kfName ?? '---'} />
+ <Tools.Button
+ icon={running ? 'EXECUTE' : 'MEDIA.PLAY'}
+ title='Run region analysis on the selected function'
+ disabled={running}
+ visible={kf !== undefined && regions.length === 0}
+ onClick={compute}
+ />
+ <IconButton
+ icon='PIN'
+ display={kf !== undefined}
+ title='Keep focus on current function'
+ selected={pinned}
+ onClick={() => setPinned(!pinned)}
+ />
+ </Tools.ToolBar>
+ <MemoryView regions={regions} />
+ </>
+ );
+}
+
+Ivette.registerComponent({
+ id: 'fc.region.main',
+ label: 'Region Analysis',
+ preferredPosition: 'BD',
+ children: <RegionAnalys />,
+});
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..a59a4adac95021d3e17cd48d6e10cb0e9aceb15f
--- /dev/null
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -0,0 +1,124 @@
+/* ************************************************************************ */
+/* */
+/* 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). */
+/* */
+/* ************************************************************************ */
+
+// --------------------------------------------------------------------------
+// --- Regions
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import * as Dot from 'dome/graph/diagram';
+import * as Region from './api';
+
+function makeRecord(
+ edges: Dot.Edge[],
+ source: string,
+ sizeof: number,
+ ranges: Region.range[]
+): Dot.Cell[] {
+ if (ranges.length === 0) return [];
+ const cells: Dot.Cell[] = [];
+ let offset = 0;
+ ranges.forEach((rg, i) => {
+ const port = `r${i}`;
+ const target = `n${rg.data}`;
+ edges.push({ source, sourcePort: port, target });
+ if (offset !== rg.offset)
+ cells.push(`${offset}..${rg.offset - 1} ##`);
+ offset = rg.offset + rg.length;
+ cells.push({
+ label: `${rg.offset}..${offset - 1} [${rg.cells}]`,
+ port,
+ });
+ });
+ if (offset !== sizeof)
+ cells.push(`${offset}..${sizeof - 1} ##`);
+ return cells;
+}
+
+interface Diagram {
+ nodes: Dot.Node[];
+ edges: Dot.Edge[];
+}
+
+function makeDiagram(regions: readonly Region.region[]): Diagram {
+ const nodes: Dot.Node[] = [];
+ const edges: Dot.Edge[] = [];
+ regions.forEach(r => {
+ const id = `n${r.node}`;
+ // --- Color
+ const color =
+ r.bytes ? 'red' :
+ r.pointed !== undefined
+ ? (r.writes ? 'orange' : 'yellow')
+ : (r.writes && r.reads) ? 'green' :
+ r.writes ? 'pink' : r.reads ? 'grey' : 'white';
+ // --- Shape
+ const font = r.ranges.length > 0 ? 'mono' : 'sans';
+ const cells = makeRecord(edges, id, r.sizeof, r.ranges);
+ const shape = cells.length > 0 ? cells : undefined;
+ nodes.push({ id, font, color, label: r.label, title: r.title, shape });
+ // --- Labels
+ const L: Dot.Node =
+ { id: '', shape: 'note', font: 'mono' };
+ 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 });
+ });
+ // --- Roots
+ const R: Dot.Node =
+ { id: '', shape: 'cds', font: 'mono' };
+ r.roots.forEach(x => {
+ const xid = `X${x}`;
+ nodes.push({ ...R, id: xid, label: x });
+ edges.push({ source: xid, headAnchor: "e", target: id });
+ });
+ // --- Pointed
+ if (r.pointed !== undefined) {
+ const pid = `n${r.pointed}`;
+ edges.push({ source: id, target: pid, head: 'dot', color: 'orange' });
+ }
+ });
+ 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}` });
+}
+
+export interface MemoryViewProps {
+ regions?: readonly Region.region[];
+ node?: Region.node | undefined;
+ label?: string;
+}
+
+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} />;
+}
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/plugins/region/pkg.json b/ivette/src/frama-c/plugins/region/pkg.json
new file mode 100644
index 0000000000000000000000000000000000000000..f9ba9b34ba90149f99ddfff2cce84846d98bbf63
--- /dev/null
+++ b/ivette/src/frama-c/plugins/region/pkg.json
@@ -0,0 +1,3 @@
+{
+ "name": "Frama-C/Region"
+}
diff --git a/ivette/src/frama-c/plugins/region/style.css b/ivette/src/frama-c/plugins/region/style.css
new file mode 100644
index 0000000000000000000000000000000000000000..0076926a0527f0215a6fa22963d4129835df2279
--- /dev/null
+++ b/ivette/src/frama-c/plugins/region/style.css
@@ -0,0 +1,9 @@
+/* -------------------------------------------------------------------------- */
+/* --- CSS for Region Views --- */
+/* -------------------------------------------------------------------------- */
+
+.region-lcd {
+ margin-top: 4px;
+ min-width: 160px;
+ text-align: center;
+}
diff --git a/nix/plugins-tests.nix b/nix/plugins-tests.nix
index a500d6d0ce11b44a18ed1f1690bd1ae250eb011a..b6a83abadd16fc420eb532347994f0e9646909e9 100644
--- a/nix/plugins-tests.nix
+++ b/nix/plugins-tests.nix
@@ -24,6 +24,7 @@ mk_tests {
@src/plugins/markdown-report/tests/ptests \
@src/plugins/nonterm/tests/ptests \
@src/plugins/report/tests/ptests \
+ @src/plugins/region/tests/ptests \
@src/plugins/server/tests/ptests \
@src/plugins/variadic/tests/ptests
'';
diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml
index fd438e7de134a87f511ac4711e676947853f92ed..24d8d26e36fc42e6af21e74e0925beaf910a755c 100644
--- a/src/kernel_services/ast_queries/cil.ml
+++ b/src/kernel_services/ast_queries/cil.ml
@@ -5936,6 +5936,11 @@ let getCompField cinfo fieldName =
(fun fi -> fi.fname = fieldName)
(Option.value ~default:[] cinfo.cfields)
+let getCompType typ =
+ match unrollTypeSkel typ with
+ | TComp(comp,_) -> comp
+ | _ -> raise Not_found
+
let sameSizeInt ?(machdep=false) (ik1 : ikind) (ik2 : ikind) =
if machdep then bytesSizeOfInt ik1 == bytesSizeOfInt ik2
else
diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli
index 2e07fd682872d525bc099358fcd556ab91934839..83a9b53210a943b23d890b72c2337b6548c27b8b 100644
--- a/src/kernel_services/ast_queries/cil.mli
+++ b/src/kernel_services/ast_queries/cil.mli
@@ -658,6 +658,8 @@ val lenOfArray64: exp option -> Integer.t
(** Return a named fieldinfo in compinfo, or raise Not_found *)
val getCompField: compinfo -> string -> fieldinfo
+(** Return the compinfo of the typ, or raise Not_found *)
+val getCompType: typ -> compinfo
(** A datatype to be used in conjunction with [existsType] *)
type existsAction =
diff --git a/src/plugins/region/README.md b/src/plugins/region/README.md
new file mode 100644
index 0000000000000000000000000000000000000000..02ef85649b845ce45b73275529c752a6e80524ae
--- /dev/null
+++ b/src/plugins/region/README.md
@@ -0,0 +1,58 @@
+# Region Analysis plugin (experimental)
+
+Region is a plugin for Frama-C that implements a new memory and alias analysis.
+This is a work in progress in early design stage.
+
+## Usage
+
+Regions are computed on demand from the registered Server requests.
+
+Command line option `-region` can be used to compute regions for all functions
+and dump on output the result analysis. With `-region-debug 1+` typed accesses
+are also reported.
+
+An API will be provided soon.
+
+## Annotations
+
+Behavior annotation `\region::region` and code annotation `\region::alias`
+can be used to specify supplementary aliases and to name regions.
+The syntax is the same:
+
+```
+//@ region [A:] lv, … , lv ;
+```
+
+Such a specification put all the l-values in the same region. A name can be
+given to the region, and reused later to put other l-values on the same region.
+Several regions can be specified in a single annotation.
+
+Unnamed regions from different annotations refer to _different_ regions unless
+they are aliased by sharing common l-values.
+
+L-values in region annotations use a similar syntax to ACSL terms.
+However, array access and pointer arithmetics must be specified with unlimited range, eg. `a[..]` or `*(p+(..))`.
+
+A syntax for specifying field aliasing and input/output array shapes will be provided soon.
+
+## Current Limitations
+
+Currently, ACSL contracts are not taken into account except for region
+annotations. Function calls are totally incomplete, and aliases that would be
+produces by function calls are not _yet_ taken into account. Use `//@alias` code-annotations as a temporary work around.
+
+## Ivette Support
+
+The Region Analysis component can be used to compute and visualize regions.
+Tooltips print access types to each regions.
+
+Colored regions means the following:
+ - _Red_ regions are those accessed with incompatible types
+ - _Yellow_ regions are constant pointers
+ - _Orange_ regions are written pointers
+ - _Green_ regions are RW regions
+ - _Pink_ regions are written-only regions (might be drop)
+ - _Grey_ regions are read-only regions (constant, no memory)
+
+Regions access and localization of currently selected marker will be
+provided soon.
diff --git a/src/plugins/region/Region.ml b/src/plugins/region/Region.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2b8fce64aec5b2f1ee6fe423ba7feb30eaf6ff69
--- /dev/null
+++ b/src/plugins/region/Region.ml
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Analysis API --- *)
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/Region.mli b/src/plugins/region/Region.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d9615a6fffe2e821fdbe14da1d0eed73de2bfc9c
--- /dev/null
+++ b/src/plugins/region/Region.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Interface for the Region plug-in. *)
diff --git a/src/plugins/region/access.ml b/src/plugins/region/access.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5baa3096b5d7d24b5bcb9d4dd089fef236646816
--- /dev/null
+++ b/src/plugins/region/access.ml
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+open Cil_datatype
+
+type acs =
+ | Exp of Stmt.t * exp
+ | Lval of Stmt.t * lval
+ | Init of Stmt.t * varinfo
+ | Term of Property.t * term_lval
+
+let compare (a : acs) (b : acs) : int =
+ match a, b with
+ | Init(sa,xa), Init(sb,xb) ->
+ let cmp = Stmt.compare sa sb in
+ if cmp <> 0 then cmp else Varinfo.compare xa xb
+ | Init _ , _ -> (-1)
+ | _ , Init _ -> (+1)
+
+ | Lval(sa,la), Lval(sb,lb) ->
+ let cmp = Stmt.compare sa sb in
+ if cmp <> 0 then cmp else Lval.compare la lb
+ | Lval _ , _ -> (-1)
+ | _ , Lval _ -> (+1)
+
+ | Exp(sa,ea), Exp(sb,eb) ->
+ let cmp = Stmt.compare sa sb in
+ if cmp <> 0 then cmp else Exp.compare ea eb
+ | Exp _ , _ -> (-1)
+ | _ , Exp _ -> (+1)
+
+ | Term(sa,ta), Term(sb,tb) ->
+ let cmp = Property.compare sa sb in
+ if cmp <> 0 then cmp else Term_lval.compare ta tb
+
+let pstmt fmt (s : stmt) =
+ match s.labels with
+ | Label(l,_,_)::_ -> Format.pp_print_string fmt l
+ | _ ->
+ let loc, _ = Stmt.loc s in
+ Format.fprintf fmt "L%d" loc.pos_lnum
+
+let pretty fmt = function
+ | Init(s,x) ->
+ Format.fprintf fmt "%a@%a" Varinfo.pretty x pstmt s
+ | Exp(s,e) ->
+ Format.fprintf fmt "%a@%a" Exp.pretty e pstmt s
+ | Lval(s,l) ->
+ Format.fprintf fmt "%a@%a" Lval.pretty l pstmt s
+ | Term(s,l) ->
+ Format.fprintf fmt "%a@%s" Term_lval.pretty l
+ (Property.Names.get_prop_name_id s)
+
+let typeof = function
+ | Init(_,x) -> x.vtype
+ | Lval(_,lv) -> Cil.typeOfLval lv
+ | Exp(_,e) -> Cil.typeOf e
+ | Term(_,lt) ->
+ match Cil.typeOfTermLval lt with
+ | Ctype ty -> ty
+ | _ -> Cil.voidType
+
+module Set = Set.Make(struct type t = acs let compare = compare end)
diff --git a/src/plugins/region/access.mli b/src/plugins/region/access.mli
new file mode 100644
index 0000000000000000000000000000000000000000..cadb24bc098a9b3908f67308bf3cd0bc39f1b7be
--- /dev/null
+++ b/src/plugins/region/access.mli
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+
+type acs =
+ | Exp of stmt * exp
+ | Lval of stmt * lval
+ | Init of stmt * varinfo
+ | Term of Property.t * term_lval
+
+val compare : acs -> acs -> int
+val pretty : Format.formatter -> acs -> unit
+
+val typeof : acs -> typ
+
+module Set : Set.S with type elt = acs
diff --git a/src/plugins/region/analysis.ml b/src/plugins/region/analysis.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b64c6571bc83fbfa648159d1701a12bf6e597a33
--- /dev/null
+++ b/src/plugins/region/analysis.ml
@@ -0,0 +1,74 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_datatype
+
+(* -------------------------------------------------------------------------- *)
+(* --- Projectification --- *)
+(* -------------------------------------------------------------------------- *)
+
+module DOMAIN : Datatype.S with type t = Code.domain =
+ Datatype.Make
+ (struct
+ type t = Code.domain
+ include Datatype.Undefined
+ let name = "Region.Analysis.MEMORY"
+ let mem_project = Datatype.never_any_project
+ let reprs =
+ let m = Memory.create () in
+ Code.[{ map = m; body = Stmt.Map.empty ; spec = Property.Map.empty }]
+ end)
+
+module STATE = State_builder.Hashtbl(Kernel_function.Hashtbl)(DOMAIN)
+ (struct
+ let size = 0
+ let name = "Region.Analysis.STATE"
+ let dependencies = [Ast.self]
+ end)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Memoized Access --- *)
+(* -------------------------------------------------------------------------- *)
+
+let find = STATE.find
+
+let get kf =
+ try STATE.find kf with Not_found ->
+ Options.feedback ~ontty:`Transient "Function %a…" Kernel_function.pretty kf ;
+ let domain = Code.domain kf in
+ 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 ->
+ Format.pp_print_newline fmt () ;
+ Memory.pp_region fmt r ;
+ end
+ end ;
+ domain
+
+let compute kf = ignore @@ get kf
+
+let add_hook f = STATE.add_hook_on_change (fun _ -> f())
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/analysis.mli b/src/plugins/region/analysis.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e9279b47420bc40e87fef33265d8a9e86a15febc
--- /dev/null
+++ b/src/plugins/region/analysis.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+
+(** @raises Not_found *)
+val find : kernel_function -> Code.domain
+
+(** Memoized *)
+val get : kernel_function -> Code.domain
+
+(** Memoized *)
+val compute : kernel_function -> unit
+
+(** Hook on update *)
+val add_hook : (unit -> unit) -> unit
diff --git a/src/plugins/region/annot.ml b/src/plugins/region/annot.ml
new file mode 100644
index 0000000000000000000000000000000000000000..825ebf5ce8f52c2fd19a66e55adf11ef979814a4
--- /dev/null
+++ b/src/plugins/region/annot.ml
@@ -0,0 +1,256 @@
+(**************************************************************************)
+(* *)
+(* 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 Logic_ptree
+open Cil_types
+open Cil_datatype
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Specifications --- *)
+(* -------------------------------------------------------------------------- *)
+
+type path = {
+ loc : location ;
+ typ : typ ;
+ step: step ;
+}
+
+and step =
+ | Var of varinfo
+ | AddrOf of path
+ | Star of path
+ | Index of path
+ | Shift of path
+ | Field of path * fieldinfo
+ | Cast of typ * path
+
+type region = {
+ rname: string option ;
+ rpath: path list ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let atomic = function
+ | Var _ | AddrOf _ | Star _ | Index _ | Field _ -> true
+ | Shift _ | Cast _ -> false
+
+let rec pp_step fmt = function
+ | Var x -> Varinfo.pretty fmt x
+ | Field(p,f) -> pfield p f fmt
+ | Index a -> Format.fprintf fmt "%a[..]" pp_atom a
+ | Shift a -> Format.fprintf fmt "%a+(..)" pp_atom a
+ | Star a -> Format.fprintf fmt "*%a" pp_atom a
+ | AddrOf a -> Format.fprintf fmt "&%a" pp_atom a
+ | Cast(t,a) -> Format.fprintf fmt "(%a)@,%a" Typ.pretty t pp_atom a
+
+and pfield p fd fmt =
+ match p.step with
+ | Star p -> Format.fprintf fmt "%a->%a" pp_atom p Fieldinfo.pretty fd
+ | _ -> Format.fprintf fmt "%a.%a" pp_atom p Fieldinfo.pretty fd
+
+and pp_atom fmt a =
+ if atomic a.step then pp_step fmt a.step
+ else Format.fprintf fmt "@[<hov 2>(%a)@]" pp_step a.step
+
+and pp_path fmt a = pp_step fmt a.step
+
+let pp_named fmt = function None -> () | Some a -> Format.fprintf fmt "%s: " a
+
+let pp_region fmt r =
+ match r.rpath with
+ | [] -> Format.pp_print_string fmt "\null"
+ | p::ps ->
+ begin
+ Format.fprintf fmt "@[<hov 2>" ;
+ pp_named fmt r.rname ;
+ pp_path fmt p ;
+ List.iter (Format.fprintf fmt ",@ %a" pp_path) ps ;
+ Format.fprintf fmt "@]" ;
+ end
+
+let pp_regions fmt = function
+ | [] -> Format.pp_print_string fmt "\null"
+ | r::rs ->
+ begin
+ Format.fprintf fmt "@[<hv 0>" ;
+ pp_region fmt r ;
+ List.iter (Format.fprintf fmt ",@ %a" pp_region) rs ;
+ Format.fprintf fmt "@]" ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Parsers --- *)
+(* -------------------------------------------------------------------------- *)
+
+type env = {
+ context: Logic_typing.typing_context ;
+ mutable named: string option ;
+ mutable paths: path list ;
+ mutable specs: region list ;
+}
+
+let error (env:env) ~loc msg = env.context.error loc msg
+
+let parse_variable (env:env) ~loc x =
+ match env.context.find_var x with
+ | { lv_origin = Some v } -> { loc ; typ = v.vtype ; step = Var v }
+ | _ -> error env ~loc "Variable '%s' is not a C-variable" x
+
+let parse_field env ~loc comp f =
+ try Cil.getCompField comp f with Not_found ->
+ error env ~loc "No field '%s' in compound type '%s'" f comp.cname
+
+let parse_compinfo env ~loc typ =
+ try Cil.getCompType typ with Not_found ->
+ error env ~loc "Expected compound type for term"
+
+let parse_lrange (env: env) (e : lexpr) =
+ match e.lexpr_node with
+ | PLrange(None,None) -> ()
+ | _ ->
+ error env ~loc:e.lexpr_loc "Unexpected index (use unspecified range only)"
+
+let parse_typ env ~loc t =
+ let open Logic_typing in
+ let g = env.context in
+ let t = g.logic_type g loc g.pre_state t in
+ match Logic_utils.unroll_type t with
+ | Ctype typ -> typ
+ | _ -> error env ~loc "C-type expected for casting l-values"
+
+let rec parse_lpath (env:env) (e: lexpr) =
+ let loc = e.lexpr_loc in
+ match e.lexpr_node with
+ | PLvar x -> parse_variable env ~loc x
+ | PLunop( Ustar , p ) ->
+ let lv = parse_lpath env p in
+ if Cil.isPointerType lv.typ then
+ let te = Cil.typeOf_pointed lv.typ in
+ { loc ; step = Star lv ; typ = te }
+ else
+ error env ~loc "Pointer-type expected for operator '*'"
+ | PLunop( Uamp , p ) ->
+ let lv = parse_lpath env p in
+ let typ = TPtr( lv.typ , [] ) in
+ { loc ; step = AddrOf lv ; typ }
+ | PLbinop( p , Badd , rg ) ->
+ parse_lrange env rg ;
+ let { typ } as lv = parse_lpath env p in
+ if Cil.isPointerType typ then
+ { loc ; step = Shift lv ; typ = typ }
+ else
+ if Cil.isArrayType typ then
+ let te = Cil.typeOf_array_elem typ in
+ { loc ; step = Shift lv ; typ = TPtr(te,[]) }
+ else
+ error env ~loc "Pointer-type expected for operator '+'"
+ | PLdot( p , f ) ->
+ let lv = parse_lpath env p in
+ let comp = parse_compinfo env ~loc:lv.loc lv.typ in
+ let fd = parse_field env ~loc comp f in
+ { loc ; step = Field(lv,fd) ; typ = fd.ftype }
+ | PLarrow( p , f ) ->
+ let sp = { lexpr_loc = loc ; lexpr_node = PLunop(Ustar,p) } in
+ let pf = { lexpr_loc = loc ; lexpr_node = PLdot(sp,f) } in
+ parse_lpath env pf
+ | PLarrget( p , rg ) ->
+ parse_lrange env rg ;
+ let { typ } as lv = parse_lpath env p in
+ if Cil.isPointerType typ then
+ let pointed = Cil.typeOf_pointed typ in
+ let ls = { loc ; step = Shift lv ; typ } in
+ { loc ; step = Star ls ; typ = pointed }
+ else
+ if Cil.isArrayType typ then
+ let elt = Cil.typeOf_array_elem typ in
+ { loc ; step = Index lv ; typ = elt }
+ else
+ error env ~loc:lv.loc "Pointer or array type expected"
+ | PLcast( t , a ) ->
+ let lv = parse_lpath env a in
+ let ty = parse_typ env ~loc t in
+ { loc ; step = Cast(ty,lv) ; typ = ty }
+ | _ ->
+ error env ~loc "Unexpected expression for region spec"
+
+let rec parse_named_lpath (env:env) p =
+ match p.lexpr_node with
+ | PLnamed( name , p ) ->
+ if env.named <> None && env.paths <> [] then
+ begin
+ env.specs <- { rname = env.named ; rpath = env.paths } :: env.specs ;
+ env.paths <- [] ;
+ end ;
+ env.named <- Some name ;
+ parse_named_lpath env p
+ | _ ->
+ let path = parse_lpath env p in
+ env.paths <- path :: env.paths
+
+(* -------------------------------------------------------------------------- *)
+(* --- Spec Typechecking & Printing --- *)
+(* -------------------------------------------------------------------------- *)
+
+let kspec = ref 0
+let registry = Hashtbl.create 0
+
+let of_extid id = try Hashtbl.find registry id with Not_found -> []
+let of_extension = function
+ | { ext_name="region" ; ext_kind = Ext_id k } -> of_extid k
+ | _ -> []
+let of_code_annot = function
+ | { annot_content = AExtended(_,_,e) } -> of_extension e
+ | _ -> []
+
+let of_behavior bhv = List.concat_map of_extension bhv.b_extended
+
+let typecheck typing_context _loc ps =
+ let env = {
+ named = None ;
+ context = typing_context ;
+ paths = [] ; specs = [] ;
+ } in
+ List.iter (parse_named_lpath env) ps ;
+ let id = !kspec in incr kspec ;
+ let specs = { rname = env.named ; rpath = env.paths } :: env.specs in
+ Hashtbl.add registry id @@ List.rev specs ;
+ Ext_id id
+
+let printer _pp fmt = function
+ | Ext_id k ->
+ let rs = try Hashtbl.find registry k with Not_found -> [] in
+ pp_regions fmt rs
+ | _ -> ()
+
+let () =
+ begin
+ Acsl_extension.register_behavior
+ ~plugin:"region" "region" typecheck ~printer false ;
+ Acsl_extension.register_code_annot
+ ~plugin:"region" "alias" typecheck ~printer false ;
+ end
+
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/annot.mli b/src/plugins/region/annot.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a2fd8bc531f698f97515c6d863fe5b3ba2f241ee
--- /dev/null
+++ b/src/plugins/region/annot.mli
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+
+type path = {
+ loc : location ;
+ typ : typ ;
+ step: step ;
+}
+
+and step =
+ | Var of varinfo
+ | AddrOf of path
+ | Star of path
+ | Index of path
+ | Shift of path
+ | Field of path * fieldinfo
+ | Cast of typ * path
+
+type region = {
+ rname: string option ;
+ rpath: path list ;
+}
+
+val pp_step : Format.formatter -> step -> unit
+val pp_atom : Format.formatter -> path -> unit
+val pp_path : Format.formatter -> path -> unit
+val pp_region : Format.formatter -> region -> unit
+val pp_regions : Format.formatter -> region list -> unit
+
+val of_extension : acsl_extension -> region list
+val of_code_annot : code_annotation -> region list
+val of_behavior : behavior -> region list
diff --git a/src/plugins/region/code.ml b/src/plugins/region/code.ml
new file mode 100644
index 0000000000000000000000000000000000000000..93bbc497df42f1f637b9fd2c72e4fcc29719c54a
--- /dev/null
+++ b/src/plugins/region/code.ml
@@ -0,0 +1,251 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+open Cil_datatype
+open Memory
+
+(* -------------------------------------------------------------------------- *)
+(* --- L-Values & Expressions --- *)
+(* -------------------------------------------------------------------------- *)
+
+type value = { from : node option ; ptr : node option }
+let integral = { from = None ; ptr = None }
+let pointer m v =
+ match v.ptr with
+ | Some p -> v, p
+ | None ->
+ let p = add_cell m () in
+ Option.iter (fun s -> Memory.add_points_to m s p) v.from ;
+ { v with ptr = Some p }, p
+
+let rec add_lval (m:map) (s:stmt) (lv:lval) : node =
+ let h = fst lv in
+ add_loffset m s (add_lhost m s h) (Cil.typeOfLhost h) (snd lv)
+
+and add_lhost (m:map) (s:stmt) = function
+ | Var x -> Memory.add_root m x
+ | Mem e -> snd @@ pointer m @@ add_exp m s e
+
+and add_loffset (m:map) (s:stmt) (r:node) (ty:typ)= function
+ | NoOffset -> r
+ | Field(fd,ofs) ->
+ add_loffset m s (add_field m r fd) fd.ftype ofs
+ | Index(_,ofs) ->
+ add_loffset m s (add_index m r ty) (Cil.typeOf_array_elem ty) ofs
+
+and add_value m s e = ignore (add_exp m s e)
+
+and add_exp (m: map) (s:stmt) (e:exp) : value =
+ match e.enode with
+
+ | AddrOf lv | StartOf lv ->
+ let rv = Some (add_lval m s lv) in
+ { from = rv ; ptr = rv }
+
+ | Lval lv ->
+ let rv = add_lval m s lv in
+ Memory.read m rv (Lval(s,lv)) ;
+ let ptr = Memory.add_value m rv @@ Cil.typeOfLval lv in
+ { from = Some rv ; ptr }
+
+ | BinOp((PlusPI|MinusPI),p,k,_) ->
+ add_value m s k ;
+ let v = add_exp m s p in
+ Option.iter (fun r -> Memory.shift m r (Exp(s,e))) v.from ; v
+
+ | UnOp(_,e,_) ->
+ add_value m s e ; integral
+
+ | BinOp(_,a,b,_) ->
+ add_value m s a ; add_value m s b ; integral
+
+ | CastE(ty,p) ->
+ let v = add_exp m s p in
+ if Cil.isPointerType ty then
+ fst @@ pointer m @@ v
+ else
+ integral
+
+ | Const _
+ | SizeOf _ | SizeOfE _ | SizeOfStr _
+ | AlignOf _ | AlignOfE _
+ -> integral
+
+(* -------------------------------------------------------------------------- *)
+(* --- Initializers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec add_init (m:map) (s:stmt) (acs:Access.acs) (lv:lval) (iv:init) =
+ match iv with
+
+ | SingleInit e ->
+ let r = add_lval m s lv in
+ Memory.write m r acs ;
+ Option.iter (Memory.add_points_to m r) (add_exp m s e).ptr
+
+ | CompoundInit(_,fvs) ->
+ List.iter
+ (fun (ofs,iv) ->
+ let lv = Cil.addOffsetLval ofs lv in
+ add_init m s acs lv iv
+ ) fvs
+
+(* -------------------------------------------------------------------------- *)
+(* --- Instructions --- *)
+(* -------------------------------------------------------------------------- *)
+
+let add_instr (m:map) (s:stmt) (instr:instr) =
+ match instr with
+ | Skip _ | Code_annot _ -> ()
+
+ | Set(lv,e,_) ->
+ let r = add_lval m s lv in
+ let v = add_exp m s e in
+ Memory.write m r (Lval(s,lv)) ;
+ Option.iter (Memory.add_points_to m r) v.ptr
+
+ | Local_init(x,AssignInit iv,_) ->
+ let acs = Access.Init(s,x) in
+ add_init m s acs (Var x,NoOffset) iv
+
+ | Call(lr,e,es,_) ->
+ add_value m s e ;
+ List.iter (add_value m s) es ;
+ Option.iter
+ (fun lv ->
+ let r = add_lval m s lv in
+ Memory.write m r (Lval(s,lv))
+ ) lr ;
+ Options.warning ~source:(fst @@ Stmt.loc s) "Incomplete call analysis"
+
+ | Local_init(_,ConsInit _,_) ->
+ Options.warning ~source:(fst @@ Stmt.loc s)
+ "Constructor init not yet implemented"
+ | Asm _ ->
+ Options.warning ~source:(fst @@ Stmt.loc s)
+ "Inline assembly not supported (ignored)"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Statements --- *)
+(* -------------------------------------------------------------------------- *)
+
+type rmap = Memory.map Stmt.Map.t ref
+
+let store rmap m s =
+ rmap := Stmt.Map.add s (Memory.copy ~locked:true m) !rmap
+
+let rec add_stmt (r:rmap) (m:map) (s:stmt) =
+ let annots = Annotations.code_annot s in
+ if annots <> [] then
+ Options.warning ~source:(fst @@ Stmt.loc s)
+ "Annotations not analyzed" ;
+ match s.skind with
+ | Instr ki -> add_instr m s ki ; store r m s
+ | Return(Some e,_) -> add_value m s e ; store r m s
+ | Goto _ | Break _ | Continue _ | Return(None,_) -> store r m s
+ | If(e,st,se,_) ->
+ add_value m s e ;
+ store r m s ;
+ add_block r m st ;
+ add_block r m se ;
+ | Switch(e,b,_,_) ->
+ add_value m s e ;
+ store r m s ;
+ add_block r m b ;
+ | Block b | Loop(_,b,_,_,_) -> add_block r m b
+ | UnspecifiedSequence s -> add_block r m @@ Cil.block_from_unspecified_sequence s
+ | Throw(exn,_) -> Option.iter (fun (e,_) -> add_value m s e) exn
+ | TryCatch(b,hs,_) ->
+ add_block r m b ;
+ List.iter (fun (c,b) -> add_catch r m c ; add_block r m b) hs ;
+ | TryExcept(a,(ks,e),b,_) ->
+ add_block r m a ;
+ List.iter (add_instr m s) ks ;
+ add_value m s e ;
+ add_block r m b ;
+ | TryFinally(a,b,_) ->
+ add_block r m a ;
+ add_block r m b ;
+
+and add_catch (r:rmap) (m:map) (c:catch_binder) =
+ match c with
+ | Catch_all -> ()
+ | Catch_exn(_,xbs) -> List.iter (fun (_,b) -> add_block r m b) xbs
+
+and add_block (r:rmap) (m:map) (b:block) =
+ List.iter (add_stmt r m) b.bstmts
+
+(* -------------------------------------------------------------------------- *)
+(* --- Behavior --- *)
+(* -------------------------------------------------------------------------- *)
+
+type imap = Memory.map Property.Map.t ref
+
+let istore imap m ip =
+ imap := Property.Map.add ip (Memory.copy ~locked:true m) !imap
+
+let add_bhv ~kf (s:imap) (m:map) (bhv:behavior) =
+ List.iter
+ (fun e ->
+ let rs = Annot.of_extension e in
+ if rs <> [] then
+ begin
+ List.iter (Logic.add_region m) rs ;
+ let ip = Property.ip_of_extended (ELContract kf) e in
+ istore s m ip ;
+ end
+ ) bhv.b_extended
+
+(* -------------------------------------------------------------------------- *)
+(* --- Function --- *)
+(* -------------------------------------------------------------------------- *)
+
+type domain = {
+ map : map ;
+ body : map Stmt.Map.t ;
+ spec : map Property.Map.t ;
+}
+
+let domain ?global kf =
+ let m = match global with Some g -> g | None -> Memory.create () in
+ let r = ref Stmt.Map.empty in
+ let s = ref Property.Map.empty in
+ begin
+ try
+ let funspec = Annotations.funspec kf in
+ List.iter (add_bhv ~kf s m) funspec.spec_behavior ;
+ with Annotations.No_funspec _ -> ()
+ end ;
+ begin
+ try
+ let fundec = Kernel_function.get_definition kf in
+ add_block r m fundec.sbody ;
+ with Kernel_function.No_Definition -> ()
+ end ;
+ {
+ map = Memory.copy ~locked:true m ;
+ body = !r ;
+ spec = !s ;
+ }
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/code.mli b/src/plugins/region/code.mli
new file mode 100644
index 0000000000000000000000000000000000000000..46cea3a9d8da0e6fc089aab9755498c699a2b022
--- /dev/null
+++ b/src/plugins/region/code.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+open Cil_datatype
+open Memory
+
+(** All the provided maps are locked. *)
+type domain = {
+ map : map ;
+ body : map Stmt.Map.t ;
+ spec : map Property.Map.t ;
+}
+
+(** The global map, if provided, is used as an accumulator. *)
+val domain : ?global:map -> kernel_function -> domain
diff --git a/src/plugins/region/dune b/src/plugins/region/dune
new file mode 100644
index 0000000000000000000000000000000000000000..f4f00f77e3abbaac66d5fb72b9b59018d629a236
--- /dev/null
+++ b/src/plugins/region/dune
@@ -0,0 +1,49 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action
+ (progn
+ (echo "Region:" %{lib-available:frama-c-region.core} "\n")
+ (echo " - Server:" %{lib-available:frama-c-server.core} "\n")
+ (echo " - UnionFind:" %{lib-available:unionFind} "\n"))))
+
+(env
+ (release
+ (flags -noassert)))
+
+(library
+ (name Region)
+ (public_name frama-c-region.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel frama-c-server.core unionFind)
+ (instrumentation (backend landmarks))
+ (instrumentation (backend bisect_ppx)))
+
+(plugin
+ (optional)
+ (name region)
+ (libraries frama-c-region.core)
+ (site
+ (frama-c plugins)))
diff --git a/src/plugins/region/dune-project b/src/plugins/region/dune-project
new file mode 100644
index 0000000000000000000000000000000000000000..cbfcc90d4ec4c33141700984567ea75170a167cb
--- /dev/null
+++ b/src/plugins/region/dune-project
@@ -0,0 +1,25 @@
+(lang dune 3.7)
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; 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). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(name frama-c-region)
+(using dune_site 0.1)
diff --git a/src/plugins/region/frama-c-region.opam b/src/plugins/region/frama-c-region.opam
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/src/plugins/region/logic.ml b/src/plugins/region/logic.ml
new file mode 100644
index 0000000000000000000000000000000000000000..6e68710a47566de2ab8c01fb50d348c2365e3707
--- /dev/null
+++ b/src/plugins/region/logic.ml
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(* *)
+(* 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 Annot
+open Memory
+
+let rec add_lval (m:map) (p:path): node =
+ match p.step with
+ | Var x -> add_root m x
+ | Field(lv,fd) -> Memory.add_field m (add_lval m lv) fd
+ | Index lv -> Memory.add_index m (add_lval m lv) lv.typ
+ | Star e | Cast(_,e) -> add_pointer m e
+ | Shift _ | AddrOf _ ->
+ Options.error ~source:(fst p.loc)
+ "Unexpected expression (l-value expected)" ;
+ Memory.add_cell m ()
+and add_pointer (m:map) (p:path): Memory.node =
+ match add_exp m p with
+ | None -> add_cell m ()
+ | Some r -> r
+
+and add_exp (m:map) (p:path): Memory.node option =
+ match p.step with
+ | (Var _ | Field _ | Index _ | Star _ | Cast _) ->
+ let r = add_lval m p in
+ add_value m r p.typ
+ | AddrOf p -> Some (add_lval m p)
+ | Shift p -> add_exp m p
+
+let add_region (m: map) (r : Annot.region) =
+ let rs = List.map (add_lval m) r.rpath in
+ merge_all m @@
+ match r.rname with
+ | None -> rs
+ | Some a -> add_label m a :: rs
diff --git a/src/plugins/region/logic.mli b/src/plugins/region/logic.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e5fb991d29aa65367eec51046aa0e15c3b86e6cf
--- /dev/null
+++ b/src/plugins/region/logic.mli
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(* *)
+(* 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 Memory
+
+val add_lval : map -> Annot.path -> node
+val add_exp : map -> Annot.path -> node option
+val add_region : map -> Annot.region -> unit
diff --git a/src/plugins/region/memory.ml b/src/plugins/region/memory.ml
new file mode 100644
index 0000000000000000000000000000000000000000..ac29123b225b9979e8d3ae8f8da320ce756307a4
--- /dev/null
+++ b/src/plugins/region/memory.ml
@@ -0,0 +1,513 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+open Cil_datatype
+module Ufind = UnionFind.Make(Store)
+module Vmap = Varinfo.Map
+module Vset = Varinfo.Set
+module Lmap = Map.Make(String)
+module Lset = Set.Make(String)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Maps --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* All offsets in bits *)
+
+type node = chunk Ufind.rref
+
+and layout =
+ | Blob
+ | Cell of int * node option
+ | Compound of int * node Ranges.t
+
+and chunk = {
+ cparents: node list ;
+ croots: Vset.t ;
+ clabels: Lset.t ;
+ creads: Access.Set.t ;
+ cwrites: Access.Set.t ;
+ cshifts: Access.Set.t ;
+ clayout: layout ;
+}
+
+type rg = node Ranges.range
+
+type map = {
+ store: chunk Ufind.store ;
+ mutable locked: bool ;
+ mutable roots: node Vmap.t ;
+ mutable labels: node Lmap.t ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Accessors --- *)
+(* -------------------------------------------------------------------------- *)
+
+let sizeof = function Blob -> 0 | Cell(s,_) | Compound(s,_) -> s
+let ranges = function Blob | Cell _ -> [] | Compound(_,R rs) -> rs
+let pointed = function Blob | Compound _ -> None | Cell(_,p) -> p
+
+let types (m : chunk) : 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.creads ;
+ Access.Set.iter add m.cwrites ;
+ Typ.Set.elements !pool
+
+let failwith_locked m fn =
+ if m.locked then raise (Invalid_argument fn)
+
+let lock m = m.locked <- true
+let unlock m = m.locked <- false
+
+(* -------------------------------------------------------------------------- *)
+(* --- Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
+let pp_node fmt (n : node) = Format.fprintf fmt "R%04x" @@ Store.id n
+
+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) ->
+ 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
+ ) rg ;
+ Format.fprintf fmt "@ }@]"
+
+let pp_chunk fmt (n: node) (m: chunk) =
+ 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.creads) (acs 'W' m.cwrites) (acs 'A' m.cshifts) ;
+ List.iter (Format.fprintf fmt "@ (%a)" Typ.pretty) (types m) ;
+ Lset.iter (Format.fprintf fmt "@ %s:") m.clabels ;
+ Vset.iter (Format.fprintf fmt "@ %a" Varinfo.pretty) m.croots ;
+ if Options.debug_atleast 1 then
+ begin
+ Access.Set.iter (Format.fprintf fmt "@ R:%a" Access.pretty) m.creads ;
+ Access.Set.iter (Format.fprintf fmt "@ W:%a" Access.pretty) m.cwrites ;
+ Access.Set.iter (Format.fprintf fmt "@ A:%a" Access.pretty) m.cshifts ;
+ end ;
+ Format.fprintf fmt "@ %a ;@]" pp_layout m.clayout ;
+ end
+[@@ warning "-32"]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Map Constructors --- *)
+(* -------------------------------------------------------------------------- *)
+
+let create () = {
+ locked = false ;
+ store = Ufind.new_store () ;
+ roots = Vmap.empty ;
+ labels = Lmap.empty ;
+}
+
+let copy ?locked m = {
+ locked = (match locked with None -> m.locked | Some l -> l) ;
+ store = Ufind.copy m.store ;
+ roots = m.roots ;
+ labels = m.labels ;
+}
+
+let empty = {
+ cparents = [] ;
+ croots = Vset.empty ;
+ clabels = Lset.empty ;
+ creads = Access.Set.empty ;
+ cwrites = Access.Set.empty ;
+ cshifts = Access.Set.empty ;
+ clayout = Blob ;
+}
+
+(* -------------------------------------------------------------------------- *)
+(* --- Map --- *)
+(* -------------------------------------------------------------------------- *)
+
+let id = Store.id
+let forge = Store.forge
+
+let node map node =
+ try Ufind.find map.store node
+ with Not_found -> node
+
+let nodes map ns = Store.list @@ List.map (node map) ns
+
+let get map node =
+ try Ufind.get map.store node
+ with Not_found -> empty
+
+(* -------------------------------------------------------------------------- *)
+(* --- Chunk Constructors --- *)
+(* -------------------------------------------------------------------------- *)
+
+let add_cell (m: map) ?size ?ptr ?root ?label () =
+ failwith_locked m "Region.Memory.add_cell" ;
+ let clayout = match size, ptr with
+ | None, None -> Blob
+ | None, Some _ -> Cell(Cil.bitsSizeOf Cil.voidPtrType,ptr)
+ | Some s, _ -> Cell(s,ptr) in
+ let croots = Vset.(match root with None -> empty | Some v -> singleton v) in
+ let clabels = Lset.(match label with None -> empty | Some a -> singleton a) in
+ Ufind.make m.store { empty with clayout ; croots ; clabels }
+
+let update (m: map) (n: node) (f: chunk -> chunk) =
+ let r = get m n in
+ Ufind.set m.store n (f r)
+
+let add_range (m: map) ~size ~offset ~length ~data : node =
+ failwith_locked m "Region.Memory.add_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 n = Ufind.make m.store { empty with clayout } in
+ update m data (fun r -> { r with cparents = nodes m @@ n :: r.cparents }) ; n
+
+let add_root (m: map) v =
+ try Vmap.find v m.roots with Not_found ->
+ failwith_locked m "Region.Memory.add_root" ;
+ let n = add_cell m ~root:v () in
+ m.roots <- Vmap.add v n m.roots ; n
+
+let add_label (m: map) a =
+ try Lmap.find a m.labels with Not_found ->
+ failwith_locked m "Region.Memory.add_label" ;
+ let n = add_cell m ~label:a () in
+ m.labels <- Lmap.add a n m.labels ; n
+
+(* -------------------------------------------------------------------------- *)
+(* --- Iterator --- *)
+(* -------------------------------------------------------------------------- *)
+
+type range = {
+ offset: int ;
+ length: int ;
+ cells: int ;
+ data: node ;
+}
+
+type region = {
+ node: node ;
+ parents: node list ;
+ roots: varinfo list ;
+ labels: string list ;
+ types: typ list ;
+ reads: Access.acs list ;
+ writes: Access.acs list ;
+ shifts: Access.acs list ;
+ sizeof: int ;
+ ranges: range list ;
+ pointed: node option ;
+}
+
+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
+
+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 ;
+ Format.fprintf fmt "@[<hv 0>" ;
+ List.iter (Format.fprintf fmt "@ %a" pp_range) m.ranges ;
+ Format.fprintf fmt "@]" ;
+ 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) (rg: rg) : range = {
+ offset = rg.offset ;
+ length = rg.length ;
+ cells = rg.length / sizeof (get m rg.data).clayout ;
+ data = node m rg.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 region map n = make_region map n (get map n)
+
+let rec walk h m f n =
+ let n = Ufind.find m.store n in
+ let id = Store.id n in
+ try Hashtbl.find h id with Not_found ->
+ Hashtbl.add h id () ;
+ let r = Ufind.get m.store n in
+ f (make_region m n r) ;
+ match r.clayout with
+ | Blob -> ()
+ | Cell(_,p) -> Option.iter (walk h m f) p
+ | Compound(_,rg) -> Ranges.iter (walk h m f) rg
+
+let iter (m:map) (f: region -> unit) =
+ let h = Hashtbl.create 0 in
+ Vmap.iter (fun _x n -> walk h m f n) m.roots
+
+let regions map =
+ let pool = ref [] in
+ iter map (fun r -> pool := r :: !pool) ;
+ List.rev !pool
+
+(* -------------------------------------------------------------------------- *)
+(* --- Merge --- *)
+(* -------------------------------------------------------------------------- *)
+
+type queue = (node * node) Queue.t
+
+let singleton ~size = function
+ | None -> Ranges.empty
+ | Some r -> Ranges.range ~length:size r
+
+let merge_node (m: map) (q: queue) (a: node) (b: node) : node =
+ if not @@ Ufind.eq m.store a b then Queue.push (a,b) q ;
+ Ufind.find m.store (min a b)
+
+let merge_opt (m: map) (q: queue)
+ (pa : node option) (pb : node option) : node option =
+ match pa, pb with
+ | None, p | p, None -> p
+ | Some pa, Some pb -> Some (merge_node m q pa pb)
+
+let merge_range (m: map) (q: queue) (ra : rg) (rb : rg) : node =
+ let na = ra.data in
+ let nb = rb.data in
+ let ma = ra.offset + ra.length in
+ let mb = rb.offset + rb.length in
+ let dp = ra.offset - rb.offset in
+ let dq = ma - mb in
+ let sa = sizeof (get m na).clayout in
+ let sb = sizeof (get m nb).clayout in
+ let size = Ranges.(sa %. sb %. dp %. dq) in
+ let data = merge_node m q na nb in
+ if size = sa && size = sb then data else
+ merge_node m q (add_cell m ~size ()) data
+
+let merge_ranges (m: map) (q: queue)
+ (sa : int) (wa : node Ranges.t)
+ (sb : int) (wb : node Ranges.t)
+ : layout =
+ if sa = sb then
+ Compound(sa, 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)
+
+let merge_layout (m: map) (q: queue) (a : layout) (b : layout) : layout =
+ match a, b with
+ | Blob, c | c, Blob -> c
+
+ | 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(sr,wr), Cell(sx,None) | Cell(sx,None), Compound(sr,wr) ->
+ let size = Ranges.gcd sx sr in
+ Compound(size, singleton ~size @@ Ranges.squash (merge_node m q) wr)
+
+ | Compound(sr,wr), Cell(sx,Some ptr) | Cell(sx,Some ptr), Compound(sr,wr) ->
+ let rp = add_cell m ~size:sx ~ptr () in
+ let wx = Ranges.range ~length:sx rp in
+ merge_ranges m q sx wx sr wr
+
+let merge_region (m: map) (q: queue) (a : chunk) (b : chunk) : chunk = {
+ cparents = nodes m @@ Store.bag a.cparents b.cparents ;
+ clabels = Lset.union a.clabels b.clabels ;
+ croots = Vset.union a.croots b.croots ;
+ creads = Access.Set.union a.creads b.creads ;
+ cwrites = Access.Set.union a.cwrites b.cwrites ;
+ cshifts = Access.Set.union a.cshifts b.cshifts ;
+ clayout = merge_layout m q a.clayout b.clayout ;
+}
+
+let do_merge (m: map) (q: queue) (a: node) (b: node): unit =
+ begin
+ let ra = Ufind.get m.store a in
+ let rb = Ufind.get m.store b in
+ let rx = Ufind.union m.store a b in
+ let rc = merge_region m q ra rb in
+ Ufind.set m.store rx rc ;
+ end
+
+let merge_all (m:map) = function
+ | [] -> ()
+ | r::rs ->
+ let q = Queue.create () in
+ List.iter (fun r' -> ignore @@ merge_node m q r r') rs ;
+ while not @@ Queue.is_empty q do
+ let a,b = Queue.pop q in
+ do_merge m q a b ;
+ done
+
+let merge (m: map) (a: node) (b: node) : node =
+ failwith_locked m "Region.Memory.merge" ;
+ merge_all m [a;b] ; Ufind.find m.store (min a b)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Offset --- *)
+(* -------------------------------------------------------------------------- *)
+
+let add_field (m:map) (r:node) (fd:fieldinfo) : node =
+ let ci = fd.fcomp in
+ if ci.cstruct then
+ let size = Cil.bitsSizeOf (TComp(ci,[])) in
+ let offset, length = Cil.fieldBitsOffset fd in
+ let data = add_cell m () in
+ let rc = add_range m ~size ~offset ~length ~data in
+ ignore @@ merge m r rc ; data
+ else r
+
+let add_index (m:map) (r:node) (ty:typ) : node =
+ let size = Cil.bitsSizeOf ty in
+ let data = add_cell m () in
+ let rc = add_range m ~size ~offset:0 ~length:size ~data in
+ ignore @@ merge m r rc ; data
+
+let add_points_to (m: map) (a: node) (b : node) =
+ failwith_locked m "Region.Memory.points_to" ;
+ ignore @@ merge m a @@ add_cell m ~ptr:b ()
+
+let add_value (m:map) (rv:node) (ty:typ) : node option =
+ if Cil.isPointerType ty then
+ let rp = add_cell m () in
+ add_points_to m rv rp ;
+ Some rp
+ else
+ None
+
+(* -------------------------------------------------------------------------- *)
+(* --- Access --- *)
+(* -------------------------------------------------------------------------- *)
+
+let access (m:map) (a:node) (ty: typ) =
+ let sr = sizeof (get m a).clayout in
+ let size = Ranges.gcd sr (Cil.bitsSizeOf ty) in
+ if sr <> size then ignore (merge m a (add_cell m ~size ()))
+
+let read (m: map) (a: node) from =
+ failwith_locked m "Region.Memory.read" ;
+ let r = get m a in
+ Ufind.set m.store a { r with creads = Access.Set.add from r.creads } ;
+ access m a (Access.typeof from)
+
+let write (m: map) (a: node) from =
+ failwith_locked m "Region.Memory.write" ;
+ let r = get m a in
+ Ufind.set m.store a { r with cwrites = Access.Set.add from r.cwrites } ;
+ access m a (Access.typeof from)
+
+let shift (m: map) (a: node) from =
+ failwith_locked m "Region.Memory.shift" ;
+ let r = get m a in
+ Ufind.set m.store a { r with cshifts = Access.Set.add from r.cshifts }
+(* no access *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Lookup ---- *)
+(* -------------------------------------------------------------------------- *)
+
+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
+
+let cpointed m r =
+ let rg = Ufind.get m.store r in
+ match rg.clayout with
+ | Blob | Compound _ | Cell(_,None) -> None
+ | Cell(_,Some r) -> Some (Ufind.find m.store r)
+
+let rec lval (m: map) (lv: lval) : node =
+ let h = host m (fst lv) in
+ offset m h (snd lv)
+
+and host (m: map) (h: lhost) : node =
+ match h with
+ | Var x -> Ufind.find m.store @@ Vmap.find x m.roots
+ | Mem e ->
+ match exp m e with
+ | None -> raise Not_found
+ | Some r -> r
+
+and offset (m: map) (r: node) (ofs: offset) : node =
+ match ofs with
+ | NoOffset -> Ufind.find m.store r
+ | Field (fd, ofs) ->
+ if fd.fcomp.cstruct then
+ let _, rgs = cranges m r in
+ let (p,w) = Cil.fieldBitsOffset fd in
+ let rg = Ranges.find p rgs in
+ if rg.offset <= p && p+w <= rg.offset + rg.length then
+ offset m rg.data ofs
+ else raise Not_found
+ else r
+ | Index (_, ofs) ->
+ let s, rgs = cranges m r in
+ match rgs with
+ | R [rg] when rg.offset = 0 && rg.length = s ->
+ offset m rg.data ofs
+ | _ -> raise Not_found
+
+and exp (m: map) (e: exp) : node option =
+ match e.enode with
+ | Const _
+ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _ -> None
+ | Lval lv -> cpointed m @@ lval m lv
+ | AddrOf lv | StartOf lv -> Some (lval m lv)
+ | CastE(_, e) -> exp m e
+ | BinOp((PlusPI|MinusPI),p,_,_) -> exp m p
+ | UnOp (_, _, _) | BinOp (_, _, _, _) -> None
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/memory.mli b/src/plugins/region/memory.mli
new file mode 100644
index 0000000000000000000000000000000000000000..79a0543ef0d220ca2a4da29b4be20a8f570f899d
--- /dev/null
+++ b/src/plugins/region/memory.mli
@@ -0,0 +1,95 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_types
+
+type node
+
+type range = {
+ offset: int ;
+ length: int ;
+ cells: int ;
+ data: node ;
+}
+
+type region = {
+ node: node ;
+ parents: node list ;
+ roots: varinfo list ;
+ labels: string list ;
+ types: typ list ;
+ reads: Access.acs list ;
+ writes: Access.acs list ;
+ shifts: Access.acs list ;
+ sizeof: int ;
+ ranges: range list ;
+ pointed: node option ;
+}
+
+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. *)
+val create : unit -> map
+
+(** Default locked status is inherited from the copied map. *)
+val copy : ?locked:bool -> map -> map
+
+(** Lock the map. No more access nor merge can be added into the map. *)
+val lock : map -> unit
+
+(** Unlock the map. *)
+val unlock : map -> unit
+
+val id : node -> int
+val forge : int -> node
+val node : map -> node -> node
+val nodes : map -> node list -> node list
+
+val iter : map -> (region -> unit) -> unit
+val region : map -> node -> region
+val regions : map -> region list
+
+val add_root : map -> Cil_types.varinfo -> node
+val add_label : map -> string -> node
+val add_cell : map -> ?size:int -> ?ptr:node -> ?root:varinfo -> ?label:string -> unit -> node
+val add_range : map -> size:int -> offset:int -> length:int -> data:node -> node
+val add_field : map -> node -> fieldinfo -> node
+val add_index : map -> node -> typ -> node
+val add_points_to : map -> node -> node -> unit
+val add_value : map -> node -> typ -> node option
+
+val read : map -> node -> Access.acs -> unit
+val write : map -> node -> Access.acs -> unit
+val shift : map -> node -> Access.acs -> unit
+
+val merge : map -> node -> node -> node
+val merge_all : map -> node list -> unit
+
+(** @raise Not_found *)
+val lval : map -> lval -> node
+
+(** @raise Not_found *)
+val exp : map -> exp -> node option
diff --git a/src/plugins/region/options.ml b/src/plugins/region/options.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5bc8f5b2d7fef1402b6783e4975098876ecd6836
--- /dev/null
+++ b/src/plugins/region/options.ml
@@ -0,0 +1,38 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Plugin Registration --- *)
+(* -------------------------------------------------------------------------- *)
+
+include Plugin.Register
+ (struct
+ let name = "Region Analysis"
+ let help = "Memory Region Analysis (experimental)"
+ let shortname = "region"
+ end)
+
+module Enabled = False
+ (struct
+ let option_name = "-region"
+ let help = "Enable Region Analysis"
+ end)
diff --git a/src/plugins/region/options.mli b/src/plugins/region/options.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8aba69998a130c61bbe960c3dda7fc546eb25e66
--- /dev/null
+++ b/src/plugins/region/options.mli
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Region Command Line Interface *)
+
+open Parameter_sig
+include Log.Messages
+
+module Enabled : Bool
diff --git a/src/plugins/region/ranges.ml b/src/plugins/region/ranges.ml
new file mode 100644
index 0000000000000000000000000000000000000000..54e7cc2c43fc0d8864f4332f1de80d8006c647f3
--- /dev/null
+++ b/src/plugins/region/ranges.ml
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+let rec gcd a b =
+ if a = 0 then abs b else
+ if b = 0 then abs a else
+ gcd b (a mod b)
+
+let (%.) = gcd
+
+(* -------------------------------------------------------------------------- *)
+(* --- Range Maps --- *)
+(* -------------------------------------------------------------------------- *)
+
+type 'a range = {
+ offset: int ;
+ length: int ;
+ data: 'a ;
+}
+
+let pp_range fmt r =
+ Format.fprintf fmt "%04d..%04d" r.offset (r.offset + r.length - 1)
+
+let pp_offset fmt r =
+ Format.fprintf fmt "%04d:%04d" r.offset r.length
+
+type 'a t = R of 'a range list (* sorted, no-overlap *)
+
+let empty = R []
+
+let singleton r =
+ if not (0 <= r.offset && 0 < r.length) then
+ raise (Invalid_argument "Region.Ranges.singleton") ;
+ R [r]
+
+let range ?(offset=0) ?(length=1) data = singleton { offset ; length ; data }
+
+let rec find (k: int) = function
+ | [] -> raise Not_found
+ | ({ offset ; length } as r) :: rs ->
+ if offset <= k && k <= offset + length then r else find k rs
+
+let find k (R rs) = find k rs
+
+let rec merge f ra rb =
+ match ra, rb with
+ | [], rs | rs, [] -> rs
+ | a :: wa, b :: wb ->
+ let a' = a.offset + a.length in
+ let b' = b.offset + b.length in
+ if a' <= b.offset then
+ a :: merge f wa rb
+ else
+ if b' < a.offset then
+ b :: merge f ra wb
+ else
+ let offset = min a.offset b.offset in
+ let length = max a' b' - offset in
+ let data = f a b in
+ let r = { offset ; length ; data } in
+ if a' < b'
+ then merge f wa (r::wb)
+ else merge f (r::wa) wb
+
+let merge f (R x) (R y) = R (merge f x y)
+
+let squash f = function
+ | R [] -> None
+ | R (x::xs) -> Some (List.fold_left (fun w r -> f w r.data) x.data xs)
+
+let iteri f (R xs) = List.iter f xs
+let iter f (R xs) = List.iter (fun r -> f r.data) xs
+let map f (R xs) = R (List.map (fun r -> { r with data = f r.data }) xs)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/ranges.mli b/src/plugins/region/ranges.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b04c273feb06930e56c6d996efe8688f8519dd86
--- /dev/null
+++ b/src/plugins/region/ranges.mli
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val gcd : int -> int -> int
+val (%.) : int -> int -> int (** gcd *)
+
+type 'a range = { offset : int; length : int; data : 'a; }
+type 'a t = private R of 'a range list (* sorted, no overlap *)
+
+(** Prints [offset..last] formatted with [%04d] *)
+val pp_range : Format.formatter -> 'a range -> unit
+
+(** Prints [offset:length] formatted with [%04d] *)
+val pp_offset : Format.formatter -> 'a range -> unit
+
+val empty : 'a t
+val singleton : 'a range -> 'a t
+val range : ?offset:int -> ?length:int -> 'a -> 'a t
+val merge : ('a range -> 'a range -> 'a) -> 'a t -> 'a t -> 'a t
+val squash : ('a -> 'a -> 'a) -> 'a t -> 'a option
+
+val find : int -> 'a t -> 'a range
+val map : ('a -> 'b) -> 'a t -> 'b t
+val iter : ('a -> unit) -> 'a t -> unit
+val iteri : ('a range -> unit) -> 'a t -> unit
diff --git a/src/plugins/region/register.ml b/src/plugins/region/register.ml
new file mode 100644
index 0000000000000000000000000000000000000000..54cd5cdd62b1d0f0a2e294a2b7ebce49a6390fca
--- /dev/null
+++ b/src/plugins/region/register.ml
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module R = Options
+
+(* -------------------------------------------------------------------------- *)
+(* --- Region Analysis Main Entry Point --- *)
+(* -------------------------------------------------------------------------- *)
+
+let main () =
+ if R.Enabled.get () then
+ begin
+ Ast.compute () ;
+ R.feedback "Analyzing regions" ;
+ Globals.Functions.iter Analysis.compute ;
+ end
+
+let () = Boot.Main.extend main
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0b5ab56eeec696b105255e42145de87b0b25027d
--- /dev/null
+++ b/src/plugins/region/services.ml
@@ -0,0 +1,262 @@
+(**************************************************************************)
+(* *)
+(* 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 Cil_datatype
+open Server
+module Md = Markdown
+
+let package = Package.package ~plugin:"region" ~title:"Region Analysis" ()
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server Data --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Node : Data.S with type t = Memory.node =
+struct
+ type t = Memory.node
+ let jtype = Data.declare ~package ~name:"node" (Jindex "node")
+ let to_json n = Json.of_int @@ Memory.id n
+ let of_json js = Memory.forge @@ Json.int js
+end
+
+module NodeOpt = Data.Joption(Node)
+module NodeList = Data.Jlist(Node)
+
+module Range : Data.S with type t = Memory.range =
+struct
+ type t = Memory.range
+ let jtype = Data.declare ~package ~name:"range" @@
+ Jrecord [
+ "offset", Jnumber ;
+ "length", Jnumber ;
+ "cells", Jnumber ;
+ "data", Node.jtype ;
+ ]
+ let to_json (rg : Memory.range) =
+ Json.of_fields [
+ "offset", Json.of_int rg.offset ;
+ "length", Json.of_int rg.length ;
+ "cells", Json.of_int rg.cells ;
+ "data", Node.to_json rg.data ;
+ ]
+ let of_json _ = failwith "Region.Range.of_json"
+end
+
+module Ranges = Data.Jlist(Range)
+
+module Region: Data.S with type t = Memory.region =
+struct
+ type t = Memory.region
+
+ let roots_to_json vs =
+ let open Cil_types in
+ Json.of_list @@ List.map (fun v -> Json.of_string v.vname) vs
+
+ let labels_to_json ls =
+ Json.of_list @@ List.map Json.of_string ls
+
+ let ikind_to_char (ikind : Cil_types.ikind) =
+ match ikind with
+ | IBool | IUChar -> 'b'
+ | IChar | ISChar -> 'c'
+ | IInt -> 'i'
+ | IUInt -> 'u'
+ | IShort -> 's'
+ | IUShort -> 'r'
+ | ILong | ILongLong -> 'l'
+ | IULong | IULongLong -> 'w'
+
+ let fkind_to_char (fkind : Cil_types.fkind) =
+ match fkind with
+ | FFloat -> 'f'
+ | FDouble | FLongDouble -> 'd'
+
+ let typ_to_char (ty: Cil_types.typ) =
+ match ty with
+ | TVoid _ -> 'b'
+ | TPtr _ -> 'p'
+ | TInt(ik,_) -> ikind_to_char ik
+ | TFloat(fk,_) -> fkind_to_char fk
+ | TComp({ cstruct }, _) -> if cstruct then 'S' else 'U'
+ | TArray _ -> 'A'
+ | TNamed _ -> 'T'
+ | TEnum _ -> 'E'
+ | TFun _ -> 'F'
+ | TBuiltin_va_list _ -> 'x'
+
+ let typs_to_char (typs : Cil_types.typ list) =
+ match typs with
+ | [] -> '-'
+ | [ty] -> typ_to_char ty
+ | _ -> 'x'
+
+ let label (m: Memory.region) =
+ let buffer = Buffer.create 4 in
+ if m.reads <> [] then Buffer.add_char buffer 'R' ;
+ if m.writes <> [] then Buffer.add_char buffer 'W' ;
+ if m.pointed <> None then Buffer.add_char buffer '*'
+ else if m.reads <> [] || m.writes <> [] then
+ begin
+ Buffer.add_char buffer '(' ;
+ Buffer.add_char buffer @@ typs_to_char m.types ;
+ Buffer.add_char buffer ')' ;
+ end ;
+ Buffer.contents buffer
+
+ let pp_typ_layout s0 fmt ty =
+ let s = Cil.bitsSizeOf ty in
+ if s <> s0 then
+ Format.fprintf fmt "(%a)%%%db" Typ.pretty ty s
+ else
+ Typ.pretty fmt ty
+
+ let title (m: Memory.region) =
+ Format.asprintf "%t (%db)"
+ begin fun fmt ->
+ match m.types with
+ | [] -> Format.pp_print_string fmt "Compound"
+ | [ty] -> pp_typ_layout m.sizeof fmt ty ;
+ | ty::ts ->
+ pp_typ_layout 0 fmt ty ;
+ List.iter (Format.fprintf fmt ", %a" (pp_typ_layout 0)) ts ;
+ end m.sizeof
+
+ let jtype = Data.declare ~package ~name:"region" @@
+ Jrecord [
+ "node", Node.jtype ;
+ "roots", Jarray Jalpha ;
+ "labels", Jarray Jalpha ;
+ "parents", NodeList.jtype ;
+ "sizeof", Jnumber ;
+ "ranges", Ranges.jtype ;
+ "pointed", NodeOpt.jtype ;
+ "reads", Jboolean ;
+ "writes", Jboolean ;
+ "bytes", Jboolean ;
+ "label", Jstring ;
+ "title", Jstring ;
+ ]
+
+ let to_json (m: Memory.region) =
+ Json.of_fields [
+ "node", Node.to_json m.node ;
+ "roots", roots_to_json m.roots ;
+ "labels", labels_to_json m.labels ;
+ "parents", NodeList.to_json m.parents ;
+ "sizeof", Json.of_int @@ m.sizeof ;
+ "ranges", Ranges.to_json @@ m.ranges ;
+ "pointed", NodeOpt.to_json @@ m.pointed ;
+ "reads", Json.of_bool (m.reads <> []) ;
+ "writes", Json.of_bool (m.writes <> []) ;
+ "bytes", Json.of_bool (List.length m.types > 1) ;
+ "label", Json.of_string @@ label m ;
+ "title", Json.of_string @@ title m ;
+ ]
+
+ let of_json _ = failwith "Region.Layout.of_json"
+end
+
+module Regions = Data.Jlist(Region)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server API --- *)
+(* -------------------------------------------------------------------------- *)
+
+let map_of_localizable ~local (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
+ match ki_of_localizable loc with
+ | Kglobal -> domain.map
+ | Kstmt s -> Stmt.Map.find s domain.body
+ else domain.map
+
+let region_of_localizable (m: Memory.map) (loc: Printer_tag.localizable) =
+ try
+ match loc with
+ | PExp(_,_,e) -> Memory.exp m e
+ | PLval(_,_,lv) -> Some (Memory.lval m lv)
+ | PVDecl(_,_,x) -> Some (Memory.lval m (Var x,NoOffset))
+ | PStmt _ | PStmtStart _
+ | PTermLval _ | PGlobal _ | PIP _ | PType _ -> None
+ with Not_found -> None
+
+let map_of_declaration (decl : Printer_tag.declaration) =
+ match decl with
+ | SFunction kf -> (Analysis.find kf).map
+ | _ -> raise Not_found
+
+let signal = Request.signal ~package ~name:"updated"
+ ~descr:(Md.plain "Region Analysis Updated")
+
+let () = Analysis.add_hook (fun () -> Request.emit signal)
+
+let () =
+ Request.register
+ ~package ~kind:`EXEC ~name:"compute"
+ ~descr:(Md.plain "Compute regions for the given declaration")
+ ~input:(module Kernel_ast.Decl)
+ ~output:(module Data.Junit)
+ (function SFunction kf -> Analysis.compute kf | _ -> ())
+
+let () =
+ Request.register
+ ~package ~kind:`GET ~name:"regions"
+ ~descr:(Md.plain "Returns computed regions for the given declaration")
+ ~input:(module Kernel_ast.Decl)
+ ~output:(module Regions)
+ ~signals:[signal]
+ begin fun decl ->
+ try Memory.regions @@ map_of_declaration decl
+ with Not_found -> []
+ end
+
+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))
+ ~output:(module Regions)
+ ~signals:[signal]
+ begin fun (loc,local) ->
+ try Memory.regions @@ map_of_localizable ~local 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))
+ ~output:(module NodeOpt)
+ ~signals:[signal]
+ begin fun (loc,local) ->
+ try
+ let map = map_of_localizable ~local loc in
+ region_of_localizable map loc
+ with Not_found -> None
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/region/services.mli b/src/plugins/region/services.mli
new file mode 100644
index 0000000000000000000000000000000000000000..2507b13f97d60fac6b22584dd12c0d4bac2f15e5
--- /dev/null
+++ b/src/plugins/region/services.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* 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 Server
+open Request
+
+val package : Package.package
+
+module Node : Data.S with type t = Memory.node
+module Range : Output with type t = Memory.range
+module Region : Output with type t = Memory.region
diff --git a/src/plugins/region/store.ml b/src/plugins/region/store.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4e964e42b373265fedea995c5665efd92e916e39
--- /dev/null
+++ b/src/plugins/region/store.ml
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- UnionFind Store with explicit integer keys --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Imap = Map.Make(Int)
+
+type 'a rref = int
+type 'a store = 'a Imap.t ref
+
+let new_store () = ref Imap.empty
+let copy r = ref !r
+let rid = ref 0
+
+let make s v =
+ let k = incr rid ; !rid in
+ s := Imap.add k v !s ; k
+
+let get s k = Imap.find k !s
+let set s k v = s := Imap.add k v !s
+
+let eq _s i j = (i == j)
+
+let id x = x
+let forge x = x
+let list = List.sort_uniq Int.compare
+let rec bag a b =
+ match a, b with
+ | [], c | c, [] -> c
+ | x::xs, y::ys -> x :: y :: bag xs ys
diff --git a/src/plugins/region/store.mli b/src/plugins/region/store.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3d9b60a6e02e310ddfd3827ec2d2f872f304f93a
--- /dev/null
+++ b/src/plugins/region/store.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include UnionFind.STORE
+
+(** Global unique identifier *)
+val id : 'a rref -> int
+
+(** Unordered union *)
+val bag: 'a list -> 'a list -> 'a list
+
+(** Sorted, unique *)
+val list : 'a rref list -> 'a rref list
+
+(**/**)
+val forge : int -> 'a rref
diff --git a/src/plugins/region/tests/ptests_config b/src/plugins/region/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..316166170520da8ec5a4067d38647cf887490c58
--- /dev/null
+++ b/src/plugins/region/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= region
diff --git a/src/plugins/region/tests/region/array1.i b/src/plugins/region/tests/region/array1.i
new file mode 100644
index 0000000000000000000000000000000000000000..eac00551a13634c34e79f284c7a0bebb362b0591
--- /dev/null
+++ b/src/plugins/region/tests/region/array1.i
@@ -0,0 +1,8 @@
+//@ region *p, *q ;
+int job( int n, int * p , int * q )
+{
+ int s = 0 ;
+ for (int k = 0; k < n; k++)
+ s += p[k] * q[k] ;
+ return s ;
+}
diff --git a/src/plugins/region/tests/region/array2.i b/src/plugins/region/tests/region/array2.i
new file mode 100644
index 0000000000000000000000000000000000000000..a9cbb53d7fffb400ff1c5b11512d50550682a934
--- /dev/null
+++ b/src/plugins/region/tests/region/array2.i
@@ -0,0 +1,8 @@
+//@ region P: *p, Q: *q ;
+int job( int n, int * p , int * q )
+{
+ int s = 0 ;
+ for (int k = 0; k < n; k++)
+ s += p[k] * q[k] ;
+ return s ;
+}
diff --git a/src/plugins/region/tests/region/fb_ADD.i b/src/plugins/region/tests/region/fb_ADD.i
new file mode 100644
index 0000000000000000000000000000000000000000..8ceb168c7af4dbce81e6776ee4fffd4b2c838ae7
--- /dev/null
+++ b/src/plugins/region/tests/region/fb_ADD.i
@@ -0,0 +1,22 @@
+typedef struct N { double v ; int s ; } *SN ;
+typedef struct L { int v ; int s ; } *SL ;
+
+typedef struct Block {
+ SN prm ;
+ SN inp1 ;
+ SN inp2 ;
+ SN inp3 ;
+ SN out1 ;
+ SN out2 ;
+ SN out3 ;
+ SL idx1 ;
+ SL idx2 ;
+ SL idx3 ;
+ SN sum ;
+} FB ;
+
+void job(FB *fb)
+{
+ fb->out1->v = fb->out1->v + fb->out2->v ;
+ fb->out1->s = fb->out1->s | fb->out2->s ;
+}
diff --git a/src/plugins/region/tests/region/fb_SORT.i b/src/plugins/region/tests/region/fb_SORT.i
new file mode 100644
index 0000000000000000000000000000000000000000..4ef65d2cfb6145f4c3266320fbeed7b8c7eb4145
--- /dev/null
+++ b/src/plugins/region/tests/region/fb_SORT.i
@@ -0,0 +1,38 @@
+typedef struct N { double v ; int s ; } *SN ;
+typedef struct L { int v ; int s ; } *SL ;
+
+typedef struct Block {
+ SN prm ;
+ SN inp1 ;
+ SN inp2 ;
+ SN inp3 ;
+ SN out1 ;
+ SN out2 ;
+ SN out3 ;
+ SL idx1 ;
+ SL idx2 ;
+ SL idx3 ;
+ SN sum ;
+} FB ;
+
+void job(FB *fb)
+{
+ SN *inp = &(fb->inp1) ;
+ SN *out = &(fb->out1) ;
+ SL *idx = &(fb->idx1) ;
+
+ for (int i = 0; i < 3; i++) {
+ out[i]->v = inp[i]->v + fb->prm->v ;
+ out[i]->s = 0 ;
+ idx[i]->v = inp[i]->s ;
+ idx[i]->s = 0 ;
+ }
+
+ fb->sum->v =
+ fb->out1->v +
+ fb->out2->v +
+ fb->out3->v ;
+
+ fb->sum->s = 0 ;
+
+}
diff --git a/src/plugins/region/tests/region/garbled.i b/src/plugins/region/tests/region/garbled.i
new file mode 100644
index 0000000000000000000000000000000000000000..6b703ba4245ba130e45827ac182b69f5dd03dfdd
--- /dev/null
+++ b/src/plugins/region/tests/region/garbled.i
@@ -0,0 +1,6 @@
+
+
+float job(int *p,int *q)
+{
+ return *q + *(float*)p + *p ;
+}
diff --git a/src/plugins/region/tests/region/oracle/array1.res.oracle b/src/plugins/region/tests/region/oracle/array1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..32aa817c98cb58cf497d73bf7b882b710c6f01aa
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/array1.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing array1.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R000b: R-- n (int) 32b ;
+ R0004: R-A p (int *) 64b (*R0002) ;
+ R0002: R-- (int) 32b ;
+ R0001: R-A q (int *) 64b (*R0002) ;
+ R0007: RW- s (int) 32b ;
+ R0009: RW- k (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/array2.res.oracle b/src/plugins/region/tests/region/oracle/array2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..03db359956cffee155c75a0a93f0336392dcd450
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/array2.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing array2.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R000d: R-- n (int) 32b ;
+ R0001: R-A p (int *) 64b (*R0004) ;
+ R0004: R-- P: (int) 32b ;
+ R0005: R-A q (int *) 64b (*R0008) ;
+ R0008: R-- Q: (int) 32b ;
+ R0009: RW- s (int) 32b ;
+ R000b: RW- k (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..84e4fe84a136c3e51118270f99079d75072b4153
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing fb_ADD.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0001: R-- fb (FB *) 64b (*R0003) ;
+ R0003: --- 704b 256..320 [1]: R0005 320..384 [1]: R0018 ;
+ R0005: R-- (struct N *) 64b (*R0008) ;
+ R0008: --- 128b 0..64 [1]: R000a 64..96 [1]: R0027 ;
+ R000a: RW- (double) 64b ;
+ R0027: RW- (int) 32b ;
+ R0018: R-- (struct N *) 64b (*R001b) ;
+ R001b: --- 128b 0..64 [1]: R001d 64..96 [1]: R003a ;
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..912201cee70ff9cb9ad26b705ce0a1674f0ab3e1
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -0,0 +1,33 @@
+[kernel] Parsing fb_SORT.i (no preprocessing)
+[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 ;
+ R0007: R-- (struct N *) 64b (*R0024) ;
+ R0024: --- 128b 0..64 [1]: R0026 64..96 [1]: R0046 ;
+ R0026: R-- (double) 64b ;
+ R0046: R-- (int) 32b ;
+ R000e: R-- (struct N *) 64b (*R001d) ;
+ R001d: --- 128b 0..64 [1]: R001f 64..96 [1]: R0038 ;
+ R001f: RW- (double) 64b ;
+ R0038: -W- (int) 32b ;
+ R0066: R-- (struct N *) 64b (*R0069) ;
+ R0069: --- 128b 0..64 [1]: R006b ;
+ R006b: R-- (double) 64b ;
+ R0015: R-- (struct N *) (struct L *) 64b (*R003e) ;
+ R003e: --- 64b 0..64 [2]: R0040 ;
+ R0040: RW- (int) (double) 32b ;
+ R0053: R-- (struct N *) 64b (*R0056) ;
+ R0056: --- 128b 0..64 [1]: R0058 64..96 [1]: R007f ;
+ R0058: -W- (double) 64b ;
+ R007f: -W- (int) 32b ;
+ R0001: RWA inp (SN *) 64b (*R0007) ;
+ R000a: RWA out (SN *) 64b (*R000e) ;
+ R0011: RWA idx (SL *) 64b (*R0015) ;
+ R0018: RW- i (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/garbled.res.oracle b/src/plugins/region/tests/region/oracle/garbled.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..024e97e7a347465d0c35c9340e432a711cbe9d92
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/garbled.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing garbled.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0007: R-- p (int *) 64b (*R0009) ;
+ R0009: R-- (int) (float) 32b ;
+ R0002: R-- q (int *) 64b (*R0004) ;
+ R0004: R-- (int) 32b ;
+ R0001: RW- __retres (float) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/swap.res.oracle b/src/plugins/region/tests/region/oracle/swap.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3117fb686d5ee476901cd95a19ab05fd51194ca0
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/swap.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing swap.i (no preprocessing)
+[region] Analyzing regions
+[region] Function swap_aliased:
+ R0004: R-- a (int *) 64b (*R0007) ;
+ R0007: RW- R: (int) 32b ;
+ R0001: R-- b (int *) 64b (*R0007) ;
+ R0008: RW- tmp (int) 32b ;
+[region] Function swap_separated:
+ R0013: R-- a (int *) 64b (*R0016) ;
+ R0016: RW- A: (int) 32b ;
+ R0017: R-- b (int *) 64b (*R001a) ;
+ R001a: RW- B: (int) 32b ;
+ R001b: RW- tmp (int) 32b ;
diff --git a/src/plugins/region/tests/region/swap.i b/src/plugins/region/tests/region/swap.i
new file mode 100644
index 0000000000000000000000000000000000000000..04816ea5fd84319d9dad1009e3cbdb643cea9272
--- /dev/null
+++ b/src/plugins/region/tests/region/swap.i
@@ -0,0 +1,29 @@
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region A: *a, B: *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_separated(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
+
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region R: *a, *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_aliased(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
diff --git a/src/plugins/region/tests/test_config b/src/plugins/region/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..4772d6b36660012dd7b95cfdc8bed12676c83fb1
--- /dev/null
+++ b/src/plugins/region/tests/test_config
@@ -0,0 +1,2 @@
+PLUGIN: region
+OPT: -region
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 5943bf96b4fa603a22956eea666dafb2db5450a6..365ac6ec02a55a33b4f1376f5540718658d92d64 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -88,16 +88,14 @@ module Joption(A : S) : S with type t = A.t option =
struct
type t = A.t option
- let nullable = try ignore (A.of_json `Null) ; true with _ -> false
- let jtype = Joption (if not nullable then A.jtype else Jtuple [A.jtype])
+ let jtype = Joption A.jtype
let to_json = function
| None -> `Null
- | Some v -> if nullable then `List [A.to_json v] else A.to_json v
+ | Some v -> A.to_json v
let of_json = function
| `Null -> None
- | `List [js] when nullable -> Some (A.of_json js)
| js -> Some (A.of_json js)
end
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index dd4561560a3c2d839554448924670aa65437006b..f2697affd43569089fda263bbf4cb02213b1f987 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -468,7 +468,7 @@ let typecheck typing_context _loc ps =
let of_extid = Hashtbl.find registry
let of_extrev = function
- | { ext_name="region" ; ext_kind = Ext_id k } -> of_extid k
+ | { ext_name="wpregion" ; ext_kind = Ext_id k } -> of_extid k
| _ -> raise Not_found
let of_extension e = List.rev (of_extrev e)
let of_behavior bhv =
@@ -498,7 +498,7 @@ let register () =
then
begin
registered := true ;
- Acsl_extension.register_behavior ~plugin:"wp" "region"
+ Acsl_extension.register_behavior ~plugin:"wp" "wpregion"
typecheck ~printer:pp_extension false
end
diff --git a/src/plugins/wp/tests/wp_region/annot.i b/src/plugins/wp/tests/wp_region/annot.i
index e141f13431ac5907cd8a06d8b5d17392d761195d..2312dafd8a402817ff5cc572dee05384826bd01c 100644
--- a/src/plugins/wp/tests/wp_region/annot.i
+++ b/src/plugins/wp/tests/wp_region/annot.i
@@ -31,7 +31,7 @@ typedef struct Block {
SN sum ;
} FB ;
-//@ \wp::region *fb ;
+//@ \wp::wpregion *fb ;
void fb_ADD(FB *fb)
{
fb->out1->v = fb->out1->v + fb->out2->v ;
@@ -39,9 +39,9 @@ void fb_ADD(FB *fb)
}
/*@
- \wp::region IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
- \wp::region OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
- \wp::region IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
+ \wp::wpregion IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
+ \wp::wpregion OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
+ \wp::wpregion IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
*/
void fb_SORT(FB *fb)
{
diff --git a/src/plugins/wp/tests/wp_region/annot/a.i b/src/plugins/wp/tests/wp_region/annot/a.i
index e684198b0e99768b84e7c3cf7aa9135e77220c27..fb6d84c2cb8cf463ae9e13dd1b6a159325899843 100644
--- a/src/plugins/wp/tests/wp_region/annot/a.i
+++ b/src/plugins/wp/tests/wp_region/annot/a.i
@@ -24,7 +24,7 @@ struct Block {
};
typedef struct Block FB;
/*@ terminates \true;
- \wp::region *fb; */
+ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
}
/*@ terminates \true;
- \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
- \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
- \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+ \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+ \wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
+ \wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
@@ -56,5 +56,3 @@ void fb_SORT(FB *fb)
(fb->sum)->s = 0;
return;
}
-
-
diff --git a/src/plugins/wp/tests/wp_region/annot/b.i b/src/plugins/wp/tests/wp_region/annot/b.i
index e684198b0e99768b84e7c3cf7aa9135e77220c27..fb6d84c2cb8cf463ae9e13dd1b6a159325899843 100644
--- a/src/plugins/wp/tests/wp_region/annot/b.i
+++ b/src/plugins/wp/tests/wp_region/annot/b.i
@@ -24,7 +24,7 @@ struct Block {
};
typedef struct Block FB;
/*@ terminates \true;
- \wp::region *fb; */
+ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
}
/*@ terminates \true;
- \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
- \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
- \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+ \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+ \wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
+ \wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
@@ -56,5 +56,3 @@ void fb_SORT(FB *fb)
(fb->sum)->s = 0;
return;
}
-
-
diff --git a/src/plugins/wp/tests/wp_region/array1.i b/src/plugins/wp/tests/wp_region/array1.i
index e7b235b05c2dae8fb2c2fc358b0b5a3b69461907..bf3da7a503c8df46be495fd87a2d73c2c600b6c6 100644
--- a/src/plugins/wp/tests/wp_region/array1.i
+++ b/src/plugins/wp/tests/wp_region/array1.i
@@ -1,4 +1,4 @@
-//@ \wp::region *p, *q ;
+//@ \wp::wpregion *p, *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
diff --git a/src/plugins/wp/tests/wp_region/array2.i b/src/plugins/wp/tests/wp_region/array2.i
index 1bc2f1baac572e05e322c75b69d676f993d21501..be59f8c030d72f6deb45f68ddcb7e2102e840a61 100644
--- a/src/plugins/wp/tests/wp_region/array2.i
+++ b/src/plugins/wp/tests/wp_region/array2.i
@@ -1,4 +1,4 @@
-//@ \wp::region *p; \wp::region *q ;
+//@ \wp::wpregion *p; \wp::wpregion *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
diff --git a/src/plugins/wp/tests/wp_region/fb_ADD.i b/src/plugins/wp/tests/wp_region/fb_ADD.i
index 2c939c92e0be417532ac6033f0fa9de7dc04779f..dc378f6d5e6eab79016343050256ad68545f2b7e 100644
--- a/src/plugins/wp/tests/wp_region/fb_ADD.i
+++ b/src/plugins/wp/tests/wp_region/fb_ADD.i
@@ -16,7 +16,7 @@ typedef struct Block {
} FB ;
/*@
- \wp::region A: fb ;
+ \wp::wpregion A: fb ;
*/
void job(FB *fb)
{
diff --git a/src/plugins/wp/tests/wp_region/fb_SORT.i b/src/plugins/wp/tests/wp_region/fb_SORT.i
index f5a79d97a696e5ab2ffd3fa2afcb28cd44a2fa1c..72629334e8a760da79b4436a7880cd15e41da5aa 100644
--- a/src/plugins/wp/tests/wp_region/fb_SORT.i
+++ b/src/plugins/wp/tests/wp_region/fb_SORT.i
@@ -16,10 +16,10 @@ typedef struct Block {
} FB ;
/*@
- \wp::region Shared: *(fb->inp1 .. fb->inp3);
- \wp::region IN: (fb->inp1 .. fb->inp3);
- \wp::region OUT: (fb->out1 .. fb->out3);
- \wp::region IDX: (fb->idx1 .. fb->idx3);
+ \wp::wpregion Shared: *(fb->inp1 .. fb->inp3);
+ \wp::wpregion IN: (fb->inp1 .. fb->inp3);
+ \wp::wpregion OUT: (fb->out1 .. fb->out3);
+ \wp::wpregion IDX: (fb->idx1 .. fb->idx3);
*/
void job(FB *fb)
{
diff --git a/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle b/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle
index 07f96795974121ec4b16386336d86296438694fc..11a2a15408554226d844aa54f49e22a8df444ae6 100644
--- a/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle
@@ -24,7 +24,7 @@ struct Block {
SN sum ;
};
typedef struct Block FB;
-/*@ \wp::region *fb; */
+/*@ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -32,9 +32,9 @@ void fb_ADD(FB *fb)
return;
}
-/*@ \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
- \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
- \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+/*@ \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
+ \wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
+ \wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
*/
void fb_SORT(FB *fb)
{
diff --git a/src/plugins/wp/tests/wp_region/structarray1.i b/src/plugins/wp/tests/wp_region/structarray1.i
index 474cab2dd54d19aa8f53bb0618ac98aaec6ec373..e8fb0e753eb65c3fb5fd35c27ba3bd74b16cf5e9 100644
--- a/src/plugins/wp/tests/wp_region/structarray1.i
+++ b/src/plugins/wp/tests/wp_region/structarray1.i
@@ -6,7 +6,7 @@ typedef struct Matrix {
int coef[4][4];
} * matrix ;
-//@ \wp::region *X , *R ;
+//@ \wp::wpregion *X , *R ;
void job( matrix M , vector X , vector R )
{
for (int i = 0; i < 4; i++) {