diff --git a/.Makefile.lint b/.Makefile.lint
index ecae11caedaf5711a2d0241b5a76796b47daffe0..7d18f22eed17986328f25354182e7a0ccd4fb06a 100644
--- a/.Makefile.lint
+++ b/.Makefile.lint
@@ -81,17 +81,6 @@ ML_LINT_KO+=src/kernel_services/ast_data/ast.mli
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.ml
ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.mli
ML_LINT_KO+=src/kernel_services/ast_data/property_status.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/cabs_debug.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_descriptive_printer.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_printer.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/cil_types_debug.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/cprint.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/cprint.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/logic_print.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/printer.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/printer_api.mli
-ML_LINT_KO+=src/kernel_services/ast_printing/printer_builder.ml
-ML_LINT_KO+=src/kernel_services/ast_printing/printer_builder.mli
ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.ml
ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.mli
ML_LINT_KO+=src/kernel_services/ast_queries/cil.mli
diff --git a/.gitignore b/.gitignore
index 633a7d72b4f6a96980eec0d1d508467a17ddfa92..0e333030f4d2f99767fd4ca245b5c91ccbfd7f55 100644
--- a/.gitignore
+++ b/.gitignore
@@ -66,6 +66,7 @@ autom4te.cache
/share/manuals/
#doc
+
/doc/manuals/
/doc/*/*.dot
/doc/*/*.aux
@@ -137,6 +138,8 @@ autom4te.cache
/doc/pdg/pdg00*.png
/doc/pdg/previous_motif.gif
+/doc/server/
+
#lib
/lib/fc/
/lib/plugins/*.mli
diff --git a/Makefile b/Makefile
index a2f6ecef224d5acb8fb13fb8f3a5a9abda75da13..43c11ae3d2657d51b590cd0944d0d2d696344025 100644
--- a/Makefile
+++ b/Makefile
@@ -84,6 +84,7 @@ PLUGIN_BIN_DOC_LIST:=
PLUGIN_DIST_EXTERNAL_LIST:=
PLUGIN_DIST_TESTS_LIST:=
PLUGIN_DISTRIBUTED_NAME_LIST:=
+MERLIN_PACKAGES:=
PLUGIN_HEADER_SPEC_LIST :=
PLUGIN_HEADER_DIRS_LIST :=
@@ -451,6 +452,7 @@ LIB_CMO =\
src/libraries/utils/leftistheap \
src/libraries/stdlib/integer \
src/libraries/utils/json \
+ src/libraries/utils/markdown \
src/libraries/utils/rich_text \
src/libraries/utils/dotgraph
@@ -1511,6 +1513,28 @@ plugins-doc:
$(addsuffix _DOC,$(PLUGIN_DISTRIBUTED_NAME_LIST)),\
$(PLUGIN_DOC_LIST)))
+.PHONY: server-doc-md server-doc-html server-doc
+
+server-doc-md: byte
+ $(PRINT) 'Generating Markdown server documentation'
+ @rm -fr doc/server
+ @mkdir -p doc/server
+ ./bin/frama-c.byte -server-doc doc/server
+
+server-doc-html: server-doc-md
+ $(PRINT) 'Generating HTML server documentation'
+ @find doc/server -name "*.md" -print -exec pandoc \
+ --standalone --toc --toc-depth=2 --to html \
+ --template doc/pandoc/template.html \
+ --metadata-file {}.json \
+ --lua-filter doc/pandoc/href.lua \
+ {} -o {}.html \;
+ @cp -f doc/pandoc/style.css doc/server/
+ $(PRINT) 'HTML server documentation ready:'
+ $(PRINT) ' open doc/server/readme.md.html'
+
+server-doc: server-doc-html
+
# to make the documentation for one plugin only,
# the name of the plugin should begin with a capital letter :
# Example for the pdg doc : make Pdg_DOC
diff --git a/doc/code/.gitignore b/doc/code/.gitignore
index b7720446464e2b86180a469acd76669aa411012f..d215811ad788d24a80392ce042fe246711ae33ff 100644
--- a/doc/code/.gitignore
+++ b/doc/code/.gitignore
@@ -33,3 +33,4 @@
/value/
/variadic/
/wp/
+/server/
diff --git a/doc/pandoc/href.lua b/doc/pandoc/href.lua
new file mode 100644
index 0000000000000000000000000000000000000000..080635d1533c0aee541b0c4b85bb8917b80bcd74
--- /dev/null
+++ b/doc/pandoc/href.lua
@@ -0,0 +1,4 @@
+function Link(el)
+ el.target = string.gsub(el.target, "%.md", ".md.html")
+ return el
+end
diff --git a/doc/pandoc/style.css b/doc/pandoc/style.css
new file mode 100644
index 0000000000000000000000000000000000000000..ba609d558f7bdb1b4936cfd8fcf9520199602f46
--- /dev/null
+++ b/doc/pandoc/style.css
@@ -0,0 +1,224 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2018 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+* { margin: 0; padding: 0 }
+
+html
+{
+ background-color: #fff;
+}
+
+* { margin: 0; padding: 0 }
+
+body {
+ position: absolute;
+ color: #222;
+ width: 100%;
+ height: 100%;
+ overflow: hidden;
+ font-family: "Verdana", sans;
+ font-size: 12pt;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Headers --- */
+/* -------------------------------------------------------------------------- */
+
+#BODY {
+ display: flex ;
+ flex-flow: row nowrap ;
+ width: 100% ;
+ height: 100% ;
+ overflow: hidden ;
+}
+
+#NAVIGATION {
+ display: block ;
+ overflow: auto ;
+ flex: 0 1 auto ;
+ order: 1 ;
+ box-sizing: border-box ;
+ min-width: 3cm ;
+ max-width: 8cm ;
+ height: 100% ;
+ padding: 0cm 0.5cm 0cm 0.5cm ;
+ background: #888 ;
+}
+
+#CONTENT {
+ display: block ;
+ overflow: auto ;
+ flex: 1 1 auto ;
+ order: 2 ;
+ justify-content: left ;
+ align-content: center ;
+ box-sizing: border-box ;
+ width: 18cm ;
+ height: 100% ;
+ padding: 0cm 1cm 1cm 1cm ;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Navigation --- */
+/* -------------------------------------------------------------------------- */
+
+#TOC {
+ font-size: smaller ;
+}
+
+#NAVIGATION a.root {
+ display: block;
+ font-family: "Optima", "Verdana", "Arial", sans;
+ font-size: 16pt;
+ margin-top: 1cm;
+ margin-bottom: 6mm;
+}
+
+#NAVIGATION a.chapter {
+ display: block ;
+ margin-left: 0px;
+ margin-top: 10px;
+ margin-bottom: 10px;
+}
+
+#NAVIGATION a:hover {
+ background-color: darkorange ;
+}
+
+#NAVIGATION a {
+ color: white ;
+}
+
+#NAVIGATION code {
+ color: black ;
+}
+
+#NAVIGATION ul {
+ width: 6cm ;
+}
+
+#NAVIGATION ul > ul {
+ margin-left: 0px ;
+ padding-top: 2px ;
+ padding-bottom: 2px ;
+ background-color: darkgrey ;
+}
+
+/* -------------------------------------------------------------------------- */
+/* --- Headers --- */
+/* -------------------------------------------------------------------------- */
+
+h1 {
+ width: 18cm;
+ font-family: "Optima", "Verdana", "Arial", sans;
+ text-align: left;
+ margin-top: 1cm;
+ margin-bottom: 6mm;
+ padding-left: 3mm;
+ border-left: 20px solid red;
+}
+
+h2 {
+ width: 18cm;
+ font-family: "Optima", "Verdana", "Arial", sans;
+ margin-top: 5mm;
+ margin-bottom: 2mm;
+ border-bottom: solid thin darkred ;
+ color: darkred;
+}
+
+h3 {
+ width: 17cm;
+ font-family: "Optima", "Verdana", "Arial", sans;
+ color: black;
+ margin-top: 5mm;
+ margin-bottom: 3mm;
+ border-bottom: thin solid #404040;
+}
+
+h4,h5,h6 {
+ margin-left: 4mm;
+ margin-top: 4mm;
+ margin-bottom: 1mm;
+ font-family: "Optima", "Verdana", "Arial", sans;
+ font-size: 10pt;
+ font-style: italic;
+ font-weight: bold;
+ color: darkred;
+}
+
+p { margin: 6px 0px 6px 0px; width: 15cm; }
+
+ul,ol,blockquote {
+ margin-left: 24px ;
+ width: 13cm;
+}
+
+li {
+ padding-left: 6px ;
+ padding-right : 6px ;
+}
+
+pre {
+ width : 15cm ;
+ background-color: #eef ;
+}
+
+pre,code { font-size: smaller ; color: #106000 }
+
+hr {
+ border: none ;
+ border-top: 1px solid #404040 ;
+ margin-top: 4mm ;
+ margin-bottom: 4mm ;
+}
+
+table {
+ border-collapse: collapse ;
+ margin-left: 6mm ;
+}
+
+th,td {
+ padding: 2px 16px 2px 12px ;
+}
+
+thead {
+ border-bottom: thin solid gray ;
+}
+
+tr.odd {
+ background-color: rgba(178, 222, 236, 0.3) ;
+}
+
+:target { background-color: darkorange; }
+
+a:visited { color: darkred; text-decoration: none }
+a:link { color: darkred; text-decoration: none }
+a:hover { background-color: lightgray; color: firebrick }
+a:active { background-color: lightgray; color: darkgreen }
+
+a:visited em { color: darkgreen; text-decoration: none }
+a:link em { color: darkgreen; text-decoration: none }
+a:hover em { background-color: lightgray; color: firebrick }
+a:active em { background-color: lightgray; color: darkgreen }
+
+/* -------------------------------------------------------------------------- */
diff --git a/doc/pandoc/template.html b/doc/pandoc/template.html
new file mode 100644
index 0000000000000000000000000000000000000000..e6871d568e832f49fc1bcaadb8171df7a7f47b0b
--- /dev/null
+++ b/doc/pandoc/template.html
@@ -0,0 +1,47 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml" lang="$lang$" xml:lang="$lang$"$if(dir)$ dir="$dir$"$endif$>
+<head>
+ <meta charset="utf-8" />
+ <meta name="generator" content="pandoc" />
+ <meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
+ <title>$if(document)$$document$ – $endif$$title$</title>
+ <link rel="stylesheet" href="$root$/style.css" />
+ <!--[if lt IE 9]>
+ <script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
+ <![endif]-->
+</head>
+<body>
+ <div id="BODY">
+ <div id="NAVIGATION">
+ <nav id="TOC">
+ <a class="root" href="$root$/readme.md.html">$document$</a>
+ $if(chapter)$
+ <a class="chapter" href="$page$">$chapter$</a>
+ $endif$
+ $if(link)$
+ <ul>
+ $if(toc)$
+ $for(link)$
+ $if(link.toc)$
+ $table-of-contents$
+ $else$
+ <li><a href="$link.href$.html">$link.title$</a></li>
+ $endif$
+ $endfor$
+ $else$
+ $for(link)$
+ <li><a href="$link.href$.html">$link.title$</a></li>
+ $endfor$
+ $endif$
+ </ul>
+ $else$
+ $table-of-contents$
+ $endif$
+ </nav>
+ </div>
+ <div id="CONTENT">
+ $body$
+ </div>
+ </div>
+</body>
+</html>
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index eddf3001da28a29bd80934dc1b513c19c84a1c73..ec689685fd2bca4b2d4bbccc5c6a0a52487960c1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -667,6 +667,8 @@ src/libraries/utils/indexer.ml: CEA_LGPL
src/libraries/utils/indexer.mli: CEA_LGPL
src/libraries/utils/leftistheap.ml: JCF_LGPL
src/libraries/utils/leftistheap.mli: JCF_LGPL
+src/libraries/utils/markdown.ml: CEA_LGPL
+src/libraries/utils/markdown.mli: CEA_LGPL
src/libraries/utils/pretty_utils.ml: CEA_LGPL
src/libraries/utils/pretty_utils.mli: CEA_LGPL
src/libraries/utils/qstack.ml: CEA_LGPL
@@ -1025,6 +1027,32 @@ src/plugins/rte/rte.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/rte.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/visit.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/visit.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/.gitignore: .ignore
+src/plugins/server/Makefile.in: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/Server.mli: .ignore
+src/plugins/server/configure.ac: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/data.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/data.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/doc.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/doc.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/jbuffer.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/jbuffer.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_ast.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_ast.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_main.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_main.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_project.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/kernel_project.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/main.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/main.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/request.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/request.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_parameters.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_parameters.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_batch.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_zmq.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/syntax.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/syntax.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/Scope.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/datascope.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/datascope.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/libraries/utils/markdown.ml b/src/libraries/utils/markdown.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0295d8007b6588eac586be4811bc619ef65947d2
--- /dev/null
+++ b/src/libraries/utils/markdown.ml
@@ -0,0 +1,333 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Markdown Documentation Generation Utility --- *)
+(* -------------------------------------------------------------------------- *)
+
+type md = Format.formatter -> unit
+type text = md
+type block = md
+type section = md
+
+let pretty fmt w = w fmt
+let pp_text = pretty
+let pp_block = pretty
+let pp_section = pretty
+
+(* -------------------------------------------------------------------------- *)
+(* --- Context --- *)
+(* -------------------------------------------------------------------------- *)
+
+type toc = level:int -> name:string -> title:string -> unit
+
+type context = {
+ page: string ;
+ path: string list ;
+ names: bool ;
+ level: int ;
+ toc: toc option ;
+}
+
+let context = ref {
+ page = "" ;
+ path = [] ;
+ names = false ;
+ level = 0 ;
+ toc = None ;
+ }
+
+let local ctxt job data =
+ let current = !context in
+ try context := ctxt ; job data ; context := current
+ with err -> context := current ; raise err
+
+(* -------------------------------------------------------------------------- *)
+(* --- Combinators --- *)
+(* -------------------------------------------------------------------------- *)
+
+let nil _fmt = ()
+let empty= nil
+let space fmt = Format.pp_print_space fmt ()
+let newline fmt = Format.pp_print_newline fmt ()
+
+let merge sep ds fmt =
+ match List.filter (fun d -> d != nil) ds with
+ | [] -> ()
+ | d::ds -> d fmt ; List.iter (fun d -> sep fmt ; d fmt) ds
+
+let glue ?sep ds fmt =
+ match sep with
+ | None -> List.iter (fun d -> d fmt) ds
+ | Some s -> merge s ds fmt
+
+let (<@>) a b =
+ if a == empty then b else
+ if b == empty then a else
+ fun fmt -> a fmt ; b fmt
+
+let (<+>) a b =
+ if a == empty then b else
+ if b == empty then a else
+ fun fmt -> a fmt ; space fmt ; b fmt
+
+let (</>) a b =
+ if a == empty then b else
+ if b == empty then a else
+ fun fmt -> a fmt ; newline fmt ; b fmt
+
+let fmt_text k fmt = Format.fprintf fmt "@[<h 0>%t@]" k
+let fmt_block k fmt = Format.fprintf fmt "@[<v 0>%t@]@\n" k
+
+(* -------------------------------------------------------------------------- *)
+(* --- Elementary Text --- *)
+(* -------------------------------------------------------------------------- *)
+
+let raw s fmt = Format.pp_print_string fmt s
+let rm s fmt = Format.pp_print_string fmt s
+let it s fmt = Format.fprintf fmt "_%s_" s
+let bf s fmt = Format.fprintf fmt "**%s**" s
+let tt s fmt = Format.fprintf fmt "`%s`" s
+let text = merge space
+let praw s = fmt_block (raw s)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Links --- *)
+(* -------------------------------------------------------------------------- *)
+
+type href = [
+ | `URL of string
+ | `Page of string
+ | `Name of string
+ | `Section of string * string
+]
+
+let filepath m = String.split_on_char '/' m
+
+let rec relative source target =
+ match source , target with
+ | p::ps , q::qs when p = q -> relative ps qs
+ | [] , _ -> target
+ | _::d , _ -> List.map (fun _ -> "..") d @ target
+
+let lnk target =
+ String.concat "/" (relative !context.path (filepath target))
+
+let id m =
+ let buffer = Buffer.create (String.length m) in
+ let lowercase = Char.lowercase_ascii in
+ let dash = ref false in
+ let emit c =
+ if !dash then (Buffer.add_char buffer '-' ; dash := false) ;
+ Buffer.add_char buffer c in
+ String.iter
+ (function
+ | '0'..'9' as c -> emit c
+ | 'a'..'z' as c -> emit c
+ | 'A'..'Z' as c -> emit (lowercase c)
+ | '.' | '_' as c -> emit c
+ | ' ' | '\t' | '\n' | '-' -> dash := (Buffer.length buffer > 0)
+ | _ -> ()) m ;
+ Buffer.contents buffer
+
+let href ?title (h : href) fmt =
+ match title , h with
+ | None , `URL url -> Format.fprintf fmt "%s" url
+ | Some w , `URL url -> Format.fprintf fmt "[%s](%s)" w url
+ | None , `Page p -> Format.fprintf fmt "[%s](%s)" p (lnk p)
+ | Some w , `Page p -> Format.fprintf fmt "[%s](%s)" w (lnk p)
+ | None , `Section(p,s) -> Format.fprintf fmt "[%s](%s#%s)" s (lnk p) (id s)
+ | Some w , `Section(p,s) -> Format.fprintf fmt "[%s](%s#%s)" w (lnk p) (id s)
+ | None , `Name a -> Format.fprintf fmt "[%s](#%s)" a (id a)
+ | Some w , `Name a -> Format.fprintf fmt "[%s](#%s)" w (id a)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Blocks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let aname anchor fmt =
+ Format.fprintf fmt "<a name=\"%s\"></a>@\n" (id anchor)
+
+let title h ?name title fmt =
+ begin
+ let { level ; names ; toc } = !context in
+ let level = max 0 (min 5 (level + h - 1)) in
+ Format.fprintf fmt "%s %s" (String.make level '#') title ;
+ if names || name <> None || toc <> None then
+ begin
+ let anchor = match name with None -> title | Some a -> a in
+ Format.fprintf fmt " {#%s}" (id anchor) ;
+ (match toc with
+ | None -> ()
+ | Some callback ->
+ callback ~level ~name:anchor ~title) ;
+ end ;
+ Format.pp_print_newline fmt () ;
+ end
+
+let h1 = title 1
+let h2 = title 2
+let h3 = title 3
+let h4 = title 4
+
+let indent h w fmt = local { !context with level = !context.level + h } w fmt
+
+let in_h1 = indent 1
+let in_h2 = indent 2
+let in_h3 = indent 3
+let in_h4 = indent 4
+
+let hrule fmt = Format.pp_print_string fmt "-------------------------@."
+
+let par w fmt = Format.fprintf fmt "@[<hov 0>%t@]@." w
+
+let list ws fmt =
+ List.iter
+ (fun w -> Format.fprintf fmt "@[<hov 2>- %t@]@." w) ws
+
+let enum ws fmt =
+ let k = ref 0 in
+ List.iter
+ (fun w -> incr k ; Format.fprintf fmt "@[<hov 3>%d. %t@]@." !k w) ws
+
+let description items fmt =
+ List.iter
+ (fun (a,w) -> Format.fprintf fmt "@[<hov 2>- **%s** %t@]@." a w) items
+
+let code ?(lang="") pp fmt =
+ begin
+ Format.fprintf fmt "@[<v 0>```%s" lang ;
+ let buffer = Buffer.create 80 in
+ let bfmt = Format.formatter_of_buffer buffer in
+ pp bfmt ; Format.pp_print_flush bfmt () ;
+ let content = Buffer.contents buffer in
+ let lines = String.split_on_char '\n' content in
+ let rec clean = function [] -> [] | ""::w -> clean w | w -> w in
+ List.iter
+ (fun l -> Format.fprintf fmt "@\n%s" l)
+ (List.rev (clean (List.rev (clean lines)))) ;
+ Format.fprintf fmt "@\n```@]@."
+ end
+
+type column = [
+ | `Left of string
+ | `Right of string
+ | `Center of string
+]
+
+let table columns rows fmt =
+ begin
+ Format.fprintf fmt "@[<v 0>" ;
+ List.iter
+ (function `Left h | `Right h | `Center h -> Format.fprintf fmt "| %s " h)
+ columns ;
+ Format.fprintf fmt "|@\n" ;
+ List.iter (fun column ->
+ let dash h k = String.make (max 3 (String.length h + k)) '-' in
+ match column with
+ | `Left h -> Format.fprintf fmt "|:%s" (dash h 1)
+ | `Right h -> Format.fprintf fmt "|%s:" (dash h 1)
+ | `Center h -> Format.fprintf fmt "|:%s:" (dash h 0)
+ ) columns ;
+ Format.fprintf fmt "|@\n" ;
+ List.iter (fun row ->
+ List.iter (fun col -> Format.fprintf fmt "| @[<h 0>%t@] " col) row ;
+ Format.fprintf fmt "|@\n" ;
+ ) rows ;
+ Format.fprintf fmt "@]@." ;
+ end
+
+let concat ps = merge newline (List.filter (fun p -> p != empty) ps)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Refs --- *)
+(* -------------------------------------------------------------------------- *)
+
+let mk f fmt = (f ()) fmt
+let mk_text = mk
+let mk_block = mk
+
+(* -------------------------------------------------------------------------- *)
+(* --- Sections --- *)
+(* -------------------------------------------------------------------------- *)
+
+let document s = s
+
+let subsections section subsections = section </> in_h1 (merge newline subsections)
+
+let section ?name ~title content subsections =
+ h1 ?name title </> content </> in_h1 (merge newline subsections)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Include File --- *)
+(* -------------------------------------------------------------------------- *)
+
+let from_file path fmt =
+ let inc = open_in path in
+ try
+ while true do
+ let line = input_line inc in
+ Format.pp_print_string fmt line ;
+ Format.pp_print_newline fmt () ;
+ done
+ with
+ | End_of_file -> close_in inc
+ | exn -> close_in inc ; raise exn
+
+let read_block = from_file
+let read_section = from_file
+let read_text path fmt = Format.fprintf fmt "@[<h 0>%t@]" (from_file path)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Dump to File --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec mkdir root page =
+ let dir = Filename.dirname page in
+ if dir <> "." && dir <> ".." then
+ let path = Printf.sprintf "%s/%s" root dir in
+ if not (Sys.file_exists path) then
+ begin
+ mkdir root dir ;
+ try Unix.mkdir path 0o755
+ with Unix.Unix_error _ ->
+ failwith (Printf.sprintf "Can not create direcoty '%s'" dir)
+ end
+
+let dump ~root ~page ?(names=false) ?toc doc =
+ local
+ { page ; path = filepath page ; level = 1 ; toc ; names = names }
+ begin fun () ->
+ mkdir root page ;
+ let out = open_out (Printf.sprintf "%s/%s" root page) in
+ let fmt = Format.formatter_of_out_channel out in
+ try
+ doc fmt ;
+ Format.pp_print_newline fmt () ;
+ close_out out ;
+ with err ->
+ Format.pp_print_newline fmt () ;
+ close_out out ;
+ raise err
+ end ()
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/libraries/utils/markdown.mli b/src/libraries/utils/markdown.mli
new file mode 100644
index 0000000000000000000000000000000000000000..34b955919fcc8696722172e66ad43680b689335c
--- /dev/null
+++ b/src/libraries/utils/markdown.mli
@@ -0,0 +1,183 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Markdown Documentation Generation Utility --- *)
+(* -------------------------------------------------------------------------- *)
+
+(** {2 Markdown}
+
+ A lightweight helper for generating Markdown documentation.
+ Two levels of formatters are defined to help managing indentation and
+ spaces: [text] for inline markdown, and [block] for markdown paragraphs.
+
+*)
+
+type text
+type block
+type section
+
+val (<@>) : text -> text -> text (** Infix operator for [glue] *)
+val (<+>) : text -> text -> text (** Infix operator for [text] *)
+val (</>) : block -> block -> block (** Infix operator for [concat] *)
+
+(** {2 Text Constructors} *)
+
+val nil : text (** Empty *)
+val raw : string -> text (** inlined markdown format *)
+val rm : string -> text (** roman (normal) style *)
+val it : string -> text (** italic style *)
+val bf : string -> text (** bold style *)
+val tt : string -> text (** typewriter style *)
+
+val glue : ?sep:text -> text list -> text (** Glue text fragments *)
+val text : text list -> text (** Glue text fragments with spaces *)
+
+(** {2 Block Constructors} *)
+
+val empty : block (** Empty *)
+val hrule : block (** Horizontal rule *)
+
+val h1 : ?name:string -> string -> block (** Title level 1 *)
+val h2 : ?name:string -> string -> block (** Title level 2 *)
+val h3 : ?name:string -> string -> block (** Title level 3 *)
+val h4 : ?name:string -> string -> block (** Title level 4 *)
+
+val in_h1 : block -> block (** Increment title levels by 1 *)
+val in_h2 : block -> block (** Increment title levels by 2 *)
+val in_h3 : block -> block (** Increment title levels by 3 *)
+val in_h4 : block -> block (** Increment title levels by 4 *)
+
+val par : text -> block (** Simple text paragraph *)
+val praw : string -> block (** Simple raw paragraph *)
+val list : text list -> block (** Itemized list *)
+val enum : text list -> block (** Enumerated list *)
+val description : (string * text) list -> block (** Description list *)
+
+(** Formatted code.
+
+ The code content is pretty-printed in a vertical [<v0>] box
+ with default [Format] formatter.
+ Leading and trailing empty lines are removed and indentation is
+ preserved. *)
+val code : ?lang:string -> (Format.formatter -> unit) -> block
+
+val concat : block list -> block (** Glue paragraphs with empty lines *)
+
+(** {2 Hyperlinks}
+
+ [`Page], [`Name] and [`Section] links refers to the current document,
+ see [dump] function below.
+
+ In [`Section(p,t)], [p] is the page path relative to the
+ document {i root}, and [t] is the section title {i or} name.
+
+ For [`Name a], the links refers to name or title [a]
+ in the {i current} page.
+
+ Hence, everywhere throughout a self-content document directory [~root],
+ local page [~page] inside [~root] can be referenced
+ by [`Page page], and its sections can by [`Section(page,title)]
+ or [`Section(page,name)].
+
+*)
+
+type href = [
+ | `URL of string
+ | `Page of string
+ | `Name of string
+ | `Section of string * string
+]
+
+(** Default [~title] is taken from [href]. When printed,
+ actual link will be relativized with respect to current page. *)
+val href : ?title:string -> href -> text
+
+(** Define a local anchor *)
+val aname : string -> block
+
+(** {2 Tables} *)
+
+type column = [
+ | `Left of string
+ | `Right of string
+ | `Center of string
+]
+
+val table : column list -> text list list -> block
+
+(** {2 Markdown Generator}
+ Generating function are called each time the markdown
+ fragment is printed. *)
+
+val mk_text : (unit -> text) -> text
+val mk_block : (unit -> block) -> block
+
+(** {2 Sections}
+
+ Sections are an alternative to [h1-h4] constructors to build
+ properly nested sub-sections. Deep sections at depth 5 and more are
+ flattened.
+*)
+
+val section : ?name:string -> title:string -> block -> section list -> section
+val subsections : section -> section list -> section
+val document : section -> block
+
+(** {2 Dump to file}
+
+ Generate the markdown [~page] in directory [~root] with the given content.
+ The [~root] directory shall be absolute or relative to the current working
+ directory. The [~page] file-path shall be relative to the [~root] directory
+ and will be used to relocate hyperlinks to other [`Page] and [`Section]
+ properly.
+
+ Hence, everywhere throughout the document, [dump ~root ~page doc]
+ is referenced by [`Page page], and its sections are referenced by
+ [`Section(page,title)].
+
+*)
+
+(** Callback to listen for actual sections when printing a page. *)
+type toc = level:int -> name:string -> title:string -> unit
+
+(** Create a markdown page.
+ - [~root] document directory (relocatable)
+ - [~page] relative file-path of the page in [~root] (non relocatable)
+ - [~names] generate explicit [<a name=...>] tags for all titles
+ - [~toc] optional callback to register table of contents
+*)
+val dump : root:string -> page:string -> ?names:bool -> ?toc:toc -> block -> unit
+
+(** {2 Miscellaneous} *)
+
+val read_text : string -> text
+val read_block : string -> block
+val read_section : string -> section
+
+val fmt_text : (Format.formatter -> unit) -> text
+val fmt_block : (Format.formatter -> unit) -> block
+val pp_text : Format.formatter -> text -> unit
+val pp_block : Format.formatter -> block -> unit
+val pp_section : Format.formatter -> section -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/.gitignore b/src/plugins/server/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..f1d2f8cc5ec41ae8f688b80afeb51e4084f3c60f
--- /dev/null
+++ b/src/plugins/server/.gitignore
@@ -0,0 +1,4 @@
+/Makefile
+/Server.mli
+/tests/ptests_config
+/tests/report/result
diff --git a/src/plugins/server/Makefile.in b/src/plugins/server/Makefile.in
new file mode 100644
index 0000000000000000000000000000000000000000..f70395724dae585cc902a00f8ca0dcc190d9ace0
--- /dev/null
+++ b/src/plugins/server/Makefile.in
@@ -0,0 +1,117 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# Do not use ?= to initialize both below variables
+# (fixed efficiency issue, see GNU Make manual, Section 8.11)
+ifndef FRAMAC_SHARE
+FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
+endif
+ifndef FRAMAC_LIBDIR
+FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
+endif
+
+include $(FRAMAC_SHARE)/Makefile.config
+# --------------------------------------------------------------------------
+# --- Plugin Setting
+# --------------------------------------------------------------------------
+
+PLUGIN_ENABLE:=@ENABLE_SERVER@
+PLUGIN_NAME:=Server
+PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
+PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
+
+PLUGIN_REQUIRES:= yojson
+PLUGIN_CMO:= \
+ server_parameters \
+ jbuffer \
+ doc syntax data main request \
+ server_batch \
+ kernel_main \
+ kernel_project \
+ kernel_ast
+
+PLUGIN_UNDOC:= server_batch.ml server_zmq.ml
+
+PLUGIN_GENERATED:= $(PLUGIN_DIR)/Server.mli
+PLUGIN_TESTS :=
+
+# --------------------------------------------------------------------------
+# --- ZeroMQ Support
+# --------------------------------------------------------------------------
+
+ifeq (@SERVER_ZMQ@,yes)
+PLUGIN_REQUIRES+= zmq
+PLUGIN_CMO+= server_zmq
+endif
+
+# --------------------------------------------------------------------------
+# --- Frama-C Dynamic Plug-in
+# --------------------------------------------------------------------------
+
+include $(FRAMAC_SHARE)/Makefile.dynamic
+
+# --------------------------------------------------------------------------
+# --- Server API
+# --------------------------------------------------------------------------
+
+SERVER_API= \
+ doc.mli syntax.mli data.mli request.mli
+
+define Capitalize
+$(shell printf "%s%s" \
+ $$($(ECHO) $(1) | cut -c 1 | tr '[:lower:]' '[:upper:]')
+ $$($(ECHO) $(1) | cut -c 2-))
+endef
+
+define ExportModule
+$(ECHO) "module $(call Capitalize, $(basename $(notdir $(1)))) : sig" >> $(2);
+$(ECHO) '# 1 "$(1)"' >> $(2);
+$(CAT) $(1) >> $(2);
+$(ECHO) "end" >> $(2);
+endef
+
+SERVER_MLI=$(addprefix $(Server_DIR)/, $(SERVER_API))
+
+$(Server_DIR)/Server.mli: $(Server_DIR)/Makefile $(SERVER_MLI)
+ $(PRINT_MAKING) $@ "from" $(SERVER_MLI)
+ $(RM) $@ $@.tmp
+ $(ECHO) "(* This file is generated. Do not edit. *)" >> $@.tmp
+ $(ECHO) "(** {b Server Public API} *)" >> $@.tmp
+ $(foreach file,$(SERVER_MLI),$(call ExportModule,$(file),$@.tmp))
+ $(CHMOD_RO) $@.tmp
+ $(MV) $@.tmp $@
+
+# --------------------------------------------------------------------------
+# --- Configure
+# --------------------------------------------------------------------------
+
+ifeq ("$(FRAMAC_INTERNAL)","yes")
+CONFIG_STATUS_DIR=$(FRAMAC_SRC)
+else
+CONFIG_STATUS_DIR=.
+endif
+
+$(Server_DIR)/Makefile: $(Server_DIR)/Makefile.in \
+ $(CONFIG_STATUS_DIR)/config.status
+ cd $(CONFIG_STATUS_DIR) && ./config.status --file $@
+
+# --------------------------------------------------------------------------
diff --git a/src/plugins/server/configure.ac b/src/plugins/server/configure.ac
new file mode 100644
index 0000000000000000000000000000000000000000..4ab9e3f73f11ed3c98fdf85d9531e12b51368e10
--- /dev/null
+++ b/src/plugins/server/configure.ac
@@ -0,0 +1,84 @@
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2019 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+########################################
+# Server as a standard Frama-C plug-in #
+########################################
+
+m4_define([plugin_file],Makefile.in)
+
+m4_define([FRAMAC_SHARE_ENV],
+ [m4_normalize(m4_esyscmd([echo $FRAMAC_SHARE]))])
+
+m4_define([FRAMAC_SHARE],
+ [m4_ifval(FRAMAC_SHARE_ENV,[FRAMAC_SHARE_ENV],
+ [m4_esyscmd(frama-c -print-path)])])
+
+m4_ifndef([FRAMAC_M4_MACROS], [m4_include(FRAMAC_SHARE/configure.ac)])
+
+check_plugin(server,PLUGIN_RELATIVE_PATH(plugin_file),[Server plug-in],yes)
+
+########################################
+# Server Main Configuration #
+########################################
+
+AC_MSG_CHECKING(for Yojson)
+SERVER_LIB_YOJSON=$($OCAMLFIND query yojson -format %v)
+if test -z "$SERVER_LIB_YOJSON"
+then
+ AC_MSG_RESULT(Server disabled (use 'opam install yojson'))
+ plugin_disable(server)
+else
+ AC_MSG_RESULT(yes)
+fi
+
+########################################
+# Server ZMQ Configuration #
+########################################
+
+AC_ARG_ENABLE(
+ server-zmq,
+ [ --enable-server-zmq Server ZeroMQ support (default: yes)],
+ SERVER_ZMQ=$enableval,
+ SERVER_ZMQ=yes
+)
+
+if test "$SERVER_ZMQ" = "yes" ;
+then
+ AC_MSG_CHECKING(for ZeroMQ)
+ SERVER_LIB_ZMQ=$($OCAMLFIND query zmq -format %v)
+ if test -z "$SERVER_LIB_ZMQ"
+ then
+ AC_MSG_RESULT(Server support for ZeroMQ disabled (use 'opam install zmq').)
+ SERVER_ZMQ=no
+ else
+ AC_MSG_RESULT(yes);
+ fi
+fi
+
+AC_SUBST(SERVER_ZMQ)
+
+#######################
+# Generating Makefile #
+#######################
+
+write_plugin_config(Makefile)
diff --git a/src/plugins/server/data.ml b/src/plugins/server/data.ml
new file mode 100644
index 0000000000000000000000000000000000000000..46c204d72366ee3e90f6160d5dbc61a078989eeb
--- /dev/null
+++ b/src/plugins/server/data.ml
@@ -0,0 +1,533 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Data Encoding --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Js = Yojson.Basic
+module Ju = Yojson.Basic.Util
+
+type json = Js.t
+let pretty = Js.pretty_print ~std:false
+
+module type S =
+sig
+ type t
+ val syntax : Syntax.t
+ val of_json : json -> t
+ val to_json : t -> json
+end
+
+module type Info =
+sig
+ val page : Doc.page
+ val name : string
+ val descr : Markdown.text
+end
+
+type 'a data = (module S with type t = 'a)
+
+let failure js msg =
+ Pretty_utils.ksfprintf (fun msg -> raise(Ju.Type_error(msg,js))) msg
+
+(* -------------------------------------------------------------------------- *)
+(* --- Option --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Joption(A : S) : S with type t = A.t option =
+struct
+ type t = A.t option
+
+ let nullable = try ignore (A.of_json `Null) ; true with _ -> false
+ let syntax =
+ Syntax.option (if nullable then A.syntax else Syntax.tuple [A.syntax])
+
+ let to_json = function
+ | None -> `Null
+ | Some v -> if nullable then `List [A.to_json v] else A.to_json v
+
+ let of_json = function
+ | `Null -> None
+ | `List [js] when nullable -> Some (A.of_json js)
+ | js -> Some (A.of_json js)
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Tuples --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Jpair(A : S)(B : S) : S with type t = A.t * B.t =
+struct
+ type t = A.t * B.t
+ let syntax = Syntax.tuple [A.syntax;B.syntax]
+ let to_json (x,y) = `List [ A.to_json x ; B.to_json y ]
+ let of_json = function
+ | `List [ ja ; jb ] -> A.of_json ja , B.of_json jb
+ | js -> failure js "Expected list with 2 elements"
+end
+
+module Jtriple(A : S)(B : S)(C : S) : S with type t = A.t * B.t * C.t =
+struct
+ type t = A.t * B.t * C.t
+ let syntax = Syntax.tuple [A.syntax;B.syntax;C.syntax]
+ let to_json (x,y,z) = `List [ A.to_json x ; B.to_json y ; C.to_json z ]
+ let of_json = function
+ | `List [ ja ; jb ; jc ] -> A.of_json ja , B.of_json jb , C.of_json jc
+ | js -> failure js "Expected list with 3 elements"
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Lists --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Jlist(A : S) : S with type t = A.t list =
+struct
+ type t = A.t list
+ let syntax = Syntax.array A.syntax
+ let to_json xs = `List (List.map A.to_json xs)
+ let of_json js = List.map A.of_json (Ju.to_list js)
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Arrays --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Jarray(A : S) : S with type t = A.t array =
+struct
+ type t = A.t array
+ let syntax = Syntax.array A.syntax
+ let to_json xs = `List (List.map A.to_json (Array.to_list xs))
+ let of_json js = Array.of_list @@ List.map A.of_json (Ju.to_list js)
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Collections --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type S_collection =
+sig
+ include S
+ module Joption : S with type t = t option
+ module Jlist : S with type t = t list
+ module Jarray : S with type t = t array
+end
+
+module Collection(A : S) : S_collection with type t = A.t =
+struct
+ include A
+ module Joption = Joption(A)
+ module Jlist = Jlist(A)
+ module Jarray = Jarray(A)
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Atomic Types --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Junit : S with type t = unit =
+struct
+ type t = unit
+ let syntax = Syntax.unit
+ let of_json _js = ()
+ let to_json () = `Null
+end
+
+module Jany : S with type t = json =
+struct
+ type t = json
+ let syntax = Syntax.any
+ let of_json js = js
+ let to_json js = js
+end
+
+module Jbool : S_collection with type t = bool =
+ Collection
+ (struct
+ type t = bool
+ let syntax = Syntax.boolean
+ let of_json = Ju.to_bool
+ let to_json b = `Bool b
+ end)
+
+module Jint : S_collection with type t = int =
+ Collection
+ (struct
+ type t = int
+ let syntax = Syntax.int
+ let of_json = Ju.to_int
+ let to_json n = `Int n
+ end)
+
+module Jfloat : S_collection with type t = float =
+ Collection
+ (struct
+ type t = float
+ let syntax = Syntax.number
+ let of_json = Ju.to_number
+ let to_json v = `Float v
+ end)
+
+module Jstring : S_collection with type t = string =
+ Collection
+ (struct
+ type t = string
+ let syntax = Syntax.string
+ let of_json = Ju.to_string
+ let to_json s = `String s
+ end)
+
+module Jident : S_collection with type t = string =
+ Collection
+ (struct
+ type t = string
+ let syntax = Syntax.ident
+ let of_json = Ju.to_string
+ let to_json s = `String s
+ end)
+
+let text_page = Doc.page `Kernel ~title:"Rich Text Format" ~filename:"text.md"
+
+module Jtext =
+struct
+ include Jany
+ let syntax = Syntax.publish ~page:text_page ~name:"text"
+ ~synopsis:Syntax.any ~descr:(Markdown.rm "Formatted text.") ()
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Records --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Fmap = Map.Make(String)
+
+module Record( R : Info ) =
+struct
+
+ type t = json Fmap.t
+
+ type 'a field = {
+ member : t -> bool ;
+ getter : t -> 'a ;
+ setter : t -> 'a -> t ;
+ }
+
+ (* Declared Fields in this Record *)
+ let fdocs = ref []
+ let defaults = ref Fmap.empty
+
+ let default () = !defaults
+ let has fd r = fd.member r
+ let get fd r = fd.getter r
+ let set fd v r = fd.setter r v
+
+ let field (type a) name ~descr ?default (d : a data) : a field =
+ let module D = (val d) in
+ begin match default with
+ | None -> ()
+ | Some v -> defaults := Fmap.add name (D.to_json v) !defaults
+ end ;
+ fdocs := Syntax.{ name ; syntax = D.syntax ; descr } :: !fdocs ;
+ let member r = Fmap.mem name r in
+ let getter r = D.of_json (Fmap.find name r) in
+ let setter r v = Fmap.add name (D.to_json v) r in
+ { member ; getter ; setter }
+
+ let option (type a) name ~descr (d : a data) : a option field =
+ let module D = (val d) in
+ fdocs := Syntax.{ name ; syntax = option D.syntax ; descr } :: !fdocs ;
+ let member r = Fmap.mem name r in
+ let getter r =
+ try Some (D.of_json (Fmap.find name r)) with Not_found -> None in
+ let setter r = function
+ | None -> Fmap.remove name r
+ | Some v -> Fmap.add name (D.to_json v) r in
+ { member ; getter ; setter }
+
+ let fields () = Syntax.fields ~title:"Field" !fdocs
+
+ let syntax =
+ Syntax.publish ~page:R.page ~name:R.name
+ ~descr:R.descr
+ ~synopsis:(Syntax.record [])
+ ~details:(Markdown.mk_block fields) ()
+
+ let of_json js =
+ List.fold_left
+ (fun r (fd,js) -> Fmap.add fd js r)
+ (default ()) (Ju.to_assoc js)
+
+ let to_json r : json =
+ `Assoc (Fmap.fold (fun fd js fds -> (fd,js) :: fds) r [])
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Index --- *)
+(* -------------------------------------------------------------------------- *)
+
+(** Simplified [Map.S] *)
+module type Map =
+sig
+ type 'a t
+ type key
+ val empty : 'a t
+ val add : key -> 'a -> 'a t -> 'a t
+ val find : key -> 'a t -> 'a
+end
+
+module type Index =
+sig
+ include S_collection
+ val get : t -> int
+ val find : int -> t
+ val clear : unit -> unit
+end
+
+let publish_id (module A : Info) =
+ Syntax.publish
+ ~page:A.page ~name:A.name ~synopsis:Syntax.int ~descr:A.descr ()
+
+module INDEXER(M : Map)(I : Info) :
+sig
+ type index
+ val create : unit -> index
+ val clear : index -> unit
+ val get : index -> M.key -> int
+ val find : index -> int -> M.key
+ val to_json : index -> M.key -> json
+ val of_json : index -> json -> M.key
+end =
+struct
+
+ type index = {
+ mutable kid : int ;
+ mutable index : int M.t ;
+ lookup : (int,M.key) Hashtbl.t ;
+ }
+
+ let create () = {
+ kid = 0 ;
+ index = M.empty ;
+ lookup = Hashtbl.create 0 ;
+ }
+
+ let clear m =
+ begin
+ m.kid <- 0 ;
+ m.index <- M.empty ;
+ Hashtbl.clear m.lookup ;
+ end
+
+ let get m a =
+ try M.find a m.index
+ with Not_found ->
+ let id = m.kid in
+ m.kid <- succ id ;
+ m.index <- M.add a id m.index ;
+ Hashtbl.add m.lookup id a ; id
+
+ let find m id = Hashtbl.find m.lookup id
+
+ let to_json m a = `Int (get m a)
+ let of_json m js =
+ let id = Ju.to_int js in
+ try find m id
+ with Not_found ->
+ failure js "[%s] No registered id #%d" I.name id
+
+end
+
+module Static(M : Map)(I : Info) : Index with type t = M.key =
+struct
+ module INDEX = INDEXER(M)(I)
+ let index = INDEX.create ()
+ let clear () = INDEX.clear index
+ let get = INDEX.get index
+ let find = INDEX.find index
+ include Collection
+ (struct
+ type t = M.key
+ let syntax = publish_id (module I)
+ let of_json = INDEX.of_json index
+ let to_json = INDEX.to_json index
+ end)
+end
+
+module Index(M : Map)(I : Info) : Index with type t = M.key =
+struct
+
+ module INDEX = INDEXER(M)(I)
+ module TYPE : Datatype.S with type t = INDEX.index =
+ Datatype.Make
+ (struct
+ type t = INDEX.index
+ include Datatype.Undefined
+ let reprs = [INDEX.create()]
+ let name = "Server.Data.Index.Type." ^ I.name
+ let mem_project = Datatype.never_any_project
+ end)
+ module STATE = State_builder.Ref(TYPE)
+ (struct
+ let name = "Server.Data.Index.State." ^ I.name
+ let dependencies = []
+ let default = INDEX.create
+ end)
+
+ let index () = STATE.get ()
+ let clear () = INDEX.clear (index())
+
+ let get a = INDEX.get (index()) a
+ let find id = INDEX.find (index()) id
+
+ include Collection
+ (struct
+ type t = M.key
+ let syntax = publish_id (module I)
+ let of_json js = INDEX.of_json (index()) js
+ let to_json v = INDEX.to_json (index()) v
+ end)
+
+end
+
+module type IdentifiedType =
+sig
+ type t
+ val id : t -> int
+ include Info
+end
+
+module Identified(A : IdentifiedType) : Index with type t = A.t =
+struct
+
+ type index = (int,A.t) Hashtbl.t
+
+ module TYPE : Datatype.S with type t = index =
+ Datatype.Make
+ (struct
+ type t = index
+ include Datatype.Undefined
+ let reprs = [Hashtbl.create 0]
+ let name = "Server.Data.Identified.Type." ^ A.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 dependencies = []
+ let default () = Hashtbl.create 0
+ end)
+
+ let lookup () = STATE.get ()
+ let clear () = Hashtbl.clear (lookup())
+
+ let get = A.id
+ let find id = Hashtbl.find (lookup()) id
+
+ include Collection
+ (struct
+ type t = A.t
+ let syntax = publish_id (module A)
+ 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 js "[%s] No registered id #%d" A.name k
+ end)
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Dictionnary --- *)
+(* -------------------------------------------------------------------------- *)
+
+module type Enum =
+sig
+ type t
+ val values : (t * string * Markdown.text) list
+ include Info
+end
+
+module Dictionary(E : Enum) =
+struct
+
+ let registered = ref false
+ let index = Hashtbl.create 0
+ let lookup = Hashtbl.create 0
+
+ let register () =
+ if not !registered then
+ begin
+ registered := true ;
+ let invalid msg tag =
+ let msg = Printf.sprintf "Server.Data.Enum.%s: duplicate %s (%S)"
+ E.name msg tag in
+ raise (Invalid_argument msg)
+ in
+ List.iter
+ (fun (value,tag,_) ->
+ if Hashtbl.mem index value then invalid "value" tag ;
+ Hashtbl.add index value tag ;
+ if Hashtbl.mem lookup tag then invalid "tag" tag ;
+ Hashtbl.add lookup tag value ;
+ ) E.values
+ end
+
+ let values () =
+ Markdown.table
+ [ `Left E.name ; `Left "Description" ]
+ (List.map
+ (fun (_,tag,descr) ->
+ [ Markdown.tt (Printf.sprintf "%S" tag) ; descr ]
+ ) E.values)
+
+ include Collection
+ (struct
+ type t = E.t
+
+ let syntax = Syntax.publish
+ ~page:E.page ~name:E.name
+ ~synopsis:Syntax.ident
+ ~descr:E.descr ~details:(Markdown.mk_block values) ()
+
+ let to_json value =
+ register () ;
+ try `String (Hashtbl.find index value)
+ with Not_found ->
+ raise (Invalid_argument
+ (Printf.sprintf "[%s] Unregistered value" E.name))
+
+ let of_json js =
+ register () ;
+ let tag = Ju.to_string js in
+ try Hashtbl.find lookup tag
+ with Not_found ->
+ let msg = Printf.sprintf "[%s] Unregistered tag %S" E.name tag in
+ raise (Ju.Type_error(msg,js))
+
+ end)
+
+end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/data.mli b/src/plugins/server/data.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f0c993fd042ca28c5abc2b961071ac01c9a4cb14
--- /dev/null
+++ b/src/plugins/server/data.mli
@@ -0,0 +1,190 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Data Encoding *)
+(* -------------------------------------------------------------------------- *)
+
+type json = Json.t
+
+val pretty : Format.formatter -> json -> unit
+
+module type S =
+sig
+ type t
+ val syntax : Syntax.t
+ val of_json : json -> t
+ val to_json : t -> json
+end
+
+
+(** Datatype registration.
+
+ Name and page must be consistent with each other:
+ - The name must be lowercase, dash-separated list of identifiers
+ - Protocol data must start with ["<server>-*"]
+ - Plugin data must start with ["<plugin>-*"]
+*)
+module type Info =
+sig
+ val page : Doc.page
+ val name : string
+ val descr : Markdown.text
+end
+
+type 'a data = (module S with type t = 'a)
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Collections} *)
+(* -------------------------------------------------------------------------- *)
+
+module type S_collection =
+sig
+ include S
+ module Joption : S with type t = t option
+ module Jlist : S with type t = t list
+ module Jarray : S with type t = t array
+end
+
+module Collection(A : S) : S_collection with type t = A.t
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Constructors} *)
+(* -------------------------------------------------------------------------- *)
+
+module Joption(A : S) : S with type t = A.t option
+module Jpair(A : S)(B : S) : S with type t = A.t * B.t
+module Jtriple(A : S)(B : S)(C : S) : S with type t = A.t * B.t * C.t
+module Jlist(A : S) : S with type t = A.t list
+module Jarray(A : S) : S with type t = A.t array
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Atomic Data} *)
+(* -------------------------------------------------------------------------- *)
+
+module Junit : S with type t = unit
+module Jany : S with type t = json
+module Jbool : S_collection with type t = bool
+module Jint : S_collection with type t = int
+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] *)
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Records} *)
+(* -------------------------------------------------------------------------- *)
+
+module Record(R : Info) :
+sig
+ (** A new type [t] is created for each application of the functor. *)
+ include S
+
+ (** Parametric field. Can only be used with type [t]. *)
+ type 'a field
+
+ (** Field constructor *)
+ val field : string -> descr:Markdown.text -> ?default:'a -> 'a data -> 'a field
+
+ (** Optional field constructor *)
+ val option : string -> descr:Markdown.text -> 'a data -> 'a option field
+
+ (** Field presence. If the field has a default value, it will be always
+ present. *)
+ val has : 'a field -> t -> bool
+
+ (** Field accessor.
+ @raise Not_found if the field is optional and not present *)
+ val get : 'a field -> t -> 'a
+
+ (** Field updator. *)
+ val set : 'a field -> 'a -> t -> t
+
+ (** Contains only the default values. *)
+ val default : unit -> t
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Indexed Values} *)
+(* -------------------------------------------------------------------------- *)
+
+(** Simplified [Map.S] *)
+module type Map =
+sig
+ type 'a t
+ type key
+ val empty : 'a t
+ val add : key -> 'a -> 'a t -> 'a t
+ val find : key -> 'a t -> 'a
+end
+
+module type Index =
+sig
+ include S_collection
+ val get : t -> int
+ val find : int -> t (** @raise Not_found if not registered *)
+ val clear : unit -> unit
+ (** Clear index tables. Use with extreme care. *)
+end
+
+(** Builds an indexer that {i does not} depend on current project. *)
+module Static(M : Map)(I : Info) : Index with type t = M.key
+
+(** Builds a {i projectified} index. *)
+module Index(M : Map)(I : Info) : Index with type t = M.key
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Identified Types} *)
+(* -------------------------------------------------------------------------- *)
+
+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
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Dictionary} *)
+(* -------------------------------------------------------------------------- *)
+
+module type Enum =
+sig
+ type t
+ val values : (t * string * Markdown.text) list
+ include Info
+end
+
+module Dictionary(E : Enum) : S_collection with type t = E.t
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Misc} *)
+(* -------------------------------------------------------------------------- *)
+
+val failure : json -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+(** @raise Yojson.Basic.Util.Type_error with provided message *)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/doc.ml b/src/plugins/server/doc.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0d141b3f018ecdd7b1946c5fa5f0db5a76bfd16f
--- /dev/null
+++ b/src/plugins/server/doc.ml
@@ -0,0 +1,204 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server Documentation --- *)
+(* -------------------------------------------------------------------------- *)
+
+type json = Yojson.Basic.t
+module Senv = Server_parameters
+module Pages = Map.Make(String)
+
+type chapter = [ `Protocol | `Kernel | `Plugin of string ]
+
+type page = {
+ path : string ;
+ rootdir : string ; (* path to document root *)
+ chapter : chapter ;
+ title : string ;
+ order : int ;
+ intro : Markdown.section ;
+ mutable sections : Markdown.section list ;
+}
+
+let order = ref 0
+let pages : page Pages.t ref = ref Pages.empty
+let plugins : string list ref = ref []
+let entries : (string * Markdown.href) list ref = ref []
+let path page = page.path
+let href page name : Markdown.href = `Section( page.path , name )
+
+(* -------------------------------------------------------------------------- *)
+(* --- Page Collection --- *)
+(* -------------------------------------------------------------------------- *)
+
+let chapter pg = pg.chapter
+
+let page chapter ~title ~filename =
+ let rootdir,path = match chapter with
+ | `Protocol -> "." , filename
+ | `Kernel -> ".." , Printf.sprintf "kernel/%s" filename
+ | `Plugin name -> "../.." , Printf.sprintf "plugins/%s/%s" name filename
+ in
+ try
+ let other = Pages.find path !pages in
+ Senv.failure "Duplicate page '%s' path@." path ; other
+ with Not_found ->
+ let intro = match chapter with
+ | `Protocol ->
+ Printf.sprintf "%s/server/protocol/%s" Config.datadir filename
+ | `Kernel ->
+ Printf.sprintf "%s/server/kernel/%s" Config.datadir filename
+ | `Plugin name ->
+ if not (List.mem name !plugins) then plugins := name :: !plugins ;
+ Printf.sprintf "%s/%s/server/%s" Config.datadir name filename in
+ let intro =
+ if Sys.file_exists intro
+ then Markdown.read_section intro
+ else Markdown.(section ~title empty []) in
+ let order = incr order ; !order in
+ let page = { order ; rootdir ; path ;
+ chapter ; title ; intro ;
+ sections=[] } in
+ pages := Pages.add path page !pages ; page
+
+let publish ~page ?name ?(index=[]) ~title content sections =
+ let id = match name with Some id -> id | None -> title in
+ let href = `Section( page.path , id ) in
+ let section = Markdown.section ?name ~title content sections in
+ List.iter (fun entry -> entries := (entry , href) :: !entries) index ;
+ page.sections <- section :: page.sections ; href
+
+let _ = page `Protocol ~title:"Architecture" ~filename:"server.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Tables of Content --- *)
+(* -------------------------------------------------------------------------- *)
+
+let title_of_chapter = function
+ | `Protocol -> "Server Protocols"
+ | `Kernel -> "Kernel Services"
+ | `Plugin name -> "Plugin " ^ String.capitalize_ascii name
+
+let pages_of_chapter c =
+ let w = ref [] in
+ Pages.iter
+ (fun _ p -> if p.chapter = c then w := p :: !w) !pages ;
+ List.sort (fun p q -> p.order - q.order) !w
+
+let table_of_chapter c fmt =
+ begin
+ Format.fprintf fmt "## %s@\n@." (title_of_chapter c) ;
+ List.iter
+ (fun p -> Format.fprintf fmt " - [%s](%s)@." p.title p.path)
+ (pages_of_chapter c) ;
+ Format.pp_print_newline fmt () ;
+ end
+
+let table_of_contents fmt =
+ begin
+ table_of_chapter `Protocol fmt ;
+ table_of_chapter `Kernel fmt ;
+ List.iter
+ (fun p -> table_of_chapter (`Plugin p) fmt)
+ (List.sort String.compare !plugins)
+ end
+
+let index () =
+ List.map
+ (fun (title,entry) -> Markdown.href ~title entry)
+ (List.sort (fun (a,_) (b,_) -> String.compare a b) !entries)
+
+let link ~toc ~title ~href : json =
+ let link = [ "title" , `String title ; "href" , `String href ] in
+ `Assoc (if not toc then link else ( "toc" , `Bool true ) :: link)
+
+let link_page page : json list =
+ List.fold_right
+ (fun p links ->
+ if p.chapter = page.chapter then
+ let toc = (p.path = page.path) in
+ let href = Filename.basename p.path in
+ link ~toc ~title:p.title ~href :: links
+ else links
+ ) (pages_of_chapter page.chapter) []
+
+let maindata : json =
+ `Assoc [
+ "document", `String "Frama-C Server" ;
+ "title",`String "Documentation" ;
+ "root", `String "." ;
+ ]
+
+let metadata page : json =
+ `Assoc [
+ "document", `String "Frama-C Server" ;
+ "chapter", `String (title_of_chapter page.chapter) ;
+ "title", `String page.title ;
+ "root", `String page.rootdir ;
+ "link",`List (link_page page) ;
+ ]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Dump Documentation --- *)
+(* -------------------------------------------------------------------------- *)
+
+let dump ~root ?(meta=true) () =
+ begin
+ Pages.iter
+ (fun path page ->
+ Senv.feedback "[doc] Page: '%s'" path ;
+ let body = Markdown.subsections page.intro (List.rev page.sections) in
+ Markdown.dump ~root ~page:path (Markdown.document body) ;
+ if meta then
+ let path = Printf.sprintf "%s/%s.json" root path in
+ Yojson.Basic.to_file path (metadata page) ;
+ ) !pages ;
+ Senv.feedback "[doc] Page: 'readme.md'" ;
+ if meta then
+ let path = Printf.sprintf "%s/readme.md.json" root in
+ Yojson.Basic.to_file path maindata ;
+ Markdown.(dump ~root ~page:"readme.md"
+ begin
+ h1 "Documentation" </>
+ par (bf "Version" <+> rm Config.version) </>
+ fmt_block table_of_contents </>
+ h2 "Index" </>
+ list (index ())
+ end) ;
+ end
+
+let () =
+ Db.Main.extend begin
+ fun () ->
+ let root = Senv.Doc.get () in
+ if root <> "" then
+ if Sys.file_exists root && Sys.is_directory root then
+ begin
+ Senv.feedback "[doc] Root: '%s'" root ;
+ dump ~root () ;
+ end
+ else
+ Senv.error "[doc] File '%s' is not a directory" root
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/doc.mli b/src/plugins/server/doc.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e204916f44b8eec01dcc173221c77821bc990e9b
--- /dev/null
+++ b/src/plugins/server/doc.mli
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Server Documentation *)
+(* -------------------------------------------------------------------------- *)
+
+open Markdown
+
+(** The main chapters of the documentation. *)
+type chapter = [ `Protocol | `Kernel | `Plugin of string ]
+
+(** A page of the server documentation. *)
+type page
+
+val path : page -> string
+val href : page -> string -> href
+val chapter : page -> chapter
+
+(** Obtain the given page in the server documentation.
+
+ The page initially contains an introductory section
+ read from the share directory:
+ - [frama-c/share/protocol/<filename>] for protocol pages,
+ - [frama-c/share/server/kernel/<filename>] for kernel pages,
+ - [frama-c/share/<plugin>/server/<filename>] for plugin's pages.
+*)
+val page : chapter -> title:string -> filename:string -> page
+
+(** Adds a section in the corresponding page.
+ Returns an href to the published section.
+ If index items are provided, they are added
+ to the server documentation index.
+*)
+val publish :
+ page:page ->
+ ?name:string ->
+ ?index:string list ->
+ title:string ->
+ Markdown.block ->
+ Markdown.section list ->
+ href
+
+(** Dumps all published pages of documentations. Unless [~meta:false],
+ also generates METADATA for each page in
+ [<filename>.json] for each page. *)
+val dump : root:string -> ?meta:bool -> unit -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/jbuffer.ml b/src/plugins/server/jbuffer.ml
new file mode 100644
index 0000000000000000000000000000000000000000..70e5d66af55ac68ad3b4d464a644f168d18f6073
--- /dev/null
+++ b/src/plugins/server/jbuffer.ml
@@ -0,0 +1,137 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type json = Yojson.Basic.t
+
+type buffer = {
+ text : FCBuffer.t ;
+ mutable rjson : json list ; (* Current op-codes in reverse order *)
+ mutable stack : ( string * json list ) list ;
+ mutable fmt : Format.formatter ;
+}
+
+let append buffer s k n =
+ FCBuffer.add_substring buffer.text s k n
+
+let flush buffer () =
+ let t = buffer.text in
+ let n = FCBuffer.length t in
+ if n > 0 then
+ let js = `String (FCBuffer.contents t) in
+ buffer.rjson <- js :: buffer.rjson ;
+ FCBuffer.clear t
+
+let push_tag buffer tag =
+ flush buffer () ;
+ buffer.stack <- ( tag , buffer.rjson ) :: buffer.stack ;
+ buffer.rjson <- []
+
+let pop_tag buffer _tag =
+ match buffer.stack with
+ | [] -> ()
+ | (tag,rjson)::stack ->
+ flush buffer () ;
+ buffer.stack <- stack ;
+ let content = List.rev buffer.rjson in
+ buffer.rjson <-
+ if content = [] then rjson
+ else
+ let block = `List ( `String tag :: content ) in
+ block :: rjson
+
+let no_mark _tag = ()
+let mark_open_tag buffer tg = push_tag buffer tg ; ""
+let mark_close_tag buffer tg = pop_tag buffer tg ; ""
+
+let create ?indent ?margin () =
+ let buffer = {
+ fmt = Format.err_formatter ;
+ text = FCBuffer.create 80 ; rjson = [] ; stack = []
+ } in
+ let fmt = Format.make_formatter (append buffer) (flush buffer) in
+ buffer.fmt <- fmt ;
+ begin match indent , margin with
+ | None , None -> ()
+ | Some k , None ->
+ let m = Format.pp_get_margin fmt () in
+ Format.pp_set_max_indent fmt (max 0 (min k m))
+ | None , Some m ->
+ Format.pp_set_margin fmt (max 0 m) ;
+ let k = Format.pp_get_max_indent fmt () in
+ if k < m-10 then Format.pp_set_max_indent fmt (max 0 (m-10))
+ | Some k , Some m ->
+ Format.pp_set_margin fmt (max 0 m) ;
+ Format.pp_set_max_indent fmt (max 0 (min k (m-10)))
+ end ;
+ begin
+ let open Format in
+ pp_set_formatter_tag_functions fmt {
+ print_open_tag = no_mark ;
+ print_close_tag = no_mark ;
+ mark_open_tag = mark_open_tag buffer ;
+ mark_close_tag = mark_close_tag buffer ;
+ } ;
+ pp_set_print_tags fmt false ;
+ pp_set_mark_tags fmt true ;
+ end ;
+ buffer
+
+let bprintf buffer msg = Format.fprintf buffer.fmt msg
+let formatter buffer = buffer.fmt
+
+let contents buffer : json =
+ flush buffer () ;
+ while buffer.stack <> [] do
+ pop_tag buffer ""
+ done ;
+ match List.rev buffer.rjson with
+ | [] -> `Null
+ | [`String _ as text] -> text
+ | content -> `List ( `String "" :: content )
+
+let format ?indent ?margin msg =
+ let buffer = create ?indent ?margin () in
+ Format.kfprintf
+ (fun fmt -> Format.pp_print_flush fmt () ; contents buffer)
+ buffer.fmt msg
+
+let to_json ?indent ?margin pp a =
+ let buffer = create ?indent ?margin () in
+ pp buffer.fmt a ;
+ Format.pp_print_flush buffer.fmt () ;
+ contents buffer
+
+let rec fprintf fmt = function
+ | `Null -> ()
+ | `String text -> Format.pp_print_string fmt text
+ | `List ( `String tag :: content ) ->
+ if tag <> "" then
+ begin
+ Format.fprintf fmt "@{<%s>" tag ;
+ List.iter (fprintf fmt) content ;
+ Format.fprintf fmt "@}" ;
+ end
+ else
+ List.iter (fprintf fmt) content
+ | js -> raise (Yojson.Basic.Util.Type_error("Invalid rich-text format",js))
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/jbuffer.mli b/src/plugins/server/jbuffer.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3e1e02a1beae8615cf925e52b980b093749766c1
--- /dev/null
+++ b/src/plugins/server/jbuffer.mli
@@ -0,0 +1,60 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type json = Json.t
+
+(** All-in-one formatter. Return the JSON encoding of formatted text. *)
+val format : ?indent:int -> ?margin:int ->
+ ('a,Format.formatter,unit,json) format4 -> 'a
+
+(** All-in-one formatter. Return the JSON encoding of formatted text. *)
+val to_json : ?indent:int -> ?margin:int ->
+ (Format.formatter -> 'a -> unit) -> 'a -> json
+
+(** Buffer for encoding formatted text. *)
+type buffer
+
+(** Create a formatter with [~indent] maximum indentation and
+ [~margin] right-margin. Defaults are those of [Format.make_formatter],
+ which are [~indent:68] and [~margin:78] with OCaml 4.05. *)
+val create : ?indent:int -> ?margin:int -> unit -> buffer
+
+(** The underlying formatter of a buffer. *)
+val formatter : buffer -> Format.formatter
+
+(** Prints into the buffer's formatter. *)
+val bprintf : buffer -> ('a,Format.formatter,unit) format -> 'a
+
+val append : buffer -> string -> int -> int -> unit
+val flush : buffer -> unit -> unit
+val push_tag : buffer -> Format.tag -> unit
+val pop_tag : buffer -> Format.tag -> unit
+
+(** Flushes the buffer and returns its JSON enoding. This pops all pending
+ tags. *)
+val contents : buffer -> json
+
+(** Prints back a JSON encoding onto the provided formatter.
+ @raise Yojson.Basic.Util.Type_error in case of ill formatted buffer. *)
+val fprintf : Format.formatter -> json -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
new file mode 100644
index 0000000000000000000000000000000000000000..229c526ab6f75a73624235f3c09c42b5a4ed27e5
--- /dev/null
+++ b/src/plugins/server/kernel_ast.ml
@@ -0,0 +1,164 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+
+open Data
+module Sy = Syntax
+module Md = Markdown
+module Js = Yojson.Basic.Util
+open Cil_types
+
+let page = Doc.page `Kernel ~title:"Ast Services" ~filename:"ast.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Compute Ast --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"kernel.ast.compute"
+ ~descr:(Md.rm "Ensures that AST is computed")
+ ~input:(module Junit) ~output:(module Junit) Ast.compute
+
+(* -------------------------------------------------------------------------- *)
+(* --- Printers --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Tag =
+struct
+
+ open Printer_tag
+
+ type index = (string,localizable) Hashtbl.t
+
+ let kid = ref 0
+
+ let index () = Hashtbl.create 0
+
+ module TYPE : Datatype.S with type t = index =
+ Datatype.Make
+ (struct
+ type t = index
+ include Datatype.Undefined
+ let reprs = [index()]
+ let name = "Server.Jprinter.Index"
+ let mem_project = Datatype.never_any_project
+ end)
+
+ module STATE = State_builder.Ref(TYPE)
+ (struct
+ let name = "Server.Jprinter.State"
+ let dependencies = []
+ let default = index
+ end)
+
+ let of_stmt s = Printf.sprintf "#s%d" s.sid
+ let of_start s = Printf.sprintf "#k%d" s.sid
+ let of_varinfo v = Printf.sprintf "#v%d" v.vid
+
+ let create_tag = function
+ | PStmt(_,st) -> of_stmt st
+ | PStmtStart(_,st) -> of_start st
+ | PVDecl(_,_,vi) -> of_varinfo vi
+ | PLval _ -> Printf.sprintf "#l%d" (incr kid ; !kid)
+ | PExp _ -> Printf.sprintf "#e%d" (incr kid ; !kid)
+ | PTermLval _ -> Printf.sprintf "#t%d" (incr kid ; !kid)
+ | PGlobal _ -> Printf.sprintf "#g%d" (incr kid ; !kid)
+ | PIP _ -> Printf.sprintf "#p%d" (incr kid ; !kid)
+
+ let create item =
+ let tag = create_tag item in
+ let index = STATE.get () in
+ Hashtbl.add index tag item ; tag
+
+ let lookup = Hashtbl.find (STATE.get())
+
+end
+
+module PP = Printer_tag.Make(Tag)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Ast Data --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Stmt = Data.Collection
+ (struct
+ type t = stmt
+ let syntax = Sy.publish ~page ~name:"stmt"
+ ~synopsis:Sy.ident
+ ~descr:(Md.rm "Code statement identifier") ()
+ let to_json st = `String (Tag.of_stmt st)
+ let of_json js =
+ try
+ let open Printer_tag in
+ match Tag.lookup (Js.to_string js) with
+ | PStmt(_,st) -> st
+ | _ -> raise Not_found
+ with Not_found ->
+ Data.failure js "Unknown stmt id"
+ end)
+
+module Ki = Data.Collection
+ (struct
+ type t = kinstr
+ let syntax = Sy.union [ Sy.tag "global" ; Stmt.syntax ]
+ let to_json = function
+ | Kglobal -> `String "global"
+ | Kstmt st -> `String (Tag.of_stmt st)
+ let of_json = function
+ | `String "global" -> Kglobal
+ | js -> Kstmt (Stmt.of_json js)
+ end)
+
+module Kf = Data.Collection
+ (struct
+ type t = kernel_function
+ let syntax = Sy.publish ~page ~name:"fct-id"
+ ~synopsis:Sy.ident
+ ~descr:(Md.rm "Function identified by its global name.") ()
+ let to_json kf =
+ `String (Kernel_function.get_name kf)
+ let of_json js =
+ try Js.to_string js |> Globals.Functions.find_by_name
+ with Not_found -> Data.failure js "Undefined function"
+ end)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Functions --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"kernel.ast.getFunctions"
+ ~descr:(Md.rm "Collect all functions in the AST")
+ ~input:(module Junit) ~output:(module Kf.Jlist)
+ begin fun () ->
+ let pool = ref [] in
+ Globals.Functions.iter (fun kf -> pool := kf :: !pool) ;
+ List.rev !pool
+ end
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"kernel.ast.printFunction"
+ ~descr:(Md.rm "Print the AST of a function")
+ ~input:(module Kf) ~output:(module Jtext)
+ (fun kf -> Jbuffer.to_json PP.pp_global (Kernel_function.get_global kf))
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_ast.mli b/src/plugins/server/kernel_ast.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0b448e0e0bb89b4bd6ff46c94080022a91893f94
--- /dev/null
+++ b/src/plugins/server/kernel_ast.mli
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(* -------------------------------------------------------------------------- *)
+(** Ast Data *)
+(* -------------------------------------------------------------------------- *)
+
+module PP : Printer_tag.S_pp
+module Kf : Data.S_collection with type t = kernel_function
+module Ki : Data.S_collection with type t = kinstr
+module Stmt : Data.S_collection with type t = stmt
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_main.ml b/src/plugins/server/kernel_main.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4cfd33596d14017a5ea0e0584435616387d44b84
--- /dev/null
+++ b/src/plugins/server/kernel_main.ml
@@ -0,0 +1,215 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Data
+module Sy = Syntax
+module Md = Markdown
+module Senv = Server_parameters
+
+(* -------------------------------------------------------------------------- *)
+(* --- Frama-C Kernel Services --- *)
+(* -------------------------------------------------------------------------- *)
+
+let page = Doc.page `Kernel ~title:"Kernel Services" ~filename:"kernel.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Config --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ let get_config = Request.signature
+ ~page ~kind:`GET ~name:"kernel.getConfig"
+ ~descr:(Md.rm "Frama-C Kernel configuration")
+ ~input:(module Junit) () in
+ let result name descr =
+ Request.result get_config ~name ~descr:(Md.rm descr) (module Jstring) in
+ let set_version = result "version" "Frama-C version" in
+ let set_datadir = result "datadir" "Shared directory (FRAMAC_SHARE)" in
+ let set_libdir = result "libdir" "Lib directory (FRAMAC_LIB)" in
+ let set_pluginpath = Request.result get_config
+ ~name:"pluginpath" ~descr:(Md.rm "Plugin directories (FRAMAC_PLUGIN)")
+ (module Jstring.Jlist) in
+ Request.register_sig get_config
+ begin fun rq () ->
+ set_version rq Config.version ;
+ set_datadir rq Config.datadir ;
+ set_libdir rq Config.libdir ;
+ set_pluginpath rq Config.plugin_dir ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- 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.rm "Source file positions.")
+ ~details:(Md.praw "The file path is normalized, \
+ and the line number starts at one.") ()
+
+ let to_json p = `Assoc [
+ "file" , `String (p.Filepath.pos_path :> string) ;
+ "line" , `Int p.Filepath.pos_lnum ;
+ ]
+
+ 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 js "Invalid source format"
+
+end
+
+module LogSource = Collection(RawSource)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Log Lind --- *)
+(* -------------------------------------------------------------------------- *)
+
+module RawKind =
+struct
+ type t = Log.kind
+ let page = page
+ let name = "kind"
+ let descr = Md.rm "Frama-C message category."
+ let values = [
+ Log.Error, "ERROR", Md.rm "User Error" ;
+ Log.Warning, "WARNING", Md.rm "User Warning" ;
+ Log.Feedback, "FEEDBACK", Md.rm "Analyzer Feedback" ;
+ Log.Result, "RESULT", Md.rm "Analyzer Result" ;
+ Log.Failure, "FAILURE", Md.rm "Analyzer Failure" ;
+ Log.Debug, "DEBUG", Md.rm "Analyser Debug" ;
+ ]
+end
+
+module LogKind = Dictionary(RawKind)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Log Events --- *)
+(* -------------------------------------------------------------------------- *)
+
+module RawEvent =
+struct
+
+ module R = Record
+ (struct
+ let page = page
+ let name = "log"
+ let descr = Md.rm "Message event record."
+ end)
+
+ let syntax = R.syntax
+
+ let descr = Md.rm
+ let kind = R.field "kind" ~descr:(descr "Message kind") (module LogKind)
+ let plugin = R.field "plugin" ~descr:(descr "Emitter plugin") (module Jstring)
+ let message = R.field "message" ~descr:(descr "Message text") (module Jstring)
+
+ let category = R.option "category"
+ ~descr:(descr "Message category (DEBUG or WARNING)")
+ (module Jstring)
+
+ let source = R.option "source" ~descr:(descr "Source file position")
+ (module LogSource)
+
+ type t = Log.event
+
+ 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)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Log Monitoring --- *)
+(* -------------------------------------------------------------------------- *)
+
+let monitoring = ref false
+let monitored = ref false
+let events : Log.event Queue.t = Queue.create ()
+
+let monitor flag =
+ if flag != !monitoring then
+ ( if flag then
+ Senv.feedback "Start logs monitoring."
+ else
+ Senv.feedback "Stop logs monitoring." ) ;
+ monitoring := flag ;
+ if !monitoring && not !monitored then
+ begin
+ monitored := true ;
+ Log.add_listener (fun evt -> if !monitoring then Queue.add evt events)
+ end
+
+let monitor_logs () = monitor (Senv.Log.get ())
+
+let monitor_server activity =
+ if activity then monitor true else monitor_logs ()
+
+let () =
+ Main.on monitor_server ;
+ Cmdline.run_after_configuring_stage monitor_logs
+
+(* -------------------------------------------------------------------------- *)
+(* --- Log Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Request.register
+ ~page ~kind:`SET ~name:"kernel.setLogs"
+ ~descr:(Md.rm "Turn logs monitoring on/off")
+ ~input:(module Jbool) ~output:(module Junit) monitor
+
+let () = Request.register
+ ~page ~kind:`GET ~name:"kernel.getLogs"
+ ~descr:(Md.rm "Flush the last emitted logs since last call (max 100)")
+ ~input:(module Junit) ~output:(module LogEvent.Jlist)
+ begin fun () ->
+ let pool = ref [] in
+ let count = ref 100 in
+ while not (Queue.is_empty events) && !count > 0 do
+ decr count ;
+ pool := Queue.pop events :: !pool
+ done ;
+ List.rev !pool
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_main.mli b/src/plugins/server/kernel_main.mli
new file mode 100644
index 0000000000000000000000000000000000000000..726d654e626ac7c69a35f08b97cc75ca6f60a33c
--- /dev/null
+++ b/src/plugins/server/kernel_main.mli
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Kernel Services *)
+(* -------------------------------------------------------------------------- *)
+
+module LogSource : Data.S_collection with type t = Filepath.position
+module LogEvent : Data.S_collection with type t = Log.event
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_project.ml b/src/plugins/server/kernel_project.ml
new file mode 100644
index 0000000000000000000000000000000000000000..883cea34f37b7ec3b8725d2c62282b14c07d22d9
--- /dev/null
+++ b/src/plugins/server/kernel_project.ml
@@ -0,0 +1,123 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Data
+module Sy = Syntax
+module Md = Markdown
+module Js = Yojson.Basic.Util
+
+let page = Doc.page `Kernel ~title:"Project Management" ~filename:"project.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Project Info --- *)
+(* -------------------------------------------------------------------------- *)
+
+module ProjectInfo =
+ Collection
+ (struct
+ type t = Project.t
+
+ let syntax = Sy.publish ~page ~name:"project-info"
+ ~descr:(Md.rm "Project informations")
+ ~synopsis:Sy.(record[ "id",ident; "name",string; "current",boolean ])
+ ()
+
+ let of_json js =
+ Js.member "id" js |> Js.to_string |> Project.from_unique_name
+
+ let to_json p =
+ `Assoc [
+ "id", `String (Project.get_unique_name p) ;
+ "name", `String (Project.get_name p) ;
+ "current", `Bool (Project.is_current p) ;
+ ]
+ end)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Project Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+module ProjectRequest =
+struct
+
+ type t = Project.t * string * json
+
+ let syntax = Sy.publish ~page ~name:"project-request"
+ ~synopsis:(Sy.(record[ "project",ident; "request",string; "data",any; ]))
+ ~descr:(Md.rm "Request to be executed on the specified project.") ()
+
+ let of_json js =
+ begin
+ Project.from_unique_name Js.(member "project" js |> to_string) ,
+ Js.(member "request" js |> to_string) ,
+ Js.(member "data" js)
+ end
+
+ let process kind (project,request,data) =
+ match Main.find request with
+ | Some(kd,handler) when kd = kind -> Project.on project handler data
+ | Some _ -> failwith (Printf.sprintf "Incompatible kind for '%s'" request)
+ | None -> failwith (Printf.sprintf "Request '%s' undefined" request)
+
+end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Project Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"kernel.project.getCurrent"
+ ~descr:(Md.rm "Returns the current project")
+ ~input:(module Junit) ~output:(module ProjectInfo)
+ Project.current
+
+let () = Request.register ~page
+ ~kind:`SET ~name:"kernel.project.setCurrent"
+ ~descr:(Md.rm "Switches the current project")
+ ~input:(module Jident) ~output:(module Junit)
+ (fun pid -> Project.(set_current (from_unique_name pid)))
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"kernel.project.getList"
+ ~descr:(Md.rm "Returns the list of all projects")
+ ~input:(module Junit) ~output:(module ProjectInfo.Jlist)
+ (fun () -> Project.fold_on_projects (fun ids p -> p :: ids) [])
+
+let () = Request.register ~page
+ ~kind:`GET ~name:"kernel.project.getOn"
+ ~descr:(Md.rm "Execute a GET request within the given project")
+ ~input:(module ProjectRequest) ~output:(module Jany)
+ (ProjectRequest.process `GET)
+
+let () = Request.register ~page
+ ~kind:`SET ~name:"kernel.project.setOn"
+ ~descr:(Md.rm "Execute a SET request within the given project")
+ ~input:(module ProjectRequest) ~output:(module Jany)
+ (ProjectRequest.process `SET)
+
+let () = Request.register ~page
+ ~kind:`EXEC ~name:"kernel.project.execOn"
+ ~descr:(Md.rm "Execute an EXEC request within the given project")
+ ~input:(module ProjectRequest) ~output:(module Jany)
+ (ProjectRequest.process `EXEC)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/kernel_project.mli b/src/plugins/server/kernel_project.mli
new file mode 100644
index 0000000000000000000000000000000000000000..975e1e094f80f095534935294154b22ef3d95979
--- /dev/null
+++ b/src/plugins/server/kernel_project.mli
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Data
+
+(* -------------------------------------------------------------------------- *)
+(** Project Services *)
+(* -------------------------------------------------------------------------- *)
+
+module ProjectInfo : Data.S with type t = Project.t
+module ProjectRequest : Request.Input with type t = Project.t * string * json
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/main.ml b/src/plugins/server/main.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2602e89fe5f4b7cef908529ccf56db56f41dc3ad
--- /dev/null
+++ b/src/plugins/server/main.ml
@@ -0,0 +1,300 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server Main Process --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Senv = Server_parameters
+
+let option f = function None -> () | Some x -> f x
+
+(* -------------------------------------------------------------------------- *)
+(* --- Registry --- *)
+(* -------------------------------------------------------------------------- *)
+
+type kind = [ `GET | `SET | `EXEC ]
+let string_of_kind = function `GET -> "GET" | `SET -> "SET" | `EXEC -> "EXEC"
+let pp_kind fmt kd = Format.pp_print_string fmt (string_of_kind kd)
+
+let registry = Hashtbl.create 32
+
+let register (kind : kind) request handler =
+ if Hashtbl.mem registry request then
+ Server_parameters.failure "Request '%s' already registered" request
+ else
+ Hashtbl.add registry request (kind,handler)
+
+let find request =
+ try Some (Hashtbl.find registry request)
+ with Not_found -> None
+
+let exec request data = (snd (Hashtbl.find registry request)) data
+
+(* -------------------------------------------------------------------------- *)
+(* --- Public API --- *)
+(* -------------------------------------------------------------------------- *)
+
+type json = Json.t
+
+type 'a request = [
+ | `Poll
+ | `Request of 'a * string * json
+ | `Kill of 'a
+ | `Shutdown
+]
+
+type 'a response = [
+ | `Data of 'a * json
+ | `Error of 'a * string
+ | `Killed of 'a
+ | `Rejected of 'a
+]
+
+type 'a message = {
+ requests : 'a request list ;
+ callback : 'a response list -> unit ;
+}
+
+(* Private API: *)
+
+type 'a exec = {
+ id : 'a ;
+ request : string ;
+ data : json ;
+ handler : json -> json ;
+ yield : bool ;
+ mutable killed : bool ;
+}
+
+type 'a server = {
+ rate : int ;
+ pretty : Format.formatter -> 'a -> unit ;
+ equal : 'a -> 'a -> bool ;
+ fetch : unit -> 'a message option ;
+ q_in : 'a exec Queue.t ;
+ q_out : 'a response Stack.t ;
+ mutable shutdown : bool ;
+ mutable coins : int ;
+ mutable running : 'a exec option ;
+}
+
+exception Killed
+
+(* -------------------------------------------------------------------------- *)
+(* --- Debug --- *)
+(* -------------------------------------------------------------------------- *)
+
+let pp_request pp fmt (r : _ request) =
+ match r with
+ | `Poll -> Format.fprintf fmt "Poll"
+ | `Shutdown -> Format.fprintf fmt "Shutdown"
+ | `Kill id -> Format.fprintf fmt "Kill %a" pp id
+ | `Request(id,request,data) ->
+ if Senv.debug_atleast 2 then
+ Format.fprintf fmt "@[<hov 2>Request %s:%a@ %a@]"
+ request pp id Data.pretty data
+ else
+ Format.fprintf fmt "Request %s:%a" request pp id
+
+let pp_response pp fmt (r : _ response) =
+ match r with
+ | `Error(id,err) -> Format.fprintf fmt "Error %a: %s" pp id err
+ | `Rejected id -> Format.fprintf fmt "Rejected %a" pp id
+ | `Killed id -> Format.fprintf fmt "Killed %a" pp id
+ | `Data(id,data) ->
+ if Senv.debug_atleast 2 then
+ Format.fprintf fmt "@[<hov 2>Response %a@ %a@]"
+ pp id Data.pretty data
+ else
+ Format.fprintf fmt "Response %a" pp id
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request Handling --- *)
+(* -------------------------------------------------------------------------- *)
+
+let no_yield () = ()
+
+let execute yield exec : _ response =
+ let db = !Db.progress in
+ try
+ Db.progress := if exec.yield then yield else no_yield ;
+ let data = exec.handler exec.data in
+ Db.progress := db ; `Data(exec.id,data)
+ with
+ | Killed -> Db.progress := db ; `Killed exec.id
+ | exn ->
+ Db.progress := db ;
+ Senv.warning "[%s] Uncaught exception:@\n%s"
+ exec.request (Cmdline.protect exn) ;
+ `Error(exec.id,Printexc.to_string exn)
+
+let execute_debug pp yield exec =
+ if Senv.debug_atleast 1 then
+ Senv.debug "Trigger %s:%a" exec.request pp exec.id ;
+ execute yield exec
+
+let reply_debug server resp =
+ if Senv.debug_atleast 1 then
+ Senv.debug "%a" (pp_response server.pretty) resp ;
+ Stack.push resp server.q_out
+
+(* -------------------------------------------------------------------------- *)
+(* --- Processing Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+let raise_if_killed = function { killed } -> if killed then raise Killed
+let kill_exec e = e.killed <- true
+let kill_request eq id e = if eq id e.id then e.killed <- true
+
+let process_request (server : 'a server) (request : 'a request) : unit =
+ if Senv.debug_atleast 1 then
+ Senv.debug "%a" (pp_request server.pretty) request ;
+ match request with
+ | `Poll -> ()
+ | `Shutdown ->
+ begin
+ option kill_exec server.running ;
+ Queue.clear server.q_in ;
+ Stack.clear server.q_out ;
+ server.shutdown <- true ;
+ end
+ | `Kill id ->
+ begin
+ let kill = kill_request server.equal id in
+ Queue.iter kill server.q_in ;
+ option kill server.running ;
+ end
+ | `Request(id,request,data) ->
+ begin
+ match find request with
+ | None -> reply_debug server (`Rejected id)
+ | Some( `GET , handler ) ->
+ let exec = { id ; request ; handler ; data ;
+ yield = false ; killed = false } in
+ reply_debug server (execute no_yield exec)
+ | Some( `SET , handler ) ->
+ let exec = { id ; request ; handler ; data ;
+ yield = false ; killed = false } in
+ Queue.push exec server.q_in
+ | Some( `EXEC , handler ) ->
+ let exec = { id ; request ; handler ; data ;
+ yield = true ; killed = false } in
+ Queue.push exec server.q_in
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Fetching a Bunck of Messages --- *)
+(* -------------------------------------------------------------------------- *)
+
+let communicate server =
+ match server.fetch () with
+ | None -> false
+ | Some message ->
+ let error =
+ try List.iter (process_request server) message.requests ; None
+ with exn -> Some exn in (* re-raised after message reply *)
+ let pool = ref [] in
+ Stack.iter (fun r -> pool := r :: !pool) server.q_out ;
+ Stack.clear server.q_out ;
+ message.callback !pool ;
+ option raise error ; true
+
+(* -------------------------------------------------------------------------- *)
+(* --- Yielding --- *)
+(* -------------------------------------------------------------------------- *)
+
+let do_yield server () =
+ begin
+ option raise_if_killed server.running ;
+ let n = server.coins in
+ if n < server.rate then
+ server.coins <- succ n
+ else
+ ( server.coins <- 0 ; ignore ( communicate server ) ) ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- One Step Process --- *)
+(* -------------------------------------------------------------------------- *)
+
+let rec fetch_exec q =
+ if Queue.is_empty q then None
+ else
+ let e = Queue.pop q in
+ if e.killed then fetch_exec q else Some e
+
+let process server =
+ match fetch_exec server.q_in with
+ | None -> communicate server
+ | Some exec ->
+ server.running <- Some exec ;
+ try
+ reply_debug server (execute_debug server.pretty (do_yield server) exec) ;
+ server.running <- None ;
+ true
+ with exn ->
+ server.running <- None ;
+ raise exn
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server Main Loop --- *)
+(* -------------------------------------------------------------------------- *)
+
+let in_range ~min:a ~max:b v = min (max a v) b
+
+let kill () = raise Killed
+let yield () = !Db.progress ()
+
+let demons = ref []
+let on callback = demons := !demons @ [ callback ]
+let signal activity =
+ List.iter (fun f -> try f activity with _ -> ()) !demons
+
+let run ~pretty ?(equal=(=)) ~fetch () =
+ begin
+ let rate = in_range ~min:1 ~max:200 (Senv.Rate.get ()) in
+ let idle_ms = in_range ~min:1 ~max:2000 (Senv.Idle.get ()) in
+ let idle_s = float_of_int idle_ms /. 1000.0 in
+ let server = {
+ fetch ; coins = 0 ; rate ; equal ; pretty ;
+ q_in = Queue.create () ;
+ q_out = Stack.create () ;
+ running = None ;
+ shutdown = false ;
+ } in
+ try
+ signal true ;
+ Senv.feedback "Server running." ;
+ while not server.shutdown do
+ let activity = process server in
+ if not activity then Unix.sleepf idle_s ;
+ done ;
+ Senv.feedback "Server shutdown." ;
+ signal false ;
+ with err ->
+ Senv.feedback "Server interruped (fatal error)." ;
+ signal false ;
+ raise err
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/main.mli b/src/plugins/server/main.mli
new file mode 100644
index 0000000000000000000000000000000000000000..721291d96e9b93c4d65676fb83b216fafba39bd7
--- /dev/null
+++ b/src/plugins/server/main.mli
@@ -0,0 +1,96 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Server Main Process *)
+(* -------------------------------------------------------------------------- *)
+
+type json = Json.t
+type kind = [ `GET | `SET | `EXEC ]
+val string_of_kind : kind -> string
+val pp_kind : Format.formatter -> kind -> unit
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Request Registry} *)
+(* -------------------------------------------------------------------------- *)
+
+val register : kind -> string -> (json -> json) -> unit
+val find : string -> (kind * (json -> json)) option
+val exec : string -> json -> json (** @raises Not_found if not registered *)
+
+(* -------------------------------------------------------------------------- *)
+(** {2 Server Main Process} *)
+(* -------------------------------------------------------------------------- *)
+
+(** Type of request messages.
+ Parametrized by the type of request identifiers. *)
+type 'a request = [
+ | `Poll
+ | `Request of 'a * string * json
+ | `Kill of 'a
+ | `Shutdown
+]
+
+(** Type of response messages.
+ Parametrized by the type of request identifiers. *)
+type 'a response = [
+ | `Data of 'a * json
+ | `Error of 'a * string
+ | `Killed of 'a
+ | `Rejected of 'a
+]
+
+(** A paired request-response message.
+ The callback will be called exactly once for each received message. *)
+type 'a message = {
+ requests : 'a request list ;
+ callback : 'a response list -> unit ;
+}
+
+(**
+ Run a server with the provided low-level network primitives to
+ actually exchange data.
+
+ The function does not return until the server is explicitely
+ Shutdown. Logs are monitored unless [~logs:false] is specified.
+
+ Default equality is the standard `(=)` one.
+*)
+val run :
+ pretty:(Format.formatter -> 'a -> unit) ->
+ ?equal:('a -> 'a -> bool) ->
+ fetch:(unit -> 'a message option) ->
+ unit -> unit
+
+(** Yield the server during the currently running request.
+ Actually, calls [!Db.progress()]. *)
+val yield : unit -> unit
+
+(** Kills the currently running request. Actually raises an exception. *)
+val kill : unit -> 'a
+
+(** Register a callback to listen for server activity.
+ All callbacks would be executed in their order of registration.
+ They shall {i never} raise any exception. *)
+val on : (bool -> unit) -> unit
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/request.ml b/src/plugins/server/request.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b355b3907879b1e91eef4345b217d39680fb98bc
--- /dev/null
+++ b/src/plugins/server/request.ml
@@ -0,0 +1,331 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Senv = Server_parameters
+module Jutil = Yojson.Basic.Util
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request Registry --- *)
+(* -------------------------------------------------------------------------- *)
+
+type json = Data.json
+type kind = [ `GET | `SET | `EXEC ]
+
+module type Input =
+sig
+ type t
+ val syntax : Syntax.t
+ val of_json : json -> t
+end
+
+module type Output =
+sig
+ type t
+ val syntax : Syntax.t
+ val to_json : t -> json
+end
+
+type 'a input = (module Input with type t = 'a)
+type 'a output = (module Output with type t = 'a)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Sanity Checks --- *)
+(* -------------------------------------------------------------------------- *)
+
+let re_set = Str.regexp_string_case_fold "SET"
+let re_get = Str.regexp_case_fold "\\(GET\\|PRINT\\)"
+let re_exec = Str.regexp_case_fold "\\(EXEC\\|COMPUTE\\)"
+let re_name = Str.regexp_case_fold "[a-zA-Z0-9.]+$"
+
+let wpage = Senv.register_warn_category "inconsistent-page"
+let wkind = Senv.register_warn_category "inconsistent-kind"
+
+let check_name name =
+ if not (Str.string_match re_name name 0) then
+ Senv.warning ~wkey:Senv.wname
+ "Request %S is not a dot-separated list of (camlCased) identifiers" name
+
+let check_plugin plugin name =
+ let p = String.lowercase_ascii plugin in
+ let n = String.lowercase_ascii name in
+ let k = String.length plugin in
+ if not (String.length name > k &&
+ String.sub n 0 k = p &&
+ String.get n k = '.')
+ then
+ Senv.warning ~wkey:wpage
+ "Request '%s' shall be named « %s.* »"
+ name (String.capitalize_ascii plugin)
+
+let check_page page name =
+ match Doc.chapter page with
+ | `Kernel -> check_plugin "kernel" name
+ | `Plugin plugin -> check_plugin plugin name
+ | `Protocol ->
+ Senv.warning ~wkey:wkind
+ "Request '%s' shall not be published in protocol pages" name
+
+let check_kind kind name =
+ let re,key = match kind with
+ | `GET -> re_get , "get|print"
+ | `SET -> re_set , "set"
+ | `EXEC -> re_exec , "exec|compute"
+ in try ignore (Str.search_forward re name 0) with Not_found ->
+ Senv.warning "Request '%s' shall be named with « %s »"
+ name key
+
+(* -------------------------------------------------------------------------- *)
+(* --- Multiple Fields Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Fmap = Map.Make(String)
+
+type rq = {
+ mutable param : json Fmap.t ;
+ mutable result : json Fmap.t ;
+}
+
+let fmap_of_json r js =
+ List.fold_left
+ (fun r (fd,js) -> Fmap.add fd js r)
+ r (Jutil.to_assoc js)
+
+let fmap_to_json r =
+ `Assoc (Fmap.fold (fun fd js r -> (fd,js)::r) r [])
+
+type 'a param = rq -> 'a
+type 'a result = rq -> 'a -> unit
+
+(* -------------------------------------------------------------------------- *)
+(* --- Input/Output Request Processing --- *)
+(* -------------------------------------------------------------------------- *)
+
+type _ rq_input =
+ | Pnone
+ | Pdata : 'a input -> 'a rq_input
+ | Pfields : Syntax.field list -> unit rq_input
+
+type _ rq_output =
+ | Rnone
+ | Rdata : 'a output -> 'a rq_output
+ | Rfields : Syntax.field list -> unit rq_output
+
+(* json input syntax *)
+let sy_input (type a) (input : a rq_input) : Syntax.t =
+ match input with
+ | Pnone -> assert false
+ | Pdata d -> let module D = (val d) in D.syntax
+ | Pfields _ -> Syntax.record []
+
+(* json output syntax *)
+let sy_output (type b) (output : b rq_output) : Syntax.t =
+ match output with
+ | Rnone -> assert false
+ | Rdata d -> let module D = (val d) in D.syntax
+ | Rfields _ -> Syntax.record []
+
+(* json input documentation *)
+let doc_input (type a) (input : a rq_input) : Markdown.block =
+ match input with
+ | Pnone -> assert false
+ | Pdata _ -> Markdown.empty
+ | Pfields fs -> Syntax.fields ~title:"Input" (List.rev fs)
+
+(* json output syntax *)
+let doc_output (type b) (output : b rq_output) : Markdown.block =
+ match output with
+ | Rnone -> assert false
+ | Rdata _ -> Markdown.empty
+ | Rfields fs -> Syntax.fields ~title:"Output" (List.rev fs)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Multi-Parameters Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+type ('a,'b) signature = {
+ page : Doc.page ;
+ kind : kind ;
+ name : string ;
+ descr : Markdown.text ;
+ details : Markdown.block ;
+ mutable defined : bool ;
+ mutable defaults : json Fmap.t ;
+ mutable required : string list ;
+ mutable input : 'a rq_input ;
+ mutable output : 'b rq_output ;
+}
+
+let failure_missing fmap name =
+ Data.failure (fmap_to_json fmap) "Missing parameter '%s'" name
+
+let check_required fmap fd =
+ if not (Fmap.mem fd fmap) then failure_missing fmap fd
+
+(* -------------------------------------------------------------------------- *)
+(* --- Named Input Parameters Definitions --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* current input fields *)
+let fds_input s : Syntax.field list =
+ if s.defined then Senv.failure "Request '%s' has been finalized." s.name ;
+ match s.input with
+ | Pdata _ ->
+ Senv.fatal "Can not define named parameters for request '%s'" s.name
+ | Pnone -> []
+ | Pfields fds -> fds
+
+let param (type a b) (s : (unit,b) signature) ~name ~descr
+ ?default (input : a input) : a param =
+ let module D = (val input) in
+ let syntax = if default = None then D.syntax else Syntax.option D.syntax in
+ let fd = Syntax.{ name ; syntax ; descr } in
+ s.input <- Pfields (fd :: fds_input s) ;
+ fun rq ->
+ try D.of_json (Fmap.find name rq.param)
+ with Not_found ->
+ match default with
+ | None -> failure_missing rq.param name
+ | Some v -> v
+
+let param_opt (type a b) (s : (unit,b) signature) ~name ~descr
+ (input : a input) : a option param =
+ let module D = (val input) in
+ let fd = Syntax.{ name ; syntax = Syntax.option D.syntax ; descr } in
+ s.input <- Pfields (fd :: fds_input s) ;
+ fun rq ->
+ try Some(D.of_json (Fmap.find name rq.param))
+ with Not_found -> None
+
+(* -------------------------------------------------------------------------- *)
+(* --- Named Output Parameters Definitions --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* current output fields *)
+let fds_output s : Syntax.field list =
+ if s.defined then Senv.failure "Request '%s' has been finalized." s.name ;
+ match s.output with
+ | Rdata _ -> Senv.fatal "Can not define named results request '%s'" s.name
+ | Rnone -> []
+ | Rfields fds -> fds
+
+let result (type a b) (s : (a,unit) signature) ~name ~descr
+ ?default (output : b output) : b result =
+ let module D = (val output) in
+ let fd = Syntax.{ name ; syntax = D.syntax ; descr } in
+ s.output <- Rfields (fd :: fds_output s) ;
+ begin
+ match default with
+ | None -> s.required <- name :: s.required
+ | Some v -> s.defaults <- Fmap.add name (D.to_json v) s.defaults
+ end ;
+ fun rq v -> rq.result <- Fmap.add name (D.to_json v) rq.result
+
+let result_opt (type a b) (s : (a,unit) signature) ~name ~descr
+ (output : b output) : b option result =
+ let module D = (val output) in
+ let fd = Syntax.{ name ; syntax = option D.syntax ; descr } in
+ s.output <- Rfields (fd :: fds_output s) ;
+ fun rq opt ->
+ match opt with None -> () | Some v ->
+ rq.result <- Fmap.add name (D.to_json v) rq.result
+
+(* -------------------------------------------------------------------------- *)
+(* --- Opened Signature Definition --- *)
+(* -------------------------------------------------------------------------- *)
+
+let signature
+ ~page ~kind ~name ~descr ?(details=Markdown.empty)
+ ?input ?output () =
+ check_name name ;
+ check_page page name ;
+ check_kind kind name ;
+ let input = match input with None -> Pnone | Some d -> Pdata d in
+ let output = match output with None -> Rnone | Some d -> Rdata d in
+ {
+ page ; kind ; name ; descr ; details ;
+ defaults = Fmap.empty ; required = [] ;
+ input ; output ; defined = false ;
+ }
+
+(* -------------------------------------------------------------------------- *)
+(* --- Opened Signature Process --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* json input processing *)
+let mk_input (type a) name defaults (input : a rq_input) : (rq -> json -> a) =
+ match input with
+ | Pnone -> Senv.fatal "No input defined for request '%s'" name
+ | Pdata d ->
+ let module D = (val d) in
+ (fun rq js -> rq.result <- defaults ; D.of_json js)
+ | Pfields _ ->
+ (fun rq js -> rq.param <- fmap_of_json rq.param js)
+
+(* json output processing *)
+let mk_output (type b) name required (output : b rq_output) : (rq -> b -> json) =
+ match output with
+ | Rnone -> Senv.fatal "No output defined for request '%s'" name
+ | Rdata d ->
+ let module D = (val d) in (fun _rq v -> D.to_json v)
+ | Rfields _ ->
+ (fun rq () ->
+ List.iter (check_required rq.result) required ;
+ fmap_to_json rq.result)
+
+let register_sig (type a b) (s : (a,b) signature) (process : rq -> a -> b) =
+ if s.defined then
+ Senv.fatal "Request '%s' is defined twice" s.name ;
+ let input = mk_input s.name s.defaults s.input in
+ let output = mk_output s.name s.required s.output in
+ let processor js =
+ let rq = { param = Fmap.empty ; result = Fmap.empty } in
+ js |> input rq |> process rq |> output rq
+ in
+ let skind = Main.string_of_kind s.kind in
+ let title = Printf.sprintf "`%s` %s" skind s.name in
+ let synopsis =
+ Markdown.table
+ [`Center "Input" ; `Center "Output" ]
+ [[ Syntax.format @@ sy_input s.input ;
+ Syntax.format @@ sy_output s.output ]] in
+ let content =
+ Markdown.concat [
+ Markdown.par s.descr ;
+ synopsis ;
+ s.details ;
+ doc_input s.input ;
+ doc_output s.output ;
+ ] in
+ let _ = Doc.publish ~page:s.page ~name:s.name ~title content [] in
+ Main.register s.kind s.name processor ;
+ s.defined <- true
+
+(* -------------------------------------------------------------------------- *)
+(* --- Request Registration --- *)
+(* -------------------------------------------------------------------------- *)
+
+let register ~page ~kind ~name ~descr ?details ~input ~output process =
+ register_sig
+ (signature ~page ~kind ~name ~descr ?details ~input ~output ())
+ (fun _rq v -> process v)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/request.mli b/src/plugins/server/request.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c855405cb85088b1d88e60660a5a6e86e268493e
--- /dev/null
+++ b/src/plugins/server/request.mli
@@ -0,0 +1,195 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** Request Registry *)
+(* -------------------------------------------------------------------------- *)
+
+type json = Data.json
+type kind = [ `GET | `SET | `EXEC ]
+
+module type Input =
+sig
+ type t
+ val syntax : Syntax.t
+ val of_json : json -> t
+end
+
+module type Output =
+sig
+ type t
+ val syntax : Syntax.t
+ val to_json : t -> json
+end
+
+type 'a input = (module Input with type t = 'a)
+type 'b output = (module Output with type t = 'b)
+
+(** {2 Simple Requests Registration} *)
+
+(** Register a simple request of type [(a -> b)].
+
+ Name, page and kind must be consistent with each others:
+ - No publication on [`Protocol] pages
+ - Kernel requests shall starts with ["Kernel.*"]
+ - Plugin requests shall starts with ["<Plugin>.*"]
+ - SET requests must contain ["set"] (case insensitive)
+ - GET requests must contain ["get"] or ["print"] (case insensitive)
+ - EXEC requests must contain ["exec"] or ["compute"] (case insensitive)
+
+*)
+val register :
+ page:Doc.page ->
+ kind:kind ->
+ name:string ->
+ descr:Markdown.text ->
+ ?details:Markdown.block ->
+ input:'a input ->
+ output:'b output ->
+ ('a -> 'b) -> unit
+
+(** {2 Requests with Named Parameters}
+
+ The API below allows for creating requests with
+ named and optional parameters. Although such requests
+ could be defined with simple registration and {i record} datatypes,
+ the helpers below allow more flexibility and a better correspondance
+ between optional parameters and OCaml option types.
+
+ To register a request with named parameters and/or named results,
+ you first create a {i signature}. Then you define named
+ parameters and results, and finally you {i register} the processing
+ function:
+
+ {[
+ (* ---- Exemple of Request Registration --- *)
+ let () =
+ let s = Request.signature ~page ~kind ~name ~descr () in
+ let get_a = Request.param s ~name:"a" ~descr:"..." (module A) in
+ let get_b = Request.param s ~name:"b" ~descr:"..." (module B) in
+ let set_c = Request.result s ~name:"c" ~descr:"..." (module C) in
+ let set_d = Request.result s ~name:"d" ~descr:"..." (module D) in
+ Request.register_sig s
+ (fun rq () ->
+ let (c,d) = some_job (get_a rq) (get_b rq) in
+ set_c rq c ; set_d rq d)
+ ]}
+
+*)
+
+(** Under definition request signature. *)
+type ('a,'b) signature
+
+(** Create an opened request signature.
+ Depending on whether [~input] and [~output] datatype are provided,
+ you shall define named parameters and results before registering the
+ request processing function. *)
+val signature :
+ page:Doc.page ->
+ kind:kind ->
+ name:string ->
+ descr:Markdown.text ->
+ ?details:Markdown.block ->
+ ?input:'a input ->
+ ?output:'b output ->
+ unit -> ('a,'b) signature
+
+(** Request JSON parameters. *)
+type rq
+
+(** Named input parameter. *)
+type 'a param = rq -> 'a
+
+(** Named output parameter. *)
+type 'b result = rq -> 'b -> unit
+
+(** Register the request JSON processing function.
+ This call finalize the signature definition and shall be called
+ once on the signature. *)
+val register_sig : ('a,'b) signature -> (rq -> 'a -> 'b) -> unit
+
+(** {2 Named Parameters and Results}
+
+ The functions bellow must be called on a freshly created signature
+ {i before} its final registration. The obtained getters and setters
+ shall be only used within the registered process.
+
+ The correspondance between input/output JSON syntax and OCaml values
+ is summarized in the tables below.Abstract_domain
+
+ For named input parameters:
+ [
+
+ API: Input JSON OCaml Getter
+ -----------------------------------------------------------------------
+ Request.param { f: a } 'a (* might raise an exception *)
+ Request.param ~default { f: a? } 'a (* defined by default *)
+ Request.param_opt { f: a? } 'a option
+
+ ]
+
+
+ For named output parameters:
+ [
+
+ API: Input JSON OCaml Setter
+ ----------------------------------------------------------------------
+ Request.result { f: a } 'a (* shall be set by process *)
+ Request.result ~default { f: a } 'a (* defined by default *)
+ Request.result_opt { f: a? } 'a option
+
+ ]
+
+*)
+
+
+(** Named input parameter. If a default value is provided,
+ the JSON input field becomes optional. Otherwized, it is required. *)
+val param : (unit,'b) signature ->
+ name:string ->
+ descr:Markdown.text ->
+ ?default:'a ->
+ 'a input -> 'a param
+
+(** Named optional input parameter. *)
+val param_opt : (unit,'b) signature ->
+ name:string ->
+ descr:Markdown.text ->
+ 'a input -> 'a option param
+
+(** Named output parameter. If a default value is provided,
+ the JSON output field is initialized with it.
+ Otherwized, it shall be set at each invocation of the request processing
+ funciton. *)
+val result : ('a,unit) signature ->
+ name:string ->
+ descr:Markdown.text ->
+ ?default:'b ->
+ 'b output -> 'b result
+
+(** Named optional output parameter. The initial value is set to [None]. *)
+val result_opt : ('a,unit) signature ->
+ name:string ->
+ descr:Markdown.text ->
+ 'b output -> 'b option result
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_batch.ml b/src/plugins/server/server_batch.ml
new file mode 100644
index 0000000000000000000000000000000000000000..0aa3c03b310a2c1104baf91a712a17bd17a9f01b
--- /dev/null
+++ b/src/plugins/server/server_batch.ml
@@ -0,0 +1,106 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Only Compiled when package Zmq is installed *)
+(* No interface, registered via side-effects *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- ZeroMQ Server Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Senv = Server_parameters
+
+let batch_group = Senv.add_group "Protocol BATCH"
+
+let () = Parameter_customize.set_group batch_group
+module Batch = Senv.String_list
+ (struct
+ let option_name = "-server-batch"
+ let arg_name = "file.json,..."
+ let help =
+ "Executes all requests in each <file.json>, and save the \
+ associated results in <file.out.json>."
+ end)
+
+let _ = Doc.page `Protocol ~title:"Batch Protocol" ~filename:"server_batch.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- Execute JSON --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Js = Yojson.Basic
+module Ju = Yojson.Basic.Util
+
+let pretty = Js.pretty_print ~std:false
+
+let execute_command js =
+ let request = Ju.member "request" js |> Ju.to_string in
+ let id = Ju.member "id" js in
+ let data = Ju.member "data" js in
+ match Main.find request with
+ | None ->
+ Senv.error "[batch] %a: request %S not found" pretty id request ;
+ `Assoc [ "id" , id ; "error" , `String "request not found" ]
+ | Some (kind,handler) ->
+ try
+ Senv.feedback "[%a] %s" Main.pp_kind kind request ;
+ `Assoc [ "id" , id ; "data" , handler data ]
+ with Ju.Type_error(msg,js) ->
+ Senv.error "[%s] incorrect encoding:@\n%s@\n@[<hov 2>At: %a@]@."
+ request msg pretty js ;
+ `Assoc [ "id" , id ; "error" , `String msg ; "at" , js ]
+
+let rec execute_batch js =
+ match js with
+ | `Null -> `Null
+ | `List js -> `List (List.map execute_batch js)
+ | js ->
+ try execute_command js
+ with Ju.Type_error(msg,js) ->
+ Senv.error "[batch] incorrect encoding:@\n%s@\n@[<hov 2>At: %a@]@."
+ msg pretty js ;
+ `Null
+
+(* -------------------------------------------------------------------------- *)
+(* --- Execute the Scripts --- *)
+(* -------------------------------------------------------------------------- *)
+
+let execute () =
+ begin
+ List.iter
+ begin fun file ->
+ Senv.feedback "Script %S" file ;
+ let response = execute_batch (Js.from_file file) in
+ let output = Filename.remove_extension file ^ ".out.js" in
+ Senv.feedback "Output %S" output ;
+ Js.to_file output response ;
+ end
+ (Batch.get()) ;
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Run the Server from the Command line --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Db.Main.extend execute
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_parameters.ml b/src/plugins/server/server_parameters.ml
new file mode 100644
index 0000000000000000000000000000000000000000..76a572cdf0cbd164afcf0c948b5fec0f9f40e9a6
--- /dev/null
+++ b/src/plugins/server/server_parameters.ml
@@ -0,0 +1,70 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(* --- Server Plugin & Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module P = Plugin.Register
+ (struct
+ let name = "Server"
+ let shortname = "server"
+ let help = "Frama-C Request Server"
+ end)
+
+include P
+
+module Idle = P.Int
+ (struct
+ let option_name = "-server-idle"
+ let arg_name = "ms"
+ let default = 10
+ let help = "Waiting time (in milliseconds) when idle"
+ end)
+
+module Rate = P.Int
+ (struct
+ let option_name = "-server-rate"
+ let arg_name = "n"
+ let default = 100
+ let help = "Number of analysis steps between server communications"
+ end)
+
+module Doc = P.String
+ (struct
+ let option_name = "-server-doc"
+ let arg_name = "dir"
+ let default = ""
+ let help = "Output a markdown documentation of the server in <dir>"
+ end)
+
+module Log = P.False
+ (struct
+ let option_name = "-server-logs"
+ let help = "Start (or stop) monitoring logs"
+ end)
+
+let wpage = register_warn_category "inconsistent-page"
+let wkind = register_warn_category "inconsistent-kind"
+let wname = register_warn_category "invalid-name"
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/server_parameters.mli b/src/plugins/server/server_parameters.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5dc5ad153438ddc07353cb1b93cc59f22d4e91de
--- /dev/null
+++ b/src/plugins/server/server_parameters.mli
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Server Plugin & Options *)
+
+include Plugin.General_services
+
+module Idle : Parameter_sig.Int (** Idle waiting time (in ms) *)
+module Rate : Parameter_sig.Int (** Number of fetch per yield *)
+module Doc : Parameter_sig.String (** Generate documentation *)
+module Log : Parameter_sig.Bool (** Monitor logs *)
+
+val wpage : warn_category (** Inconsistent page warning *)
+val wkind : warn_category (** Inconsistent category warning *)
+val wname : warn_category (** Invalid name warning *)
+
+(**************************************************************************)
diff --git a/src/plugins/server/server_zmq.ml b/src/plugins/server/server_zmq.ml
new file mode 100644
index 0000000000000000000000000000000000000000..82d2ce4316762eb1f638f499c928eb15000d2442
--- /dev/null
+++ b/src/plugins/server/server_zmq.ml
@@ -0,0 +1,141 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* Only Compiled when package Zmq is installed *)
+(* No interface, registered via side-effects *)
+
+(* -------------------------------------------------------------------------- *)
+(* --- ZeroMQ Server Options --- *)
+(* -------------------------------------------------------------------------- *)
+
+module Senv = Server_parameters
+
+let zmq_group = Senv.add_group "Protocol ZeroMQ"
+
+let () = Parameter_customize.set_group zmq_group
+module Enabled = Senv.String
+ (struct
+ let option_name = "-server-zmq"
+ let arg_name = "url"
+ let default = ""
+ let help = "Establish a ZeroMQ server and listen for connections"
+ end)
+
+let _ = Doc.page `Protocol ~title:"ZeroMQ Protocol" ~filename:"server_zmq.md"
+
+(* -------------------------------------------------------------------------- *)
+(* --- ZMQ Context --- *)
+(* -------------------------------------------------------------------------- *)
+
+let context =
+ let zmq = ref None in
+ fun () ->
+ match !zmq with
+ | Some ctxt -> ctxt
+ | None ->
+ let major,minor,patch = Zmq.version () in
+ Senv.feedback "ZeroMQ %d.%d.%d" major minor patch ;
+ let ctxt = Zmq.Context.create () in
+ at_exit (fun () -> Zmq.Context.terminate ctxt) ;
+ zmq := Some ctxt ; ctxt
+
+(* -------------------------------------------------------------------------- *)
+(* --- Decoding Requests --- *)
+(* -------------------------------------------------------------------------- *)
+
+exception WrongEncoding of string
+
+let jdecode txt =
+ try Yojson.Basic.from_string txt
+ with exn ->
+ (* Exception if purely local from Yojson *)
+ raise (WrongEncoding (Printexc.to_string exn))
+
+let jencode js =
+ try Yojson.Basic.to_string ~std:false js
+ with exn ->
+ (* Exception if purely local from Yojson *)
+ raise (WrongEncoding (Printexc.to_string exn))
+
+let rec decode = function
+ | ("GET"|"SET"|"EXEC")::id::request::data :: w ->
+ `Request(id,request,jdecode data) :: decode w
+ | "KILL"::id:: w -> `Kill id :: decode w
+ | "POLL" :: w -> `Poll :: decode w
+ | "SHUTDOWN" :: _ -> [`Shutdown]
+ | cmd::_ -> raise (WrongEncoding cmd)
+ | [] -> []
+
+let rec encode = function
+ | `Data(id,data) :: w -> "DATA" :: id :: jencode data :: encode w
+ | `Error(id,msg) :: w -> "ERROR" :: id :: msg :: encode w
+ | `Killed id :: w -> "KILLED" :: id :: encode w
+ | `Rejected id :: w -> "REJECTED" :: id :: encode w
+ | [] -> []
+
+(* -------------------------------------------------------------------------- *)
+(* --- ZMQ Messages --- *)
+(* -------------------------------------------------------------------------- *)
+
+let callback socket responses =
+ try
+ let msg = encode responses in
+ Zmq.Socket.send_all socket (if msg = [] then ["NONE"] else msg)
+ with WrongEncoding msg ->
+ Zmq.Socket.send_all socket [ "WRONG" ; msg ]
+
+let fetch socket () =
+ try
+ let msg = Zmq.Socket.recv_all ~block:false socket in
+ try Some Main.{ requests = decode msg ; callback = callback socket }
+ with WrongEncoding msg ->
+ Zmq.Socket.send_all socket [ "WRONG" ; msg ] ; None
+ with
+ | Unix.Unix_error( Unix.EAGAIN , _ , _ ) -> None
+ | Zmq.ZMQ_exception(_,msg) -> Senv.fatal "ZeroMQ error: %s" msg
+
+(* -------------------------------------------------------------------------- *)
+(* --- Establish the Server --- *)
+(* -------------------------------------------------------------------------- *)
+
+let establish url =
+ if url <> "" then
+ begin
+ let context = context () in
+ let socket = Zmq.Socket.(create context rep) in
+ try
+ Zmq.Socket.bind socket url ;
+ Senv.feedback "ZeroMQ [%s]" url ;
+ Main.run ~pretty:Format.pp_print_string ~fetch:(fetch socket) () ;
+ Zmq.Socket.close socket ;
+ with exn ->
+ Zmq.Socket.close socket ;
+ raise exn
+ end
+
+(* -------------------------------------------------------------------------- *)
+(* --- Establish the Server from Command line --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () = Db.Main.extend (fun () -> establish (Enabled.get ()))
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/share/kernel/ast.md b/src/plugins/server/share/kernel/ast.md
new file mode 100644
index 0000000000000000000000000000000000000000..b5aaa2d57d7967f620d4cd9cc363691d9df7ddef
--- /dev/null
+++ b/src/plugins/server/share/kernel/ast.md
@@ -0,0 +1,15 @@
+# Ast Services
+
+The Frama-C internal representation of source files need to be computed before
+being accessed. This generally involves preprocessing of sources and finally
+parsing, typechecking and normalization.
+
+Although this step is generally performed silently on-demand inside Frama-C,
+from the Server point of view, this is a non-trivial procedure that should _not_ be
+triggered outside an `EXEC` request.
+
+Hence, most AST services might fail or return empty data if the AST has not been
+actually computed before. However, in typical usage of Frama-C from the
+command-line, the AST would have been computed just before any other plug-in,
+including the Server.
+
diff --git a/src/plugins/server/share/kernel/kernel.md b/src/plugins/server/share/kernel/kernel.md
new file mode 100644
index 0000000000000000000000000000000000000000..394e2a7b0e2a5aded0eae70c8f361c78afdf5401
--- /dev/null
+++ b/src/plugins/server/share/kernel/kernel.md
@@ -0,0 +1,21 @@
+# Kernel Services
+
+This section deals with requests related to the management
+of the Frama-C platform and services offered by the kernel.
+This covers several topics: configuration, logs.
+
+Configuration deals with versioning and resource directories.
+Project services allow to work with several Frama-C projects.
+
+Logs are automatically tracked by the server plug-in and queued.
+This monitoring can be controlled by `Kernel.SetLogs` command, but by
+default, monitoring is turned on as soon as some server is started
+(except for the batch server). The `Kernel.GetLogs` allow to flush this queue,
+with a maximum number of messages. Non-flushed messages
+can be recovered by subsequent calls, until the requests replies with an empty
+message set.
+
+However, logs emitted prior to the execution of a server, or after its shutdown,
+are _not_ collected by default. To enable this monitoring, for instance to collect
+messages before the server is started, you shall set the `-server-logs` option, which
+takes effect at configuration time (you can also use `... -then -server-logs ...`).
diff --git a/src/plugins/server/share/kernel/project.md b/src/plugins/server/share/kernel/project.md
new file mode 100644
index 0000000000000000000000000000000000000000..79715b8efc3e93df73d1943768f9394ddbc27f3c
--- /dev/null
+++ b/src/plugins/server/share/kernel/project.md
@@ -0,0 +1,17 @@
+# Project Management
+
+The Frama-C current project can be managed with the server requests provided below.
+
+## Current Project
+
+Initially, the current project is the one selected when the server starts.
+Hence, from the Frama-C command line, `-then-on <P> -server-xxx`
+would start the server with current project `<P>`.
+
+When modifying the current project through request `Kernel.Project.SetCurrent`,
+client shall wait for an acknowledgement before sending further `GET` requests.
+Otherwise, the `GET` might be executed on a different project, due to the
+asynchronous behavior of the server.
+
+However, it is still possible to execute a request on a specific project with
+`Kernel.Project.{Get|Set|Exec}On` requests.
diff --git a/src/plugins/server/share/kernel/text.md b/src/plugins/server/share/kernel/text.md
new file mode 100644
index 0000000000000000000000000000000000000000..b73c79016e9a72b0ed8c3873527b030b23f22161
--- /dev/null
+++ b/src/plugins/server/share/kernel/text.md
@@ -0,0 +1,47 @@
+# Rich Text Format
+
+In various place of the server, the Frama-C requests might return
+rich-text format, which is text annotated with special tags,
+for tagging or styling purpose.
+
+The JSON encoding of rich-text is defined by the _text_ type, which takes one
+of the following possible formats:
+
+| Format | Description |
+|:------:|:------------|
+| `"null"` | Empty text |
+| _string_ | Standard UTF-8 text |
+| `[` (_tag_`,`)? _text_`,`…`,` _text_ `]` | Sequence of text with an optional tag |
+
+Tags are simple strings, not to be printed, that encode the style or tag to
+apply on the sequence. Tags starting with a sharp (`"#…"`) must be understood as
+semantic tags, with a meaning depending on the context. Tags starting with
+a dot (`".…"`) shall be understood as style names. Other values must be understand
+as regular text.
+
+The empty tag (`""`) shall be ignored, but can used to group sequence of text
+together. Concatenation of sequence of text must be performed without any
+spacing or cut in the between.
+
+Text blocks can be nested. For instance, considerer the following JSON
+encoding:
+
+<pre>
+[
+ "This ",
+ [
+ "#frama-c-server-doc",
+ "Frama", [ ".tt", "-C" ], " server"
+ ],
+ " is ", [ ".it", "awesome" ], " isn't it?"
+]
+</pre>
+
+Provided the `#frama-c-server-doc` semantic is understood as a link to the
+main page of the Frama-C server documentation, the designated rich-text
+shall be printed as:
+
+> This [Frama-`C` server](../readme.md) is _awesome_ isn't it?
+
+The precise meaning of styles and semantic tags might depends on the context,
+and is detailed in each occurence of _text_ format.
diff --git a/src/plugins/server/share/protocol/server.md b/src/plugins/server/share/protocol/server.md
new file mode 100644
index 0000000000000000000000000000000000000000..1e479798cef4eba9c42ebf5412a5886e77e6feae
--- /dev/null
+++ b/src/plugins/server/share/protocol/server.md
@@ -0,0 +1,131 @@
+# Architecture
+
+The Server plug-in provides a _remote procedure call_ (RPC) interface to foreign
+applications. The protocol is organized in three logic layers, organized as
+follows:
+
+1. Many external entry points, based on various networking and system facilities
+2. A generic logic run-time responsible for scheduling the requests coming from
+ the various entry points
+3. The Frama-C implementation of requests handler, at the kernel or plug-in
+ level
+
+The intermediate, logic layer, is responsible for adding a small bit of
+parallelism upon the intrinsically synchronous behavior of Frama-C. This makes
+Frama-C resembling an asynchronous RPC server.
+
+The externally visible layer is only focused on transporting external requests
+to the logic layer, and transporting back the results to the caller. The only
+requirement for an entry point is to be able to transport a sequence of 1-input
+message for 1-output message over time.
+
+The concrete layer is implemented by the Frama-C kernel and its plug-ins. All
+requests must be registered _via_ the Frama-C Server OCaml API in order to be
+accessible from the entry-points. Some parts of this documentation are
+automatically generated from the registered requests.
+
+## Logical Requests
+
+From a functional point of view, requests are remote procedures with input
+data that reply with output data. Each request is identified by a unique name.
+Input and output parameters are encoded into JSON values.
+
+To adapt the internal synchronous Frama-C implementation with the external
+asynchronous entry points, requests are classified into three kinds:
+
+- `GET` to instantaneously return data from the internal state of Frama-C
+- `SET` to instantaneously modifies the state or configure Frama-C plug-ins
+- `EXEC` to starts a resource intensive analysis in Frama-C
+
+During an `EXEC` requests, the implementation of the all resource demanding
+computations shall repeatedly call the yielding routine `!Db.progress()` of the
+Frama-C kernel to ensures a smooth asynchronous behavior of the Server. During a
+_yield_ call, the Server would be allowed to handle few `GET` pending requests,
+since they shall be fast without any modification. When the server is idled, any
+kind of requests can be started.
+
+To summarize:
+
+| Request | During Yields | Allowed to Yield | Computation |
+|:--------|:-------------:|:----------------:|:------------:|
+| `GET` | ✓ | - | fast, pure |
+| `SET` | - | - | fast, side-effects |
+| `EXEC` | - | ✓ | resource demanding |
+
+## Transport Messages
+
+From the entry points layer, the asynchronous behavior of the Server makes
+output data and input data to be dispatched into different messages. However,
+from the Client side, we still want to have _one_ response message for each
+incoming message. However, answer messages might contains output data from
+potentially _any_ previously received requests.
+
+When the client has no more requests to send, but is simply waiting for pending
+requests responses, it must periodically send _polling_ requests to simply get
+back the expected responses.
+
+To implement those features, the Client-Server protocol consists of a sequence of
+paired _intput messages_ and _output messages_. Each single input message consists of
+a list of _commands_:
+
+| Commands | Parameters | Description |
+|:--------:|:----------:|:------------|
+| `POLL` | - | Ask for pending responses, if any |
+| `GET` | `id,request,data` | En-queue the given GET request |
+| `SET` | `id,request,data` | En-queue the given SET request |
+| `EXEC` | `id,request,data` | En-queue the given EXEC request |
+| `KILL` | `id` | Cancel the given request or interrupt its execution |
+| `SHUTDOWN` | - | Makes the server to stop running |
+
+Similarly, a single output message consists of a list
+of _replies_, listed in table below:
+
+| Replies | Parameters | Description |
+|:--------:|:----------:|:------------|
+| `DATA` | `id,data` | Response data from the identified request |
+| `ERROR` | `id,message` | Error message from the identified request |
+| `KILLED` | `id` | The identified request has been killed or interrupted |
+| `REJECTED` | `id` | The identified request was not registered on the Server |
+
+The logic layer makes no usage of _identifiers_ and simply pass them unchanged into
+output messages in response to received requests.
+
+At the transport message layer, input and output data are made of a
+single `JSON` encoded value. Requests are identified by string, and
+request identifiers can be of any type from the entry-points.
+
+**Remark** the `GET`, `SET` or `EXEC` behavior of a request is actually defined
+by the request implementation, from the Frama-C internal side. The Server will
+silently ignore the request kind from the incoming messages and use the actual
+internal one instead. The distinction still appears in the transport protocol
+only for a purpose of information, as clients shall know what they are asking
+for.
+
+## Entry Points
+
+Implementations of entry points layers shall provide a non-blocking `fetch`
+function that possibly returns a list of commands, associated with a
+callback for emitting the paired list of replies. The Server main
+loop is guaranteed to invoke the callback exactly once.
+
+The Server plug-in implements two entry-points, however, other Frama-C plugins might
+implement their own entry-points and call the `Server.Main.run ~fetch ()` function
+to make the server starting and exchanging messages with the external world.
+
+## Request Implementations
+
+It is the responsibility of Frama-C plug-ins to implement and register requests
+into the Server to make them accessible _via_ any entry point. Whereas data is
+encoded into JSON structures at the transport layer, requests are processes with
+well typed OCaml types from the internal side.
+
+Hence, the requests implementations also requires data encoder and decoders to
+be defined. Some predefined data types are provided by the Server plug-in, but
+more complex types can be defined and shared among plug-ins _via_ the
+`Server.Data` module factory.
+
+Registration of requests, data encoder and decoders always comes with their
+markdown documentation thanks to the `Markdown` library provided by the Frama-C
+kernel. Hence, a full documentation of all implemented requests with their data
+formats can be generated consistently at any time. See option `-server-doc` of the
+Server plug-in for more details.
diff --git a/src/plugins/server/share/protocol/server_batch.md b/src/plugins/server/share/protocol/server_batch.md
new file mode 100644
index 0000000000000000000000000000000000000000..1092cc6c5b2a28c8822db87182d5dde7c307ff18
--- /dev/null
+++ b/src/plugins/server/share/protocol/server_batch.md
@@ -0,0 +1,31 @@
+# Batch Protocol
+
+This section presents a Frama-C command-line entry point to Server requests.
+Although it is not full-featured server entry point, it allows for executing
+requests from the command line or JSON scripts.
+
+The `-server-script` option of the Frama-C/Server plug-in takes a (list of)
+script file `<file.json>`, parse it and execute its commands, and output the
+reponses in file `<file.out.json>`.
+
+## Input Script Format
+
+A JSON script is either a single JSON command or an array of JSON commands, or `null`.
+Each command is a record with the following fields:
+
+| Input Field | Format | Description |
+|:------|:-------|:-----------:|
+| `id` | _any_ ? | The command identifier (optional) |
+| `request` | _string_ | The request name |
+| `data` | _any_ | The request input parameters |
+
+## Output Script Format
+
+Each command leads to an assiated JSON record, with the following fields:
+
+| Output Field | Format | Description |
+|:------|:-------|:-----------:|
+| `id` | _any_ ? | The command identifier (as provided in input) |
+| `data` | _any_ ? | The request output parameters (if successfull) |
+| `error` | _string_ ? | The request error message (in case of occurence) |
+| `at` | _any_ ? | Wrongly encoded part of the request (when appropriate) |
diff --git a/src/plugins/server/share/protocol/server_zmq.md b/src/plugins/server/share/protocol/server_zmq.md
new file mode 100644
index 0000000000000000000000000000000000000000..f510a31888e81e509a0635425bf6a9ef3cbf75e2
--- /dev/null
+++ b/src/plugins/server/share/protocol/server_zmq.md
@@ -0,0 +1,62 @@
+# ZeroMQ Protocol
+
+This section presents a [ZeroMQ](http://zeromq.org) based entry point for Frama-C Server.
+It is activated by option `-server-zmq <URL>` option of the Server plug-in, which is compiled
+when the OCaml package `zmq` is detected at Frama-C configure time.
+
+The protocol builds a ZeroMQ socket of type `REP` which is the standard for a request server.
+It is meant for accepting connection from a ZeroMQ socket of type `REQ` on the same `URL`.
+The paired `REP`-`REQ` sockets use
+[ZeroMQ multi-part messages](http://zguide.zeromq.org/page:all#Multipart-Messages) to transfer data.
+
+A typical example to start a Frama-C server for inter-process communication is:
+
+```shell
+$ frama-c [options...] -then -server-zmq ipc:///tmp/my-server.io
+```
+
+## Input Message Format
+
+Each input message consists of a list of commands. Each command takes
+a fixed number of parts from the incomming ZeroMQ message. The first part
+of each command is a single string identifying the command:
+
+| Commands | Parts | Part 1 | Part 2 | Part 3 | Part 4 |
+|:--------|:-----:|:-------|:-------|:-------|:-------|
+| `POLL()` | 1 | `"POLL"` | | | |
+| `GET(id,request,data)` | 4 | `"GET"` | id | request | data |
+| `SET(id,request,data)` | 4 | `"SET"` | id | request | data |
+| `EXEC(id,request,data)` | 4 | `"EXEC"` | id | request | data |
+| `KILL(id)` | 2 | `"KILL"` | id | | |
+| `SHUTDOWN` | 1 | `"SHUTDOWN"` | | | |
+
+## Output Message Format
+
+Each output message consists of a list of replies. Each reply takes
+a fixed number of parts from the incomming ZeroMQ message. The first part
+of each reply is a finel string identifying the reply:
+
+| Replies | Parts | Part 1 | Part 2 | Part 3 |
+|:--------|:-----:|:-------|:-------|:-------|
+| `DATA(id,data)` | 3 | `"DATA"` | id | data |
+| `ERROR(id,message)` | 4 | `"ERROR"` | id | message |
+| `KILLED(id)` | 2 | `"KILLED"` | id | |
+| `REJECTED(id)` | 2 | `"REJECTED"` | id | |
+| (special) | 2 | `"WRONG"` | message | |
+| (special) | 1 | `"NONE"` | | |
+
+The two special responses `"WRONG"` and `"NONE"` are used to handle special issues
+with the ZeroMQ layer protocol: `WRONG(message)` signals an error in the message formats;
+`NONE` is used in the special case where the reply message from the server is completely
+empty. This generaly means that the server is busy or idled.
+
+## Data Format
+
+Request identifiers can be any string, encoded into a single part of a ZeroMQ message.
+
+Data are stringified JSON data structures. Each command or reply data shall be packed
+into a single JSON data, which leads to a single part of the associated ZeroMQ message.
+
+Since ZeroMQ prococol accepts any kind of strings as a single
+message part, the stringified JSON data might contains spaces, newlines and any
+other spacing characters.
diff --git a/src/plugins/server/syntax.ml b/src/plugins/server/syntax.ml
new file mode 100644
index 0000000000000000000000000000000000000000..565a227cde54a50190a518e5d45f036b9b44d913
--- /dev/null
+++ b/src/plugins/server/syntax.ml
@@ -0,0 +1,129 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+
+module Senv = Server_parameters
+
+let check_plugin plugin name =
+ let p = String.lowercase_ascii plugin in
+ let n = String.lowercase_ascii name in
+ let k = String.length plugin in
+ if not (String.length name > k &&
+ String.sub n 0 k = p &&
+ String.get n k = '.')
+ then
+ Senv.warning ~wkey:Senv.wpage
+ "Data %S shall be named « %s-* »"
+ name plugin
+
+let check_page page name =
+ match Doc.chapter page with
+ | `Kernel -> ()
+ | `Plugin plugin -> check_plugin plugin name
+ | `Protocol -> check_plugin "server" name
+
+let re_name = Str.regexp "[a-z0-9-]+$"
+
+let check_name name =
+ if not (Str.string_match re_name name 0) then
+ Senv.warning ~wkey:Senv.wname
+ "Data name %S is not a dash-separated list of lowercase identifiers" name
+
+(* -------------------------------------------------------------------------- *)
+
+type t = { atomic:bool ; text:Markdown.text }
+
+let atom md = { atomic=true ; text=md }
+let flow md = { atomic=false ; text=md }
+
+let format { text } = text
+let protect a =
+ if a.atomic then a.text else Markdown.(rm "(" <+> a.text <+> rm ")")
+
+let publish ~page ~name ~descr ~synopsis ?(details = Markdown.empty) () =
+ check_name name ;
+ check_page page name ;
+ let id = Printf.sprintf "data-%s" name in
+ let title = Printf.sprintf "`DATA` %s" name in
+ let format = ref Markdown.nil in
+ let syntax = Markdown.fmt_block (fun fmt ->
+ Format.fprintf fmt "> %a ::= %a"
+ Markdown.pp_text !format
+ Markdown.pp_text synopsis.text
+ ) in
+ let content = Markdown.( par descr </> syntax </> details ) in
+ let href = Doc.publish ~page ~name:id ~title ~index:[name] content [] in
+ let link_title = Printf.sprintf "_%s_" name in
+ let link = Markdown.href ~title:link_title href in
+ format := link ; atom @@ link
+
+let unit = atom @@ Markdown.rm "-"
+let any = atom @@ Markdown.it "any"
+let int = atom @@ Markdown.it "int"
+let ident = atom @@ Markdown.it "ident"
+let string = atom @@ Markdown.it "string"
+let number = atom @@ Markdown.it "number"
+let boolean = atom @@ Markdown.it "boolean"
+
+let escaped name = Markdown.tt @@ Printf.sprintf "'%s'" @@ String.escaped name
+
+let tag name = atom @@ escaped name
+
+let array a = atom @@ Markdown.(tt "[" <+> protect a <+> tt ", … ]")
+
+let tuple ts =
+ atom @@ Markdown.(tt "["
+ <+> glue ~sep:(raw " `,` ") (List.map protect ts) <+>
+ tt "]")
+
+let union ts = flow @@ Markdown.(glue ~sep:(raw " | ") (List.map protect ts))
+
+let option t = atom @@ Markdown.(protect t <@> tt "?")
+
+let field (a,t) = Markdown.( escaped a <+> tt ":" <+> t.text )
+
+let record fds =
+ let fields =
+ if fds = [] then Markdown.rm "…" else
+ Markdown.(glue ~sep:(raw " `;` ") (List.map field fds))
+ in atom @@ Markdown.(tt "{" <+> fields <+> tt "}")
+
+type field = {
+ name : string ;
+ syntax : t ;
+ descr : Markdown.text ;
+}
+
+let fields ~title (fds : field list) =
+ let c_field = `Left title in
+ let c_format = `Center "Format" in
+ let c_descr = `Left "Description" in
+ Markdown.table [ c_field ; c_format ; c_descr ]
+ begin
+ List.map
+ (fun f ->
+ [ Markdown.tt f.name ; format f.syntax ; f.descr ])
+ fds
+ end
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/server/syntax.mli b/src/plugins/server/syntax.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ff4c575e6c3ed0e65a38b66f593272850942ddaf
--- /dev/null
+++ b/src/plugins/server/syntax.mli
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(* -------------------------------------------------------------------------- *)
+(** JSON Encoding Documentation *)
+(* -------------------------------------------------------------------------- *)
+
+type t
+
+val format : t -> Markdown.text
+
+(** The provided synopsis must be very short, to fit in one line.
+ Extended definition, like record fields and such, must be detailed in
+ the description block. *)
+val publish :
+ page:Doc.page -> name:string -> descr:Markdown.text ->
+ synopsis:t -> ?details:Markdown.block -> unit -> t
+
+val unit : t
+val any : t
+val int : t (* small, non-decimal, number *)
+val ident : t (* integer of string *)
+val string : t
+val number : t
+val boolean : t
+
+val tag : string -> t
+val array : t -> t
+val tuple : t list -> t
+val union : t list -> t
+val option : t -> t
+val record : (string * t) list -> t
+
+type field = { name : string ; syntax : t ; descr : Markdown.text }
+
+(** Builds a table with fields column named with [~title]
+ (shall be capitalized) *)
+val fields : title:string -> field list -> Markdown.block
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/GuiSource.ml b/src/plugins/wp/GuiSource.ml
index 66a2c8abcf00bd2f5a755b87814bc08bde0674fb..38697bcde348ac5389e4ffeb545c3972702ea15f 100644
--- a/src/plugins/wp/GuiSource.ml
+++ b/src/plugins/wp/GuiSource.ml
@@ -232,7 +232,7 @@ class highlighter (main:Design.main_window_extension_points) =
~(start:int) ~(stop:int) =
let buffer = buffer#buffer in
begin match loc with
- | PStmt( _ , stmt ) ->
+ | PStmt( _ , stmt ) | PStmtStart( _ , stmt ) ->
begin
match effect with
| Some(s,_) when Stmt.equal stmt s ->
@@ -250,7 +250,7 @@ class highlighter (main:Design.main_window_extension_points) =
if DEPS.mem ip deps then
apply_depend buffer start stop
end
- | PStmtStart _ | PGlobal _
+ | PGlobal _
| PVDecl _ | PTermLval _ | PLval _ | PExp _ -> ()
end