From f35a1395c0f8252500f906c3ded7772a08320d58 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 14 Oct 2021 17:03:40 +0200
Subject: [PATCH] [eacsl] Add a user-provided function to replace RTL symbols
---
.../e-acsl/src/code_generator/injector.ml | 14 +++++++++---
src/plugins/e-acsl/src/libraries/functions.ml | 22 +++++++++----------
.../e-acsl/src/libraries/functions.mli | 16 +++++++-------
src/plugins/e-acsl/src/libraries/misc.ml | 2 +-
.../e-acsl/src/project_initializer/rtl.ml | 8 +++----
.../e-acsl/src/project_initializer/rtl.mli | 7 +++---
6 files changed, 39 insertions(+), 30 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index f7c37db6cc4..528ce36f51b 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/libraries/functions.ml b/src/plugins/e-acsl/src/libraries/functions.ml
index 9602cd7e1bf..d44745b0694 100644
--- a/src/plugins/e-acsl/src/libraries/functions.ml
+++ b/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"
diff --git a/src/plugins/e-acsl/src/libraries/functions.mli b/src/plugins/e-acsl/src/libraries/functions.mli
index dbfbffe530e..c2d1453c34e 100644
--- a/src/plugins/e-acsl/src/libraries/functions.mli
+++ b/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 *)
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 17e737b66fe..8602698152a 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.ml b/src/plugins/e-acsl/src/project_initializer/rtl.ml
index 671e517c3f1..092dc9b45e0 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.ml
+++ b/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
diff --git a/src/plugins/e-acsl/src/project_initializer/rtl.mli b/src/plugins/e-acsl/src/project_initializer/rtl.mli
index c864353d59a..684d63b9bbf 100644
--- a/src/plugins/e-acsl/src/project_initializer/rtl.mli
+++ b/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
(*
--
GitLab