Commit 5eefe617 authored by Basile Desloges 's avatar Basile Desloges
Browse files

Merge branch 'feature/basile/libc-memfunc-support' into 'master'

[eacsl] Update memory model when calling libc functions

Closes e-acsl#40 and e-acsl#157

See merge request frama-c/frama-c!3225
parents 14d393c9 f6087ae8
......@@ -4998,6 +4998,8 @@ let cvar_to_lvar vi = match vi.vlogic_var_assoc with
vi.vlogic_var_assoc <- Some lv; lv
| Some lv -> lv
let cvar_to_term ~loc vi = tvar ~loc (cvar_to_lvar vi)
let copyVarinfo (vi: varinfo) (newname: string) : varinfo =
let vi' = Cil_const.copy_with_new_vid vi in
vi'.vname <- newname;
......
......@@ -2281,6 +2281,10 @@ val stmt_of_instr_list : ?loc:location -> instr list -> stmtkind
The returned logic variable is unique for a given C variable. *)
val cvar_to_lvar : varinfo -> logic_var
(** Convert a C variable into a logic term.
@since Frama-C+dev *)
val cvar_to_term: loc:location -> varinfo -> term
(** Make a temporary variable to use in annotations *)
val make_temp_logic_var: logic_type -> logic_var
......
......@@ -93,6 +93,7 @@ SRC_CODE_GENERATOR:= \
memory_observer \
literal_observer \
global_observer \
libc \
injector
SRC_CODE_GENERATOR:=$(addprefix src/code_generator/, $(SRC_CODE_GENERATOR))
......@@ -178,7 +179,8 @@ PLUGIN_TESTS_DIRS := \
format \
temporal \
special \
builtin
builtin \
libc
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
......
......@@ -25,9 +25,11 @@
Plugin E-ACSL <next-release>
############################
- E-ACSL [2021-08-03] Correct monitoring of code depending on libc
function calls that write memory locations (frama-c/e-acsl#157).
-* E-ACSL [2021-07-30] Fix incorrect evaluation of quantified
predicates when a strict guard overlaps with the type of the
bound variable (unlikely in practice) (frama-c/e-acsl#149).
predicates when a strict guard overlaps with the type of the
bound variable (unlikely in practice) (frama-c/e-acsl#149).
- E-ACSL [2021-07-06] Add support for the extended quantifier \sum.
-* E-ACSL [2021-06-22] Fix a crash that occured when using certain
combinations of nested blocks and annotations.
......
......@@ -98,6 +98,8 @@ src/code_generator/injector.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/injector.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/label.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/label.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/libc.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/libc.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/literal_observer.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/code_generator/logic_array.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
......
......@@ -37,7 +37,7 @@
becomes unsound.
TODO: may only happen for annotations containing memory-related properties.
For arithmetic properties, the verdict is always sound (?). */
extern int eacsl_runtime_sound_verdict;
extern int __attribute__((FC_BUILTIN)) eacsl_runtime_sound_verdict;
/*! \brief Runtime assertion verifying a given predicate
* \param pred integer code of a predicate
......
......@@ -31,6 +31,7 @@
#include "../internals/e_acsl_private_assert.h"
#include "../internals/e_acsl_rtl_io.h"
#include "../internals/e_acsl_rtl_string.h"
#include "../observation_model/e_acsl_observation_model.h"
#include "e_acsl_string.h"
#include "e_acsl_stdio.h"
......@@ -942,7 +943,11 @@ int eacsl_builtin_sprintf(const char *fmtdesc, char *buffer, const char *fmt, ..
va_start(ap, fmt);
validate_format(fmtdesc, fmt, ap, "sprintf", buffer, len + 1);
va_start(ap, fmt);
return vsprintf(buffer, fmt, ap);
int res = vsprintf(buffer, fmt, ap);
if (res >= 0) {
eacsl_initialize(buffer, res + 1);
}
return res;
}
int eacsl_builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
......@@ -956,7 +961,11 @@ int eacsl_builtin_snprintf(const char *fmtdesc, char *buffer, size_t size,
private_abort("sprintf: output buffer is unallocated or has insufficient length "
"to store %d characters and \\0 terminator or not writeable\n", size);
va_start(ap, fmt);
return vsnprintf(buffer, size, fmt, ap);
int res = vsnprintf(buffer, size, fmt, ap);
if (res >= 0 && size > 0) {
eacsl_initialize(buffer, size <= res ? size : res + 1);
}
return res;
}
int eacsl_builtin_syslog(const char *fmtdesc, int priority, const char *fmt, ...) {
......
......@@ -160,7 +160,9 @@ char *eacsl_builtin_strcpy(char *dest, const char *src) {
/* source and destination strings should not overlap */
validate_overlapping_spaces
((uintptr_t)dest, size + 1, (uintptr_t)src, size + 1, "strcpy");
return strcpy(dest, src);
char * res = strcpy(dest, src);
eacsl_initialize(dest, size + 1);
return res;
}
char *eacsl_builtin_strncpy(char *dest, const char *src, size_t n) {
......@@ -170,7 +172,9 @@ char *eacsl_builtin_strncpy(char *dest, const char *src, size_t n) {
validate_writeable_space(dest, n, "strncpy", "destination string ");
/* source and destination strings should not overlap */
validate_overlapping_spaces((uintptr_t)dest, n, (uintptr_t)src, n, "strncpy");
return strncpy(dest, src, n);
char * res = strncpy(dest, src, n);
eacsl_initialize(dest, n);
return res;
}
int eacsl_builtin_strcmp(const char *s1, const char *s2) {
......@@ -200,11 +204,14 @@ char *eacsl_builtin_strcat(char *dest, const char *src) {
}
validate_overlapping_spaces
((uintptr_t)src, src_sz + 1, (uintptr_t)dest, dest_sz + 1, "strcat");
return strcat(dest, src);
char * res = strcat(dest, src);
eacsl_initialize(&dest[dest_sz], src_sz + 1);
return res;
}
char *eacsl_builtin_strncat(char *dest, const char *src, size_t n) {
validate_allocated_string((char*)src, n, "strncat", "source string ");
long src_sz =
validate_allocated_string((char*)src, n, "strncat", "source string ");
long dest_sz =
validate_writeable_string((char*)dest, -1, "strcat", "destination string ");
size_t avail_sz = eacsl_block_length(dest) - eacsl_offset(dest);
......@@ -215,7 +222,9 @@ char *eacsl_builtin_strncat(char *dest, const char *src, size_t n) {
}
validate_overlapping_spaces
((uintptr_t)src, n, (uintptr_t)dest, dest_sz, "strcat");
return strncat(dest, src, n);
char * res = strncat(dest, src, n);
eacsl_initialize(&dest[dest_sz], src_sz + 1);
return res;
}
/* }}} */
......@@ -227,12 +236,16 @@ void *eacsl_builtin_memcpy(void *dest, const void *src, size_t n) {
validate_allocated_space((void*)src, n, "memcpy", "source space ");
validate_writeable_space((void*)dest, n, "memcpy", "destination space ");
validate_overlapping_spaces((uintptr_t)src, n, (uintptr_t)dest, n, "memcpy");
return memcpy(dest, src, n);
void * res = memcpy(dest, src, n);
eacsl_initialize(dest, n);
return res;
}
void *eacsl_builtin_memset(void *s, int c, size_t n) {
validate_writeable_space((void*)s, n, "memset", "space ");
return memset(s, c, n);
void * res = memset(s, c, n);
eacsl_initialize(s, n);
return res;
}
int eacsl_builtin_memcmp(const void *s1, const void *s2, size_t n) {
......@@ -245,7 +258,9 @@ int eacsl_builtin_memcmp(const void *s1, const void *s2, size_t n) {
void *eacsl_builtin_memmove(void *dest, const void *src, size_t n) {
validate_allocated_space((void*)src, n, "memcmp", "source space ");
validate_writeable_space((void*)dest, n, "memcmp", "destination space ");
return memmove(dest, src, n);
void * res = memmove(dest, src, n);
eacsl_initialize(dest, n);
return res;
}
/* }}} */
......
......@@ -93,7 +93,8 @@ val add_stmt: ?post:bool -> ?before:stmt -> t -> kernel_function -> stmt -> t
(** [add_stmt env s] extends [env] with the new statement [s].
[before] may define which stmt the new one is included before. This is to
say that any labels attached to [before] are moved to [stmt]. [post]
indicates that [stmt] should be added after the target statement. *)
indicates that [stmt] should be added after the target statement.
[before] and [post] are mutually exclusive. *)
val extend_stmt_in_place: t -> stmt -> label:logic_label -> block -> t
(** [extend_stmt_in_place env stmt ~label b] modifies [stmt] in place in
......
......@@ -49,20 +49,22 @@ 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.vname then begin
&& Functions.RTL.has_rtl_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
fvi, args
end
else if Options.Validate_format_strings.get ()
&& Functions.Libc.is_printf_name caller.vname then
&& Functions.Libc.is_printf_name caller.vorig_name then
(* 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 *)
(* replacement name, e.g., [printf] -> [__e_acsl_builtin_printf] *)
let fvi = Rtl.Symbols.libc_replacement caller in
let fmt = Functions.Libc.get_printf_argument_str ~loc caller.vname args in
let fmt =
Functions.Libc.get_printf_argument_str ~loc caller.vorig_name args
in
fvi, fmt :: args
else
caller, args
......@@ -86,7 +88,7 @@ let rec inject_in_init env kf_opt vi off = function
in
CompoundInit(typ, List.rev l), env
let inject_in_local_init loc env kf vi = function
let inject_in_local_init ~loc ~stmt env kf vi = function
| ConsInit (fvi, sz :: _, _) as init
when Functions.Libc.is_vla_alloc_name fvi.vname ->
(* add a store statement when creating a variable length array *)
......@@ -97,6 +99,13 @@ let inject_in_local_init loc env kf vi = function
| ConsInit (caller, args, kind) ->
let args, env = replace_literal_strings_in_args env (Some kf) args in
let caller, args = rename_caller ~loc caller args in
let _, env =
if Libc.is_writing_memory caller then begin
let result = Var vi, NoOffset in
Libc.update_memory_model ~loc ~stmt env kf ~result caller args
end else
None, env
in
ConsInit(caller, args, kind), env
| AssignInit init ->
......@@ -151,6 +160,14 @@ let inject_in_instr env kf stmt = function
Cil.evar fvi, args
| _ -> caller, args
in
(* if this is a call to a libc function that writes into a memory block then
manually update the memory model *)
let result, env =
match caller.enode with
| Lval (Var cvi, _) when Libc.is_writing_memory cvi ->
Libc.update_memory_model ~loc ~stmt env kf ?result cvi args
| _ -> result, env
in
(* add statement tracking initialization of return values *)
let env =
match result with
......@@ -175,7 +192,7 @@ let inject_in_instr env kf stmt = function
| Local_init(vi, linit, loc) ->
let lv = Var vi, NoOffset in
let env = add_initializer loc ~vi lv ~post:true stmt env kf in
let linit, env = inject_in_local_init loc env kf vi linit in
let linit, env = inject_in_local_init ~loc ~stmt env kf vi linit in
Local_init(vi, linit, loc), env
(* nothing to do: *)
......
(**************************************************************************)
(* *)
(* This file is part of the Frama-C's E-ACSL plug-in. *)
(* *)
(* Copyright (C) 2012-2020 *)
(* 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). *)
(* *)
(**************************************************************************)
(** Code generation for libc functions *)
open Cil_types
(* Retrieve the name of the caller function. [vorig_name] is used instead of
[vname] because some plugins like "Variadic" may change the value of [vname] 
for some functions like [sprintf]. *)
let get_caller_name caller =
caller.vorig_name
let is_writing_memory caller =
match get_caller_name caller with
(* Input / output functions *)
(* - Formatted *)
| "sprintf" | "snprintf" | "vsprintf" | "vsnprintf" | "swprintf" | "vswprintf"
| "scanf" | "fscanf" | "sscanf" | "vscanf" | "vfscanf" | "vsscanf" | "wscanf"
| "fwscanf" | "swscanf" | "vwscanf" | "vfwscanf" | "vswscanf"
(* - Unformatted *)
| "gets" | "fgets" | "fgetws"
(* - Direct *)
| "fread"
(* Byte strings *)
(* - Conversions *)
| "strtol" | "strtoll" | "strtoul" | "strtoull" | "strtof" | "strtod"
| "strtold" | "strtoimax" | "strtoumax"
(* - String manipulation *)
| "strcpy" | "strncpy" | "strcat" | "strncat" | "strxfrm"
(* - Character array manipulation *)
| "memset" | "memcpy" | "memmove"
(* Multi-byte strings *)
| "mbtowc" | "wctomb" | "mbstowcs" | "wcstombs" | "mbrtowc" | "wcrtomb"
| "mbsrtowcs" | "wcsrtombs"
(* Wide strings *)
(* - Conversions *)
| "wcstol" | "wcstoll" | "wcstoul" | "wcstoull" | "wcstof" | "wcstod"
| "wcstold" | "wcstoimax" | "wcstoumax"
(* - Wide string manipulation *)
| "wcscpy" | "wcsncpy" | "wcscat" | "wcsncat" | "wcsxfrm"
(* - Wide character array manipulation *)
| "wmemset" | "wmemcpy" | "wmemmove"
-> true
| _ -> false
let () =
Prepare_ast.is_libc_writing_memory_ref := is_writing_memory
(** [get_result_var ~loc ~name kf ty env result_opt] returns an lvalue
representing the result of the call to the libc function. If [result_opt]
is [Some var] then this lvalue is directly returned, but if the return value
of the function was not saved and [result_opt] is [None], then a new value
is created to hold the result of the call. *)
let get_result_var ~loc ~name kf ty env result_opt =
match result_opt with
| Some result -> result, env
| None ->
let vi, _, env =
Env.new_var
~loc
~scope:Varname.Function
~name:(name ^ "_res")
env
kf
None
ty
(fun _ _ -> [])
in
Cil.var vi, env
(** [rtl_call_to_new_var ~loc ~name env kf ty fname args] creates a call to the
RTL function [fname] with arguments [args] and stores the result in a new
variable named [name]. *)
let rtl_call_to_new_var ~loc ~name env kf ty fname args =
let vi, e, env =
Env.new_var
~loc
~scope:Varname.Function
~name
env
kf
None
ty
(fun _ _ -> [])
in
let stmt =
Smart_stmt.rtl_call ~loc ~result:(Cil.var vi) fname args
in
vi, e, stmt, env
(** [strlen ~loc ~name env kf e] generates a call to the RTL function
[__e_acsl_builtin_strlen] and stores the result in a new variable named
[name].
The E-ACSL built-in version of [strlen] is used to be able to work even if
[string.h] was not included in the original code. Moreover, the built-in
version already check the preconditions of the function so it is not
necessary to generate more RTE checks. *)
let strlen ~loc ~name env kf e =
rtl_call_to_new_var
~loc
~name
env
kf
Cil.theMachine.typeOfSizeOf
"builtin_strlen"
[ e ]
(** [wrong_number_of_arguments name] aborts the execution of E-ACSL with a
message about the number of arguments for [name]. *)
let wrong_number_of_arguments name =
Options.fatal
"Wrong number of arguments for E-ACSL built-in '%s'. Should have been \
caught by Frama-C kernel before."
name
(** [lval_to_term ~loc lval] converts the lvalue [lval] to a term. *)
let lval_to_term ~loc lval =
let ty = Cil.typeOfLval lval in
Logic_const.term ~loc (TLval (Logic_utils.lval_to_term_lval lval)) (Ctype ty)
(** [zarith ~loc bop t1 t2] creates an integer term representing the arithmetic
operation [t1 bop t2]. *)
let zarith ~loc bop t1 t2 =
(* Check that we are building an arithmetic operation *)
(match bop with
| PlusA | MinusA | Mult | Div | Mod | Shiftlt | Shiftrt -> ()
| PlusPI | IndexPI | MinusPI | MinusPP | Lt | Gt | Le | Ge | Eq | Ne | BAnd
| BXor | BOr | LAnd | LOr ->
Options.fatal
"Using Libc.zarith to build '%a' instead of an arithmetic operation"
Printer.pp_binop bop);
(* Coerce arguments to integers *)
let t1 = Logic_utils.numeric_coerce Linteger t1 in
let t2 = Logic_utils.numeric_coerce Linteger t2 in
(* Create binop term *)
Logic_const.term ~loc (TBinOp (bop, t1, t2)) Linteger
(** [check_integer_bounds ~from target] checks if the bounds need to be checked
while coercing an integer variable from the kind [from] to the kind
[target].
@return a pair where the first element is true if the lower bound needs to
be checked and false otherwise, and the second element is true if the upper
bound needs to be checked and false otherwise. *)
let check_integer_bounds ~from target =
let from_bitsize = Cil.bitsSizeOfInt from in
let target_bitsize = Cil.bitsSizeOfInt target in
match Cil.isSigned from, Cil.isSigned target with
| true, true | false, false ->
let check_bounds = from_bitsize > target_bitsize in
check_bounds, check_bounds
| true, false ->
let from_max = Cil.max_signed_number from_bitsize in
let target_max = Cil.max_unsigned_number target_bitsize in
true, from_max > target_max
| false, true ->
let from_max = Cil.max_unsigned_number from_bitsize in
let target_max = Cil.max_signed_number target_bitsize in
false, from_max > target_max
(** [term_to_sizet_exp ~loc ?check_lower_bound kf env t] translates the term [t]
to a C expression of type [size_t]. If the term is a GMP value then bounding
checks are added to ensure that the term holds in the C type.
If [check_lower_bound] is set to false, then the lower bound check is not
performed. *)
let term_to_sizet_exp ~loc ~name ?(check_lower_bound=true) kf env t =
Typing.type_term ~use_gmp_opt:false t;
match Typing.get_number_ty t with
| Typing.Gmpz ->
Translate.gmp_to_sizet ~loc ~name ~check_lower_bound kf env t
| Typing.(C_integer _ | C_float _) as nty ->
(* We know that [t] can be translated to a C type, so we start with that *)
let e, env = Translate.term_to_exp kf env t in
(* Then we can check if the expression will fit in a [size_t] *)
let sizet = Cil.(theMachine.typeOfSizeOf) in
let sizet_kind = Cil.(theMachine.kindOfSizeOf) in
let check_lower_bound, check_upper_bound =
let lower, upper =
match nty with
| Typing.C_integer t_kind ->
check_integer_bounds ~from:t_kind sizet_kind
| Typing.C_float _ -> true, true
| _ -> assert false
in
lower && check_lower_bound, upper
in
let stmts, env =
if check_lower_bound then begin
let lower_guard = Cil.mkBinOp ~loc Ge e (Cil.zero ~loc) in
let lower_guard_pp =
Logic_const.prel ~loc (Rge, t, Cil.lzero ~loc ())
in
let assertion =
Smart_stmt.runtime_check
~pred_kind:Assert
Smart_stmt.RTE
kf
lower_guard
lower_guard_pp
in
[ assertion ], env
end else [], env
in
let stmts, env =
if check_upper_bound then begin
let sizet_max_z = Cil.max_unsigned_number (Cil.bitsSizeOf sizet) in
let sizet_max_t = Logic_const.tint ~loc sizet_max_z in
let sizet_max_e =
Cil.kinteger64 ~loc ~kind:sizet_kind sizet_max_z
in
let upper_guard_pp = Logic_const.prel ~loc (Rle, t, sizet_max_t) in
let upper_guard = Cil.mkBinOp ~loc Le e sizet_max_e in
let assertion =
Smart_stmt.runtime_check
~pred_kind:Assert
Smart_stmt.RTE
kf
upper_guard
upper_guard_pp
in
assertion :: stmts, env
end else
stmts, env
in
(* If no assertions have been generated we can directly return the
translated expression, otherwise we create a [size_t] variable to hold
the conversion*)
if stmts = [] then
e, env
else
let _, e, env =
Env.new_var
~loc
env
kf
None
sizet
(fun vi _ ->
let assigns = Smart_stmt.assigns ~loc ~result:(Cil.var vi) e in
List.rev (assigns :: stmts))
in
e, env
| Typing.(Rational | Real) ->
Env.not_yet env "cast of rational or real to size_t"
| Typing.Nan ->
Options.fatal
"Trying to translate a term that is not an integer or a C type: %a"
Printer.pp_term t
(** Code generation of [update_memory_model] for [strcat] and [strncat]. *)
let process_strcat ~loc ~stmt ?result env kf ?size_e dest_e src_e =
let src_size_vi, src_size_e, src_size_stmt, env =
strlen ~loc ~name:"strcat_src_size" env kf src_e
in
let pre_stmts = [ src_size_stmt ] in
let pre_stmts =
match size_e with
| Some size_e ->
let src_size_if_stmt =
Smart_stmt.if_stmt
~loc
~cond:(Cil.mkBinOp ~loc Lt size_e src_size_e)
(Cil.mkBlock [
Smart_stmt.assigns ~loc ~result:(Cil.var src_size_vi) size_e
])
in
src_size_if_stmt :: pre_stmts
| None -> pre_stmts
in
let dest_size_vi, _, dest_size_stmt, env =
strlen ~loc ~name:"strcat_dest_size" env kf dest_e
in
let pre_stmts = dest_size_stmt :: pre_stmts in
let env = Env.push env in
let src_size_term = Cil.cvar_to_term ~loc src_size_vi in
let dest_size_term = Cil.cvar_to_term ~loc dest_size_vi in
let n_t = zarith ~loc PlusA src_size_term dest_size_term in
let n_t = zarith ~loc PlusA n_t (Cil.lone ~loc ()) in
(* By construction, [n_t] cannot be negative so we do not need to check the
lower bound. *)
let n, env =
term_to_sizet_exp ~loc ~name:"size" ~check_lower_bound:false kf env n_t
in
(* The specifications of [strcat] and [strncat] indicate that these functions
write only from [dest_e + strlen(dest)] to
[dest_e + strlen(dest_e) + strlen(src_e) + 1]. However since they require
the [dest_e] string to be valid from [dest_e] to
[dest_e + strlen(dest_e) +1], we can call initialize from [dest_e] to
[dest_e + strlen(dest_e) + strlen(src_e) + 1]. This allows us to only
compute the size of the initialization (in [n]) instead of computing the
start pointer and the size. *)
let initialize = Smart_stmt.rtl_call ~loc "initialize" [ dest_e; n ] in
let initialize_blk, env =