Skip to content

GitLab

Commit 159bca76 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

Merge branch 'fix/wp/initialized-issues-965' into 'master' 

Fixes initialized bugs #965

Closes #965

See merge request frama-c/frama-c!2883
parents fd63f8a7 f5c9ca1d
Hide whitespace changes
Inline Side-by-side
src/plugins/wp/CodeSemantics.ml
View file @ 159bca76
......@@ -113,7 +113,7 @@ struct
let is_exp_range sigma l obj a b v =
let x = Lang.freshvar ~basename:"k" Logic.Int in
let k = e_var x in
let range = [ p_leq a k ; p_lt k b ] in
let range = [ p_leq a k ; p_leq k b ] in
let init =
match v with
| None -> is_zero sigma obj (M.shift l obj k)
......@@ -443,31 +443,35 @@ struct
~severe:false ~effect:"Skip initializer"
(fun () ->
let l = lval sigma lv in
match init with
| Some e ->
let v = M.load sigma obj l in
p_equal (val_of_exp sigma e) (cval v)
| None -> is_zero sigma obj l
let value_hyp = match init with
| Some e ->
let v = M.load sigma obj l in
p_equal (val_of_exp sigma e) (cval v)
| None -> is_zero sigma obj l
in
value_hyp, (M.initialized sigma (Rloc(obj, l)))
) () in
match outcome with
| Warning.Failed warn -> warn , F.p_true
| Warning.Failed warn -> warn , (F.p_true, F.p_true)
| Warning.Result(warn , hyp) -> warn , hyp
let init_range ~sigma lv typ a b value =
let init_range ~sigma lv typ low up value =
let obj = Ctypes.object_of typ in
let outcome = Warning.catch
~severe:false ~effect:"Skip initializer"
(fun () ->
let l = lval sigma lv in
let e = Extlib.opt_map (exp sigma) value in
is_exp_range sigma l obj (e_bigint a) (e_bigint b) e
let low = e_bigint low and up = e_bigint up in
(is_exp_range sigma l obj low up e),
(M.initialized sigma (Rrange(l, obj, Some low, Some up)))
) () in
match outcome with
| Warning.Failed warn -> warn , F.p_true
| Warning.Failed warn -> warn , (F.p_true, F.p_true)
| Warning.Result(warn , hyp) -> warn , hyp
type warned_hyp = Warning.Set.t * Lang.F.pred
type warned_hyp = Warning.Set.t * (Lang.F.pred * Lang.F.pred)
(* Hypothesis for initialization of one variable *)
let rec init_variable ~sigma lv init acc =
......@@ -517,8 +521,7 @@ struct
| (_,None) -> acc (* nothing was delayed *)
| (il,Some (i0,_,exp)) when Integer.lt il i0 ->
(* Added pred: \forall i \in [il .. i0] ; t[i]==exp *)
let i2 = Integer.succ i0 in
init_range ~sigma lv ty il i2 (Some exp) :: acc
init_range ~sigma lv ty il i0 (Some exp) :: acc
| (_il,Some (_i0,off,exp)) ->
(* case [_il=_i0], so uses [off] corresponding to [_i0]
Added pred: t[i]==exp*)
......@@ -531,7 +534,7 @@ struct
if Integer.ge i0 i1 then (* no hole *) acc
else (* defaults values
Added pred: \forall i \in [i0 .. i1[ ; t[i]==default *)
init_range ~sigma lv ty i0 i1 None :: acc
init_range ~sigma lv ty i0 (Integer.pred i1) None :: acc
in
let acc, delayed =
List.fold_left
......
src/plugins/wp/MemVar.ml
View file @ 159bca76
......@@ -1085,11 +1085,11 @@ struct
| Ref _ -> p_true
| Loc l -> M.initialized sigma.mem (Rloc(obj,l))
| Val(m,x,p) ->
if (x.vformal || x.vglob) then
if is_heap_allocated m then
M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
else if (x.vformal || x.vglob) then
try valid_offset RW (vobject m x) p
with ShiftMismatch -> shift_mismatch l
else if is_heap_allocated m then
M.initialized sigma.mem (Rloc(obj,mloc_of_loc l))
else
initialized_loc sigma obj x p
end
......@@ -1099,17 +1099,26 @@ struct
| Loc l -> M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
| Val(m,x,p) ->
try
let in_array = valid_range RW (vobject m x) p (elt, a, b) in
let initialized =
if x.vformal || x.vglob then p_true
else initialized_range sigma (vobject m x) x p a b
in
F.p_imply (F.p_leq a b) (p_and in_array initialized)
with ShiftMismatch ->
if is_heap_allocated m then
let l = mloc_of_loc l in
M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
else shift_mismatch l
else
let rec normalize obj = function
| [] -> [], a, b
| [Shift(elt, i)] when Ctypes.equal obj elt ->
[], F.e_add a i, F.e_add b i
| f :: ofs ->
let l, a, b = normalize obj ofs in f :: l, a, b
in
let p, a, b = normalize elt p in
let in_array = valid_range RW (vobject m x) p (elt, a, b) in
let initialized =
if x.vformal || x.vglob then p_true
else initialized_range sigma (vobject m x) x p a b
in
F.p_imply (F.p_leq a b) (p_and in_array initialized)
with ShiftMismatch ->
shift_mismatch l
end
| Rrange(l, _,a,b) ->
Warning.error
......@@ -1190,7 +1199,10 @@ struct
match scope with
| Leave -> []
| Enter ->
let xs = List.filter (fun v -> not v.vformal && not v.vglob) xs in
let xs = List.filter
(fun v -> is_mvar_alloc v && not v.vformal &&
not v.vglob && not v.vdefined) xs
in
let uninitialized v =
let value = Cvalues.uninitialized_obj (Ctypes.object_of v.vtype) in
Lang.F.p_equal (access_init (get_init_term seq.post v) []) value
......
src/plugins/wp/Sigs.ml
View file @ 159bca76
......@@ -587,7 +587,7 @@ sig
Express that all objects in a range of locations have a given value.
More precisely, [is_exp_range sigma loc ty a b v] express that
value at [( ty* )loc + k] equals [v], forall [a <= k < b].
value at [( ty* )loc + k] equals [v], forall [a <= k <= b].
Value [v=None] stands for zero.
*)
val is_exp_range :
......@@ -598,17 +598,25 @@ sig
val unchanged : M.sigma -> M.sigma -> varinfo -> pred
(** Express that a given variable has the same value in two memory states. *)
type warned_hyp = Warning.Set.t * pred
val init : sigma:M.sigma -> varinfo -> init option -> warned_hyp list
(** Express that some variable has some initial value at the
given memory state.
Remark: [None] initializer are interpreted as zeroes. This is consistent
with the [init option] associated with global variables in CIL,
for which the default initializer are zeroes. There is no
[init option] value associated with local initializers.
*)
type warned_hyp = Warning.Set.t * (pred * pred)
val init :
sigma:M.sigma -> varinfo -> init option -> warned_hyp list
(** Express that some variable has some initial value at the
given memory state. The first predicate states the value,
the second, the initialization status.
Note: we DO NOT merge values and initialization status
hypotheses as the factorization performed by Qed can make
predicates too hard to simplify later.
Remark: [None] initializer are interpreted as zeroes. This is consistent
with the [init option] associated with global variables in CIL,
for which the default initializer are zeroes. This function is called
for global initializers and local initializers ([Cil.Local_init]).
It is not called for local variables without initializers as they do not
have a [Cil.init option].
*)
end
......
src/plugins/wp/StmtSemantics.ml
View file @ 159bca76
......@@ -416,7 +416,10 @@ struct
let here = Sigma.create () in
let next = Sigma.create () in
(*TODO: make something of warnings *)
let hyp = Lang.F.p_all snd (C.init ~sigma:next vi (Some init)) in
let init = C.init ~sigma:next vi (Some init) in
let hyp_value = Lang.F.p_all (fun (_, h) -> fst h) init in
let hyp_init = Lang.F.p_all (fun (_, h) -> snd h) init in
let hyp = Lang.F.p_and hyp_init hyp_value in
effect (env @: Clabels.here) (Cfg.E.create {pre=here; post=next} hyp) (env @: Clabels.next)
| Skip _ | Code_annot _ -> goto (env @: Clabels.here) (env @: Clabels.next)
......@@ -669,7 +672,10 @@ struct
let cfg_init = Globals.Vars.fold_in_file_order
(fun var initinfo cfg ->
if var.vstorage = Extern then cfg else
let h = Lang.F.p_all snd (C.init ~sigma:sinit var initinfo.init) in
let init = C.init ~sigma:sinit var initinfo.init in
let hvalue = Lang.F.p_all (fun (_, h) -> fst h) init in
let hinit = Lang.F.p_all (fun (_, h) -> snd h) init in
let h = Lang.F.p_and hvalue hinit in
let h = Cfg.P.create
(Cfg.Node.Map.add ninit sinit Cfg.Node.Map.empty)
h
......
src/plugins/wp/cfgWP.ml
View file @ 159bca76
......@@ -248,11 +248,6 @@ struct
path = path ;
}
let assume_vcs ?descr ?filter ?init whs vc =
List.fold_left
(fun vc (warn,hyp) -> assume_vc ?descr ?filter ?init ~warn [hyp] vc)
vc whs
(* -------------------------------------------------------------------------- *)
(* --- Branching --- *)
(* -------------------------------------------------------------------------- *)
......@@ -906,13 +901,14 @@ struct
[C.unchanged shere sinit v]
in { wp with vcs = gmap const_vc wp.vcs })
let init wenv var init wp = in_wenv wenv wp
let init wenv var opt_init wp = in_wenv wenv wp
(fun env wp ->
let assume = assume_vc ~descr:"Initializer" ~filter:true ~init:true in
let sigma = L.current env in
let init_vc = assume_vcs
~init:true ~filter:true
~descr:"Initializer"
(C.init ~sigma var init)
let init_vc vc =
List.fold_left
(fun vc (warn,(hv,hi)) -> assume ~warn [hi] (assume ~warn [hv] vc))
vc (C.init ~sigma var opt_init)
in { wp with vcs = gmap init_vc wp.vcs })
(* -------------------------------------------------------------------------- *)
......
src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
View file @ 159bca76
......@@ -352,7 +352,7 @@ new way
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
......@@ -370,7 +370,7 @@ Prove: foo_0 = 1.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
......@@ -387,7 +387,7 @@ Prove: true.
main_assigns_global sequent:
Assume {
Have: foo_1 = 42.
Have: (Init_r_0=false) /\ (ta_r_0=true) /\ (ta_r_1=false).
Have: (ta_r_0=true) /\ (ta_r_1=false).
Have: foo_2 = 1.
Have: x = result_0.
Have: x = foo_0.
......@@ -405,8 +405,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
......@@ -428,8 +428,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i = 0).
Have: (Init_i_1=true) /\ ((1 + i) = i_1).
Have: i_1 <= 10.
Have: i_2 <= 10.
......@@ -448,8 +448,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
......@@ -467,8 +467,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i <= 10.
......@@ -485,8 +485,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i).
}
Prove: i <= 10.
......@@ -500,8 +500,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i_1 = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i_1 = 0).
Have: (Init_i_1=true) /\ ((1 + i_1) = i_2).
Have: i_2 <= 10.
Have: i_3 <= 10.
......@@ -520,8 +520,8 @@ zloop sequent:
Assume {
Have: foo_0 = 42.
Have: 0 <= x.
Have: (Init_i_0=false) /\ (ta_i_0=true) /\ (ta_i_1=false).
Have: i = 0.
Have: (ta_i_0=true) /\ (ta_i_1=false).
Have: (Init_i_0=true) /\ (i = 0).
Have: (Init_i_1=true) /\ ((1 + i) = i_1).
Have: i_1 <= 10.
Have: i_2 <= 10.
......
src/plugins/wp/tests/wp_acsl/initialized_local_init.i 0 → 100644
View file @ 159bca76
void l_int(void){
int x = 1 ;
//@ assert SUCCS: x == 1;
//@ assert SUCCS: \initialized(&x);
//@ check FAILS: \false ;
}
void l_array(void){
int x[3] = { 0 } ;
//@ assert SUCCS: x[0] == x[1] == x[2] == 0 ;
//@ assert SUCCS: \initialized(&x);
//@ check FAILS: \false ;
}
typedef struct { int x ; char t[2] ; } S;
void l_struct(void){
S s = { 0 };
//@ assert SUCCS: s.x == s.t[0] == s.t[1] == 0 ;
//@ assert SUCCS: \initialized(&s);
//@ check FAILS: \false ;
}
src/plugins/wp/tests/wp_acsl/initialized_memtyped.i
View file @ 159bca76
......@@ -81,4 +81,10 @@ void formal(int x)
{
int * p = &x ;
//@ assert provable: \initialized(p);
}
\ No newline at end of file
}
void ptr_on_local(void){
int x[3] = {0} ;
int *p = x ;
//@ assert provable: \initialized(p + (0..2));
}
src/plugins/wp/tests/wp_acsl/initialized_shift_array.i 0 → 100644
View file @ 159bca76
/*@
requires \initialized(buf + (0 .. count - 1));
*/
int test(char *buf, int count);
// Success:
void succ_full_first_cell(void){
char buf[3] = {0};
test(buf , 1);
}
void succ_full_full(void){
char buf[3] = {0};
test(&buf[0], 3);
}
void succ_full_from_1(void){
char buf[3] = {0};
test(buf+1 , 2);
}
void succ_from_1_from_1(void){
char buf[3];
buf[1] = buf[2] = 1 ;
test(buf+1 , 2);
}
void succ_full_from_2(void){
char buf[3] = {0};
test(&buf[2], 1);
}
// Failure:
void fail_cell_before(void){
char buf[3] = {0};
test(buf-1 , 1);
}
void fail_too_long(void){
char buf[3] = {0};
test(buf , 4);
}
void fail_too_long_from_1(void){
char buf[3] = {0};
test(&buf[1], 3);
}
void fail_too_long_from_2(void){
char buf[3] = {0};
test(buf+2 , 2);
}
void fail_cell_after_end(void){
char buf[3] = {0};
test(buf+3 , 1);
}
void fail_partial_not_full(void){
char buf[3];
buf[0] = buf[1] = 0;
test(&buf[0], 3);
}
src/plugins/wp/tests/wp_acsl/oracle/initialized_local_init.res.oracle 0 → 100644
View file @ 159bca76
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/initialized_local_init.i (no preprocessing)
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function l_array
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 9):
Let x_1 = x[1].
Let x_2 = x[2].
Assume {
Type: is_sint32(x_1) /\ is_sint32(x_2).
(* Initializer *)
Init: x[0] = 0.
(* Initializer *)
Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
}
Prove: (x_1 = 0) /\ (x_2 = 0) /\ (x_2 = x_1).
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 10):
Assume {
(* Goal *)
When: (0 <= i) /\ (i <= 2).
(* Initializer *)
Init: (Init_x_0[0]=true).
(* Initializer *)
Init: x[0] = 0.
(* Initializer *)
Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (Init_x_0[i_1]=true))).
(* Initializer *)
Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) -> (x[i_1] = 0))).
(* Assertion 'SUCCS' *)
Have: (x[1] = 0) /\ (x[2] = 0).
}
Prove: (Init_x_0[i]=true).
------------------------------------------------------------
Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 11):
Assume {
(* Initializer *)
Init: x[0] = 0.
(* Initializer *)
Init: forall i : Z. ((0 < i) -> ((i <= 2) -> (x[i] = 0))).
(* Assertion 'SUCCS' *)
Have: (x[1] = 0) /\ (x[2] = 0).
}
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function l_int
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 3):
Prove: true.
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 4):
Prove: true.
------------------------------------------------------------
Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 5):
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function l_struct
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 16):
Prove: true.
------------------------------------------------------------
Goal Assertion 'SUCCS' (file tests/wp_acsl/initialized_local_init.i, line 17):
Prove: true.
------------------------------------------------------------
Goal Check 'FAILS' (file tests/wp_acsl/initialized_local_init.i, line 18):
Prove: false.
------------------------------------------------------------
src/plugins/wp/tests/wp_acsl/oracle/initialized_memtyped.res.oracle
View file @ 159bca76
......@@ -50,6 +50,26 @@ Goal Post-condition 'unknown' in 'glob_var':
Assume { (* Heap *) Type: (region(px_0.base) <= 0) /\ cinits(Init_0). }
Prove: (Init_0[px_0]=true).
------------------------------------------------------------
------------------------------------------------------------
Function ptr_on_local
------------------------------------------------------------
Goal Assertion 'provable' (file tests/wp_acsl/initialized_memtyped.i, line 89):
Let a = global(L_x_63).
Assume {
(* Heap *)
Type: cinits(Init_0).
(* Goal *)
When: (0 <= i) /\ (i <= 2).
(* Initializer *)
Init: (Init_0[shift_sint32(a, 0)]=true).
(* Initializer *)
Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
(Init_0[shift_sint32(a, i_1)]=true))).
}
Prove: (Init_0[shift_sint32(a, i)]=true).
------------------------------------------------------------
------------------------------------------------------------
Function test
......
src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle 0 → 100644
View file @ 159bca76
# frama-c -wp [...]
[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
[wp] Running WP plugin...
[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning:
No code nor implicit assigns clause for function test, generating default assigns from the prototype
[wp] Warning: Missing RTE guards
------------------------------------------------------------
Function fail_cell_after_end
------------------------------------------------------------
Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_after_end' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 50)
:
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function fail_cell_before
------------------------------------------------------------
Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_before' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 34)
:
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function fail_partial_not_full
------------------------------------------------------------
Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_partial_not_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 55)
:
Assume { (* Goal *) When: (0 <= i) /\ (i <= 2). }
Prove: (([false..])[1 <- true][0 <- true][i]=true).
------------------------------------------------------------
------------------------------------------------------------
Function fail_too_long
------------------------------------------------------------
Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 38)
:
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function fail_too_long_from_1
------------------------------------------------------------
Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 42)
:
Prove: false.
------------------------------------------------------------
------------------------------------------------------------
Function fail_too_long_from_2