Skip to content

GitLab

Commit e30f970d authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'master' into feature/dome/code-mirror-ts

parents 807813e7 05d368b5
Expand all Hide whitespace changes
Inline Side-by-side
Changelog
View file @ e30f970d
......@@ -17,6 +17,10 @@
Open Source Release <next-release>
##################################
- Eva [2020-07-27] Improved automatic loop unroll (-eva-auto-loop-unroll
option) on loops with several exit conditions, conditions using
equality operators, temporary variables introduced by the Frama-C
normalization or goto statements.
- Eva [2020-05-29] New builtins for trigonometric functions acos, asin
and atan (and their single-precision version acosf, asinf, atanf).
- Kernel [2020-05-28] Support for C11's _Thread_local storage specifier
......
doc/code/.gitignore
View file @ e30f970d
......@@ -6,6 +6,7 @@
/callgraph_gui/
/constant_propagation/
/counter-examples/
/dive/
/dynamic_plugins/
/e-acsl/
/from/
......
headers/header_spec.txt
View file @ e30f970d
......@@ -768,14 +768,18 @@ src/plugins/dive/build.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/callstack.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/callstack.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/context.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/context.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_graph.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/graph_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/imprecision_graph.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/imprecision_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_range.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_range.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/self.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/self.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/server_interface.ml: CEA_LGPL_OR_PROPRIETARY
......
ivette/api/kernel/ast/index.ts
View file @ e30f970d
......@@ -227,6 +227,33 @@ export const jMarkerSafe: Json.Safe<marker> =
/** Natural order for `marker` */
export const byMarker: Compare.Order<marker> = Compare.structural;
/** Location: function and marker */
export interface location {
/** Function */
function: Json.key<'#fct'>;
/** Marker */
marker: marker;
}
/** Loose decoder for `location` */
export const jLocation: Json.Loose<location> =
Json.jObject({
function: Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
marker: jMarkerSafe,
});
/** Safe decoder for `location` */
export const jLocationSafe: Json.Safe<location> =
Json.jFail(jLocation,'Location expected');
/** Natural order for `location` */
export const byLocation: Compare.Order<location> =
Compare.byFields
<{ function: Json.key<'#fct'>, marker: marker }>({
function: Compare.string,
marker: byMarker,
});
const getFunctions_internal: Server.GetRequest<null,Json.key<'#fct'>[]> = {
kind: Server.RqKind.GET,
name: 'kernel.ast.getFunctions',
......
ivette/api/plugins/dive/index.ts
View file @ e30f970d
......@@ -15,42 +15,296 @@ import * as Server from 'frama-c/server';
//@ts-ignore
import * as State from 'frama-c/states';
//@ts-ignore
import { byLocation } from 'api/kernel/ast';
//@ts-ignore
import { byMarker } from 'api/kernel/ast';
//@ts-ignore
import { jLocation } from 'api/kernel/ast';
//@ts-ignore
import { jLocationSafe } from 'api/kernel/ast';
//@ts-ignore
import { jMarker } from 'api/kernel/ast';
//@ts-ignore
import { jMarkerSafe } from 'api/kernel/ast';
//@ts-ignore
import { location } from 'api/kernel/ast';
//@ts-ignore
import { marker } from 'api/kernel/ast';
/** The name of variable of the program */
export interface variableName {
/** owner function for a local variable */
funName?: string;
/** variable name */
varName: string;
/** Parametrization of the exploration range. */
export interface range {
/** range for the write dependencies */
backward?: number;
/** range for the read dependencies */
forward?: number;
}
/** Loose decoder for `variableName` */
export const jVariableName: Json.Loose<variableName> =
/** Loose decoder for `range` */
export const jRange: Json.Loose<range> =
Json.jObject({ backward: Json.jNumber, forward: Json.jNumber,});
/** Safe decoder for `range` */
export const jRangeSafe: Json.Safe<range> =
Json.jFail(jRange,'Range expected');
/** Natural order for `range` */
export const byRange: Compare.Order<range> =
Compare.byFields
<{ backward?: number, forward?: number }>({
backward: Compare.defined(Compare.number),
forward: Compare.defined(Compare.number),
});
/** Global parametrization of the exploration. */
export interface explorationWindow {
/** how far dive will explore from root nodes ; must be a finite range */
perception: range;
/** range beyond which the nodes must be hidden */
horizon: range;
}
/** Loose decoder for `explorationWindow` */
export const jExplorationWindow: Json.Loose<explorationWindow> =
Json.jObject({ perception: jRangeSafe, horizon: jRangeSafe,});
/** Safe decoder for `explorationWindow` */
export const jExplorationWindowSafe: Json.Safe<explorationWindow> =
Json.jFail(jExplorationWindow,'ExplorationWindow expected');
/** Natural order for `explorationWindow` */
export const byExplorationWindow: Compare.Order<explorationWindow> =
Compare.byFields
<{ perception: range, horizon: range }>({
perception: byRange,
horizon: byRange,
});
/** A node identifier in the graph */
export type nodeId = number;
/** Loose decoder for `nodeId` */
export const jNodeId: Json.Loose<nodeId> = Json.jNumber;
/** Safe decoder for `nodeId` */
export const jNodeIdSafe: Json.Safe<nodeId> =
Json.jFail(Json.jNumber,'Number expected');
/** Natural order for `nodeId` */
export const byNodeId: Compare.Order<nodeId> = Compare.number;
/** A callsite */
export type callsite = { fun: string, instr: number | string };
/** Loose decoder for `callsite` */
export const jCallsite: Json.Loose<callsite> =
Json.jObject({
fun: Json.jFail(Json.jString,'String expected'),
instr: Json.jFail(
Json.jUnion<number | string>( Json.jNumber, Json.jString,),
'Union expected'),
});
/** Safe decoder for `callsite` */
export const jCallsiteSafe: Json.Safe<callsite> =
Json.jFail(jCallsite,'Callsite expected');
/** Natural order for `callsite` */
export const byCallsite: Compare.Order<callsite> =
Compare.byFields
<{ fun: string, instr: number | string }>({
fun: Compare.string,
instr: Compare.structural,
});
/** The callstack context for a node */
export type callstack = callsite[];
/** Safe decoder for `callstack` */
export const jCallstackSafe: Json.Safe<callstack> =
Json.jArray(jCallsiteSafe);
/** Loose decoder for `callstack` */
export const jCallstack: Json.Loose<callstack> = Json.jTry(jCallstackSafe);
/** Natural order for `callstack` */
export const byCallstack: Compare.Order<callstack> =
Compare.array(byCallsite);
/** The description of a node locality */
export type nodeLocality = { file: string, callstack?: callstack };
/** Loose decoder for `nodeLocality` */
export const jNodeLocality: Json.Loose<nodeLocality> =
Json.jObject({
funName: Json.jString,
varName: Json.jFail(Json.jString,'String expected'),
file: Json.jFail(Json.jString,'String expected'),
callstack: jCallstack,
});
/** Safe decoder for `variableName` */
export const jVariableNameSafe: Json.Safe<variableName> =
Json.jFail(jVariableName,'VariableName expected');
/** Safe decoder for `nodeLocality` */
export const jNodeLocalitySafe: Json.Safe<nodeLocality> =
Json.jFail(jNodeLocality,'NodeLocality expected');
/** Natural order for `variableName` */
export const byVariableName: Compare.Order<variableName> =
/** Natural order for `nodeLocality` */
export const byNodeLocality: Compare.Order<nodeLocality> =
Compare.byFields
<{ funName?: string, varName: string }>({
funName: Compare.defined(Compare.alpha),
varName: Compare.alpha,
<{ file: string, callstack?: callstack }>({
file: Compare.string,
callstack: Compare.defined(byCallstack),
});
const graph_internal: Server.GetRequest<null,Json.json> = {
/** A graph node */
export type node =
{ id: nodeId, label: string, kind: string, locality: nodeLocality,
is_root: boolean, backward_explored: string, forward_explored: string,
writes: location[], values?: string, range: number | string,
type?: string };
/** Loose decoder for `node` */
export const jNode: Json.Loose<node> =
Json.jObject({
id: jNodeIdSafe,
label: Json.jFail(Json.jString,'String expected'),
kind: Json.jFail(Json.jString,'String expected'),
locality: jNodeLocalitySafe,
is_root: Json.jFail(Json.jBoolean,'Boolean expected'),
backward_explored: Json.jFail(Json.jString,'String expected'),
forward_explored: Json.jFail(Json.jString,'String expected'),
writes: Json.jArray(jLocationSafe),
values: Json.jString,
range: Json.jFail(
Json.jUnion<number | string>( Json.jNumber, Json.jString,),
'Union expected'),
type: Json.jString,
});
/** Safe decoder for `node` */
export const jNodeSafe: Json.Safe<node> = Json.jFail(jNode,'Node expected');
/** Natural order for `node` */
export const byNode: Compare.Order<node> =
Compare.byFields
<{ id: nodeId, label: string, kind: string, locality: nodeLocality,
is_root: boolean, backward_explored: string, forward_explored: string,
writes: location[], values?: string, range: number | string,
type?: string }>({
id: byNodeId,
label: Compare.string,
kind: Compare.string,
locality: byNodeLocality,
is_root: Compare.boolean,
backward_explored: Compare.string,
forward_explored: Compare.string,
writes: Compare.array(byLocation),
values: Compare.defined(Compare.string),
range: Compare.structural,
type: Compare.defined(Compare.string),
});
/** The dependency between two nodes */
export type dependency =
{ id: number, src: nodeId, dst: nodeId, kind: string, origins: location[] };
/** Loose decoder for `dependency` */
export const jDependency: Json.Loose<dependency> =
Json.jObject({
id: Json.jFail(Json.jNumber,'Number expected'),
src: jNodeIdSafe,
dst: jNodeIdSafe,
kind: Json.jFail(Json.jString,'String expected'),
origins: Json.jArray(jLocationSafe),
});
/** Safe decoder for `dependency` */
export const jDependencySafe: Json.Safe<dependency> =
Json.jFail(jDependency,'Dependency expected');
/** Natural order for `dependency` */
export const byDependency: Compare.Order<dependency> =
Compare.byFields
<{ id: number, src: nodeId, dst: nodeId, kind: string,
origins: location[] }>({
id: Compare.number,
src: byNodeId,
dst: byNodeId,
kind: Compare.string,
origins: Compare.array(byLocation),
});
/** The whole graph being built */
export type graphData = { nodes: node[], deps: dependency[] };
/** Loose decoder for `graphData` */
export const jGraphData: Json.Loose<graphData> =
Json.jObject({
nodes: Json.jArray(jNodeSafe),
deps: Json.jArray(jDependencySafe),
});
/** Safe decoder for `graphData` */
export const jGraphDataSafe: Json.Safe<graphData> =
Json.jFail(jGraphData,'GraphData expected');
/** Natural order for `graphData` */
export const byGraphData: Compare.Order<graphData> =
Compare.byFields
<{ nodes: node[], deps: dependency[] }>({
nodes: Compare.array(byNode),
deps: Compare.array(byDependency),
});
/** Graph differences from the last action. */
export type diffData =
{ root?: nodeId, add: { nodes: node[], deps: dependency[] }, sub: nodeId[]
};
/** Loose decoder for `diffData` */
export const jDiffData: Json.Loose<diffData> =
Json.jObject({
root: jNodeId,
add: Json.jFail(
Json.jObject({
nodes: Json.jArray(jNodeSafe),
deps: Json.jArray(jDependencySafe),
}),'Record expected'),
sub: Json.jArray(jNodeIdSafe),
});
/** Safe decoder for `diffData` */
export const jDiffDataSafe: Json.Safe<diffData> =
Json.jFail(jDiffData,'DiffData expected');
/** Natural order for `diffData` */
export const byDiffData: Compare.Order<diffData> =
Compare.byFields
<{ root?: nodeId, add: { nodes: node[], deps: dependency[] },
sub: nodeId[] }>({
root: Compare.defined(byNodeId),
add: Compare.byFields
<{ nodes: node[], deps: dependency[] }>({
nodes: Compare.array(byNode),
deps: Compare.array(byDependency),
}),
sub: Compare.array(byNodeId),
});
const window_internal: Server.SetRequest<explorationWindow,null> = {
kind: Server.RqKind.SET,
name: 'plugins.dive.window',
input: jExplorationWindow,
output: Json.jNull,
};
/** Set the exploration window */
export const window: Server.SetRequest<explorationWindow,null>= window_internal;
const graph_internal: Server.GetRequest<null,graphData> = {
kind: Server.RqKind.GET,
name: 'plugins.dive.graph',
input: Json.jNull,
output: Json.jAny,
output: jGraphData,
};
/** Retrieve the whole graph */
export const graph: Server.GetRequest<null,Json.json>= graph_internal;
export const graph: Server.GetRequest<null,graphData>= graph_internal;
const clear_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
......@@ -61,58 +315,40 @@ const clear_internal: Server.ExecRequest<null,null> = {
/** Erase the graph and start over with an empty one */
export const clear: Server.ExecRequest<null,null>= clear_internal;
const addVar_internal: Server.ExecRequest<variableName,Json.json> = {
const add_internal: Server.ExecRequest<marker,diffData> = {
kind: Server.RqKind.EXEC,
name: 'plugins.dive.addVar',
input: jVariableName,
output: Json.jAny,
name: 'plugins.dive.add',
input: jMarker,
output: jDiffData,
};
/** Add a variable to the graph */
export const addVar: Server.ExecRequest<variableName,Json.json>= addVar_internal;
/** Add a node to the graph */
export const add: Server.ExecRequest<marker,diffData>= add_internal;
const addFunctionAlarms_internal: Server.ExecRequest<
Json.key<'#fct'>,
Json.json
> = {
kind: Server.RqKind.EXEC,
name: 'plugins.dive.addFunctionAlarms',
input: Json.jKey<'#fct'>('#fct'),
output: Json.jAny,
};
/** Add all alarms of the given function */
export const addFunctionAlarms: Server.ExecRequest<
Json.key<'#fct'>,
Json.json
>= addFunctionAlarms_internal;
const explore_internal: Server.ExecRequest<
Json.index<'#dive-node'>,
Json.json
> = {
const explore_internal: Server.ExecRequest<nodeId,diffData> = {
kind: Server.RqKind.EXEC,
name: 'plugins.dive.explore',
input: Json.jIndex<'#dive-node'>('#dive-node'),
output: Json.jAny,
input: jNodeId,
output: jDiffData,
};
/** Explore the graph starting from an existing vertex */
export const explore: Server.ExecRequest<Json.index<'#dive-node'>,Json.json>= explore_internal;
export const explore: Server.ExecRequest<nodeId,diffData>= explore_internal;
const show_internal: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
const show_internal: Server.ExecRequest<nodeId,diffData> = {
kind: Server.RqKind.EXEC,
name: 'plugins.dive.show',
input: Json.jIndex<'#dive-node'>('#dive-node'),
output: Json.jAny,
input: jNodeId,
output: jDiffData,
};
/** Show the dependencies of an existing vertex */
export const show: Server.ExecRequest<Json.index<'#dive-node'>,Json.json>= show_internal;
export const show: Server.ExecRequest<nodeId,diffData>= show_internal;
const hide_internal: Server.ExecRequest<Json.index<'#dive-node'>,Json.json> = {
const hide_internal: Server.ExecRequest<nodeId,diffData> = {
kind: Server.RqKind.EXEC,
name: 'plugins.dive.hide',
input: Json.jIndex<'#dive-node'>('#dive-node'),
output: Json.jAny,
input: jNodeId,
output: jDiffData,
};
/** Hide the dependencies of an existing vertex */
export const hide: Server.ExecRequest<Json.index<'#dive-node'>,Json.json>= hide_internal;
export const hide: Server.ExecRequest<nodeId,diffData>= hide_internal;
/* ------------------------------------- */
ivette/api/server_tsc.ml
View file @ e30f970d
......@@ -167,7 +167,7 @@ let rec makeDecoder ~safe ?self ~names fmt js =
| Jboolean -> jsafe ~safe "Boolean" jprim fmt "jBoolean"
| Jnumber -> jsafe ~safe "Number" jprim fmt "jNumber"
| Jstring | Jalpha -> jsafe ~safe "String" jprim fmt "jString"
| Jtag a -> Format.fprintf fmt "jTag(\"%s\")" a
| Jtag a -> Format.fprintf fmt "Json.jTag(\"%s\")" a
| Jkey kd -> jsafe ~safe ("#" ^ kd) jkey fmt kd
| Jindex kd -> jsafe ~safe ("#" ^ kd) jindex fmt kd
| Jdata id -> jcall names fmt (Pkg.Derived.decode ~safe id)
......@@ -188,6 +188,10 @@ let rec makeDecoder ~safe ?self ~names fmt js =
| Jrecord jfs -> jsafe ~safe "Record" (jrecord ~makeSafe) fmt jfs
| Jtuple jts -> jtry ~safe (jtuple ~makeSafe) fmt jts
let makeLooseNeedSafe = function
| Pkg.Jtuple _ | Pkg.Jarray _ -> true
| _ -> false
let makeRootDecoder ~safe ~self ~names fmt js =
let open Pkg in
match js with
......@@ -414,12 +418,13 @@ let makeDeclaration fmt names d =
type ranking = {
mutable rank : int ;
mutable mark : int Pkg.IdMap.t ;
index : Pkg.declInfo Pkg.IdMap.t ;
}
let depends d =
match d.Pkg.d_kind with
| D_loose(id,(Jtuple _ | Jarray _)) -> [Pkg.Derived.safe id]
| D_safe(id,_) -> [Pkg.Derived.loose id]
| D_loose(id,t) when makeLooseNeedSafe t -> [Pkg.Derived.safe id]
| D_safe(id,t) when not (makeLooseNeedSafe t) -> [Pkg.Derived.loose id]
| D_array _ ->
let id = d.d_ident in
let data = Pkg.Derived.data id in
......@@ -439,13 +444,20 @@ let next m id =
m.mark <- Pkg.IdMap.add id r m.mark ;
m.rank <- succ r
let mark m d =
let rec mark m d =
let id = d.Pkg.d_ident in
if not (Pkg.IdMap.mem id m.mark) then
( List.iter (next m) (depends d) ; next m id )
( List.iter (mark_id m) (depends d) ; next m id )
and mark_id m id =
try mark m (Pkg.IdMap.find id m.index)
with Not_found -> ()
let ranking ds =
let m = { rank = 0 ; mark = Pkg.IdMap.empty } in
let index = List.fold_left
(fun m d -> Pkg.IdMap.add d.Pkg.d_ident d m)
Pkg.IdMap.empty ds in
let m = { rank = 0 ; mark = Pkg.IdMap.empty ; index } in
List.iter (mark m) ds ;
let rk = m.mark in
let getRank a = try Pkg.IdMap.find a.Pkg.d_ident rk with Not_found -> 0 in
......
ivette/package.json
View file @ e30f970d
......@@ -22,6 +22,7 @@
"@babel/preset-typescript": "^7.9.0",
"@hot-loader/react-dom": "^16.13.0",
"@types/codemirror": "^0.0.97",
"@types/cytoscape": "^3.14.5",
"@types/lodash": "^4.14.149",
"@types/node": "12.12.21",
"@types/react": "^16.9.17",
......@@ -53,15 +54,25 @@
},
"dependencies": {
"@babel/runtime": "^7.9.2",
"@fortawesome/fontawesome-free": "^5.13.1",
"codemirror": "^5.52.2",
"cytoscape": "^3.15.1",
"cytoscape-cola": "^2.3.1",
"cytoscape-cose-bilkent": "^4.1.0",
"cytoscape-cxtmenu": "^3.1.2",
"cytoscape-dagre": "^2.2.2",
"cytoscape-klay": "^3.1.3",
"cytoscape-popper": "^1.0.7",
"immutable": "^4.0.0-rc.12",
"lodash": "^4.17.15",
"react": "^16.8",
"react-cytoscapejs": "^1.2.1",
"react-dom": "^16.13.1",
"react-draggable": "^4.2.0",
"react-fast-compare": "^3.2.0",
"react-virtualized": "^9.21.2",
"source-map-support": "^0.5.16",
"tippy.js": "5.2.1",
"zeromq": "^6.0.0-beta.5"
}
}
ivette/src/dome/src/renderer/data/json.ts
View file @ e30f970d
......@@ -188,7 +188,7 @@ export function jCatch<A>(fn: Loose<A>, fallBack: A): Safe<A> {
try {
return fn(js) ?? fallBack;
} catch (err) {
if (DEVEL) console.error('[Dome.json]', err);
if (DEVEL) console.warn('[Dome.json]', err);
return fallBack;
}
};
......@@ -202,7 +202,8 @@ export function jTry<A>(fn: Loose<A>, defaultValue?: A): Loose<A> {
return (js: json) => {
try {
return fn(js) ?? defaultValue;
} catch (_err) {
} catch (err) {
if (DEVEL) console.warn('[Dome.json]', err);
return defaultValue;
}
};
......