[Builtin] Better code generation + validate contracts

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

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

src/plugins/builtin/builtin_builder.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  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

src/plugins/builtin/builtin_builder.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  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

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)
+  end)
\ No newline at end of file

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)
+  end)
\ No newline at end of file

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)
+  end)
\ No newline at end of file

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

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

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;

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);

src/plugins/builtin/tests/functions/oracle/memmove.res.oracle

 [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;
 }
 
 

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 ()

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