From 36d9d4279fa52def216b74483dad2be5b6b9c593 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 25 Jul 2024 09:16:02 +0200
Subject: [PATCH] [region] visualize current marker
---
.../src/frama-c/plugins/region/api/index.ts | 26 +++++---------
ivette/src/frama-c/plugins/region/index.tsx | 6 ++--
ivette/src/frama-c/plugins/region/memory.tsx | 35 +++++++++++++------
src/plugins/region/services.ml | 20 +++++------
4 files changed, 48 insertions(+), 39 deletions(-)
diff --git a/ivette/src/frama-c/plugins/region/api/index.ts b/ivette/src/frama-c/plugins/region/api/index.ts
index 5d01bdbe22a..909a2221fa8 100644
--- a/ivette/src/frama-c/plugins/region/api/index.ts
+++ b/ivette/src/frama-c/plugins/region/api/index.ts
@@ -166,34 +166,26 @@ const regions_internal: Server.GetRequest<decl,region[]> = {
/** Returns computed regions for the given declaration */
export const regions: Server.GetRequest<decl,region[]>= regions_internal;
-const regionsAt_internal: Server.GetRequest<[ marker, boolean ],region[]> = {
+const regionsAt_internal: Server.GetRequest<marker,region[]> = {
kind: Server.RqKind.GET,
name: 'plugins.region.regionsAt',
- input: Json.jPair( jMarker, Json.jBoolean,),
+ input: jMarker,
output: Json.jArray(jRegion),
fallback: [],
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Compute regions at the given marker */
-export const regionsAt: Server.GetRequest<[ marker, boolean ],region[]>= regionsAt_internal;
-
-const localize_internal: Server.GetRequest<
- [ marker, boolean ],
- node |
- undefined
- > = {
+/** Compute regions at the given marker program point */
+export const regionsAt: Server.GetRequest<marker,region[]>= regionsAt_internal;
+
+const localize_internal: Server.GetRequest<marker,node | undefined> = {
kind: Server.RqKind.GET,
name: 'plugins.region.localize',
- input: Json.jPair( jMarker, Json.jBoolean,),
+ input: jMarker,
output: Json.jOption(jNode),
fallback: undefined,
signals: [ { name: 'plugins.region.updated' } ],
};
-/** Localize in the local (true) or global map (false) */
-export const localize: Server.GetRequest<
- [ marker, boolean ],
- node |
- undefined
- >= localize_internal;
+/** Localize the marker in its map */
+export const localize: Server.GetRequest<marker,node | undefined>= localize_internal;
/* ------------------------------------- */
diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx
index eed8bea5b81..b5faa2a37f1 100644
--- a/ivette/src/frama-c/plugins/region/index.tsx
+++ b/ivette/src/frama-c/plugins/region/index.tsx
@@ -43,9 +43,11 @@ function RegionAnalys(): JSX.Element {
const [pinned, setPinned] = React.useState(false);
const [running, setRunning] = React.useState(false);
const setComputing = Dome.useProtected(setRunning);
- const scope = States.useCurrentScope();
+ const { scope, marker } = States.useCurrentLocation();
const { kind, name } = States.useDeclaration(scope);
const regions = States.useRequestStable(Region.regions, kf);
+ const node = States.useRequestStable(Region.localize, marker);
+ const { descr: label } = States.useMarker(marker);
React.useEffect(() => {
if (!pinned && kind === 'FUNCTION' && scope !== kf) {
setKf(scope);
@@ -84,7 +86,7 @@ function RegionAnalys(): JSX.Element {
onClick={() => setPinned(!pinned)}
/>
</Tools.ToolBar>
- <MemoryView regions={regions} />
+ <MemoryView regions={regions} node={node} label={label} />
</>
);
}
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index 2b00616c491..055907b7d4a 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -58,8 +58,8 @@ function makeRecord(
}
interface Diagram {
- nodes: Dot.Node[];
- edges: Dot.Edge[];
+ nodes: readonly Dot.Node[];
+ edges: readonly Dot.Edge[];
}
function makeDiagram(regions: readonly Region.region[]): Diagram {
@@ -110,11 +110,23 @@ function makeDiagram(regions: readonly Region.region[]): Diagram {
return { nodes, edges };
}
-function addSelected(d: Diagram, label: string, node: Region.node): void {
- d.nodes.push({
- id: 'Selected', label, title: "Selected Marker", shape: 'note'
- });
- d.edges.push({ source: 'Selected', target: `n${node}` });
+function addSelected(
+ diag: Diagram,
+ node: Region.node | undefined,
+ label: string | undefined
+): Diagram {
+ if (node && label) {
+ const nodes = diag.nodes.concat({
+ id: 'Selected', label, title: "Selected Marker",
+ shape: 'note', color: 'selected'
+ });
+ const edges = diag.edges.concat({
+ source: 'Selected', target: `n${node}`, aligned: true,
+ headAnchor: 's', tailAnchor: 'n',
+ });
+ return { nodes, edges };
+ } else
+ return diag;
}
export interface MemoryViewProps {
@@ -125,9 +137,12 @@ export interface MemoryViewProps {
export function MemoryView(props: MemoryViewProps): JSX.Element {
const { regions = [], label, node } = props;
- const diagram = React.useMemo(() => makeDiagram(regions), [regions]);
- if (label && node) addSelected(diagram, label, node);
- return <Dot.Diagram {...diagram} />;
+ const baseDiagram = React.useMemo(() => makeDiagram(regions), [regions]);
+ const fullDiagram = React.useMemo(
+ () => addSelected(baseDiagram, node, label),
+ [baseDiagram, node, label]
+ );
+ return <Dot.Diagram {...fullDiagram} />;
}
// --------------------------------------------------------------------------
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 0b5ab56eeec..0604d92fb7d 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -181,13 +181,13 @@ module Regions = Data.Jlist(Region)
(* --- Server API --- *)
(* -------------------------------------------------------------------------- *)
-let map_of_localizable ~local (loc : Printer_tag.localizable) =
+let map_of_localizable ?(atStmt=false) (loc : Printer_tag.localizable) =
let open Printer_tag in
match kf_of_localizable loc with
| None -> raise Not_found
| Some kf ->
let domain = Analysis.find kf in
- if local then
+ if atStmt then
match ki_of_localizable loc with
| Kglobal -> domain.map
| Kstmt s -> Stmt.Map.find s domain.body
@@ -236,25 +236,25 @@ let () =
let () =
Request.register
~package ~kind:`GET ~name:"regionsAt"
- ~descr:(Md.plain "Compute regions at the given marker")
- ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~descr:(Md.plain "Compute regions at the given marker program point")
+ ~input:(module Kernel_ast.Marker)
~output:(module Regions)
~signals:[signal]
- begin fun (loc,local) ->
- try Memory.regions @@ map_of_localizable ~local loc
+ begin fun loc ->
+ try Memory.regions @@ map_of_localizable ~atStmt:true loc
with Not_found -> []
end
let () =
Request.register
~package ~kind:`GET ~name:"localize"
- ~descr:(Md.plain "Localize in the local (true) or global map (false)")
- ~input:(module Data.Jpair(Kernel_ast.Marker)(Data.Jbool))
+ ~descr:(Md.plain "Localize the marker in its map")
+ ~input:(module Kernel_ast.Marker)
~output:(module NodeOpt)
~signals:[signal]
- begin fun (loc,local) ->
+ begin fun loc ->
try
- let map = map_of_localizable ~local loc in
+ let map = map_of_localizable loc in
region_of_localizable map loc
with Not_found -> None
end
--
GitLab