Skip to content
Snippets Groups Projects
Commit 5ba39bd2 authored by Remi Lazarini's avatar Remi Lazarini
Browse files

Merge branch 'feature/properties/filters' into 'master' 

[Ivette] Properties : add hook for menu filter + change DEFAULTS filters structure

See merge request frama-c/frama-c!4736
parents b3b4062f 9a2c6edf
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
ivette/src/frama-c/kernel/Globals.tsx
+ 2
− 2
View file @ 5ba39bd2
...@@ -82,8 +82,8 @@ function resetMode(enabled: boolean): void { ...@@ -82,8 +82,8 @@ function resetMode(enabled: boolean): void {
// --- Menu item // --- Menu item
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
type setting = [boolean, () => void] export type setting = [boolean, () => void]
function menuItem(label: string, [b, flip]: setting, enabled?: boolean) export function menuItem(label: string, [b, flip]: setting, enabled?: boolean)
: Dome.PopupMenuItem { : Dome.PopupMenuItem {
return { return {
label: label, label: label,
......
ivette/src/frama-c/kernel/Properties.tsx
+ 177
− 121
View file @ 5ba39bd2
...@@ -43,6 +43,7 @@ import { Table, Column, ColumnProps, Renderer } from 'dome/table/views'; ...@@ -43,6 +43,7 @@ import { Table, Column, ColumnProps, Renderer } from 'dome/table/views';
import { RSplit } from 'dome/layout/splitters'; import { RSplit } from 'dome/layout/splitters';
import { TitleBar } from 'ivette'; import { TitleBar } from 'ivette';
import { menuItem, setting } from './Globals';
import * as Ast from 'frama-c/kernel/api/ast'; import * as Ast from 'frama-c/kernel/api/ast';
...@@ -58,54 +59,87 @@ type Property = Properties.statusData | ...@@ -58,54 +59,87 @@ type Property = Properties.statusData |
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
// --- Filters // --- Filters
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
export enum EFilterType {
STATUS = "status",
KIND = "kind",
SOURCE = "source",
ALARMS = "alarms",
EVA = "eva"
}
export type TFilterType = `${EFilterType}`;
interface IFilterContent {
value: boolean;
label: string;
title?: string;
}
function newFilter(
value: boolean,
label: string,
title?: string,
): IFilterContent {
return { value, label, title };
}
const DEFAULTS: { [key: string]: boolean } = { const DEFAULTS: { [key: string]: IFilterContent } = {
'currentScope': false, 'currentScope': newFilter(false, "Current scope"),
'status.valid': true, /** status */
'status.valid_hyp': true, 'status.valid': newFilter(true, "Valid"),
'status.unknown': true, 'status.valid_hyp': newFilter(true, "Valid under hyp."),
'status.invalid': true, 'status.unknown': newFilter(true, "Unknown"),
'status.invalid_hyp': true, 'status.invalid': newFilter(true, "Invalid"),
'status.considered_valid': false, 'status.invalid_hyp': newFilter(true, "Invalid under hyp."),
'status.untried': false, 'status.considered_valid': newFilter(false, "Considered valid"),
'status.dead': false, 'status.untried': newFilter(false, "Untried"),
'status.inconsistent': true, 'status.dead': newFilter(false, "Dead"),
'kind.assert': true, 'status.inconsistent': newFilter(true, "Inconsistent"),
'kind.invariant': true, /** kind */
'kind.variant': true, 'kind.assert': newFilter(true, "Assertions"),
'kind.requires': true, 'kind.invariant': newFilter(true, "Invariants"),
'kind.ensures': true, 'kind.variant': newFilter(true, "Variants"),
'kind.instance': true, 'kind.requires': newFilter(true, "Preconditions"),
'kind.assumes': true, 'kind.ensures': newFilter(true, "Postconditions"),
'kind.assigns': true, 'kind.instance': newFilter(true, "Instance"),
'kind.froms': true, 'kind.assigns': newFilter(true, "Assigns clauses"),
'kind.allocates': true, 'kind.froms': newFilter(true, "From clauses"),
'kind.behavior': false, 'kind.allocates': newFilter(true, "Allocates"),
'kind.reachable': false, 'kind.behavior': newFilter(false, "Behaviors"),
'kind.axiomatic': true, 'kind.reachable': newFilter(false, "Reachables"),
'kind.pragma': true, 'kind.axiomatic': newFilter(true, "Axiomatics"),
'kind.others': true, 'kind.pragma': newFilter(true, "Pragma"),
'source.alarms': true, // show properties that are alarms 'kind.assumes': newFilter(true, "Assumes"),
'source.others': true, // show properties that are not alarms 'kind.others': newFilter(true, "Others"),
'alarms.overflow': true, /** source */
'alarms.division_by_zero': true, 'source.alarms': newFilter(true, "Alarms"),
'alarms.mem_access': true, 'source.others': newFilter(true, "Others"),
'alarms.index_bound': true, /** alarms */
'alarms.pointer_value': true, 'alarms.overflow': newFilter(true, "Overflows"),
'alarms.shift': true, 'alarms.division_by_zero': newFilter(true, "Divisions by zero"),
'alarms.ptr_comparison': true, 'alarms.shift': newFilter(true, "Shifts"),
'alarms.differing_blocks': true, 'alarms.special_float': newFilter(true, "Special floats"),
'alarms.separation': true, 'alarms.float_to_int': newFilter(true, "Float to int"),
'alarms.overlap': true, 'alarms.bool_value': newFilter(true, "_Bool values"),
'alarms.initialization': true, 'alarms.mem_access': newFilter(true, "Memory accesses"),
'alarms.dangling_pointer': true, 'alarms.index_bound': newFilter(true, "Index bounds"),
'alarms.special_float': true, 'alarms.initialization': newFilter(true, "Initializations"),
'alarms.float_to_int': true, 'alarms.dangling_pointer': newFilter(true, "Dangling pointers"),
'alarms.function_pointer': true, 'alarms.pointer_value': newFilter(true, "Pointer values"),
'alarms.bool_value': true, 'alarms.function_pointer': newFilter(true, "Function pointers"),
'eva.priority_only': false, 'alarms.ptr_comparison': newFilter(true, "Pointer comparisons"),
'eva.data_tainted_only': false, 'alarms.differing_blocks': newFilter(true, "Differing blocks"),
'eva.ctrl_tainted_only': false, 'alarms.separation': newFilter(true, "Separations"),
'alarms.overlap': newFilter(true, "Overlaps"),
/** eva */
'eva.priority_only': newFilter(false, "High-priority only",
"Show only high-priority properties for the Eva analysis"
),
'eva.data_tainted_only': newFilter(false, "Data-tainted only",
"Show only data-tainted properties according to the Eva taint domain"
),
'eva.ctrl_tainted_only': newFilter(false, "Control-tainted only",
"Show only control-tainted properties according to the Eva taint domain"
),
}; };
function filter(path: string): boolean { function filter(path: string): boolean {
...@@ -113,15 +147,15 @@ function filter(path: string): boolean { ...@@ -113,15 +147,15 @@ function filter(path: string): boolean {
return Settings.getWindowSettings( return Settings.getWindowSettings(
`ivette.properties.filter.${path}`, `ivette.properties.filter.${path}`,
Json.jBoolean, Json.jBoolean,
defaultValue, defaultValue.value,
); );
} }
function useFilter(path: string): [boolean, () => void] { export function useFilter(path: string): [boolean, () => void] {
const defaultValue = DEFAULTS[path] ?? true; const defaultValue = DEFAULTS[path] ?? true;
return Dome.useFlipSettings( return Dome.useFlipSettings(
`ivette.properties.filter.${path}`, `ivette.properties.filter.${path}`,
defaultValue, defaultValue.value,
); );
} }
...@@ -143,7 +177,7 @@ function useFilterStr(path: string): Form.FieldState<string> { ...@@ -143,7 +177,7 @@ function useFilterStr(path: string): Form.FieldState<string> {
function resetFilters(prefix: string, b?: boolean) : void { function resetFilters(prefix: string, b?: boolean) : void {
for (const key in DEFAULTS) { for (const key in DEFAULTS) {
if (key.startsWith(prefix)) { if (key.startsWith(prefix)) {
const target = b ?? DEFAULTS[key]; const target = b ?? DEFAULTS[key].value;
const path = `ivette.properties.filter.${key}`; const path = `ivette.properties.filter.${key}`;
Settings.setWindowSettings(path, target); Settings.setWindowSettings(path, target);
} }
...@@ -280,6 +314,79 @@ function filterProperty(p: Property): boolean { ...@@ -280,6 +314,79 @@ function filterProperty(p: Property): boolean {
&& filterNames(p.names); && filterNames(p.names);
} }
export interface IFilterState {
contextMenu: Dome.PopupMenuItem[],
show: (status: Properties.statusData) => boolean
}
function getContextMenu(
type: TFilterType,
filters: {[key: string]: setting}
):Dome.PopupMenuItem[] {
const typeStr = type+".";
return Object.entries(DEFAULTS)
.filter(([k, ]) => k.startsWith(typeStr))
.map(([k, elt]) => menuItem(elt.label, filters[k.replace(typeStr, "")]));
}
export function useStatusFilter(): IFilterState {
const filters: {[key: string]: setting} = {};
filters.valid = useFilter('status.valid');
filters.validHyp = useFilter('status.valid_hyp');
filters.unknown = useFilter('status.unknown');
filters.invalid = useFilter('status.invalid');
filters.invalidHyp = useFilter('status.invalid_hyp');
filters.consideredValid = useFilter('status.considered_valid');
filters.untried = useFilter('status.untried');
filters.dead = useFilter('status.dead');
filters.inconsistent = useFilter('status.inconsistent');
return {
contextMenu: getContextMenu(EFilterType.STATUS, filters),
show: (statusData: Property) =>
filterStatus(statusData.status),
};
}
export function useKindPropertiesFilter(): IFilterState {
const filters: {[key: string]: setting} = {};
filters.assert = useFilter('kind.assert');
filters.invariant = useFilter('kind.invariant');
filters.variant = useFilter('kind.variant');
filters.requires = useFilter('kind.requires');
filters.ensures = useFilter('kind.ensures');
filters.instance = useFilter('kind.instance');
filters.assigns = useFilter('kind.assigns');
filters.froms = useFilter('kind.froms');
filters.allocates = useFilter('kind.allocates');
filters.behavior = useFilter('kind.behavior',);
filters.reachable = useFilter('kind.reachable',);
filters.axiomatic = useFilter('kind.axiomatic');
filters.pragma = useFilter('kind.pragma');
filters.assumes = useFilter('kind.assumes');
filters.others = useFilter('kind.others');
return {
contextMenu: getContextMenu(EFilterType.KIND, filters),
show: (statusData: Property) => filterKind(statusData.kind),
};
}
export function useEvaPropertiesFilter(): IFilterState {
const filters: {[key: string]: setting} = {};
filters.priorityOnly = useFilter('eva.priority_only');
filters.dataTaintedOnly = useFilter('eva.data_tainted_only');
filters.ctrlTaintedOnly = useFilter('eva.ctrl_tainted_only');
return {
contextMenu: getContextMenu(EFilterType.EVA, filters),
show: (statusData: Property) => filterEva(statusData),
};
}
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
// --- Property Columns // --- Property Columns
// -------------------------------------------------------------------------- // --------------------------------------------------------------------------
...@@ -422,12 +529,12 @@ const Reload = new Dome.Event('ivette.properties.reload'); ...@@ -422,12 +529,12 @@ const Reload = new Dome.Event('ivette.properties.reload');
interface SectionProps { interface SectionProps {
label: string; label: string;
prefix?: string; prefix?: TFilterType;
unfold?: boolean; unfold?: boolean;
children: React.ReactNode; children: React.ReactNode;
} }
function onContextMenu(prefix: string): void { export function onContextMenu(prefix: string): void {
const items: Dome.PopupMenuItem[] = [ const items: Dome.PopupMenuItem[] = [
{ {
label: 'Reset to default', label: 'Reset to default',
...@@ -503,9 +610,19 @@ function PropertyFilter(): JSX.Element { ...@@ -503,9 +610,19 @@ function PropertyFilter(): JSX.Element {
return "At least 2 characters"; return "At least 2 characters";
}; };
const getCheckBox = (type: TFilterType): JSX.Element => {
return <> {
Object.entries(DEFAULTS)
.filter(([key, ]) => key.startsWith(type+"."))
.map(([key, elt]) =>
<CheckField key={key} label={elt.label} path={key} title={elt.title}/>
)
}</>;
};
return ( return (
<Scroll> <Scroll>
<CheckField label="Current scope" path="currentScope" /> <CheckField label={DEFAULTS.currentScope.label} path="currentScope" />
<Section <Section
label="Search" label="Search"
defaultUnfold={true} defaultUnfold={true}
...@@ -524,73 +641,12 @@ function PropertyFilter(): JSX.Element { ...@@ -524,73 +641,12 @@ function PropertyFilter(): JSX.Element {
checker={checkerNames} checker={checkerNames}
/> />
</Section> </Section>
<FilterSection label="Status" prefix="status" unfold>
<CheckField label="Valid" path="status.valid" /> <FilterSection label="Status" prefix="status" unfold> { getCheckBox("status") } </FilterSection>
<CheckField label="Valid under hyp." path="status.valid_hyp" /> <FilterSection label="Property kind" prefix="kind"> { getCheckBox("kind") } </FilterSection>
<CheckField label="Unknown" path="status.unknown" /> <FilterSection label="Source" prefix="source"> { getCheckBox("source") } </FilterSection>
<CheckField label="Invalid" path="status.invalid" /> <FilterSection label="Alarms kind" prefix="alarms"> { getCheckBox("alarms") } </FilterSection>
<CheckField label="Invalid under hyp." path="status.invalid_hyp" /> <FilterSection label="Eva"> { getCheckBox("eva") } </FilterSection>
<CheckField label="Considered valid" path="status.considered_valid" />
<CheckField label="Untried" path="status.untried" />
<CheckField label="Dead" path="status.dead" />
<CheckField label="Inconsistent" path="status.inconsistent" />
</FilterSection>
<FilterSection label="Property kind" prefix="kind">
<CheckField label="Assertions" path="kind.assert" />
<CheckField label="Invariants" path="kind.invariant" />
<CheckField label="Variants" path="kind.variant" />
<CheckField label="Preconditions" path="kind.requires" />
<CheckField label="Postconditions" path="kind.ensures" />
<CheckField label="Instance" path="kind.instance" />
<CheckField label="Assigns clauses" path="kind.assigns" />
<CheckField label="From clauses" path="kind.froms" />
<CheckField label="Allocates" path="kind.allocates" />
<CheckField label="Behaviors" path="kind.behavior" />
<CheckField label="Reachables" path="kind.reachable" />
<CheckField label="Axiomatics" path="kind.axiomatic" />
<CheckField label="Pragma" path="kind.pragma" />
<CheckField label="Assumes" path="kind.assumes" />
<CheckField label="Others" path="kind.others" />
</FilterSection>
<FilterSection label="Source" prefix="source">
<CheckField label="Alarms" path="source.alarms" />
<CheckField label="Others" path="source.others" />
</FilterSection>
<FilterSection label="Alarms kind" prefix="alarms">
<CheckField label="Overflows" path="alarms.overflow" />
<CheckField label="Divisions by zero" path="alarms.division_by_zero" />
<CheckField label="Shifts" path="alarms.shift" />
<CheckField label="Special floats" path="alarms.special_float" />
<CheckField label="Float to int" path="alarms.float_to_int" />
<CheckField label="_Bool values" path="alarms.bool_value" />
<CheckField label="Memory accesses" path="alarms.mem_access" />
<CheckField label="Index bounds" path="alarms.index_bound" />
<CheckField label="Initializations" path="alarms.initialization" />
<CheckField label="Dangling pointers" path="alarms.dangling_pointer" />
<CheckField label="Pointer values" path="alarms.pointer_value" />
<CheckField label="Function pointers" path="alarms.function_pointer" />
<CheckField label="Pointer comparisons" path="alarms.ptr_comparison" />
<CheckField label="Differing blocks" path="alarms.differing_blocks" />
<CheckField label="Separations" path="alarms.separation" />
<CheckField label="Overlaps" path="alarms.overlap" />
</FilterSection>
<FilterSection label="Eva">
<CheckField
label="High-priority only"
path="eva.priority_only"
title="Show only high-priority properties for the Eva analysis"
/>
<CheckField
label="Data-tainted only"
path="eva.data_tainted_only"
title="Show only data-tainted properties according to the Eva taint domain"
/>
<CheckField
label="Control-tainted only"
path="eva.ctrl_tainted_only"
title="Show only control-tainted properties according to the Eva taint domain"
/>
</FilterSection>
</Scroll> </Scroll>
); );
} }
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment