diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 41c9799d728213bcd1d3af67d98a09370c1b046b..e29fccb1861e052928775f85ed2c0ff0d9c17eee 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -933,6 +933,8 @@ src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/Builtin.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/builtin_builder.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/builtin/builtin_builder.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/builtin/memcmp.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/builtin/Makefile.in b/src/plugins/builtin/Makefile.in
index 702ddb08ba8a3e8e3f600c81ecec9af5adc6572d..c2c0f929c77c68ea118e7390ce3270ca12144c4f 100644
--- a/src/plugins/builtin/Makefile.in
+++ b/src/plugins/builtin/Makefile.in
@@ -37,7 +37,9 @@ PLUGIN_DIR ?= .
PLUGIN_ENABLE := @ENABLE_BUILTIN@
PLUGIN_NAME := Builtin
PLUGIN_CMI :=
-PLUGIN_CMO := basic_blocks options transform memcpy memcmp memmove register
+PLUGIN_CMO := basic_blocks options builtin_builder transform \
+ memcpy memcmp memmove memset \
+ register
PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
#PLUGIN_NO_DEFAULT_TEST := no
diff --git a/src/plugins/builtin/builtin_builder.ml b/src/plugins/builtin/builtin_builder.ml
new file mode 100644
index 0000000000000000000000000000000000000000..12299a7886d7ea054856da8d0b1030bcbf2bc3fb
--- /dev/null
+++ b/src/plugins/builtin/builtin_builder.ml
@@ -0,0 +1,110 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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
+open Basic_blocks
+
+module type Generator_sig = sig
+ module Hashtbl: Datatype.Hashtbl
+ type override_key = Hashtbl.key
+
+ val function_name: string
+ val well_typed_call: exp list -> bool
+ val key_from_call: exp list -> override_key
+ val retype_args: 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
+ module Enabled: Parameter_sig.Bool
+ type override_key
+
+ val function_name: string
+ val well_typed_call: exp list -> bool
+ val key_from_call: exp list -> override_key
+ val retype_args: override_key -> exp list -> exp list
+ val get_override: override_key -> fundec
+ val get_kfs: unit -> kernel_function list
+ val mark_as_computed: ?project:Project.t -> unit -> unit
+end
+
+
+let build_body caller callee args_generator =
+ let open Extlib in
+ let loc = Cil_datatype.Location.unknown in
+ let ret_var = match Cil.getReturnType caller.svar.vtype with
+ | t when Cil.isVoidType t -> None
+ | t -> Some (Cil.makeLocalVar caller "__retres" t)
+ in
+ let call =
+ let args = args_generator caller 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
+ { (Cil.mkBlock [call ; ret]) with blocals = list_of_opt ret_var }
+
+module Make_builtin (G: Generator_sig) = struct
+ include G
+ module Enabled = Options.NewBuiltin (G)
+ module Cache = State_builder.Hashtbl (G.Hashtbl) (Cil_datatype.Fundec)
+ (struct
+ let size = 5
+ let dependencies = []
+ let name = "Builtins." ^ G.function_name
+ end)
+
+ let make_fundec key =
+ let open Globals.Functions in
+ let (name, typ) = G.generate_prototype key in
+ let fd = Basic_blocks.prepare_definition name typ in
+ let orig = get_vi (find_by_name function_name) in
+ let sbody = build_body fd orig (G.args_for_original key) in
+ let fd = { fd with sbody } in
+ Cfg.cfgFun fd ;
+ fd
+
+ let build_function key =
+ let loc = Cil_datatype.Location.unknown in
+ let fd = make_fundec key in
+ let spec = Cil.empty_funspec () in
+ Globals.Functions.replace_by_definition spec fd loc ;
+ let kf = Globals.Functions.get fd.svar in
+ let spec = generate_spec key fd loc in
+ Annotations.add_behaviors Options.emitter kf spec.spec_behavior ;
+ fd
+
+ let get_override key =
+ try
+ Cache.find key
+ with Not_found ->
+ let fd = build_function key in
+ Cache.add key fd ;
+ fd
+
+ (* If you use this before finalization, you'll have problems *)
+ let get_kfs () =
+ Cache.fold (fun _ fd l -> Globals.Functions.get fd.svar :: l) []
+
+ let mark_as_computed = Cache.mark_as_computed
+end
diff --git a/src/plugins/builtin/builtin_builder.mli b/src/plugins/builtin/builtin_builder.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f45a623f37010f689ff20d2b54a371b2ebb7733a
--- /dev/null
+++ b/src/plugins/builtin/builtin_builder.mli
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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 type Generator_sig = sig
+ module Hashtbl: Datatype.Hashtbl
+ type override_key = Hashtbl.key
+
+ val function_name: string
+ val well_typed_call: exp list -> bool
+ val key_from_call: exp list -> override_key
+ val retype_args: 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
+ module Enabled: Parameter_sig.Bool
+ type override_key
+
+ val function_name: string
+ val well_typed_call: exp list -> bool
+ val key_from_call: exp list -> override_key
+ val retype_args: override_key -> exp list -> exp list
+ val get_override: override_key -> fundec
+ val get_kfs: unit -> kernel_function list
+ val mark_as_computed: ?project:Project.t -> unit -> unit
+end
+
+module Make_builtin (G: Generator_sig) : Builtin
diff --git a/src/plugins/builtin/memcmp.ml b/src/plugins/builtin/memcmp.ml
index a5b8bea26479d901ef87f27a1da06dfc8a2194f7..370347fe47383603950bee6e558543c343cf436d 100644
--- a/src/plugins/builtin/memcmp.ml
+++ b/src/plugins/builtin/memcmp.ml
@@ -125,4 +125,4 @@ let () = Transform.register (module struct
let generate_prototype = generate_prototype
let generate_spec = generate_spec
let args_for_original = args_for_original
- end)
\ No newline at end of file
+ end)
diff --git a/src/plugins/builtin/memcpy.ml b/src/plugins/builtin/memcpy.ml
index 717c7009ae1390c71b69016b9a20b9883d6ae5d2..2c5674a0c4e915761528ba86b40a83b5b437b4d6 100644
--- a/src/plugins/builtin/memcpy.ml
+++ b/src/plugins/builtin/memcpy.ml
@@ -129,4 +129,4 @@ let () = Transform.register (module struct
let generate_prototype = generate_prototype
let generate_spec = generate_spec
let args_for_original = args_for_original
- end)
\ No newline at end of file
+ end)
diff --git a/src/plugins/builtin/memmove.ml b/src/plugins/builtin/memmove.ml
index e5b7b6f7ff2640fae0e98409d3d207d0d14aed89..99e4dee3078c2d7aa5192090db288b3c8d8cf29d 100644
--- a/src/plugins/builtin/memmove.ml
+++ b/src/plugins/builtin/memmove.ml
@@ -124,4 +124,4 @@ let () = Transform.register (module struct
let generate_prototype = generate_prototype
let generate_spec = generate_spec
let args_for_original = args_for_original
- end)
\ No newline at end of file
+ end)
diff --git a/src/plugins/builtin/options.mli b/src/plugins/builtin/options.mli
index bf1d0244b37b5cb2ea30725cf9c0fa517d6d4bc9..3ff7f8a32bc1d63f0d7f8994e199420e27ba3aa1 100644
--- a/src/plugins/builtin/options.mli
+++ b/src/plugins/builtin/options.mli
@@ -25,7 +25,7 @@ include Plugin.General_services
module Enabled : Parameter_sig.Bool
module Kfs : Parameter_sig.Kernel_function_set
-module NewBuiltin
+module NewBuiltin
(B : sig val function_name: string end) : Parameter_sig.Bool
val emitter: Emitter.t
diff --git a/src/plugins/builtin/tests/functions/memmove.c b/src/plugins/builtin/tests/functions/memmove.c
index d97eda5defe9355cb1c26465802bb516bf00b390..7a17026266d3fe21d3af5411715e868baa97c7c1 100644
--- a/src/plugins/builtin/tests/functions/memmove.c
+++ b/src/plugins/builtin/tests/functions/memmove.c
@@ -7,6 +7,6 @@ int main(void){
int *p = memmove(dest, src, sizeof(src));
}
-int* nested(int (*dest) [10], int (*src) [10], size_t n){
+void nested(int (*dest) [10], int (*src) [10], size_t n) {
memmove(dest, src, n) ;
}
\ No newline at end of file
diff --git a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
index 15722b108753d340b9ec61cfe67acf2a2ffdb761..77e86fe5a03fe77a5a9665dd6784e0bf69e3b447 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcmp.res.oracle
@@ -3,33 +3,6 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
-/*@ requires aligned_end: len % 40 ≡ 0;
- requires
- valid_read_s1:
- \let __fc_len = len / 40; \valid_read(s1 + (0 .. __fc_len - 1));
- requires
- valid_read_s2:
- \let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
- ensures
- equals:
- \let __fc_len = len / 40;
- \result ≡ 0 ⇔
- (∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒
- (∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒ (*(s1 + j0))[j1] ≡ (*(s2 + j0))[j1]));
- assigns \result;
- assigns \result
- \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 __retres;
- __retres = memcmp((void const *)s1,(void const *)s2,len);
- return __retres;
-}
-
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -64,24 +37,6 @@ int main(void)
return __retres;
}
-int nested(int (*dest)[10], int (*src)[10], size_t n)
-{
- int tmp;
- tmp = memcmp_arr10_int(dest,src,n);
- return tmp;
-}
-
-
-[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: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:66 (sum 1974); keeping the one at tests/functions/result/memcmp.c:66.
-/* Generated by Frama-C */
-#include "stddef.h"
-#include "string.h"
-#include "strings.h"
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_read_s1:
@@ -91,13 +46,12 @@ int nested(int (*dest)[10], int (*src)[10], size_t n)
\let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
ensures
equals:
- \let __fc_len = \old(len) / 40;
+ \let __fc_len = len / 40;
\result ≡ 0 ⇔
(∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒
- (*(\old(s1) + j0))[j1] ≡ (*(\old(s2) + j0))[j1]));
+ 0 ≤ j1 < 10 ⇒ (*(s1 + j0))[j1] ≡ (*(s2 + j0))[j1]));
assigns \result;
assigns \result
\from (indirect: (*(s1 + (0 .. len - 1)))[0 .. 10 - 1]),
@@ -110,6 +64,24 @@ int memcmp_arr10_int(int const (*s1)[10], int const (*s2)[10], size_t len)
return __retres;
}
+int nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+ int tmp;
+ tmp = memcmp_arr10_int(dest,src,n);
+ return tmp;
+}
+
+
+[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:29 (sum 4629); keeping the one at tests/functions/result/memcmp.c:29.
+[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:66 (sum 1974); keeping the one at tests/functions/result/memcmp.c:66.
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_read_s1:
@@ -145,6 +117,34 @@ int main(void)
return __retres;
}
+/*@ requires aligned_end: len % 40 ≡ 0;
+ requires
+ valid_read_s1:
+ \let __fc_len = len / 40; \valid_read(s1 + (0 .. __fc_len - 1));
+ requires
+ valid_read_s2:
+ \let __fc_len = len / 40; \valid_read(s2 + (0 .. __fc_len - 1));
+ ensures
+ equals:
+ \let __fc_len = \old(len) / 40;
+ \result ≡ 0 ⇔
+ (∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒
+ (∀ ℤ j1;
+ 0 ≤ j1 < 10 ⇒
+ (*(\old(s1) + j0))[j1] ≡ (*(\old(s2) + j0))[j1]));
+ assigns \result;
+ assigns \result
+ \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 __retres;
+ __retres = memcmp((void const *)s1,(void const *)s2,len);
+ return __retres;
+}
+
int nested(int (*dest)[10], int (*src)[10], size_t n)
{
int tmp;
diff --git a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
index b9fb245dddd9f70ead802df6a15c651fc922753d..7c8012b7448858d598c0bab558ad7559c994f605 100644
--- a/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memcpy.res.oracle
@@ -3,37 +3,6 @@
#include "stddef.h"
#include "string.h"
#include "strings.h"
-/*@ requires aligned_end: len % 40 ≡ 0;
- requires
- valid_dest:
- \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
- requires
- valid_read_src:
- \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
- requires
- separation:
- \let __fc_len = len / 40;
- \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
- ensures
- copied:
- \let __fc_len = len / 40;
- ∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒
- (∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
- ensures result: \result ≡ dest;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
- \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 (*__retres)[10];
- __retres = (int (*)[10])memcpy((void *)dest,(void const *)src,len);
- return __retres;
-}
-
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -70,23 +39,6 @@ int main(void)
return __retres;
}
-void nested(int (*dest)[10], int (*src)[10], size_t n)
-{
- memcpy_arr10_int(dest,src,n);
- return;
-}
-
-
-[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: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:72
-/* Generated by Frama-C */
-#include "stddef.h"
-#include "string.h"
-#include "strings.h"
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
@@ -100,13 +52,12 @@ void nested(int (*dest)[10], int (*src)[10], size_t n)
\separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
ensures
copied:
- \let __fc_len = \old(len) / 40;
+ \let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒
- (*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
- ensures result: \result ≡ \old(dest);
+ 0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
+ ensures result: \result ≡ dest;
assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
\from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
@@ -119,6 +70,23 @@ int (*memcpy_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
return __retres;
}
+void nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+ memcpy_arr10_int(dest,src,n);
+ return;
+}
+
+
+[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:31 (sum 3742); keeping the one at tests/functions/result/memcpy.c:31.
+[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:72
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -156,6 +124,38 @@ int main(void)
return __retres;
}
+/*@ requires aligned_end: len % 40 ≡ 0;
+ requires
+ valid_dest:
+ \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
+ requires
+ valid_read_src:
+ \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
+ requires
+ separation:
+ \let __fc_len = len / 40;
+ \separated(dest + (0 .. __fc_len - 1), src + (0 .. __fc_len - 1));
+ ensures
+ copied:
+ \let __fc_len = \old(len) / 40;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒
+ (∀ ℤ j1;
+ 0 ≤ j1 < 10 ⇒
+ (*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
+ ensures result: \result ≡ \old(dest);
+ assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
+ assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
+ \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 (*__retres)[10];
+ __retres = (int (*)[10])memcpy((void *)dest,(void const *)src,len);
+ return __retres;
+}
+
void nested(int (*dest)[10], int (*src)[10], size_t n)
{
memcpy_arr10_int(dest,(int const (*)[10])src,n);
diff --git a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
index fc95dbda3e23ea98d3165a67ec5d44493d56a740..e6c64844a253de24791d81c903ecf9da780c3fa9 100644
--- a/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
+++ b/src/plugins/builtin/tests/functions/oracle/memmove.res.oracle
@@ -1,37 +1,8 @@
[kernel] Parsing tests/functions/memmove.c (with preprocessing)
-[kernel] tests/functions/memmove.c:11: Warning:
- Body of function nested falls-through. Adding a return statement
/* Generated by Frama-C */
#include "stddef.h"
#include "string.h"
#include "strings.h"
-/*@ requires aligned_end: len % 40 ≡ 0;
- requires
- valid_dest:
- \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
- requires
- valid_read_src:
- \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
- ensures
- moved:
- \let __fc_len = len / 40;
- ∀ ℤ j0;
- 0 ≤ j0 < __fc_len ⇒
- (∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
- ensures result: \result ≡ dest;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
- assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
- \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 (*__retres)[10];
- __retres = (int (*)[10])memmove((void *)dest,(void const *)src,len);
- return __retres;
-}
-
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -64,28 +35,6 @@ int main(void)
return __retres;
}
-int *nested(int (*dest)[10], int (*src)[10], size_t n)
-{
- int *__retres;
- memmove_arr10_int(dest,src,n);
- /*@ assert missing_return: \false; */ ;
- __retres = (int *)0;
- return __retres;
-}
-
-
-[kernel] Parsing tests/functions/result/memmove.c (with preprocessing)
-[kernel] Parsing tests/functions/memmove.c (with preprocessing)
-[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: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:64 (sum 4635); keeping the one at tests/functions/result/memmove.c:64.
-/* Generated by Frama-C */
-#include "stddef.h"
-#include "string.h"
-#include "strings.h"
/*@ requires aligned_end: len % 40 ≡ 0;
requires
valid_dest:
@@ -95,13 +44,12 @@ int *nested(int (*dest)[10], int (*src)[10], size_t n)
\let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
ensures
moved:
- \let __fc_len = \old(len) / 40;
+ \let __fc_len = len / 40;
∀ ℤ j0;
0 ≤ j0 < __fc_len ⇒
(∀ ℤ j1;
- 0 ≤ j1 < 10 ⇒
- (*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
- ensures result: \result ≡ \old(dest);
+ 0 ≤ j1 < 10 ⇒ (*(dest + j0))[j1] ≡ (*(src + j0))[j1]);
+ ensures result: \result ≡ dest;
assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
\from (*(src + (0 .. len - 1)))[0 .. 10 - 1];
@@ -114,6 +62,23 @@ int (*memmove_arr10_int(int (*dest)[10], int const (*src)[10], size_t len))[10]
return __retres;
}
+void nested(int (*dest)[10], int (*src)[10], size_t n)
+{
+ memmove_arr10_int(dest,src,n);
+ return;
+}
+
+
+[kernel] Parsing tests/functions/result/memmove.c (with preprocessing)
+[kernel] Parsing tests/functions/memmove.c (with preprocessing)
+[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:27 (sum 3742); keeping the one at tests/functions/result/memmove.c:27.
+[kernel] tests/functions/memmove.c:10: Warning:
+ dropping duplicate def'n of func nested at tests/functions/memmove.c:10 in favor of that at tests/functions/result/memmove.c:64
+/* Generated by Frama-C */
+#include "stddef.h"
+#include "string.h"
+#include "strings.h"
/*@ requires aligned_end: len % 4 ≡ 0;
requires
valid_dest: \let __fc_len = len / 4; \valid(dest + (0 .. __fc_len - 1));
@@ -147,13 +112,38 @@ int main(void)
return __retres;
}
-int *nested(int (*dest)[10], int (*src)[10], size_t n)
+/*@ requires aligned_end: len % 40 ≡ 0;
+ requires
+ valid_dest:
+ \let __fc_len = len / 40; \valid(dest + (0 .. __fc_len - 1));
+ requires
+ valid_read_src:
+ \let __fc_len = len / 40; \valid_read(src + (0 .. __fc_len - 1));
+ ensures
+ moved:
+ \let __fc_len = \old(len) / 40;
+ ∀ ℤ j0;
+ 0 ≤ j0 < __fc_len ⇒
+ (∀ ℤ j1;
+ 0 ≤ j1 < 10 ⇒
+ (*(\old(dest) + j0))[j1] ≡ (*(\old(src) + j0))[j1]);
+ ensures result: \result ≡ \old(dest);
+ assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1], \result;
+ assigns (*(dest + (0 .. len - 1)))[0 .. 10 - 1]
+ \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 (*__retres)[10];
+ __retres = (int (*)[10])memmove((void *)dest,(void const *)src,len);
+ return __retres;
+}
+
+void nested(int (*dest)[10], int (*src)[10], size_t n)
{
- int *__retres;
memmove_arr10_int(dest,(int const (*)[10])src,n);
- /*@ assert missing_return: \false; */ ;
- __retres = (int *)0;
- return __retres;
+ return;
}
diff --git a/src/plugins/builtin/transform.ml b/src/plugins/builtin/transform.ml
index a14e9360266f1d0be691214b54d4eac01a1e6acc..87f5677b0b395c8a6c1fec053c60999e3717aa85 100644
--- a/src/plugins/builtin/transform.ml
+++ b/src/plugins/builtin/transform.ml
@@ -21,148 +21,97 @@
(**************************************************************************)
open Cil_types
-open Basic_blocks
-
-module type Builtin = sig
- module Hashtbl: Datatype.Hashtbl
- type override_key = Hashtbl.key
-
- val function_name: string
- val well_typed_call: exp list -> bool
- val key_from_call: exp list -> override_key
- val retype_args: 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
+open Builtin_builder
-module type Internal_builtin = sig
- include Builtin
- module Enabled: Parameter_sig.Bool
- val get_override: override_key -> fundec
- val get_globals: location -> global list
- val mark_as_computed: ?project:Project.t -> unit -> unit
-end
+let base : (string, (module Builtin)) Hashtbl.t = Hashtbl.create 17
-module Make_internal_builtin (B: Builtin) = struct
- include B
- module Enabled = Options.NewBuiltin (B)
- module Cache = State_builder.Hashtbl (B.Hashtbl) (Cil_datatype.Fundec)
- (struct
- let size = 5
- let dependencies = [Ast.self]
- let name = "Builtins." ^ B.function_name
- end)
-
- let create_and_add key =
- let (name, typ) = B.generate_prototype key in
- let fd = Basic_blocks.prepare_definition name typ in
- let loc = Cil_datatype.Location.unknown in
- let open Globals.Functions in
- let open Extlib in
- let ret_var = match Cil.getReturnType fd.svar.vtype with
- | t when Cil.isVoidType t -> None
- | t -> Some (Cil.makeLocalVar fd "__retres" t)
- in
- let call =
- let orig = get_vi (find_by_name function_name) in
- let args = B.args_for_original key fd in
- Instr(call_function (opt_map Cil.var ret_var) orig args)
- in
- let ret = Return ( (opt_map Cil.evar ret_var), loc) in
- fd.sbody <-
- { (Cil.mkBlock (List.map Cil.mkStmt [ call ; ret ]))
- with blocals = list_of_opt ret_var } ;
- File.must_recompute_cfg fd ;
- Cache.add key fd
-
- let get_override key =
- try
- Cache.find key
- with Not_found ->
- create_and_add key ;
- Cache.find key
-
- let get_globals location =
- let finalize key fd =
- let spec = B.generate_spec key fd location in
- Globals.Functions.replace_by_definition spec fd location ;
- Cil_types.GFun(fd, location)
- in
- Cache.fold (fun k vi l -> (finalize k vi) :: l) []
-
- let mark_as_computed = Cache.mark_as_computed
-end
-
-let base : (string, (module Internal_builtin)) Hashtbl.t = Hashtbl.create 17
-
-let register (module B: Builtin) =
- let module Internal_builtin = Make_internal_builtin(B) in
- Hashtbl.add base B.function_name (module Internal_builtin)
+let register (module G: Generator_sig) =
+ let module Builtin = Make_builtin(G) in
+ Hashtbl.add base G.function_name (module Builtin)
let mark_as_computed () =
let mark_as_computed _ builtin =
- let module B = (val builtin: Internal_builtin) in B.mark_as_computed ()
+ let module B = (val builtin: Builtin) in B.mark_as_computed ()
in
Hashtbl.iter mark_as_computed base
-let get_globals loc =
- let get_globals _ builtin =
- let module B = (val builtin: Internal_builtin) in B.get_globals loc
+let get_kfs () =
+ let get_kfs _ builtin =
+ let module B = (val builtin: Builtin) in
+ let res = B.get_kfs () in
+ res
in
- Hashtbl.fold (fun k v l -> (get_globals k v) @ l) base []
+ 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
-let replace_call (fct, args) =
- try
- find_stdlib_attr fct ;
- let builtin = Hashtbl.find base fct.vname in
- let module B = (val builtin: Internal_builtin) in
- if B.well_typed_call args then
- let key = B.key_from_call args in
- let fundec = B.get_override key in
- let new_args = B.retype_args key args in
- (fundec.svar), new_args
- else begin
- Options.warning ~current:true "Ignore call: not well typed" ;
- (fct, args)
- end
- with
- | Not_found -> (fct, args)
-
-class visitor = object(_)
+module VISet = Cil_datatype.Varinfo.Hptset
+
+class transformer = object(self)
inherit Visitor.frama_c_inplace
+ val introduced_builtins = ref VISet.empty
+ val used_builtin_last_kf = Queue.create ()
+
method! vfile _ =
- let after f =
- let loc = Cil.CurrentLoc.get() in
- let globals = get_globals loc in
- f.globals <- globals @ f.globals ;
- mark_as_computed () ;
+ let post f =
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
- File.reorder_ast () ;
+ mark_as_computed () ;
f
in
- Cil.DoChildrenPost after
+ Cil.DoChildrenPost post
+
+ method! vglob_aux _ =
+ let post g =
+ let loc = Cil.CurrentLoc.get() in
+ let folding l fd =
+ if VISet.mem fd.svar !introduced_builtins then l
+ else begin
+ introduced_builtins := VISet.add fd.svar !introduced_builtins ;
+ GFun (fd, loc) :: l
+ end
+ in
+ Queue.fold folding g used_builtin_last_kf
+ in
+ Cil.DoChildrenPost post
method! vfunc f =
let kf = Globals.Functions.get f.svar in
- if Options.Kfs.is_empty () || Options.Kfs.mem kf then
+ if not (Options.Kfs.is_set ()) || Options.Kfs.mem kf then
Cil.DoChildren
else
Cil.SkipChildren
+ method private replace_call (fct, args) =
+ try
+ find_stdlib_attr fct ;
+ let builtin = Hashtbl.find base fct.vname in
+ let module B = (val builtin: Builtin) in
+ if B.Enabled.get () then
+ if B.well_typed_call args then
+ let key = B.key_from_call args in
+ let fundec = B.get_override key in
+ let new_args = B.retype_args key args in
+ Queue.add fundec used_builtin_last_kf ;
+ (fundec.svar), new_args
+ else begin
+ Options.warning ~current:true "Ignore call: not well typed" ;
+ (fct, args)
+ end
+ else (fct, args)
+ with
+ | Not_found -> (fct, args)
+
method! vinst = function
| Call(_) | Local_init(_, ConsInit(_, _, Plain_func), _) ->
let change = function
| [ Call(r, ({ enode = Lval((Var f), NoOffset) } as e), args, loc) ] ->
- let f, args = replace_call (f, args) in
+ let f, args = self#replace_call (f, args) in
[ Call(r, { e with enode = Lval((Var f), NoOffset) }, args, loc) ]
| [ Local_init(r, ConsInit(f, args, Plain_func), loc) ] ->
- let f, args = replace_call (f, args) in
+ let f, args = self#replace_call (f, args) in
[ Local_init(r, ConsInit(f, args, Plain_func), loc) ]
| _ -> assert false
in
@@ -170,10 +119,42 @@ class visitor = object(_)
| _ -> Cil.DoChildren
end
-let transform file =
- let filter _ b =
- let module B = (val b : Internal_builtin) in
- if B.Enabled.get () then Some b else None
+let validate_property p =
+ Property_status.emit Options.emitter ~hyps:[] p Property_status.True
+
+let compute_preconditions_statuses kf =
+ let stmt = Kernel_function.find_first_stmt kf in
+ let _ = Kernel_function.find_all_enclosing_blocks stmt in
+ match stmt.skind with
+ | Instr (Call(_, { enode = Lval ((Var fct), NoOffset) }, _, _)) ->
+ let called_kf = Globals.Functions.get fct in
+ Statuses_by_call.setup_all_preconditions_proxies called_kf ;
+ let reqs = Statuses_by_call.all_call_preconditions_at
+ ~warn_missing:true called_kf stmt
+ in
+ List.iter (fun (_, p) -> validate_property p) reqs ;
+ | _ -> assert false
+
+let compute_statuses_all_calls () =
+ let kfs = get_kfs () in
+ List.iter compute_preconditions_statuses kfs ;
+
+ let module Kfs = Kernel_function.Hptset in
+ let open Property in
+ let kfs = List.fold_left (fun s kf -> Kfs.add kf s) Kfs.empty kfs in
+ let validate_if_builtin_post ip =
+ match ip with
+ (* Constracts of generated functions *)
+ | IPPredicate { ip_kf=kf ; ip_kind=PKEnsures _ }
+ | IPAssigns { ias_kf=kf }
+ | IPFrom { if_kf=kf }
+ when Kfs.mem kf kfs ->
+ validate_property ip
+ | _ -> ()
in
- Hashtbl.filter_map_inplace filter base ;
- Visitor.visitFramacFile (new visitor) file
+ Property_status.iter validate_if_builtin_post
+
+
+let transform file =
+ Visitor.visitFramacFile (new transformer) file ;
+ compute_statuses_all_calls ()
diff --git a/src/plugins/builtin/transform.mli b/src/plugins/builtin/transform.mli
index e5876ab7a520906e99bce092e1fbfa0cc1d0e5e6..10e265d87196c9c5bc6d29d81a6c1510c321ebc0 100644
--- a/src/plugins/builtin/transform.mli
+++ b/src/plugins/builtin/transform.mli
@@ -20,21 +20,5 @@
(* *)
(**************************************************************************)
-open Cil_types
-
-module type Builtin = sig
- module Hashtbl: Datatype.Hashtbl
- type override_key = Hashtbl.key
-
- val function_name: string
- val well_typed_call: exp list -> bool
- val key_from_call: exp list -> override_key
- val retype_args: 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
-
-val register: (module Builtin) -> unit
-
+val register: (module Builtin_builder.Generator_sig) -> unit
val transform: Cil_types.file -> unit