Commit 7da89554 authored by Basile Desloges's avatar Basile Desloges
Browse files

[eacsl] Fix file indentations

parent 362083a7
......@@ -344,10 +344,3 @@ ML_LINT_KO+=src/plugins/variadic/standard.ml
ML_LINT_KO+=src/plugins/variadic/translate.ml
ML_LINT_KO+=src/plugins/variadic/va_build.ml
ML_LINT_KO+=src/plugins/variadic/va_types.mli
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
ML_LINT_KO+=src/plugins/e-acsl/src/analyses/rte.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.ml
ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.mli
......@@ -27,7 +27,7 @@
let warn_rte warn exn =
if warn then
Options.warning "@[@[cannot run RTE:@ %s.@]@ \
Ignoring potential runtime errors in annotations."
Ignoring potential runtime errors in annotations."
(Printexc.to_string exn)
(* ************************************************************************** *)
......@@ -45,8 +45,8 @@ let stmt ?(warn=true) =
(let module L = Datatype.List(Code_annotation) in L.ty))
with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
->
warn_rte warn exn;
fun _ _ -> []
warn_rte warn exn;
fun _ _ -> []
let exp ?(warn=true) =
try
......@@ -57,8 +57,8 @@ let exp ?(warn=true) =
(let module L = Datatype.List(Code_annotation) in L.ty))
with Failure _ | Dynamic.Unbound_value _ | Dynamic.Incompatible_type _ as exn
->
warn_rte warn exn;
fun _ _ _ -> []
warn_rte warn exn;
fun _ _ _ -> []
(*
Local Variables:
......
......@@ -39,8 +39,8 @@ let term_to_exp_ref
(*****************************************************************************)
(* Remove all the bindings for [kf]. [Cil_datatype.Kf.Hashtbl] does not
provide the [remove_all] function. Thus we need to keep calling [remove]
until all entries are removed. *)
provide the [remove_all] function. Thus we need to keep calling [remove]
until all entries are removed. *)
let rec remove_all tbl kf =
if Cil_datatype.Kf.Hashtbl.mem tbl kf then begin
Cil_datatype.Kf.Hashtbl.remove tbl kf;
......@@ -66,10 +66,10 @@ end
(**************************************************************************)
(* Builds the terms [t_size] and [t_shifted] from each
[Lvs_quantif(tmin, lv, tmax)] from [lscope]
where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
[Lvs_quantif(tmin, lv, tmax)] from [lscope]
where [t_size = tmax - tmin + (-1|0|1)] depending on whether the
inequalities are strict or large
and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
and [t_shifted = lv - tmin + (-1|0)] (so that we start indexing at 0) *)
let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
match lscope with
| [] ->
......@@ -97,29 +97,29 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
in
let iv = Interval.(extract_ival (infer t_size)) in
(* The EXACT amount of memory that is needed can be known at runtime. This
is because the tightest bounds for the variables can be known at runtime.
Example: In the following predicate
is because the tightest bounds for the variables can be known at runtime.
Example: In the following predicate
[\exists integer u; 9 <= u <= 13 &&
\forall integer v; -5 < v <= (u <= 11 ? u + 6 : u - 9) ==>
\at(u + v > 0, K)]
the upper bound [M] for [v] depends on [u].
In chronological order, [M] equals to 15, 16, 17, 3 and 4.
Thus the tightest upper bound for [v] is [max(M)=17].
HOWEVER, computing that exact information requires extra nested loops,
prior to the [malloc] stmts, that will try all the possible values of the
variables involved in the bounds.
Instead of sacrificing time over memory (by performing these extra
computations), we consider that sacrificing memory over time is more
beneficial. In particular, though we may allocate more memory than
needed, the number of reads/writes into it is the same in both cases.
Conclusion: over-approximate [t_size] *)
HOWEVER, computing that exact information requires extra nested loops,
prior to the [malloc] stmts, that will try all the possible values of the
variables involved in the bounds.
Instead of sacrificing time over memory (by performing these extra
computations), we consider that sacrificing memory over time is more
beneficial. In particular, though we may allocate more memory than
needed, the number of reads/writes into it is the same in both cases.
Conclusion: over-approximate [t_size] *)
let t_size = match Ival.min_and_max iv with
| _, Some max ->
Logic_const.tint ~loc max
| _, None ->
Error.not_yet
"\\at on purely logic variables and with quantifier that uses \
too complex bound (E-ACSL cannot infer a finite upper bound to it)"
too complex bound (E-ACSL cannot infer a finite upper bound to it)"
in
(* Index *)
let t_lv = Logic_const.tvar ~loc lv in
......@@ -148,13 +148,13 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
let size_from_sizes_and_shifts ~loc = function
| [] ->
(* No quantified variable. But still need to allocate [1*sizeof(_)] amount
of memory to store purely logic variables that are NOT quantified
(example: from \let). *)
of memory to store purely logic variables that are NOT quantified
(example: from \let). *)
Cil.lone ~loc ()
| (size, _) :: sizes_and_shifts ->
List.fold_left
(fun t_size (t_s, _) ->
Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
Logic_const.term ~loc (TBinOp(Mult, t_size, t_s)) Linteger)
size
sizes_and_shifts
......@@ -171,35 +171,35 @@ let lval_at_index ~loc kf env (e_at, vi_at, t_index) =
lval_at_index, env
(* Associate to each possible tuple of quantifiers
a unique index from the set {n | 0 <= n < n_max}.
That index will serve to identify the memory location where the evaluation
of the term/predicate is stored for the given tuple of quantifier.
The following gives the smallest set of such indexes (hence we use the
smallest amount of memory in some respect):
To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
where 0 <= t_shifted_i < beta_i
corresponds: \sum_{i=1}^n( t_shifted_i * \pi_{j=1}^{i-1}(beta_j) ) *)
a unique index from the set {n | 0 <= n < n_max}.
That index will serve to identify the memory location where the evaluation
of the term/predicate is stored for the given tuple of quantifier.
The following gives the smallest set of such indexes (hence we use the
smallest amount of memory in some respect):
To (t_shifted_n, t_shifted_n-1, ..., t_shifted_1)
where 0 <= t_shifted_i < beta_i
corresponds: \sum_{i=1}^n( t_shifted_i * \pi_{j=1}^{i-1}(beta_j) ) *)
let index_from_sizes_and_shifts ~loc sizes_and_shifts =
let product terms = List.fold_left
(fun product t ->
Logic_const.term ~loc (TBinOp(Mult, product, t)) Linteger)
(Cil.lone ~loc ())
terms
(fun product t ->
Logic_const.term ~loc (TBinOp(Mult, product, t)) Linteger)
(Cil.lone ~loc ())
terms
in
let sum, _ = List.fold_left
(fun (index, sizes) (t_size, t_shifted) ->
let pi_beta_j = product sizes in
let bi_mult_pi_beta_j =
Logic_const.term ~loc (TBinOp(Mult, t_shifted, pi_beta_j)) Linteger
in
let sum = Logic_const.term
~loc
(TBinOp(PlusA, bi_mult_pi_beta_j, index))
Linteger
in
sum, t_size :: sizes)
(Cil.lzero ~loc (), [])
sizes_and_shifts
(fun (index, sizes) (t_size, t_shifted) ->
let pi_beta_j = product sizes in
let bi_mult_pi_beta_j =
Logic_const.term ~loc (TBinOp(Mult, t_shifted, pi_beta_j)) Linteger
in
let sum = Logic_const.term
~loc
(TBinOp(PlusA, bi_mult_pi_beta_j, index))
Linteger
in
sum, t_size :: sizes)
(Cil.lzero ~loc (), [])
sizes_and_shifts
in
sum
......@@ -225,62 +225,63 @@ let to_exp ~loc kf env pot label =
in
(* Creating the pointer *)
let ty = match pot with
| Lscope.PoT_pred _ ->
Cil.intType
| Lscope.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
Typing.get_typ t
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
| Lscope.PoT_pred _ ->
Cil.intType
| Lscope.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
Typing.get_typ t
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
let ty_ptr = TPtr(ty, []) in
let vi_at, e_at, env = Env.new_var
~loc
~name:"at"
~scope:Varname.Function
env
kf
None
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_number_ty t_size with
| Typing.C_integer IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Constructor.mk_lib_call ~loc
~result:(Cil.var vi)
"malloc"
[ e_size ]
in
malloc_stmt
| Typing.(C_integer _ | C_float _ | Gmpz) ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.(Rational | Real | Nan) ->
Error.not_yet "quantification over non-integer type"
in
let free_stmt = Constructor.mk_lib_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
Thus we need to add [malloc] and [free] through dedicated functions. *)
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
~loc
~name:"at"
~scope:Varname.Function
env
kf
None
ty_ptr
(fun vi e ->
(* Handle [malloc] and [free] stmts *)
let lty_sizeof = Ctype Cil.(theMachine.typeOfSizeOf) in
let t_sizeof = Logic_const.term ~loc (TSizeOf ty) lty_sizeof in
let t_size = size_from_sizes_and_shifts ~loc sizes_and_shifts in
let t_size =
Logic_const.term ~loc (TBinOp(Mult, t_sizeof, t_size)) lty_sizeof
in
Typing.type_term ~use_gmp_opt:false t_size;
let malloc_stmt = match Typing.get_number_ty t_size with
| Typing.C_integer IInt ->
let e_size, _ = term_to_exp kf env t_size in
let e_size = Cil.constFold false e_size in
let malloc_stmt =
Constructor.mk_lib_call ~loc
~result:(Cil.var vi)
"malloc"
[ e_size ]
in
malloc_stmt
| Typing.(C_integer _ | C_float _ | Gmpz) ->
Error.not_yet
"\\at on purely logic variables that needs to allocate \
too much memory (bigger than int_max bytes)"
| Typing.(Rational | Real | Nan) ->
Error.not_yet "quantification over non-integer type"
in
let free_stmt = Constructor.mk_lib_call ~loc "free" [e] in
(* The list of stmts returned by the current closure are inserted
LOCALLY to the block where the new var is FIRST used, whatever scope
is indicated to [Env.new_var].
Thus we need to add [malloc] and [free] through dedicated functions.
*)
Malloc.add kf malloc_stmt;
Free.add kf free_stmt;
[])
in
(* Index *)
let t_index = index_from_sizes_and_shifts ~loc sizes_and_shifts in
......@@ -301,28 +302,28 @@ let to_exp ~loc kf env pot label =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
variable declarations. *)
[ Constructor.mk_block_stmt block ], env
| Lscope.PoT_term t ->
begin match Typing.get_number_ty t with
| Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, env = term_to_exp kf env t in
let e = Cil.constFold false e in
let storing_stmt =
Constructor.mk_assigns ~loc ~result:lval e
in
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Constructor.mk_block_stmt block ], env
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
| Typing.(C_integer _ | C_float _ | Nan) ->
let env = Env.push env in
let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
let e, env = term_to_exp kf env t in
let e = Cil.constFold false e in
let storing_stmt =
Constructor.mk_assigns ~loc ~result:lval e
in
let block, env =
Env.pop_and_get env storing_stmt ~global_clear:false Env.After
in
(* We CANNOT return [block.bstmts] because it does NOT contain
variable declarations. *)
[ Constructor.mk_block_stmt block ], env
| Typing.(Rational | Real) ->
Error.not_yet "\\at on purely logic variables and over real type"
| Typing.Gmpz ->
Error.not_yet "\\at on purely logic variables and over gmp type"
end
in
(* Storing loops *)
......@@ -333,10 +334,10 @@ let to_exp ~loc kf env pot label =
in
let storing_loops_block = Cil.mkBlock storing_loops_stmts in
let storing_loops_block, env = Env.pop_and_get
env
(Constructor.mk_block_stmt storing_loops_block)
~global_clear:false
Env.After
env
(Constructor.mk_block_stmt storing_loops_block)
~global_clear:false
Env.After
in
(* Put at label *)
let env = put_block_at_label env kf storing_loops_block label in
......
......@@ -24,7 +24,7 @@ open Cil_types
open Cil_datatype
(* Convert \at on terms or predicates in which we can find purely
logic variable. *)
logic variable. *)
(**************************************************************************)
(*************************** Translation **********************************)
......@@ -39,8 +39,8 @@ val to_exp:
(*****************************************************************************)
(* The different possible evaluations of the [\at] under study are
stored in a memory location that needs to be alloted then freed.
This part is designed for that purpose. *)
stored in a memory location that needs to be alloted then freed.
This part is designed for that purpose. *)
module Malloc: sig
val find_all: kernel_function -> stmt list
......
......@@ -51,9 +51,9 @@ type flow =
module Mk: sig
(* Generate either
- [store_nblock(lhs, rhs)], or
- [store_nreferent(lhs, rhs)]
function call based on the value of [flow] *)
- [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 *)
......@@ -106,8 +106,8 @@ end = struct
in
(* TODO: Returning structs is unsupported so far *)
(match (Cil.typeOf lhs) with
| TPtr _ -> ()
| _ -> Error.not_yet "Struct in return");
| TPtr _ -> ()
| _ -> Error.not_yet "Struct in return");
Constructor.mk_lib_call ~loc (RTL.mk_temporal_name fname) [ lhs ]
let reset_return_referent ~loc =
......@@ -125,10 +125,10 @@ end
(* ************************************************************************** *)
(* Given an lvalue [lhs] representing LHS of an assignment, and an expression
[rhs] representing its RHS compute 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
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 origin number of [r]
+ Copy - metadata of [r] is copied to metadata of [l] *)
......@@ -145,51 +145,52 @@ let assign ?(ltype) lhs rhs loc =
let base, _ = Misc.ptr_index rhs in
let rhs, flow =
(match base.enode with
| AddrOf _
| StartOf _ -> rhs, 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) *)
| Const _ | UnOp _ -> base, Direct
(* Special case for literal strings which E-ACSL rewrites into
global variables: take the origin number of a string *)
| Lval(Var vi, _) when RTL.is_generated_name vi.vname ->
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 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 (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 origin number *)
| BinOp(op, _, _, _) ->
(* At this point [ptr_index] should have split pointer arithmetic into
base pointer and index so there should be no pointer arithmetic
operations there. The following bit is to make sure of it. *)
(match op with
| AddrOf _
| StartOf _ -> rhs, 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) *)
| Const _ | UnOp _ -> base, Direct
(* Special case for literal strings which E-ACSL rewrites into
global variables: take the origin number of a string *)
| Lval(Var vi, _) when RTL.is_generated_name vi.vname ->
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 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 (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 origin number *)
| BinOp(op, _, _, _) ->
(* At this point [ptr_index] should have split pointer arithmetic into
base pointer and index so there should be no pointer arithmetic
operations there. The following bit is to make sure of it. *)
(match op with
| MinusPI | PlusPI | IndexPI -> assert false
| _ -> ());
base, Direct
| _ -> assert false)
base, Direct
| _ -> assert false)
in Some (lhs, rhs, flow)
| TNamed _ -> assert false
| TInt _ | TFloat _ | TEnum _ -> None
| TComp _ ->
let rhs = match rhs.enode with
| AddrOf _ -> rhs
| 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
| AddrOf _ -> rhs
| 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 *)
......@@ -240,23 +241,23 @@ end = struct
structure so they can be retrieved once that function is called *)
let save_params current_stmt loc args env kf =
let (env, _) = List.fold_left
(fun (env, index) param ->
let lv = Mem(param), NoOffset in
let ltype = Cil.typeOf param in
let vals = assign ~ltype lv param loc in
Extlib.may_map
(fun (_, rhs, flow) ->
let env =
if Mmodel_analysis.must_model_exp ~kf param then
let stmt = Mk.save_param ~loc flow rhs index in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else env
in
(env, index+1))
~dft:(env, index+1)
vals)
(env, 0)
args
(fun (env, index) param ->
let lv = Mem(param), NoOffset in
let ltype = Cil.typeOf param in
let vals = assign ~ltype lv param loc in
Extlib.may_map
(fun (_, rhs, flow) ->
let env =
if Mmodel_analysis.must_model_exp ~kf param then
let stmt = Mk.save_param ~loc flow rhs index in
Env.add_stmt ~before:current_stmt ~post:false env kf stmt
else env
in
(env, index+1))
~dft:(env, index+1)
vals)
(env, 0)
args
in env
(* Update local environment with a statement tracking temporal metadata
......@@ -282,17 +283,17 @@ end = struct
[pull_return] added via a call to [Mk.handle_return_referent] *)
Extlib.may_map
(fun (lhs, rhs, flow) ->
let flow, rhs = match flow with
| Indirect when alloc -> Direct, (Constructor.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
Env.add_stmt ~before:current_stmt ~post:true env kf stmt)
let flow, rhs = match flow with
| Indirect when alloc -> Direct, (Constructor.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
Env.add_stmt ~before:current_stmt ~post:true env kf stmt)
~dft:env
vals
......@@ -340,9 +341,9 @@ end = struct
let alloc = not has_def in
Extlib.may_map
(fun lhs ->
if Mmodel_analysis.must_model_lval ~kf lhs then
call_with_ret ~alloc current_stmt loc lhs env kf
else env)
if Mmodel_analysis.must_model_lval ~kf lhs then
call_with_ret ~alloc current_stmt loc lhs env kf
else env)
~dft:env