Commit 44bcb61e authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Track variables bypassed by goto statements

parent e8f4885d
......@@ -79,8 +79,8 @@ let bypass_warning goto var =
| Goto(_, l) -> l
| _ -> assert false
in
Options.warning "Declaration of variable %s at %a is bypassed by a goto at \
%a. Execution of a monitored program will fail"
Options.warning "Declaration of local variable %s at %a is bypassed by a\
goto statement at %a"
var.vname
Printer.pp_location var.vdecl
Printer.pp_location loc
......
......@@ -39,8 +39,7 @@ val delete_vars: Cil_types.stmt -> Cil_types.varinfo list
val is_bypassed_by: Cil_types.varinfo -> Cil_types.stmt option
(** Given a variable [vi] returns a [goto] statement which bypasses the
declaration of [vi] and as a consequence misses the execution of
[store_block] instrumented immediately after the declaration. *)
declaration of [vi]. *)
val bypass_warning: Cil_types.stmt -> Cil_types.varinfo -> unit
(** Emit a warning if a given variable is bypassed by a given goto statement *)
......
......@@ -34,14 +34,14 @@ let library_files () =
"e_acsl_gmp.h";
"e_acsl_mmodel_api.h" ]
let normalized_library_files =
let normalized_library_files =
lazy (List.map Filepath.normalize (library_files ()))
let is_library_loc (loc, _) =
let is_library_loc (loc, _) =
List.mem loc.Lexing.pos_fname (Lazy.force normalized_library_files)
let library_functions = Datatype.String.Hashtbl.create 17
let register_library_function vi =
let register_library_function vi =
Datatype.String.Hashtbl.add library_functions vi.vname vi
let reset () = Datatype.String.Hashtbl.clear library_functions
......@@ -69,7 +69,7 @@ let mk_call ~loc ?result fname args =
in
let args =
List.map2
(fun (_, ty, _) arg ->
(fun (_, ty, _) arg ->
let e =
match ty, Cil.unrollType (Cil.typeOf arg), arg.enode with
| TPtr _, TArray _, Lval lv -> Cil.new_exp ~loc (StartOf lv)
......@@ -82,15 +82,15 @@ let mk_call ~loc ?result fname args =
in
Cil.mkStmtOneInstr ~valid_sid:true (Call(result, f, args, loc))
type annotation_kind =
type annotation_kind =
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
let kind_to_string loc k =
Cil.mkString
let kind_to_string loc k =
Cil.mkString
~loc
(match k with
| Assertion -> "Assertion"
......@@ -143,44 +143,44 @@ let mk_api_name fname =
e_acsl_api_prefix ^ fname
let mk_gen_name name =
e_acsl_gen_prefix ^ name
e_acsl_gen_prefix ^ name
(* Build a C conditional doing a runtime assertion check. *)
let mk_e_acsl_guard ?(reverse=false) kind kf e p =
let loc = p.pred_loc in
let msg =
let msg =
Kernel.Unicode.without_unicode
(Format.asprintf "%a@?" Printer.pp_predicate) p
(Format.asprintf "%a@?" Printer.pp_predicate) p
in
let line = (fst loc).Lexing.pos_lnum in
let e =
if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
let e =
if reverse then e else Cil.new_exp ~loc:e.eloc (UnOp(LNot, e, Cil.intType))
in
mk_call
~loc
mk_call
~loc
(mk_api_name "assert")
[ e;
kind_to_string loc kind;
Cil.mkString ~loc (get_orig_name kf);
Cil.mkString ~loc msg;
Cil.integer loc line ]
[ e;
kind_to_string loc kind;
Cil.mkString ~loc (get_orig_name kf);
Cil.mkString ~loc msg;
Cil.integer loc line ]
let mk_block prj stmt b =
let mk_block prj stmt b =
let mk b = match b.bstmts with
| [] ->
| [] ->
(match stmt.skind with
| Instr(Skip _) -> stmt
| _ -> assert false)
| [ s ] ->
if Stmt.equal stmt s then s
else
| [ s ] ->
if Stmt.equal stmt s then s
else
(* [JS 2012/10/19] this case exactly corresponds to
__e_acsl_assert(...) when the annotation is associated to a
statement <skip>. Creating a block prevents the printer to add
a stupid unintuitive block *)
Cil.mkStmt ~valid_sid:true (Block b)
| _ :: _ -> Cil.mkStmt ~valid_sid:true (Block b)
in
in
Project.on prj mk b
(* ************************************************************************** *)
......@@ -188,8 +188,8 @@ let mk_block prj stmt b =
(* ************************************************************************** *)
let result_lhost kf =
let stmt =
try Kernel_function.find_return kf
let stmt =
try Kernel_function.find_return kf
with Kernel_function.No_Statement -> assert false
in
match stmt.skind with
......@@ -206,11 +206,11 @@ let result_vi kf = match result_lhost kf with
let mk_debug_mmodel_stmt stmt =
if Options.debug_atleast 1
&& Options.is_debug_key_enabled Options.dkey_analysis
&& Options.is_debug_key_enabled Options.dkey_analysis
then
let debug = mk_call ~loc:(Stmt.loc stmt) (mk_api_name "memory_debug") [] in
Cil.mkStmt ~valid_sid:true (Block (Cil.mkBlock [ stmt; debug]))
else
else
stmt
let mk_full_init_stmt ?(addr=true) vi =
......@@ -223,21 +223,21 @@ let mk_full_init_stmt ?(addr=true) vi =
mk_debug_mmodel_stmt stmt
let mk_initialize ~loc (host, offset as lv) = match host, offset with
| Var _, NoOffset -> mk_call ~loc
| Var _, NoOffset -> mk_call ~loc
(mk_api_name "full_init")
[ Cil.mkAddrOf ~loc lv ]
| _ ->
| _ ->
let typ = Cil.typeOfLval lv in
mk_call ~loc
mk_call ~loc
(mk_api_name "initialize")
[ Cil.mkAddrOf ~loc lv; Cil.new_exp loc (SizeOf typ) ]
let mk_store_stmt ?str_size vi =
let mk_store_stmt_aux name ?str_size vi =
let ty = Cil.unrollType vi.vtype in
let loc = vi.vdecl in
let store = mk_call ~loc (mk_api_name "store_block") in
let store = mk_call ~loc (mk_api_name name) in
let stmt = match ty, str_size with
| TArray(_, Some _,_,_), None ->
| TArray(_, Some _,_,_), None ->
store [ Cil.evar ~loc vi ; Cil.sizeOf ~loc ty ]
| TPtr(TInt(IChar, _), _), Some size -> store [ Cil.evar ~loc vi ; size ]
| _, None -> store [ Cil.mkAddrOfVi vi ; Cil.sizeOf ~loc ty ]
......@@ -245,12 +245,17 @@ let mk_store_stmt ?str_size vi =
in
mk_debug_mmodel_stmt stmt
let mk_store_stmt ?str_size vi =
mk_store_stmt_aux "store_block" ?str_size vi
let mk_duplicate_store_stmt ?str_size vi =
mk_store_stmt_aux "store_block_duplicate" ?str_size vi
let mk_delete_stmt vi =
let loc = vi.vdecl in
let stmt = match Cil.unrollType vi.vtype with
| TArray(_, Some _, _, _) ->
mk_call ~loc (mk_api_name "delete_block") [ Cil.evar ~loc vi ]
(* | Tarray(_, None, _, _)*)
| _ -> mk_call ~loc (mk_api_name "delete_block") [ Cil.mkAddrOfVi vi ]
in
mk_debug_mmodel_stmt stmt
......
......@@ -38,15 +38,15 @@ val mk_call: loc:Location.t -> ?result:lval -> string -> exp list -> stmt
val mk_debug_mmodel_stmt: stmt -> stmt
type annotation_kind =
type annotation_kind =
| Assertion
| Precondition
| Postcondition
| Invariant
| RTE
val mk_e_acsl_guard:
?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
val mk_e_acsl_guard:
?reverse:bool -> annotation_kind -> kernel_function -> exp -> predicate
-> stmt
val mk_block: Project.t -> stmt -> block -> stmt
......@@ -71,6 +71,7 @@ val register_library_function: varinfo -> unit
val reset: unit -> unit
val mk_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_duplicate_store_stmt: ?str_size:exp -> varinfo -> stmt
val mk_delete_stmt: varinfo -> stmt
val mk_full_init_stmt: ?addr:bool -> varinfo -> stmt
val mk_initialize: loc:location -> lval -> stmt
......
......@@ -448,27 +448,25 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let e = Cil.visitCilExpr o e in
e, !env_ref
method private allocate_function env kf vars =
method private add_tracking_fn fn ?before env kf vars =
List.fold_left
(fun env vi ->
if generate && Mmodel_analysis.must_model_vi ~kf vi then
let vi = Cil.get_varinfo (Env.get_behavior env) vi in
Env.add_stmt env (Misc.mk_store_stmt vi)
Env.add_stmt ?before env (fn vi)
else
env)
env
vars
method private deallocate_function env kf vars =
List.fold_left
(fun env vi ->
if generate && Mmodel_analysis.must_model_vi ~kf vi then
let vi = Cil.get_varinfo (Env.get_behavior env) vi in
Env.add_stmt env (Misc.mk_delete_stmt vi)
else
env)
env
vars
method private add_store_stmt ?before env kf vars =
self#add_tracking_fn Misc.mk_store_stmt ?before env kf vars
method private add_duplicate_store_stmt ?before env kf vars =
self#add_tracking_fn Misc.mk_duplicate_store_stmt ?before env kf vars
method private add_delete_stmt ?before env kf vars =
self#add_tracking_fn Misc.mk_delete_stmt ?before env kf vars
method !vstmt_aux stmt =
Options.debug ~level:4 "proceeding stmt (sid %d) %a@."
......@@ -484,7 +482,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
if self#is_first_stmt kf stmt then
(* JS: should be done in the new project? *)
let env = if generate then
self#allocate_function env kf (Kernel_function.get_formals kf)
self#add_store_stmt env kf (Kernel_function.get_formals kf)
else
env
in
......@@ -515,6 +513,13 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(Cil.get_original_stmt self#behavior stmt)
(env, [])
in
(* Add [__e_acsl_store_duplicate] calls for local variables which
* declarations are bypassed by gotos. Note: should be done before
* [vinst] method (which adds initializers) is executed, otherwise
* init calls appear before store calls. *)
let duplicates = (Exit_points.store_vars stmt) in
let env = self#add_duplicate_store_stmt ~before:stmt env kf duplicates in
function_env := env;
let mk_block stmt =
......@@ -546,7 +551,7 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
let new_stmt, env =
(* Remove local variables which scopes ended via goto/break/continue. *)
let del_vars = Exit_points.delete_vars stmt in
let env = self#deallocate_function env kf del_vars in
let env = self#add_delete_stmt ~before:stmt env kf del_vars in
if self#is_return kf stmt then
(* must generate the post_block before including [stmt] (the 'return')
since no code is executed after it. However, since this statement
......@@ -565,9 +570,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
(* de-allocating memory previously allocating by the kf *)
(* JS: should be done in the new project? *)
if generate then
(* Remove recorded function argument *)
(* Remove recorded function arguments *)
let fargs = (Kernel_function.get_formals kf) in
let env = self#deallocate_function env kf fargs in
let env = self#add_delete_stmt env kf fargs in
let b, env =
Env.pop_and_get env new_stmt ~global_clear:true Env.After
in
......
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