[Builtin] Simplifies addition of a builtin function

headers/header_spec.txt

@@ -932,8 +932,6 @@ src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
 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_cache.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/builtin/builtin_cache.mli: CEA_LGPL_OR_PROPRIETARY
 src/plugins/builtin/Builtin.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/Makefile.in

@@ -37,7 +37,7 @@ PLUGIN_DIR ?= .
 PLUGIN_ENABLE := @ENABLE_BUILTIN@
 PLUGIN_NAME := Builtin
 PLUGIN_CMI := 
-PLUGIN_CMO := options transform builtin_cache basic_blocks memcpy memcmp memmove register
+PLUGIN_CMO := options transform basic_blocks memcpy memcmp memmove register
 PLUGIN_DISTRIBUTED := $(PLUGIN_ENABLE)
 PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
 #PLUGIN_NO_DEFAULT_TEST := no

src/plugins/builtin/builtin_cache.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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type Table = sig
-  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_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.Fundec)
-     (struct
-       let size = 5
-       let dependencies = [Ast.self]
-       let name = "Builtins." ^ M.function_name
-     end))
-
-module Make (Generator: Generator) = struct
-  module Internal_table = Make_internal_table(Generator)
-  open Cil_types
-
-  let get_varinfo t = try
-      (Internal_table.find t).svar
-    with Not_found ->
-      let fct = Generator.build_function t in
-      Internal_table.add t fct ;
-      fct.svar
-
-  let get_globals 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) []
-
-  let mark_as_computed = Internal_table.mark_as_computed
-end

src/plugins/builtin/builtin_cache.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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-module type Generator = sig
-  val function_name: String.t
-  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_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 Make (M: Generator) : Table

src/plugins/builtin/memcmp.ml

@@ -57,7 +57,7 @@ let generate_ensures loc s1 s2 len =
     { (presult_memcmp_len_bytes ~loc s1 s2 len) with pred_name = [ "equals" ] }
   ]
 
-let generate_spec vi loc =
+let generate_spec _t { svar = vi } loc =
   let (c_s1, c_s2, clen) = match Cil.getFormalsDecl vi with
     | [ s1 ; s2 ; len ] -> s1, s2, len
     | _ -> assert false
@@ -96,39 +96,41 @@ let generate_function t =
   set_function_body fd (generate_body fd) ;
   fd
 
-module Table = Builtin_cache.Make(struct
-    let function_name = function_name
-    let build_function = generate_function
-    let build_spec = generate_spec
-  end)
-
-let type_from_parameter x =
+let type_from_arg 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 replace_call = function
-  | (_fct, [ s1 ; s2 ; len ]) ->
+let well_typed_call = function
+  | [ s1 ; s2 ; len ] ->
+    (Cil.isIntegralType (Cil.typeOf len)) &&
+    (Cil_datatype.Typ.equal (type_from_arg s1) (type_from_arg s2))
+  | _ -> false
+
+let key_from_call = function
+  | [ s1 ; _ ; _ ] -> type_from_arg s1
+  | _ -> failwith "Call to Memmove.key_from_call on an ill-typed builtin call"
+
+let retype_args override_key = function
+  | [ s1 ; s2 ; len ] ->
     let s1 = Cil.stripCasts s1 in
     let s2 = Cil.stripCasts s2 in
-    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))
+    assert (
+      Cil_datatype.Typ.equal (type_from_arg s1) override_key &&
+      Cil_datatype.Typ.equal (type_from_arg s2) override_key
+    ) ;
+    [ s1 ; s2 ; len ]
+  | _ -> failwith "Call to Memmove.retype_args on an ill-typed builtin call"
 
 let () = Transform.register (module struct
+    module Hashtbl = Cil_datatype.Typ.Hashtbl
+    type override_key = typ
+
     let function_name = function_name
-    let replace_call  = replace_call
-    let get_globals   = Table.get_globals
-    let mark_as_computed = Table.mark_as_computed
-  end)
+    let well_typed_call = well_typed_call
+    let key_from_call = key_from_call
+    let retype_args = retype_args
+    let generate_function = generate_function
+    let generate_spec = generate_spec
+  end)
\ No newline at end of file

src/plugins/builtin/memcpy.ml

@@ -59,7 +59,7 @@ let generate_ensures loc t dest src len =
     { (presult_dest ~loc t dest)            with pred_name = [ "result"] }
   ]
 
-let generate_spec vi loc =
+let generate_spec _t { svar = vi } loc =
   let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
     | [ dest ; src ; len ] -> dest, src, len
     | _ -> assert false
