Commit 491db38f authored by Allan Blanchard's avatar Allan Blanchard

[Builtin] API: external builtin registration

parent 838879f8
......@@ -19,3 +19,83 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
open Cil_types
module Builtin_builder: sig
(** Builds a [Builtin] module (used by [Transform]) from a [Generator_sig] *)
(** Signature for a new builtin 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_builtin] module to generate the
function cache. The [key] ([override_key]) must identify a function
module Hashtbl: Datatype.Hashtbl
type override_key = Hashtbl.key
(** Name of the implemented builtin function *)
val function_name: string
(** [well_typed_call ret 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 -> exp list -> bool
(** [key_from_call ret args] must return an identifier for the corresponding
call. [key_from_call ret1 args1] and [key_from_call ret2 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 -> 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 [Builtin] 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_builtin].
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 fundec loc] 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 -> fundec -> location -> funspec
module Transform: sig
(** Registers a new [Builtin] to the visitor from the [Generator_sig] module
of this builtin. Each new builtin function generator should call this
val register: (module Builtin_builder.Generator_sig) -> unit
......@@ -62,7 +62,7 @@ PLUGIN_CMO := \
PLUGIN_TESTS_DIRS := string stdlib options
PLUGIN_TESTS_DIRS := string stdlib options api
# Generic part #
/* run.config
OPT: -load-script tests/api/ -builtin -check -print
void mine(void* parameter) ;
void foo(void){
int *i ;
float *f ;
\ No newline at end of file
let function_name = "mine"
let well_typed_call _ = function
| [ e ] ->
let t = Cil.typeOf(Cil.stripCasts e) in
not (Cil.isVoidPtrType t) && Cil.isPointerType t
| _ -> false
let key_from_call _ = function
| [ e ] ->
let t = Cil.typeOf(Cil.stripCasts e) in
Cil.typeOf_pointed t
| _ -> assert false
let retype_args _ = function
| [ e ] -> [ Cil.stripCasts e ]
| _ -> assert false
let generate_function_type t =
let params = [
("x", Cil_types.TPtr(t, []), [])
] in
Cil_types.TFun(Cil.voidType, Some params, false, [])
let generate_prototype t =
let fun_type = generate_function_type t in
let name = function_name ^ "_" ^ match t with
| Cil_types.TInt(_) -> "int"
| Cil_types.TFloat(_) -> "float"
| _ -> assert false (* nothing else in our test *)
name, fun_type
let generate_spec _ _ _ = Cil.empty_funspec ()
let args_for_original _ x = x
let () = Builtin.Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = Hashtbl.key
let function_name = function_name
let well_typed_call = well_typed_call
let key_from_call = key_from_call
let retype_args = retype_args
let generate_prototype = generate_prototype
let generate_spec = generate_spec
let args_for_original = args_for_original
\ No newline at end of file
[kernel] Parsing tests/api/external_builtin_registration.c (with preprocessing)
/* Generated by Frama-C */
void mine(void *parameter);
void mine_float(float *x)
mine((void *)x);
void mine_int(int *x)
mine((void *)x);
void foo(void)
int *i;
float *f;
......@@ -43,9 +43,6 @@ let get_kfs () =
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
let find_stdlib_attr fct =
if not (Cil.hasAttribute "fc_stdlib" fct.vattr) then raise Not_found
module VISet = Cil_datatype.Varinfo.Hptset
class transformer = object(self)
......@@ -85,7 +82,6 @@ class transformer = object(self)
method private find_enabled_builtin fct =
find_stdlib_attr fct ;
let builtin = Hashtbl.find base fct.vname in
let module B = (val builtin: Builtin) in
if not (B.Enabled.get ()) then raise Not_found ;
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment