From 2ceb184a483e578efe68370c0874c92fe78b16fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Thu, 27 Feb 2020 12:02:43 +0100 Subject: [PATCH] [server] publish dictionaries and kernel data types --- src/plugins/server/data.ml | 72 +++++++++- src/plugins/server/data.mli | 25 +++- src/plugins/server/kernel_ast.ml | 4 +- src/plugins/server/kernel_main.ml | 180 ++++++++++++------------ src/plugins/server/kernel_properties.ml | 35 +++-- src/plugins/server/request.ml | 17 +++ src/plugins/server/request.mli | 6 + src/plugins/server/syntax.ml | 4 +- src/plugins/server/syntax.mli | 6 +- 9 files changed, 230 insertions(+), 119 deletions(-) diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml index 44d1d3bbc2a..f600d853cb9 100644 --- a/src/plugins/server/data.ml +++ b/src/plugins/server/data.ml @@ -63,6 +63,8 @@ let failure ?json msg = let failure_from_type_error msg json = failure ~json "%s" msg +let page = Doc.page `Kernel ~title:"Kernel Types" ~filename:"data.md" + (* -------------------------------------------------------------------------- *) (* --- Option --- *) (* -------------------------------------------------------------------------- *) @@ -347,19 +349,59 @@ struct end +module Jmarkdown : S with type t = Markdown.text = +struct + + type t = Markdown.text + let syntax = Syntax.publish ~page + ~name:"markdown" ~descr:(Markdown.plain "Markdown (inlined text)") + ~synopsis:Syntax.string () + let of_json js = Markdown.plain (Ju.to_string js) + let to_json txt = + `String (Pretty_utils.to_string (Markdown.pp_text ?page:None) txt) + +end + (* -------------------------------------------------------------------------- *) (* --- Enums --- *) (* -------------------------------------------------------------------------- *) +module Tag = Collection + (struct + type t = Syntax.tag + + let syntax = Syntax.publish ~page ~name:"tag" + ~descr:(Markdown.plain "Tag description") + ~synopsis:(Syntax.record [ + "name",Syntax.string ; + "label",Jmarkdown.syntax ; + "descr",Jmarkdown.syntax ; + ]) () + + let to_json tg = `Assoc [ + "name", `String tg.Syntax.tag_name ; + "label", Jmarkdown.to_json tg.tag_label ; + "descr" , Jmarkdown.to_json tg.tag_descr ; + ] + + let of_json js = Syntax.{ + tag_name = Ju.member "name" js |> Ju.to_string ; + tag_label = Ju.member "label" js |> Jmarkdown.of_json ; + tag_descr = Ju.member "descr" js |> Jmarkdown.of_json ; + } + end) + module Enum = struct type 'a dictionary = { page : Doc.page ; name : string ; + title : string ; descr : Markdown.text ; values : (string,'a option) Hashtbl.t ; vindex : ('a,string) Hashtbl.t ; + mutable syntax : Markdown.text ; mutable published : bool ; mutable tags : Syntax.tag list ; } @@ -367,13 +409,17 @@ struct type 'a tag = string type 'a prefix = string -> 'a tag - let name tg = tg + let tag_name tg = tg + let tag_label a = function + | None -> Markdown.plain (String.(capitalize_ascii (lowercase_ascii a))) + | Some lbl -> lbl - let dictionary ~page ~name ~descr () = { - page ; name ; descr ; + let dictionary ~page ~name ~title ~descr () = { + page ; name ; descr ; title ; published = false ; values = Hashtbl.create 0 ; vindex = Hashtbl.create 0 ; + syntax = [] ; tags = [] ; } @@ -381,12 +427,20 @@ struct let msg = Printf.sprintf "Server.Data.Enum.%s: %s" name reason in raise (Invalid_argument msg) - let tag (d : 'a dictionary) ~name ~descr ?value () : 'a tag = + let page (d : 'a dictionary) = d.page + let name (d : 'a dictionary) = d.name + let syntax (d : 'a dictionary) = d.syntax + + let tag (d : 'a dictionary) ~name ?label ~descr ?value () : 'a tag = if d.published then invalid d.name (Printf.sprintf "published enum (%s)" name) ; if Hashtbl.mem d.values name then invalid d.name (Printf.sprintf "duplicate tag (%s)" name) ; - let tg = Syntax.{ tag_name = name ; tag_descr = descr } in + let tg = Syntax.{ + tag_name = name ; + tag_label = tag_label name label ; + tag_descr = descr ; + } in d.tags <- tg :: d.tags ; Hashtbl.add d.values name value ; begin match value with @@ -394,13 +448,14 @@ struct | Some v -> Hashtbl.add d.vindex v name end ; name - let prefix (d : 'a dictionary) ~prefix ?(var="*") ~descr + let prefix (d : 'a dictionary) ~prefix ?(var="*") ?label ~descr () : string -> 'a tag = if d.published then invalid d.name (Printf.sprintf "published enum (%s:*)" prefix) ; let make = Printf.sprintf "%s:%s" prefix in let tg = Syntax.{ tag_name = make var ; + tag_label = tag_label (prefix ^ ".") label ; tag_descr = descr ; } in d.tags <- tg :: d.tags ; make @@ -419,6 +474,8 @@ struct | exception Not_found -> failure "[%s] Not registered tag '%s" name tag + let tags d = List.rev d.tags + let publish (type a) (d : a dictionary) ?tag () = if d.published then invalid d.name "already published" ; @@ -427,7 +484,7 @@ struct type t = a let descr = d.descr let syntax = - let tags = Syntax.tags ~title:"Tag" (List.rev d.tags) in + let tags = Syntax.tags ~title:d.title (List.rev d.tags) in Syntax.publish ~page:d.page ~name:d.name ~descr ~synopsis:(Syntax.string) ~details:[tags] () @@ -439,6 +496,7 @@ struct end in begin d.published <- true ; + d.syntax <- Syntax.text M.syntax ; (module M : S with type t = a) end diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli index 6950b98de51..3297d75cbda 100644 --- a/src/plugins/server/data.mli +++ b/src/plugins/server/data.mli @@ -26,6 +26,7 @@ type json = Json.t +val page : Doc.page (** Page for builtin kernel data types *) val pretty : Format.formatter -> json -> unit module type S = @@ -89,6 +90,7 @@ module Jfloat : S_collection with type t = float module Jstring : S_collection with type t = string module Jident : S_collection with type t = string (** Syntax is {i ident}. *) module Jtext : S with type t = json (** Rich text encoding, see [Jbuffer] *) +module Jmarkdown : S with type t = Markdown.text (* -------------------------------------------------------------------------- *) (** {2 Records} *) @@ -158,6 +160,8 @@ end (** {2 Enums} *) (* -------------------------------------------------------------------------- *) +module Tag : S_collection with type t = Syntax.tag + (** Enum factory. You shall start by declaring a dictionnary with @@ -185,29 +189,42 @@ sig type 'a tag type 'a prefix = string -> 'a tag - val name : 'a tag -> string + val tag_name : 'a tag -> string (** Creates an opened, empty dictionnary. *) val dictionary : - page:Doc.page -> name:string -> descr:Markdown.text -> + page:Doc.page -> name:string -> title:string -> descr:Markdown.text -> unit -> 'a dictionary (** Register a new tag in the dictionnary. + The default label is the capitalized name. The provided value, if any, will be used for decoding json tags. If would be used also for encoding values to json tags if no [~tag] function is provided when publishing the dictionnary. Registered values must be hashable with [Hashtbl.hash] function. *) val tag : 'a dictionary -> - name:string -> descr:Markdown.text -> ?value:'a -> + name:string -> + ?label:Markdown.text -> descr:Markdown.text -> + ?value:'a -> unit -> 'a tag (** Register a new prefix tag in the dictionnary. + The default label is the capitalized prefix. To decoding from json is provided to prefix tags. Encoding is done by emitting tags with form ['prefix:*']. The variable part of the prefix is documented as ['prefix:xxx'] when [~var:"xxx"] is provided. *) val prefix : 'a dictionary -> - prefix:string -> ?var:string -> descr:Markdown.text -> unit -> 'a prefix + prefix:string -> ?var:string -> + ?label:Markdown.text -> descr:Markdown.text -> + unit -> 'a prefix + + (** Obtain all the tags from the dictionnary. *) + val tags : 'a dictionary -> Tag.t list + + val page : 'a dictionary -> Doc.page + val name : 'a dictionary -> string + val syntax : 'a dictionary -> Markdown.text (** Publish the dictionnary. To more tag nor prefix can be added after. If no [~tag] function is provided, registered values with tags diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml index 3861b8cfc8e..2c68bdbac36 100644 --- a/src/plugins/server/kernel_ast.ml +++ b/src/plugins/server/kernel_ast.ml @@ -102,7 +102,7 @@ module PP = Printer_tag.Make(Tag) module Stmt = Data.Collection (struct type t = stmt - let syntax = Sy.publish ~page ~name:"stmt" + let syntax = Sy.publish ~page:Data.page ~name:"stmt" ~synopsis:Sy.ident ~descr:(Md.plain "Code statement identifier") () let to_json st = `String (Tag.of_stmt st) @@ -132,7 +132,7 @@ module Ki = Data.Collection module Kf = Data.Collection (struct type t = kernel_function - let syntax = Sy.publish ~page ~name:"fct-id" + let syntax = Sy.publish ~page:Data.page ~name:"fct-id" ~synopsis:Sy.ident ~descr:(Md.plain "Function identified by its global name.") () let to_json kf = diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml index 28e9a6574f0..67ec006f68b 100644 --- a/src/plugins/server/kernel_main.ml +++ b/src/plugins/server/kernel_main.ml @@ -78,118 +78,114 @@ let () = (* --- File Positions --- *) (* -------------------------------------------------------------------------- *) -module RawSource = -struct - type t = Filepath.position - - let syntax = Sy.publish ~page ~name:"source" - ~synopsis:(Sy.record [ "file" , Sy.string ; "line" , Sy.int ]) - ~descr:(Md.plain "Source file positions.") - ~details:Md.([Block [Text (plain "The file path is normalized, \ - and the line number starts at one.")]]) - () +module LogSource = Collection + (struct + type t = Filepath.position - let to_json p = `Assoc [ - "file" , `String (p.Filepath.pos_path :> string) ; - "line" , `Int p.Filepath.pos_lnum ; - ] + let syntax = Sy.publish ~page:Data.page ~name:"source" + ~synopsis:(Sy.record [ "file" , Sy.string ; "line" , Sy.int ]) + ~descr:(Md.plain "Source file positions.") + ~details:Md.([Block [Text (plain "The file path is normalized, \ + and the line number starts at one.")]]) + () - let of_json = function - | `Assoc [ "file" , `String path ; "line" , `Int line ] - | `Assoc [ "line" , `Int line ; "file" , `String path ] - -> Log.source ~file:(Filepath.Normalized.of_string path) ~line - | js -> failure_from_type_error "Invalid source format" js + let to_json p = `Assoc [ + "file" , `String (p.Filepath.pos_path :> string) ; + "line" , `Int p.Filepath.pos_lnum ; + ] -end + let of_json = function + | `Assoc [ "file" , `String path ; "line" , `Int line ] + | `Assoc [ "line" , `Int line ; "file" , `String path ] + -> Log.source ~file:(Filepath.Normalized.of_string path) ~line + | js -> failure_from_type_error "Invalid source format" js -module LogSource = Collection(RawSource) + end) (* -------------------------------------------------------------------------- *) (* --- Log Lind --- *) (* -------------------------------------------------------------------------- *) -module RawKind = -struct - let kinds = Enum.dictionary ~page - ~name:"kind" - ~descr:(Md.plain "Frama-C message category.") - () +module LogKind = Collection + (struct - let t_kind value name descr = - Enum.tag kinds ~name ~descr:(Md.plain descr) ~value () + let kinds = Enum.dictionary ~page + ~name:"logkind" ~title:"Log Kind" + ~descr:(Md.plain "Frama-C message category.") + () - let t_error = t_kind Log.Error "ERROR" "User Error" - let t_warning = t_kind Log.Warning "WARNING" "User Warning" - let t_feedback = t_kind Log.Feedback "FEEDBACK" "Plugin Feedback" - let t_result = t_kind Log.Result "RESULT" "Plugin Result" - let t_failure = t_kind Log.Failure "FAILURE" "Plugin Failure" - let t_debug = t_kind Log.Debug "DEBUG" "Analyser Debug" + let t_kind value name descr = + Enum.tag kinds ~name ~descr:(Md.plain descr) ~value () - let tag = function - | Log.Error -> t_error - | Log.Warning -> t_warning - | Log.Feedback -> t_feedback - | Log.Result -> t_result - | Log.Failure -> t_failure - | Log.Debug -> t_debug + let t_error = t_kind Log.Error "ERROR" "User Error" + let t_warning = t_kind Log.Warning "WARNING" "User Warning" + let t_feedback = t_kind Log.Feedback "FEEDBACK" "Plugin Feedback" + let t_result = t_kind Log.Result "RESULT" "Plugin Result" + let t_failure = t_kind Log.Failure "FAILURE" "Plugin Failure" + let t_debug = t_kind Log.Debug "DEBUG" "Analyser Debug" - let data = Enum.publish kinds ~tag () + let tag = function + | Log.Error -> t_error + | Log.Warning -> t_warning + | Log.Feedback -> t_feedback + | Log.Result -> t_result + | Log.Failure -> t_failure + | Log.Debug -> t_debug - include (val data : S with type t = Log.kind) -end + let data = Enum.publish kinds ~tag () + let () = Request.dictionary kinds -module LogKind = Collection(RawKind) + include (val data : S with type t = Log.kind) + end) (* -------------------------------------------------------------------------- *) (* --- Log Events --- *) (* -------------------------------------------------------------------------- *) -module RawEvent = -struct - - type rlog - - let jlog : rlog Record.signature = Record.signature ~page - ~name:"log" ~descr:(Md.plain "Message event record.") () - - let kind = Record.field jlog ~name:"kind" - ~descr:(Md.plain "Message kind") (module LogKind) - let plugin = Record.field jlog ~name:"plugin" - ~descr:(Md.plain "Emitter plugin") (module Jstring) - let message = Record.field jlog ~name:"message" - ~descr:(Md.plain "Message text") (module Jstring) - let category = Record.option jlog ~name:"category" - ~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring) - let source = Record.option jlog ~name:"source" - ~descr:(Md.plain "Source file position") (module LogSource) - - module R = (val (Record.publish jlog) : Record.S with type r = rlog) - - type t = Log.event - let syntax = R.syntax - - let to_json evt = - R.default |> - R.set plugin evt.Log.evt_plugin |> - R.set kind evt.Log.evt_kind |> - R.set category evt.Log.evt_category |> - R.set source evt.Log.evt_source |> - R.set message evt.Log.evt_message |> - R.to_json - - let of_json js = - let r = R.of_json js in - { - Log.evt_plugin = R.get plugin r ; - Log.evt_kind = R.get kind r ; - Log.evt_category = R.get category r ; - Log.evt_source = R.get source r ; - Log.evt_message = R.get message r ; - } - -end - -module LogEvent = Collection(RawEvent) +module LogEvent = Collection + (struct + + type rlog + + let jlog : rlog Record.signature = Record.signature ~page + ~name:"log" ~descr:(Md.plain "Message event record.") () + + let kind = Record.field jlog ~name:"kind" + ~descr:(Md.plain "Message kind") (module LogKind) + let plugin = Record.field jlog ~name:"plugin" + ~descr:(Md.plain "Emitter plugin") (module Jstring) + let message = Record.field jlog ~name:"message" + ~descr:(Md.plain "Message text") (module Jstring) + let category = Record.option jlog ~name:"category" + ~descr:(Md.plain "Message category (DEBUG or WARNING)") (module Jstring) + let source = Record.option jlog ~name:"source" + ~descr:(Md.plain "Source file position") (module LogSource) + + module R = (val (Record.publish jlog) : Record.S with type r = rlog) + + type t = Log.event + let syntax = R.syntax + + let to_json evt = + R.default |> + R.set plugin evt.Log.evt_plugin |> + R.set kind evt.Log.evt_kind |> + R.set category evt.Log.evt_category |> + R.set source evt.Log.evt_source |> + R.set message evt.Log.evt_message |> + R.to_json + + let of_json js = + let r = R.of_json js in + { + Log.evt_plugin = R.get plugin r ; + Log.evt_kind = R.get kind r ; + Log.evt_category = R.get category r ; + Log.evt_source = R.get source r ; + Log.evt_message = R.get message r ; + } + + end) (* -------------------------------------------------------------------------- *) (* --- Log Monitoring --- *) diff --git a/src/plugins/server/kernel_properties.ml b/src/plugins/server/kernel_properties.ml index fe71601a655..46e46b0f250 100644 --- a/src/plugins/server/kernel_properties.ml +++ b/src/plugins/server/kernel_properties.ml @@ -37,7 +37,7 @@ let page = Doc.page `Kernel ~title:"Property Services" ~filename:"properties.md" module PropKind = struct let kinds = Enum.dictionary ~page - ~name:"propkind" + ~name:"propkind" ~title:"Kind" ~descr:(Md.plain "Property Kind") () @@ -129,8 +129,8 @@ struct | IPGlobalInvariant _ -> t_global_invariant | IPOther { io_name } -> t_other io_name - let data = Enum.publish kinds ~tag () + let () = Request.dictionary kinds include (val data : S with type t = Property.t) end @@ -142,36 +142,46 @@ end module PropStatus = struct - let status = Enum.dictionary ~page ~name:"status" + let status = Enum.dictionary ~page + ~name:"propstatus" ~title:"Status" ~descr:(Md.plain "Property Status (consolidated)") () - let t_status value name descr = - Enum.tag status ~name ~descr:(Md.plain descr) ~value () + let t_status value name ?label descr = + Enum.tag status ~name + ?label:(Extlib.opt_map Md.plain label) + ~descr:(Md.plain descr) ~value () open Property_status.Feedback let t_unknown = t_status Unknown "unknown" "Unknown status" let t_never_tried = - t_status Never_tried "never-tried" "Unknown status (never tried)" + t_status Never_tried "never_tried" + ~label:"Never tried" "Unknown status (never tried)" let t_inconsistent = t_status Inconsistent "inconsistent" "Inconsistent status" let t_valid = t_status Valid "valid" "Valid property" let t_valid_under_hyp = - t_status Valid_under_hyp "valid_under_hyp" "Valid (under hypotheses)" + t_status Valid_under_hyp "valid_under_hyp" + ~label:"Valid(?)" "Valid (under hypotheses)" let t_considered_valid = - t_status Considered_valid "considered_valid" "Valid (external assumption)" + t_status Considered_valid "considered_valid" + ~label:"Valid(!)" "Valid (external assumption)" let t_invalid = t_status Invalid "invalid" "Invalid property (counter example found)" let t_invalid_under_hyp = - t_status Invalid_under_hyp "invalid_under_hyp" "Invalid property (under hypotheses)" + t_status Invalid_under_hyp "invalid_under_hyp" + ~label:"Invalid(?)" "Invalid property (under hypotheses)" let t_invalid_but_dead = - t_status Invalid_but_dead "invalid_but_dead" "Dead property (but invalid)" + t_status Invalid_but_dead "invalid_but_dead" + ~label:"Invalid(âœ)" "Dead property (but invalid)" let t_valid_but_dead = - t_status Valid_but_dead "valid_but_dead" "Dead property (but valid)" + t_status Valid_but_dead "valid_but_dead" + ~label:"Valid(âœ)" "Dead property (but valid)" let t_unknown_but_dead = - t_status Unknown_but_dead "unknown_but_dead" "Dead property (but unknown)" + t_status Unknown_but_dead "unknown_but_dead" + ~label:"Unknown(âœ)" "Dead property (but unknown)" let tag = function | Valid -> t_valid @@ -187,6 +197,7 @@ struct | Inconsistent -> t_inconsistent let data = Enum.publish status ~tag () + let () = Request.dictionary status include (val data : S with type t = Property_status.Feedback.t) end diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml index ebd45441bbc..51c2eb26c90 100644 --- a/src/plugins/server/request.ml +++ b/src/plugins/server/request.ml @@ -81,6 +81,12 @@ let check_page page name = Senv.warning ~wkey:wkind "Request '%s' shall not be published in protocol pages" name +let page_prefix page = + match Doc.chapter page with + | `Kernel -> "kernel" + | `Plugin plugin -> plugin + | `Protocol -> "protocol" + (* -------------------------------------------------------------------------- *) (* --- Signals --- *) (* -------------------------------------------------------------------------- *) @@ -359,4 +365,15 @@ let register ~page ~kind ~name ~descr ?details ~input ~output process = (signature ~page ~kind ~name ~descr ?details ~input ~output ()) (fun _rq v -> process v) +let dictionary (d : 'a Data.Enum.dictionary) = + let name = Data.Enum.name d in + let page = Data.Enum.page d in + let descr = Markdown.plain "Returns all tags registered for" @ + Data.Enum.syntax d in + register ~kind:`GET ~page + ~name:(Printf.sprintf "%s.dictionary.%s" (page_prefix page) name) ~descr + ~input:(module Data.Junit) + ~output:(module Data.Tag.Jlist) + (fun () -> Data.Enum.tags d) + (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/request.mli b/src/plugins/server/request.mli index 14e1a565476..dbe3f5e133c 100644 --- a/src/plugins/server/request.mli +++ b/src/plugins/server/request.mli @@ -211,4 +211,10 @@ val result_opt : ('a,unit) signature -> descr:Markdown.text -> 'b output -> 'b option result +(** {2 Exporting Dictionaries} *) + +(** Register a [GET] request [dictionary.<name>] to retrieve all tags + registered in the dictionary. *) +val dictionary : 'a Data.Enum.dictionary -> unit + (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml index 7c7a4778f4b..79ccfcbde3a 100644 --- a/src/plugins/server/syntax.ml +++ b/src/plugins/server/syntax.ml @@ -107,6 +107,7 @@ let option t = atom @@ Markdown.(protect t @ code "?") type tag = { tag_name : string ; + tag_label : Markdown.text ; tag_descr : Markdown.text ; } @@ -114,9 +115,10 @@ let tags ?(title="Tag") (tgs : tag list) = let open Markdown in let header = [ plain title, Left; + plain "Value", Left; plain "Description", Left ] in - let row tg = [ escaped tg.tag_name ; tg.tag_descr ] in + let row tg = [ tg.tag_label ; escaped tg.tag_name ; tg.tag_descr ] in Markdown.Table { caption = None ; header ; content = List.map row tgs ; } diff --git a/src/plugins/server/syntax.mli b/src/plugins/server/syntax.mli index b5f0367df2d..c9ac038bfc8 100644 --- a/src/plugins/server/syntax.mli +++ b/src/plugins/server/syntax.mli @@ -51,7 +51,11 @@ val option : t -> t val record : (string * t) list -> t val data : string -> Markdown.href -> t -type tag = { tag_name : string ; tag_descr : Markdown.text } +type tag = { + tag_name : string ; + tag_label : Markdown.text ; + tag_descr : Markdown.text ; +} (** Builds a table with tags description. The [~title] is applied to the tag name column -- GitLab