Commit 6c45c7a3 authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica
Browse files

Memory instrumentation moved in Mmodel_translate.

parent 344f786c
......@@ -78,6 +78,7 @@ PLUGIN_CMO:= local_config \
loops \
quantif \
at_with_lscope \
mmodel_translate \
translate \
temporal \
prepare_ast \
......
......@@ -306,6 +306,11 @@ let term_has_lv_from_vi t =
type pred_or_term = PoT_pred of predicate | PoT_term of term
let mk_ptr_sizeof typ loc =
match Cil.unrollType typ with
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
(*
Local Variables:
compile-command: "make"
......
......@@ -120,6 +120,10 @@ val term_has_lv_from_vi: term -> bool
type pred_or_term = PoT_pred of predicate | PoT_term of term
val mk_ptr_sizeof: typ -> location -> exp
(* [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
to a [typ] typ and returns [sizeof(typ)]. *)
(*
Local Variables:
compile-command: "make"
......
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
let predicate_to_exp_ref
: (kernel_function -> Env.t -> predicate -> exp * Env.t) ref
= Extlib.mk_fun "named_predicate_to_exp_ref"
let term_to_exp_ref
: (kernel_function -> Env.t -> term -> exp * Env.t) ref
= Extlib.mk_fun "term_to_exp_ref"
(*****************************************************************************)
(****************************** Ranges Elimination ***************************)
(*****************************************************************************)
(* We call Range Elimination the operation through which ranges are
substituted by universally quantified logic variables.
Example:
[\valid(&t[(n-1)..(n+2)][1][0..1])] can be soundly transformed into
[\forall integer q1; n-1 <= q1 <= n+2 ==>
\forall integer q2; 0 <= q2 <= 1 ==>
\valid(&t[q1][1][q2])]
However, the substition can be unsound,
in which case [Range_elimination_exception] must be raised.
Example:
[\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
since [==] refers to set equality when applied on ranges.
But Range Elimination will give a predicate equivalent to [\valid(&t[1])]
since [\forall 0 <= q1,q2 <= 2: q1==q2] is false.
Hence [Range_elimination_exception] must be raised. *)
exception Range_elimination_exception
(* Takes a [toffset] and checks whether it contains an index that is a set *)
let rec has_set_as_index = function
| TNoOffset ->
false
| TIndex(t, toffset) ->
Logic_const.is_set_type t.term_type || has_set_as_index toffset
| TModel(_, toffset) | TField(_, toffset) ->
has_set_as_index toffset
(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
Raises [Range_elimination_exception] if whether the operation is unsound or
if we don't support the construction yet. *)
let eliminate_ranges_from_index_of_term ~loc t =
match t.term_node with
| Trange(Some n1, Some n2) ->
let name = Env.Varname.get ~scope:Env.Local_block "range" in
let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
let tlv = Logic_const.tvar ~loc lv in
tlv, (n1, lv, n2)
| _ ->
raise Range_elimination_exception
(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
Raises [Range_elimination_exception], through [eliminate_ranges_from_
index_of_term], if whether the operation is unsound or
if we don't support the construction yet. *)
let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
match toffset with
| TIndex(t, toffset') ->
if Misc.is_range_free t then
let toffset', quantifiers' =
eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
in
TIndex(t, toffset'), quantifiers'
else
(* Attempt Range Elimination on [t] *)
let t1, quantifiers1 =
eliminate_ranges_from_index_of_term ~loc t
in
let toffset2, quantifiers2 =
eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
in
let toffset3 = TIndex(t1, toffset2) in
toffset3, quantifiers1 :: quantifiers2
| TNoOffset ->
toffset, quantifiers
| TModel _ ->
Error.not_yet "range elimination on TModel"
| TField _ ->
Error.not_yet "range elimination on TField"
(*****************************************************************************)
(********************** Calls without Range Elimination **********************)
(************** \base_addr, \block_length, \offset, \freeable ****************)
(*****************************************************************************)
(* \base_addr, \block_length, \offset and \freeable *)
let call ~loc kf name ctx env t =
assert (name = "base_addr" || name = "block_length"
|| name = "offset" || name ="freeable");
let term_to_exp = !term_to_exp_ref in
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let name = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) name [ e ] ])
in
res, env
(*****************************************************************************)
(************************* Calls with Range Elimination **********************)
(********************** \initialized, \valid, \valid_read ********************)
(*****************************************************************************)
(* Call to [__e_acsl_<name>] for terms of the form [p + r]
when [<name> = valid or initialized or valid_read] and
where [p] is an address and [r] a range offset *)
let call_memory_block ~loc kf name ctx env p r =
let n1, n2 = match r.term_node with
| Trange(Some n1, Some n2) ->
n1, n2
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSL"
| _ ->
assert false
in
(* s *)
let ty = match Cil.unrollType (Misc.cty p.term_type) with
| TPtr(ty, _) | TArray(ty, _, _, _) -> ty
| _ -> assert false
in
let s = Logic_const.term ~loc (TSizeOf ty) Linteger in
(* ptr *)
let typ_charptr = Cil.charPtrType in
let ptr = Logic_const.term
~loc
(TBinOp(
PlusPI,
Logic_utils.mk_cast ~loc ~force:false typ_charptr p,
Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
(Ctype typ_charptr)
in
Typing.type_term ~use_gmp_opt:false ~ctx:Typing.other ptr;
let term_to_exp = !term_to_exp_ref in
let ptr, env = term_to_exp kf (Env.rte env true) ptr in
(* size *)
let size = Logic_const.term
~loc
(TBinOp(
Mult,
s,
Logic_const.term ~loc (TBinOp(MinusA, n2, n1)) Linteger))
Linteger
in
let ctx_ity = Typing.integer_ty_of_typ ctx in
Typing.type_term ~use_gmp_opt:false ~ctx:ctx_ity size;
let ity = Typing.get_integer_ty size in
if ity = Typing.gmp then Error.not_yet "size of memory area in GMP";
let size, env = term_to_exp kf env size in
let size = Cil.constFold false size in
(* base and base_addr *)
let base, _ = Misc.ptr_index ~loc ptr in
let base_addr = match base.enode with
| AddrOf _ | Const _ -> Cil.zero ~loc
| Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
(* generating env *)
let _, e, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let fname = Functions.RTL.mk_api_name name in
let args = match name with
| "valid" | "valid_read" -> [ ptr; size; base; base_addr ]
| "initialized" -> [ ptr; size ]
| _ -> Error.not_yet ("builtin " ^ name)
in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
e, env
(* [call_with_ranges] handles ranges in [t] when calling builtin [name].
It only supports the following cases for the time being:
A: [\builtin(p+r)] where [p] is an address and [r] a range or
[\builtin(t[r])] or
[\builtin(t[i_1]...[i_n])] where [t] is dynamically allocated
and all the indexes are integers,
except the last one which is a range
The generated code is a SINGLE call to the corresponding E-ACSL builtin
B: [\builtin(t[i_1]...[i_n])] where [t] is NOT dynamically allocated
and the indexes are integers or ranges
The generated code is a SET OF calls to the corresponding E-ACSL builtin
C: Any other use of ranges/No range
Call [call_default] which performs the translation for
range free terms, and raises Not_yet if it ever encouters a range.
Example for case:
A: [\valid(&t[3..5])]
Contiguous locations -> a single call to [__e_acsl_valid]
B: [\valid(&t[4][3..5][2])]
NON-contiguous locations -> multiple calls (3) to [__e_acsl_valid] *)
let call_with_ranges ~loc kf name ctx env t call_default =
if Misc.is_bitfield_pointers t.term_type then
Error.not_yet "bitfield pointer";
match t.term_node with
| TBinOp((PlusPI | IndexPI), p, ({ term_node = Trange _ } as r)) ->
if Misc.is_set_of_ptr_or_array p.term_type then
Error.not_yet "arithmetic over set of pointers or arrays"
else
(* Case A *)
call_memory_block ~loc kf name ctx env p r
| TAddrOf(TVar lv, TIndex({ term_node = Trange _ } as r, TNoOffset)) ->
(* Case A *)
assert (Logic_const.is_set_type t.term_type);
let lty_noset = Logic_const.type_of_element t.term_type in
let p = Logic_const.taddrof ~loc (TVar lv, TNoOffset) lty_noset in
call_memory_block ~loc kf name ctx env p r
| TAddrOf(TVar ({ lv_type = Ctype (TArray _) } as lv), toffset) ->
if has_set_as_index toffset then
(* Case B *)
try
let toffset', quantifiers =
eliminate_ranges_from_index_of_toffset ~loc toffset []
in
let lty_noset =
if Logic_const.is_set_type t.term_type then
Logic_const.type_of_element t.term_type
else
t.term_type
in
let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
let p_quantified =
(* [loc] prevents a type error with eta-expansion and label *)
let loc = Some loc in
let call f = f ?loc (Logic_const.here_label, t') in
match name with
| "valid" -> call Logic_const.pvalid
| "initialized" -> call Logic_const.pinitialized
| "valid_read" -> call Logic_const.pvalid_read
| _ -> Options.fatal "[call_with_ranges] unexpected builtin"
in
let p_quantified = List.fold_left
(fun p (tmin, lv, tmax) ->
(* \forall integer tlv; tmin <= tlv <= tmax ==> p *)
let tlv = Logic_const.tvar ~loc lv in
let lower_bound = Logic_const.prel ~loc (Rle, tmin, tlv) in
let upper_bound = Logic_const.prel ~loc (Rle, tlv, tmax) in
let bound = Logic_const.pand ~loc (lower_bound, upper_bound) in
let bound_imp_p = Logic_const.pimplies ~loc (bound, p) in
Logic_const.pforall ~loc ([lv], bound_imp_p))
p_quantified
quantifiers
in
Typing.type_named_predicate ~must_clear:true p_quantified;
let named_predicate_to_exp = !predicate_to_exp_ref in
named_predicate_to_exp kf env p_quantified
with Range_elimination_exception ->
(* Case C *)
call_default ~loc kf name ctx env t
else
(* Case C *)
call_default ~loc kf name ctx env t
| _ ->
(* Case C *)
call_default ~loc kf name ctx env t
(* \initialized *)
let call_with_size ~loc kf name ctx env t =
assert (name = "initialized");
let call_for_unsupported_constructs ~loc kf name ctx env t =
let term_to_exp = !term_to_exp_ref in
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = Misc.cty t.term_type in
let sizeof = Misc.mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env
in
call_with_ranges
~loc
kf
name
ctx
env
t
call_for_unsupported_constructs
(* \valid and \valid_read *)
let call_valid ~loc kf name ctx env t =
assert (name = "valid" || name = "valid_read");
let call_for_unsupported_constructs ~loc kf name ctx env t =
let term_to_exp = !term_to_exp_ref in
let e, env = term_to_exp kf (Env.rte env true) t in
let base, _ = Misc.ptr_index ~loc e in
let base_addr = match base.enode with
| AddrOf _ | Const _ -> Cil.zero ~loc
| Lval lv | StartOf lv -> Cil.mkAddrOrStartOf ~loc lv
| _ -> assert false
in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = Misc.cty t.term_type in
let sizeof = Misc.mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
let args = [ e; sizeof; base; base_addr ] in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname args ])
in
res, env
in
call_with_ranges
~loc
kf
name
ctx
env
t
call_for_unsupported_constructs
\ No newline at end of file
(**************************************************************************)
(* *)
(* This file is part of Frama-C. *)
(* *)
(* Copyright (C) 2007-2018 *)
(* 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). *)
(* *)
(**************************************************************************)
open Cil_types
(* Create calls to a few memory builtins.
Partial support for ranges is provided. *)
val call:
loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
exp * Env.t
(* [call ~loc kf name ctx env t] creates a call to the E-ACSL memory builtin
identified by [name] which only requires a single argument, namely the
pointer under study. The supported builtins are:
[base_addr], [block_length], [offset] and [freeable]. *)
val call_with_size:
loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
exp * Env.t
(* [call_with_size ~loc kf name ctx env t] creates a call to the E-ACSL memory
builtin identified by [name] which requires two arguments, namely
the pointer under study and a size in bytes.
The only supported builtin is: [initialized].
[t] can denote ranges of memory locations. *)
val call_valid:
loc:location -> kernel_function -> string -> typ -> Env.t -> term ->
exp * Env.t
(* [call_valid ~loc kf name ctx env t] creates a call to the E-ACSL memory
builtin [valid] or [valid_read] according to [name].
[t] can denote ranges of memory locations. *)
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
val predicate_to_exp_ref:
(kernel_function -> Env.t -> predicate -> exp * Env.t) ref
val term_to_exp_ref:
(kernel_function -> Env.t -> term -> exp * Env.t) ref
\ No newline at end of file
......@@ -39,78 +39,6 @@ let handle_error f env =
It is [true] iff we are currently visiting \valid. *)
let is_visiting_valid = ref false
(*****************************************************************************)
(*************************** Ranges in a few builtins ************************)
(*****************************************************************************)
(* We call Range Elimination the operation through which ranges are
substituted by universally quantified logic variables.
Example:
[\valid(&t[(n-1)..(n+2)][1][0..1])] can be soundly transformed into
[\forall integer q1; n-1 <= q1 <= n+2 ==>
\forall integer q2; 0 <= q2 <= 1 ==>
\valid(&t[q1][1][q2])]
However, the substition can be unsound,
in which case [Range_elimination_exception] must be raised.
Example:
[\valid(&t[(0..2)==(0..2) ? 0 : 1])] is equivalent to [\valid(&t[0])]
since [==] refers to set equality when applied on ranges.
But Range Elimination will give a predicate equivalent to [\valid(&t[1])]
since [\forall 0 <= q1,q2 <= 2: q1==q2] is false.
Hence [Range_elimination_exception] must be raised. *)
exception Range_elimination_exception
(* Takes a [toffset] and checks whether it contains an index that is a set *)
let rec has_set_as_index = function
| TNoOffset ->
false
| TIndex(t, toffset) ->
Logic_const.is_set_type t.term_type || has_set_as_index toffset
| TModel(_, toffset) | TField(_, toffset) ->
has_set_as_index toffset
(* Performs Range Elimination on index [TIndex(term, offset)]. Term part.
Raises [Range_elimination_exception] if whether the operation is unsound or
if we don't support the construction yet. *)
let eliminate_ranges_from_index_of_term ~loc t =
match t.term_node with
| Trange(Some n1, Some n2) ->
let name = Env.Varname.get ~scope:Env.Local_block "range" in
let lv = Cil_const.make_logic_var_kind name LVQuant Linteger in
let tlv = Logic_const.tvar ~loc lv in
tlv, (n1, lv, n2)
| _ ->
raise Range_elimination_exception
(* Performs Range Elimination on index [TIndex(term, offset)]. Offset part.
Raises [Range_elimination_exception], through [eliminate_ranges_from_
index_of_term], if whether the operation is unsound or
if we don't support the construction yet. *)
let rec eliminate_ranges_from_index_of_toffset ~loc toffset quantifiers =
match toffset with
| TIndex(t, toffset') ->
if Misc.is_range_free t then
let toffset', quantifiers' =
eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
in
TIndex(t, toffset'), quantifiers'
else
(* Attempt Range Elimination on [t] *)
let t1, quantifiers1 =
eliminate_ranges_from_index_of_term ~loc t
in
let toffset2, quantifiers2 =
eliminate_ranges_from_index_of_toffset ~loc toffset' quantifiers
in
let toffset3 = TIndex(t1, toffset2) in
toffset3, quantifiers1 :: quantifiers2
| TNoOffset ->
toffset, quantifiers
| TModel _ ->
Error.not_yet "range elimination on TModel"
| TField _ ->
Error.not_yet "range elimination on TField"
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
......@@ -572,15 +500,21 @@ and context_insensitive_term_to_exp kf env t =
let e, env, is_mpz_string = at_to_exp_no_lscope env (Some t) label e in
e, env, is_mpz_string, ""
| Tbase_addr(BuiltinLabel Here, t) ->
mmodel_call ~loc kf "base_addr" Cil.voidPtrType env t
let name = "base_addr" in
let e, env = Mmodel_translate.call ~loc kf name Cil.voidPtrType env t in
e, env, false, name
| Tbase_addr _ -> not_yet env "labeled \\base_addr"
| Toffset(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
mmodel_call ~loc kf "offset" size_t env t
let name = "offset" in
let e, env = Mmodel_translate.call ~loc kf name size_t env t in
e, env, false, name
| Toffset _ -> not_yet env "labeled \\offset"
| Tblock_length(BuiltinLabel Here, t) ->
let size_t = Cil.theMachine.Cil.typeOfSizeOf in
mmodel_call ~loc kf "block_length" size_t env t
let name = "block_length" in
let e, env = Mmodel_translate.call ~loc kf name size_t env t in
e, env, false, name
| Tblock_length _ -> not_yet env "labeled \\block_length"
| Tnull -> Cil.mkCast (Cil.zero ~loc) (TPtr(TVoid [], [])), env, false, "null"
| TCoerce _ -> Error.untypable "coercion" (* Jessie specific *)
......@@ -652,247 +586,6 @@ and comparison_to_exp
| Typing.C_type _ | Typing.Other ->
Cil.mkBinOp ~loc bop e1 e2, env
(* \base_addr, \block_length and \freeable annotations *)
and mmodel_call ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let name = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) name [ e ] ])
in
res, env, false, name
and get_c_term_type = function
| Ctype ty -> ty
| _ -> assert false
and mk_ptr_sizeof typ loc =
match Cil.unrollType typ with
| TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
| _ -> assert false
(* \valid, \offset and \initialized annotations *)
and mmodel_call_with_size ~loc kf name ctx env t =
let call_for_unsupported_constructs ~loc kf name ctx env t =
let e, env = term_to_exp kf (Env.rte env true) t in
let _, res, env =
Env.new_var
~loc
~name
env
None
ctx
(fun v _ ->
let ty = get_c_term_type t.term_type in
let sizeof = mk_ptr_sizeof ty loc in
let fname = Functions.RTL.mk_api_name name in
[ Misc.mk_call ~loc ~result:(Cil.var v) fname [ e; sizeof ] ])
in
res, env