@@ -100,39 +100,41 @@ let generate_function t =
   set_function_body fd (generate_body t fd) ;
   fd
 
-module Table = Builtin_cache.Make(struct
-    let function_name = function_name
-    let build_function = generate_function
-    let build_spec = generate_spec
-  end)
-
-let type_from_parameter x =
+let type_from_arg 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 replace_call = function
-  | (_fct, [ dest ; src ; len ]) ->
+let well_typed_call = function
+  | [ dest ; src ; len ] ->
+    (Cil.isIntegralType (Cil.typeOf len)) &&
+    (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src))
+  | _ -> false
+
+let key_from_call = function
+  | [ dest ; _ ; _ ] -> type_from_arg dest
+  | _ -> failwith "Call to Memcpy.key_from_call on an ill-typed builtin call"
+
+let retype_args override_key = function
+  | [ dest ; src ; len ] ->
     let dest = Cil.stripCasts dest in
     let src = Cil.stripCasts src in
-    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))
+    assert (
+      Cil_datatype.Typ.equal (type_from_arg dest) override_key &&
+      Cil_datatype.Typ.equal (type_from_arg src) override_key
+    ) ;
+    [ dest ; src ; len ]
+  | _ -> failwith "Call to Memcpy.retype_args on an ill-typed builtin call"
 
 let () = Transform.register (module struct
+    module Hashtbl = Cil_datatype.Typ.Hashtbl
+    type override_key = typ
+
     let function_name = function_name
-    let replace_call  = replace_call
-    let get_globals   = Table.get_globals
-    let mark_as_computed = Table.mark_as_computed
-  end)
+    let well_typed_call = well_typed_call
+    let key_from_call = key_from_call
+    let retype_args = retype_args
+    let generate_function = generate_function
+    let generate_spec = generate_spec
+  end)
\ No newline at end of file

src/plugins/builtin/memmove.ml

@@ -54,7 +54,7 @@ let generate_ensures loc t dest src len =
     { (presult_dest ~loc t dest)           with pred_name = [ "result"] }
   ]
 
-let generate_spec vi loc =
+let generate_spec _t { svar = vi } loc =
   let (cdest, csrc, clen) = match Cil.getFormalsDecl vi with
     | [ dest ; src ; len ] -> dest, src, len
     | _ -> assert false
@@ -95,40 +95,41 @@ let generate_function t =
   set_function_body fd (generate_body t fd) ;
   fd
 
-module Table = Builtin_cache.Make(struct
-    let function_name = function_name
-    let build_function = generate_function
-    let build_spec = generate_spec
-  end)
-
-let type_from_parameter x =
+let type_from_arg 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 replace_call = function
-  | (_fct, [ dest ; src ; len ]) ->
+let well_typed_call = function
+  | [ dest ; src ; len ] ->
+    (Cil.isIntegralType (Cil.typeOf len)) &&
+    (Cil_datatype.Typ.equal (type_from_arg dest) (type_from_arg src))
+  | _ -> false
+
+let key_from_call = function
+  | [ dest ; _ ; _ ] -> type_from_arg dest
+  | _ -> failwith "Call to Memmove.key_from_call on an ill-typed builtin call"
+
+let retype_args override_key = function
+  | [ dest ; src ; len ] ->
     let dest = Cil.stripCasts dest in
     let src = Cil.stripCasts src in
-    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))
+    assert (
+      Cil_datatype.Typ.equal (type_from_arg dest) override_key &&
+      Cil_datatype.Typ.equal (type_from_arg src) override_key
+    ) ;
+    [ dest ; src ; len ]
+  | _ -> failwith "Call to Memmove.retype_args on an ill-typed builtin call"
 
 let () = Transform.register (module struct
+    module Hashtbl = Cil_datatype.Typ.Hashtbl
+    type override_key = typ
+
     let function_name = function_name
-    let replace_call  = replace_call
-    let get_globals   = Table.get_globals
-    let mark_as_computed = Table.mark_as_computed
-  end)
+    let well_typed_call = well_typed_call
+    let key_from_call = key_from_call
+    let retype_args = retype_args
+    let generate_function = generate_function
+    let generate_spec = generate_spec
+  end)
\ No newline at end of file

src/plugins/builtin/options.ml

@@ -26,14 +26,28 @@ let shortname = "builtin"
 include Plugin.Register
     (struct
       let name = name
-      let shortname = shortname
+      let shortname = "-" ^ shortname
       let help = "Overrides standard library functions"
     end)
 
 module Enabled = False
     (struct
-      let option_name = "-builtin"
+      let option_name = "-" ^ shortname
       let help = ""
     end)
 
