package frama-c

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

Source file LogicBuiltins.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* Registry for ACSL Builtins                                             --- *)
(* -------------------------------------------------------------------------- *)

open Cil_types
open Ctypes
open Qed
open Lang

type category = Lang.lfun Qed.Logic.category

type builtin =
  | ACSLDEF
  | LFUN of lfun
  | HACK of (F.term list -> F.term)

type kind =
  | B (* boolean *)
  | Z (* integer *)
  | R (* real *)
  | I of Ctypes.c_int
  | F of Ctypes.c_float
  | A (* abstract data *)

(* [LC] kinds can be compared by Stdlib.compare *)

let okind = function
  | C_int i -> I i
  | C_float f -> F f
  | _ -> A

let ckind typ = okind (object_of typ)

let skind = function
  | B -> Logic.Sbool
  | I _ | Z -> Logic.Sint
  | F _ | R -> Logic.Sreal
  | A -> Logic.Sdata

let rec lkind t =
  match Logic_utils.unroll_type ~unroll_typedef:false t with
  | Ctype ty -> ckind ty
  | Ltype({lt_name="set"},[t]) -> lkind t
  | Lreal -> R
  | Linteger -> Z
  | Lboolean -> B
  | Ltype _ | Larrow _ | Lvar _ -> A

let kind_of_tau = function
  | Qed.Logic.Int -> Z
  | Qed.Logic.Real -> R
  | Qed.Logic.Bool -> B
  | _ -> A

let pp_kind fmt = function
  | I i -> Ctypes.pp_int fmt i
  | F f -> Ctypes.pp_float fmt f
  | B -> Format.pp_print_string fmt "bool"
  | Z -> Format.pp_print_string fmt "int"
  | R -> Format.pp_print_string fmt "real"
  | A -> Format.pp_print_string fmt "_"

let pp_kinds fmt = function
  | [] -> ()
  | t::ts ->
    Format.fprintf fmt "(%a" pp_kind t ;
    List.iter (fun t -> Format.fprintf fmt ",%a" pp_kind t) ts ;
    Format.fprintf fmt ")"

let pp_libs fmt = function
  | [] -> ()
  | t::ts ->
    Format.fprintf fmt ": %s" t ;
    List.iter (fun t -> Format.fprintf fmt ",%s" t) ts

let pp_link fmt = function
  | ACSLDEF -> Format.pp_print_string fmt "(ACSL)"
  | HACK _ -> Format.pp_print_string fmt "(HACK)"
  | LFUN f -> Fun.pretty fmt f

(* -------------------------------------------------------------------------- *)
(* --- Driver & Lookup & Registry                                         --- *)
(* -------------------------------------------------------------------------- *)

type sigfun = kind list * builtin

type driver = {
  driverid : string;
  description : string;
  includes : Filepath.Normalized.t list;
  hlogic : (string , sigfun list) Hashtbl.t;
  htypes : (string , t_builtin) Hashtbl.t;
  hdeps : (string, string list) Hashtbl.t;
  hoptions :
    (string (* library *) * string (* group *) * string (* name *), string list)
      Hashtbl.t;
  mutable locked: bool
}

let lock driver = driver.locked <- true

let id d = d.driverid
let descr d = d.description
let is_default d = (d.driverid = "")
let compare d d' = String.compare d.driverid d'.driverid

let driver = Context.create "driver"
let cdriver_ro () = Context.get driver
let cdriver_rw () =
  let driver = Context.get driver in
  if driver.locked then
    Wp_parameters.failure "Attempt to modify locked: %s" driver.driverid ;
  driver

let lookup_driver name kinds =
  try
    let sigs = Hashtbl.find (cdriver_ro ()).hlogic name in
    try List.assoc kinds sigs
    with Not_found ->
      Wp_parameters.feedback ~once:true
        "Use -wp-msg-key 'driver' for debugging drivers" ;
      if kinds=[]
      then Warning.error "Builtin %s undefined as a constant" name
      else Warning.error "Builtin %s undefined with signature %a" name
          pp_kinds kinds
  with Not_found ->
    if Logic_env.is_builtin_logic_function name
    || Logic_env.is_builtin_logic_ctor name
    then
      Warning.error "Builtin %s%a not defined" name pp_kinds kinds
    else
      ACSLDEF

