From 33fc04950eaf753e3d864a9c42111e11fb1fff7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 24 Jun 2020 16:46:45 +0200
Subject: [PATCH] [ivette] natural orders
---
ivette/api/dive.ts | 7 ++
ivette/api/kernel/ast.ts | 5 ++
ivette/api/kernel/data.ts | 10 +++
ivette/api/kernel/project.ts | 14 ++++
ivette/api/kernel/properties.ts | 6 ++
ivette/api/kernel/services.ts | 20 ++++-
ivette/api/server_tsc.ml | 84 +++++++++++++++++---
ivette/src/dome/src/renderer/data/compare.ts | 18 ++++-
src/plugins/dive/server_interface.ml | 4 +-
src/plugins/server/data.ml | 3 +-
src/plugins/server/data.mli | 1 +
src/plugins/server/package.ml | 2 +-
12 files changed, 155 insertions(+), 19 deletions(-)
diff --git a/ivette/api/dive.ts b/ivette/api/dive.ts
index de058d27793..cb3badb52ff 100644
--- a/ivette/api/dive.ts
+++ b/ivette/api/dive.ts
@@ -7,7 +7,9 @@
*/
import * as Json from 'dome/data/json';
+import * as Compare from 'dome/data/compare';
import * as Server from 'frama-c/server';
+import * as State from 'frama-c/states';
/** The name of variable of the program */
@@ -30,6 +32,11 @@ export const jVariableName: Json.Loose<variableName> =
Json.jTry(jVariableNameSafe);
/** Natural order for `variableName` */
+export const byVariableName: Compare.Order<variableName> =
+ Compare.byFields({
+ funName: Compare.defined(Compare.alpha),
+ varName: Compare.alpha,
+ });
/** Retrieve the whole graph */
export const graph: Server.GetRequest<null,Json.json> = {
diff --git a/ivette/api/kernel/ast.ts b/ivette/api/kernel/ast.ts
index b6016940b3d..18f6889d903 100644
--- a/ivette/api/kernel/ast.ts
+++ b/ivette/api/kernel/ast.ts
@@ -7,7 +7,9 @@
*/
import * as Json from 'dome/data/json';
+import * as Compare from 'dome/data/compare';
import * as Server from 'frama-c/server';
+import * as State from 'frama-c/states';
import { byTag } from 'api/kernel/data';
import { byText } from 'api/kernel/data';
@@ -56,6 +58,8 @@ export const jMarkerKindSafe: Json.Safe<markerKind> =
export const jMarkerKind: Json.Loose<markerKind> = Json.jEnum(markerKind);
/** Natural order for `markerKind` */
+export const byMarkerKind: Compare.Order<markerKind> =
+ Compare.byEnym(markerKind);
/** Registered tags for the above type. */
export const markerKindTags: Server.GetRequest<null,tag[]> = {
@@ -138,6 +142,7 @@ export const jMarker: Json.Loose<marker> =
);
/** Natural order for `marker` */
+export const byMarker: Compare.Order<marker> = Compare.structural;
/** Collect all functions in the AST */
export const getFunctions: Server.GetRequest<null,Json.Key<'#fct'>[]> = {
diff --git a/ivette/api/kernel/data.ts b/ivette/api/kernel/data.ts
index 9ea5ff79642..151f9226057 100644
--- a/ivette/api/kernel/data.ts
+++ b/ivette/api/kernel/data.ts
@@ -7,7 +7,9 @@
*/
import * as Json from 'dome/data/json';
+import * as Compare from 'dome/data/compare';
import * as Server from 'frama-c/server';
+import * as State from 'frama-c/states';
/** Markdown (inlined) text. */
@@ -21,6 +23,7 @@ export const jMarkdownSafe: Json.Safe<markdown> =
export const jMarkdown: Json.Loose<markdown> = Json.jString;
/** Natural order for `markdown` */
+export const byMarkdown: Compare.Order<markdown> = Compare.primitive;
/** Rich text format uses `[tag; …text ]` to apply the tag `tag` to the enclosed text. Empty tag `""` can also used to simply group text together. */
export type text = null | string | text[];
@@ -37,6 +40,7 @@ export const jText: Json.Loose<text> =
);
/** Natural order for `text` */
+export const byText: Compare.Order<text> = Compare.structural;
/** Enum Tag Description */
export type tag = { name: string, label: markdown, descr: markdown };
@@ -53,5 +57,11 @@ export const jTagSafe: Json.Safe<tag> =
export const jTag: Json.Loose<tag> = Json.jTry(jTagSafe);
/** Natural order for `tag` */
+export const byTag: Compare.Order<tag> =
+ Compare.byFields({
+ name: Compare.primitive,
+ label: byMarkdown,
+ descr: byMarkdown,
+ });
/* ------------------------------------- */
diff --git a/ivette/api/kernel/project.ts b/ivette/api/kernel/project.ts
index 5335e9e6cc8..9af041819f0 100644
--- a/ivette/api/kernel/project.ts
+++ b/ivette/api/kernel/project.ts
@@ -7,7 +7,9 @@
*/
import * as Json from 'dome/data/json';
+import * as Compare from 'dome/data/compare';
import * as Server from 'frama-c/server';
+import * as State from 'frama-c/states';
/** Project informations */
@@ -27,6 +29,12 @@ export const jProjectInfo: Json.Loose<projectInfo> =
Json.jTry(jProjectInfoSafe);
/** Natural order for `projectInfo` */
+export const byProjectInfo: Compare.Order<projectInfo> =
+ Compare.byFields({
+ id: Compare.primitive,
+ name: Compare.primitive,
+ current: Compare.primitive,
+ });
/** Request to be executed on the specified project. */
export type projectRequest =
@@ -45,6 +53,12 @@ export const jProjectRequest: Json.Loose<projectRequest> =
Json.jTry(jProjectRequestSafe);
/** Natural order for `projectRequest` */
+export const byProjectRequest: Compare.Order<projectRequest> =
+ Compare.byFields({
+ project: Compare.primitive,
+ request: Compare.primitive,
+ data: Compare.structural,
+ });
/** Returns the current project */
export const getCurrent: Server.GetRequest<null,projectInfo> = {
diff --git a/ivette/api/kernel/properties.ts b/ivette/api/kernel/properties.ts
index 696f28775e0..a17f096b215 100644
--- a/ivette/api/kernel/properties.ts
+++ b/ivette/api/kernel/properties.ts
@@ -7,7 +7,9 @@
*/
import * as Json from 'dome/data/json';
+import * as Compare from 'dome/data/compare';
import * as Server from 'frama-c/server';
+import * as State from 'frama-c/states';
import { byTag } from 'api/kernel/data';
import { jTag } from 'api/kernel/data';
@@ -98,6 +100,7 @@ export const jPropKindSafe: Json.Safe<propKind> =
export const jPropKind: Json.Loose<propKind> = Json.jEnum(propKind);
/** Natural order for `propKind` */
+export const byPropKind: Compare.Order<propKind> = Compare.byEnym(propKind);
/** Registered tags for the above type. */
export const propKindTags: Server.GetRequest<null,tag[]> = {
@@ -141,6 +144,8 @@ export const jPropStatusSafe: Json.Safe<propStatus> =
export const jPropStatus: Json.Loose<propStatus> = Json.jEnum(propStatus);
/** Natural order for `propStatus` */
+export const byPropStatus: Compare.Order<propStatus> =
+ Compare.byEnym(propStatus);
/** Registered tags for the above type. */
export const propStatusTags: Server.GetRequest<null,tag[]> = {
@@ -198,6 +203,7 @@ export const jAlarmsSafe: Json.Safe<alarms> =
export const jAlarms: Json.Loose<alarms> = Json.jEnum(alarms);
/** Natural order for `alarms` */
+export const byAlarms: Compare.Order<alarms> = Compare.byEnym(alarms);
/** Registered tags for the above type. */
export const alarmsTags: Server.GetRequest<null,tag[]> = {
diff --git a/ivette/api/kernel/services.ts b/ivette/api/kernel/services.ts
index 56348fad9fc..ed4ed06e0f9 100644
--- a/ivette/api/kernel/services.ts
+++ b/ivette/api/kernel/services.ts
@@ -7,7 +7,9 @@
*/
import * as Json from 'dome/data/json';
+import * as Compare from 'dome/data/compare';
import * as Server from 'frama-c/server';
+import * as State from 'frama-c/states';
import { byTag } from 'api/kernel/data';
import { jTag } from 'api/kernel/data';
@@ -55,6 +57,13 @@ export const jSourceSafe: Json.Safe<source> =
export const jSource: Json.Loose<source> = Json.jTry(jSourceSafe);
/** Natural order for `source` */
+export const bySource: Compare.Order<source> =
+ Compare.byFields({
+ dir: Compare.primitive,
+ base: Compare.primitive,
+ file: Compare.primitive,
+ line: Compare.primitive,
+ });
/** Log messages categories. */
export enum logkind {
@@ -80,6 +89,7 @@ export const jLogkindSafe: Json.Safe<logkind> =
export const jLogkind: Json.Loose<logkind> = Json.jEnum(logkind);
/** Natural order for `logkind` */
+export const byLogkind: Compare.Order<logkind> = Compare.byEnym(logkind);
/** Registered tags for the above type. */
export const logkindTags: Server.GetRequest<null,tag[]> = {
@@ -106,7 +116,7 @@ export interface log {
/** Safe decoder for `log` */
export const jLogSafe: Json.Safe<log> =
Json.jObject({
- kind: Json.jFail(Json.jEnum(logkind),'kernel.services.logkind expected'),
+ kind: jLogkindSafe,
plugin: Json.jFail(Json.jString,'String expected'),
message: Json.jFail(Json.jString,'String expected'),
category: Json.jString,
@@ -117,6 +127,14 @@ export const jLogSafe: Json.Safe<log> =
export const jLog: Json.Loose<log> = Json.jTry(jLogSafe);
/** Natural order for `log` */
+export const byLog: Compare.Order<log> =
+ Compare.byFields({
+ kind: byLogkind,
+ plugin: Compare.primitive,
+ message: Compare.primitive,
+ category: Compare.defined(Compare.primitive),
+ source: Compare.defined(bySource),
+ });
/** Turn logs monitoring on/off */
export const setLogs: Server.SetRequest<boolean,null> = {
diff --git a/ivette/api/server_tsc.ml b/ivette/api/server_tsc.ml
index 378dfc49d94..48c3b15877f 100644
--- a/ivette/api/server_tsc.ml
+++ b/ivette/api/server_tsc.ml
@@ -39,7 +39,7 @@ let keywords = [
"let"; "package"; "private"; "protected"; "public"; "static"; "yield"; "any";
"boolean"; "constructor"; "declare"; "get"; "module"; "require"; "number";
"set"; "string"; "symbol"; "type"; "from"; "of";
- "Json";
+ "Json"; "Compare"; "Server"; "State";
]
let pp_descr = Md.pp_text ?page:None
@@ -205,6 +205,49 @@ let typeOfParam = function
let field fd = fd.Pkg.fd_name , fd.Pkg.fd_type in
Jrecord (List.map field fjs)
+(* -------------------------------------------------------------------------- *)
+(* --- Jtype Order --- *)
+(* -------------------------------------------------------------------------- *)
+
+let makeOrder ~self ~names fmt js =
+ let open Pkg in
+ let rec pp fmt = function
+ | Jnull -> Format.pp_print_string fmt "Compare.equal"
+ | Jalpha -> Format.pp_print_string fmt "Compare.alpha"
+ | Jnumber | Jstring | Jboolean | Jkey _ | Jindex _
+ -> Format.pp_print_string fmt "Compare.primitive"
+ | Jself -> jcall names fmt (Pkg.Derived.order self)
+ | Jdata id -> jcall names fmt (Pkg.Derived.order id)
+ | Joption js ->
+ Format.fprintf fmt "@[<hov 2>Compare.defined(@,%a)@]" pp js
+ | Jany | Junion _ -> (* Can not find a better solution *)
+ Format.fprintf fmt "Compare.structural"
+ | Jenum id ->
+ Format.fprintf fmt "@[<hov 2>Compare.byEnym(@,%a)@]" (jcall names) id
+ | Jlist js | Jarray js ->
+ Format.fprintf fmt "@[<hov 2>Compare.array(@,%a)@]" pp js
+ | Jtuple jts ->
+ let name = match List.length jts with
+ | 2 -> "pair"
+ | 3 -> "triple"
+ | 4 -> "tuple4"
+ | 5 -> "tuple5"
+ | n -> Self.abort "No comparison for %d-tuples" n in
+ Format.fprintf fmt "@[<hv 0>@[<hv 2>Compare.%s(" name ;
+ List.iter (fun js -> Format.fprintf fmt "@,%a," pp js) jts ;
+ Format.fprintf fmt "@]@,)@]" ;
+ | Jrecord jfs ->
+ Format.fprintf fmt "@[<hv 0>@[<hv 2>Compare.byFields({" ;
+ List.iter
+ (fun (fd,js) -> Format.fprintf fmt "@ @[<hov 2>%s: %a,@]" fd pp js) jfs ;
+ Format.fprintf fmt "@]@ })@]" ;
+ | Jdict(kd,js) ->
+ let jtype fmt js = makeJtype ~names fmt js in
+ Format.fprintf fmt
+ "@[<hov 2>Compare.dictionary<@,Json.dict<'#%s'@,%a>>(@,%a)@]"
+ kd jtype js pp js
+ in pp fmt js
+
(* -------------------------------------------------------------------------- *)
(* --- Declaration Generator --- *)
(* -------------------------------------------------------------------------- *)
@@ -216,8 +259,10 @@ let makeDeclaration fmt names d =
let self = d.d_ident in
let jtype = makeJtype ~self ~names in
match d.d_kind with
+
| D_type js ->
- Format.fprintf fmt "@[<hv 2>export type %s =@ %a;@]@\n" self.name jtype js ;
+ Format.fprintf fmt "@[<hv 2>export type %s =@ %a;@]@\n" self.name jtype js
+
| D_record fjs ->
Format.fprintf fmt "export interface %s {@\n" self.name ;
List.iter
@@ -229,7 +274,8 @@ let makeDeclaration fmt names d =
| _ ->
Format.fprintf fmt " @[<hov 2>%s: %a;@]@\n" fd jtype js
) fjs ;
- Format.fprintf fmt "}@\n" ;
+ Format.fprintf fmt "}@\n"
+
| D_enum tgs ->
Format.fprintf fmt "export enum %s {@\n" self.name ;
List.iter
@@ -237,11 +283,13 @@ let makeDeclaration fmt names d =
makeDescr ~indent:" " fmt doc ;
Format.fprintf fmt " %s = '%s';@\n" tag tag ;
) tgs ;
- Format.fprintf fmt "}@\n" ;
+ Format.fprintf fmt "}@\n"
+
| D_signal ->
Format.fprintf fmt "export const %s: Server.Signal = {@\n" self.name ;
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident d.d_ident) ;
- Format.fprintf fmt "};@\n" ;
+ Format.fprintf fmt "};@\n"
+
| D_request rq ->
let kind = name_of_kind rq.rq_kind in
let prefix = String.capitalize_ascii (String.lowercase_ascii kind) in
@@ -255,7 +303,8 @@ let makeDeclaration fmt names d =
Format.fprintf fmt " name: '%s',@\n" (Pkg.name_of_ident d.d_ident) ;
Format.fprintf fmt " input: %a,@\n" makeParam input ;
Format.fprintf fmt " output: %a,@\n" makeParam output ;
- Format.fprintf fmt "};@\n" ;
+ Format.fprintf fmt "};@\n"
+
| D_value js ->
Format.fprintf fmt
"@[<hov 2>export const %s: State.Value<@,%a@,> = {@]@\n"
@@ -264,7 +313,8 @@ let makeDeclaration fmt names d =
(jcall names) (Pkg.Derived.signal self) ;
Format.fprintf fmt " getter: %a,@\n"
(jcall names) (Pkg.Derived.getter self) ;
- Format.fprintf fmt "};@\n" ;
+ Format.fprintf fmt "};@\n"
+
| D_state js ->
Format.fprintf fmt
"@[<hov 2>export const %s: State.State<@,%a@,> = {@]@\n"
@@ -275,7 +325,8 @@ let makeDeclaration fmt names d =
(jcall names) (Pkg.Derived.getter self) ;
Format.fprintf fmt " setter: %a,@\n"
(jcall names) (Pkg.Derived.setter self) ;
- Format.fprintf fmt "};@\n" ;
+ Format.fprintf fmt "};@\n"
+
| D_array kd ->
let data = Pkg.Derived.data self in
Format.fprintf fmt
@@ -287,18 +338,25 @@ let makeDeclaration fmt names d =
(jcall names) (Pkg.Derived.fetch self) ;
Format.fprintf fmt " reload: %a,@\n"
(jcall names) (Pkg.Derived.reload self) ;
- Format.fprintf fmt "};@\n" ;
+ Format.fprintf fmt "};@\n"
+
| D_safe(id,js) ->
Format.fprintf fmt
"@[<hov 2>export const %s: Json.Safe<@,%a@,> =@ %a;@]\n"
self.name (jcall names) id
- (makeRootDecoder ~safe:true ~self:id ~names) js ;
+ (makeRootDecoder ~safe:true ~self:id ~names) js
+
| D_loose(id,js) ->
Format.fprintf fmt
"@[<hov 2>export const %s: Json.Loose<@,%a@,> =@ %a;@]\n"
self.name (jcall names) id
- (makeRootDecoder ~safe:false ~self:id ~names) js ;
- | D_order _ -> ()
+ (makeRootDecoder ~safe:false ~self:id ~names) js
+
+ | D_order(id,js) ->
+ Format.fprintf fmt
+ "@[<hov 2>export const %s: Compare.Order<@,%a@,> =@ %a;@]\n"
+ self.name (jcall names) id
+ (makeOrder ~self:id ~names) js
(* -------------------------------------------------------------------------- *)
(* --- Package Generator --- *)
@@ -316,7 +374,9 @@ let makePackage pkg name fmt =
Format.fprintf fmt "*/@\n@." ;
let names = Pkg.resolve ~keywords pkg in
Format.fprintf fmt "import * as Json from 'dome/data/json';@\n" ;
+ Format.fprintf fmt "import * as Compare from 'dome/data/compare';@\n" ;
Format.fprintf fmt "import * as Server from 'frama-c/server';@\n" ;
+ Format.fprintf fmt "import * as State from 'frama-c/states';@\n" ;
Format.pp_print_newline fmt () ;
Pkg.IdMap.iter
(fun id name ->
diff --git a/ivette/src/dome/src/renderer/data/compare.ts b/ivette/src/dome/src/renderer/data/compare.ts
index 5f643b4cc85..9419679dd6f 100644
--- a/ivette/src/dome/src/renderer/data/compare.ts
+++ b/ivette/src/dome/src/renderer/data/compare.ts
@@ -131,8 +131,24 @@ export function array<A>(order: Order<A>): Order<A[]> {
};
}
+/** Order by dictionary order.
+ Can be used directly with an enum type declaration.
+ */
+export function byEnum<A extends string>(d: { [key: string]: A }): Order<A> {
+ const ranks: { [index: string]: number } = {};
+ const values = Object.keys(d);
+ const wildcard = values.length;
+ values.forEach((C, k) => ranks[C] = k);
+ return (x: A, y: A) => {
+ if (x === y) return 0;
+ const rx = ranks[x] ?? wildcard;
+ const ry = ranks[y] ?? wildcard;
+ return rx - ry;
+ };
+}
+
/** Order string enumeration constants.
- `enums(v1,...,vN)` will order constant following the order of arguments.
+ `byRank(v1,...,vN)` will order constant following the order of arguments.
Non-listed constants appear at the end, or at the rank specified by `'*'`. */
export function byRank(...args: string[]): Order<string> {
const ranks: { [index: string]: number } = {};
diff --git a/src/plugins/dive/server_interface.ml b/src/plugins/dive/server_interface.ml
index 51f5267c7a9..65179a2d791 100644
--- a/src/plugins/dive/server_interface.ml
+++ b/src/plugins/dive/server_interface.ml
@@ -59,12 +59,12 @@ struct
let fun_field = Data.Record.option signature
~name:"funName"
~descr:(Markdown.plain "owner function for a local variable")
- (module Data.Jstring)
+ (module Data.Jalpha)
let var_field = Data.Record.field signature
~name:"varName"
~descr:(Markdown.plain "variable name")
- (module Data.Jstring)
+ (module Data.Jalpha)
type t = Cil_types.varinfo
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
index 75833d9b461..e6ad81cbbf9 100644
--- a/src/plugins/server/data.ml
+++ b/src/plugins/server/data.ml
@@ -549,8 +549,7 @@ struct
let jtype =
let enums = D_enum (List.rev d.tags) in
let id = Package.declare_id ~package ~name ~descr enums in
- let js = Jenum id in
- derived ~package ~id js ; js
+ derived ~package ~id (Jenum id) ; Jdata id
let of_json = of_json name d.values
let to_json = to_json name d.lookup d.vindex
end in
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
index 6134493c968..6ba578402a2 100644
--- a/src/plugins/server/data.mli
+++ b/src/plugins/server/data.mli
@@ -80,6 +80,7 @@ module Jbool : S with type t = bool
module Jint : S with type t = int
module Jfloat : S with type t = float
module Jstring : S with type t = string
+module Jalpha : S with type t = string
module Jtext : S with type t = json (** Rich text encoding, see [Jbuffer]. *)
module Jmarkdown : S with type t = Markdown.text
diff --git a/src/plugins/server/package.ml b/src/plugins/server/package.ml
index 837861f6bb1..b0361dcbd90 100644
--- a/src/plugins/server/package.ml
+++ b/src/plugins/server/package.ml
@@ -176,7 +176,7 @@ type jtype =
| Junion of jtype list
| Jrecord of (string * jtype) list
| Jdata of ident
- | Jenum of ident (* data that is an enum *)
+ | Jenum of ident (* enum type declaration *)
| Jself (* for (simply) recursive types *)
(* -------------------------------------------------------------------------- *)
--
GitLab