Merge branch 'feature/eva/ivette-functions-table' into 'master'

Feature/eva/ivette functions table

See merge request frama-c/frama-c!3884

ivette/src/frama-c/kernel/Globals.tsx

@@ -31,10 +31,12 @@ import { alpha } from 'dome/data/compare';
 import { Section, Item } from 'dome/frame/sidebars';
 import { Button } from 'dome/controls/buttons';
 import * as Toolbars from 'dome/frame/toolbars';
+import * as ArrayUtils from 'dome/data/arrays';
 
 import * as States from 'frama-c/states';
-import { functions, functionsData } from 'frama-c/kernel/api/ast';
+import * as Kernel from 'frama-c/kernel/api/ast';
 import { computationState } from 'frama-c/plugins/eva/api/general';
+import * as Eva from 'frama-c/plugins/eva/api/general';
 
 // --------------------------------------------------------------------------
 // --- Global Search Hints
@@ -51,7 +53,7 @@ function makeFunctionHint(fct: functionsData): Toolbars.Hint {
 
 async function lookupGlobals(pattern: string): Promise<Toolbars.Hint[]> {
   const lookup = pattern.toLowerCase();
-  const fcts = States.getSyncArray(functions).getArray();
+  const fcts = States.getSyncArray(Kernel.functions).getArray();
   return fcts.filter((fn) => (
     0 <= fn.name.toLowerCase().indexOf(lookup)
   )).map(makeFunctionHint);
@@ -96,13 +98,18 @@ function FctItem(props: FctItemProps): JSX.Element {
 // --- Globals Section(s)
 // --------------------------------------------------------------------------
 
+type functionsData =
+  Kernel.functionsData | (Kernel.functionsData & Eva.functionsData)
+
 export default function Globals(): JSX.Element {
 
   // Hooks
   const [selection, updateSelection] = States.useSelection();
-  const fcts = States.useSyncArray(functions).getArray().sort(
+  const kernelFcts = States.useSyncArray(Kernel.functions).getArray().sort(
     (f, g) => alpha(f.name, g.name),
   );
+  const evaFcts = States.useSyncArray(Eva.functions).getArray();
+  const fcts = ArrayUtils.mergeArraysByKey(kernelFcts, evaFcts);
   const { useFlipSettings } = Dome;
   const [stdlib, flipStdlib] =
     useFlipSettings('ivette.globals.stdlib', false);
@@ -132,7 +139,8 @@ export default function Globals(): JSX.Element {
       (stdlib || !fct.stdlib)
       && (builtin || !fct.builtin)
       && (undef || fct.defined)
-      && (!evaOnly || !evaComputed || (fct.eva_analyzed === true))
+      && (!evaOnly || !evaComputed ||
+        ('eva_analyzed' in fct && fct.eva_analyzed === true))
       && (!selected || !multipleSelectionActive || isSelected(fct));
     return visible || (!!current && fct.name === current);
   }

ivette/src/frama-c/kernel/api/ast/index.ts

@@ -367,8 +367,6 @@ export interface functionsData {
   stdlib?: boolean;
   /** Is the function a Frama-C builtin? */
   builtin?: boolean;
-  /** Has the function been analyzed by Eva */
-  eva_analyzed?: boolean;
   /** Source location */
   sloc: source;
 }
@@ -384,7 +382,6 @@ export const jFunctionsData: Json.Loose<functionsData> =
     defined: Json.jBoolean,
     stdlib: Json.jBoolean,
     builtin: Json.jBoolean,
-    eva_analyzed: Json.jBoolean,
     sloc: jSourceSafe,
   });
 
@@ -397,7 +394,7 @@ export const byFunctionsData: Compare.Order<functionsData> =
   Compare.byFields
     <{ key: Json.key<'#functions'>, name: string, signature: string,
        main?: boolean, defined?: boolean, stdlib?: boolean,
-       builtin?: boolean, eva_analyzed?: boolean, sloc: source }>({
+       builtin?: boolean, sloc: source }>({
     key: Compare.string,
     name: Compare.alpha,
     signature: Compare.string,
@@ -405,7 +402,6 @@ export const byFunctionsData: Compare.Order<functionsData> =
     defined: Compare.defined(Compare.boolean),
     stdlib: Compare.defined(Compare.boolean),
     builtin: Compare.defined(Compare.boolean),
-    eva_analyzed: Compare.defined(Compare.boolean),
     sloc: bySource,
   });
 

ivette/src/frama-c/plugins/eva/api/general/index.ts

@@ -123,6 +123,83 @@ export const getCallers: Server.GetRequest<
   [ Json.key<'#fct'>, Json.key<'#stmt'> ][]
   >= getCallers_internal;
 
+/** Data for array rows [`functions`](#functions)  */
+export interface functionsData {
+  /** Entry identifier. */
+  key: Json.key<'#functions'>;
+  /** Has the function been analyzed by Eva */
+  eva_analyzed?: boolean;
+}
+
+/** Loose decoder for `functionsData` */
+export const jFunctionsData: Json.Loose<functionsData> =
+  Json.jObject({
+    key: Json.jFail(Json.jKey<'#functions'>('#functions'),
+           '#functions expected'),
+    eva_analyzed: Json.jBoolean,
+  });
+
+/** Safe decoder for `functionsData` */
+export const jFunctionsDataSafe: Json.Safe<functionsData> =
+  Json.jFail(jFunctionsData,'FunctionsData expected');
+
+/** Natural order for `functionsData` */
+export const byFunctionsData: Compare.Order<functionsData> =
+  Compare.byFields
+    <{ key: Json.key<'#functions'>, eva_analyzed?: boolean }>({
+    key: Compare.string,
+    eva_analyzed: Compare.defined(Compare.boolean),
+  });
+
+/** Signal for array [`functions`](#functions)  */
+export const signalFunctions: Server.Signal = {
+  name: 'plugins.eva.general.signalFunctions',
+};
+
+const reloadFunctions_internal: Server.GetRequest<null,null> = {
+  kind: Server.RqKind.GET,
+  name:   'plugins.eva.general.reloadFunctions',
+  input:  Json.jNull,
+  output: Json.jNull,
+  signals: [],
+};
+/** Force full reload for array [`functions`](#functions)  */
+export const reloadFunctions: Server.GetRequest<null,null>= reloadFunctions_internal;
+
+const fetchFunctions_internal: Server.GetRequest<
+  number,
+  { pending: number, updated: functionsData[],
+    removed: Json.key<'#functions'>[], reload: boolean }
+  > = {
+  kind: Server.RqKind.GET,
+  name:   'plugins.eva.general.fetchFunctions',
+  input:  Json.jNumber,
+  output: Json.jObject({
+            pending: Json.jFail(Json.jNumber,'Number expected'),
+            updated: Json.jList(jFunctionsData),
+            removed: Json.jList(Json.jKey<'#functions'>('#functions')),
+            reload: Json.jFail(Json.jBoolean,'Boolean expected'),
+          }),
+  signals: [],
+};
+/** Data fetcher for array [`functions`](#functions)  */
+export const fetchFunctions: Server.GetRequest<
+  number,
+  { pending: number, updated: functionsData[],
+    removed: Json.key<'#functions'>[], reload: boolean }
+  >= fetchFunctions_internal;
+
+const functions_internal: State.Array<Json.key<'#functions'>,functionsData> = {
+  name: 'plugins.eva.general.functions',
+  getkey: ((d:functionsData) => d.key),
+  signal: signalFunctions,
+  fetch: fetchFunctions,
+  reload: reloadFunctions,
+  order: byFunctionsData,
+};
+/** AST Functions */
+export const functions: State.Array<Json.key<'#functions'>,functionsData> = functions_internal;
+
 /** Unreachable and non terminating statements. */
 export interface deadCode {
   /** List of unreachable statements. */

src/plugins/eva/api/general_requests.ml

@@ -71,10 +71,27 @@ let () = Request.register ~package
 
 (* ----- Functions ---------------------------------------------------------- *)
 
-let () =
-  Analysis.register_computation_hook
-    (fun _ -> States.reload Kernel_ast.Functions.array)
-
+module Functions =
+struct
+  let _array : kernel_function States.array =
+    let model = States.model () in
+
+    States.column model
+      ~name:"eva_analyzed"
+      ~descr:(Markdown.plain "Has the function been analyzed by Eva")
+      ~data:(module Data.Jbool)
+      ~default:false
+      ~get:Results.is_called;
+
+    States.register_array model
+      ~package
+      ~key:Server.Kernel_ast.Functions.key
+      ~name:"functions"
+      ~descr:(Markdown.plain "AST Functions")
+      ~iter:Server.Kernel_ast.Functions.iter
+      ~add_reload_hook:(fun f ->
+          Analysis.register_computation_hook (fun _ -> f () ))
+end
 
 (* ----- Dead code: unreachable and non-terminating statements -------------- *)
 

src/plugins/server/kernel_ast.ml

@@ -508,9 +508,6 @@ struct
     let vi = Kernel_function.get_vi kf in
     Cil.is_in_libc vi.vattr
 
-  let is_eva_analyzed kf =
-    if Db.Value.is_computed () then !Db.Value.is_called kf else false
-
   let iter f =
     Globals.Functions.iter
       (fun kf ->
@@ -554,12 +551,6 @@ struct
         ~data:(module Data.Jbool)
         ~default:false
         ~get:is_builtin;
-      States.column model
-        ~name:"eva_analyzed"
-        ~descr:(Md.plain "Has the function been analyzed by Eva")
-        ~data:(module Data.Jbool)
-        ~default:false
-        ~get:is_eva_analyzed;
       States.column model
         ~name:"sloc"
         ~descr:(Md.plain "Source location")

src/plugins/server/kernel_ast.mli

@@ -95,6 +95,8 @@ end
 
 module Functions :
 sig
+  val iter : (kernel_function -> unit) -> unit
+  val key : kernel_function -> string
   val array : kernel_function States.array
 end