From 8485cd471969b628568ee5c82a363b620b6d6346 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 14 Oct 2019 15:31:04 +0200
Subject: [PATCH] [Builtin] Now generates function definitions
---
src/plugins/builtin/basic_blocks.ml | 25 +++++++
src/plugins/builtin/basic_blocks.mli | 4 ++
src/plugins/builtin/builtin_cache.ml | 23 +++---
src/plugins/builtin/builtin_cache.mli | 4 +-
src/plugins/builtin/memcmp.ml | 72 ++++++++++---------
src/plugins/builtin/memcpy.ml | 65 +++++++++--------
src/plugins/builtin/memmove.ml | 64 +++++++++--------
.../tests/functions/oracle/memcmp.res.oracle | 32 +++++++--
.../tests/functions/oracle/memcpy.res.oracle | 32 +++++++--
.../tests/functions/oracle/memmove.res.oracle | 32 +++++++--
src/plugins/builtin/tests/test_config | 2 +-
src/plugins/builtin/transform.ml | 39 +++++-----
src/plugins/builtin/transform.mli | 4 +-
13 files changed, 257 insertions(+), 141 deletions(-)
diff --git a/src/plugins/builtin/basic_blocks.ml b/src/plugins/builtin/basic_blocks.ml
index 633b0cb10fa..65ae46edd4e 100644
--- a/src/plugins/builtin/basic_blocks.ml
+++ b/src/plugins/builtin/basic_blocks.ml
@@ -31,6 +31,31 @@ let const_of t = Cil.typeAddAttributes [Attr("const", [])] t
let size_t () =
Globals.Types.find_type Logic_typing.Typedef "size_t"
+let prepare_definition name fun_type =
+ let vi = Cil.makeGlobalVar ~referenced:true name fun_type in
+ let fd = Cil.emptyFunctionFromVI vi in
+ Cil.setFormalsDecl vi fun_type ;
+ fd.sformals <- Cil.getFormalsDecl vi ;
+ fd
+
+let set_function_body fd body =
+ fd.sbody <- body ;
+ fd.svar.vdefined <- true ;
+ File.must_recompute_cfg fd
+
+let call_function lval name args =
+ let open Globals.Functions in
+ let loc = Cil_datatype.Location.unknown in
+ let vi = get_vi (find_by_name name) in
+ let _, typs, _, _ = Cil.splitFunctionTypeVI vi in
+ let typs = Cil.argsToList typs in
+ let gen_arg exp (_, typ, _) =
+ if Cil_datatype.Typ.equal vi.vtype typ then exp
+ else Cil.mkCast exp typ
+ in
+ let args = List.map2 gen_arg args typs in
+ Call(lval, (Cil.evar vi), args, loc)
+
let rec string_of_typ_aux = function
| TInt(IBool, _) -> "bool"
| TInt(IChar, _) -> "char"
diff --git a/src/plugins/builtin/basic_blocks.mli b/src/plugins/builtin/basic_blocks.mli
index 7ece0de7ecc..642e8c1b69f 100644
--- a/src/plugins/builtin/basic_blocks.mli
+++ b/src/plugins/builtin/basic_blocks.mli
@@ -27,6 +27,10 @@ val const_of: typ -> typ
val size_t: unit -> typ
+val prepare_definition: string -> typ -> fundec
+val set_function_body: fundec -> block -> unit
+val call_function: lval option -> string -> exp list -> instr
+
val string_of_typ: typ -> string
val ttype_of_pointed: logic_type -> logic_type
diff --git a/src/plugins/builtin/builtin_cache.ml b/src/plugins/builtin/builtin_cache.ml
index a4f3ac5ed30..e1ad5716ab7 100644
--- a/src/plugins/builtin/builtin_cache.ml
+++ b/src/plugins/builtin/builtin_cache.ml
@@ -21,19 +21,19 @@
(**************************************************************************)
module type Table = sig
- val get_function: Cil_types.typ -> Cil_types.varinfo
+ val get_varinfo: Cil_types.typ -> Cil_types.varinfo
val get_globals: Cil_types.location -> Cil_types.global list
val mark_as_computed: ?project:Project.t -> unit -> unit
end
module type Generator = sig
val function_name: String.t
- val build_prototype: Cil_types.typ -> Cil_types.varinfo
+ val build_function: Cil_types.typ -> Cil_types.fundec
val build_spec: Cil_types.varinfo -> Cil_types.location -> Cil_types.funspec
end
module Make_internal_table (M: Generator) =
- (State_builder.Hashtbl(Cil_datatype.Typ.Hashtbl) (Cil_datatype.Varinfo)
+ (State_builder.Hashtbl(Cil_datatype.Typ.Hashtbl) (Cil_datatype.Fundec)
(struct
let size = 5
let dependencies = [Ast.self]
@@ -42,19 +42,20 @@ module Make_internal_table (M: Generator) =
module Make (Generator: Generator) = struct
module Internal_table = Make_internal_table(Generator)
+ open Cil_types
- let get_function t = try
- Internal_table.find t
+ let get_varinfo t = try
+ (Internal_table.find t).svar
with Not_found ->
- let fct = Generator.build_prototype t in
+ let fct = Generator.build_function t in
Internal_table.add t fct ;
- fct
+ fct.svar
let get_globals loc =
- let finalize vi =
- let spec = Generator.build_spec vi loc in
- Globals.Functions.replace_by_declaration spec vi loc ;
- Cil_types.GFunDecl(Cil.empty_funspec(), vi, loc)
+ let finalize fd =
+ let spec = Generator.build_spec (fd.svar) loc in
+ Globals.Functions.replace_by_definition spec fd loc ;
+ Cil_types.GFun(fd, loc)
in
Internal_table.fold (fun _ vi l -> (finalize vi) :: l) []
diff --git a/src/plugins/builtin/builtin_cache.mli b/src/plugins/builtin/builtin_cache.mli
index 1252adcfc6f..c8c5c52968d 100644
--- a/src/plugins/builtin/builtin_cache.mli
+++ b/src/plugins/builtin/builtin_cache.mli
@@ -22,12 +22,12 @@
module type Generator = sig
val function_name: String.t
- val build_prototype: Cil_types.typ -> Cil_types.varinfo
+ val build_function: Cil_types.typ -> Cil_types.fundec
val build_spec: Cil_types.varinfo -> Cil_types.location -> Cil_types.funspec
end
module type Table = sig
- val get_function: Cil_types.typ -> Cil_types.varinfo
+ val get_varinfo: Cil_types.typ -> Cil_types.varinfo
val get_globals: Cil_types.location -> Cil_types.global list
val mark_as_computed: ?project:Project.t -> unit -> unit
end
diff --git a/src/plugins/builtin/memcmp.ml b/src/plugins/builtin/memcmp.ml
index 89fdc1c43b3..fe1caaaa3f3 100644
--- a/src/plugins/builtin/memcmp.ml
+++ b/src/plugins/builtin/memcmp.ml
@@ -38,14 +38,14 @@ let presult_memcmp ?loc p1 p2 len =
let res = prel ?loc (Req, (tresult ?loc Cil.intType), (tinteger ?loc 0)) in
piff ?loc (res, eq)
-let generate_assigns loc t s1 s2 len =
+let generate_assigns loc s1 s2 len =
let indirect_range loc s len =
let t = { (tunref_range ~loc s len) with term_name = ["indirect"] } in
new_identified_term t
in
let s1_range = indirect_range loc s1 len in
let s2_range = indirect_range loc s2 len in
- let result = new_identified_term (tresult t) in
+ let result = new_identified_term (tresult Cil.intType) in
let res = result, From [s1_range ; s2_range] in
Writes [ res ]
@@ -62,63 +62,69 @@ let generate_spec vi loc =
| [ s1 ; s2 ; len ] -> s1, s2, len
| _ -> assert false
in
- let t = c_s1.vtype in
let s1 = cvar_to_tvar c_s1 in
let s2 = cvar_to_tvar c_s2 in
let len = cvar_to_tvar clen in
let requires = generate_requires loc s1 s2 len in
- let assigns = generate_assigns loc t s1 s2 len in
+ let assigns = generate_assigns loc s1 s2 len in
let ensures = generate_ensures loc s1 s2 len in
make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-let generate_prototype t =
- let name = function_name ^ "_" ^ (string_of_typ t) in
+let generate_function_type t =
let t = ptr_of (const_of t) in
let params = [
("s1", t, []) ;
("s2", t, []) ;
("len", size_t (), [])
] in
- let fun_t = TFun(Cil.intType, Some params, false, []) in
- let vi = Cil.makeGlobalVar ~referenced:true name fun_t in
- Cil.setFormalsDecl vi fun_t ;
- vi
+ TFun(Cil.intType, Some params, false, [])
+
+let generate_body fd =
+ let loc = Cil_datatype.Location.unknown in
+ let rv = Cil.makeLocalVar fd "__retres" Cil.intType in
+ let args = List.map Cil.evar fd.sformals in
+ let call = Instr(call_function (Some (Var rv, NoOffset)) function_name args) in
+ let ret = Return (Some (Cil.evar rv), loc) in
+ let block = Cil.mkBlock (List.map Cil.mkStmt [ call ; ret]) in
+ block.blocals <- [ rv ] ;
+ block
+
+let generate_function t =
+ let name = function_name ^ "_" ^ (string_of_typ t) in
+ let fun_t = generate_function_type t in
+ let fd = prepare_definition name fun_t in
+ set_function_body fd (generate_body fd) ;
+ fd
module Table = Builtin_cache.Make(struct
let function_name = function_name
- let build_prototype = generate_prototype
+ let build_function = generate_function
let build_spec = generate_spec
end)
let type_from_parameter x =
- let x = Cil.stripCasts x in
let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
let xt = Cil.type_remove_qualifier_attributes_deep xt in
Cil.typeOf_pointed xt
-let well_typed_parameters s1 s2 =
- let s1_t = type_from_parameter s1 in
- let s2_t = type_from_parameter s2 in
- Cil_datatype.Typ.equal s1_t s2_t
-
-let create_call fct (s1, s2, len) =
- if well_typed_parameters s1 s2 then
- let typ = type_from_parameter s1 in
- let fct = Table.get_function typ in
+let replace_call = function
+ | (_fct, [ s1 ; s2 ; len ]) ->
let s1 = Cil.stripCasts s1 in
let s2 = Cil.stripCasts s2 in
- fct, (s1, s2, len)
- else
- fct, (s1, s2, len)
-
-let replace_call = function
- | Call(r, ({ enode = Lval((Var fct), NoOffset) } as e), [ s1 ; s2 ; len ], loc) ->
- let fct, (s1, s2, len) = create_call fct (s1, s2, len) in
- Call(r, { e with enode = Lval((Var fct), NoOffset) }, [ s1 ; s2 ; len ], loc)
- | Local_init(r, ConsInit(fct, [ s1 ; s2 ; len ], Plain_func), loc) ->
- let fct, (s1, s2, len) = create_call fct (s1, s2, len) in
- Local_init(r, ConsInit(fct, [ s1 ; s2 ; len ], Plain_func), loc)
- | _ -> assert false
+ let s1_t = type_from_parameter s1 in
+ let s2_t = type_from_parameter s2 in
+ if Cil_datatype.Typ.equal s1_t s2_t then
+ (Table.get_varinfo s1_t), [ s1 ; s2 ; len ]
+ else
+ let msg =
+ Format.asprintf "incompatible types for %s: src:%a(%a) dest:%a(%a)"
+ function_name
+ Cil_printer.pp_exp s1 Cil_printer.pp_typ s1_t
+ Cil_printer.pp_exp s2 Cil_printer.pp_typ s2_t
+ in
+ raise (Transform.Bad_typing msg)
+ | (_, _) ->
+ raise (Transform.Bad_typing ("Expected 3 arguments for " ^ function_name))
let () = Transform.register (module struct
let function_name = function_name
diff --git a/src/plugins/builtin/memcpy.ml b/src/plugins/builtin/memcpy.ml
index 5ecf6c306bb..0beafb0463d 100644
--- a/src/plugins/builtin/memcpy.ml
+++ b/src/plugins/builtin/memcpy.ml
@@ -73,8 +73,7 @@ let generate_spec vi loc =
let ensures = generate_ensures loc t dest src len in
make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-let generate_prototype t =
- let name = function_name ^ "_" ^ (string_of_typ t) in
+let generate_function_type t =
let dt = ptr_of t in
let st = ptr_of (const_of t) in
let params = [
@@ -82,46 +81,54 @@ let generate_prototype t =
("src", st, []) ;
("len", size_t (), [])
] in
- let fun_t = TFun(dt, Some params, false, []) in
- let vi = Cil.makeGlobalVar ~referenced:true name fun_t in
- Cil.setFormalsDecl vi fun_t ;
- vi
+ TFun(dt, Some params, false, [])
+
+let generate_body t fd =
+ let loc = Cil_datatype.Location.unknown in
+ let rv = Cil.makeLocalVar fd "__retres" (TPtr(t, [])) in
+ let args = List.map Cil.evar fd.sformals in
+ let call = Instr(call_function (Some (Var rv, NoOffset)) function_name args) in
+ let ret = Return (Some (Cil.evar rv), loc) in
+ let block = Cil.mkBlock (List.map Cil.mkStmt [ call ; ret]) in
+ block.blocals <- [ rv ] ;
+ block
+
+let generate_function t =
+ let name = function_name ^ "_" ^ (string_of_typ t) in
+ let fun_t = generate_function_type t in
+ let fd = prepare_definition name fun_t in
+ set_function_body fd (generate_body t fd) ;
+ fd
module Table = Builtin_cache.Make(struct
let function_name = function_name
- let build_prototype = generate_prototype
+ let build_function = generate_function
let build_spec = generate_spec
end)
let type_from_parameter x =
- let x = Cil.stripCasts x in
let xt = Cil.unrollTypeDeep (Cil.typeOf x) in
let xt = Cil.type_remove_qualifier_attributes_deep xt in
Cil.typeOf_pointed xt
-let well_typed_parameters dest src =
- let dt = type_from_parameter dest in
- let st = type_from_parameter src in
- Cil_datatype.Typ.equal dt st
-
-let create_call fct (dest, src, len) =
- if well_typed_parameters dest src then
- let typ = type_from_parameter dest in
- let fct = Table.get_function typ in
+let replace_call = function
+ | (_fct, [ dest ; src ; len ]) ->
let dest = Cil.stripCasts dest in
let src = Cil.stripCasts src in
- fct, (dest, src, len)
- else
- fct, (dest, src, len)
-
-let replace_call = function
- | Call(r, ({ enode = Lval((Var fct), NoOffset) } as e), [ dest ; src ; len ], loc) ->
- let fct, (dest, src, len) = create_call fct (dest, src, len) in
- Call(r, { e with enode = Lval((Var fct), NoOffset) }, [ dest ; src ; len ], loc)
- | Local_init(r, ConsInit(fct, [ dest ; src ; len ], Plain_func), loc) ->
- let fct, (dest, src, len) = create_call fct (dest, src, len) in
- Local_init(r, ConsInit(fct, [ dest ; src ; len ], Plain_func), loc)
- | _ -> assert false
+ let dt = type_from_parameter dest in
+ let st = type_from_parameter src in
+ if Cil_datatype.Typ.equal dt st then
+ (Table.get_varinfo dt), [ dest ; src ; len ]
+ else
+ let msg =
+ Format.asprintf "incompatible types for %s: src:%a(%a) dest:%a(%a)"
+ function_name
+ Cil_printer.pp_exp dest Cil_printer.pp_typ dt
+ Cil_printer.pp_exp src Cil_printer.pp_typ st
+ in
+ raise (Transform.Bad_typing msg)
+ | (_, _) ->
+ raise (Transform.Bad_typing ("Expected 3 arguments for " ^ function_name))
let () = Transform.register (module struct
let function_name = function_name
diff --git a/src/plugins/builtin/memmove.ml b/src/plugins/builtin/memmove.ml
index 0084c68dc78..78f105b3e15 100644
--- a/src/plugins/builtin/memmove.ml
+++ b/src/plugins/builtin/memmove.ml
@@ -68,8 +68,7 @@ let generate_spec vi loc =
let ensures = generate_ensures loc t dest src len in
make_funspec [make_behavior ~requires ~assigns ~ensures ()] ()
-let generate_prototype t =
- let name = function_name ^ "_" ^ (string_of_typ t) in
+let generate_function_type t =
let dt = ptr_of t in
let st = ptr_of (const_of t) in
let params = [
@@ -77,14 +76,28 @@ let generate_prototype t =
("src", st, []) ;
("len", size_t (), [])
] in
- let fun_t = TFun(dt, Some params, false, []) in
- let vi = Cil.makeGlobalVar ~referenced:true name fun_t in
- Cil.setFormalsDecl vi fun_t ;
- vi
+ TFun(dt, Some params, false, [])
+
+let generate_body t fd =
+ let loc = Cil_datatype.Location.unknown in
+ let rv = Cil.makeLocalVar fd "__retres" (TPtr(t, [])) in
+ let args = List.map Cil.evar fd.sformals in
+ let call = Instr(call_function (Some (Var rv, NoOffset)) function_name args) in
+ let ret = Return (Some (Cil.evar rv), loc) in
+ let block = Cil.mkBlock (List.map Cil.mkStmt [ call ; ret]) in
+ block.blocals <- [ rv ] ;
+ block
+
+let generate_function t =
+ let name = function_name ^ "_" ^ (string_of_typ t) in
+ let fun_t = generate_function_type t in
+ let fd = prepare_definition name fun_t in
+ set_function_body fd (generate_body t fd) ;
+ fd
module Table = Builtin_cache.Make(struct
let function_name = function_name
- let build_prototype = generate_prototype
+ let build_function = generate_function
let build_spec = generate_spec
end)
@@ -94,29 +107,24 @@ let type_from_parameter x =
let xt = Cil.type_remove_qualifier_attributes_deep xt in
Cil.typeOf_pointed xt
-let well_typed_parameters dest src =
- let dt = type_from_parameter dest in
- let st = type_from_parameter src in
- Cil_datatype.Typ.equal dt st
-
-let create_call fct (dest, src, len) =
- if well_typed_parameters dest src then
- let typ = type_from_parameter dest in
- let fct = Table.get_function typ in
+let replace_call = function
+ | (_fct, [ dest ; src ; len ]) ->
let dest = Cil.stripCasts dest in
let src = Cil.stripCasts src in
- fct, (dest, src, len)
- else
- fct, (dest, src, len)
-
-let replace_call = function
- | Call(r, ({ enode = Lval((Var fct), NoOffset) } as e), [ dest ; src ; len ], loc) ->
- let fct, (dest, src, len) = create_call fct (dest, src, len) in
- Call(r, { e with enode = Lval((Var fct), NoOffset) }, [ dest ; src ; len ], loc)
- | Local_init(r, ConsInit(fct, [ dest ; src ; len ], Plain_func), loc) ->
- let fct, (dest, src, len) = create_call fct (dest, src, len) in
- Local_init(r, ConsInit(fct, [ dest ; src ; len ], Plain_func), loc)
- | _ -> assert false
+ let dt = type_from_parameter dest in
+ let st = type_from_parameter src in
+ if Cil_datatype.Typ.equal dt st then
+ (Table.get_varinfo dt), [ dest ; src ; len ]
+ else
+ let msg =
+ Format.asprintf "incompatible types for %s: src:%a(%a) dest:%a(%a)"
+ function_name
+ Cil_printer.pp_exp dest Cil_printer.pp_typ dt
+ Cil_printer.pp_exp src Cil_printer.pp_typ st
+ in
+ raise (Transform.Bad_typing msg)
+ | (_, _) ->
+ raise (Transform.Bad_typing ("Expected 3 arguments for " ^ function_name))
let () = Transform.register (module struct
let function_name = function_name
diff --git a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
index 456152c88ff..15722b10875 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
@@ -23,7 +23,12 @@
\from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
(indirect: (*(s2 + (0 .. len - 1)))[0 .. 10 - 1]);
*/
-int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len);
+int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
+{
+ int __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
@@ -42,7 +47,12 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len);
\from (indirect: *(s1 + (0 .. len - 1))),
(indirect: *(s2 + (0 .. len - 1)));
*/
-int memcmp_int(int const *s1, int const *s2, size_t len);
+int memcmp_int(int const *s1, int const *s2, size_t len)
+{
+ int __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
int main(void)
{
@@ -65,9 +75,9 @@ int nested(int (*dest)[10], int (*src)[10], size_t n)
[kernel] Parsing tests/functions/result/memcmp.c (with preprocessing)
[kernel] Parsing tests/functions/memcmp.c (with preprocessing)
[kernel] tests/functions/memcmp.c:3: Warning:
- def'n of func main at tests/functions/memcmp.c:3 (sum 2855) conflicts with the one at tests/functions/result/memcmp.c:46 (sum 4629); keeping the one at tests/functions/result/memcmp.c:46.
+ def'n of func main at tests/functions/memcmp.c:3 (sum 2855) conflicts with the one at tests/functions/result/memcmp.c:56 (sum 4629); keeping the one at tests/functions/result/memcmp.c:56.
[kernel] tests/functions/memcmp.c:10: Warning:
- def'n of func nested at tests/functions/memcmp.c:10 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:56 (sum 1974); keeping the one at tests/functions/result/memcmp.c:56.
+ def'n of func nested at tests/functions/memcmp.c:10 (sum 1087) conflicts with the one at tests/functions/result/memcmp.c:66 (sum 1974); keeping the one at tests/functions/result/memcmp.c:66.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -93,7 +103,12 @@ int nested(int (*dest)[10], int (*src)[10], size_t n)
\from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
(indirect: (*(s2 + (0 .. len - 1)))[0 .. 10 - 1]);
*/
-int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len);
+int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
+{
+ int __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
@@ -113,7 +128,12 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len);
\from (indirect: *(s1 + (0 .. len - 1))),
(indirect: *(s2 + (0 .. len - 1)));
*/
-int memcmp_int(int const *s1, int const *s2, size_t len);
+int memcmp_int(int const *s1, int const *s2, size_t len)
+{
+ int __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
int main(void)
{
diff --git a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
index 86774bd9c82..b9fb245dddd 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
@@ -27,7 +27,12 @@
\from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
-int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
@@ -48,7 +53,12 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
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);
+int *memcpy_int(int *dest, int const *src, size_t len)
+{
+ int *__retres;
+ __retres = (int *)memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
int main(void)
{
@@ -70,9 +80,9 @@ void nested(int (*dest)[10], int (*src)[10], size_t n)
[kernel] Parsing tests/functions/result/memcpy.c (with preprocessing)
[kernel] Parsing tests/functions/memcpy.c (with preprocessing)
[kernel] tests/functions/memcpy.c:3: Warning:
- def'n of func main at tests/functions/memcpy.c:3 (sum 1968) conflicts with the one at tests/functions/result/memcpy.c:52 (sum 3742); keeping the one at tests/functions/result/memcpy.c:52.
+ def'n of func main at tests/functions/memcpy.c:3 (sum 1968) conflicts with the one at tests/functions/result/memcpy.c:62 (sum 3742); keeping the one at tests/functions/result/memcpy.c:62.
[kernel] tests/functions/memcpy.c:10: Warning:
- dropping duplicate def'n of func nested at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:62
+ dropping duplicate def'n of func nested at tests/functions/memcpy.c:10 in favor of that at tests/functions/result/memcpy.c:72
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -102,7 +112,12 @@ void nested(int (*dest)[10], int (*src)[10], size_t n)
\from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
-int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
@@ -124,7 +139,12 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
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);
+int *memcpy_int(int *dest, int const *src, size_t len)
+{
+ int *__retres;
+ __retres = (int *)memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
int main(void)
{
diff --git a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
index 314166b974d..fc95dbda3e2 100644
--- a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
@@ -25,7 +25,12 @@
\from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
-int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
@@ -42,7 +47,12 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
*/
-int *memmove_int(int *dest, int const *src, size_t len);
+int *memmove_int(int *dest, int const *src, size_t len)
+{
+ int *__retres;
+ __retres = (int *)memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
int main(void)
{
@@ -69,9 +79,9 @@ int *nested(int (*dest)[10], int (*src)[10], size_t n)
[kernel] tests/functions/memmove.c:11: Warning:
Body of function nested falls-through. Adding a return statement
[kernel] tests/functions/memmove.c:3: Warning:
- def'n of func main at tests/functions/memmove.c:3 (sum 1968) conflicts with the one at tests/functions/result/memmove.c:44 (sum 3742); keeping the one at tests/functions/result/memmove.c:44.
+ def'n of func main at tests/functions/memmove.c:3 (sum 1968) conflicts with the one at tests/functions/result/memmove.c:54 (sum 3742); keeping the one at tests/functions/result/memmove.c:54.
[kernel] tests/functions/memmove.c:10: Warning:
- def'n of func nested at tests/functions/memmove.c:10 (sum 1974) conflicts with the one at tests/functions/result/memmove.c:54 (sum 4635); keeping the one at tests/functions/result/memmove.c:54.
+ def'n of func nested at tests/functions/memmove.c:10 (sum 1974) conflicts with the one at tests/functions/result/memmove.c:64 (sum 4635); keeping the one at tests/functions/result/memmove.c:64.
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
@@ -97,7 +107,12 @@ int *nested(int (*dest)[10], int (*src)[10], size_t n)
\from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
assigns \result \from dest;
*/
-int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
+int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
+{
+ int (*__retres)[10];
+ __retres = (int (*)[10])memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
/*@ requires aligned_end: len % 4 ≡ 0;
requires
@@ -115,7 +130,12 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10];
assigns *(dest + (0 .. len - 1)) \from *(src + (0 .. len - 1));
assigns \result \from dest;
*/
-int *memmove_int(int *dest, int const *src, size_t len);
+int *memmove_int(int *dest, int const *src, size_t len)
+{
+ int *__retres;
+ __retres = (int *)memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
int main(void)
{
diff --git a/src/plugins/builtin/tests/test_config b/src/plugins/builtin/tests/test_config
index c72c35a2465..467fffb4bcb 100644
--- a/src/plugins/builtin/tests/test_config
+++ b/src/plugins/builtin/tests/test_config
@@ -1 +1 @@
-OPT: @PTEST_FILE@ -builtin -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
+OPT: @PTEST_FILE@ -builtin -print -check -then -ocode @PTEST_DIR@/result/@PTEST_NAME@.c -print -then -no-builtin @PTEST_DIR@/result/@PTEST_NAME@.c @PTEST_FILE@ -ocode="" -print
\ No newline at end of file
diff --git a/src/plugins/builtin/transform.ml b/src/plugins/builtin/transform.ml
index a09358d511d..037c73aaf9a 100644
--- a/src/plugins/builtin/transform.ml
+++ b/src/plugins/builtin/transform.ml
@@ -22,9 +22,11 @@
open Cil_types
+exception Bad_typing of string
+
module type Builtin = sig
val function_name: string
- val replace_call: instr -> instr
+ val replace_call: (varinfo * exp list) -> (varinfo * exp list)
val get_globals: location -> global list
val mark_as_computed: ?project:Project.t -> unit -> unit
end
@@ -45,26 +47,20 @@ let get_globals loc =
in
Hashtbl.fold (fun _ v l -> (get_globals v) @ l) base []
-let called_function = function
- | Call(_, { enode = Lval((Var fct), NoOffset) }, _, _)
- | Local_init(_, ConsInit(fct, _, Plain_func), _) -> fct
- | _ -> assert false
-
-let called_function_name inst =
- let fct = called_function inst in fct.vname
-
-let find_stdlib_attr_in_call inst =
- let fct = called_function inst in
+let find_stdlib_attr fct =
if not (Cil.hasAttribute "fc_stdlib" fct.vattr) then raise Not_found
-let replace_call inst =
+let replace_call (fct, args) =
try
- find_stdlib_attr_in_call inst ;
- let name = called_function_name inst in
- let m = Hashtbl.find base name in
+ find_stdlib_attr fct ;
+ let m = Hashtbl.find base fct.vname in
let module M = (val m: Builtin) in
- M.replace_call inst
- with Not_found -> inst
+ M.replace_call (fct, args)
+ with
+ | Not_found -> (fct, args)
+ | Bad_typing s ->
+ Options.warning ~current:true "Ignored: %s" s ;
+ (fct, args)
class visitor = object(_)
inherit Visitor.frama_c_inplace
@@ -76,6 +72,8 @@ class visitor = object(_)
f.globals <- globals @ f.globals ;
mark_as_computed () ;
Ast.mark_as_changed () ;
+ Ast.mark_as_grown () ;
+ File.reorder_ast () ;
f
in
Cil.DoChildrenPost after
@@ -83,7 +81,12 @@ class visitor = object(_)
method! vinst = function
| Call(_) | Local_init(_, ConsInit(_, _, Plain_func), _) ->
let change = function
- | [i] -> [ replace_call i ]
+ | [ Call(r, ({ enode = Lval((Var fct), NoOffset) } as e), args, loc) ] ->
+ let fct, args = replace_call (fct, args) in
+ [ Call(r, { e with enode = Lval((Var fct), NoOffset) }, args, loc) ]
+ | [ Local_init(r, ConsInit(fct, args, Plain_func), loc) ] ->
+ let fct, args = replace_call (fct, args) in
+ [ Local_init(r, ConsInit(fct, args, Plain_func), loc) ]
| _ -> assert false
in
Cil.DoChildrenPost change
diff --git a/src/plugins/builtin/transform.mli b/src/plugins/builtin/transform.mli
index 53d02fbfc2d..12b6647d509 100644
--- a/src/plugins/builtin/transform.mli
+++ b/src/plugins/builtin/transform.mli
@@ -22,9 +22,11 @@
open Cil_types
+exception Bad_typing of string
+
module type Builtin = sig
val function_name: string
- val replace_call: instr -> instr
+ val replace_call: (varinfo * exp list) -> (varinfo * exp list)
val get_globals: location -> global list
val mark_as_computed: ?project:Project.t -> unit -> unit
end
--
GitLab