Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • pub/frama-c
  • proidiot/frama-c
  • lthls/frama-c
3 results
Show changes
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 2845 additions and 1318 deletions
ivette/src/frama-c/plugins/eva/stacks.ts deleted 100644 → 0
View file @ 5e23a535
/* ************************************************************************ */
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2022 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/* ************************************************************************ */
// --------------------------------------------------------------------------
// --- CallStacks
// --------------------------------------------------------------------------
import * as Server from 'frama-c/server';
import * as Ast from 'frama-c/kernel/api/ast';
import * as Values from 'frama-c/plugins/eva/api/values';
import { ModelCallbacks } from './cells';
// --------------------------------------------------------------------------
// --- Callstack infos
// --------------------------------------------------------------------------
export type callstacks = Values.callstack[];
export interface Callsite {
callee: string;
caller?: string;
stmt?: Ast.marker;
}
function equalSite(a: Callsite, b: Callsite): boolean {
return a.stmt === b.stmt && a.callee === b.callee;
}
// --------------------------------------------------------------------------
// --- CallStacks Cache
// --------------------------------------------------------------------------
export class StacksCache {
private readonly model: ModelCallbacks;
private readonly stacks = new Map<string, callstacks>();
private readonly summary = new Map<string, boolean>();
private readonly calls = new Map<Values.callstack, Callsite[]>();
// --------------------------------------------------------------------------
// --- LifeCycle
// --------------------------------------------------------------------------
constructor(state: ModelCallbacks) {
this.model = state;
}
clear(): void {
this.stacks.clear();
this.calls.clear();
}
// --------------------------------------------------------------------------
// --- Getters
// --------------------------------------------------------------------------
getSummary(fct: string): boolean {
return this.summary.get(fct) ?? true;
}
setSummary(fct: string, s: boolean): void {
this.summary.set(fct, s);
this.model.forceLayout();
}
getStacks(...markers: Ast.marker[]): callstacks {
if (markers.length === 0) return [];
const key = markers.join('$');
const cs = this.stacks.get(key);
if (cs !== undefined) return cs;
this.stacks.set(key, []);
this.requestStacks(key, markers);
return [];
}
getCalls(cs: Values.callstack): Callsite[] {
const fs = this.calls.get(cs);
if (fs !== undefined) return fs;
this.calls.set(cs, []);
this.requestCalls(cs);
return [];
}
aligned(a: Values.callstack, b: Values.callstack): boolean {
if (a === b) return true;
const ca = this.getCalls(a);
const cb = this.getCalls(b);
let ka = ca.length - 1;
let kb = cb.length - 1;
while (ka >= 0 && kb >= 0 && equalSite(ca[ka], cb[kb])) {
--ka;
--kb;
}
return ka < 0 || kb < 0;
}
// --------------------------------------------------------------------------
// --- Fetchers
// --------------------------------------------------------------------------
private requestStacks(key: string, markers: Ast.marker[]): void {
Server
.send(Values.getCallstacks, markers)
.then((stacks: callstacks) => {
this.stacks.set(key, stacks);
this.model.forceLayout();
this.model.forceUpdate();
});
}
private requestCalls(cs: Values.callstack): void {
Server
.send(Values.getCallstackInfo, cs)
.then((calls) => {
this.calls.set(cs, calls);
this.model.forceUpdate();
});
}
}
// --------------------------------------------------------------------------
ivette/src/frama-c/plugins/eva/style.css
View file @ b7ce41a1
/* -------------------------------------------------------------------------- */
/* --- Probe Panel --- */
/* --- Call Stack Info --- */
/* -------------------------------------------------------------------------- */
.eva-probeinfo {
min-height: 32px;
padding-left: 6px;
padding-top: 2px;
padding-bottom: 4px;
width: 100%;
background: var(--background-profound);
display: flex;
:root {
--eva-min-width: 90px;
}
.eva-probeinfo-label {
flex: 0 1 auto;
min-width: 22px;
text-align: left;
.eva-info {
width: 100%;
display: flex;
flex-wrap: nowrap;
align-items: center;
background: var(--background-profound);
padding: 2px;
}
.eva-probeinfo-code {
flex: 0 1 auto;
height: fit-content;
background: var(--background-intense);
min-width: 120px;
width: auto;
border: thin solid var(--border);
padding-left: 6px;
padding-right: 6px;
border-radius: 4px;
overflow: hidden;
.eva-info-wrap {
flex: auto;
flex-wrap: wrap;
}
.eva-probeinfo-stmt {
flex: 0 0 auto;
margin-left: 2px;
margin-right: 0px;
margin-top: 2px;
.eva-callsite {
flex: 0 0 auto;
fill: var(--selected-element);
background: var(--background-softer);
border-radius: 4px;
border: thin solid var(--border);
padding-right: 7px;
}
.eva-probeinfo-button {
flex: 0 0 auto;
margin: 1px;
min-width: 16px;
.eva-cell-container {
display: flex;
justify-content: center;
}
.eva-probeinfo-state {
margin-top: 2px;
margin-bottom: 2px;
.eva-cell-left {
flex: 1;
}
/* -------------------------------------------------------------------------- */
/* --- Call Satck Info --- */
/* -------------------------------------------------------------------------- */
.eva-info {
width: 100%;
flex-wrap: wrap;
background: var(--background-profound);
padding-top: 3px;
padding-left: 12px;
padding-bottom: 2px;
.eva-cell-content {
margin-left: 4px;
margin-right: 4px;
flex: 0 auto;
overflow: hidden;
display: flex;
align-items: baseline;
}
.eva-callsite {
flex: 0 0 auto;
fill: var(--selected-element);
background: var(--background-softer);
border-radius: 4px;
border: thin solid var(--border);
padding-right: 7px;
}
.eva-callsite.eva-focused {
background: var(--warning-button-color);
.eva-header-text-overflow {
overflow: hidden;
text-overflow: ellipsis;
}
.eva-callsite.eva-focused.eva-transient {
background: var(--code-select);
.eva-cell-right {
display: flex;
flex: 1;
min-width: max-content;
justify-content: flex-end;
}
/* -------------------------------------------------------------------------- */
......@@ -84,17 +64,15 @@
/* -------------------------------------------------------------------------- */
.eva-cell-alarms {
fill: orange;
position: absolute;
top: -1px;
right: 3px;
z-index: 1;
margin: 0px;
padding: 0px;
margin-right: 4px;
}
.eva-alarm-info {
font-size: x-small;
padding: 0px;
margin: 1px;
font-size: x-small;
padding: 0px;
margin: 1px;
}
.eva-alarm-none { display: none; }
......@@ -103,173 +81,225 @@
.eva-alarm-Unknown { fill: var(--eva-alarms-unknown); }
/* -------------------------------------------------------------------------- */
/* --- Styling Values --- */
/* --- Styling Statement display --- */
/* -------------------------------------------------------------------------- */
.eva-stmt {
color: var(--info-text);
text-select: none;
}
.eva-sized-area {
padding: 3px;
white-space: pre;
overflow: hidden;
text-overflow: ellipsis;
color: var(--info-text);
font-weight: normal;
}
/* -------------------------------------------------------------------------- */
/* --- Table Rows --- */
/* --- Function Section Header --- */
/* -------------------------------------------------------------------------- */
.eva-row {
display: flex;
position: relative;
flex: 0 1 auto;
height: 100%;
.eva-function {
padding: 2px;
background: var(--background-profound);
height: 25px;
align-items: center;
}
.eva-fct-fold {
margin-left: 4px;
margin-right: 8px;
padding: 0px;
}
.eva-fct-name {
font-weight: bold;
}
/* -------------------------------------------------------------------------- */
/* --- Table Heads --- */
/* --- Table General CSS --- */
/* -------------------------------------------------------------------------- */
.eva-function {
padding-top: 0px;
background: var(--background-profound);
.eva-table {
border: 0px;
border-spacing: 0px;
}
.eva-table-header-sticky {
position: sticky;
top: 0;
z-index: +1;
}
.eva-head {
padding-top: 2px;
color: var(--info-text);
text-align: center;
border-left: thin solid var(--border);
border-bottom: thin solid var(--border);
.eva-table tr:nth-child(n + 4) {
cursor: pointer;
}
.eva-probes .eva-head {
border-top: thin solid var(--border);
.eva-table tr th {
border-right: thin solid var(--border);
border-top: thin solid var(--border);
border-bottom: thin solid var(--border);
height: 22px;
min-height: 22px;
max-height: 22px;
min-width: calc(var(--eva-min-width) + 30px);
max-width: calc(var(--eva-min-width) + 30px);
}
.eva-phantom {
visibility: hidden;
height: 0;
.eva-table tr:nth-child(2n) {
background-color: var(--background-alterning-even);
}
.eva-table tr:nth-child(2n + 1) {
background-color: var(--background-alterning-odd);
}
.eva-table-container {
position: relative;
overflow: auto;
height: 100%;
min-height: 66px;
}
.eva-functions-section {
display: grid;
overflow: auto;
align-content: start;
}
.eva-nb-callstacks {
color: var(--info-text);
padding-right: 11px;
}
/* -------------------------------------------------------------------------- */
/* --- Table Cells --- */
/* --- Table Headers CSS --- */
/* -------------------------------------------------------------------------- */
.eva-fct-fold {
margin-left: 4px;
margin-right: 8px;
padding: 0px;
.eva-header-tracked {
}
.eva-fct-name {
padding: 2px;
font-weight: bold;
.eva-header-tracked-focused {
}
.eva-cell {
flex: 1 1 auto;
border-right: thin solid var(--border);
border-bottom: thin solid var(--border);
overflow: hidden;
display: flex;
justify-content: center;
position: relative;
.eva-header-just-focused {
background: var(--code-select);
}
.eva-cell .eva-stmt {
margin-left: 0.2em;
padding: 2px 0px;
.eva-header-pinned {
background: var(--eva-probes-pinned);
}
.eva-cell-expression {
text-align: center;
text-overflow: ellipsis;
flex: 0 1 auto;
display: inline-block;
overflow: hidden;
.eva-header-pinned-focused {
background: var(--eva-probes-pinned-focused);
}
.eva-cell:nth-child(2) {
border-left: thin solid var(--border);
.eva-header-after-condition {
display: flex;
justify-content: center;
gap: 0.3em;
}
.eva-probes .eva-cell {
padding: 2px 4px;
text-align: center;
border-top: thin solid var(--border);
.eva-header-buttons-container {
position: absolute;
right: 1px;
top: 0px;
padding-left: 2px;
display: flex;
z-index: +1;
background: inherit;
}
.eva-cell * {
user-select: text;
.eva-header-button {
padding: 2px 2px 3px 2px;
}
.eva-header-text {
display: flex;
}
/* -------------------------------------------------------------------------- */
/* --- Cell Diffs --- */
/* --- Table Callsite Boxes --- */
/* -------------------------------------------------------------------------- */
.eva-diff-shadow {
border: solid transparent 2px;
position: relative;
z-index: -1;
.eva-table-callsite-box {
width: 18px;
min-width: 18px;
background: var(--background);
border: 0px;
text-align: center;
color: var(--info-text);
border-left: thin solid var(--border);
border-right: thin solid var(--border);
border-bottom: thin solid var(--border);
padding: 2px;
}
.eva-diff-added { }
.eva-diff-removed { text-decoration: strike }
.eva-state-Before .eva-diff { background: var(--eva-state-before); }
.eva-state-After .eva-diff { background: var(--eva-state-after); }
.eva-state-Cond .eva-diff { background: var(--eva-state-before); }
.eva-state-Then .eva-diff { background: var(--eva-state-then); }
.eva-state-Else .eva-diff { background: var(--eva-state-else); }
tr:first-of-type > .eva-table-callsite-box {
border-top: thin solid var(--border);
}
/* -------------------------------------------------------------------------- */
/* --- Table Rows Background --- */
/* --- Table Values --- */
/* -------------------------------------------------------------------------- */
/* --- Probes --- */
.eva-probes .eva-cell {
background: var(--eva-probes-pinned);
.eva-table-values {
position: relative;
border: 0px;
padding: 2px 3px 2px 3px;
border-bottom: thin solid var(--border);
border-right: thin solid var(--border);
min-width: var(--eva-min-width);
font-family: Andale Mono, monospace;
font-size: 9pt;
height: 22px;
min-height: 22px;
max-height: 22px;
white-space: pre;
}
.eva-probes .eva-focused {
background: var(--eva-probes-pinned-focused);
.eva-table-descrs {
background-color: var(--background-sidebar);
border-right: thin solid var(--border);
}
.eva-probes .eva-transient {
background: var(--eva-probes-transient);
align-items: center;
.eva-table-descr-sticky {
position: sticky;
top: 22px;
z-index: +1;
}
.eva-probes .eva-transient.eva-focused {
background: var(--eva-probes-transient-focused);
.eva-table-callsite-box.eva-table-header-sticky {
left: 0px;
z-index: +2;
}
.eva-table-value-sticky {
position: sticky;
left: 0px;
z-index: +1;
}
/* --- Values / Callstacks --- */
.eva-values .eva-cell {
background: var(--background-alterning-odd);
.eva-values-position {
display: inline-block;
width: 0px;
}
.eva-callstack.eva-row-odd .eva-cell {
background: var(--background-alterning-odd);
.eva-table-text {
cursor: text;
user-select: text;
margin-left: 1px;
margin-right: 1px;
}
.eva-callstack.eva-row-even .eva-cell {
background: var(--background-alterning-even);
/* -------------------------------------------------------------------------- */
/* --- Miscellaneous --- */
/* -------------------------------------------------------------------------- */
.eva-button {
margin: 0px;
}
.eva-callstack.eva-row-aligned {
background: var(--grid-layout-holder);
.eva-italic {
font-style: italic;
}
.eva-callstack.eva-row-selected {
background: var(--code-select);
.eva-focused {
background: var(--code-select);
}
/* -------------------------------------------------------------------------- */
ivette/src/frama-c/plugins/eva/valueinfos.tsx deleted 100644 → 0
View file @ 5e23a535
/* ************************************************************************ */
/* */
/* This file is part of Frama-C. */
/* */
/* Copyright (C) 2007-2022 */
/* CEA (Commissariat à l'énergie atomique et aux énergies */
/* alternatives) */
/* */
/* you can redistribute it and/or modify it under the terms of the GNU */
/* Lesser General Public License as published by the Free Software */
/* Foundation, version 2.1. */
/* */
/* It is distributed in the hope that it will be useful, */
/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
/* GNU Lesser General Public License for more details. */
/* */
/* See the GNU Lesser General Public License version 2.1 */
/* for more details (enclosed in the file licenses/LGPLv2.1). */
/* */
/* ************************************************************************ */
/* eslint-disable @typescript-eslint/explicit-function-return-type */
// --------------------------------------------------------------------------
// --- Info Components
// --------------------------------------------------------------------------
// React & Dome
import React from 'react';
import { classes } from 'dome/misc/utils';
import { Hpack, Vpack } from 'dome/layout/boxes';
import { Code, Cell } from 'dome/controls/labels';
import * as States from 'frama-c/states';
import * as Ast from 'frama-c/kernel/api/ast';
import { ModelProp } from 'frama-c/plugins/eva/model';
// Locals
import { EvaAlarm } from './cells';
import { Callsite } from './stacks';
// --------------------------------------------------------------------------
// --- Stmt Printer
// --------------------------------------------------------------------------
interface StmtProps {
stmt?: Ast.marker;
marker: Ast.marker;
short?: boolean;
}
export function Stmt(props: StmtProps) {
const markersInfo = States.useSyncArray(Ast.markerInfo);
const { stmt, marker, short } = props;
if (!stmt) return null;
const line = markersInfo.getData(marker)?.sloc?.line;
const filename = markersInfo.getData(marker)?.sloc?.base;
const title = markersInfo.getData(stmt)?.descr;
const text = short ? `@L${line}` : `@${filename}:${line}`;
return (
<span className="dome-text-cell eva-stmt" title={title}>
{text}
</span>
);
}
// --------------------------------------------------------------------------
// --- Alarms Panel
// --------------------------------------------------------------------------
export function AlarmsInfos(props: ModelProp) {
const { model } = props;
const probe = model.getFocused();
if (probe) {
const callstack = model.getCallstack();
const domain = model.values.getValues(probe, callstack);
const alarms = domain?.vBefore.alarms ?? [];
if (alarms.length > 0) {
const renderAlarm = ([status, alarm]: EvaAlarm) => {
const className = `eva-alarm-info eva-alarm-${status}`;
return (
<Code className={className} icon="WARNING">{alarm}</Code>
);
};
return (
<Vpack className="eva-info">
{React.Children.toArray(alarms.map(renderAlarm))}
</Vpack>
);
}
}
return null;
}
// --------------------------------------------------------------------------
// --- Stack Panel
// --------------------------------------------------------------------------
export function StackInfos(props: ModelProp) {
const { model } = props;
const [, setSelection] = States.useSelection();
const focused = model.getFocused();
const callstack = model.getCalls();
if (callstack.length <= 1) return null;
const makeCallsite = ({ caller, stmt }: Callsite) => {
if (!caller || !stmt) return null;
const key = `${caller}@${stmt}`;
const isFocused = focused?.marker === stmt;
const isTransient = focused?.transient;
const className = classes(
'eva-callsite',
isFocused && 'eva-focused',
isTransient && 'eva-transient',
);
const select = (meta: boolean) => {
const location = { fct: caller, marker: stmt };
setSelection({ location });
if (meta) States.MetaSelection.emit(location);
};
const onClick = (evt: React.MouseEvent) => {
select(evt.altKey);
};
const onDoubleClick = (evt: React.MouseEvent) => {
evt.preventDefault();
select(true);
};
return (
<Cell
key={key}
icon="TRIANGLE.LEFT"
className={className}
onClick={onClick}
onDoubleClick={onDoubleClick}
>
{caller}
<Stmt stmt={stmt} marker={stmt} />
</Cell>
);
};
return (
<Hpack className="eva-info">
{callstack.map(makeCallsite)}
</Hpack>
);
}
// --------------------------------------------------------------------------
ivette/src/frama-c/utils.ts → ivette/src/frama-c/richtext.tsx
View file @ b7ce41a1
......@@ -26,12 +26,14 @@
/**
* @packageDocumentation
* @module frama-c/utils
*/
* @module frama-c/richtext
*/
import React from 'react';
import * as Dome from 'dome';
import * as DomeBuffers from 'dome/text/buffers';
import * as KernelData from 'frama-c/kernel/api/data';
import { classes } from 'dome/misc/utils';
const D = new Dome.Debug('Utils');
......@@ -42,33 +44,82 @@ const D = new Dome.Debug('Utils');
/**
* Print text containing tags into buffer.
* @param buffer Rich text buffer to print into.
* @param contents Actual text containing tags.
* @param text Actual text containing tags.
* @param options Specify particular marker options.
*/
export function printTextWithTags(
buffer: DomeBuffers.RichTextBuffer,
contents: KernelData.text,
text: KernelData.text,
options?: DomeBuffers.MarkerProps,
): void {
if (Array.isArray(contents)) {
let marker = false;
const tag = contents.shift();
if (tag) {
if (Array.isArray(tag)) {
contents.unshift(tag);
} else {
buffer.openTextMarker({ id: tag, ...options ?? {} });
marker = true;
}
if (Array.isArray(text)) {
const tag = text[0];
const marker = typeof (tag) === 'string';
if (marker) {
buffer.openTextMarker({ id: tag, ...options ?? {} });
}
for (let k = marker ? 1 : 0; k < text.length; k++) {
printTextWithTags(buffer, text[k], options);
}
contents.forEach((txt) => printTextWithTags(buffer, txt, options));
if (marker) {
marker = false;
buffer.closeTextMarker();
}
} else if (typeof contents === 'string') {
buffer.append(contents);
} else if (typeof text === 'string') {
buffer.append(text);
} else {
D.error('Unexpected text', contents);
D.error('Unexpected text', text);
}
}
// --------------------------------------------------------------------------
// --- Lightweight Text Renderer
// --------------------------------------------------------------------------
interface MarkerProps {
marker: string;
onMarker?: (marker: string) => void;
children?: React.ReactNode;
}
function Marker(props: MarkerProps): JSX.Element {
const { marker, onMarker, children } = props;
const onClick = (): void => { if (onMarker) onMarker(marker); };
return (
<span
className="kernel-text-marker"
onClick={onClick}
>
{children}
</span>
);
}
function makeContents(text: KernelData.text): React.ReactNode {
if (Array.isArray(text)) {
const tag = text[0];
const marker = tag && typeof (tag) === 'string';
const array = marker ? text.slice(1) : text;
const contents = React.Children.toArray(array.map(makeContents));
if (marker) {
return <Marker marker={tag}>{contents}</Marker>;
}
return <>{contents}</>;
} if (typeof text === 'string') {
return text;
}
D.error('Unexpected text', text);
return null;
}
export interface TextProps {
text: KernelData.text;
onMarker?: (marker: string) => void;
className?: string;
}
export function Text(props: TextProps): JSX.Element {
const className = classes('kernel-text', 'dome-text-code', props.className);
return <div className={className}>{makeContents(props.text)}</div>;
}
// --------------------------------------------------------------------------
ivette/src/frama-c/server.ts
View file @ b7ce41a1
......@@ -50,8 +50,10 @@ export enum Status {
OFF = 'OFF',
/** Server is starting, but not on yet. */
STARTING = 'STARTING',
/** Server is on. */
/** Server is running. */
ON = 'ON',
/** Server is running command line. */
CMD = 'CMD',
/** Server is halting, but not off yet. */
HALTING = 'HALTING',
/** Server is restarting. */
......@@ -76,7 +78,7 @@ const STATUS = new Dome.Event<Status>('frama-c.server.status');
/**
* Server is actually started and running.
* This event is emitted when ther server _enters_ the `ON` state.
* This event is emitted when ther server _enters_ the `ON` or `CMD` state.
* The server is now ready to handle requests.
*/
const READY = new Dome.Event('frama-c.server.ready');
......@@ -84,7 +86,7 @@ const READY = new Dome.Event('frama-c.server.ready');
/**
* Server Status Notification Event
* This event is emitted when ther server _leaves_ the `ON` state.
* This event is emitted when ther server _leaves_ the `ON` or `CMD` state.
* The server is no more able to handle requests until restart.
*/
const SHUTDOWN = new Dome.Event('frama-c.server.shutdown');
......@@ -121,7 +123,7 @@ const pending = new Map<string, PendingRequest>();
let process: ChildProcess | undefined;
/** Polling timeout when server is busy. */
const pollingTimeout = 200;
const pollingTimeout = 50;
let pollingTimer: NodeJS.Timeout | undefined;
/** Killing timeout and timer for server process hard kill. */
......@@ -154,11 +156,17 @@ export function useStatus(): Status {
return status;
}
const running = (st: Status): boolean =>
(st === Status.ON || st === Status.CMD);
/**
* Whether the server is running and ready to handle requests.
* @return {boolean} Whether server stage is [[ON]].
* @return {boolean} Whether server is in running stage,
* defined by status `ON` or `CMD`.
*/
export function isRunning(): boolean { return status === Status.ON; }
export function isRunning(): boolean {
return running(status);
}
/**
* Number of requests still pending.
......@@ -170,7 +178,7 @@ export function getPending(): number {
/**
* Register callback on `READY` event.
* @param {function} callback Invoked when the server enters [[ON]] stage.
* @param {function} callback Invoked when the server enters running stage.
*/
export function onReady(callback: () => void): void {
READY.on(callback);
......@@ -178,7 +186,7 @@ export function onReady(callback: () => void): void {
/**
* Register callback on `SHUTDOWN` event.
* @param {function} callback Invoked when the server leaves [[ON]] stage.
* @param {function} callback Invoked when the server leaves running stage.
*/
export function onShutdown(callback: () => void): void {
SHUTDOWN.on(callback);
......@@ -193,11 +201,15 @@ function _status(newStatus: Status): void {
const oldStatus = status;
status = newStatus;
STATUS.emit(newStatus);
if (oldStatus === Status.ON) SHUTDOWN.emit();
if (newStatus === Status.ON) READY.emit();
const oldRun = running(oldStatus);
const newRun = running(newStatus);
if (oldRun && !newRun) SHUTDOWN.emit();
if (!oldRun && newRun) READY.emit();
}
}
const _update: () => void = debounce(() => STATUS.emit(status), 100);
// --------------------------------------------------------------------------
// --- Server Control (Start)
// --------------------------------------------------------------------------
......@@ -226,6 +238,7 @@ export async function start(): Promise<void> {
_status(Status.RESTARTING);
return;
case Status.ON:
case Status.CMD:
case Status.STARTING:
return;
default:
......@@ -252,6 +265,7 @@ export function stop(): void {
_kill();
return;
case Status.ON:
case Status.CMD:
case Status.HALTING:
_status(Status.HALTING);
_shutdown();
......@@ -283,6 +297,7 @@ export function stop(): void {
export function kill(): void {
switch (status) {
case Status.ON:
case Status.CMD:
case Status.HALTING:
case Status.STARTING:
case Status.RESTARTING:
......@@ -318,6 +333,7 @@ export function restart(): void {
start();
return;
case Status.ON:
case Status.CMD:
_status(Status.RESTARTING);
_shutdown();
return;
......@@ -477,6 +493,26 @@ async function _launch(): Promise<void> {
client.connect(sockaddr);
}
// --------------------------------------------------------------------------
// --- Polling Management
// --------------------------------------------------------------------------
function _startPolling(): void {
if (!pollingTimer) {
const polling = (config && config.polling) || pollingTimeout;
pollingTimer = setInterval(() => {
client.poll();
}, polling);
}
}
function _stopPolling(): void {
if (pollingTimer) {
clearInterval(pollingTimer);
pollingTimer = undefined;
}
}
// --------------------------------------------------------------------------
// --- Low-level Killing
// --------------------------------------------------------------------------
......@@ -485,10 +521,7 @@ function _clear(): void {
rqCount = 0;
pending.forEach((p: PendingRequest) => p.reject('clear'));
pending.clear();
if (pollingTimer) {
clearTimeout(pollingTimer);
pollingTimer = undefined;
}
_stopPolling();
if (killingTimer) {
clearTimeout(killingTimer);
killingTimer = undefined;
......@@ -732,12 +765,8 @@ export function send<In, Out>(
});
response.kill = () => pending.get(rid)?.reject('kill');
client.send(request.kind, rid, request.name, param as unknown as Json.json);
if (!pollingTimer) {
const polling = (config && config.polling) || pollingTimeout;
pollingTimer = setInterval(() => {
client.poll();
}, polling);
}
_startPolling();
_update();
return response;
}
......@@ -747,20 +776,20 @@ export function send<In, Out>(
function _resolved(id: string): void {
pending.delete(id);
if (pending.size === 0) {
if (pending.size === 0 && status === Status.ON) {
rqCount = 0;
if (pollingTimer) {
clearInterval(pollingTimer);
pollingTimer = undefined;
}
_stopPolling();
_update();
}
}
client.onConnect((err?: Error) => {
if (err) {
_status(Status.FAILURE);
_clear();
} else {
_status(Status.ON);
_status(Status.CMD);
_startPolling();
}
});
......@@ -800,4 +829,14 @@ client.onSignal((id: string) => {
_signal(id).emit();
});
client.onCmdLine((cmd: boolean) => {
_status(cmd ? Status.CMD : Status.ON);
if (cmd)
_startPolling();
else {
if (pending.size === 0)
_stopPolling();
}
});
// --------------------------------------------------------------------------
ivette/src/frama-c/states.ts
View file @ b7ce41a1
......@@ -188,7 +188,7 @@ export function useRequest<In, Out>(
}
});
const signals = options.onSignals ?? rq.signals;
const signals = rq.signals.concat(options.onSignals ?? []);
React.useEffect(() => {
signals.forEach((s) => Server.onSignal(s, trigger));
return () => {
......@@ -304,6 +304,7 @@ class SyncState<A> {
`Fail to set value of SyncState '${this.handler.name}'.`,
`${error}`,
);
this.UPDATE.emit();
}
}
......@@ -311,16 +312,18 @@ class SyncState<A> {
try {
this.upToDate = true;
this.value = undefined;
this.UPDATE.emit();
if (Server.isRunning()) {
const v = await Server.send(this.handler.getter, null);
this.value = v;
this.UPDATE.emit();
}
this.UPDATE.emit();
} catch (error) {
D.error(
`Fail to update SyncState '${this.handler.name}'.`,
`${error}`,
);
this.UPDATE.emit();
}
}
}
......@@ -484,6 +487,7 @@ export function useSyncArray<K, A>(
const st = lookupSyncArray(arr);
React.useEffect(() => st.update(), [st]);
Server.useSignal(arr.signal, st.fetch);
st.update();
useModel(st.model, sync);
return st.model;
}
......@@ -764,11 +768,18 @@ const emptySelection = {
},
};
export type Hovered = Location | undefined;
export const MetaSelection = new Dome.Event<Location>('frama-c-meta-selection');
export const GlobalHovered = new GlobalState<Hovered>(undefined);
export const GlobalSelection = new GlobalState<Selection>(emptySelection);
Server.onShutdown(() => GlobalSelection.setValue(emptySelection));
export function setHovered(h: Hovered) { GlobalHovered.setValue(h); }
export function useHovered(): [Hovered, (h: Hovered) => void] {
return useGlobalState(GlobalHovered);
}
export function setSelection(location: Location, meta = false) {
const s = GlobalSelection.getValue();
GlobalSelection.setValue(reducer(s, { location }));
......@@ -778,7 +789,10 @@ export function setSelection(location: Location, meta = false) {
/** Current selection. */
export function useSelection(): [Selection, (a: SelectionActions) => void] {
const [current, setCurrent] = useGlobalState(GlobalSelection);
return [current, (action) => setCurrent(reducer(current, action))];
const callback = React.useCallback((action) => {
setCurrent(reducer(current, action));
}, [ current, setCurrent ]);
return [current, callback];
}
/** Resets the selected locations. */
......
ivette/src/ivette/index.tsx
View file @ b7ce41a1
......@@ -180,32 +180,6 @@ export function TitleBar(props: TitleBarProps) {
);
}
/* --------------------------------------------------------------------------*/
/* --- Search Hints ---*/
/* --------------------------------------------------------------------------*/
export interface Hint {
id: string;
label: string | JSX.Element;
title?: string;
rank?: number;
onSelection: () => void;
}
/**
Register a hint search engine for the Ivette toolbar.
*/
export function registerHints(
id: string,
lookup: (pattern: string) => Promise<Hint[]>,
) {
const adaptor = (h: Hint): Ext.SearchHint => (
{ ...h, value: () => h.onSelection() }
);
const search = (p: string) => lookup(p).then((hs) => hs.map(adaptor));
Ext.registerHints({ id, search });
}
/* --------------------------------------------------------------------------*/
/* --- Sidebar Panels ---*/
/* --------------------------------------------------------------------------*/
......
ivette/src/renderer/Application.tsx
View file @ b7ce41a1
......@@ -47,10 +47,7 @@ export default function Application(): JSX.Element {
Dome.useFlipSettings('frama-c.sidebar.unfold', true);
const [viewbar, flipViewbar] =
Dome.useFlipSettings('frama-c.viewbar.unfold', true);
const hints = Extensions.useSearchHints();
const onSelectedHints = (): void => {
if (hints.length === 1) Extensions.onSearchHint(hints[0]);
};
return (
<Vfill>
<Toolbar.ToolBar>
......@@ -63,15 +60,9 @@ export default function Application(): JSX.Element {
<Controller.Control />
<Extensions.Toolbar />
<Toolbar.Filler />
<Toolbar.SearchField
placeholder="Search…"
hints={hints}
onSearch={Extensions.searchHints}
onHint={Extensions.onSearchHint}
onSelect={onSelectedHints}
/>
<IvettePrefs.ThemeSwitchTool />
<IvettePrefs.FontTools />
<Toolbar.ModalActionField />
<Toolbar.Button
icon="ITEMS.GRID"
title="Customize Main View"
......
ivette/src/renderer/Controller.tsx
View file @ b7ce41a1
......@@ -160,6 +160,7 @@ export const Control = () => {
play = { enabled: true, onClick: Server.start };
break;
case Server.Status.ON:
case Server.Status.CMD:
case Server.Status.FAILURE:
stop = { enabled: true, onClick: Server.stop };
reload = { enabled: true, onClick: Server.restart };
......@@ -372,36 +373,50 @@ export const Status = () => {
const status = Server.useStatus();
const pending = Server.getPending();
let led: LEDstatus = 'inactive';
let title = undefined;
let icon = undefined;
let running = 'OFF';
let blink = false;
switch (status) {
case Server.Status.OFF:
title = 'Server is off';
break;
case Server.Status.STARTING:
led = 'active';
blink = true;
running = 'BOOT';
title = 'Server is starting';
break;
case Server.Status.ON:
led = pending > 0 ? 'positive' : 'active';
led = 'active';
blink = pending > 0;
running = 'ON';
title = 'Server is running';
break;
case Server.Status.CMD:
led = 'positive';
blink = true;
running = 'CMD';
title = 'Command-line processing';
break;
case Server.Status.HALTING:
led = 'negative';
blink = true;
running = 'HALT';
title = 'Server is halting';
break;
case Server.Status.RESTARTING:
led = 'warning';
blink = true;
running = 'REBOOT';
title = 'Server is restarting';
break;
case Server.Status.FAILURE:
led = 'negative';
blink = true;
running = 'ERR';
title = 'Server halted because of failure';
icon = 'WARNING';
break;
}
......@@ -409,7 +424,7 @@ export const Status = () => {
return (
<>
<LED status={led} blink={blink} />
<Code icon={icon} label={running} />
<Code icon={icon} label={running} title={title} />
<Toolbars.Separator />
</>
);
......
ivette/src/renderer/Extensions.tsx
View file @ b7ce41a1
......@@ -28,84 +28,6 @@
import React from 'react';
import * as Dome from 'dome';
import { Hint } from 'dome/frame/toolbars';
/* --------------------------------------------------------------------------*/
/* --- Search Hints ---*/
/* --------------------------------------------------------------------------*/
export interface HintCallback {
(): void;
}
export interface SearchHint extends Hint<HintCallback> {
rank?: number;
}
function bySearchHint(a: SearchHint, b: SearchHint) {
const ra = a.rank ?? 0;
const rb = b.rank ?? 0;
if (ra < rb) return -1;
if (ra > rb) return +1;
return 0;
}
export interface SearchEngine {
id: string;
search: (pattern: string) => Promise<SearchHint[]>;
}
const NEWHINTS = new Dome.Event('ivette.hints');
const HINTLOOKUP = new Map<string, SearchEngine>();
const HINTS = new Map<string, SearchHint[]>();
let CURRENT = '';
export function updateHints() {
if (CURRENT !== '')
NEWHINTS.emit();
}
export function registerHints(E: SearchEngine) {
HINTLOOKUP.set(E.id, E);
}
export function searchHints(pattern: string) {
if (pattern === '') {
CURRENT = '';
HINTS.clear();
NEWHINTS.emit();
} else {
const REF = pattern;
CURRENT = pattern;
HINTLOOKUP.forEach((E: SearchEngine) => {
E.search(REF).then((hs) => {
if (REF === CURRENT) {
HINTS.set(E.id, hs);
NEWHINTS.emit();
}
}).catch(() => {
if (REF === CURRENT) {
HINTS.delete(E.id);
NEWHINTS.emit();
}
});
});
}
}
export function onSearchHint(h: SearchHint) {
h.value();
}
export function useSearchHints() {
const [hints, setHints] = React.useState<SearchHint[]>([]);
Dome.useEvent(NEWHINTS, () => {
let hs: SearchHint[] = [];
HINTS.forEach((rhs) => { hs = hs.concat(rhs); });
setHints(hs.sort(bySearchHint));
});
return hints;
}
/* --------------------------------------------------------------------------*/
/* --- Extension Elements ---*/
......@@ -133,9 +55,12 @@ function byPanel(p: ElementProps, q: ElementProps) {
export class ElementRack {
private rank = 1;
private readonly items = new Map<string, ElementProps>();
register(elt: ElementProps) {
if (elt.rank === undefined) elt.rank = this.rank;
this.rank++;
this.items.set(elt.id, elt);
UPDATED.emit();
}
......
ivette/yarn.lock
View file @ b7ce41a1
This diff is collapsed.
share/analysis-scripts/build.py
View file @ b7ce41a1
This diff is collapsed.
share/analysis-scripts/detect_recursion.py
View file @ b7ce41a1
#!/usr/bin/env python3
#-*- coding: utf-8 -*-
# -*- coding: utf-8 -*-
##########################################################################
# #
# This file is part of Frama-C. #
......@@ -22,8 +22,8 @@
# #
##########################################################################
# This script finds files containing likely declarations and definitions
# for a given function name, via heuristic syntactic matching.
"""This script finds files containing likely declarations and definitions
for a given function name, via heuristic syntactic matching."""
import sys
import build_callgraph
......
share/analysis-scripts/find_fun.py
View file @ b7ce41a1
This diff is collapsed.
share/analysis-scripts/frama_c_results.py
View file @ b7ce41a1
......@@ -24,31 +24,35 @@ import re
stat_file_re = re.compile("^([^=]*)=(.*)$", re.MULTILINE)
def load(filename):
data = {}
try:
with open(filename, 'r') as file:
with open(filename, "r") as file:
content = file.read()
for (key,value) in stat_file_re.findall(content):
for (key, value) in stat_file_re.findall(content):
data[key] = value
except OSError:
pass
return data
re_escape_space = re.compile(r'\\ ')
re_escape_space = re.compile(r"\\ ")
def convert(data, key, to_type, default=None):
try:
value = data[key].strip()
if to_type is str:
value = re.sub(r'\\ ', ' ', value)
value = re.sub(r'\\,', ',', value)
value = re.sub(r"\\ ", " ", value)
value = re.sub(r"\\,", ",", value)
return value
else:
return to_type(value)
except (ValueError, TypeError, KeyError):
return default
def parse(data):
result = {}
result["timestamp"] = convert(data, "timestamp", str)
......@@ -63,11 +67,12 @@ def parse(data):
result["memory"] = convert(data, "memory", int)
result["cmd_args"] = convert(data, "cmd_args", str)
result["benchmark_tag"] = convert(data, "benchmark_tag", str)
if result["sem_reach_stmt"] != None and result["syn_reach_stmt"] != None:
if result["sem_reach_stmt"] is not None and result["syn_reach_stmt"] is not None:
result["coverage"] = result["sem_reach_stmt"] / result["syn_reach_stmt"]
else:
result["coverage"] = None
return result
def read(filename):
return parse(load(filename))