diff --git a/ivette/src/dome/src/renderer/text/buffers.js b/ivette/src/dome/src/renderer/text/buffers.js
index 30c272d3f99a511b7d3b98b31320ac37bd418b8d..0c0265b78498c432757390e73638c8db3a2c3cbc 100644
--- a/ivette/src/dome/src/renderer/text/buffers.js
+++ b/ivette/src/dome/src/renderer/text/buffers.js
@@ -540,6 +540,37 @@ is blocked.
.finally(endOperation);
}
+ // --------------------------------------------------------------------------
+ // --- Print Utilities
+ // --------------------------------------------------------------------------
+
+ /**
+ @summary Print text containing tags into buffer (bound to `this`).
+ @param {string|string[]} text - Text to print.
+ @param {object} options - CodeMirror
+ [text marker](https://codemirror.net/doc/manual.html#api_marker) options.
+ */
+ printTextWithTags(text, options = {}) {
+ if (Array.isArray(text)) {
+ const tag = text.shift();
+ if (tag !== '') {
+ const markerOptions = { id: tag, ...options };
+ this.openTextMarker(markerOptions);
+ }
+ text.forEach((txt) => this.printTextWithTags(txt, options));
+ if (tag !== '') {
+ this.closeTextMarker();
+ }
+ } else if (typeof (text) === 'string') {
+ this.append(text);
+ } else { // This case should be useless when using TS.
+ console.error(
+ `Function 'printTextWithTags' accepts a parameter of `
+ + `type string or string array: got '${typeof text}'.`
+ );
+ }
+ }
+
}
// --------------------------------------------------------------------------
diff --git a/ivette/src/frama-c/states.ts b/ivette/src/frama-c/states.ts
index 5fc3a473d838bb478f267c6ab7472fe621c0bc4c..b846dee4fa49c752ec8489d5bc1fdd505a6fe8b8 100644
--- a/ivette/src/frama-c/states.ts
+++ b/ivette/src/frama-c/states.ts
@@ -172,22 +172,23 @@ export function useRequest(rq: string, params: any, options: any = {}) {
const state = React.useRef<string>();
const project = useProject();
const [response, setResponse] = React.useState(options.offline);
- const footprint =
- project ? JSON.stringify([project, rq, params]) : undefined;
+ const footprint = project ? JSON.stringify([project, rq, params]) : undefined;
async function trigger() {
if (project) {
try {
- const r = await Server.GET({ endpoint: rq, params });
- setResponse(r);
+ if (rq && params) {
+ const r = await Server.GET({ endpoint: rq, params });
+ setResponse(r);
+ }
} catch (error) {
PP.error(`Fail in useRequest '${rq}'. ${error.toString()}`);
const err = options.error;
- if (err !== undefined) setResponse(err);
+ setResponse(err);
}
} else {
const off = options.offline;
- if (off !== undefined) setResponse(off);
+ setResponse(off);
}
}
@@ -447,7 +448,7 @@ class SyncArray {
Dome.emit(this.UPDATE);
} catch (error) {
PP.error(
- `Fail to set reload of syncArray '${this.id}. ${error.toString()}`,
+ `Fail to set reload of syncArray '${this.id}'. ${error.toString()}`,
);
}
}
diff --git a/ivette/src/renderer/ASTinfo.tsx b/ivette/src/renderer/ASTinfo.tsx
new file mode 100644
index 0000000000000000000000000000000000000000..e505f52dbcd6fd8f59b56336268cd43df87798a6
--- /dev/null
+++ b/ivette/src/renderer/ASTinfo.tsx
@@ -0,0 +1,67 @@
+// --------------------------------------------------------------------------
+// --- AST Information
+// --------------------------------------------------------------------------
+
+import React from 'react';
+import * as States from 'frama-c/states';
+
+import { Vfill } from 'dome/layout/boxes';
+import { RichTextBuffer } from 'dome/text/buffers';
+import { Text } from 'dome/text/editors';
+import { Component } from 'frama-c/LabViews';
+
+// --------------------------------------------------------------------------
+// --- Information Panel
+// --------------------------------------------------------------------------
+
+const ASTinfo = () => {
+
+ const buffer = React.useMemo(() => new RichTextBuffer(), []);
+ const [select, setSelect] = States.useSelection();
+ const marker = select && select.marker;
+ const data = States.useRequest('kernel.ast.info', marker);
+
+ React.useEffect(() => {
+ buffer.clear();
+ if (data) {
+ buffer.printTextWithTags(data, { css: 'color: blue' });
+ }
+ }, [buffer, data]);
+
+ // Callbacks
+ function onSelection(name: string) {
+ // For now, the only markers are functions.
+ setSelect({ function: name });
+ }
+
+ // Component
+ return (
+ <>
+ <Vfill>
+ <Text
+ buffer={buffer}
+ mode="text"
+ theme="default"
+ onSelection={onSelection}
+ readOnly
+ />
+ </Vfill>
+ </>
+ );
+};
+
+// --------------------------------------------------------------------------
+// --- Export Component
+// --------------------------------------------------------------------------
+
+export default () => (
+ <Component
+ id="frama-c.astinfo"
+ label="Information"
+ title="AST Information"
+ >
+ <ASTinfo />
+ </Component>
+);
+
+// --------------------------------------------------------------------------
diff --git a/ivette/src/renderer/ASTview.tsx b/ivette/src/renderer/ASTview.tsx
index d21a73b27ea2376869a9a98478ea912595337a74..3fc396103d7f31e045b07c33646d66746e8cf821 100644
--- a/ivette/src/renderer/ASTview.tsx
+++ b/ivette/src/renderer/ASTview.tsx
@@ -33,22 +33,9 @@ const PP = new Dome.PP('AST View');
// --- Rich Text Printer
// --------------------------------------------------------------------------
-const printAST = (buffer: any, text: string) => {
- if (Array.isArray(text)) {
- const tag = text.shift();
- if (tag !== '') {
- buffer.openTextMarker({ id: tag });
- }
- text.forEach((txt) => printAST(buffer, txt));
- if (tag !== '') {
- buffer.closeTextMarker();
- }
- } else if (typeof (text) === 'string') {
- buffer.append(text);
- }
-};
-
-async function loadAST(buffer: any, theFunction?: string, theMarker?: string) {
+async function loadAST(
+ buffer: RichTextBuffer, theFunction?: string, theMarker?: string,
+) {
buffer.clear();
if (theFunction) {
buffer.log('// Loading', theFunction, '…');
@@ -60,9 +47,10 @@ async function loadAST(buffer: any, theFunction?: string, theMarker?: string) {
});
buffer.operation(() => {
buffer.clear();
- if (!data)
+ if (!data) {
buffer.log('// No code for function ', theFunction);
- printAST(buffer, data);
+ }
+ buffer.printTextWithTags(data);
if (theMarker)
buffer.scroll(theMarker, undefined);
});
@@ -89,6 +77,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('kernel.ast.markerKind');
const theFunction = select && select.function;
const theMarker = select && select.marker;
@@ -111,8 +100,18 @@ const ASTview = () => {
const zoomOut = () => fontSize > 4 && setFontSize(fontSize - 2);
const onSelection = (marker: any) => setSelect({ marker });
- // Theme Popup
+ function contextMenu(id: string) {
+ const marker = markers[id];
+ if (marker && marker.kind === 'function') {
+ const item1 = {
+ label: `Go to definition of ${marker.name}`,
+ onClick: () => setSelect({ function: marker.name }),
+ };
+ Dome.popupMenu([item1]);
+ }
+ }
+ // Theme Popup
const selectTheme = (id?: string) => id && setTheme(id);
const checkTheme =
(th: { id: string }) => ({ checked: th.id === theme, ...th });
@@ -155,6 +154,7 @@ const ASTview = () => {
lineWrapping={wrapText}
selection={theMarker}
onSelection={onSelection}
+ onContextMenu={contextMenu}
readOnly
/>
</>
diff --git a/ivette/src/renderer/Application.tsx b/ivette/src/renderer/Application.tsx
index 10439a75ba89564f385e65850aea5776c04a71d9..e3c343f52bd17df20d95344b3d7e8594ec368b8f 100644
--- a/ivette/src/renderer/Application.tsx
+++ b/ivette/src/renderer/Application.tsx
@@ -16,6 +16,7 @@ import { GridItem } from 'dome/layout/grids';
import * as Controller from './Controller';
import Properties from './Properties';
import ASTview from './ASTview';
+import ASTinfo from './ASTinfo';
// --------------------------------------------------------------------------
// --- Main View
@@ -64,6 +65,7 @@ export default (() => {
<Controller.Console />
<Properties />
<ASTview />
+ <ASTinfo />
</Group>
</LabView>
</Splitter>
diff --git a/src/kernel_services/ast_printing/printer_tag.ml b/src/kernel_services/ast_printing/printer_tag.ml
index a2befca2aa5df23dd6a38a390fe48ae753240b3d..c66a996f4213f566054c7a0f5aee972f5fd015e0 100644
--- a/src/kernel_services/ast_printing/printer_tag.ml
+++ b/src/kernel_services/ast_printing/printer_tag.ml
@@ -169,14 +169,17 @@ let ki_of_localizable loc = match loc with
| PIP ip -> Property.get_kinstr ip
| PGlobal _ -> Kglobal
-let varinfo_of_localizable loc =
- match kf_of_localizable loc with
- | Some kf -> Some (Kernel_function.get_vi kf)
- | None ->
- match loc with
- | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)
- | GFunDecl (_, vi, _) | GFun ({svar = vi }, _)) -> Some vi
- | _ -> None
+let varinfo_of_localizable = function
+ | PLval (_, _, (Var vi, NoOffset)) -> Some vi
+ | PVDecl (_, _, vi) -> Some vi
+ | PGlobal (GVar (vi, _, _) | GVarDecl (vi, _)
+ | GFunDecl (_, vi, _) | GFun ({svar = vi }, _)) -> Some vi
+ | _ -> None
+
+let typ_of_localizable = function
+ | PLval (_, _, lval) -> Some (Cil.typeOfLval lval)
+ | PExp (_, _, expr) -> Some (Cil.typeOf expr)
+ | _ -> None
let loc_of_localizable = function
| PStmt (_,st) | PStmtStart(_,st)
diff --git a/src/kernel_services/ast_printing/printer_tag.mli b/src/kernel_services/ast_printing/printer_tag.mli
index 074ec5c58ef05e47a804294db77e5b7fd1903f03..1986b69ae802643e3e16023b539a410c5d3a0e88 100644
--- a/src/kernel_services/ast_printing/printer_tag.mli
+++ b/src/kernel_services/ast_printing/printer_tag.mli
@@ -46,6 +46,7 @@ module Localizable: Datatype.S_with_collections with type t = localizable
val kf_of_localizable : localizable -> kernel_function option
val ki_of_localizable : localizable -> kinstr
val varinfo_of_localizable : localizable -> varinfo option
+val typ_of_localizable: localizable -> typ option
val loc_of_localizable : localizable -> location
(** Might return [Location.unknown] *)
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index f83bc30afaad8b70869486bbfaa1ba8c473877fa..460f01de5cb0fe57a65b3123cf6e77d965a652c1 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -215,7 +215,7 @@ module TypNoUnroll: S_with_collections_pretty with type t = typ
module Typeinfo: S_with_collections with type t = typeinfo
-module Varinfo_Id: Hptmap.Id_Datatype
+module Varinfo_Id: Hptmap.Id_Datatype with type t = varinfo
(** @plugin development guide *)
module Varinfo: sig
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index fc2c301f10a7b9767efac7374f0807850a768a66..c575f3a26c7762ba76abe9854b6a7b1f845eab2d 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -632,10 +632,9 @@ module type IdentifiedType =
sig
type t
val id : t -> int
- include Info
end
-module Identified(A : IdentifiedType) : Index with type t = A.t =
+module Identified(A : IdentifiedType)(I : Info) : Index with type t = A.t =
struct
type index = (int,A.t) Hashtbl.t
@@ -646,13 +645,13 @@ struct
type t = index
include Datatype.Undefined
let reprs = [Hashtbl.create 0]
- let name = "Server.Data.Identified.Type." ^ A.name
+ let name = "Server.Data.Identified.Type." ^ I.name
let mem_project = Datatype.never_any_project
end)
module STATE = State_builder.Ref(TYPE)
(struct
- let name = "Server.Data.Identified.State." ^ A.name
+ let name = "Server.Data.Identified.State." ^ I.name
let dependencies = []
let default () = Hashtbl.create 0
end)
@@ -666,12 +665,12 @@ struct
include Collection
(struct
type t = A.t
- let syntax = publish_id (module A)
+ let syntax = publish_id (module I)
let to_json a = `Int (get a)
let of_json js =
let k = Ju.to_int js in
try find k
- with Not_found -> failure "[%s] No registered id #%d" A.name k
+ with Not_found -> failure "[%s] No registered id #%d" I.name k
end)
end
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index bac87bebda5ca38ee8299dfe2e19a7d2e9767853..f10bf45b1714a36b59dca6ee225199845e964281 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -321,11 +321,10 @@ module type IdentifiedType =
sig
type t
val id : t -> int
- include Info
end
(** Builds a {i projectified} index on types with {i unique} identifiers. *)
-module Identified(A : IdentifiedType) : Index with type t = A.t
+module Identified(A : IdentifiedType)(I:Info) : Index with type t = A.t
(* -------------------------------------------------------------------------- *)
(** {2 Error handling}
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 21f6d0abeb19a78e6d158aa8886e7d510c3a1a5a..db4e8cd38e87e83a7f2827cae0561ac572f7808d 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -41,6 +41,41 @@ let () = Request.register ~page
(* --- Printers --- *)
(* -------------------------------------------------------------------------- *)
+(* The kind of a marker. *)
+module MarkerKind = struct
+ let t =
+ Enum.dictionary ~page ~name:"markerkind" ~title:"Marker kind"
+ ~descr:(Md.plain "Marker kind") ()
+
+ let kind name = Enum.tag t ~name ~descr:(Md.plain name) ()
+ let expr = kind "expression"
+ let lval = kind "lvalue"
+ let var = kind "variable"
+ let fct = kind "function"
+ let decl = kind "declaration"
+ let stmt = kind "statement"
+ let glob = kind "global"
+ let term = kind "term"
+ let prop = kind "property"
+
+ let tag =
+ let open Printer_tag in
+ function
+ | PStmt _ -> stmt
+ | PStmtStart _ -> stmt
+ | PVDecl _ -> decl
+ | PLval (_, _, (Var vi, NoOffset)) ->
+ if Cil.isFunctionType vi.vtype then fct else var
+ | PLval _ -> lval
+ | PExp _ -> expr
+ | PTermLval _ -> term
+ | PGlobal _ -> glob
+ | PIP _ -> prop
+
+ let data = Enum.publish t ~tag ()
+ include (val data : S with type t = Printer_tag.localizable)
+end
+
module Marker =
struct
@@ -75,6 +110,39 @@ struct
let default = index
end)
+ let get_name = function
+ | PLval (_, _, (Var vi, NoOffset)) -> Some vi.vname
+ | PLval (_, _, lval) -> Some (Format.asprintf "%a" Printer.pp_lval lval)
+ | PExp (_, _, expr) -> Some (Format.asprintf "%a" Printer.pp_exp expr)
+ | PStmt _ | PStmtStart _ | PVDecl _
+ | PTermLval _ | PGlobal _| PIP _ -> None
+
+ let iter f =
+ Localizable.Hashtbl.iter (fun key str -> f (key, str)) (STATE.get ()).tags
+
+ let array =
+ let model = States.model () in
+ let () =
+ States.column ~model
+ ~name:"kind" ~descr:(Md.plain "Marker kind")
+ ~data:(module MarkerKind) ~get:fst ()
+ in
+ let () =
+ States.column ~model
+ ~name:"name"
+ ~descr:(Md.plain "Marker identifier for the end-user, if any")
+ ~data:(module Jstring.Joption)
+ ~get:(fun (tag, _) -> get_name tag)
+ ()
+ in
+ States.register_array
+ ~page
+ ~name:"kernel.ast.markerKind"
+ ~descr:(Md.plain "Kind of markers")
+ ~key:snd
+ ~iter
+ model
+
let create_tag = function
| PStmt(_,s) -> Printf.sprintf "#s%d" s.sid
| PStmtStart(_,s) -> Printf.sprintf "#k%d" s.sid
@@ -92,6 +160,7 @@ struct
let tag = create_tag loc in
Localizable.Hashtbl.add tags loc tag ;
Hashtbl.add locs tag loc ;
+ States.update array (loc, tag);
tag
let lookup tag = Hashtbl.find (STATE.get()).locs tag
@@ -177,6 +246,76 @@ let () = Request.register ~page
~input:(module Kf) ~output:(module Jtext)
(fun kf -> Jbuffer.to_json Printer.pp_global (Kernel_function.get_global kf))
+(* -------------------------------------------------------------------------- *)
+(* --- Information --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Info = struct
+ open Printer_tag
+
+ let print_function fmt name =
+ let stag = Transitioning.Format.stag_of_string name in
+ Transitioning.Format.pp_open_stag fmt stag;
+ Format.pp_print_string fmt name;
+ Transitioning.Format.pp_close_stag fmt ()
+
+ let print_kf fmt kf = print_function fmt (Kernel_function.get_name kf)
+
+ let print_variable fmt vi =
+ Format.fprintf fmt "Variable %s has type %a.@."
+ vi.vname Printer.pp_typ vi.vtype;
+ let kf = Kernel_function.find_defining_kf vi in
+ let pp_kf fmt kf = Format.fprintf fmt " of function %a" print_kf kf in
+ Format.fprintf fmt "It is a %s variable%a.@."
+ (if vi.vglob then "global" else if vi.vformal then "formal" else "local")
+ (Transitioning.Format.pp_print_option pp_kf) kf;
+ if vi.vtemp then
+ Format.fprintf fmt "This is a temporary variable%s.@."
+ (match vi.vdescr with None -> "" | Some descr -> " for " ^ descr);
+ Format.fprintf fmt "It is %sreferenced and its address is %staken."
+ (if vi.vreferenced then "" else "not ")
+ (if vi.vaddrof then "" else "not ")
+
+ let print_varinfo fmt vi =
+ if Cil.isFunctionType vi.vtype
+ then
+ Format.fprintf fmt "%a is a C function of type '%a'."
+ print_function vi.vname Printer.pp_typ vi.vtype
+ else print_variable fmt vi
+
+ let print_lvalue fmt _loc = function
+ | Var vi, NoOffset -> print_varinfo fmt vi
+ | lval ->
+ Format.fprintf fmt "This is an lvalue of type %a."
+ Printer.pp_typ (Cil.typeOfLval lval)
+
+ let print_localizable fmt = function
+ | PExp (_, _, e) ->
+ Format.fprintf fmt "This is a pure C expression of type %a."
+ Printer.pp_typ (Cil.typeOf e)
+ | PLval (_, _, lval) as loc -> print_lvalue fmt loc lval
+ | PVDecl (_, _, vi) ->
+ Format.fprintf fmt "This is the declaration of variable %a.@.@."
+ Printer.pp_varinfo vi;
+ print_varinfo fmt vi
+ | PStmt (kf, _) | PStmtStart (kf, _) ->
+ Format.fprintf fmt "This is a statement of function %a." print_kf kf
+ | _ -> ()
+
+ let get_marker_info loc =
+ let buffer = Jbuffer.create () in
+ let fmt = Jbuffer.formatter buffer in
+ print_localizable fmt loc;
+ Format.pp_print_flush fmt ();
+ Jbuffer.contents buffer
+end
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"kernel.ast.info"
+ ~descr:(Md.plain "Get textual information about a marker")
+ ~input:(module Marker) ~output:(module Jtext)
+ Info.get_marker_info
+
(* -------------------------------------------------------------------------- *)
(* --- Files --- *)
(* -------------------------------------------------------------------------- *)