diff --git a/src/plugins/builtin/builtin_builder.ml b/src/plugins/builtin/builtin_builder.ml
index 05294da6d68c5825fc8c18f2968be7f425fb7b55..15952538624d65bfd2d03ac646363ff12bfac868 100644
--- a/src/plugins/builtin/builtin_builder.ml
+++ b/src/plugins/builtin/builtin_builder.ml
@@ -31,9 +31,9 @@ module type Generator_sig = sig
val well_typed_call: lval option -> exp list -> bool
val key_from_call: lval option -> exp list -> override_key
val retype_args: override_key -> exp list -> exp list
+ val args_for_original: override_key -> exp list -> exp list
val generate_prototype: override_key -> (string * typ)
val generate_spec: override_key -> fundec -> location -> funspec
- val args_for_original: override_key -> fundec -> exp list
end
module type Builtin = sig
@@ -58,7 +58,8 @@ let build_body caller callee args_generator =
| t -> Some (Cil.makeLocalVar caller "__retres" t)
in
let call =
- let args = args_generator caller in
+ let args = List.map Cil.evar caller.sformals in
+ let args = args_generator args in
Cil.mkStmt (Instr(call_function (opt_map Cil.var ret_var) callee args))
in
let ret = Cil.mkStmt (Return ( (opt_map Cil.evar ret_var), loc)) in
diff --git a/src/plugins/builtin/builtin_builder.mli b/src/plugins/builtin/builtin_builder.mli
index 7e16ff3d2f6b75cf8829217fca8dcc05e2048ad9..82924b9e8ed8a516d63fda22e1b225f6d19e82fc 100644
--- a/src/plugins/builtin/builtin_builder.mli
+++ b/src/plugins/builtin/builtin_builder.mli
@@ -22,30 +22,115 @@
open Cil_types
+(** 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
+ override.
+ *)
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
- val args_for_original: override_key -> fundec -> exp list
end
+(** Signature of a builtin.
+
+ Module built by the [Transform] module from a [Generator_sig].
+ Used to perform the different replacements in the AST. This
+ should be only used by the [Transform] module.
+*)
module type Builtin = sig
+ (** Plugin option that allows to check whether the builtin is enabled. *)
module Enabled: Parameter_sig.Bool
+ (** Same as [Generator_sig.override_key] *)
type override_key
+ (** Same as [Generator_sig.override_key] *)
val function_name: string
+ (** Same as [Generator_sig.override_key] *)
val well_typed_call: lval option -> exp list -> bool
+ (** Same as [Generator_sig.override_key] *)
val key_from_call: lval option -> exp list -> override_key
+ (** Same as [Generator_sig.override_key] *)
val retype_args: override_key -> exp list -> exp list
+
+ (** [get_override key] returns the function generated for [key].
+ This value is cached so that if it does not exist, it is created using the
+ different [Generator_sig] generation functions, else the cached version is
+ returned.
+ *)
val get_override: override_key -> fundec
+
+ (** [get_kfs ()] returns all generated kernel functions for the current
+ project.
+ *)
val get_kfs: unit -> kernel_function list
+
+ (** [mark_as_computed ?project ()] applies the [mark_as_computed] on the
+ internal table.
+ *)
val mark_as_computed: ?project:Project.t -> unit -> unit
end
+(** Generates a [Builtin] from a [Generator_sig] adding all necessary stuff for
+ cache and function definition generation, as well as specification
+ registration. This should only be used by [Transform].
+*)
module Make_builtin (G: Generator_sig) : Builtin
diff --git a/src/plugins/builtin/stdlib/calloc.ml b/src/plugins/builtin/stdlib/calloc.ml
index 1f0b3cf976049d0b81be1358f5f2eb6b03d20a74..88924bfb7b8a0ebba7953a731006d943dd665f50 100644
--- a/src/plugins/builtin/stdlib/calloc.ml
+++ b/src/plugins/builtin/stdlib/calloc.ml
@@ -145,8 +145,7 @@ let key_from_call ret _ =
| None -> assert false
let retype_args _typ args = args
-let args_for_original _typ fd =
- List.map Cil.evar fd.sformals
+let args_for_original _typ args = args
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
diff --git a/src/plugins/builtin/stdlib/free.ml b/src/plugins/builtin/stdlib/free.ml
index 4a0e106eddad54daf5adf66c668488c398b4eb52..ff07eaec2e7173ec3e6ab99d0e0e4adb32dda969 100644
--- a/src/plugins/builtin/stdlib/free.ml
+++ b/src/plugins/builtin/stdlib/free.ml
@@ -98,8 +98,7 @@ let key_from_call _ret args =
| _ -> assert false
let retype_args _typ args = List.map Cil.stripCasts args
-let args_for_original _typ fd =
- List.map Cil.evar fd.sformals
+let args_for_original _typ args = args
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
diff --git a/src/plugins/builtin/stdlib/malloc.ml b/src/plugins/builtin/stdlib/malloc.ml
index e206b2bdcc86b707d0aeb832640022d26a7c0855..f7ddcaba5fc9b02bce885bc76c4ac6621c7efcaa 100644
--- a/src/plugins/builtin/stdlib/malloc.ml
+++ b/src/plugins/builtin/stdlib/malloc.ml
@@ -84,8 +84,7 @@ let key_from_call ret _ =
| None -> assert false
let retype_args _typ args = args
-let args_for_original _typ fd =
- List.map Cil.evar fd.sformals
+let args_for_original _typ args = args
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
diff --git a/src/plugins/builtin/string/memcmp.ml b/src/plugins/builtin/string/memcmp.ml
index bfda47316ec5b6180f43ba7aa4f533c6ea38082a..6399e653ecc6d81c1eb9c07a3623c61f9812810a 100644
--- a/src/plugins/builtin/string/memcmp.ml
+++ b/src/plugins/builtin/string/memcmp.ml
@@ -87,9 +87,6 @@ let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
name, fun_type
-let args_for_original _t fd =
- List.map Cil.evar fd.sformals
-
let type_from_arg x =
let x = Cil.stripCasts x in
let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
@@ -118,6 +115,8 @@ let retype_args override_key = function
[ s1 ; s2 ; len ]
| _ -> failwith "Call to Memmove.retype_args on an ill-typed builtin call"
+let args_for_original _t args = args
+
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
diff --git a/src/plugins/builtin/string/memcpy.ml b/src/plugins/builtin/string/memcpy.ml
index 6c450e5e59c5981585fa5a815c8ce344cf75f44d..4346977aa87fad6f41abf7abdde23b26eb33a8ca 100644
--- a/src/plugins/builtin/string/memcpy.ml
+++ b/src/plugins/builtin/string/memcpy.ml
@@ -93,9 +93,6 @@ let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
name, fun_type
-let args_for_original _t fd =
- List.map Cil.evar fd.sformals
-
let type_from_arg x =
let x = Cil.stripCasts x in
let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
@@ -124,6 +121,8 @@ let retype_args override_key = function
[ dest ; src ; len ]
| _ -> failwith "Call to Memcpy.retype_args on an ill-typed builtin call"
+let args_for_original _t args = args
+
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
diff --git a/src/plugins/builtin/string/memmove.ml b/src/plugins/builtin/string/memmove.ml
index d4b87f7f28818db33b47052bbed063acab7370af..aa200185ca3aa9338a3748092379ece14faba9db 100644
--- a/src/plugins/builtin/string/memmove.ml
+++ b/src/plugins/builtin/string/memmove.ml
@@ -87,9 +87,6 @@ let generate_prototype t =
let name = function_name ^ "_" ^ (string_of_typ t) in
name, fun_type
-let args_for_original _t fd =
- List.map Cil.evar fd.sformals
-
let type_from_arg x =
let x = Cil.stripCasts x in
let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
@@ -118,6 +115,8 @@ let retype_args override_key = function
[ dest ; src ; len ]
| _ -> failwith "Call to Memmove.retype_args on an ill-typed builtin call"
+let args_for_original _t args = args
+
let () = Transform.register (module struct
module Hashtbl = Cil_datatype.Typ.Hashtbl
type override_key = typ
diff --git a/src/plugins/builtin/string/memset.ml b/src/plugins/builtin/string/memset.ml
index 1f6d3d09e67a6e5a83d7fcb13056fda9ad85197e..34c8e2b601cda21483ef768464856b9535b14c4d 100644
--- a/src/plugins/builtin/string/memset.ml
+++ b/src/plugins/builtin/string/memset.ml
@@ -250,12 +250,12 @@ let retype_args (t, e) args =
| _ ->
failwith "Call to Memset.retype_args on an ill-typed builtin call"
-let args_for_original (_t , e) fd =
+let args_for_original (_t , e) args =
match e with
- | None -> List.map Cil.evar fd.sformals
+ | None -> args
| Some n ->
let loc = Cil_datatype.Location.unknown in
- match List.map Cil.evar fd.sformals with
+ match args with
| [ ptr ; len ] -> [ ptr ; (Cil.integer ~loc n) ; len]
| _ -> assert false