Commit 55392f04 authored by Michele Alberti's avatar Michele Alberti
Browse files

Merge branch 'feature/ivette/values' into 'master'

[Ivette] New component for the values inferred by an Eva analysis

Closes #864

See merge request frama-c/frama-c!2679
parents 65e801a6 773d21ee
......@@ -829,7 +829,7 @@ PLUGIN_NAME:=Eva
PLUGIN_DIR:=src/plugins/value
PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
domains/gauges domains/equality legacy partitioning utils gui_files \
values/numerors domains/numerors
api values/numerors domains/numerors
PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
......@@ -912,6 +912,7 @@ PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
engine/compute_functions engine/analysis register \
api/general_requests \
utils/unit_tests \
api/values_request \
$(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
......
......@@ -1210,6 +1210,8 @@ src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/general_requests.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/api/values_request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/abstract_domain.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/printer_domain.mli: CEA_LGPL_OR_PROPRIETARY
......
......@@ -43,10 +43,6 @@ export const compute: Server.ExecRequest<null,null>= compute_internal;
/** Marker kind */
export enum markerKind {
/** Variable */
variable = 'variable',
/** Function */
function = 'function',
/** Expression */
expression = 'expression',
/** Lvalue */
......@@ -83,12 +79,44 @@ const markerKindTags_internal: Server.GetRequest<null,tag[]> = {
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]>= markerKindTags_internal;
/** Marker variable */
export enum markerVar {
/** None */
none = 'none',
/** Variable */
variable = 'variable',
/** Function */
function = 'function',
}
/** Loose decoder for `markerVar` */
export const jMarkerVar: Json.Loose<markerVar> = Json.jEnum(markerVar);
/** Safe decoder for `markerVar` */
export const jMarkerVarSafe: Json.Safe<markerVar> =
Json.jFail(Json.jEnum(markerVar),'kernel.ast.markerVar expected');
/** Natural order for `markerVar` */
export const byMarkerVar: Compare.Order<markerVar> =
Compare.byEnum(markerVar);
const markerVarTags_internal: Server.GetRequest<null,tag[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.markerVarTags',
input: Json.jNull,
output: Json.jList(jTag),
};
/** Registered tags for the above type. */
export const markerVarTags: Server.GetRequest<null,tag[]>= markerVarTags_internal;
/** Data for array rows [`markerInfo`](#markerinfo) */
export interface markerInfoData {
/** Entry identifier. */
key: Json.key<'#markerInfo'>;
/** Marker kind */
kind: markerKind;
/** Marker variable */
var: markerVar;
/** Marker short name */
name: string;
/** Marker declaration or description */
......@@ -101,6 +129,7 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> =
key: Json.jFail(Json.jKey<'#markerInfo'>('#markerInfo'),
'#markerInfo expected'),
kind: jMarkerKindSafe,
var: jMarkerVarSafe,
name: Json.jFail(Json.jString,'String expected'),
descr: Json.jFail(Json.jString,'String expected'),
});
......@@ -112,10 +141,11 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
/** Natural order for `markerInfoData` */
export const byMarkerInfoData: Compare.Order<markerInfoData> =
Compare.byFields
<{ key: Json.key<'#markerInfo'>, kind: markerKind, name: string,
descr: string }>({
<{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar,
name: string, descr: string }>({
key: Compare.string,
kind: byMarkerKind,
var: byMarkerVar,
name: Compare.alpha,
descr: Compare.string,
});
......
......@@ -3,7 +3,7 @@
/**
Eva General Services
@packageDocumentation
@module api/plugins/eva
@module api/plugins/eva/general
*/
//@ts-ignore
......@@ -21,7 +21,7 @@ const getCallers_internal: Server.GetRequest<
[ Json.key<'#fct'>, Json.key<'#stmt'> ][]
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.getCallers',
name: 'plugins.eva.general.getCallers',
input: Json.jKey<'#fct'>('#fct'),
output: Json.jList(Json.jTry(
Json.jPair(
......
/* --- Generated Frama-C Server API --- */
/**
Eva Values
@packageDocumentation
@module api/plugins/eva/values
*/
//@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 { byMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarkerSafe } from 'api/kernel/ast';
//@ts-ignore
import { marker } from 'api/kernel/ast';
/** CallStack */
export interface callstack {
/** Callstack id */
id: number;
/** Short name for the callstack */
short: string;
/** Full name for the callstack */
full: string;
}
/** Loose decoder for `callstack` */
export const jCallstack: Json.Loose<callstack> =
Json.jObject({
id: Json.jFail(Json.jNumber,'Number expected'),
short: Json.jFail(Json.jString,'String expected'),
full: Json.jFail(Json.jString,'String expected'),
});
/** Safe decoder for `callstack` */
export const jCallstackSafe: Json.Safe<callstack> =
Json.jFail(jCallstack,'Callstack expected');
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> =
Compare.byFields
<{ id: number, short: string, full: string }>({
id: Compare.number,
short: Compare.string,
full: Compare.string,
});
/** Data for array rows [`values`](#values) */
export interface valuesData {
/** Entry identifier. */
key: Json.key<'#values'>;
/** CallStack */
callstack: callstack;
/** Value inferred just before the selected point */
value_before: string;
/** Did the evaluation led to an alarm? */
alarm: boolean;
/** Value inferred just after the selected point */
value_after?: string;
}
/** Loose decoder for `valuesData` */
export const jValuesData: Json.Loose<valuesData> =
Json.jObject({
key: Json.jFail(Json.jKey<'#values'>('#values'),'#values expected'),
callstack: jCallstackSafe,
value_before: Json.jFail(Json.jString,'String expected'),
alarm: Json.jFail(Json.jBoolean,'Boolean expected'),
value_after: Json.jString,
});
/** Safe decoder for `valuesData` */
export const jValuesDataSafe: Json.Safe<valuesData> =
Json.jFail(jValuesData,'ValuesData expected');
/** Natural order for `valuesData` */
export const byValuesData: Compare.Order<valuesData> =
Compare.byFields
<{ key: Json.key<'#values'>, callstack: callstack, value_before: string,
alarm: boolean, value_after?: string }>({
key: Compare.string,
callstack: byCallstack,
value_before: Compare.string,
alarm: Compare.boolean,
value_after: Compare.defined(Compare.string),
});
/** Signal for array [`values`](#values) */
export const signalValues: Server.Signal = {
name: 'plugins.eva.values.signalValues',
};
const reloadValues_internal: Server.GetRequest<null,null> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.reloadValues',
input: Json.jNull,
output: Json.jNull,
};
/** Force full reload for array [`values`](#values) */
export const reloadValues: Server.GetRequest<null,null>= reloadValues_internal;
const fetchValues_internal: Server.GetRequest<
number,
{ pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
reload: boolean }
> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.fetchValues',
input: Json.jNumber,
output: Json.jObject({
pending: Json.jFail(Json.jNumber,'Number expected'),
updated: Json.jList(jValuesData),
removed: Json.jList(Json.jKey<'#values'>('#values')),
reload: Json.jFail(Json.jBoolean,'Boolean expected'),
}),
};
/** Data fetcher for array [`values`](#values) */
export const fetchValues: Server.GetRequest<
number,
{ pending: number, updated: valuesData[], removed: Json.key<'#values'>[],
reload: boolean }
>= fetchValues_internal;
const values_internal: State.Array<Json.key<'#values'>,valuesData> = {
name: 'plugins.eva.values.values',
getkey: ((d:valuesData) => d.key),
signal: signalValues,
fetch: fetchValues,
reload: reloadValues,
order: byValuesData,
};
/** Abstract values inferred by the Eva analysis */
export const values: State.Array<Json.key<'#values'>,valuesData> = values_internal;
const getValues_internal: Server.GetRequest<marker,null> = {
kind: Server.RqKind.GET,
name: 'plugins.eva.values.getValues',
input: jMarker,
output: Json.jNull,
};
/** Get the abstract values computed for an expression or lvalue */
export const getValues: Server.GetRequest<marker,null>= getValues_internal;
/* ------------------------------------- */
......@@ -33,7 +33,7 @@
"css-loader": "^3.4.0",
"electron": "^7",
"electron-builder": "^22.4.1",
"electron-devtools-installer": "^2.2.4",
"electron-devtools-installer": "^3.0.0",
"electron-webpack": "^2.8.2",
"eslint": "^6.8.0",
"eslint-config-airbnb": "^18.1.0",
......
......@@ -392,7 +392,10 @@ function createPrimaryWindow()
// React Developper Tools
if (DEVEL)
installExtension(REACT_DEVELOPER_TOOLS,true);
installExtension(REACT_DEVELOPER_TOOLS,true)
.catch((err) => {
console.error('[Dome] Enable to install React dev-tools',err);
});
const cwd = process.cwd();
const wdir = cwd === '/' ? app.getPath('home') : cwd ;
const argv = stripElectronArgv(process.argv);
......
......@@ -8,5 +8,5 @@ export const REACT_DEVELOPER_TOOLS = undefined ;
// Shall not be used in non-development mode
export default function installExtension(_id) {
return Promise.reject();
return Promise.resolve();
}
......@@ -429,7 +429,7 @@ export class ArrayModel<Key, Row>
// --------------------------------------------------------------------------
/**
@template Row - object data that also contains their « key »
@template Row - object data that also contains their « key ».
*/
export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
......@@ -460,7 +460,6 @@ export class CompactModel<Key, Row> extends ArrayModel<Key, Row> {
this.reload();
}
}
// --------------------------------------------------------------------------
......@@ -59,6 +59,14 @@ export type RenderByFields<Row> = {
export type index = number | number[]
/**
Column Properties.
__Warning:__ callback properties, namely `getter`, `render`
and `onContextMenu`, shall be as stable as possible to prevent
the table from constantly re-rendering.
Use constant callbacks whenever possible, or memoize them with
`React.useCallback()` hook.
@template Row - table row data of some table entries
@template Cell - type of cell data to render in this column
*/
......@@ -104,14 +112,17 @@ export interface ColumnProps<Row, Cell> {
visible?: boolean | 'never' | 'always';
/**
Data getter for this column.
Shall be constant or protected by `React.useCallback`.
*/
getter?: (row: Row, dataKey: string) => Cell | undefined;
/**
Override table by-fields cell renderers.
Shall be constant or protected by `React.useCallback`.
*/
render?: Renderer<Cell>;
/**
Override table right-click callback.
Shall be constant or protected by `React.useCallback`.
*/
onContextMenu?: (row: Row, index: number, dataKey: string) => void;
}
......
......@@ -15,7 +15,7 @@ import { IconButton } from 'dome/controls/buttons';
import { Component, TitleBar } from 'frama-c/LabViews';
import { printFunction, markerInfo } from 'api/kernel/ast';
import { getCallers } from 'api/plugins/eva';
import { getCallers } from 'api/plugins/eva/general';
import 'codemirror/mode/clike/clike';
import 'codemirror/theme/ambiance.css';
......@@ -123,7 +123,7 @@ const ASTview = () => {
const zoomIn = () => fontSize < 48 && setFontSize(fontSize + 2);
const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2);
function onTextSelection(id: key<'#markerIndo'>) {
function onTextSelection(id: key<'#markerInfo'>) {
if (selection.current) {
const location = { ...selection.current, marker: id };
updateSelection({ location });
......@@ -133,18 +133,8 @@ const ASTview = () => {
async function onContextMenu(id: key<'#markerInfo'>) {
const items = [];
const selectedMarkerInfo = markersInfo.find((e) => e.key === id);
switch (selectedMarkerInfo?.kind) {
case 'function': {
items.push({
label: `Go to definition of ${selectedMarkerInfo.name}`,
onClick: () => {
const location = { function: selectedMarkerInfo.name };
updateSelection({ location });
},
});
break;
}
case 'declaration': {
if (selectedMarkerInfo?.var === 'function') {
if (selectedMarkerInfo.kind === 'declaration') {
if (selectedMarkerInfo?.name) {
const locations = await functionCallers(selectedMarkerInfo.name);
const locationsByFunction = _.groupBy(locations, (e) => e.function);
......@@ -162,10 +152,15 @@ const ASTview = () => {
});
});
}
break;
} else {
items.push({
label: `Go to definition of ${selectedMarkerInfo.name}`,
onClick: () => {
const location = { function: selectedMarkerInfo.name };
updateSelection({ location });
},
});
}
default:
break;
}
if (items.length > 0)
Dome.popupMenu(items);
......
......@@ -21,6 +21,7 @@ import ASTinfo from './ASTinfo';
import Globals from './Globals';
import Properties from './Properties';
import Locations from './Locations';
import Values from './Values';
// --------------------------------------------------------------------------
// --- Selection Controls
......@@ -101,6 +102,7 @@ export default (() => {
<ASTview />
<ASTinfo />
<Locations />
<Values />
</Group>
</LabView>
</Splitter>
......
// --------------------------------------------------------------------------
// --- Eva Values
// --------------------------------------------------------------------------
import React from 'react';
import * as States from 'frama-c/states';
import * as Json from 'dome/data/json';
import * as Eva from 'api/plugins/eva/values';
import * as Ast from 'api/kernel/ast';
import * as Compare from 'dome/data/compare';
import { Table, Column } from 'dome/table/views';
import { ArrayModel } from 'dome/table/arrays';
import { Component } from 'frama-c/LabViews';
import { Icon } from 'dome/controls/icons';
import { Label } from 'dome/controls/labels';
// --------------------------------------------------------------------------
// --- Columns
// --------------------------------------------------------------------------
const CallstackRenderer = (
(cs: Eva.callstack) => <Label label={cs.short} title={cs.full} />
);
const ColumnCallstack = () => Column({
id: 'callstack',
label: 'Callstack',
title: 'Context of the evaluation',
align: 'left',
width: 150,
render: CallstackRenderer,
});
const AlarmRenderer = (
(alarm: boolean) => <>{alarm && <Icon id="ATTENTION" />}</>
);
const ColumnAlarm = (props: { visible: boolean }) => Column({
id: 'alarm',
label: 'Alarm',
title: 'Did the evaluation emit an alarm?',
align: 'center',
width: 26,
fixed: true,
icon: 'WARNING',
visible: props.visible,
render: AlarmRenderer,
});
const byValues: Compare.ByFields<Eva.valuesData> =
{ callstack: Compare.defined(Compare.byFields({ full: Compare.string })) };
class ValuesModel extends ArrayModel<Json.key<'#values'>, Eva.valuesData> {
constructor() {
super();
this.setOrderingByFields(byValues);
}
}
// --------------------------------------------------------------------------
// --- Values Panel
// --------------------------------------------------------------------------
const Values = () => {
const model = React.useMemo(() => new ValuesModel(), []);
const evaValues = States.useSyncArray(Eva.values).getArray();
const selectMarker = States.useSelection()[0]?.current?.marker;
const markerInfo = States.useSyncArray(Ast.markerInfo).getArray();
const [name, setName] = React.useState<string | undefined>(undefined);
States.useRequest(Eva.getValues, selectMarker);
React.useEffect(() => {
model.removeAllData();
if (selectMarker && evaValues) {
const selectMarkerInfo = markerInfo.find((e) => e.key === selectMarker);
if (selectMarkerInfo && selectMarkerInfo.var !== 'function') {
switch (selectMarkerInfo.kind) {
case 'expression':
case 'lvalue':
evaValues.forEach((i) => model.setData(i.key, i));
setName(selectMarkerInfo.descr);
break;
case 'declaration':
evaValues.forEach((i) => model.setData(i.key, i));
setName(selectMarkerInfo.name);
break;
default:
setName(undefined);
}
}
} else {
setName(undefined);
}
model.reload();
}, [evaValues, selectMarker, markerInfo, model]);
// Component
return (
<>
<Table model={model}>
<ColumnCallstack />
<Column
id="value_before"
visible={!!name}
label={name && `${name} (before)`}
title="Values inferred by Eva just before the selected point"
disableSort
width={300}
/>
<ColumnAlarm visible={!!name} />
<Column
id="value_after"
visible={!!name}
label={name && `${name} (after)`}
title="Values inferred by Eva just after the selected point"
disableSort
width={300}
/>
</Table>
</>
);
};
// --------------------------------------------------------------------------
// --- Export Component
// --------------------------------------------------------------------------
export default () => (
<Component
id="frama-c.values"
label="Eva Values"
title="Values inferred by the Eva analysis"
>
<Values />
</Component>
);
// --------------------------------------------------------------------------
volatile int nondet;
void fun () {
int x = nondet;
x = -x;
}
void yet_another () {
int x = nondet;
fun ();
int y = 100 / x;
}
void main () {
fun ();
/*@ assert boh: 1 == 1; */
yet_another ();
int i = 0;
/*@ assert user: i == 0; */
}
......@@ -3337,6 +3337,15 @@ electron-devtools-installer@^2.2.4:
rimraf "^2.5.2"
semver "^5.3.0"
electron-devtools-installer@^3.0.0:
version "3.1.1"
resolved "https://registry.yarnpkg.com/electron-devtools-installer/-/electron-devtools-installer-3.1.1.tgz#7b56c8c86475c5e4e10de6917d150c53c9ceb55e"