let hacks = Hashtbl.create 8
let hack name phi = Hashtbl.replace hacks name phi

let lookup name kinds =
  try
    let hack = Hashtbl.find hacks name in
    let compute es =
      try hack es with Not_found ->
      match lookup_driver name kinds with
      | ACSLDEF | HACK _ -> Warning.error "No fallback for hacked '%s'" name
      | LFUN p -> F.e_fun p es
    in HACK compute
  with Not_found -> lookup_driver name kinds

let register ?source name kinds link =
  let driver = cdriver_rw () in
  let sigs = try Hashtbl.find driver.hlogic name with Not_found -> [] in
  if List.exists (fun (s,_) -> s = kinds) sigs then
    Wp_parameters.warning ?source "Redefinition of logic %s%a"
      name pp_kinds kinds ;
  let entry = (kinds,link) in
  Hashtbl.add driver.hlogic name (entry::sigs)

let register_type ?source name builtin =
  let driver = cdriver_rw () in
  if Hashtbl.mem driver.htypes name then
    Wp_parameters.warning ?source "Redifinition of type %s" name ;
  Hashtbl.add driver.htypes name builtin

let iter_table f =
  let items = ref [] in
  Hashtbl.iter
    (fun a sigs -> List.iter (fun (ks,lnk) -> items := (a,ks,lnk)::!items) sigs)
    (cdriver_ro ()).hlogic ;
  List.iter f (List.sort Stdlib.compare !items)

let iter_libs f =
  let items = ref [] in
  Hashtbl.iter
    (fun a libs -> items := (a,libs) :: !items)
    (cdriver_ro ()).hdeps ;
  List.iter f (List.sort Stdlib.compare !items)

let dump () =
  Log.print_on_output
    begin fun fmt ->
      Format.fprintf fmt "Builtins:@\n" ;
      iter_libs
        (fun (name,libs) -> Format.fprintf fmt " * Library %s%a@\n"
            name pp_libs libs) ;
      iter_table
        (fun (name,k,lnk) -> Format.fprintf fmt " * Logic %s%a = %a@\n"
            name pp_kinds k pp_link lnk) ;
    end

(* -------------------------------------------------------------------------- *)
(* --- Implemented Builtins                                               --- *)
(* -------------------------------------------------------------------------- *)

let logic phi =
  lookup phi.l_var_info.lv_name
    (List.map (fun v -> lkind v.lv_type) phi.l_profile)

let ctor phi =
  lookup phi.ctor_name (List.map lkind phi.ctor_params)

let constant name =
  lookup name []

(* -------------------------------------------------------------------------- *)
(* --- Declaration of Builtins                                            --- *)
(* -------------------------------------------------------------------------- *)

let dependencies lib =
  Hashtbl.find (cdriver_ro ()).hdeps lib

let add_library lib deps =
  let others = try dependencies lib with Not_found -> [] in
  Hashtbl.add (cdriver_rw ()).hdeps lib (others @ deps)

let add_alias ~source name kinds ~alias () =
  register ~source name kinds (lookup alias kinds)

let add_logic ~source result name kinds ~library ?category ~link () =
  let sort = skind result in
  let params = List.map skind kinds in
  let lfun = Lang.extern_s ~library ?category ~sort ~params ~link name in
  register ~source name kinds (LFUN lfun)

let add_predicate ~source name kinds ~library ~link () =
  let params = List.map skind kinds in
  let lfun = Lang.extern_fp ~library ~params ~link link in
  register ~source name kinds (LFUN lfun)

let add_ctor ~source name kinds ~library ~link () =
  let category = Logic.Constructor in
  let params = List.map skind kinds in
  let lfun = Lang.extern_s ~library ~category ~params ~link name in
  register ~source name kinds (LFUN lfun)

