Commit 07718350 authored by Fonenantsoa Maurica 's avatar Fonenantsoa Maurica
Browse files

Addresses Julien's review no.1:

- Interval inference and typing
- Multi-dimensional arrays with ranges as indexes:
  - If the only range is the last index -> single call to builtin
  - Else -> not yet "arithmetic over set of pointers" (requires Mmodel modification)
- Tests for struct
- Richer pattern matching instead of is_trange
- has_range -> Misc.is_range_free
- Using Cil_const.make_logic_var_kind, Logic_const.taddrof, Logic_const.type_of_element and Logic_utils.mk_cast
- [elt] @ list -> elt :: list
- Options.fatal -> Options.abort
- Comments:
  - On the Range Elimination operation
  - Describing the formula for the range-free term
  - Describing mmodel_call_with_ranges and mmodel_call_default
parent 1e6d9642
......@@ -190,7 +190,12 @@ let rec infer t =
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
| Trange (_,_) -> Ival.inject_range None None
| Trange(Some n1, Some n2) ->
let i1 = infer n1 in
let i2 = infer n2 in
Ival.join i1 i2
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSl"
| Tlet (li,t) ->
let li_t = Misc.term_of_li li in
......
......@@ -250,6 +250,28 @@ let term_of_li li = match li.l_body with
| LBterm t -> t
| LBnone | LBreads _ | LBpred _ | LBinductive _ ->
Options.fatal "li.l_body does not match LBterm(t) in Misc.term_of_li"
let is_set_of_ptr_or_array lty =
try
let lty = Logic_const.type_of_element lty in
(Logic_utils.isLogicPointerType lty) || (Logic_utils.isLogicArrayType lty)
with Failure _ ->
false
let is_range_free t =
let res_ref = ref true in
let has_range_visitor = object inherit Visitor.frama_c_inplace
method !vterm t = match t.term_node with
| Trange _ ->
res_ref := false;
Cil.SkipChildren
| _ ->
Cil.DoChildren
end
in
ignore (Visitor.visitFramacTerm has_range_visitor t);
!res_ref
(*
Local Variables:
compile-command: "make"
......
......@@ -104,6 +104,12 @@ val term_of_li: logic_info -> term
(* [term_of_li li] assumes that [li.l_body] matches [LBterm t]
and returns [t]. *)
val is_set_of_ptr_or_array: logic_type -> bool
(* Checks whehter the given logic type is a set of pointers. *)
val is_range_free: term -> bool
(* Returns [true] iff the given term does not contain any range. *)
(*
Local Variables:
compile-command: "make"
......
......@@ -302,7 +302,15 @@ module rec Transfer
| _ ->
match t2.term_type with
| Ctype ty when is_ptr_or_array ty -> register_term kf varinfos t2
| _ -> assert false)
| _ ->
if (Misc.is_set_of_ptr_or_array t1.term_type) ||
(Misc.is_set_of_ptr_or_array t2.term_type) then
(* Occurs for example from:
\valid(&multi_dynamic[2..4][1..7])
where multi_dynamic has been dynamically allocated *)
Error.not_yet "arithmetic over set of pointers or arrays"
else
assert false)
| TConst _ | TSizeOf _ | TSizeOfE _ | TSizeOfStr _ | TAlignOf _
| TAlignOfE _ | Tnull | Ttype _ | TUnOp _ | TBinOp _ ->
varinfos
......
/* Generated by Frama-C */
#include "stdio.h"
#include "stdlib.h"
struct S {
int a[2] ;
float *b ;
float *c ;
};
int main(void)
{
int __retres;
......@@ -8,7 +13,12 @@ int main(void)
char *b;
double t2[4];
float t3[7][2][4];
struct S s;
int **multi_dynamic;
int i;
__e_acsl_memory_init((int *)0,(char ***)0,(size_t)8);
__e_acsl_store_block((void *)(& multi_dynamic),(size_t)8);
__e_acsl_store_block((void *)(& s),(size_t)24);
__e_acsl_store_block((void *)(t3),(size_t)224);
__e_acsl_store_block((void *)(t2),(size_t)32);
__e_acsl_store_block((void *)(& b),(size_t)8);
......@@ -190,7 +200,68 @@ int main(void)
__e_acsl_assert(__gen_e_acsl_forall_3,(char *)"Assertion",(char *)"main",
(char *)"\\valid_read(&t3[n - 1 .. n + 2][1])",42);
}
__e_acsl_initialize((void *)(& s.a[0]),sizeof(int));
s.a[0] = 7;
__e_acsl_initialize((void *)(& s.a[1]),sizeof(int));
s.a[1] = 8;
/*@ assert \initialized(&s.a[0] + (1 .. 2)); */
{
int __gen_e_acsl_initialized_5;
__gen_e_acsl_initialized_5 = __e_acsl_initialized((void *)((char *)(& s.a[0]) +
4 * 1),
(size_t)4);
__e_acsl_assert(__gen_e_acsl_initialized_5,(char *)"Assertion",
(char *)"main",
(char *)"\\initialized(&s.a[0] + (1 .. 2))",46);
}
/*@ assert ¬\initialized(s.b + (0 .. 1)); */
{
int __gen_e_acsl_initialized_6;
__gen_e_acsl_initialized_6 = __e_acsl_initialized((void *)((char *)s.b +
4 * 0),
(size_t)4);
__e_acsl_assert(! __gen_e_acsl_initialized_6,(char *)"Assertion",
(char *)"main",(char *)"!\\initialized(s.b + (0 .. 1))",
47);
}
int size1 = 5;
int size2 = 9;
__e_acsl_full_init((void *)(& multi_dynamic));
multi_dynamic = (int **)malloc((unsigned long)size1 * sizeof(*multi_dynamic));
i = 0;
while (i < size1) {
__e_acsl_initialize((void *)(multi_dynamic + i),sizeof(int *));
*(multi_dynamic + i) = (int *)malloc((unsigned long)size2 * sizeof(*(*(
multi_dynamic + i))));
i ++;
}
/*@ assert \valid(*(multi_dynamic + 4) + (1 .. 7)); */
{
int __gen_e_acsl_valid_read_3;
int __gen_e_acsl_valid_8;
__gen_e_acsl_valid_read_3 = __e_acsl_valid_read((void *)(multi_dynamic + 4),
sizeof(int *),
(void *)multi_dynamic,
(void *)(& multi_dynamic));
__e_acsl_assert(__gen_e_acsl_valid_read_3,(char *)"RTE",(char *)"main",
(char *)"mem_access: \\valid_read(multi_dynamic + 4)",56);
__gen_e_acsl_valid_8 = __e_acsl_valid((void *)((char *)*(multi_dynamic + 4) +
4 * 1),(size_t)24,
(void *)*(multi_dynamic + 4),
(void *)(multi_dynamic + 4));
__e_acsl_assert(__gen_e_acsl_valid_8,(char *)"Assertion",(char *)"main",
(char *)"\\valid(*(multi_dynamic + 4) + (1 .. 7))",56);
}
/*@ assert \valid(*(multi_dynamic + (2 .. 4)) + (1 .. 7)); */ ;
i --;
while (i >= 0) {
free((void *)*(multi_dynamic + i));
i --;
}
free((void *)multi_dynamic);
__retres = 0;
__e_acsl_delete_block((void *)(& multi_dynamic));
__e_acsl_delete_block((void *)(& s));
__e_acsl_delete_block((void *)(t3));
__e_acsl_delete_block((void *)(t2));
__e_acsl_delete_block((void *)(t));
......
[e-acsl] beginning translation.
[e-acsl] tests/runtime/ranges_in_builtins.c:57: Warning:
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
Ignoring annotation.
[e-acsl] tests/runtime/ranges_in_builtins.c:57: Warning:
E-ACSL construct `arithmetic over set of pointers or arrays'
is not yet supported.
Ignoring annotation.
[e-acsl] translation done in project "e-acsl".
[eva:alarm] tests/runtime/ranges_in_builtins.c:13: Warning:
assertion got status unknown.
......
......@@ -6,7 +6,7 @@
extern void *malloc(size_t p);
extern void free(void* p);
struct S { int a[2]; float *b; float *c;};
int main(void) {
int *a;
a = malloc(10*sizeof(int));
......@@ -40,4 +40,24 @@ int main(void) {
/*@ assert !\valid_read(&t3[6][1][0] + (2..10)); */
/*@ assert \valid_read(&t3[(n-1)..(n+2)][1]); */
struct S s;
s.a[0] = 7; s.a[1] = 8;
/*@ assert \initialized(&s.a[0] + (1..2)); */ ;
/*@ assert !\initialized(s.b + (0..1)); */ ;
int **multi_dynamic;
int size1 = 5, size2 = 9;
multi_dynamic = malloc(size1 * sizeof(*multi_dynamic));
int i;
for(i = 0; i < size1; i++) {
multi_dynamic[i] = malloc(size2 * sizeof(*(multi_dynamic[i])));
}
/*@ assert \valid(&multi_dynamic[4][1..7]); */ // single call to builtin
/*@ assert \valid(&multi_dynamic[2..4][1..7]); */ // need to modify Mmodel
// => not_yet
for(i = i-1 ; i >= 0 ; i--) {
free(multi_dynamic[i]);
}
free(multi_dynamic);
}
\ No newline at end of file
......@@ -224,6 +224,21 @@ let cast_integer_to_float lty lty_t e =
else
e
(* 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 [RangeEliminationException] 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 [RangeEliminationException] must be raised. *)
exception RangeEliminationException
let rec thost_to_host kf env = function
......@@ -413,6 +428,9 @@ and context_insensitive_term_to_exp kf env t =
(* other logic/arith operators *)
not_yet env "missing binary bitwise operator"
| TBinOp(PlusPI | IndexPI | MinusPI | MinusPP as bop, t1, t2) ->
if (Misc.is_set_of_ptr_or_array t1.term_type) ||
(Misc.is_set_of_ptr_or_array t2.term_type) then
Error.not_yet "arithmetic over set of pointers or arrays";
(* binary operation over pointers *)
let ty = match t1.term_type with
| Ctype ty -> ty
......@@ -628,75 +646,117 @@ and mmodel_call_valid ~loc kf name ctx env t =
res, env
end
(* [mmodel_call_with_ranges] attempts to handle ranges in [t]
when calling builtin [name].
[mmodel_call_with_ranges] supports the following cases:
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 all the indexes are integers,
except the last one which is a range,
and [t] is dynamically allocated
The generated code is a SINGLE call to the corresponding E-ACSL builtin
B: [\builtin(t[i_1]...[i_n])] where the indexes are integers or ranges
and [t] is NOT dynamically allocated
The generated code is a SET OF calls to the corresponding E-ACSL builtin
C: Default case/Unsupported cases
[mmodel_call_with_ranges] will simply make E-ACSL behave as before
through [mmodel_call_default] for soundness and
for backward compatibility *)
and mmodel_call_with_ranges ~loc kf name ctx env t mmodel_call_default =
match t.term_node with
| TAddrOf(TVar lv, TIndex(r, TNoOffset)) when is_trange r ->
let p = Logic_const.term
~loc
(TAddrOf(TVar lv, TIndex(Logic_const.tinteger ~loc 0, TNoOffset)))
lv.lv_type
in
mmodel_call_memory_block ~loc kf name ctx env p r
| TBinOp(PlusPI, p, r) when Logic_utils.isLogicPointer p && is_trange r ->
mmodel_call_memory_block ~loc kf name ctx env p r
| TAddrOf(TVar lv, toffset)
when is_offset_of_array toffset && has_range t ->
begin try
let toffset', quantifiers =
eliminate_ranges_from_offset_of_array ~loc toffset []
in
let lty_noset = match t.term_type with
(* Now that ranges are eliminated, the type of the term is changed
from set<lty> to lty *)
| Ltype(lti, [lty]) when lti.lt_name = "set" ->
lty
| Ltype _ | Ctype _ | Linteger | Lreal | Larrow _ | Lvar _ as lty ->
lty
in
let t' = Logic_const.term
~loc
(TAddrOf(TVar lv, toffset'))
lty_noset
in
let p_quantified = match name with
| "valid" ->
Logic_const.pvalid ~loc (Logic_const.here_label, t')
| "initialized" ->
Logic_const.pinitialized ~loc (Logic_const.here_label, t')
| "valid_read" ->
Logic_const.pvalid_read ~loc (Logic_const.here_label, t')
| _ as s ->
Options.fatal "unexpected builtin %s during range elimination" s;
in
let p_quantified = List.fold_left
(fun p (tmin, lv, tmax) ->
let tlv = Logic_const.tvar ~loc lv in
let bound1 = Logic_const.prel ~loc (Rle, tmin, tlv) in
let bound2 = Logic_const.prel ~loc (Rle, tlv, tmax) in
let bound = Logic_const.pand ~loc (bound1, bound2) 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 e, env = named_predicate_to_exp kf env p_quantified in
e, env
with RangeEliminationException ->
| TAddrOf(thost, toffset) ->
begin match thost, toffset with
| TVar lv, TIndex(r, TNoOffset) ->
begin match r.term_node with
| Trange _ ->
(* Case A *)
let lty_noset =
try Logic_const.type_of_element t.term_type
with Failure _ -> assert false (* due to the range *)
in
let p = Logic_const.term
~loc
(TAddrOf(TVar lv, TIndex(Logic_const.tinteger ~loc 0, TNoOffset)))
lty_noset
in
mmodel_call_memory_block ~loc kf name ctx env p r
| _ ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
end
| TVar lv, toffset ->
if is_offset_of_array toffset && not (Misc.is_range_free t) then
(* Case B *)
begin try
let toffset', quantifiers =
eliminate_ranges_from_index_offset_of_array ~loc toffset []
in
let lty_noset =
try Logic_const.type_of_element t.term_type
with Failure _ -> t.term_type
in
let t' = Logic_const.taddrof ~loc (TVar lv, toffset') lty_noset in
let p_quantified = match name with
| "valid" ->
Logic_const.pvalid ~loc (Logic_const.here_label, t')
| "initialized" ->
Logic_const.pinitialized ~loc (Logic_const.here_label, t')
| "valid_read" ->
Logic_const.pvalid_read ~loc (Logic_const.here_label, t')
| _ as s ->
Options.fatal "unexpected builtin %s during range elimination" s
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 bound1 = Logic_const.prel ~loc (Rle, tmin, tlv) in
let bound2 = Logic_const.prel ~loc (Rle, tlv, tmax) in
let bound = Logic_const.pand ~loc (bound1, bound2) 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 e, env = named_predicate_to_exp kf env p_quantified in
e, env
with RangeEliminationException ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
end
else
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
| (TMem _ | TResult _), (TIndex _ | _) ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
end
| TBinOp((PlusPI | IndexPI), p, r) ->
begin match r.term_node with
| Trange _ ->
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 *)
mmodel_call_memory_block ~loc kf name ctx env p r
| _ ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
end
| _ ->
(* Case C *)
mmodel_call_default ~loc kf name ctx env t
(* Call to [__e_acsl_<name>] for term of the form [p + r]
when [<name> = valid or initialized or valid_read] and
where [p] is an address, [r] a range offset *)
and mmodel_call_memory_block ~loc kf name ctx env p r =
(* Call to [__e_acsl_<name>] for term of the form [p + r]
when [<name> = valid or initialized or valid_read] and
where [p] is an address, [r] a range offset *)
let n1, n2 = match r.term_node with
| Trange(Some n1, Some n2) ->
n1, n2
| Trange(None, _) | Trange(_, None) ->
Options.fatal "unbounded ranges are not part of E-ACSL"
Options.abort "unbounded ranges are not part of E-ACSL"
| _ ->
assert false
in
......@@ -712,7 +772,7 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
~loc
(TBinOp(
PlusPI,
Logic_const.term ~loc (TCastE(typ_charptr, p)) (Ctype typ_charptr),
Logic_utils.mk_cast ~loc ~force:false typ_charptr p,
Logic_const.term ~loc (TBinOp(Mult, s, n1)) Linteger))
(Ctype typ_charptr)
in
......@@ -757,86 +817,68 @@ and mmodel_call_memory_block ~loc kf name ctx env p r =
in
res, env
and is_trange t = match t.term_node with
| Trange _ -> true
| _ -> false
(* [is_offset_of_array toff] returns [true] if [toff] if the offset of a
multi-dimensional array. Returns [false] otherwise *)
and is_offset_of_array toffset = match toffset with
(* [true] if multi-dimensional array, false otherwise *)
| TIndex(_, TNoOffset) -> true
| TIndex(_, toffset) -> is_offset_of_array toffset
| _ -> false
| TNoOffset | TModel _ | TField _ -> false
and eliminate_ranges_from_offset_of_array ~loc toffset quantifiers =
(* Performs Range Elimination on index [TIndex(term, offset)]
of (multi-dimensional) array. Offset part.
Raises [RangeEliminationException], through [eliminate_ranges_from_
index_term_of_array], if whether the operation is unsound or
if we don't support the construction yet. *)
and eliminate_ranges_from_index_offset_of_array ~loc toffset quantifiers =
assert(is_offset_of_array toffset);
match toffset with
| TIndex(t, TNoOffset) when not (has_range t) ->
toffset, quantifiers
| TIndex(t, toffset') when not (has_range t) ->
let toffset', quantifiers' =
eliminate_ranges_from_offset_of_array ~loc toffset' quantifiers
in
TIndex(t, toffset'), quantifiers'
| TIndex(t, TNoOffset) when has_range t ->
let t', q = eliminate_ranges_from_term ~loc t in
TIndex(t', TNoOffset), q :: quantifiers
| TIndex(t, toffset') when has_range t ->
let t1, quantifiers1 = eliminate_ranges_from_term ~loc t in
let toffset2, quantifiers2 =
eliminate_ranges_from_offset_of_array ~loc toffset' quantifiers
in
let toffset3 = TIndex(t1, toffset2) in
toffset3, [quantifiers1] @ quantifiers2
| _ ->
| TIndex(t, TNoOffset) ->
if Misc.is_range_free t then
toffset, quantifiers
else
(* Attempt Range Elimination on [t] *)
let t', q = eliminate_ranges_from_index_term_of_array ~loc t in
TIndex(t', TNoOffset), q :: quantifiers
| TIndex(t, toffset') ->
if Misc.is_range_free t then
let toffset', quantifiers' =
eliminate_ranges_from_index_offset_of_array ~loc toffset' quantifiers
in
TIndex(t, toffset'), quantifiers'
else
(* Attempt Range Elimination on [t] *)
let t1, quantifiers1 = eliminate_ranges_from_index_term_of_array ~loc t in
let toffset2, quantifiers2 =
eliminate_ranges_from_index_offset_of_array ~loc toffset' quantifiers
in
let toffset3 = TIndex(t1, toffset2) in
toffset3, quantifiers1 :: quantifiers2
| TNoOffset | TModel _ | TField _ ->
assert false
and has_range t =
let has_range_visitor = object(self) inherit Visitor.frama_c_inplace
val mutable has_range = false
method !vterm t = match t.term_node with
| Trange _ ->
has_range <- true;
Cil.SkipChildren
| _ ->
Cil.DoChildren
method visit t =
ignore (Visitor.visitFramacTerm (self :> Visitor.frama_c_inplace) t);
has_range
end
in
has_range_visitor#visit t
and eliminate_ranges_from_term ~loc t: term * (term * logic_var * term) =
(* Performs Range Elimination on index [TIndex(term, offset)]
of (multi-dimensional) array. Term part.
Raises [RangeEliminationException] if whether the operation is unsound or
if we don't support the construction yet. *)
and eliminate_ranges_from_index_term_of_array ~loc t =
match t.term_node with
| Trange(Some _, Some _) ->
let n1, lv, n2 = bounded_lv_of_range t in
| 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)
| TBinOp(PlusA, _, r) when is_trange r ->
(* t[n + (0..3)] results in a typing error:
| TBinOp(PlusA, _, r) ->
begin match r.term_node with
| Trange _ ->
(* t[n + (0..3)] results in a typing error:
arithmetic conversion between non arithmetic types int and set<ℤ> *)
assert false
assert false
| _ ->
raise RangeEliminationException
end
| _ ->
raise RangeEliminationException
and bounded_lv_of_range t =
match t.term_node with
| Trange(Some n1, Some n2) ->
let id = Cil_const.new_raw_id () in
let name = Env.Varname.get ~scope:Env.Local_block "range" in
let lv = {
lv_name = name;
lv_id = id;
lv_type = Linteger;
lv_kind = LVQuant;
lv_origin = None;
lv_attr = []
}
in
n1, lv, n2
| _ ->
assert false
and at_to_exp env t_opt label e =
let stmt = E_acsl_label.get_stmt (Env.get_visitor env) label in
(* generate a new variable denoting [\at(t',label)].
......
......@@ -474,7 +474,14 @@ let rec type_term ~use_gmp_opt ?(arith_operand=false) ?ctx t =
| Tunion _ -> Error.not_yet "tset union"
| Tinter _ -> Error.not_yet "tset intersection"
| Tcomprehension (_,_,_) -> Error.not_yet "tset comprehension"
| Trange (_,_) -> dup Gmp
| Trange(Some n1, Some n2) ->
ignore (type_term ~use_gmp_opt:true n1);
ignore (type_term ~use_gmp_opt:true n2);
let i = Interval.infer t in
let ty = ty_of_interv ?ctx i in
dup ty
| Trange(None, _) | Trange(_, None) ->
Options.abort "unbounded ranges are not part of E-ACSl"
| Tlet(li, t) ->
infer_if_integer li;
let li_t = Misc.term_of_li li 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