From 660e007da88b9b09c8f1d2a9ba77a119c14ab646 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 24 Oct 2019 17:18:55 +0200
Subject: [PATCH] [Builtin] Small fix + Doc
---
src/plugins/builtin/README.md | 130 +++++++++++++++
src/plugins/builtin/basic_blocks.ml | 6 +-
src/plugins/builtin/basic_blocks.mli | 155 +++++++++++++++++-
src/plugins/builtin/options.mli | 7 +
.../tests/stdlib/oracle/calloc.res.oracle | 20 +--
.../tests/stdlib/oracle/malloc.res.oracle | 16 +-
.../tests/string/oracle/memcmp.res.oracle | 10 +-
.../tests/string/oracle/memcpy.res.oracle | 13 +-
.../tests/string/oracle/memmove.res.oracle | 13 +-
.../tests/string/oracle/memset_0.res.oracle | 12 +-
.../tests/string/oracle/memset_FF.res.oracle | 12 +-
src/plugins/builtin/transform.mli | 12 ++
12 files changed, 348 insertions(+), 58 deletions(-)
create mode 100644 src/plugins/builtin/README.md
diff --git a/src/plugins/builtin/README.md b/src/plugins/builtin/README.md
new file mode 100644
index 00000000000..ffdc7099383
--- /dev/null
+++ b/src/plugins/builtin/README.md
@@ -0,0 +1,130 @@
+# Builtin plugin
+
+## Description
+
+The builtin plugin is meant to build function specialization to C functions in
+a project when the original specification (or prototype of the function) cannot
+be efficiently used by some plugins.
+
+For example, the specification of a function like `memcpy` cannot be efficiently
+used by a plugin like `WP` because it involves `void*` pointers and requires to
+deduce that bytes equality implies (typed) data equality. While for example it
+is easy to produce a typed specification for a type `int`:
+
+```c
+/*@ requires valid_dest: \valid(dest + (0 .. len-1));
+ requires valid_read_src: \valid_read(src + (0 .. len-1));
+ requires separation: \separated(dest + (0 .. len-1), src + (0 .. len-1));
+ ensures copied: ∀ ℤ j0; 0 ≤ j0 < len ⇒ *(dest + j0) ≡ *(src + j0);
+ ensures result: \result ≡ dest;
+ assigns *(dest + (0 .. len - 1)), \result;
+ assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
+ assigns \result \from dest;
+ */
+int *memcpy_int(int *dest, int const *src, size_t len);
+```
+
+That can be easily used by WP.
+
+The role of the Builtin plugin is to find each call for which a builtin
+generator is available and if the call is well-typed according to the generator
+(for example for `memcpy` if `dest` and `src` are both pointers to integers), to
+replace this call with a call to an automatically generated specialization
+corresponding to the call.
+
+## Options
+
+- `-builtin` activate builtin replacement
+- `-builtin-fct=f,...` only replace calls in specified functions (default to all)
+- `-builtin-(no-)<function_name>` activate or deactivate a particular builtin
+ function, defaults to true.
+
+## Available builtin functions
+
+### `string.h`
+
+```c
+int memcmp(void const* s1, void const* s2, size_t len);
+```
+
+The parameters `s1` and `s2` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `s1` or `s2` cannot be `void*`.
+
+```c
+void* memcpy(void * dest, void const* src, size_t len);
+```
+
+The parameters `dest` and `src` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `dest` or `src` cannot be `void*`.
+
+```c
+void* memmove(void * dest, void const* src, size_t len);
+```
+
+The parameters `dest` and `src` must have the same types, except that qualifiers
+and typedefs are ignored. The type of `dest` or `src` cannot be `void*`.
+
+```c
+void* memset(void * ptr, int value, size_t len);
+```
+
+If `ptr` is of `char*` type (include signed and unsigned variants), `value` must
+be a `char`.
+
+If `ptr` is of any other pointer type (except `void*`), `value` must be a
+constant that statically evaluates to `0x00` or `0xFF`.
+
+### `stdlib.h`
+
+```c
+void* calloc(size_t num, size_t size);
+
+{
+ type* res = calloc(...) ;
+}
+```
+
+`calloc` is typed according to the variable that receives its result. It must be
+a pointer type different from `void*`. If the pointed type has a flexible array
+member, `num` is assumed to evaluate to `1` (a precondition is created for this).
+
+```c
+void free(void* ptr);
+```
+
+The type of `ptr` must be different from `void*`.
+
+
+```c
+void* malloc(size_t num, size_t size);
+
+{
+ type* res = calloc(...) ;
+}
+```
+
+`malloc` is typed according to the variable that receives its result. It must be
+a pointer type different from `void*`.
+
+## Adding a new builtin
+
+To add a new builtin, one has to register a new module implementing the
+`Builtin_builder.Generator_sig` module type to the `Transform` module. The
+lasts steps of the code should look like:
+
+```ocaml
+let () = Transform.register (module struct
+ module Hashtbl = ...
+ type override_key = ...
+
+ let function_name = "my_builtin_function"
+ let well_typed_call = ...
+ let key_from_call = ...
+ let retype_args = ...
+ let generate_prototype = ...
+ let generate_spec = ...
+ let args_for_original = ...
+ end)
+```
+
+The role and types of each function is documented in `Builtin_builder.mli`.
\ No newline at end of file
diff --git a/src/plugins/builtin/basic_blocks.ml b/src/plugins/builtin/basic_blocks.ml
index ac48f23160f..2cddd187f02 100644
--- a/src/plugins/builtin/basic_blocks.ml
+++ b/src/plugins/builtin/basic_blocks.ml
@@ -51,6 +51,7 @@ let call_function lval vi args =
Call(lval, (Cil.evar vi), args, loc)
let rec string_of_typ_aux = function
+ | TVoid(_) -> "void"
| TInt(IBool, _) -> "bool"
| TInt(IChar, _) -> "char"
| TInt(ISChar, _) -> "schar"
@@ -67,8 +68,9 @@ let rec string_of_typ_aux = function
| TFloat(FDouble, _) -> "double"
| TFloat(FLongDouble, _) -> "ldouble"
| TPtr(t, _) -> "ptr_" ^ string_of_typ t
- | TEnum (ei, _) -> ei.ename
- | TComp (ci, _, _) -> ci.cname
+ | TEnum (ei, _) -> "e_" ^ ei.ename
+ | TComp (ci, _, _) when ci.cstruct -> "st_" ^ ci.cname
+ | TComp (ci, _, _) -> "un_" ^ ci.cname
| TArray (t, Some e, _, _) ->
"arr" ^ (string_of_exp e) ^ "_" ^ string_of_typ t
| _ -> assert false
diff --git a/src/plugins/builtin/basic_blocks.mli b/src/plugins/builtin/basic_blocks.mli
index 890cd71cab3..b7547d10c24 100644
--- a/src/plugins/builtin/basic_blocks.mli
+++ b/src/plugins/builtin/basic_blocks.mli
@@ -22,44 +22,177 @@
open Cil_types
+(** [string_of_typ t] returns a name generated from the given [t]. This is
+ basically the C name of the type except that:
+ - separator is ["_"],
+ - [unsigned] is ["u"]
+ - [[SIZE]] is ["arrSIZE"],
+ - [*] is ["ptr"],
+ - [enum] is ["e_"],
+ - [struct] is ["st_"],
+ - [union] is ["un_"]
+
+ For example for: [struct X ( * ) [10]], the name is ["ptr_arr10_st_X"].
+*)
+val string_of_typ: typ -> string
+
+(** Returns the type of pointed for a give logic_type *)
+val ttype_of_pointed: logic_type -> logic_type
+
+
+(** {2 C} *)
+
+(** For a type [T], returns [T*] *)
val ptr_of: typ -> typ
+
+(** For a type [T], returns [T const] *)
val const_of: typ -> typ
+(** Finds and returns [size_t] *)
val size_t: unit -> typ
+(** Create a function definition from a name and a type
+ - [vdefined] is positionned to [true]
+ - formals are registered to FormalsDecl
+*)
val prepare_definition: string -> typ -> fundec
+
+(** [call_function ret_lval vi args] creates an instruction
+ - [(ret_lval = ) vi.vname(args)].
+*)
val call_function: lval option -> varinfo -> exp list -> instr
-val string_of_typ: typ -> string
-val ttype_of_pointed: logic_type -> logic_type
+(** {2 Terms} *)
+(** Builds a term from a varinfo *)
val cvar_to_tvar: varinfo -> term
+
+(** [tunref_range ~loc ptr len] builds [*(ptr + (0 .. len-1))] *)
val tunref_range: ?loc:location -> term -> term -> term
+
+(** [tplus ~loc t1 t2] builds [t1+t2] *)
val tplus: ?loc:location -> term -> term -> term
+
+(** [tminus ~loc t1 t2] builds [t1-t2] *)
val tminus: ?loc:location -> term -> term -> term
+
+(** [tdivide ~loc t1 t2] builds [t1/t2] *)
val tdivide: ?loc:location -> term -> term -> term
+
+(** {2 Predicates} *)
+
+(** [pbounds_incl_excl ~loc low v up] builds [low <= v < up]. *)
val pbounds_incl_excl: ?loc:location -> term -> term -> term -> predicate
-val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
-val pvalid_read_len_bytes:
- ?loc:location -> logic_label -> term -> term -> predicate
-val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
+
+(** [plet_len_div_size ~loc ~name_ext ltyp bytes_len pred] buils a predicate:
+ - [\let name = bytes_len / sizeof(ltyp) ; < pred name >]
+
+ with [name = "__fc_<name_ext>len"]. For example, if [pred len] generates an
+ ACSL predicate:
+ - [\forall int x ; 0 <= x < len ==> p[x] == 0],
+
+ [ltyp] is [int], and [bytes_len] is 16, it generates:
+ - [\let __fc_len = bytes_len / sizeof(ltyp) ;
+ \forall int x ; 0 <= x < __fc_len ==> p[x] == 0].
+
+ Parameters:
+ - [loc] defaults to [Cil_datatype.Location.unknown]
+ - [name_ext] defaults to [""]
+ - [ltyp] must be a logic C type
+ - [bytes_len] is a value in bytes that should be divided by the [sizeof(ltyp)]
+ - if the elements contains structures they cannot have flexible array member
+*)
+val plet_len_div_size:
+ ?loc:location -> ?name_ext:string ->
+ logic_type -> term -> (term -> predicate) -> predicate
+
+(** [punfold_all_elems_eq ~loc p1 p2 len] builds a predicate:
+ - [\forall integer j1 ; 0 <= j1 < len ==> p1[j1] == p2[j1]].
+
+ If [p1[j1]] is itself an array, it recursively builds a predicate:
+ - [\forall integer j2 ; 0 <= j2 < len_of_array ==> ...].
+
+ Parameters:
+ - [p1] and [p2] must be pointers to the same type
+*)
val punfold_all_elems_eq: ?loc:location -> term -> term -> term -> predicate
+
+(** [punfold_all_elems_pred ~loc ptr len pred] builds a predicate:
+ - [\forall integer j ; 0 <= j1 < len ==> < pred (\*(ptr + j1)) >].
+
+ If [ptr[j1]] is a compound type (array or structure), it recursively builds
+ a predicate on each element (either by introducing a new [\forall] for
+ arrays or a conjunction for structure fields).
+
+ - [ptr] must be a pointer
+ - [pred] must be applicable on simple types or pointers
+ - if the elements contains structures they cannot have flexible array member
+*)
val punfold_all_elems_pred:
?loc:location -> term -> term ->
(?loc: location -> term -> predicate) -> predicate
+
+(** [punfold_flexible_struct_pred ~loc struct bytes_len pred].
+
+ For a [struct] term of C type [struct X { ... ; Type a[]; };], it generates
+ a predicate:
+ - [\let __fc_len = (bytes_len - sizeof(struct X)) / sizeof(Type) ;
+ < pred on struct fields > &&
+ \forall integer j ; 0 <= j <= __fc_len ==> < pred on struct.a[j] >]
+
+ If met components are compound, it behaves like [punfold_all_elems_pred].
+
+ Parameters:
+ - [struct] must be a (term) structure with a flexible array member
+ - [bytes_len] is the length of the structure in bytes
+ - [pred] must be applicable on simple types or pointers
+*)
val punfold_flexible_struct_pred:
?loc:location -> term -> term ->
(?loc: location -> term -> predicate) -> predicate
+(** [pvalid_len_bytes ~loc label ptr bytes_len] generates a predicate
+ - [\valid{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))].
+
+ Parameters:
+ - [ptr] must be a term of pointer type.
+*)
+val pvalid_len_bytes: ?loc:location -> logic_label -> term -> term -> predicate
+
+(** [pvalid_read_len_bytes ~loc label ptr bytes_len] generates a predicate
+ - [\valid_read{label}(ptr + (0 .. (len_bytes/sizeof(\*ptr))))].
+
+ Parameters:
+ - [ptr] must be a term of pointer type.
+ *)
+val pvalid_read_len_bytes:
+ ?loc:location -> logic_label -> term -> term -> predicate
+
+(** [pcorrect_len_bytes ~loc ltyp bytes_len] returns a predicate
+ [bytes_len % sizeof(ltyp) == 0].
+*)
+val pcorrect_len_bytes: ?loc:location -> logic_type -> term -> predicate
+
+(** [pseparated_memories ~loc p1 len1 p2 len2] returns a predicate:
+ - [\separated(p1 + (0 .. len1), p2 + (0 .. len2))]
+
+ Parameters:
+ - [p1] and [p2] must be of pointer type
+*)
val pseparated_memories:
?loc:location -> term -> term -> term -> term -> predicate
-val plet_len_div_size:
- ?loc:location -> ?name_ext:string ->
- logic_type -> term -> (term -> predicate) -> predicate
+(** {2 Specification} *)
+(** Builds a behavior from its components. If a component is missing,
+ it defaults to:
+ - [name]: [Cil.default_behavior_name]
+ - [requires], [ensures], [extension]: [[]]
+ - [assigns]: = [WritesAny]
+ - [alloc]: [FreeAllocAny]
+*)
val make_behavior:
?name:string ->
?assumes:identified_predicate list ->
@@ -71,6 +204,10 @@ val make_behavior:
unit ->
behavior
+(** Builds a funspec from a list of behaviors.
+ - [termination] defaults to [None]
+ - [complete_disjoint] default to all disjoint, all complete
+*)
val make_funspec:
behavior list ->
?termination:identified_predicate option ->
diff --git a/src/plugins/builtin/options.mli b/src/plugins/builtin/options.mli
index 3ff7f8a32bc..8086aca2afe 100644
--- a/src/plugins/builtin/options.mli
+++ b/src/plugins/builtin/options.mli
@@ -22,9 +22,16 @@
include Plugin.General_services
+(** Builtin transformtion enabled *)
module Enabled : Parameter_sig.Bool
+
+(** Set of kernel function provided for transformation *)
module Kfs : Parameter_sig.Kernel_function_set
+(** Used by [Builtin_builder] to generate builtin options. For a given builtin,
+ the module generate an option "-builtin-(no-)<function_name>" that defaults
+ to true.
+*)
module NewBuiltin
(B : sig val function_name: string end) : Parameter_sig.Bool
diff --git a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
index e116acefd06..aad87a80a21 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
+++ b/src/plugins/builtin/tests/stdlib/oracle/calloc.res.oracle
@@ -49,7 +49,7 @@ struct Flex {
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct Flex *calloc_Flex(size_t num, size_t size)
+struct Flex *calloc_st_Flex(size_t num, size_t size)
{
struct Flex *__retres;
__retres = (struct Flex *)calloc(num,size);
@@ -170,7 +170,7 @@ char *calloc_char(size_t num, size_t size)
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct X *calloc_X(size_t num, size_t size)
+struct X *calloc_st_X(size_t num, size_t size)
{
struct X *__retres;
__retres = (struct X *)calloc(num,size);
@@ -256,12 +256,12 @@ int main(void)
int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int));
float *pf = calloc_float((unsigned int)10,sizeof(float));
- struct X *px = calloc_X((unsigned int)10,sizeof(struct X));
+ struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char));
int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
struct Flex *f =
- calloc_Flex((unsigned int)1,
- sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ calloc_st_Flex((unsigned int)1,
+ sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char));
__retres = 0;
return __retres;
@@ -320,7 +320,7 @@ struct Flex {
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct Flex *calloc_Flex(size_t num, size_t size)
+struct Flex *calloc_st_Flex(size_t num, size_t size)
{
struct Flex *__retres;
__retres = (struct Flex *)calloc(num,size);
@@ -444,7 +444,7 @@ char *calloc_char(size_t num, size_t size)
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct X *calloc_X(size_t num, size_t size)
+struct X *calloc_st_X(size_t num, size_t size)
{
struct X *__retres;
__retres = (struct X *)calloc(num,size);
@@ -532,12 +532,12 @@ int main(void)
int __retres;
int *pi = calloc_int((unsigned int)10,sizeof(int));
float *pf = calloc_float((unsigned int)10,sizeof(float));
- struct X *px = calloc_X((unsigned int)10,sizeof(struct X));
+ struct X *px = calloc_st_X((unsigned int)10,sizeof(struct X));
char *pc = calloc_char((unsigned int)10,sizeof(char));
int (*pa)[10] = calloc_arr10_int((unsigned int)10,sizeof(int [10]));
struct Flex *f =
- calloc_Flex((unsigned int)1,
- sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ calloc_st_Flex((unsigned int)1,
+ sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = calloc((unsigned int)10,sizeof(char));
__retres = 0;
return __retres;
diff --git a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle b/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
index c552df1af72..a43a99fddf6 100644
--- a/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
+++ b/src/plugins/builtin/tests/stdlib/oracle/malloc.res.oracle
@@ -35,7 +35,7 @@ struct Flex {
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct Flex *malloc_Flex(size_t size)
+struct Flex *malloc_st_Flex(size_t size)
{
struct Flex *__retres;
__retres = (struct Flex *)malloc(size);
@@ -128,7 +128,7 @@ char *malloc_char(size_t size)
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct X *malloc_X(size_t size)
+struct X *malloc_st_X(size_t size)
{
struct X *__retres;
__retres = (struct X *)malloc(size);
@@ -202,11 +202,11 @@ int main(void)
int __retres;
int *pi = malloc_int(sizeof(int) * (unsigned int)10);
float *pf = malloc_float(sizeof(float) * (unsigned int)10);
- struct X *px = malloc_X(sizeof(struct X) * (unsigned int)10);
+ struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
char *pc = malloc_char((unsigned int)10);
int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
struct Flex *f =
- malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10);
__retres = 0;
return __retres;
@@ -252,7 +252,7 @@ struct Flex {
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct Flex *malloc_Flex(size_t size)
+struct Flex *malloc_st_Flex(size_t size)
{
struct Flex *__retres;
__retres = (struct Flex *)malloc(size);
@@ -345,7 +345,7 @@ char *malloc_char(size_t size)
complete behaviors no_allocation, allocation;
disjoint behaviors no_allocation, allocation;
*/
-struct X *malloc_X(size_t size)
+struct X *malloc_st_X(size_t size)
{
struct X *__retres;
__retres = (struct X *)malloc(size);
@@ -419,11 +419,11 @@ int main(void)
int __retres;
int *pi = malloc_int(sizeof(int) * (unsigned int)10);
float *pf = malloc_float(sizeof(float) * (unsigned int)10);
- struct X *px = malloc_X(sizeof(struct X) * (unsigned int)10);
+ struct X *px = malloc_st_X(sizeof(struct X) * (unsigned int)10);
char *pc = malloc_char((unsigned int)10);
int (*pa)[10] = malloc_arr10_int(sizeof(int [10]) * (unsigned int)10);
struct Flex *f =
- malloc_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
+ malloc_st_Flex(sizeof(struct Flex) + (unsigned int)3 * sizeof(int));
void *v = malloc(sizeof(char) * (unsigned int)10);
__retres = 0;
return __retres;
diff --git a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
index 1e239406f5d..7b39a351f64 100644
--- a/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memcmp.res.oracle
@@ -64,7 +64,7 @@ int with_named(named * /*[10]*/ s1, named * /*[10]*/ s2)
\from (indirect: *(s1 + (0 .. len - 1))),
(indirect: *(s2 + (0 .. len - 1)));
*/
-int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
{
int __retres;
__retres = memcmp((void const *)s1,(void const *)s2,len);
@@ -74,7 +74,7 @@ int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
int structure(struct X * /*[10]*/ s1, struct X * /*[10]*/ s2)
{
int tmp;
- tmp = memcmp_X(s1,s2,(unsigned int)10 * sizeof(struct X));
+ tmp = memcmp_st_X(s1,s2,(unsigned int)10 * sizeof(struct X));
return tmp;
}
@@ -233,7 +233,7 @@ int with_named(named *s1, named *s2)
\from (indirect: *(s1 + (0 .. len - 1))),
(indirect: *(s2 + (0 .. len - 1)));
*/
-int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
+int memcmp_st_X(struct X const *s1, struct X const *s2, size_t len)
{
int __retres;
__retres = memcmp((void const *)s1,(void const *)s2,len);
@@ -243,8 +243,8 @@ int memcmp_X(struct X const *s1, struct X const *s2, size_t len)
int structure(struct X *s1, struct X *s2)
{
int tmp;
- tmp = memcmp_X((struct X const *)s1,(struct X const *)s2,
- (unsigned int)10 * sizeof(struct X));
+ tmp = memcmp_st_X((struct X const *)s1,(struct X const *)s2,
+ (unsigned int)10 * sizeof(struct X));
return tmp;
}
diff --git a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
index b0d5a8eaba6..ced9071c356 100644
--- a/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memcpy.res.oracle
@@ -69,7 +69,7 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
*/
-struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
{
struct X *__retres;
__retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
@@ -78,8 +78,8 @@ struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{
- struct X *res = memcpy_X(dest,src,(unsigned int)10 * sizeof(struct X));
- memcpy_X(src,res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memcpy_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
+ memcpy_st_X(src,res,(unsigned int)10 * sizeof(struct X));
return;
}
@@ -249,7 +249,7 @@ void with_named(named *src, named *dest)
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
*/
-struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
+struct X *memcpy_st_X(struct X *dest, struct X const *src, size_t len)
{
struct X *__retres;
__retres = (struct X *)memcpy((void *)dest,(void const *)src,len);
@@ -259,8 +259,9 @@ struct X *memcpy_X(struct X *dest, struct X const *src, size_t len)
void structure(struct X *src, struct X *dest)
{
struct X *res =
- memcpy_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
- memcpy_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+ memcpy_st_X(dest,(struct X const *)src,
+ (unsigned int)10 * sizeof(struct X));
+ memcpy_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
return;
}
diff --git a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
index 75ff285878b..7b7122fb41a 100644
--- a/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memmove.res.oracle
@@ -61,7 +61,7 @@ void with_named(named * /*[10]*/ src, named * /*[10]*/ dest)
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
*/
-struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
{
struct X *__retres;
__retres = (struct X *)memmove((void *)dest,(void const *)src,len);
@@ -70,8 +70,8 @@ struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
void structure(struct X * /*[10]*/ src, struct X * /*[10]*/ dest)
{
- struct X *res = memmove_X(dest,src,(unsigned int)10 * sizeof(struct X));
- memmove_X(src,res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memmove_st_X(dest,src,(unsigned int)10 * sizeof(struct X));
+ memmove_st_X(src,res,(unsigned int)10 * sizeof(struct X));
return;
}
@@ -225,7 +225,7 @@ void with_named(named *src, named *dest)
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
*/
-struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
+struct X *memmove_st_X(struct X *dest, struct X const *src, size_t len)
{
struct X *__retres;
__retres = (struct X *)memmove((void *)dest,(void const *)src,len);
@@ -235,8 +235,9 @@ struct X *memmove_X(struct X *dest, struct X const *src, size_t len)
void structure(struct X *src, struct X *dest)
{
struct X *res =
- memmove_X(dest,(struct X const *)src,(unsigned int)10 * sizeof(struct X));
- memmove_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
+ memmove_st_X(dest,(struct X const *)src,
+ (unsigned int)10 * sizeof(struct X));
+ memmove_st_X(src,(struct X const *)res,(unsigned int)10 * sizeof(struct X));
return;
}
diff --git a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
index ecaeedab7db..ba939b95fc5 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_0.res.oracle
@@ -157,7 +157,7 @@ void with_named(named * /*[10]*/ dest)
assigns *(ptr + (0 .. num - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_X_0(struct X *ptr, size_t num)
+struct X *memset_st_X_0(struct X *ptr, size_t num)
{
struct X *__retres;
__retres = (struct X *)memset((void *)ptr,0,num);
@@ -166,8 +166,8 @@ struct X *memset_X_0(struct X *ptr, size_t num)
void structure(struct X * /*[10]*/ dest)
{
- struct X *res = memset_X_0(dest,(unsigned int)10 * sizeof(struct X));
- memset_X_0(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
+ memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
return;
}
@@ -418,7 +418,7 @@ void with_named(named *dest)
assigns *(ptr + (0 .. num - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_X_0(struct X *ptr, size_t num)
+struct X *memset_st_X_0(struct X *ptr, size_t num)
{
struct X *__retres;
__retres = (struct X *)memset((void *)ptr,0,num);
@@ -427,8 +427,8 @@ struct X *memset_X_0(struct X *ptr, size_t num)
void structure(struct X *dest)
{
- struct X *res = memset_X_0(dest,(unsigned int)10 * sizeof(struct X));
- memset_X_0(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_0(dest,(unsigned int)10 * sizeof(struct X));
+ memset_st_X_0(res,(unsigned int)10 * sizeof(struct X));
return;
}
diff --git a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
index a50c0bf600c..1115c29a5ac 100644
--- a/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
+++ b/src/plugins/builtin/tests/string/oracle/memset_FF.res.oracle
@@ -295,7 +295,7 @@ void with_named(named * /*[10]*/ dest)
assigns *(ptr + (0 .. num - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_X_FF(struct X *ptr, size_t num)
+struct X *memset_st_X_FF(struct X *ptr, size_t num)
{
struct X *__retres;
__retres = (struct X *)memset((void *)ptr,255,num);
@@ -304,8 +304,8 @@ struct X *memset_X_FF(struct X *ptr, size_t num)
void structure(struct X * /*[10]*/ dest)
{
- struct X *res = memset_X_FF(dest,(unsigned int)10 * sizeof(struct X));
- memset_X_FF(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
+ memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
return;
}
@@ -704,7 +704,7 @@ void with_named(named *dest)
assigns *(ptr + (0 .. num - 1)) \from \nothing;
assigns \result \from ptr;
*/
-struct X *memset_X_FF(struct X *ptr, size_t num)
+struct X *memset_st_X_FF(struct X *ptr, size_t num)
{
struct X *__retres;
__retres = (struct X *)memset((void *)ptr,255,num);
@@ -713,8 +713,8 @@ struct X *memset_X_FF(struct X *ptr, size_t num)
void structure(struct X *dest)
{
- struct X *res = memset_X_FF(dest,(unsigned int)10 * sizeof(struct X));
- memset_X_FF(res,(unsigned int)10 * sizeof(struct X));
+ struct X *res = memset_st_X_FF(dest,(unsigned int)10 * sizeof(struct X));
+ memset_st_X_FF(res,(unsigned int)10 * sizeof(struct X));
return;
}
diff --git a/src/plugins/builtin/transform.mli b/src/plugins/builtin/transform.mli
index 10e265d8719..72800ee3426 100644
--- a/src/plugins/builtin/transform.mli
+++ b/src/plugins/builtin/transform.mli
@@ -20,5 +20,17 @@
(* *)
(**************************************************************************)
+(** Module for AST transformation *)
+
+(** Registers a new [Builtin] to the visitor from the [Generator_sig] module
+ of this builtin. Each new builtin function generator should call this
+ globally.
+*)
val register: (module Builtin_builder.Generator_sig) -> unit
+
+(** In all selected functions of the given file, for all function call, if there
+ exists a builtin module for this function, and the call is well-typed,
+ replaces it with a call to the generated override function and inserted the
+ generated function in the AST.
+*)
val transform: Cil_types.file -> unit
--
GitLab