package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file package.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    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 Md = Markdown

(* -------------------------------------------------------------------------- *)

type plugin = Kernel | Plugin of string
type ident = { plugin: plugin; package: string list; name: string }

let pp_step fmt a =
  ( Format.pp_print_string fmt a ; Format.pp_print_char fmt '.' )

let pp_plugin fmt = function
  | Kernel -> pp_step fmt "kernel"
  | Plugin p -> pp_step fmt "plugins" ; pp_step fmt p

let pp_ident fmt { plugin ; package ; name } =
  ( pp_plugin fmt plugin ;
    List.iter (pp_step fmt) package ;
    Format.pp_print_string fmt name )

(* -------------------------------------------------------------------------- *)
(* --- Name Resolution                                                    --- *)
(* -------------------------------------------------------------------------- *)

module Std = Stdlib
module Id = struct type t = ident let compare = Std.compare end
module IdMap = Map.Make(Id)
module IdSet = Set.Make(Id)
module NameSet = Set.Make(String)

module Scope =
struct

  let rec inpkg ids = function
    | [] -> ids
    | [p] -> p::ids
    | _::ps -> inpkg ids ps

  let relative ~source ~target ids =
    if target = source then ids else
      match target with
      | Kernel -> ids
      | Plugin p -> p::ids

  let target p ids =
    match p with
    | Kernel -> "kernel" :: ids
    | Plugin p -> "plugins" :: p :: ids

  (* propose various abbreviations ; finally render full qualified name *)
  let ranked source { plugin ; package ; name } k =
    String.concat "_" @@
    let name = [name] in
    match k with
    | 0 -> name
    | 1 -> relative ~source ~target:plugin name
    | 2 -> relative ~source ~target:plugin (inpkg name package)
    | 3 -> relative ~source ~target:plugin (package @ name)
    | _ -> target plugin (package @ name)

  type t = {
    source : plugin ;
    mutable clashes : bool ;
    mutable index : (string,int IdMap.t) Hashtbl.t ;
    mutable names : string IdMap.t ;
    mutable reserved : NameSet.t ;
  }

  let create source = {
    source ;
    index = Hashtbl.create 0 ;
    clashes = false ;
    names = IdMap.empty ;
    reserved = NameSet.empty ;
  }

  let rec non_reserved scope id rk =
    let a = ranked scope.source id rk in
    if NameSet.mem a scope.reserved then
      non_reserved scope id (succ rk)
    else a,rk

  let push scope id rk =
    begin
      let name, rk = non_reserved scope id rk in
      scope.names <- IdMap.add id name scope.names ;
      let index = scope.index in
      match Hashtbl.find_opt index name with
      | None ->
        Hashtbl.add index name (IdMap.add id rk IdMap.empty)
      | Some idks ->
        if IdMap.mem id idks then
          scope.clashes <- true
        else
          Hashtbl.replace index name (IdMap.add id rk idks)
    end

  let use scope id =
    if not (IdMap.mem id scope.names) then
      push scope id 0

  let reserve scope name =
    assert (IdMap.is_empty scope.names) ;
    scope.reserved <- NameSet.add name scope.reserved

  let declare scope id =
    begin
      let { name } = id in
      if NameSet.mem name scope.reserved then
        Senv.fatal "Reserved name for identifier '%a'" pp_ident id ;
      scope.names <- IdMap.add id name scope.names ;
      scope.reserved <- NameSet.add name scope.reserved ;
    end

  let rec resolve scope =
    if not scope.clashes then scope.names else
      begin
        let index = scope.index in
        scope.index <- Hashtbl.create 0 ;
        scope.clashes <- false ;
        Hashtbl.iter
          (fun _name idks ->
             match IdMap.bindings idks with
             | [id,rk] ->
               push scope id rk
             | idks ->
               List.iter (fun (id,rk) -> push scope id (succ rk)) idks
          ) index ;
        resolve scope
      end

end

(* -------------------------------------------------------------------------- *)
(* --- JSON Datatypes                                                     --- *)
(* -------------------------------------------------------------------------- *)

