From d14e3b2a6198a9bd1bcc302cd70627b968e50fba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Sat, 25 Nov 2023 15:40:12 +0100
Subject: [PATCH] [server] New synchronized array for global variables.
---
ivette/src/frama-c/kernel/api/ast/index.ts | 120 +++++++++++++++++++++
src/plugins/server/kernel_ast.ml | 73 +++++++++++++
2 files changed, 193 insertions(+)
diff --git a/ivette/src/frama-c/kernel/api/ast/index.ts b/ivette/src/frama-c/kernel/api/ast/index.ts
index 749c722b9e3..65907b9357a 100644
--- a/ivette/src/frama-c/kernel/api/ast/index.ts
+++ b/ivette/src/frama-c/kernel/api/ast/index.ts
@@ -513,6 +513,126 @@ export const functionsDataDefault: functionsData =
stdlib: undefined, builtin: undefined, extern: undefined,
sloc: sourceDefault };
+/** Data for array rows [`globals`](#globals) */
+export interface globalsData {
+ /** Entry identifier. */
+ key: Json.key<'#globals'>;
+ /** Declaration Tag */
+ decl: decl;
+ /** Name */
+ name: string;
+ /** Type */
+ type: string;
+ /** Is the variable from the Frama-C stdlib? */
+ stdlib: boolean;
+ /** Is the variable extern? */
+ extern: boolean;
+ /** Is the variable const? */
+ const: boolean;
+ /** Is the variable volatile? */
+ volatile: boolean;
+ /** Is the variable ghost? */
+ ghost: boolean;
+ /** Is the variable explicitly initialized? */
+ init: boolean;
+ /** Is the variable in the source code? */
+ source: boolean;
+ /** Source location */
+ sloc: source;
+}
+
+/** Decoder for `globalsData` */
+export const jGlobalsData: Json.Decoder<globalsData> =
+ Json.jObject({
+ key: Json.jKey<'#globals'>('#globals'),
+ decl: jDecl,
+ name: Json.jString,
+ type: Json.jString,
+ stdlib: Json.jBoolean,
+ extern: Json.jBoolean,
+ const: Json.jBoolean,
+ volatile: Json.jBoolean,
+ ghost: Json.jBoolean,
+ init: Json.jBoolean,
+ source: Json.jBoolean,
+ sloc: jSource,
+ });
+
+/** Natural order for `globalsData` */
+export const byGlobalsData: Compare.Order<globalsData> =
+ Compare.byFields
+ <{ key: Json.key<'#globals'>, decl: decl, name: string, type: string,
+ stdlib: boolean, extern: boolean, const: boolean, volatile: boolean,
+ ghost: boolean, init: boolean, source: boolean, sloc: source }>({
+ key: Compare.string,
+ decl: byDecl,
+ name: Compare.alpha,
+ type: Compare.string,
+ stdlib: Compare.boolean,
+ extern: Compare.boolean,
+ const: Compare.boolean,
+ volatile: Compare.boolean,
+ ghost: Compare.boolean,
+ init: Compare.boolean,
+ source: Compare.boolean,
+ sloc: bySource,
+ });
+
+/** Signal for array [`globals`](#globals) */
+export const signalGlobals: Server.Signal = {
+ name: 'kernel.ast.signalGlobals',
+};
+
+const reloadGlobals_internal: Server.GetRequest<null,null> = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.reloadGlobals',
+ input: Json.jNull,
+ output: Json.jNull,
+ signals: [],
+};
+/** Force full reload for array [`globals`](#globals) */
+export const reloadGlobals: Server.GetRequest<null,null>= reloadGlobals_internal;
+
+const fetchGlobals_internal: Server.GetRequest<
+ number,
+ { reload: boolean, removed: Json.key<'#globals'>[], updated: globalsData[],
+ pending: number }
+ > = {
+ kind: Server.RqKind.GET,
+ name: 'kernel.ast.fetchGlobals',
+ input: Json.jNumber,
+ output: Json.jObject({
+ reload: Json.jBoolean,
+ removed: Json.jArray(Json.jKey<'#globals'>('#globals')),
+ updated: Json.jArray(jGlobalsData),
+ pending: Json.jNumber,
+ }),
+ signals: [],
+};
+/** Data fetcher for array [`globals`](#globals) */
+export const fetchGlobals: Server.GetRequest<
+ number,
+ { reload: boolean, removed: Json.key<'#globals'>[], updated: globalsData[],
+ pending: number }
+ >= fetchGlobals_internal;
+
+const globals_internal: State.Array<Json.key<'#globals'>,globalsData> = {
+ name: 'kernel.ast.globals',
+ getkey: ((d:globalsData) => d.key),
+ signal: signalGlobals,
+ fetch: fetchGlobals,
+ reload: reloadGlobals,
+ order: byGlobalsData,
+};
+/** AST global variables */
+export const globals: State.Array<Json.key<'#globals'>,globalsData> = globals_internal;
+
+/** Default value for `globalsData` */
+export const globalsDataDefault: globalsData =
+ { key: Json.jKey<'#globals'>('#globals')(''), decl: declDefault, name: '',
+ type: '', stdlib: false, extern: false, const: false, volatile: false,
+ ghost: false, init: false, source: false, sloc: sourceDefault };
+
/** Updated AST information */
export const getInformationUpdate: Server.Signal = {
name: 'kernel.ast.getInformationUpdate',
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index db570556c41..41fc7a08cf5 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -683,6 +683,79 @@ struct
end
+(* -------------------------------------------------------------------------- *)
+(* --- Global variables --- *)
+(* -------------------------------------------------------------------------- *)
+
+module GlobalVars = struct
+
+ let key vi = Printf.sprintf "vi#%d" vi.vid
+
+ let _ : varinfo States.array =
+ let model = States.model () in
+ States.column model
+ ~name:"decl"
+ ~descr:(Md.plain "Declaration Tag")
+ ~data:(module Decl)
+ ~get:(fun vi -> Printer_tag.SGlobal vi);
+ States.column model
+ ~name:"name"
+ ~descr:(Md.plain "Name")
+ ~data:(module Data.Jalpha)
+ ~get:(fun vi -> vi.vname);
+ States.column model
+ ~name:"type"
+ ~descr:(Md.plain "Type")
+ ~data:(module Jstring)
+ ~get:(fun vi -> Rich_text.to_string Printer.pp_typ vi.vtype);
+ States.column model
+ ~name:"stdlib"
+ ~descr:(Md.plain "Is the variable from the Frama-C stdlib?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> Cil.is_in_libc vi.vattr);
+ States.column model
+ ~name:"extern"
+ ~descr:(Md.plain "Is the variable extern?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> vi.vstorage = Extern);
+ States.column model
+ ~name:"const"
+ ~descr:(Md.plain "Is the variable const?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> Cil.isGlobalInitConst vi);
+ States.column model
+ ~name:"volatile"
+ ~descr:(Md.plain "Is the variable volatile?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> Cil.isVolatileType vi.vtype);
+ States.column model
+ ~name:"ghost"
+ ~descr:(Md.plain "Is the variable ghost?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> Cil.isGhostType vi.vtype);
+ States.column model
+ ~name:"init"
+ ~descr:(Md.plain "Is the variable explicitly initialized?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> Option.is_some (Globals.Vars.find vi).init);
+ States.column model
+ ~name:"source"
+ ~descr:(Md.plain "Is the variable in the source code?")
+ ~data:(module Data.Jbool)
+ ~get:(fun vi -> vi.vsource);
+ States.column model
+ ~name:"sloc"
+ ~descr:(Md.plain "Source location")
+ ~data:(module Position)
+ ~get:(fun vi -> fst vi.vdecl);
+ States.register_array model
+ ~package ~key
+ ~name:"globals"
+ ~descr:(Md.plain "AST global variables")
+ ~iter:(fun f -> Globals.Vars.iter (fun vi _init -> f vi))
+ ~add_reload_hook:ast_update_hook
+end
+
(* -------------------------------------------------------------------------- *)
(* --- Marker Information --- *)
(* -------------------------------------------------------------------------- *)
--
GitLab