From f7e1335980fbd03fb7bf7262a3293014be26af90 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 8 Jun 2020 10:35:15 +0200
Subject: [PATCH] [ivette] Adds filters to the property table.
---
ivette/src/renderer/Properties.tsx | 293 +++++++++++++++++++++++++----
1 file changed, 260 insertions(+), 33 deletions(-)
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 80d42e5d81d..9a06620a0d1 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -10,6 +10,146 @@ import { Label, Code } from 'dome/controls/labels';
import { ArrayModel } from 'dome/table/arrays';
import { Table, Column, ColumnProps, Renderer } from 'dome/table/views';
import { Component } from 'frama-c/LabViews';
+import { Vfill } from 'dome/layout/boxes';
+import { Splitter } from 'dome/layout/splitters';
+import { Form, Section, FieldCheckbox } from 'dome/layout/forms';
+
+// --------------------------------------------------------------------------
+// --- Filters
+// --------------------------------------------------------------------------
+
+const defaultStatusFilter =
+{
+ valid: true,
+ valid_hyp: true,
+ unknown: true,
+ invalid: true,
+ invalid_hyp: true,
+ considered_valid: false,
+ untried: false,
+ dead: false,
+ inconsistent: true,
+};
+
+const defaultKindFilter =
+{
+ assert: true,
+ invariant: true,
+ variant: true,
+ requires: true,
+ ensures: true,
+ instance: true,
+ assumes: true,
+ assigns: true,
+ from: true,
+ allocates: true,
+ behavior: false,
+ reachable: false,
+ axiomatic: true,
+ pragma: true,
+ others: true,
+};
+
+const defaultAlarmsFilter =
+{
+ alarms: true, // show properties that are alarms
+ others: true, // show properties that are not alarms
+ overflow: true,
+ division_by_zero: true,
+ mem_access: true,
+ index_bound: true,
+ pointer_value: true,
+ shift: true,
+ ptr_comparison: true,
+ differing_blocks: true,
+ separation: true,
+ overlap: true,
+ initialization: true,
+ dangling_pointer: true,
+ special_float: true,
+ float_to_int: true,
+ function_pointer: true,
+ union_initialization: true,
+ bool_value: true,
+};
+
+const defaultFilter =
+{
+ currentFunction: false,
+ status: defaultStatusFilter,
+ kind: defaultKindFilter,
+ alarms: defaultAlarmsFilter,
+};
+
+
+function filterStatus(f: typeof defaultStatusFilter, status: string) {
+ switch (status) {
+ case 'valid':
+ case 'valid_but_dead': return f.valid;
+ case 'valid_under_hyp': return f.valid_hyp;
+ case 'invalid':
+ case 'invalid_but_dead': return f.invalid;
+ case 'invalid_under_hyp': return f.invalid_hyp;
+ case 'unknown':
+ case 'unknown_but_dead': return f.unknown;
+ case 'considered_valid': return f.considered_valid;
+ case 'never_tried': return f.untried;
+ case 'dead': return f.dead;
+ case 'inconsistent': return f.inconsistent;
+ default: return true;
+ }
+}
+
+function filterKind(f: typeof defaultKindFilter, kind: string) {
+ switch (kind) {
+ case 'assert': return f.assert;
+ case 'invariant': return f.invariant;
+ case 'variant': return f.variant;
+ case 'requires': return f.requires;
+ case 'ensures': return f.ensures;
+ case 'instance': return f.instance;
+ case 'assigns': return f.assigns;
+ case 'from': return f.from;
+ case 'allocates': return f.allocates;
+ case 'behavior': return f.behavior;
+ case 'reachable': return f.reachable;
+ case 'axiomatic': return f.axiomatic;
+ case 'pragma': return f.pragma;
+ default: return f.others;
+ }
+}
+
+function filterAlarm(f: typeof defaultAlarmsFilter, alarm: string) {
+ switch (alarm) {
+ case 'overflow': return f.overflow;
+ case 'division_by_zero': return f.division_by_zero;
+ case 'mem_access': return f.mem_access;
+ case 'index_bound': return f.index_bound;
+ case 'pointer_value': return f.pointer_value;
+ case 'shift': return f.shift;
+ case 'ptr_comparison': return f.ptr_comparison;
+ case 'differing_blocks': return f.differing_blocks;
+ case 'separation': return f.separation;
+ case 'overlap': return f.overlap;
+ case 'initialization': return f.initialization;
+ case 'dangling_pointer': return f.dangling_pointer;
+ case 'is_nan_or_infinite':
+ case 'is_nan': return f.special_float;
+ case 'float_to_int': return f.float_to_int;
+ case 'function_pointer': return f.function_pointer;
+ case 'initialization_of_union': return f.union_initialization;
+ case 'bool_value': return f.bool_value;
+ default: return true;
+ }
+}
+
+function filterProperty(f: typeof defaultFilter, item: Property) {
+ return filterStatus(f.status, item.status)
+ && filterKind(f.kind, item.kind)
+ && ((item.alarm && f.alarms.alarms)
+ || (!item.alarm && f.alarms.others))
+ && (!item.alarm || filterAlarm(f.alarms, item.alarm));
+}
// --------------------------------------------------------------------------
// --- Property Columns
@@ -35,11 +175,12 @@ const renderNames: Renderer<string[]> =
(names?: string[]) => {
const label = names?.join(': ');
return (label ? <Label label={label} /> : null);
- }
+ };
const renderFile: Renderer<SourceLoc> =
- (loc?: SourceLoc) =>
- (loc ? <Label label={loc.base} title={loc.file} /> : null);
+ (loc?: SourceLoc) => (
+ loc ? <Label label={loc.base} title={loc.file} /> : null
+ );
// --------------------------------------------------------------------------
// --- Properties Table
@@ -112,6 +253,8 @@ const RenderTable = () => {
States.useDictionary('kernel.dictionary.propstatus');
const [select, setSelect] =
States.useSelection();
+ const selectedFunction = select?.function;
+ const filter = React.useRef(defaultFilter);
React.useEffect(() => {
const data = _.toArray(items);
@@ -132,38 +275,122 @@ const RenderTable = () => {
const selection = select?.marker;
+ /* --- Filters selection -------------------------------------------------- */
+
+ React.useEffect(() => {
+
+ function filtering(item: Property) {
+ const current =
+ !filter.current.currentFunction
+ || (selectedFunction === item?.function);
+ return current && filterProperty(filter.current, item);
+ }
+
+ model.setFilter(filtering);
+ }, [model, filter, selectedFunction]);
+
+ const filtersList = (
+ <Form
+ value={filter.current}
+ onChange={() => model.reload()}
+ >
+ <FieldCheckbox label="Current function" path="currentFunction" />
+ <Section label="Status" unfold path="status">
+ <FieldCheckbox label="Valid" path="valid" />
+ <FieldCheckbox label="Valid under hyp." path="valid_hyp" />
+ <FieldCheckbox label="Unknown" path="unknown" />
+ <FieldCheckbox label="Invalid" path="invalid" />
+ <FieldCheckbox label="Invalid under hyp." path="invalid_hyp" />
+ <FieldCheckbox label="Considered valid" path="considered_valid" />
+ <FieldCheckbox label="Untried" path="untried" />
+ <FieldCheckbox label="Dead" path="dead" />
+ <FieldCheckbox label="Inconsistent" path="inconsistent" />
+ </Section>
+ <Section label="Property kind" path="kind">
+ <FieldCheckbox label="Assertions" path="assert" />
+ <FieldCheckbox label="Invariants" path="invariant" />
+ <FieldCheckbox label="Variants" path="variant" />
+ <FieldCheckbox label="Preconditions" path="requires" />
+ <FieldCheckbox label="Postconditions" path="ensures" />
+ <FieldCheckbox label="Instance" path="instance" />
+ <FieldCheckbox label="Assigns clauses" path="assigns" />
+ <FieldCheckbox label="From clauses" path="from" />
+ <FieldCheckbox label="Allocates" path="allocates" />
+ <FieldCheckbox label="Behaviors" path="behavior" />
+ <FieldCheckbox label="Reachables" path="reachable" />
+ <FieldCheckbox label="Axiomatics" path="axiomatic" />
+ <FieldCheckbox label="Pragma" path="pragma" />
+ <FieldCheckbox label="Others" path="others" />
+ </Section>
+ <Section label="Alarms" path="alarms">
+ <FieldCheckbox label="Alarms" path="alarms" />
+ <FieldCheckbox label="Others" path="others" />
+ </Section>
+ <Section label="Alarms kind" path="alarms">
+ <FieldCheckbox label="Overflows" path="overflow" />
+ <FieldCheckbox label="Divisions by zero" path="division_by_zero" />
+ <FieldCheckbox label="Shifts" path="shift" />
+ <FieldCheckbox label="Special floats" path="special_float" />
+ <FieldCheckbox label="Float to int" path="float_to_int" />
+ <FieldCheckbox label="_Bool values" path="bool_value" />
+ <FieldCheckbox label="Memory accesses" path="mem_access" />
+ <FieldCheckbox label="Index bounds" path="index_bound" />
+ <FieldCheckbox label="Initializations" path="initialization" />
+ <FieldCheckbox label="Dangling pointers" path="dangling_pointer" />
+ <FieldCheckbox label="Pointer values" path="pointer_value" />
+ <FieldCheckbox label="Function pointers" path="function_pointer" />
+ <FieldCheckbox label="Pointer comparisons" path="ptr_comparison" />
+ <FieldCheckbox label="Differing blocks" path="differing_blocks" />
+ <FieldCheckbox label="Separations" path="separation" />
+ <FieldCheckbox label="Overlaps" path="overlap" />
+ <FieldCheckbox
+ label="Initialization of unions"
+ path="union_initialization"
+ />
+ </Section>
+ </Form>
+ );
+
// Rendering
return (
- <Table<string, Property>
- model={model}
- sorting={model}
- selection={selection}
- onSelection={onSelection}
- settings="ivette.properties.table"
- >
- <Column
- id="path"
- label="Directory"
- width={240}
- visible={false}
- getter={(prop: Property) => prop.source.dir}
- />
- <Column id="source" label="File" width={120} render={renderFile} />
- <ColumnCode id="function" label="Function" width={120} />
- <ColumnCode id="kind" label="Property kind" width={120} />
- <ColumnCode id="alarm" label="Alarms" width={160} />
- <Column id="names" label="Names" width={240} visible={false}
- render={renderNames} />
- <ColumnCode id="predicate" label="Predicate" fill />
- <ColumnCode id="descr" label="Property" fill visible={false} />
- <ColumnTag
- id="status"
- label="Status"
- width={100}
- align="center"
- getter={getStatus}
- />
- </Table>
+ <Splitter dir="LEFT">
+ <Vfill> {filtersList} </Vfill>
+ <Table<string, Property>
+ model={model}
+ sorting={model}
+ selection={selection}
+ onSelection={onSelection}
+ settings="ivette.properties.table"
+ >
+ <Column
+ id="path"
+ label="Directory"
+ width={240}
+ visible={false}
+ getter={(prop: Property) => prop.source.dir}
+ />
+ <Column id="source" label="File" width={120} render={renderFile} />
+ <ColumnCode id="function" label="Function" width={120} />
+ <ColumnCode id="kind" label="Property kind" width={120} />
+ <ColumnCode id="alarm" label="Alarms" width={160} />
+ <Column
+ id="names"
+ label="Names"
+ width={240}
+ visible={false}
+ render={renderNames}
+ />
+ <ColumnCode id="predicate" label="Predicate" fill />
+ <ColumnCode id="descr" label="Property" fill visible={false} />
+ <ColumnTag
+ id="status"
+ label="Status"
+ width={100}
+ align="center"
+ getter={getStatus}
+ />
+ </Table>
+ </Splitter>
);
};
--
GitLab