Commit 0b2b2f42 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov Committed by Julien Signoles
Browse files

Functionality to rewrite function names (format and libc replacements)

parent 9e6a5430
......@@ -51,16 +51,17 @@ let reset () = Datatype.String.Hashtbl.clear library_functions
(* ************************************************************************** *)
exception Unregistered_library_function of string
let mk_call ~loc ?result fname args =
let vi =
try Datatype.String.Hashtbl.find library_functions fname
let get_lib_fun_vi fname =
try Datatype.String.Hashtbl.find library_functions fname
with Not_found ->
try Builtins.find fname
with Not_found ->
(* could not happen in normal mode, but coud be raised when E-ACSL is
used as a library *)
raise (Unregistered_library_function fname)
in
let mk_call ~loc ?result fname args =
let vi = get_lib_fun_vi fname in
let f = Cil.evar ~loc vi in
vi.vreferenced <- true;
let make_args args ty_params =
......
......@@ -30,6 +30,9 @@ open Cil_datatype
(* ************************************************************************** *)
exception Unregistered_library_function of string
val get_lib_fun_vi: string -> varinfo
(** Return varinfo corresponding to a name of a given library function *)
val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
(** Call an E-ACSL library function or an E-ACSL built-in.
@raise Unregistered_library_function if the given string does not represent
......
......@@ -109,9 +109,11 @@ static void describe_run();
# error "No E-ACSL memory model defined. Aborting compilation"
#endif
/* This header contains temporal analysis shared by both models.
It should be here as it uses differently defined macros */
#include "e_acsl_temporal.h"
/* Headers containing implementation of functions belonging to the E-ACSL
external API shared across different memory models */
#include "e_acsl_libc_replacements.h" /* */
#include "e_acsl_format.h" /* format functions with error checking */
#include "e_acsl_temporal.h" /* temporal analysis */
#ifdef E_ACSL_WEAK_VALIDITY
# define E_ACSL_VALIDITY_DESC "weak"
......@@ -121,7 +123,7 @@ static void describe_run();
/* Print basic configuration before each run */
static void describe_run() {
#if defined(E_ACSL_VERBOSE) || defined(E_ACSL_DEBUG)
#if defined(E_ACSL_VERBOSE)
rtl_printf("/* ========================================================= */\n");
rtl_printf(" * E-ACSL instrumented run\n" );
rtl_printf(" * Memory tracking: %s\n", E_ACSL_MMODEL_DESC);
......@@ -133,6 +135,7 @@ static void describe_run() {
rtl_printf(" * Execution mode: %s\n", E_ACSL_DEBUG_DESC);
rtl_printf(" * Assertions mode: %s\n", E_ACSL_ASSERT_NO_FAIL_DESC);
rtl_printf(" * Validity notion: %s\n", E_ACSL_VALIDITY_DESC);
rtl_printf(" * Format Checks: %s\n", E_ACSL_FORMAT_VALIDITY_DESC);
rtl_printf("/* ========================================================= */\n");
#endif
}
......@@ -745,6 +745,8 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
else
env
in
let check_formats = Options.Validate_format_strings.get () in
let replace_libc_fn = Options.Replace_libc_functions.get () in
match stmt.skind with
| Instr(Set(lv, _, loc)) -> add_initializer loc lv stmt env kf
| Instr(Local_init(vi, init, loc)) ->
......@@ -754,30 +756,64 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
Here each instance of [__fc_vla_alloc] is rewritten to [alloca]
(that is used to implement VLA) and further a custom call to
[store_block] tracking VLA allocation is issued. *)
(* KV NOTE: Do not add handling [alloca] allocation here (or anywhere
else for that matter). Handling of [alloca] should be implemented
in Frama-C (eventually). This is such that each call to [alloca]
becomes [__fc_vla_alloc]. It is already handled using the code below.
*)
(* KV: Do not add handling [alloca] allocation here (or anywhere else for
that matter). Handling of [alloca] should be implemented in Frama-C
(eventually). This is such that each call to [alloca] becomes
[__fc_vla_alloc]. It is already handled using the code below. *)
(match init with
| ConsInit (fvi, sz :: _, _) when Libc.is_vla_alloc_name fvi.vname ->
fvi.vname <- Libc.actual_alloca;
(* since we need to pass vi by value cannot use [Misc.mk_store_stmt]
(* Since we need to pass [vi] by value cannot use [Misc.mk_store_stmt]
here. Do it manually. *)
let sname = RTL.mk_api_name "store_block" in
let store = Misc.mk_call ~loc sname [ Cil.evar vi ; sz ] in
Env.add_stmt ~post:true env store
(* Rewrite format functions (e.g., [printf]). See some comments below *)
| ConsInit (fvi, args, knd) when check_formats
&& Libc.is_printf_name fvi.vname ->
let name = RTL.get_rtl_replacement_name fvi.vname in
let new_vi = Misc.get_lib_fun_vi name in
let fmt = Libc.get_printf_argument_str ~loc fvi.vname args in
stmt.skind <-
Instr(Local_init(vi, ConsInit(new_vi, fmt :: args, knd), loc));
env
(* Rewrite names of functions for which we have alternative
definitions in the RTL. *)
| ConsInit (fvi, _, _) when replace_libc_fn &&
RTL.has_rtl_replacement fvi.vname ->
fvi.vname <- RTL.get_rtl_replacement_name fvi.vname;
env
| _ -> env)
| Instr(Call (Some lv, _, _, loc)) ->
if not (RTL.is_generated_kf kf) then
add_initializer loc lv ~post:false stmt env kf
else env
(* Handle variable-length array allocation via [__fc_vla_free].
Rewrite its name to [delete_block]. The rest is in place. *)
| Instr(Call (_, { enode = Lval(Var(vi), _) }, _, _))
when Libc.is_vla_free_name vi.vname ->
vi.vname <- RTL.mk_api_name "delete_block";
env
| Instr(Call (result, exp, args, loc)) ->
(match exp.enode with
(* Rewrite names of functions for which we have alternative
definitions in the RTL. *)
| Lval(Var(vi), _) when replace_libc_fn &&
RTL.has_rtl_replacement vi.vname ->
vi.vname <- RTL.get_rtl_replacement_name vi.vname
(* Handle variable-length array allocation via [__fc_vla_free].
Rewrite its name to [delete_block]. The rest is in place. *)
| Lval(Var(vi), _) when Libc.is_vla_free_name vi.vname ->
vi.vname <- RTL.mk_api_name "delete_block"
(* Rewrite names of format functions (such as printf). This case differs
from the above because argument list of format functions is extended
with an argument describing actual variadic arguments *)
| Lval(Var(vi), _) when check_formats && Libc.is_printf_name vi.vname ->
(* Replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
let name = RTL.get_rtl_replacement_name vi.vname in
(* Variadic arguments descriptor *)
let fmt = Libc.get_printf_argument_str ~loc vi.vname args in
(* get the name of the library function we need. Cannot just rewrite
the name as AST check will then fail *)
let vi = Misc.get_lib_fun_vi name in
stmt.skind <- Instr(Call (result, Cil.evar vi, fmt :: args, loc))
| _ -> ());
(* Add statement tracking initialization of return values of function
calls *)
(match result with
| Some lv when not (RTL.is_generated_kf kf) ->
add_initializer loc lv ~post:false stmt env kf
| _ -> env)
| _ -> env
method !vblock blk =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment