[eacsl] Add a user-provided function to replace RTL symbols

src/plugins/e-acsl/src/code_generator/injector.ml

@@ -50,10 +50,14 @@ let replace_literal_strings_in_args env kf_opt (* None for globals *) args =
    RTL. *)
 let rename_caller ~loc caller args =
   if Options.Replace_libc_functions.get ()
-  && Functions.RTL.has_rtl_replacement caller.vorig_name then begin
+  && Functions.Libc.has_replacement caller.vorig_name then begin
     (* rewrite names of functions for which we have alternative definitions in
        the RTL. *)
-    let fvi = Rtl.Symbols.libc_replacement caller in
+    let fvi =
+      Rtl.Symbols.replacement
+        ~get_name:Functions.Libc.replacement_name
+        caller
+    in
     fvi, args
   end
   else if Options.Validate_format_strings.get ()
@@ -62,7 +66,11 @@ let rename_caller ~loc caller args =
        from the above because argument list of format functions is extended with
        an argument describing actual variadic arguments *)
     (* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
-    let fvi = Rtl.Symbols.libc_replacement caller in
+    let fvi =
+      Rtl.Symbols.replacement
+        ~get_name:Functions.Libc.replacement_name
+        caller
+    in
     let fmt =
       Functions.Libc.get_printf_argument_str ~loc caller.vorig_name args
     in

src/plugins/e-acsl/src/libraries/functions.ml

@@ -68,10 +68,6 @@ module RTL = struct
   (* prefix of temporal analysis functions of the public E-ACSL API *)
   let temporal_prefix = api_prefix ^ "temporal_"
 
-  (* prefix of all builtin functions/variables from the public E-ACSL API,
-     Builtin functions replace original calls in programs. *)
-  let e_acsl_builtin_prefix =  api_prefix ^ "builtin_"
-
   (* prefix of functions/variables generated by E-ACSL *)
   let e_acsl_gen_prefix = "__gen_e_acsl_"
 
@@ -95,13 +91,6 @@ module RTL = struct
   let is_generated_literal_string_name name =
     startswith e_acsl_lit_string_prefix name
 
-  let libc_replacement_name fn = e_acsl_builtin_prefix ^ fn
-
-  let has_rtl_replacement = function
-    | "strcpy"  | "strncpy" | "strlen" | "strcat" | "strncat" | "strcmp"
-    | "strncmp" | "memcpy"  | "memset" | "memcmp" | "memmove" -> true
-    | _ -> false
-
 end
 
 (* ************************************************************************** *)
@@ -110,6 +99,17 @@ end
 
 module Libc = struct
 
+  (* prefix of all builtin functions/variables from the public E-ACSL API,
+     Builtin functions replace original calls in programs. *)
+  let e_acsl_builtin_prefix =  RTL.api_prefix ^ "builtin_"
+
+  let has_replacement = function
+    | "strcpy"  | "strncpy" | "strlen" | "strcat" | "strncat" | "strcmp"
+    | "strncmp" | "memcpy"  | "memset" | "memcmp" | "memmove" -> true
+    | _ -> false
+
+  let replacement_name fn = e_acsl_builtin_prefix ^ fn
+
   let is_dyn_alloc_name name =
     name = "malloc" || name = "realloc" || name = "calloc"
 

src/plugins/e-acsl/src/libraries/functions.mli

@@ -73,14 +73,6 @@ module RTL: sig
   (** Retrieve the name of the kernel function and strip prefix that indicates
       that it has been generated by the instrumentation. *)
 
-  val libc_replacement_name: string -> string
-  (** Given the name of C library function return the name of the RTL function
-      that potentially replaces it. *)
-
-  val has_rtl_replacement: string -> bool
-  (** Given the name of C library function return true if there is a drop-in
-      replacement function for it in the RTL. *)
-
 end (* Rtl *)
 
 (* ************************************************************************** *)
@@ -89,6 +81,14 @@ end (* Rtl *)
 
 module Libc: sig
 
+  val has_replacement: string -> bool
+  (** Given the name of C library function return true if there is a drop-in
+      replacement function for it in the RTL. *)
+
+  val replacement_name: string -> string
+  (** Given the name of C library function return the name of the RTL function
+      that potentially replaces it. *)
+
   val is_memcpy: exp -> bool
   (** Return [true] if [exp] captures a function name that matches [memcpy] or
       an equivalent function *)

src/plugins/e-acsl/src/libraries/misc.ml

@@ -36,7 +36,7 @@ let is_fc_or_compiler_builtin vi =
    Datatype.String.equal prefix "__builtin_")
   ||
   (Options.Replace_libc_functions.get ()
-   && Functions.RTL.has_rtl_replacement vi.vname)
+   && Functions.Libc.has_replacement vi.vname)
 
 let is_fc_stdlib_generated vi =
   Cil.hasAttribute "fc_stdlib_generated" vi.vattr

src/plugins/e-acsl/src/project_initializer/rtl.ml

@@ -51,7 +51,7 @@ module Symbols: sig
   val mem_vi: string -> bool
   exception Unregistered of string
   val find_vi: string -> varinfo (* may raise Unregistered *)
-  val libc_replacement: varinfo -> varinfo
+  val replacement: get_name:(string -> string) -> varinfo -> varinfo
   val _debug: unit -> unit
 end = struct
 
@@ -74,13 +74,13 @@ end = struct
     try Datatype.String.Hashtbl.find vars s
     with Not_found -> raise (Unregistered s)
 
-  let libc_replacement fvi =
-    let name = Functions.RTL.libc_replacement_name fvi.vorig_name in
+  let replacement ~get_name fvi =
+    let name = get_name fvi.vorig_name in
     try
       find_vi name
     with Unregistered _ ->
       Options.fatal
-        "Unable to find RTL function '%s' to replace libc function '%s'"
+        "Unable to find RTL function '%s' to replace function '%s'"
         name
         fvi.vname
 

src/plugins/e-acsl/src/project_initializer/rtl.mli

@@ -39,9 +39,10 @@ module Symbols: sig
   val find_vi: string -> varinfo
   (** @raise Unregistered if the given name is not part of the RTL. *)
 
-  val libc_replacement: varinfo -> varinfo
-  (** Given the varinfo of a C library function with an RTL replacement, return
-      the varinfo of the RTL function that replaces it. *)
+  val replacement: get_name:(string -> string) -> varinfo -> varinfo
+  (** Given the varinfo of a C function with an RTL replacement, return
+      the varinfo of the RTL function that replaces it. The function
+      [get_name] is used to find the name of the RTL replacement. *)
 end
 
 (*