let add_type ?source name ~library ?(link=name) () =
  let mdt = Lang.extern_t name ~link ~library in
  register_type ?source name (E_mdt mdt)

let hack_type name poly =
  register_type name (E_poly poly)

type sanitizer = driver_dir:string -> string -> string
let sanitizers : ( string * string , sanitizer ) Hashtbl.t = Hashtbl.create 10

exception Unknown_option of string * string

let sanitize ~driver_dir group name v =
  try
    (Hashtbl.find sanitizers (group,name)) ~driver_dir v
  with Not_found -> raise (Unknown_option(group,name))

type doption = string * string

let create_option ~sanitizer group name =
  let option = (group,name) in
  Hashtbl.replace sanitizers option sanitizer ;
  option

let get_option (group,name) ~library =
  try Hashtbl.find (cdriver_ro ()).hoptions (library,group,name)
  with Not_found -> []

let set_option ~driver_dir group name ~library value =
  let value = sanitize ~driver_dir group name value in
  Hashtbl.replace (cdriver_rw ()).hoptions (library,group,name) [value]

let add_option ~driver_dir group name ~library value =
  let value = sanitize ~driver_dir group name value in
  let l = get_option (group,name) ~library in
  Hashtbl.replace (cdriver_rw ()).hoptions (library,group,name) (l @ [value])


(** Includes *)

let find_lib file =
  if Filepath.exists file then file else
    let rec lookup file = function
      | [] -> Wp_parameters.abort "File '%a' not found"
                Filepath.Normalized.pretty file
      | dir::dirs ->
        let path = Filepath.Normalized.concat dir (file :> string) in
        if Filepath.exists path then path else lookup file dirs
    in
    lookup file (cdriver_ro ()).includes

(* -------------------------------------------------------------------------- *)
(* --- Implemented Builtins                                               --- *)
(* -------------------------------------------------------------------------- *)

let builtin_driver = {
  driverid = "builtin driver";
  description = "builtin driver";
  includes = [];
  hlogic = Hashtbl.create 131;
  htypes = Hashtbl.create 131;
  hdeps  = Hashtbl.create 31;
  hoptions = Hashtbl.create 131;
  locked = false
}

let add_builtin name kinds lfun =
  let phi = LFUN lfun in
  if Context.defined driver then
    register name kinds phi
  else
    Context.bind driver builtin_driver (register name kinds) phi

let add_builtin_type name adt =
  let bt =
    match adt with
    | Mtype m -> E_mdt m
    | Wtype(p,m,s) -> E_why3(p,m,s)
    | _ -> assert false
  in
  if Context.defined driver then
    register_type name bt
  else
    Context.bind driver builtin_driver (register_type name) bt

let add_type ?source name ~library ?link () =
  if Context.defined driver then
    add_type ?source name ~library ?link ()
  else
    Context.bind driver builtin_driver
      (add_type ?source name ~library ?link) ()

let hack_type name poly =
  if Context.defined driver then hack_type name poly
  else Context.bind driver builtin_driver hack_type name poly

let find_type name =
  Hashtbl.find (cdriver_ro ()).htypes name
let find_type name =
  if Context.defined driver then find_type name
  else Context.bind driver builtin_driver find_type name

let () = Context.set Lang.builtin_types find_type

let new_driver ~id ?(base=builtin_driver)
    ?(descr=id) ?(includes=[]) ?(configure=fun () -> ()) () =
  lock base ;
  let new_driver = {
    driverid = id ;
    description = descr ;
    includes = includes @ base.includes ;
    hlogic = Hashtbl.copy base.hlogic ;
    htypes = Hashtbl.copy base.htypes ;
    hdeps  = Hashtbl.copy base.hdeps ;
    hoptions = Hashtbl.copy base.hoptions ;
    locked = false
  } in
  let old = Context.push driver new_driver in
  configure () ;
  Context.pop driver old ;
  new_driver

(* -------------------------------------------------------------------------- *)
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