diff --git a/ivette/api/plugins/eva/index.ts b/ivette/api/plugins/eva/general/index.ts similarity index 92% rename from ivette/api/plugins/eva/index.ts rename to ivette/api/plugins/eva/general/index.ts index 4b46b34354923641cd17852220a4a7ff037b790f..9f77331803e084829e2e0d6ac13847d0f4d7f625 100644 --- a/ivette/api/plugins/eva/index.ts +++ b/ivette/api/plugins/eva/general/index.ts @@ -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( diff --git a/ivette/api/plugins/eva/values/index.ts b/ivette/api/plugins/eva/values/index.ts new file mode 100644 index 0000000000000000000000000000000000000000..22375d253f9b2f0bac5f1242c8cfe80693973c0e --- /dev/null +++ b/ivette/api/plugins/eva/values/index.ts @@ -0,0 +1,154 @@ +/* --- 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; + +/* ------------------------------------- */ diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx index f97145728dc4ddb26db0f447df3a9c93aecd843a..86f89c08b215fd301838896fc79ca4c95709d5ad 100644 --- a/ivette/src/renderer/ASTview.tsx +++ b/ivette/src/renderer/ASTview.tsx @@ -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 }); diff --git a/ivette/src/renderer/Values.tsx b/ivette/src/renderer/Values.tsx index 2730471c3e08c07e7e917d40a094e67de443d5dd..00c174ed4a471ace61ec9a992531daba90a79157 100644 --- a/ivette/src/renderer/Values.tsx +++ b/ivette/src/renderer/Values.tsx @@ -2,9 +2,11 @@ // --- Eva Values // -------------------------------------------------------------------------- -import _ from 'lodash'; 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 { Table, Column } from 'dome/table/views'; import { ArrayModel } from 'dome/table/arrays'; @@ -16,19 +18,13 @@ import { Label } from 'dome/controls/labels'; // --- Columns // -------------------------------------------------------------------------- -interface Callstack { - id: number; - short: string; - full: string; -} - const ColumnCallstack = () => Column({ id: 'callstack', label: 'Callstack', title: 'Context of the evaluation', align: 'left', width: 100, - render: (cs: Callstack) => <Label label={cs.short} title={cs.full} />, + render: (cs: Eva.callstack) => <Label label={cs.short} title={cs.full} />, }); const ColumnAlarm = () => Column({ @@ -46,33 +42,30 @@ const ColumnAlarm = () => Column({ // --- Values Panel // -------------------------------------------------------------------------- -interface Value { - key: string; - callstack: Callstack; - value_before: string; - alarm: boolean; - value_after?: string; -} - const Values = () => { - const model = React.useMemo(() => new ArrayModel<Value>('key'), []); - const items = States.useSyncArray('eva.values'); - const [select] = States.useSelection(); - const marker = select?.current?.marker; - const t = States.useRequest('eva.values.compute', marker || ''); - const markerKinds = States.useSyncArray('kernel.ast.markerKind'); - const name = React.useRef(''); + const model = React.useMemo( + () => new ArrayModel<Json.key<'#values'>, Eva.valuesData>(), + [], + ); + + const items = States.useSyncArray(Eva.values).getArray(); + const marker = States.useSelection()[0]?.current?.marker; + const t = States.useRequest(Eva.getValues, marker); + const markerInfo = States.useSyncArray(Ast.markerInfo).getArray(); + const [name, setName] = React.useState(''); React.useEffect(() => { if (marker && items) { - const mark = markerKinds[marker]; - if (mark && mark.name) { - name.current = mark.name; + const m = markerInfo.find((e) => e.key === marker); + if (m) { + setName(m.descr); } - model.replace(_.toArray(items)); + model.removeAllData(); + items.forEach((i) => model.setData(i.key, i)); + model.reload(); } - }, [model, items, t, name, marker, markerKinds]); + }, [model, items, t, marker, markerInfo]); // Component return ( @@ -81,7 +74,7 @@ const Values = () => { <ColumnCallstack /> <Column id="value_before" - label={`${name.current} (before)`} + label={`${name} (before)`} title="Values inferred by Eva just before the selected point" disableSort fill @@ -89,7 +82,7 @@ const Values = () => { <ColumnAlarm /> <Column id="value_after" - label={`${name.current} (after)`} + label={`${name} (after)`} title="Values inferred by Eva just after the selected point" disableSort fill diff --git a/src/plugins/value/api/general_requests.ml b/src/plugins/value/api/general_requests.ml index 5c30a704fbcb1fc5e59c9b7bbcf611adc6091460..09877676a76673136ad2b7a7f7f179ec8cadfbdd 100644 --- a/src/plugins/value/api/general_requests.ml +++ b/src/plugins/value/api/general_requests.ml @@ -22,8 +22,13 @@ open Server -let package = Package.package ~plugin:"eva" - ~title:"Eva General Services" ~readme:"eva.md" () +let package = + Package.package + ~plugin:"eva" + ~name:"general" + ~title:"Eva General Services" + ~readme:"eva.md" + () module CallSite = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Stmt) diff --git a/src/plugins/value/api/values_request.ml b/src/plugins/value/api/values_request.ml index 68e837e3ebfe6432cc0cc847bc33e33b1d7c31cf..793f97b6127a323d7bcd27dd30c9af36d594dfe5 100644 --- a/src/plugins/value/api/values_request.ml +++ b/src/plugins/value/api/values_request.ml @@ -26,7 +26,12 @@ open Cil_types module Md = Markdown let package = - Package.package ~plugin:"eva" ~title:"Eva Values" ~readme:"eva.md" () + Package.package + ~plugin:"eva" + ~name:"values" + ~title:"Eva Values" + ~readme:"eva.md" + () type value = { value: string;