From 88c3379af03f7cb9ec6dc960399eea9461c0c1d3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 29 Jun 2020 15:38:11 +0200
Subject: [PATCH] [frama-c] upgrade API
---
ivette/api/dive/index.ts | 7 +++---
ivette/api/kernel/ast/index.ts | 22 +++++++++++-------
ivette/api/kernel/properties/index.ts | 11 +++++----
ivette/api/kernel/services/index.ts | 3 ++-
ivette/api/server_tsc.ml | 22 ++++++++++--------
ivette/src/renderer/ASTview.tsx | 2 +-
ivette/src/renderer/Globals.tsx | 20 ++---------------
ivette/src/renderer/Properties.tsx | 32 +++++++++++++--------------
8 files changed, 59 insertions(+), 60 deletions(-)
diff --git a/ivette/api/dive/index.ts b/ivette/api/dive/index.ts
index 7433dc5f951..a6bfaf5c218 100644
--- a/ivette/api/dive/index.ts
+++ b/ivette/api/dive/index.ts
@@ -68,7 +68,9 @@ export const addVar: Server.ExecRequest<variableName,Json.json> = {
};
/** Add all alarms of the given function */
-export const addFunctionAlarms: Server.ExecRequest<Json.key<'#fct'>,Json.json
+export const addFunctionAlarms: Server.ExecRequest<
+ Json.key<'#fct'>,
+ Json.json
> = {
kind: Server.RqKind.EXEC,
name: 'dive.addFunctionAlarms',
@@ -77,8 +79,7 @@ export const addFunctionAlarms: Server.ExecRequest<Json.key<'#fct'>,Json.json
};
/** Explore the graph starting from an existing vertex */
-export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json
- > = {
+export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
kind: Server.RqKind.EXEC,
name: 'dive.explore',
input: Json.jIndex<'#dive-node'>('#dive-node'),
diff --git a/ivette/api/kernel/ast/index.ts b/ivette/api/kernel/ast/index.ts
index 0709335396e..a7c5a9921cb 100644
--- a/ivette/api/kernel/ast/index.ts
+++ b/ivette/api/kernel/ast/index.ts
@@ -132,9 +132,11 @@ export const reloadMarkerInfo: Server.GetRequest<null,null> = {
};
/** Data fetcher for array [`markerInfo`](#markerinfo) */
-export const fetchMarkerInfo: Server.GetRequest<number,
+export const fetchMarkerInfo: Server.GetRequest<
+ number,
{ pending: number, updated: markerInfoData[],
- removed: Json.key<'#markerInfo'>[], reload: boolean }> = {
+ removed: Json.key<'#markerInfo'>[], reload: boolean }
+ > = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchMarkerInfo',
input: Json.jNumber,
@@ -147,12 +149,13 @@ export const fetchMarkerInfo: Server.GetRequest<number,
};
/** Marker informations */
-export const markerInfo: State.Array<'#markerInfo',markerInfoData> = {
+export const markerInfo: State.Array<Json.key<'#markerInfo'>,markerInfoData> = {
name: 'kernel.ast.markerInfo',
- key: 'key',
+ getkey: ((d:markerInfoData) => d.key),
signal: signalMarkerInfo,
fetch: fetchMarkerInfo,
reload: reloadMarkerInfo,
+ order: byMarkerInfoData,
};
/** Localizable AST markers */
@@ -244,9 +247,11 @@ export const reloadFunctions: Server.GetRequest<null,null> = {
};
/** Data fetcher for array [`functions`](#functions) */
-export const fetchFunctions: Server.GetRequest<number,
+export const fetchFunctions: Server.GetRequest<
+ number,
{ pending: number, updated: functionsData[],
- removed: Json.key<'#functions'>[], reload: boolean }> = {
+ removed: Json.key<'#functions'>[], reload: boolean }
+ > = {
kind: Server.RqKind.GET,
name: 'kernel.ast.fetchFunctions',
input: Json.jNumber,
@@ -259,12 +264,13 @@ export const fetchFunctions: Server.GetRequest<number,
};
/** AST Functions */
-export const functions: State.Array<'#functions',functionsData> = {
+export const functions: State.Array<Json.key<'#functions'>,functionsData> = {
name: 'kernel.ast.functions',
- key: 'key',
+ getkey: ((d:functionsData) => d.key),
signal: signalFunctions,
fetch: fetchFunctions,
reload: reloadFunctions,
+ order: byFunctionsData,
};
/** Get textual information about a marker */
diff --git a/ivette/api/kernel/properties/index.ts b/ivette/api/kernel/properties/index.ts
index f04292d0a80..3e336583d5a 100644
--- a/ivette/api/kernel/properties/index.ts
+++ b/ivette/api/kernel/properties/index.ts
@@ -299,9 +299,11 @@ export const reloadStatus: Server.GetRequest<null,null> = {
};
/** Data fetcher for array [`status`](#status) */
-export const fetchStatus: Server.GetRequest<number,
+export const fetchStatus: Server.GetRequest<
+ number,
{ pending: number, updated: statusData[], removed: Json.key<'#status'>[],
- reload: boolean }> = {
+ reload: boolean }
+ > = {
kind: Server.RqKind.GET,
name: 'kernel.properties.fetchStatus',
input: Json.jNumber,
@@ -314,12 +316,13 @@ export const fetchStatus: Server.GetRequest<number,
};
/** Status of Registered Properties */
-export const status: State.Array<'#status',statusData> = {
+export const status: State.Array<Json.key<'#status'>,statusData> = {
name: 'kernel.properties.status',
- key: 'key',
+ getkey: ((d:statusData) => d.key),
signal: signalStatus,
fetch: fetchStatus,
reload: reloadStatus,
+ order: byStatusData,
};
/* ------------------------------------- */
diff --git a/ivette/api/kernel/services/index.ts b/ivette/api/kernel/services/index.ts
index fcfcf35b1fb..7da04e4a0ae 100644
--- a/ivette/api/kernel/services/index.ts
+++ b/ivette/api/kernel/services/index.ts
@@ -25,7 +25,8 @@ import { jTagSafe } from 'api/kernel/data';
import { tag } from 'api/kernel/data';
/** Frama-C Kernel configuration */
-export const getConfig: Server.GetRequest<null,
+export const getConfig: Server.GetRequest<
+ null,
{ pluginpath: string[], libdir: string, datadir: string, version: string }
> = {
kind: Server.RqKind.GET,
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
index cf88117b4e2..3df4c37188e 100644
--- a/ivette/api/server_tsc.ml
+++ b/ivette/api/server_tsc.ml
@@ -311,7 +311,7 @@ let makeDeclaration fmt names d =
let output = typeOfParam rq.rq_output in
let makeParam fmt js = makeDecoder ~safe:false ~names fmt js in
Format.fprintf fmt
- "@[<hov 2>export const %s: Server.%sRequest<@,%a,@,%a@,> = {@]@\n"
+ "@[<hv 2>export const %s: Server.%sRequest<@,%a,@,%a@,>@] = {@\n"
self.name prefix jtype input jtype output ;
Format.fprintf fmt " kind: Server.RqKind.%s,@\n" kind ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident d.d_ident) ;
@@ -321,7 +321,7 @@ let makeDeclaration fmt names d =
| D_value js ->
Format.fprintf fmt
- "@[<hov 2>export const %s: State.Value<@,%a@,> = {@]@\n"
+ "@[<hv 2>export const %s: State.Value<@,%a@,>@] = {\n"
self.name jtype js ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident self) ;
Format.fprintf fmt " signal: %a,@\n"
@@ -332,7 +332,7 @@ let makeDeclaration fmt names d =
| D_state js ->
Format.fprintf fmt
- "@[<hov 2>export const %s: State.State<@,%a@,> = {@]@\n"
+ "@[<hv 2>export const %s: State.State<@,%a@,>@] = {@\n"
self.name jtype js ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident self) ;
Format.fprintf fmt " signal: %a,@\n"
@@ -345,34 +345,38 @@ let makeDeclaration fmt names d =
| D_array { arr_key ; arr_kind } ->
let data = Pkg.Derived.data self in
+ let jkey = (Pkg.Jkey arr_kind) in
+ let jrow = (Pkg.Jdata data) in
Format.fprintf fmt
- "@[<hov 2>export const %s: State.Array<@,'#%s',@,%a@,> = {@]@\n"
- self.name arr_kind (jcall names) data ;
+ "@[<hv 2>export const %s: State.Array<@,%a,@,%a@,>@] = {@\n"
+ self.name jtype jkey jtype jrow ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident self) ;
- Format.fprintf fmt " key: '%s',@\n" arr_key ;
+ Format.fprintf fmt " getkey: ((d:%a) => d.%s),@\n" jtype jrow arr_key ;
Format.fprintf fmt " signal: %a,@\n"
(jcall names) (Pkg.Derived.signal self) ;
Format.fprintf fmt " fetch: %a,@\n"
(jcall names) (Pkg.Derived.fetch self) ;
Format.fprintf fmt " reload: %a,@\n"
(jcall names) (Pkg.Derived.reload self) ;
+ Format.fprintf fmt " order: %a,@\n"
+ (jcall names) (Pkg.Derived.order data) ;
Format.fprintf fmt "};@\n"
| D_safe(id,js) ->
Format.fprintf fmt
- "@[<hov 2>export const %s: Json.Safe<@,%a@,> =@ %a;@]\n"
+ "@[<hov 2>@[<hv 0>export const %s: Json.Safe<@,%a@,>@] =@ %a;@]\n"
self.name (jcall names) id
(makeRecursive (makeRootDecoder ~safe:true ~self:id ~names)) js
| D_loose(id,js) ->
Format.fprintf fmt
- "@[<hov 2>export const %s: Json.Loose<@,%a@,> =@ %a;@]\n"
+ "@[<hov 2>@[<hv 0>export const %s: Json.Loose<@,%a@,>@] =@ %a;@]\n"
self.name (jcall names) id
(makeRecursive (makeRootDecoder ~safe:false ~self:id ~names)) js
| D_order(id,js) ->
Format.fprintf fmt
- "@[<hov 2>export const %s: Compare.Order<@,%a@,> =@ %a;@]\n"
+ "@[<hov 2>@[<hv 0>export const %s: Compare.Order<@,%a@,>@] =@ %a;@]\n"
self.name (jcall names) id
(makeRecursive2 (makeOrder ~self:id ~names)) js
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 5ec7d4272ee..5fc898ca878 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -78,7 +78,7 @@ const ASTview = () => {
const [theme, setTheme] = Dome.useGlobalSetting('ASTview.theme', 'default');
const [fontSize, setFontSize] = Dome.useGlobalSetting('ASTview.fontSize', 12);
const [wrapText, setWrapText] = Dome.useSwitch('ASTview.wrapText', false);
- const markers = States.useSyncArray(markerInfo);
+ const markers = States.useSyncModel(markerInfo);
const theFunction = selection?.current?.function;
const theMarker = selection?.current?.marker;
diff --git a/ivette/src/renderer/Globals.tsx b/ivette/src/renderer/Globals.tsx
index 94a501716c0..5d4e1cd82df 100644
--- a/ivette/src/renderer/Globals.tsx
+++ b/ivette/src/renderer/Globals.tsx
@@ -3,10 +3,8 @@
// --------------------------------------------------------------------------
import React from 'react';
-import * as Dome from 'dome';
import { Section, Item } from 'dome/frame/sidebars';
import * as States from 'frama-c/states';
-import { alpha } from 'dome/data/compare';
import { functions, functionsData } from 'api/kernel/ast';
// --------------------------------------------------------------------------
@@ -17,23 +15,9 @@ export default () => {
// Hooks
const [selection, updateSelection] = States.useSelection();
- const model = States.useSyncArray(functions);
- const forceUpdate = Dome.useForceUpdate() as (() => void);
- React.useEffect(() => {
- model.setNaturalOrder((f1, f2) => alpha(f1.name, f2.name));
- const client = model.link();
- client.onReload(forceUpdate);
- client.onUpdate(forceUpdate);
- return client.unlink;
- }, [model, forceUpdate]);
-
- // Functions
- const n = model.getRowCount();
- const fcts: functionsData[] = [];
- for (let i = 0; i < n; i++) {
- fcts.push(model.getRowAt(i));
- }
+ const fcts = States.useSyncArray(functions);
+ // Items
const current: undefined | string = selection?.current?.function;
const makeFctItem = (fct: functionsData) => {
const kf = fct.name;
diff --git a/ivette/src/renderer/Properties.tsx b/ivette/src/renderer/Properties.tsx
index 6e44c4a4d55..b3b63b9c570 100644
--- a/ivette/src/renderer/Properties.tsx
+++ b/ivette/src/renderer/Properties.tsx
@@ -3,12 +3,14 @@
// --------------------------------------------------------------------------
import _ from 'lodash';
-import React from 'react';
+import React, { useEffect } from 'react';
import * as Dome from 'dome';
+import { key } from 'dome/data/json';
import * as States from 'frama-c/states';
import * as Compare from 'dome/data/compare';
import { Label, Code } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
+import * as Models from 'dome/table/models';
import * as Arrays from 'dome/table/arrays';
import { Table, Column, ColumnProps, Renderer } from 'dome/table/views';
import { TitleBar, Component } from 'frama-c/LabViews';
@@ -238,13 +240,13 @@ const byColumn: Arrays.ByColumns<Property> = {
file: Compare.byFields<Property>({ source: byFile }),
};
-class PropertyModel extends Arrays.ArrayModel<Property> {
+class PropertyModel extends Arrays.CompactModel<key<'#status'>, Property> {
private filterFun?: string;
private filterProp = _.cloneDeep(defaultFilter);
constructor() {
- super('key');
+ super((p: Property) => p.key);
this.setOrderingByFields(byProperty);
this.setColumnOrder(byColumn);
this.setFilter(this.filterItem.bind(this));
@@ -410,19 +412,13 @@ const PropertyColumns = () => {
};
function FilterRatio({ model }: { model: PropertyModel }) {
- const forceUpdate = Dome.useForceUpdate() as (() => void);
- React.useEffect(() => {
- const client = model.link();
- client.onReload(forceUpdate);
- return client.unlink;
- });
- const filtered = model.getRowCount();
- const total = model.getTotalRowCount();
+ Models.useModel(model);
+ const [filtered, total] = [model.getRowCount(), model.getTotalRowCount()];
return (
<Label
className="component-info"
title="Displayed Properties / Total"
- display={filtered !== total}
+ display={filtered !== total || true}
>
{filtered} / {total}
</Label>
@@ -436,8 +432,12 @@ function FilterRatio({ model }: { model: PropertyModel }) {
const RenderTable = () => {
// Hooks
const model = React.useMemo(() => new PropertyModel(), []);
-
- States.useSyncArray<'#status', Property>(Properties.status, model);
+ const data = States.useSyncArray(Properties.status);
+ useEffect(() => {
+ model.removeAllData();
+ model.updateData(data);
+ model.reload();
+ }, [model, data]);
const [selection, updateSelection] = States.useSelection();
@@ -454,8 +454,8 @@ const RenderTable = () => {
// Callbacks
const onPropertySelection = React.useCallback(
- ({ key, function: fct }: Property) => {
- const location = { function: fct, marker: key };
+ ({ key: propKey, function: fct }: Property) => {
+ const location = { function: fct, marker: propKey };
updateSelection({ location });
}, [updateSelection],
);
--
GitLab