type jtype =
  | Jany
  | Jnull
  | Jboolean
  | Jnumber
  | Jstring
  | Jalpha (* string primarily compared without case *)
  | Jtag of string (* single constant string *)
  | Jkey of string (* kind of a string used for indexing *)
  | Jindex of string (* kind of an integer used for indexing *)
  | Joption of jtype
  | Jdict of jtype (* dictionaries *)
  | Jarray of jtype (* order matters *)
  | Jtuple of jtype list
  | Junion of jtype list
  | Jrecord of (string * jtype) list
  | Jenum of ident * string list (* type and tags *)
  | Jdata of ident * jtype (* type and definition *)
  | Jself (* for (simply) recursive types *)

(* -------------------------------------------------------------------------- *)
(* --- Declarations                                                       --- *)
(* -------------------------------------------------------------------------- *)

type fieldInfo = {
  fd_name: string;
  fd_type: jtype;
  fd_descr: Markdown.text;
}

type tagInfo = {
  tg_name: string;
  tg_label: Markdown.text;
  tg_descr: Markdown.text;
}

type paramInfo =
  | P_value of jtype
  | P_named of fieldInfo list

type requestInfo = {
  rq_kind: [ `GET | `SET | `EXEC ];
  rq_input: paramInfo ;
  rq_output: paramInfo ;
  rq_signals: string list ;
}

type arrayInfo = {
  arr_key: string;
  arr_kind: jtype;
  arr_rows: jtype;
}

type declKindInfo =
  | D_signal
  | D_type of jtype
  | D_enum of tagInfo list
  | D_record of fieldInfo list
  | D_request of requestInfo
  | D_value of jtype
  | D_state of jtype
  | D_array of arrayInfo (* key kind *)
  | D_decoder of ident * jtype
  | D_order of ident * jtype (* natural ordering *)
  | D_default of ident * jtype (* default value *)

type declInfo = {
  d_ident : ident;
  d_descr : Markdown.text;
  d_kind : declKindInfo;
}

type packageInfo = {
  p_plugin : plugin ;
  p_package : string list ;
  p_title : string ;
  p_descr : Markdown.text ;
  p_readme : string option ;
  p_content : declInfo list ;
}

let name_of_ident ?(sep=".") id =
  String.concat sep @@ match id.plugin with
  | Kernel -> "kernel" :: id.package @ [ id.name ]
  | Plugin p -> "plugins" :: p :: (id.package @ [id.name ])

let name_of_pkg ?(sep=".") plugin package =
  String.concat sep @@ match plugin with
  | Kernel -> "kernel" :: package
  | Plugin p -> "plugins" :: p :: package

let name_of_pkginfo ?sep { p_plugin ; p_package } =
  name_of_pkg ?sep p_plugin p_package

let pp_pkgname fmt { p_plugin ; p_package } =
  ( pp_plugin fmt p_plugin ;
    List.iter (pp_step fmt) p_package )

(* -------------------------------------------------------------------------- *)
(* --- Derived Names                                                      --- *)
(* -------------------------------------------------------------------------- *)

let derived ?prefix ?suffix id =
  let capitalize = String.capitalize_ascii in
  match prefix , suffix with
  | None , None -> id
  | Some p , None -> { id with name = p ^ capitalize id.name }
  | None , Some q -> { id with name = id.name ^ q }
  | Some p , Some q -> { id with name = p ^ capitalize id.name ^ q }

module Derived =
struct
  let signal id = derived ~prefix:"signal" id
  let getter id = derived ~prefix:"get" id
  let setter id = derived ~prefix:"set" id
  let data id = derived ~suffix:"Data" id
  let default id = derived ~suffix:"Default" id
  let fetch id = derived ~prefix:"fetch" id
  let reload id = derived ~prefix:"reload" id
  let order id = derived ~prefix:"by" id
  let decode id = derived ~prefix:"j" id
end

(* -------------------------------------------------------------------------- *)
(* --- Visitors                                                           --- *)
(* -------------------------------------------------------------------------- *)

let rec isRecursive = function
  | Jself -> true
  | Jdata _ | Jenum _
  | Jany | Jnull | Jboolean | Jnumber
  | Jstring | Jalpha | Jkey _ | Jindex _ | Jtag _ -> false
  | Joption js | Jdict js  | Jarray js -> isRecursive js
  | Jtuple js | Junion js -> List.exists isRecursive js
  | Jrecord fjs -> List.exists (fun (_,js) -> isRecursive js) fjs

let rec visit_jtype fn = function
  | Jany | Jself | Jnull | Jboolean | Jnumber
  | Jstring | Jalpha | Jkey _ | Jindex _ | Jtag _ -> ()
  | Joption js | Jdict js  | Jarray js -> visit_jtype fn js
  | Jtuple js | Junion js -> List.iter (visit_jtype fn) js
  | Jrecord fjs -> List.iter (fun (_,js) -> visit_jtype fn js) fjs
  | Jdata(id,_) | Jenum(id,_) ->
    begin
      fn id ;
      fn (Derived.default id) ;
      fn (Derived.decode id) ;
      fn (Derived.order id) ;
    end

let visit_field f { fd_type } = visit_jtype f fd_type

let visit_param f = function
  | P_value js -> visit_jtype f js
  | P_named fds -> List.iter (visit_field f) fds

let visit_request f { rq_input ; rq_output } =
  ( visit_param f rq_input ; visit_param f rq_output )

let visit_dkind f = function
  | D_signal | D_enum _ | D_array _ -> ()
  | D_type js | D_state js | D_value js -> visit_jtype f js
  | D_decoder (id,js) | D_order(id,js) | D_default(id,js)
    -> f id ; visit_jtype f js
  | D_record fds -> List.iter (visit_field f) fds
  | D_request rq -> visit_request f rq

let visit_decl f { d_kind } = visit_dkind f d_kind

let visit_package_decl f { p_content } =
  List.iter (fun { d_ident } -> f d_ident) p_content

let visit_package_used f { p_content } =
  List.iter (visit_decl f) p_content

let resolve ?(keywords=[]) pkg =
  let scope = Scope.create pkg.p_plugin in
  List.iter (Scope.reserve scope) keywords ;
  visit_package_decl (Scope.declare scope) pkg ;
  visit_package_used (Scope.use scope) pkg ;
  Scope.resolve scope

(* -------------------------------------------------------------------------- *)
(* --- Server API                                                         --- *)
(* -------------------------------------------------------------------------- *)

type package = {
  pkgInfo : packageInfo ; (* with empty decl *)
  mutable revDecl : declInfo list ; (* in reverse order *)
}

let field fd = fd.fd_name , fd.fd_type

let name_of_package ?sep pkg = name_of_pkginfo ?sep pkg.pkgInfo

let registry = ref IdSet.empty (* including packages *)
let packages = ref [] (* in reverse order *)
let collection = ref None (* computed *)

let name_re = Str.regexp "^[a-zA-Z0-9]+$"
let package_re = Str.regexp "^[a-z0-9]+\\(\\.[a-z0-9]+\\)*$"

let check_package pkg =
  if not (Str.string_match package_re pkg 0) then
    Senv.fatal
      "Invalid package identifier %S (use dot separated lowercase names)"
      pkg

let check_name name =
  if not (Str.string_match name_re name 0) then
    Senv.fatal
      "Invalid identifier %S (use « camlCased » names)" name

let register_ident id =
  if IdSet.mem id !registry then
    Senv.fatal "Duplicate identifier '%a'" pp_ident id ;
  registry := IdSet.add id !registry

(* -------------------------------------------------------------------------- *)
(* --- Declarations                                                       --- *)
(* -------------------------------------------------------------------------- *)

let package ?plugin ?name ~title ?(descr=[]) ?readme () =
  let plugin = match plugin with None -> Kernel | Some p -> Plugin p in
  let pkgname = match name with
    | None -> []
    | Some pkg -> check_package pkg ; String.split_on_char '.' pkg in
  let pkgid = { plugin ; package = pkgname ; name = "*"} in
  let pkgInfo = {
    p_plugin = plugin ;
    p_package = pkgname ;
    p_title = title ;
    p_descr = descr ;
    p_readme = readme ;
    p_content = [] ;
  } in
  let package = { pkgInfo ; revDecl=[] } in
  register_ident pkgid ;
  collection := None ;
  packages := package :: !packages ;
  package

let declare_id ~package:pkg ~name ?(descr=[]) decl =
  check_name name ;
  let { p_plugin = plugin ; p_package = package } = pkg.pkgInfo in
  let ident = { plugin ; package ; name } in
  let decl = { d_ident=ident ; d_descr=descr ; d_kind=decl } in
  register_ident ident ;
  pkg.revDecl <- decl :: pkg.revDecl ; ident

let declare ~package ~name ?descr decl =
  let _id = declare_id ~package ~name ?descr decl in ()

let update ~package:pkg ~name decl =
  pkg.revDecl <- List.map
      (fun curr ->
         if curr.d_ident.name = name then
           { curr with d_kind = decl }
         else curr
      ) pkg.revDecl

let iter f =
  List.iter f @@
  match !collection with
  | Some pkgs -> pkgs
  | None ->
    let pkgs =
      List.sort (fun a b -> Std.compare a.p_plugin b.p_plugin) @@
      List.rev_map
        (fun pkg -> { pkg.pkgInfo with p_content = List.rev pkg.revDecl })
        !packages
    in collection := Some pkgs ; pkgs

(* -------------------------------------------------------------------------- *)
(* --- JSON To MarkDown                                                   --- *)
(* -------------------------------------------------------------------------- *)

let key kd = Md.plain (Printf.sprintf "`$%s`" kd)
let index kd = Md.plain (Printf.sprintf "`#%s`" kd)
let litteral tag = Md.plain (Printf.sprintf "`\"%s\"`" tag)

type pp = {
  self: Md.text ;
  ident: ident -> Md.text ;
}

let rec md_jtype pp = function
  | Jany -> Md.emph "any"
  | Jself -> pp.self
  | Jnull -> Md.emph "null"
  | Jnumber -> Md.emph "number"
  | Jboolean -> Md.emph "boolean"
  | Jstring | Jalpha -> Md.emph "string"
  | Jtag a -> litteral a
  | Jkey kd -> key kd
  | Jindex kd -> index kd
  | Jdata(id,_) | Jenum(id,_) -> pp.ident id
  | Joption js -> protect pp js @ Md.code "?"
  | Jtuple js -> Md.code "[" @ md_jlist pp "," js @ Md.code "]"
  | Junion js -> md_jlist pp "|" js
  | Jarray js -> protect pp js @ Md.code "[]"
  | Jrecord fjs -> Md.code "{" @ fields pp fjs @ Md.code "}"
  | Jdict js -> Md.code "{[key]:" @ md_jtype pp js @ Md.code "}"

and md_jlist pp sep js =
  Md.glue ~sep:(Md.plain sep)  (List.map (md_jtype pp) js)

and fields pp fjs =
  Md.glue ~sep:(Md.plain ",") @@
  List.map (fun (fd,js) ->
      litteral fd @
      match js with
      | Joption js -> Md.code ":?" @ md_jtype pp js
      | _ -> Md.code ":" @ md_jtype pp js
    ) fjs

and protect names js =
  match js with
  | Junion _ -> Md.code "(" @ md_jtype names js @ Md.code ")"
  | _ -> md_jtype names js

(* -------------------------------------------------------------------------- *)
(* --- Tags & Fields                                                      --- *)
(* -------------------------------------------------------------------------- *)

let md_tags ?(title="Tags") (tags : tagInfo list) =
  let header = Md.[
      plain title, Left;
      plain "Value", Left;
      plain "Description", Left
    ] in
  let row tg = [
    tg.tg_label ;
    litteral tg.tg_name ;
    tg.tg_descr ;
  ] in
  Md.{ caption = None ; header ; content = List.map row tags  }

let md_fields ?(title="Field") pp (fields : fieldInfo list) =
  let header = Md.[
      plain title, Left;
      plain "Format", Center;
      plain "Description", Left;
    ] in
  let row f =
    match f.fd_type with
    | Joption js -> [
        litteral f.fd_name @ Md.plain "(opt.)" ;
        md_jtype pp js ;
        f.fd_descr ;
      ]
    | _ -> [
        litteral f.fd_name ;
        md_jtype pp f.fd_type ;
        f.fd_descr ;
      ]
  in
  Md.{ caption = None ; header ; content = List.map row fields }

(* -------------------------------------------------------------------------- *)
(* --- Printer                                                            --- *)
(* -------------------------------------------------------------------------- *)

let pp_jtype fmt js =
  let scope = Scope.create Kernel in
  visit_jtype (Scope.use scope) js ;
  let ns = Scope.resolve scope in
  let self = Md.emph "self" in
  let ident id = Md.emph (IdMap.find id ns) in
  Markdown.pp_text fmt (md_jtype { self ; ident } js)

(* -------------------------------------------------------------------------- *)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct