Functionality to support rewriting function names in the instrumentation engine

src/plugins/e-acsl/functions.ml

@@ -70,6 +70,8 @@ module RTL: sig
   val is_generated_literal_string_name: string -> bool
   val is_generated_kf: kernel_function -> bool
   val get_original_name: kernel_function -> string
+  val get_rtl_replacement_name: string -> string
+  val has_rtl_replacement: string -> bool
 end = struct
 
   (* prefix of all functions/variables from the public E-ACSL API *)
@@ -78,6 +80,10 @@ end = struct
   (* prefix of temporal analysis functions of the public E-ACSL API *)
   let e_acsl_temporal_prefix = e_acsl_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 =  e_acsl_api_prefix ^ "builtin_"
+
   (* prefix of functions/variables generated by E-ACSL *)
   let e_acsl_gen_prefix = "__gen_e_acsl_"
 
@@ -102,6 +108,13 @@ end = struct
 
   let is_generated_literal_string_name name =
     startswith e_acsl_lit_string_prefix name
+
+  let get_rtl_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
 (* }}} *)
 
@@ -124,6 +137,10 @@ module Libc: sig
   val is_vla_alloc_name: string -> bool
   val is_alloca: exp -> bool
   val is_alloca_name: string -> bool
+  val is_printf: exp -> bool
+  val is_printf_name: string -> bool
+  val printf_fmt_position: string -> int
+  val get_printf_argument_str: loc:location -> string -> exp list -> exp
   val actual_alloca: string
 end = struct
   let is_dyn_alloc_name name =
@@ -156,5 +173,72 @@ end = struct
   let is_memcpy exp = is_fn is_memcpy_name exp
 
   let is_memset exp = is_fn is_memset_name exp
+
+  let printf_fmt_position = function
+    | "printf" -> 1
+    | "syslog" | "dprintf" | "fprintf" | "sprintf" -> 2
+    | "snprintf" -> 3
+    | _ -> 0
+
+  let is_printf_name name = printf_fmt_position name <> 0
+
+  let is_printf exp = is_fn is_printf_name exp
+
+  let get_printf_argument_str ~loc fn args =
+    assert (is_printf_name fn);
+    (* drop first n elements from a list *)
+    let rec drop n l =
+      assert (n >= 0);
+      if n > 0 then drop (n-1) (match l with _::e -> e | [] -> [])
+      else l
+    in
+    (* get a character representing an integer type *)
+    let get_ikind_str = function
+      | IInt -> "d" (* [int] *)
+      | IUInt -> "D" (* [unsigned int] *)
+      | ILong -> "l" (* [long] *)
+      | IULong -> "L" (* [unsigned long] *)
+      | ILongLong -> "r" (* [long long] *)
+      | IULongLong -> "R" (* [unsigned long long] *)
+      (* _Bool, char and short (either signed or unsigned are promoted to int) *)
+      | IBool | IChar | ISChar | IUChar | IShort | IUShort -> "d"
+    in
+    (* get a character representing an floating point type *)
+    let get_fkind_str = function
+      (* Format-based functions expect only double-precision floats.
+         Single-precision floating points are promoted to doubles so
+         this case should never happen in fact. *)
+      | FFloat -> "f" (* [float] *)
+      | FDouble  -> "e" (* [float/double] *)
+      | FLongDouble -> "E" (* [long double] *)
+    in
+    (* get a character representing a pointer type *)
+    let get_pkind_str ty = match ty with
+      | TInt(IChar,_) | TInt(ISChar,_) -> "s" (* [char*] *)
+      | TInt(IUChar,_) -> "S" (* [unsigned char*] *)
+      | TInt(IShort,_) -> "q" (* [short*] *)
+      | TInt(IUShort,_) -> "Q" (* [unsigned short*] *)
+      | TInt(IInt,_) -> "i" (* [int*] *)
+      | TInt(IUInt,_) -> "I" (* [unsigned int*] *)
+      | TInt(ILong,_) -> "z" (* [long int*] *)
+      | TInt(IULong,_) -> "Z" (* [unsigned long int*] *)
+      | TInt(ILongLong,_) -> "w" (* [long int*] *)
+      | TInt(IULongLong,_) -> "W" (* [unsigned long int*] *)
+      | TVoid _ -> "p" (* [void*] *)
+      | _ -> Options.fatal "Unexpected argument type in printf: %a @."
+        Printer.pp_typ ty
+    in
+    let exps = drop (printf_fmt_position fn) args in
+    let param_str = List.fold_left
+      (fun acc exp ->
+        match Cil.unrollTypeDeep (Cil.typeOf exp) with
+        | TInt(k,_) -> acc ^ get_ikind_str k
+        | TFloat(k,_) -> acc ^ get_fkind_str k
+        | TPtr(ty,_) -> acc ^ get_pkind_str ty
+        | TVoid _ | TArray _ | TFun _ | TNamed _ | TComp _ | TEnum _
+        | TBuiltin_va_list _ -> assert false)
+      ""
+      exps
+    in Cil.mkString ~loc param_str
 end
 (* }}} *)

src/plugins/e-acsl/functions.mli

@@ -67,6 +67,14 @@ module RTL: sig
   val get_original_name: kernel_function -> string
   (** Retrieve the name of the kernel function and strip prefix that indicates
       that it has been generated by the instrumentation. *)
+
+  val get_rtl_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
 
 (* ************************************************************************** *)
@@ -124,6 +132,42 @@ module Libc: sig
   val is_alloca_name: string -> bool
   (** Same as [is_alloca] but for strings *)
 
+  val is_printf: exp -> bool
+  (** Return [true] if [exp] captures a function name that matches
+      a printf-like function such as [printf], [fprintf], [dprintf] etc. *)
+
+  val is_printf_name: string -> bool
+  (** Same as [is_printf] but for strings *)
+
+  val printf_fmt_position: string -> int
+  (** Given the name of a printf-like function (as determined by
+     [is_printf_name]) return the number of arguments preceding its variadic
+     arguments. *)
+
+  val get_printf_argument_str: loc:location -> string -> exp list -> exp
+  (** Given the name of a printf-like function ([string]) and the list
+      of its variadic arguments [exp list] return a literal string expression
+      where each character describes the type of an argument from a list.
+      Such characters are also called abbreviated types. Conversion between
+      abbreviated and C types characters is as follows:
+         -  "b" -> [_Bool]
+         -  "c" -> [signed char]
+         -  "C" -> [unsigned char]
+         -  "d" -> [int]
+         -  "D" -> [unsigned int]
+         -  "h" -> [short]
+         -  "H" -> [unsigned short]
+         -  "l" -> [long]
+         -  "L" -> [unsigned long]
+         -  "r" -> [long long]
+         -  "R" -> [unsigned long long]
+         -  "f" -> [float]
+         -  "e" -> [double]
+         -  "E" -> [long double]
+         -  "s" -> [char*]
+         -  "i" -> [int*]
+         -  "p" -> [void*] *)
+
   val actual_alloca: string
   (** The name of an actual [alloca] function used at link-time.
       In GCC/Clang [alloca] is typically implemented via [__builtin_alloca] *)