From 5ac2525de6b185d9a5065ef57ae57a85d9cb1a09 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Fri, 28 Jul 2017 13:46:04 +0200
Subject: [PATCH] MR !151 Review: address reviewer's comments
---
src/plugins/e-acsl/prepare_ast.ml | 14 +-
src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c | 4 +-
.../share/e-acsl/e_acsl_temporal_timestamp.h | 4 +-
.../segment_model/e_acsl_segment_tracking.h | 2 +-
src/plugins/e-acsl/temporal.ml | 567 +++++++++---------
src/plugins/e-acsl/temporal.mli | 11 +-
.../tests/temporal/oracle/gen_t_addr-by-val.c | 36 ++
.../temporal/oracle/t_addr-by-val.err.oracle | 0
.../temporal/oracle/t_addr-by-val.res.oracle | 2 +
.../e-acsl/tests/temporal/t_addr-by-val.c | 18 +
src/plugins/e-acsl/visit.ml | 75 ++-
11 files changed, 407 insertions(+), 326 deletions(-)
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
create mode 100644 src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
diff --git a/src/plugins/e-acsl/prepare_ast.ml b/src/plugins/e-acsl/prepare_ast.ml
index 980326a32fb..f67f0411757 100644
--- a/src/plugins/e-acsl/prepare_ast.ml
+++ b/src/plugins/e-acsl/prepare_ast.ml
@@ -50,28 +50,26 @@ let sufficiently_aligned attrs algn =
should not happen really *)
assert false
| _ -> acc
- ) 0 attrs in
- if alignment > 0 then true else false
+ ) 0 attrs in alignment > 0
(* Given the type and the list of attributes of [varinfo] ([fieldinfo]) return
* true if that [varinfo] ([fieldinfo]) requires to be aligned at the boundary
* of [algn] (i.e., less than [algn] bytes and has no alignment attribute *)
let require_alignment typ attrs algn =
- if (Cil.bitsSizeOf typ) < algn*8 && not (sufficiently_aligned attrs algn) then
- true
- else
- false
+ Cil.bitsSizeOf typ < algn*8 && not (sufficiently_aligned attrs algn)
class prepare_visitor prj = object (_)
inherit Visitor.frama_c_copy prj
(* Add align attributes to local variables (required by temporal analysis) *)
method !vblock _ =
- if (Temporal.is_enabled ()) then
+ if Temporal.is_enabled () then
Cil.DoChildrenPost (fun blk ->
List.iter (fun vi ->
+ (* 4 bytes alignment is required to allow sufficient space for storage
+ of 32-bit timestamps in a 1:1 shadow. *)
if require_alignment vi.vtype vi.vattr 4; then begin
- vi.vattr <- Attr("aligned",[AInt(Integer.four)]) :: vi.vattr
+ vi.vattr <- Attr("aligned",[AInt Integer.four]) :: vi.vattr
end)
blk.blocals;
blk)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
index 55db362411c..1f00c49e34d 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_rtl.c
@@ -105,8 +105,8 @@ static void describe_run();
# error "No E-ACSL memory model defined. Aborting compilation"
#endif
-/* Temporal analysis shared by both models.
- * Uses macros differently defined macros */
+/* This header contains temporal analysis shared by both models.
+ It should be here as it uses differently defined macros */
#include "e_acsl_temporal.h"
#ifdef E_ACSL_WEAK_VALIDITY
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h
index 40b7a006c17..55ceb6261f9 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_temporal_timestamp.h
@@ -51,9 +51,11 @@ static uint32_t temporal_timestamp = 2;
struct temporal_parameter {
void *ptr;
+ /* Number all members such that there is no `0` which potentially
+ corresponds to an invalid number */
enum {
TBlockN = 10,
- TReferentN = 20,
+ TReferentN = 20,
TCopy = 30
} temporal_flow;
};
diff --git a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
index 94101e24955..f1a03d0df9b 100644
--- a/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
+++ b/src/plugins/e-acsl/share/e-acsl/segment_model/e_acsl_segment_tracking.h
@@ -1234,7 +1234,7 @@ static int heap_initialized(uintptr_t addr, long len) {
#ifdef E_ACSL_TEMPORAL
static uint32_t heap_temporal_info(uintptr_t addr, int origin) {
/* NOTE: No checking for allocated blocks, since an invalid
- timestamp is zero and ununsed memory is nullified then an invalid
+ timestamp is zero and unused memory is nullified then an invalid
timestamp is also returned for allocated memory */
if (origin) {
uintptr_t *aligned_shadow = (uintptr_t*)ALIGNED_HEAP_SHADOW(addr);
diff --git a/src/plugins/e-acsl/temporal.ml b/src/plugins/e-acsl/temporal.ml
index 6ecaacaa95e..e6314460f69 100644
--- a/src/plugins/e-acsl/temporal.ml
+++ b/src/plugins/e-acsl/temporal.ml
@@ -24,7 +24,7 @@ open Cil_types
open Cil_datatype
(* ************************************************************************** *)
-(** {Configuration} {{{ *)
+(* Configuration {{{ *)
(* ************************************************************************** *)
let current_stmt = ref Cil.dummyStmt
@@ -33,223 +33,230 @@ let generate = ref false
(* }}} *)
(* ************************************************************************** *)
-(** {Types} {{{ *)
+(* Types {{{ *)
(* ************************************************************************** *)
(* Type of identifier tracked by a LHS referent number *)
type flow =
- | Direct (* take BlockID of RHS *)
- | Indirect (* take ReferentID of RHS *)
+ | Direct (* take origin number of RHS *)
+ | Indirect (* take referent number of RHS *)
| Copy (* Copy shadow from RHS to LHS *)
(* }}} *)
(* ************************************************************************** *)
-(** {Miscellaneous} {{{ *)
+(* Miscellaneous {{{ *)
(* ************************************************************************** *)
(* Generate a function name in the temporal analysis name space, i.e., prefixed
by [__e_acsl_temporal_ + function name].
NOTE: Further on, all analysis function names are used without prefix *)
-let mk_api_name name =
- let fname = "temporal_" ^ name in Misc.mk_api_name fname
+let mk_api_name name = Misc.mk_api_name ("temporal_" ^ name)
-let is_alloc_name fn =
- fn = "malloc" || fn = "free" || fn = "realloc" || fn = "calloc"
+let is_alloc_name fn = fn = "malloc" || fn = "free" || fn = "realloc" || fn = "calloc"
-let is_memcpy_name fn =
- fn = "memcpy"
+let is_memcpy_name fn = fn = "memcpy"
-let is_memset_name fn =
- fn = "memset"
+let is_memset_name fn = fn = "memset"
-let is_fn fname f =
- match fname with
- | { enode = Lval(Var(vi), _) } when f vi.vname -> true
- | _ -> false
+let get_fname = function
+ | { enode = Lval(Var(vi), _) } -> vi.vname
+ | _ -> ""
-let is_alloc fvi =
- is_fn fvi is_alloc_name
+let is_fn f fname = f (get_fname fname)
-let is_memcpy fvi =
- is_fn fvi is_memcpy_name
+let is_alloc fvi = is_fn is_alloc_name fvi
-let is_memset fvi =
- is_fn fvi is_memset_name
+let is_memcpy fvi = is_fn is_memcpy_name fvi
+
+let is_memset fvi = is_fn is_memset_name fvi
(* True if a named function has a definition and false otherwise *)
let has_fundef fname =
let recognize fn =
- try
- let _ = Globals.Functions.find_def_by_name fn in true
- with
- Not_found -> false
- in is_fn fname recognize
+ try let _ = Globals.Functions.find_def_by_name fn in true
+ with Not_found -> false
+ in
+ is_fn recognize fname
(* Shortcuts for SA in Mmodel_analysis *)
let must_model_exp exp env =
let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
- Mmodel_analysis.must_model_exp ~bhv ~kf exp
+ Mmodel_analysis.must_model_exp ~bhv ~kf exp
let must_model_lval lv env =
let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
- Mmodel_analysis.must_model_lval ~bhv ~kf lv
+ Mmodel_analysis.must_model_lval ~bhv ~kf lv
let must_model_vi vi env =
let kf, bhv = Extlib.the (Env.current_kf env), Env.get_behavior env in
- Mmodel_analysis.must_model_vi ~bhv ~kf vi
+ Mmodel_analysis.must_model_vi ~bhv ~kf vi
(* }}} *)
(* ************************************************************************* *)
-(** {Analysis function calls} {{{ *)
+(* Generate analysis function calls {{{ *)
(* ************************************************************************** *)
-(* Generate either
- - [store_nblock(lhs, rhs)], or
- - [store_nreferent(lhs, rhs)]
-function call based on the value of [flow] *)
-let mk_store_reference ~loc flow lhs rhs =
- let fname = match flow with
- | Direct -> "store_nblock"
- | Indirect -> "store_nreferent"
- | Copy -> failwith "Copy flow type in mk_store_reference"
- in
- Misc.mk_call ~loc (mk_api_name fname) [ Cil.mkAddrOf ~loc lhs; rhs ]
-
-(* Generate a [save_*_parameter] call *)
-let mk_save_param ~loc flow lhs pos =
- let infix = match flow with
- | Direct -> "nblock"
- | Indirect -> "nreferent"
- | Copy -> "copy"
- in
- let fname = "save_" ^ infix ^ "_parameter" in
- Misc.mk_call ~loc (mk_api_name fname) [ lhs ; Cil.integer ~loc pos ]
-
-(* Generate [pull_parameter] call *)
-let mk_pull_param ~loc vi pos =
- let exp = Cil.mkAddrOfVi vi in
- let fname = mk_api_name "pull_parameter" in
- let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
- Misc.mk_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
-
-(* Generate [(save|pull)_return(lhs, param_no)] call *)
-let mk_handle_return_referent ?(save=true) ~loc lhs =
- let fname = match save with
- | true -> "save_return"
- | false -> "pull_return"
- in
- (* TODO: Returning structs is unsupported so far *)
- ignore(match (Cil.typeOf lhs) with
- | TPtr _ -> ()
- | _ -> failwith "Struct in return");
- Misc.mk_call ~loc (mk_api_name fname) [ lhs ]
-
-(* Generate [reset_return()] call *)
-let mk_reset_return_referent ~loc =
- Misc.mk_call ~loc (mk_api_name "reset_return") []
-
-(* Generate [memcpy(lhs, rhs, size)] function call assuming that [lhs = rhs]
- represents an assignment of struct to a struct, that is, both sides are left
- values and we need to use addressof for both sides *)
-let mk_temporal_memcpy_struct ~loc lhs rhs =
- let fname = mk_api_name "memcpy" in
- let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
- let lhs = Cil.mkAddrOf ~loc lhs in
- Misc.mk_call ~loc fname [ lhs; rhs; size ]
+module Mk: sig
+ (* Generate either
+ - [store_nblock(lhs, rhs)], or
+ - [store_nreferent(lhs, rhs)]
+ function call based on the value of [flow] *)
+ val store_reference: loc:location -> flow -> lval -> exp -> stmt
+
+ (* Generate a [save_*_parameter] call *)
+ val save_param: loc:location -> flow -> exp -> int -> stmt
+
+ (* Generate [pull_parameter] call *)
+ val pull_param: loc:location -> varinfo -> int -> stmt
+
+ (* Generate [(save|pull)_return(lhs, param_no)] call *)
+ val handle_return_referent: save:bool -> loc:location -> exp -> stmt
+
+ (* Generate [reset_return()] call *)
+ val reset_return_referent: loc:location -> stmt
+
+ (* Generate [memcpy(lhs, rhs, size)] function call assuming that [lhs = rhs]
+ represents an assignment of struct to a struct, that is, both sides are left
+ values and we need to use addressof for both sides *)
+ val temporal_memcpy_struct: loc:location -> lval -> exp -> stmt
+end = struct
+
+ let store_reference ~loc flow lhs rhs =
+ let fname = match flow with
+ | Direct -> "store_nblock"
+ | Indirect -> "store_nreferent"
+ | Copy -> Options.fatal "Copy flow type in store_reference"
+ in
+ Misc.mk_call ~loc (mk_api_name fname) [ Cil.mkAddrOf ~loc lhs; rhs ]
+
+ let save_param ~loc flow lhs pos =
+ let infix = match flow with
+ | Direct -> "nblock"
+ | Indirect -> "nreferent"
+ | Copy -> "copy"
+ in
+ let fname = "save_" ^ infix ^ "_parameter" in
+ Misc.mk_call ~loc (mk_api_name fname) [ lhs ; Cil.integer ~loc pos ]
+
+ let pull_param ~loc vi pos =
+ let exp = Cil.mkAddrOfVi vi in
+ let fname = mk_api_name "pull_parameter" in
+ let sz = Cil.kinteger ~loc IULong (Cil.bytesSizeOf vi.vtype) in
+ Misc.mk_call ~loc fname [ exp ; Cil.integer ~loc pos ; sz ]
+
+ let handle_return_referent ~save ~loc lhs =
+ let fname = match save with
+ | true -> "save_return"
+ | false -> "pull_return"
+ in
+ (* TODO: Returning structs is unsupported so far *)
+ (match (Cil.typeOf lhs) with
+ | TPtr _ -> ()
+ | _ -> Error.not_yet "Struct in return");
+ Misc.mk_call ~loc (mk_api_name fname) [ lhs ]
+
+ let reset_return_referent ~loc =
+ Misc.mk_call ~loc (mk_api_name "reset_return") []
+
+ let temporal_memcpy_struct ~loc lhs rhs =
+ let fname = mk_api_name "memcpy" in
+ let size = Cil.sizeOf ~loc (Cil.typeOfLval lhs) in
+ Misc.mk_call ~loc fname [ Cil.mkAddrOf ~loc lhs; rhs; size ]
+end
(* }}} *)
(* ************************************************************************** *)
-(** {Handle assignments} {{{ *)
+(* Handle assignments {{{ *)
(* ************************************************************************** *)
(* Given an lvalue [lhs] representing LHS of an assignment, and an expression
- [rhs] representing its RHS compute addresses compute a triple (l,r,f), such
- that:
+ [rhs] representing its RHS compute triple (l,r,f), such that:
- lval [l] and exp [r] are addresses of a pointer and a memory block, and
- flow [f] indicates how to update the meta-data of [l] using information
stored by [r]. The values of [f] indicate the following
+ Direct - referent number of [l] is assigned the referent number of [r]
- + Indirect - referent number of [l] is assigned the block number of [r]
+ + Indirect - referent number of [l] is assigned the origin number of [r]
+ Copy - metadata of [r] is copied to metadata of [l] *)
-let rec assign_aux ?(ltype) lhs rhs loc =
+let assign ?(ltype) lhs rhs loc =
+ (* Do not use [Extlib.opt_conv] here, application of the [None] part should
+ not be evaluated at this point, as otherwise it will lead to an exception
+ via [Cil.typeOfLval] later *)
let ltype = match ltype with
| Some l -> l
| None -> (Cil.typeOfLval lhs)
in
- match ltype with
+ match Cil.unrollType ltype with
| TPtr _ ->
let base, _ = Misc.ptr_index rhs in
let rhs, flow =
(match base.enode with
| AddrOf _
| StartOf _ -> rhs, Direct
- | Const _ -> base, Direct
(* Unary operator describes !, ~ or -: treat it same as Const since
it implies integer or logical operations. This case is rare but
happens: for instance in Gap SPEC CPU benchmark the returned pointer
is assigned -1 (for whatever bizarre reason) *)
- | UnOp _ -> base, Direct
+ | Const _ | UnOp _ -> base, Direct
(* Special case for literal strings which E-ACSL rewrites into
- global variables: take the block number of a string *)
- | Lval(Var(vi), _) when Misc.is_generated_varinfo vi -> base, Direct
- (* Lvalue can be of different type than a pointer, for instance for
- the case when address is taken by value.
+ global variables: take the origin number of a string *)
+ | Lval(Var vi, _) when Misc.is_generated_varinfo vi -> base, Direct
+ (* Lvalue of a pointer type can be a cast of an integral type, for
+ instance for the case when address is taken by value (shown via the
+ following example).
uintptr_t addr = ...;
char *p = (char* )addr;
- If this is the case then the analysis assumes that pointer is
- unavailable and takes the block number of address and the referent
- number of a pointer otherwise *)
- | Lval(lv) ->
- if Cil.isPointerType (Cil.typeOfLval lv) then
+ If this is the case then the analysis takes the value of a variable. *)
+ | Lval lv ->
+ if Cil.isPointerType (Cil.unrollType (Cil.typeOfLval lv)) then
Cil.mkAddrOf ~loc lv, Indirect
else
rhs, Direct
- (* Binary operation which yields an integer (of FP) type.
+ (* Binary operation which yields an integer (or FP) type.
Since LHS is of pointer type we assume that the whole integer
expression computes to an address for which there is no
- outer container, so the only thing to do is to take block number *)
+ outer container, so the only thing to do is to take origin number *)
| BinOp(op, _, _, _) ->
- (* Make sure there are no be pointer operations here *)
- ignore((match op with
+ (* Make sure there are no pointer operations here *)
+ (match op with
| MinusPI | PlusPI | IndexPI -> assert false
- | _ -> ()));
+ | _ -> ());
base, Direct
| _ -> assert false)
in Some (lhs, rhs, flow)
- | TNamed(info, _) ->
- assign_aux ~ltype:info.ttype lhs rhs loc
+ | TNamed _ ->
+ assert false
| TInt _ | TFloat _ | TEnum _ -> None
- | TComp _ ->
- let rhs = (match rhs.enode with
+ | TComp _ ->
+ let rhs = match rhs.enode with
| AddrOf _ -> rhs
- | Lval(lv) -> Cil.mkAddrOf ~loc lv
- | _ -> assert false) in
- Some (lhs, rhs, Copy)
+ | Lval lv -> Cil.mkAddrOf ~loc lv
+ | Const _ | SizeOf _ | SizeOfE _ | SizeOfStr _ | AlignOf _ | AlignOfE _
+ | UnOp _ | BinOp _ | CastE _ | StartOf _ | Info _ ->
+ Options.abort "unsupported RHS %a" Printer.pp_exp rhs
+ in Some (lhs, rhs, Copy)
(* va_list is a builtin type, we assume it has no pointers here and treat
it as a "big" integer rather than a struct *)
| TBuiltin_va_list _ -> None
| TArray _ -> Some (lhs, rhs, Direct)
(* void type should not happen as we are dealing with assignments *)
- | TVoid _ -> failwith "Void type in assignment"
- | TFun _ -> failwith "TFun type in assignment"
+ | TVoid _ -> Options.fatal "Void type in assignment"
+ | TFun _ -> Options.fatal "TFun type in assignment"
(* Generate a statement tracking temporal metadata associated with assignment
[lhs] = [rhs], where lhs is a left value and [rhs] is an expression. *)
let mk_stmt_from_assign loc lhs rhs =
- match (assign_aux lhs rhs loc) with
+ match assign lhs rhs loc with
| Some (lhs, rhs, flow) ->
let stmt = (match flow with
- | Direct | Indirect ->
- mk_store_reference ~loc flow lhs rhs
- | Copy ->
- mk_temporal_memcpy_struct ~loc lhs rhs)
+ | Direct | Indirect -> Mk.store_reference ~loc flow lhs rhs
+ | Copy -> Mk.temporal_memcpy_struct ~loc lhs rhs)
in Some stmt
| None -> None
(* }}} *)
(* ************************************************************************** *)
-(** {Handle Set instructions} {{{ *)
+(* Handle Set instructions {{{ *)
(* ************************************************************************** *)
(* Update local environment with a statement tracking temporal metadata
@@ -265,168 +272,181 @@ let set_instr ?(post=false) loc lhs rhs fenv =
let set_instr ?(post=false) loc lhs rhs fenv =
if must_model_lval lhs !fenv then
set_instr ~post loc lhs rhs fenv
-
(* }}} *)
(* ************************************************************************** *)
-(** {Handle Call instructions} {{{ *)
+(* Handle Call instructions {{{ *)
(* ************************************************************************** *)
-(* Track function arguments: export referents of arguments to a global
- structure so they can be retrieved once that function is called *)
-let save_params loc args fenv =
- List.iteri
- (fun index param ->
- let dummy_lv = Mem(param),NoOffset in
- let ltype = Cil.typeOf param in
- let vals = assign_aux ~ltype dummy_lv param loc in
- Extlib.may
- (fun (_, rhs, flow) ->
- if must_model_exp param !fenv then begin
- let stmt = mk_save_param ~loc flow rhs index in
- fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt
- end)
- vals)
- args
-
-(* Update local environment with a statement tracking temporal metadata
- associated with assignment [ret] = [func(args)]. *)
-let call_with_ret ?(alloc=false) loc ret fenv =
- let rhs = Cil.new_exp ~loc (Lval(ret)) in
- let vals = assign_aux ret rhs loc in
- (* Track referent numbers of assignments via function calls *)
- Extlib.may
- (fun (lhs, rhs, flow) ->
- let flow, rhs = match flow with
- | Indirect when alloc -> Direct, (Misc.mk_deref ~loc rhs)
- | _ -> flow, rhs
- in
- let stmt =
- if alloc then
- mk_store_reference ~loc flow lhs rhs
- else
- mk_handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
- in
- fenv := Env.add_stmt ~before:!current_stmt ~post:true !fenv stmt)
- vals
+module Function_call: sig
+ (* Top-level handler for Call instructions *)
+ val instr: lval option -> exp -> exp list -> location -> Env.t ref -> unit
+end = struct
+
+ (* Track function arguments: export referents of arguments to a global
+ structure so they can be retrieved once that function is called *)
+ let save_params loc args fenv =
+ List.iteri
+ (fun index param ->
+ let lv = Mem(param), NoOffset in
+ let ltype = Cil.typeOf param in
+ let vals = assign ~ltype lv param loc in
+ Extlib.may
+ (fun (_, rhs, flow) ->
+ if must_model_exp param !fenv then begin
+ let stmt = Mk.save_param ~loc flow rhs index in
+ fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt
+ end)
+ vals)
+ args
+
+ (* Update local environment with a statement tracking temporal metadata
+ associated with assignment [ret] = [func(args)]. *)
+ let call_with_ret ?(alloc=false) loc ret fenv =
+ let rhs = Cil.new_exp ~loc (Lval ret) in
+ let vals = assign ret rhs loc in
+ (* Track referent numbers of assignments via function calls.
+ Library functions (i.e., with no source code available) that return
+ values are considered to be functions that allocate memory. They are
+ considered so because they need to be handled exactly as memory
+ allocating functions, that is the referent of the returned pointer is
+ assigned the origin number associated with the return value. For
+ instance, for some [p = call();] [store_nblock( *p,..)] is appended.
+ Note that for this we need [Direct] flow and also dereference the
+ pointer to get its number. This is done in the following statement
+ (where variable [alloc] indicates whether a function is a
+ memory-allocating function or not).
+
+ Alternatively, if a function does not allocate memory and its body has
+ been instrumented, then information about referent numbers should be
+ stored in the internal data structure and it is retrieved using
+ [pull_return] added via a call to [Mk.handle_return_referent] *)
+ Extlib.may
+ (fun (lhs, rhs, flow) ->
+ let flow, rhs = match flow with
+ | Indirect when alloc -> Direct, (Misc.mk_deref ~loc rhs)
+ | _ -> flow, rhs
+ in
+ let stmt =
+ if alloc then
+ Mk.store_reference ~loc flow lhs rhs
+ else
+ Mk.handle_return_referent ~save:false ~loc (Cil.mkAddrOf ~loc lhs)
+ in
+ fenv := Env.add_stmt ~before:!current_stmt ~post:true !fenv stmt)
+ vals
+
+ (* Update local environment with a statement tracking temporal metadata
+ associated with memcpy/memset call *)
+ let call_memxxx loc args fname fenv =
+ if is_memcpy fname || is_memset fname then begin
+ let stmt = Misc.mk_call ~loc (mk_api_name (get_fname fname)) args in
+ fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
+ end
-(* Update local environment with a statement tracking temporal metadata
- associated with a memcpy call *)
-let call_memcpy loc args fname fenv =
- if (is_memcpy fname) then begin
- let stmt = Misc.mk_call ~loc (mk_api_name "memcpy") args in
+ let instr ret fname args loc fenv =
+ (* Add function calls to reset_parameters and reset_return before each
+ function call regardless. They are not really required, as if the
+ instrumentation is correct then the right parameters will be saved
+ and the right parameter will be pulled at runtime. In practice, however,
+ it makes sense to make this somewhat-debug-level-call. In production mode
+ the implementation of the function should be empty and compiler should
+ be able to optimize that code out. *)
+ let stmt = Misc.mk_call ~loc (mk_api_name "reset_parameters") [] in
fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
- end
-
-(* Update local environment with a statement tracking temporal metadata
- associated with a memset call. *)
-let call_memset loc args fname fenv =
- if (is_memset fname) then begin
- let stmt = Misc.mk_call ~loc (mk_api_name "memset") args in
+ let stmt = Mk.reset_return_referent ~loc in
fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
- end
-
-(* Top-level handler for Call instructions *)
-let call_instr ret fname args loc fenv =
- (* Add function calls to reset_parameters and reset_return before each
- function call regardless. They are is not really required, as if the
- instrumentation is correct then the right parameters will be saved
- and the right parameter will be pulled at runtime. In practice, however,
- it makes sense to make this somewhat-debug-level-call. In production mode
- the implementation of the function should be empty and compiler should
- be able to optimize that code out. *)
- let stmt = Misc.mk_call ~loc (mk_api_name "reset_parameters") [] in
- fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
- let stmt = mk_reset_return_referent ~loc in
- fenv := Env.add_stmt ~before:!current_stmt ~post:false !fenv stmt;
- (* Push parameters with either a call to a function pointer or a function
- definition otherwise there is no point. *)
- if Cil.isFunctionType (Cil.typeOf fname) || has_fundef fname then begin
- save_params loc args fenv
- end;
- (* Handle special cases of memcpy and memset *)
- call_memcpy loc args fname fenv;
- call_memset loc args fname fenv;
- let alloc = is_alloc fname || not (has_fundef fname) in
- Extlib.may
- (fun lhs ->
- if must_model_lval lhs !fenv then call_with_ret ~alloc loc lhs fenv)
- ret
+ (* Push parameters with either a call to a function pointer or a function
+ definition otherwise there is no point. *)
+ if Cil.isFunctionType (Cil.typeOf fname) || has_fundef fname then begin
+ save_params loc args fenv
+ end;
+ (* Handle special cases of memcpy/memset *)
+ call_memxxx loc args fname fenv;
+ let alloc = is_alloc fname || not (has_fundef fname) in
+ Extlib.may
+ (fun lhs ->
+ if must_model_lval lhs !fenv then call_with_ret ~alloc loc lhs fenv)
+ ret
+end
(* }}} *)
(* ************************************************************************** *)
-(** {Handle Local_init instructions} {{{ *)
+(* Handle Local_init instructions {{{ *)
(* ************************************************************************** *)
-let rec handle_local_init_aux ?(offset=NoOffset) loc vi init fenv =
- match init with
- | SingleInit(exp) ->
- set_instr ~post:true loc (Var(vi), offset) exp fenv
- | CompoundInit(_, inits) ->
- List.iter
- (fun (off, init) ->
- let off = Cil.addOffset off offset in
- handle_local_init_aux ~offset:off loc vi init fenv)
- inits
-
-let handle_local_init loc vi init fenv =
- handle_local_init_aux loc vi init fenv
-
-let local_init_instr vi li loc fenv =
- match li with
- | AssignInit(init) ->
- handle_local_init loc vi init fenv
- | ConsInit(fname, args, _) ->
- let ret = Some (Var(vi), NoOffset) in
- let fname = Cil.evar ~loc fname in
- call_instr ret fname args loc fenv
-
-(* Top-level handler for Local_init instructions *)
-let local_init_instr vi li loc fenv =
- if must_model_vi vi !fenv then
- local_init_instr vi li loc fenv
+module Local_init: sig
+ (* Top-level handler for Local_init instructions *)
+ val instr: varinfo -> local_init -> location -> Env.t ref -> unit
+end = struct
+
+ let rec handle_init offset loc vi init fenv =
+ match init with
+ | SingleInit exp ->
+ set_instr ~post:true loc (Var vi, offset) exp fenv
+ | CompoundInit(_, inits) ->
+ List.iter
+ (fun (off, init) ->
+ let offset = Cil.addOffset off offset in
+ handle_init offset loc vi init fenv)
+ inits
+
+ let instr vi li loc fenv =
+ match li with
+ | AssignInit init ->
+ handle_init NoOffset loc vi init fenv
+ | ConsInit(fname, args, _) ->
+ let ret = Some (Cil.var vi) in
+ let fname = Cil.evar ~loc fname in
+ Function_call.instr ret fname args loc fenv
+
+ let instr vi li loc fenv =
+ if must_model_vi vi !fenv then
+ instr vi li loc fenv
+end
(* }}} *)
(* ************************************************************************** *)
-(** {Track function arguments} {{{ *)
+(* Track function arguments {{{ *)
(* ************************************************************************** *)
(* Update local environment with a statement tracking temporal metadata
associated with adding a function argument to a stack frame *)
-let rec track_argument ?(typ) param index env =
+let track_argument ?(typ) param index env =
let typ = Extlib.opt_conv param.vtype typ in
- match typ with
+ match Cil.unrollType typ with
| TPtr _
| TComp _ ->
- let stmt = mk_pull_param ~loc:Location.unknown param index in
+ let stmt = Mk.pull_param ~loc:Location.unknown param index in
Env.add_stmt ~post:false env stmt
| TInt _ | TFloat _ | TEnum _ | TBuiltin_va_list _ -> env
- | TNamed(info, _) ->
- track_argument ~typ:info.ttype param index env
- | _ -> failwith "Failed to handle function parameter"
+ | TNamed _ -> assert false
+ | TVoid _ |TArray _ | TFun _ ->
+ Options.fatal "Failed to handle function parameter"
(* }}} *)
(* ************************************************************************** *)
-(** {Handle return statements} {{{ *)
+(* Handle return statements {{{ *)
(* ************************************************************************** *)
(* Update local environment [fenv] with statements tracking return value
of a function. *)
let handle_return_stmt loc ret fenv =
match ret.enode with
- | Lval(lv) ->
+ | Lval lv ->
if Cil.isPointerType (Cil.typeOfLval lv) then begin
let exp = Cil.mkAddrOf ~loc lv in
- let stmt = mk_handle_return_referent ~loc ~save:true exp in
+ let stmt = Mk.handle_return_referent ~loc ~save:true exp in
fenv := Env.add_stmt ~post:false !fenv stmt
end
- | _ -> failwith "Something other than Lval in return"
+ | _ -> Options.fatal "Something other than Lval in return"
let handle_return_stmt loc ret fenv =
if must_model_exp ret !fenv then
handle_return_stmt loc ret fenv
+(* }}} *)
(* ************************************************************************** *)
-(** {Handle instructions} {{{ *)
+(* Handle instructions {{{ *)
(* ************************************************************************** *)
(* Update local environment [fenv] with statements tracking
@@ -436,68 +456,70 @@ let handle_instruction instr fenv =
| Set(lv, exp, loc) ->
set_instr loc lv exp fenv
| Call(ret, fname, args, loc) ->
- call_instr ret fname args loc fenv
+ Function_call.instr ret fname args loc fenv
| Local_init(vi, li, loc) ->
- local_init_instr vi li loc fenv
- | Asm _ | Skip _ -> ()
- | Code_annot _ -> failwith "Code_annot is not supported"
-
+ Local_init.instr vi li loc fenv
+ | Asm _ -> Options.warning ~once:true ~current:true "@[Analysis is\
+potentially incorrect in presence of assembly code.@]";
+ | Skip _ -> ()
+ | Code_annot _ -> ()
+(* }}} *)
(* ************************************************************************** *)
-(** {Initialization of globals} {{{ *)
+(* Initialization of globals {{{ *)
(* ************************************************************************** *)
+
(* Provided that [vi] is a global variable initialized by the initializer [init]
at offset [off] return [Some stmt], where [stmt] is a statement
tracking that initialization. If [init] does not need to be tracked than
the return value is [None] *)
-let mk_global_init vi off init env =
+let mk_global_init ~loc vi off init env =
let exp = match init with
- | SingleInit(e) -> e
+ | SingleInit e -> e
(* Compound initializers should have been thrown away at this point *)
- | _ -> failwith "Unexpected ComppoundInit in global initializer"
+ | _ -> Options.fatal "Unexpected ComppoundInit in global initializer"
in
(* Initializer expression can be a literal string, so look up the
corresponding variable which that literal string has been converted to *)
- let exp = (try
- let rec get_string e = match e.enode with
+ let exp =
+ try let rec get_string e = match e.enode with
| Const(CStr str) -> str
| CastE(_, exp) -> get_string exp
| _ -> raise Not_found
in
let str = get_string exp in
- Cil.evar ~loc:Location.unknown (Literal_strings.find str)
+ Cil.evar ~loc (Literal_strings.find str)
with
(* Not a literal string: just use the expression at hand *)
- Not_found -> exp)
+ Not_found -> exp
in
(* The input [vi] is from the old project, so get the corresponding variable
from the new one, otherwise AST integrity is violated *)
let vi = Cil.get_varinfo (Env.get_behavior env) vi in
- let lv = (Var(vi), off) in
- mk_stmt_from_assign Location.unknown lv exp
+ let lv = Var vi, off in
+ mk_stmt_from_assign loc lv exp
+(* }}} *)
(* ************************************************************************** *)
-(** {Public API} {{{ *)
+(* Public API {{{ *)
(* ************************************************************************** *)
-let enable param =
- generate := param
+let enable param = generate := param
-let is_enabled () =
- !generate
+let is_enabled () = !generate
let handle_arguments kf env =
if is_enabled () then
- let getpar = Cil.get_varinfo (Env.get_behavior env) in
- let formals = List.map getpar (Kernel_function.get_formals kf) in
let env, _ = List.fold_left
(fun (env, index) param ->
- if Mmodel_analysis.must_model_vi ~kf param then
- track_argument param index env, index + 1
- else
- env, index + 1)
+ let param = Cil.get_varinfo (Env.get_behavior env) param in
+ let env =
+ if Mmodel_analysis.must_model_vi ~kf param then
+ track_argument param index env
+ else env
+ in env, index + 1)
(env, 0)
- formals
+ (Kernel_function.get_formals kf)
in env
else
env
@@ -507,11 +529,13 @@ let handle_stmt stmt env =
current_stmt := stmt;
let fenv = ref env in
(match stmt.skind with
- | Instr(instr) ->
+ | Instr instr ->
handle_instruction instr fenv
| Return(ret, loc) ->
Extlib.may (fun ret -> handle_return_stmt loc ret fenv) ret
- | _ -> ());
+ | Goto _ | Break _ | Continue _ | If _ | Switch _ | Loop _ | Block _
+ | UnspecifiedSequence _ | Throw _ | TryCatch _ | TryFinally _
+ | TryExcept _ -> ());
current_stmt := Cil.dummyStmt;
!fenv
end else
@@ -519,8 +543,7 @@ let handle_stmt stmt env =
let handle_global_init vi off init env =
if is_enabled () then
- mk_global_init vi off init env
+ mk_global_init ~loc:vi.vdecl vi off init env
else
None
-
(* }}} *)
diff --git a/src/plugins/e-acsl/temporal.mli b/src/plugins/e-acsl/temporal.mli
index 9225abf9c37..de424624f3c 100644
--- a/src/plugins/e-acsl/temporal.mli
+++ b/src/plugins/e-acsl/temporal.mli
@@ -20,6 +20,12 @@
(* *)
(**************************************************************************)
+(** Transformations to detect temporal memory errors (e.g., derererence of
+ stale pointers). Detailed description of the transformations is presented
+ in Sections 2 and 3 of the RV'17 paper "Runtime Detection of Temporal Memory
+ Errors" by K. Vorobyov, N. Kosmatov, J Signoles and A. Jakobsson.
+*)
+
val enable: bool -> unit
(** Enable/disable temporal transformations *)
@@ -28,7 +34,10 @@ val is_enabled: unit -> bool
val handle_arguments: Cil_types.kernel_function -> Env.t -> Env.t
(** Update local environment ([Env.t]) with statements allowing to track
- referent numbers across function calls *)
+ referent numbers across calls function whose definitions are available.
+ This is such that whenever a function [f] is called (and a new stack
+ frame is created) [handle_arguments] generates statements that transfer
+ referent numbers stored in RTL to the new stack frame. *)
val handle_stmt: Cil_types.stmt -> Env.t -> Env.t
(** Update local environment ([Env.t]) with statements tracking temporal
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
new file mode 100644
index 00000000000..079bed7a282
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle/gen_t_addr-by-val.c
@@ -0,0 +1,36 @@
+/* Generated by Frama-C */
+#include "stdint.h"
+#include "stdlib.h"
+int main(int argc, char **argv)
+{
+ int __retres;
+ char *p;
+ int *q;
+ __e_acsl_memory_init(& argc,& argv,(size_t)8);
+ __e_acsl_store_block((void *)(& q),(size_t)8);
+ __e_acsl_store_block((void *)(& p),(size_t)8);
+ uintptr_t addr = (unsigned long)(& argc);
+ __e_acsl_store_block((void *)(& addr),(size_t)8);
+ __e_acsl_full_init((void *)(& addr));
+ __e_acsl_temporal_store_nblock((void *)(& q),(void *)(& argc));
+ __e_acsl_full_init((void *)(& q));
+ q = & argc;
+ __e_acsl_temporal_store_nblock((void *)(& p),(void *)((char *)addr));
+ __e_acsl_full_init((void *)(& p));
+ p = (char *)addr;
+ __e_acsl_temporal_store_nblock((void *)(& p),(void *)0x123456);
+ __e_acsl_full_init((void *)(& p));
+ p = (char *)0x123456;
+ __e_acsl_temporal_store_nreferent((void *)(& p),(void *)(& q));
+ __e_acsl_full_init((void *)(& p));
+ p = (char *)q;
+ __retres = 0;
+ __e_acsl_delete_block((void *)(& argc));
+ __e_acsl_delete_block((void *)(& q));
+ __e_acsl_delete_block((void *)(& p));
+ __e_acsl_delete_block((void *)(& addr));
+ __e_acsl_memory_clean();
+ return __retres;
+}
+
+
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.err.oracle
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
new file mode 100644
index 00000000000..efd02631129
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_addr-by-val.res.oracle
@@ -0,0 +1,2 @@
+[e-acsl] beginning translation.
+[e-acsl] translation done in project "e-acsl".
diff --git a/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c b/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
new file mode 100644
index 00000000000..562cc4e026c
--- /dev/null
+++ b/src/plugins/e-acsl/tests/temporal/t_addr-by-val.c
@@ -0,0 +1,18 @@
+/* run.config
+ COMMENT: Case when a pointer is taking address by value.
+*/
+
+#include <stdint.h>
+
+int main (int argc, char **argv) {
+ uintptr_t addr = (uintptr_t)&argc;
+ char *p;
+ int *q;
+ q = &argc;
+ /* Here the referent of p should be assigned from the value of addr */
+ p = (char*)addr;
+ p = (char*)0x123456;
+ p = (char*)q;
+}
+
+
diff --git a/src/plugins/e-acsl/visit.ml b/src/plugins/e-acsl/visit.ml
index 91a22644d4d..de3806a0d62 100644
--- a/src/plugins/e-acsl/visit.ml
+++ b/src/plugins/e-acsl/visit.ml
@@ -206,6 +206,8 @@ class e_acsl_visitor prj generate = object (self)
:: stmts)
stmts
in
+ let return =
+ Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown)) in
(* Generate init statements for temporal analysis *)
let tinit_stmts = Varinfo.Hashtbl.fold
(fun vi (off, init) acc ->
@@ -215,11 +217,9 @@ class e_acsl_visitor prj generate = object (self)
(match stmt with | Some stmt -> stmt :: acc | None -> acc)
| None -> acc)
global_vars
- []
+ [return]
in
- let return =
- Cil.mkStmt ~valid_sid:true (Return(None, Location.unknown)) in
- let stmts = stmts @ tinit_stmts @ [return] in
+ let stmts = stmts @ tinit_stmts in
(* Create a new code block with generated statements *)
let (b, env), stmts = match stmts with
| [] -> assert false
@@ -601,7 +601,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let env = Temporal.handle_stmt stmt env in
(* Add initialization statements and store_block statements stemming
from Local_init *)
- self#add_initializers stmt env kf
+ self#handle_instructions stmt env kf
else
env
in
@@ -727,47 +727,40 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
in
Cil.ChangeDoChildrenPost(stmt, mk_block)
- method private add_initializer loc ?vi lv ?(post=false) stmt env kf =
- assert generate;
- let may_safely_ignore = function
- | Var vi, NoOffset -> vi.vglob || vi.vformal
- | _ -> false
- in
- if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~kf lv then
- let before = Cil.memo_stmt self#behavior stmt in
- let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
- let new_stmt = Cil.memo_stmt self#behavior new_stmt in
- let env = Env.add_stmt ~post ~before env new_stmt in
- let env = match vi with
- | None -> env
- | Some vi ->
- let new_stmt = Project.on prj Misc.mk_store_stmt vi in
- let new_stmt = Cil.memo_stmt self#behavior new_stmt in
- Env.add_stmt ~post ~before env new_stmt
+ method private handle_instructions stmt env kf =
+ let add_initializer loc ?vi lv ?(post=false) stmt env kf =
+ assert generate;
+ let may_safely_ignore = function
+ | Var vi, NoOffset -> vi.vglob || vi.vformal
+ | _ -> false
in
- env
- else
- env
-
- method private add_initializers stmt env kf =
- let do_instr instr =
- match instr with
- | Set(lv, _, loc) ->
- self#add_initializer loc lv stmt env kf
- | Local_init(vi, _, loc) ->
- let lv = (Var(vi), NoOffset) in
- self#add_initializer loc ~vi lv ~post:true stmt env kf
- | Call (Some lv, _, _, loc) ->
- if not (Misc.is_generated_kf kf) then
- self#add_initializer loc lv ~post:false stmt env kf
- else env
- | _ -> env
+ if not (may_safely_ignore lv) && Mmodel_analysis.must_model_lval ~stmt ~kf lv then
+ let before = Cil.memo_stmt self#behavior stmt in
+ let new_stmt = Project.on prj (Misc.mk_initialize ~loc) lv in
+ let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+ let env = Env.add_stmt ~post ~before env new_stmt in
+ let env = match vi with
+ | None -> env
+ | Some vi ->
+ let new_stmt = Project.on prj Misc.mk_store_stmt vi in
+ let new_stmt = Cil.memo_stmt self#behavior new_stmt in
+ Env.add_stmt ~post ~before env new_stmt
+ in
+ env
+ else
+ env
in
match stmt.skind with
- | Instr(i) -> do_instr i
+ | Instr(Set(lv, _, loc)) -> add_initializer loc lv stmt env kf
+ | Instr(Local_init(vi, _, loc)) ->
+ let lv = (Var(vi), NoOffset) in
+ add_initializer loc ~vi lv ~post:true stmt env kf
+ | Instr(Call (Some lv, _, _, loc)) ->
+ if not (Misc.is_generated_kf kf) then
+ add_initializer loc lv ~post:false stmt env kf
+ else env
| _ -> env
-
method !vblock blk =
let handle_memory new_blk =
match new_blk.blocals with
--
GitLab