From 64f3e438a7cda1be0b481bedda42439c9bd8db84 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lo=C3=AFc=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 7 Jun 2024 15:35:27 +0200
Subject: [PATCH] [region] show "padding" in compounds

---
 ivette/src/frama-c/plugins/region/index.tsx  | 10 +++-
 ivette/src/frama-c/plugins/region/memory.tsx | 55 +++++++++++++++-----
 src/plugins/region/services.ml               |  2 +-
 3 files changed, 52 insertions(+), 15 deletions(-)

diff --git a/ivette/src/frama-c/plugins/region/index.tsx b/ivette/src/frama-c/plugins/region/index.tsx
index 3bf4a449f4d..c733ef9e7d9 100644
--- a/ivette/src/frama-c/plugins/region/index.tsx
+++ b/ivette/src/frama-c/plugins/region/index.tsx
@@ -42,6 +42,7 @@ function RegionAnalys(): JSX.Element {
   const [kfName, setName] = React.useState<string>();
   const [pinned, setPinned] = React.useState(false);
   const [running, setRunning] = React.useState(false);
+  const [padding, setPadding] = React.useState(true);
   const setComputing = Dome.useProtected(setRunning);
   const scope = States.useCurrentScope();
   const { kind, name } = States.useDeclaration(scope);
@@ -83,8 +84,15 @@ function RegionAnalys(): JSX.Element {
           selected={pinned}
           onClick={() => setPinned(!pinned)}
         />
+        <Tools.Filler />
+        <Tools.Button
+          icon='ITEMS.LIST'
+          title='Show non-accessed ranges in compounds'
+          selected={padding}
+          onClick={() => setPadding(!padding)}
+        />
       </Tools.ToolBar>
-      <MemoryView regions={regions} />
+      <MemoryView padding={padding} regions={regions} />
     </>
   );
 }
diff --git a/ivette/src/frama-c/plugins/region/memory.tsx b/ivette/src/frama-c/plugins/region/memory.tsx
index 81c4fd55d9f..67336ef18ae 100644
--- a/ivette/src/frama-c/plugins/region/memory.tsx
+++ b/ivette/src/frama-c/plugins/region/memory.tsx
@@ -28,34 +28,59 @@ import React from 'react';
 import * as Dot from 'dome/graph/diagram';
 import * as Region from './api';
 
-function makeDiagram(regions: readonly Region.region[]): Dot.DiagramProps {
+function makeRecord(
+  edges: Dot.Edge[],
+  source: string,
+  sizeof: number,
+  padding: boolean,
+  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 (padding && 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 (padding && offset !== sizeof)
+    cells.push(`${offset}..${sizeof-1} ##`);
+  return cells;
+}
+
+function makeDiagram(
+  regions: readonly Region.region[],
+  padding: boolean,
+): Dot.DiagramProps {
   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';
-    const cells =
-      r.ranges.map((rg, i): Dot.Cell => {
-        const port = `r${i}`;
-        const target = `n${rg.data}`;
-        edges.push({ source: id, sourcePort: port, target });
-        return ({
-          label: `${rg.offset}..${rg.offset + rg.length - 1} [${rg.cells}]`,
-          port,
-        });
-      });
+    // --- Shape
+    const cells = makeRecord(edges, id, r.sizeof, padding, r.ranges);
     const shape = cells.length > 0 ? cells : undefined;
     nodes.push({ id: id, color, label: r.label, title: r.title, shape });
+    // --- Roots
     r.roots.forEach(x => {
       const xid = `X${x}`;
       nodes.push({ id: xid, label: x, shape: 'folder', color: 'blue' });
       edges.push({ source: xid, target: id });
     });
+    // --- Pointed
     if (r.pointed !== undefined) {
       const pid = `n${r.pointed}`;
       edges.push({ source: id, target: pid, head: 'dot', color: 'orange' });
@@ -66,10 +91,14 @@ function makeDiagram(regions: readonly Region.region[]): Dot.DiagramProps {
 
 export interface MemoryViewProps {
   regions: readonly Region.region[];
+  padding?: boolean;
 }
 
 export function MemoryView(props: MemoryViewProps): JSX.Element {
-  const { regions } = props;
-  const diagram = React.useMemo(() => makeDiagram(regions), [regions]);
+  const { regions, padding=true } = props;
+  const diagram = React.useMemo(
+    () => makeDiagram(regions, padding),
+    [regions, padding]
+  );
   return <Dot.Diagram {...diagram} />;
 }
diff --git a/src/plugins/region/services.ml b/src/plugins/region/services.ml
index 990424bbe4d..c8b31e72d36 100644
--- a/src/plugins/region/services.ml
+++ b/src/plugins/region/services.ml
@@ -126,7 +126,7 @@ struct
     Format.asprintf "%t (%db)"
       begin fun fmt ->
         match m.types with
-        | [] -> Format.pp_print_string fmt "void"
+        | [] -> Format.pp_print_string fmt "Compound"
         | [ty] -> pp_typ_layout m.sizeof fmt ty ;
         | ty::ts ->
           pp_typ_layout 0 fmt ty ;
-- 
GitLab