+module Kfs =
+  Kernel_function_set
+    (struct
+      let option_name = "-" ^ shortname ^ "-fct"
+      let arg_name = "f,..."
+      let help = "Override stdlib functions only into the specified functions (defaults to all)."
+    end)
+
+module NewBuiltin (B: sig val function_name: string end) = True
+    (struct
+      let option_name = "-" ^ shortname ^ "-" ^ B.function_name
+      let help = "Activate replacement for function '" ^ B.function_name ^ "'"
+    end)
+
 let emitter = Emitter.create shortname [Emitter.Funspec] ~correctness:[] ~tuning:[]

src/plugins/builtin/options.mli

@@ -23,5 +23,9 @@
 include Plugin.General_services
 
 module Enabled : Parameter_sig.Bool
+module Kfs : Parameter_sig.Kernel_function_set
+
+module NewBuiltin 
+    (B : sig val function_name: string end) : Parameter_sig.Bool
 
 val emitter: Emitter.t

src/plugins/builtin/transform.ml

@@ -22,30 +22,72 @@
 
 open Cil_types
 
-exception Bad_typing of string
-
 module type Builtin = sig
+  module Hashtbl: Datatype.Hashtbl
+  type override_key = Hashtbl.key
+
   val function_name: string
-  val replace_call: (varinfo * exp list) -> (varinfo * exp list)
+  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_function: override_key -> fundec
+  val generate_spec: override_key -> fundec -> location -> funspec
+end
+
+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
+  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 register ((module M: Builtin) as m) =
-  Hashtbl.add base M.function_name m
+  let get_override key =
+    try
+      Cache.find key
+    with Not_found ->
+      let fct = B.generate_function key in
+      Cache.add key fct ;
+      fct
+
+  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 mark_as_computed () =
-  let mark _ m = let module M = (val m: Builtin) in M.mark_as_computed () in
-  Hashtbl.iter mark base
+  let mark_as_computed _ builtin =
+    let module B = (val builtin: Internal_builtin) in B.mark_as_computed ()
+  in
+  Hashtbl.iter mark_as_computed base
 
 let get_globals loc =
-  let get_globals m =
-    let module M = (val m: Builtin) in
-    M.get_globals loc
+  let get_globals _ builtin =
+    let module B = (val builtin: Internal_builtin) in B.get_globals loc
   in
-  Hashtbl.fold (fun _ v l -> (get_globals v) @ l) base []
+  Hashtbl.fold (fun k v l -> (get_globals k v) @ l) base []
 
 let find_stdlib_attr fct =
   if not (Cil.hasAttribute "fc_stdlib" fct.vattr) then raise Not_found
@@ -53,14 +95,19 @@ let find_stdlib_attr fct =
 let replace_call (fct, args) =
   try
     find_stdlib_attr fct ;
-    let m = Hashtbl.find base fct.vname in
-    let module M = (val m: Builtin) in
-    M.replace_call (fct, args)
+    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)
-  | Bad_typing s ->
-    Options.warning ~current:true "Ignored: %s" s ;
-    (fct, args)
 
 class visitor = object(_)
   inherit Visitor.frama_c_inplace
@@ -78,6 +125,13 @@ class visitor = object(_)
     in
     Cil.DoChildrenPost after
 
+  method! vfunc f =
+    let kf = Globals.Functions.get f.svar in
+    if Options.Kfs.is_empty () || Options.Kfs.mem kf then
+      Cil.DoChildren
+    else
+      Cil.SkipChildren
+
   method! vinst = function
     | Call(_) | Local_init(_, ConsInit(_, _, Plain_func), _) ->
       let change = function
@@ -94,4 +148,9 @@ class visitor = object(_)
 end
 
 let transform file =
+  let filter _ b =
+    let module B = (val b : Internal_builtin) in
+    if B.Enabled.get () then Some b else None
+  in
+  Hashtbl.filter_map_inplace filter base ;
   Visitor.visitFramacFile (new visitor) file

src/plugins/builtin/transform.mli

@@ -22,14 +22,18 @@
 
 open Cil_types
 
-exception Bad_typing of string
-
 module type Builtin = sig
+  module Hashtbl: Datatype.Hashtbl
+  type override_key = Hashtbl.key
+
   val function_name: string
-  val replace_call: (varinfo * exp list) -> (varinfo * exp list)
-  val get_globals: location -> global list
-  val mark_as_computed: ?project:Project.t -> unit -> unit
+  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_function: override_key -> fundec
+  val generate_spec: override_key -> fundec -> location -> funspec
 end
+
 val register: (module Builtin) -> unit
 
 val transform: Cil_types.file -> unit