Source file `Instantiate.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2023                                               *)
(*    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

module Instantiator_builder: sig
  (** Builds a [Instantiator] module (used by [Transform]) from a [Generator_sig] *)

  (** Signature for a new instantiator generator.

      In order to support a new function, this module must be implemented and
      registered to the [Transform] module.
  *)
  module type Generator_sig = sig
    (** [Hashtbl] module used by the [Make_instantiator] module to generate the
        function cache. The [key] ([override_key]) must identify a function
        override.
    *)
    module Hashtbl: Datatype.Hashtbl
    type override_key = Hashtbl.key

    (** Name of the implemented instantiator function *)
    val function_name: string

    (** [well_typed_call ret fct args] must return true if and only if the
        corresponding call is well typed in the sens that the generator can
        produce a function override for the corresponding return value and
        parameters, according to their types and/or values.
    *)
    val well_typed_call: lval option -> varinfo -> exp list -> bool

    (** [key_from_call ret fct args] must return an identifier for the
        corresponding call. [key_from_call ret1 fct1 args1] and
        [key_from_call ret2 fct2 args2] must equal if and only if the same
        override function can be used for both call. Any call for which
        [well_typed_call] returns true must be able to give a key.
    *)
    val key_from_call: lval option -> varinfo -> exp list -> override_key

    (** [retype_args key args] must returns a new argument list compatible with
        the function identified by [override_key]. [args] is the list of arguments
        that were given to the call for with [Transform] is currently replacing.
        Most of the time, it will consists in removing/changing some casts. But
        note that arguments can be removed (for example if the override is built
        because some constant have specialized).
    *)
    val retype_args: override_key -> exp list -> exp list

    (** [args_for_original key args] must transform the list of parameters of the
        override function such that the new list can be given to the original
        function. For example, if for a call:
        [foo(x, 0, z)]
        The [Instantiator] module generates an override:
        [void foo_spec(int p1, int p3);]
        The received list of expression is [ p1 ; p3 ] and thus the returned list
        should be [ p1 ; 0 ; p3 ] (so that the replaced call [foo_spec(x, z)] has
        the same behavior).
        Note that there is no need to introduce casts to the original type, it is
        introduced by [Make_instantiator].
    *)
    val args_for_original: override_key -> exp list -> exp list

    (** [generate_prototype key] must generate the name and the type corresponding
        to [key].
    *)
    val generate_prototype: override_key -> (string * typ)

    (** [generate_spec key loc fundec] must generate the specification of the
        [fundec] generated from [key]. The location is the one generated by the
        [Transform] visitor. Note that it must return a [funspec] but should
        {b not} register it in [Annotations] tables.
    *)
    val generate_spec: override_key -> location -> fundec -> funspec
  end
end = Instantiator_builder

module Transform: sig
  (** Registers a new [Instantiator] to the visitor from the [Generator_sig] module
      of this instantiator. Each new instantiator function generator should call this
      globally.
  *)
  val register: (module Instantiator_builder.Generator_sig) -> unit
end = Transform

module Global_context:sig
  (** [get_variable name f] searches for an existing variable [name]. If this
      variable does not exists, it is created using [f].

      The obtained varinfo does not need to be registered, nor [f] needs to
      perform the registration, it will be done by the transformation.
  *)
  val get_variable: string -> (unit -> varinfo) -> varinfo
end = Global_context