diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 18b91267bf15ef43f86ba5fe2c7b046b07162595..b4c1ddf551edc3130030aba5718106e5d2160da4 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1211,6 +1211,8 @@ src/plugins/studia/reads.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/reads.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/studia_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/studia_gui.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/studia/studia_request.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/studia/studia_request.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/Studia.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/writes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/writes.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/ivette/api/generated/kernel/ast/index.ts b/ivette/api/generated/kernel/ast/index.ts
index dc1398e2ab95606276eb5ab92a4475f1ffbe3299..eaaf033326b4ba7835ba5f16fc80c302180a1fee 100644
--- a/ivette/api/generated/kernel/ast/index.ts
+++ b/ivette/api/generated/kernel/ast/index.ts
@@ -31,6 +31,14 @@ import { jTextSafe } from 'frama-c/api/kernel/data';
import { tag } from 'frama-c/api/kernel/data';
//@ts-ignore
import { text } from 'frama-c/api/kernel/data';
+//@ts-ignore
+import { bySource } from 'frama-c/api/kernel/services';
+//@ts-ignore
+import { jSource } from 'frama-c/api/kernel/services';
+//@ts-ignore
+import { jSourceSafe } from 'frama-c/api/kernel/services';
+//@ts-ignore
+import { source } from 'frama-c/api/kernel/services';
const compute_internal: Server.ExecRequest<null,null> = {
kind: Server.RqKind.EXEC,
@@ -121,6 +129,8 @@ export interface markerInfoData {
name: string;
/** Marker declaration or description */
descr: string;
+ /** Marker position */
+ position: source;
}
/** Loose decoder for `markerInfoData` */
@@ -132,6 +142,7 @@ export const jMarkerInfoData: Json.Loose<markerInfoData> =
var: jMarkerVarSafe,
name: Json.jFail(Json.jString,'String expected'),
descr: Json.jFail(Json.jString,'String expected'),
+ position: jSourceSafe,
});
/** Safe decoder for `markerInfoData` */
@@ -142,12 +153,13 @@ export const jMarkerInfoDataSafe: Json.Safe<markerInfoData> =
export const byMarkerInfoData: Compare.Order<markerInfoData> =
Compare.byFields
<{ key: Json.key<'#markerInfo'>, kind: markerKind, var: markerVar,
- name: string, descr: string }>({
+ name: string, descr: string, position: source }>({
key: Compare.string,
kind: byMarkerKind,
var: byMarkerVar,
name: Compare.alpha,
descr: Compare.string,
+ position: bySource,
});
/** Signal for array [`markerInfo`](#markerinfo) */
diff --git a/ivette/api/generated/plugins/studia/studia/index.ts b/ivette/api/generated/plugins/studia/studia/index.ts
new file mode 100644
index 0000000000000000000000000000000000000000..003c89fe0638336421928fcdbade1fd3b06b209d
--- /dev/null
+++ b/ivette/api/generated/plugins/studia/studia/index.ts
@@ -0,0 +1,83 @@
+/* --- Generated Frama-C Server API --- */
+
+/**
+ Studia
+ @packageDocumentation
+ @module frama-c/api/plugins/studia/studia
+*/
+
+//@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 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jMarker } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { jMarkerSafe } from 'frama-c/api/kernel/ast';
+//@ts-ignore
+import { marker } from 'frama-c/api/kernel/ast';
+
+/** Statements that read or write a location. */
+export interface effects {
+ /** List of statements with direct effect. */
+ direct: [ Json.key<'#fct'>, marker ][];
+ /** List of statements with indirect effect. */
+ indirect: [ Json.key<'#fct'>, marker ][];
+}
+
+/** Loose decoder for `effects` */
+export const jEffects: Json.Loose<effects> =
+ Json.jObject({
+ direct: Json.jList(
+ Json.jTry(
+ Json.jPair(
+ Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
+ jMarkerSafe,
+ ))),
+ indirect: Json.jList(
+ Json.jTry(
+ Json.jPair(
+ Json.jFail(Json.jKey<'#fct'>('#fct'),'#fct expected'),
+ jMarkerSafe,
+ ))),
+ });
+
+/** Safe decoder for `effects` */
+export const jEffectsSafe: Json.Safe<effects> =
+ Json.jFail(jEffects,'Effects expected');
+
+/** Natural order for `effects` */
+export const byEffects: Compare.Order<effects> =
+ Compare.byFields
+ <{ direct: [ Json.key<'#fct'>, marker ][],
+ indirect: [ Json.key<'#fct'>, marker ][] }>({
+ direct: Compare.array(Compare.pair(Compare.string,byMarker,)),
+ indirect: Compare.array(Compare.pair(Compare.string,byMarker,)),
+ });
+
+const getReadsLval_internal: Server.GetRequest<Json.key<'#lval'>,effects> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.studia.studia.getReadsLval',
+ input: Json.jKey<'#lval'>('#lval'),
+ output: jEffects,
+};
+/** Get the list of statements that read a lval. */
+export const getReadsLval: Server.GetRequest<Json.key<'#lval'>,effects>= getReadsLval_internal;
+
+const getWritesLval_internal: Server.GetRequest<Json.key<'#lval'>,effects> = {
+ kind: Server.RqKind.GET,
+ name: 'plugins.studia.studia.getWritesLval',
+ input: Json.jKey<'#lval'>('#lval'),
+ output: jEffects,
+};
+/** Get the list of statements that write a lval. */
+export const getWritesLval: Server.GetRequest<Json.key<'#lval'>,effects>= getWritesLval_internal;
+
+/* ------------------------------------- */
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index d44bfe0e1314b7bbb8dd14aa30a6204158a16357..3895ee4978f75af68bed38a3677e579510941174 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -479,6 +479,10 @@ export type HistorySelectActions = 'HISTORY_PREV' | 'HISTORY_NEXT';
/** A selection of multiple locations. */
export interface MultipleSelection {
+ /** Name of the multiple selection. */
+ name: string;
+ /** Explanatory description of the multiple selection. */
+ title: string;
/** The index of the current selected location in [[allSelections]]. */
index: number;
/** All locations forming a multiple selection. */
@@ -487,6 +491,8 @@ export interface MultipleSelection {
/** A select action on multiple locations. */
export interface MultipleSelect {
+ readonly name: string;
+ readonly title: string;
readonly index: number;
readonly locations: Location[];
}
@@ -625,6 +631,8 @@ function fromMultipleSelections(
return {
...s,
multiple: {
+ name: '',
+ title: '',
index: 0,
allSelections: [],
},
@@ -640,13 +648,15 @@ function reducer(s: Selection, action: SelectionActions): Selection {
return selectLocation(s, action.location);
}
if (isMultipleSelect(action)) {
- if (action.locations.length === 0)
- return s;
const index = action.index > 0 ? action.index : 0;
- const selection = selectLocation(s, action.locations[index]);
+ const selection =
+ action.locations.length === 0 ? s :
+ selectLocation(s, action.locations[index]);
return {
...selection,
multiple: {
+ name: action.name,
+ title: action.title,
allSelections: action.locations,
index,
},
@@ -684,6 +694,8 @@ const emptySelection = {
nextSelections: [],
},
multiple: {
+ name: '',
+ title: '',
index: 0,
allSelections: [],
},
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index 44fde3657cf205c47dcd9a2a659356d9b25d0d60..4f50844ba06148864328be399f9ee4716de12cea 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -15,8 +15,10 @@ import { RichTextBuffer } from 'dome/text/buffers';
import { Text } from 'dome/text/editors';
import { IconButton } from 'dome/controls/buttons';
import { Component, TitleBar } from 'frama-c/LabViews';
-import { printFunction, markerInfo } from 'frama-c/api/kernel/ast';
+import { printFunction, markerInfo, markerInfoData }
+ from 'frama-c/api/kernel/ast';
import { getCallers, getDeadCode } from 'frama-c/api/plugins/eva/general';
+import { getWritesLval, getReadsLval } from 'frama-c/api/plugins/studia/studia';
import 'codemirror/mode/clike/clike';
import 'codemirror/theme/ambiance.css';
@@ -79,6 +81,24 @@ async function functionCallers(functionName: string) {
}
}
+type access = 'Reads' | 'Writes';
+
+async function studia(marker: string, info: markerInfoData, kind: access) {
+ const request = kind === 'Reads' ? getReadsLval : getWritesLval;
+ const data = await Server.send(request, marker);
+ const locations = data.direct.map(([f, m]) => ({ function: f, marker: m }));
+ const lval = info.name;
+ if (locations.length > 0) {
+ const name = `${kind} of ${lval}`;
+ const title = `List of statements ${
+ (kind === 'Reads') ? 'accessing' : 'modifying'
+ } the memory location pointed by ${lval}.`;
+ return { name, title, locations, index: 0 };
+ }
+ const name = `No ${kind.toLowerCase()} of ${lval}`;
+ return { name, title: '', locations: [], index: 0 };
+}
+
// --------------------------------------------------------------------------
// --- AST Printer
// --------------------------------------------------------------------------
@@ -143,8 +163,9 @@ const ASTview = () => {
const selectedMarkerInfo = markersInfo.getData(markerId);
if (selectedMarkerInfo?.var === 'function') {
if (selectedMarkerInfo.kind === 'declaration') {
- if (selectedMarkerInfo?.name) {
- const locations = await functionCallers(selectedMarkerInfo.name);
+ const name = selectedMarkerInfo?.name;
+ if (name) {
+ const locations = await functionCallers(name);
const locationsByFunction = _.groupBy(locations, (e) => e.function);
_.forEach(locationsByFunction,
(e) => {
@@ -154,6 +175,7 @@ const ASTview = () => {
`Go to caller ${callerName} ` +
`${e.length > 1 ? `(${e.length} call sites)` : ''}`,
onClick: () => updateSelection({
+ name: `Call sites of function ${name}`,
locations,
index: locations.findIndex((l) => l.function === callerName),
}),
@@ -170,6 +192,22 @@ const ASTview = () => {
});
}
}
+ const enabled = selectedMarkerInfo?.kind === 'lvalue'
+ || selectedMarkerInfo?.var === 'variable';
+ function onClick(kind: access) {
+ if (selectedMarkerInfo)
+ studia(markerId, selectedMarkerInfo, kind).then(updateSelection);
+ }
+ items.push({
+ label: 'Studia: select writes',
+ enabled,
+ onClick: () => onClick('Writes'),
+ });
+ items.push({
+ label: 'Studia: select reads',
+ enabled,
+ onClick: () => onClick('Reads'),
+ });
if (items.length > 0)
Dome.popupMenu(items);
}
diff --git a/ivette/src/renderer/Locations.tsx b/ivette/src/renderer/Locations.tsx
index 3008d8d9cd2e83bd70089181f168d8f98578d9a2..2e61bdd697411a6b6f018ab1083c1e2e0b2b1cd0 100644
--- a/ivette/src/renderer/Locations.tsx
+++ b/ivette/src/renderer/Locations.tsx
@@ -5,12 +5,14 @@
import React from 'react';
import * as States from 'frama-c/states';
+import * as Json from 'dome/data/json';
import { CompactModel } from 'dome/table/arrays';
-import { Table, Column } from 'dome/table/views';
+import { Table, Column, Renderer } from 'dome/table/views';
import { Label } from 'dome/controls/labels';
import { IconButton } from 'dome/controls/buttons';
import { Space } from 'dome/frame/toolbars';
import { Component, TitleBar } from 'frama-c/LabViews';
+import { markerInfo } from 'frama-c/api/kernel/ast';
// --------------------------------------------------------------------------
// --- Locations Panel
@@ -27,6 +29,17 @@ const LocationsTable = () => {
), []);
const multipleSelections = selection?.multiple;
const numberOfSelections = multipleSelections?.allSelections?.length;
+ const markersInfo = States.useSyncArray(markerInfo);
+
+ // Renderer for statement markers.
+ const renderMarker: Renderer<string> =
+ (loc: string) => {
+ const markerId = (loc as Json.key<'#markerInfo'>);
+ const info = markersInfo.getData(markerId);
+ const source = info?.position;
+ const position = `${source?.base}:${source?.line}`;
+ return <Label label={position} title={info?.descr} />;
+ };
// Updates [[model]] with the current multiple selections.
React.useEffect(() => {
@@ -94,6 +107,11 @@ const LocationsTable = () => {
title={`Clear location${numberOfSelections > 1 ? 's' : ''}`}
/>
</TitleBar>
+ <Label
+ label={multipleSelections?.name}
+ title={multipleSelections?.title}
+ style={{ textAlign: 'center' }}
+ />
<Table
model={model}
selection={multipleSelections?.index}
@@ -107,7 +125,12 @@ const LocationsTable = () => {
getter={(r: { id: number }) => r.id + 1}
/>
<Column id="function" label="Function" width={120} />
- <Column id="marker" label="Marker" fill />
+ <Column
+ id="marker"
+ label="Statement"
+ fill
+ render={renderMarker}
+ />
</Table>
</>
);
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index 8d8d6f6c87f5a2e8f075865c0889cb7a5f5ea2f5..bd1fa410041bf8bac9a1852b9e87e0eefba3ec6a 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -76,9 +76,7 @@ let pretty fmt = function
| PExp (_, _, expr) -> Printer.pp_exp fmt expr
| PTermLval (_, _, _, lv) -> Printer.pp_term_lval fmt lv
| PIP prop -> Description.pp_property fmt prop
- | PStmt(_,stmt) | PStmtStart (_, stmt) ->
- let p = fst @@ Cil_datatype.Stmt.loc stmt in
- Format.fprintf fmt "Statement at %a" Filepath.pp_pos p
+ | PStmt(_,stmt) | PStmtStart (_, stmt) -> Printer.pp_stmt fmt stmt
| PGlobal g -> Printer.pp_global fmt (decl_of g)
let pp_ki_loc fmt ki =
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 6dd76c134789afb91c5d3db8ef6eb3213da42721..a3fe97c94e4ac970d3f3c228715d63eee5af6714 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -194,6 +194,14 @@ struct
~get:(fun (tag, _) -> Rich_text.to_string Printer_tag.pretty tag)
model
in
+ let () =
+ States.column
+ ~name:"position"
+ ~descr:(Md.plain "Marker position")
+ ~data:(module Kernel_main.LogSource)
+ ~get:(fun (tag, _) -> fst (Printer_tag.loc_of_localizable tag))
+ model
+ in
States.register_array
~package
~name:"markerInfo"
@@ -254,6 +262,25 @@ module Printer = Printer_tag.Make(Marker)
(* --- Ast Data --- *)
(* -------------------------------------------------------------------------- *)
+module Lval =
+struct
+ type t = kinstr * lval
+ let jtype = Marker.jlval
+ let to_json (kinstr, lval) =
+ let kf = match kinstr with
+ | Kglobal -> None
+ | Kstmt stmt -> Some (Kernel_function.find_englobing_kf stmt)
+ in
+ Marker.to_json (PLval (kf, kinstr, lval))
+ let of_json js =
+ let open Printer_tag in
+ match Marker.of_json js with
+ | PLval (_, kinstr, lval) -> kinstr, lval
+ | PVDecl (_, kinstr, vi) -> kinstr, Cil.var vi
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)) -> Kglobal, Cil.var vi
+ | _ -> Data.failure "not a lval marker"
+end
+
module Stmt =
struct
type t = stmt
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
index 6832e10f4ed79ccfd685b8bd8f966de80c09bd63..f9e56c08f27a90fa306f789c5453704a690176c5 100644
--- a/src/plugins/server/kernel_ast.mli
+++ b/src/plugins/server/kernel_ast.mli
@@ -30,6 +30,7 @@ open Cil_types
module Kf : Data.S with type t = kernel_function
module Ki : Data.S with type t = kinstr
module Stmt : Data.S with type t = stmt
+module Lval : Data.S with type t = kinstr * lval
module Marker :
sig
diff --git a/src/plugins/studia/Makefile.in b/src/plugins/studia/Makefile.in
index 76fa49dac96432f94679700c99e724905b665c85..c49e1893f2ea65bb13148d6189f58c7b667a2de0 100644
--- a/src/plugins/studia/Makefile.in
+++ b/src/plugins/studia/Makefile.in
@@ -36,7 +36,7 @@ endif
PLUGIN_DIR ?=.
PLUGIN_ENABLE:=@ENABLE_STUDIA@
PLUGIN_NAME:=Studia
-PLUGIN_CMO:= options writes reads
+PLUGIN_CMO:= options writes reads studia_request
PLUGIN_GUI_CMO:= studia_gui
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
diff --git a/src/plugins/studia/studia_request.ml b/src/plugins/studia/studia_request.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0297777d9b0147d901414f4702bc43368b01fef8
--- /dev/null
+++ b/src/plugins/studia/studia_request.ml
@@ -0,0 +1,98 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Server
+open Cil_types
+
+let package =
+ Package.package ~plugin:"studia" ~name:"studia" ~title:"Studia"
+ ~readme:"studia.md" ()
+
+type effects =
+ { direct: stmt list;
+ indirect: stmt list; }
+
+module Effects = struct
+ open Server.Data
+
+ type record
+ let record: record Record.signature = Record.signature ()
+
+ module Location = Data.Jpair (Kernel_ast.Kf) (Kernel_ast.Marker)
+
+ let direct = Record.field record ~name:"direct"
+ ~descr:(Markdown.plain "List of statements with direct effect.")
+ (module Data.Jlist (Location))
+ let indirect = Record.field record ~name:"indirect"
+ ~descr:(Markdown.plain "List of statements with indirect effect.")
+ (module Data.Jlist (Location))
+
+ let data = Record.publish record ~package ~name:"effects"
+ ~descr:(Markdown.plain "Statements that read or write a location.")
+
+ module R : Record.S with type r = record = (val data)
+ type t = effects
+ let jtype = R.jtype
+
+ let to_json effects =
+ let output_stmt stmt =
+ let kf = Kernel_function.find_englobing_kf stmt in
+ kf, Printer_tag.PStmtStart (kf, stmt)
+ in
+ R.default |>
+ R.set direct (List.map output_stmt effects.direct) |>
+ R.set indirect (List.map output_stmt effects.indirect) |>
+ R.to_json
+end
+
+
+type kind = Reads | Writes
+
+let compute kind zone =
+ let stmts = match kind with
+ | Reads -> Reads.compute zone
+ | Writes -> Writes.compute zone
+ in
+ let add_if b stmt acc = if b then stmt :: acc else acc in
+ let add acc (stmt, e) =
+ let direct = add_if e.Writes.direct stmt acc.direct in
+ let indirect = add_if e.Writes.indirect stmt acc.indirect in
+ { direct; indirect }
+ in
+ let empty = { direct = []; indirect = []; } in
+ List.fold_left add empty stmts
+
+let lval_location kinstr lval = !Db.Value.lval_to_zone kinstr lval
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getReadsLval"
+ ~descr:(Markdown.plain "Get the list of statements that read a lval.")
+ ~input:(module Kernel_ast.Lval)
+ ~output:(module Effects)
+ (fun (kinstr, lval) -> compute Reads (lval_location kinstr lval))
+
+let () = Request.register ~package
+ ~kind:`GET ~name:"getWritesLval"
+ ~descr:(Markdown.plain "Get the list of statements that write a lval.")
+ ~input:(module Kernel_ast.Lval)
+ ~output:(module Effects)
+ (fun (kinstr, lval) -> compute Writes (lval_location kinstr lval))
diff --git a/src/plugins/studia/studia_request.mli b/src/plugins/studia/studia_request.mli
new file mode 100644
index 0000000000000000000000000000000000000000..182bc40a8e1af00f6d1329952d449d0f2e6808e1
--- /dev/null
+++ b/src/plugins/studia/studia_request.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* 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). *)
+(* *)
+(**************************************************************************)