diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index ac6e5cbcda1d19012b80a37f5a0ea87ae09c44ca..4b8f5ba39f7d4b123a16d776839ab9515c977d7c 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -79,7 +79,7 @@ sig
val store_float : Sigma.t -> c_float -> loc -> term -> Chunk.t * term
val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
- val init_atom : Sigma.t -> loc -> Chunk.t * term
+ val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val is_init_atom : Sigma.t -> loc -> term
end
@@ -382,43 +382,26 @@ struct
let () = initrec := initvalue
- (* -------------------------------------------------------------------------- *)
- (* --- Havocs --- *)
- (* -------------------------------------------------------------------------- *)
-
- let havoc_length s obj loc length =
- let ps = ref [] in
- Domain.iter
- (fun chunk ->
- let pre = Sigma.value s.pre chunk in
- let post = Sigma.value s.post chunk in
- let tau = Chunk.tau_of_chunk chunk in
- let basename = Chunk.basename_of_chunk chunk ^ "_undef" in
- let fresh = F.e_var (Lang.freshvar ~basename tau) in
- let havoc = M.havoc obj loc ~length chunk ~fresh ~current:pre in
- ps := Set(post,havoc) :: !ps
- ) (domain obj loc) ; !ps
-
- let havoc seq obj loc = havoc_length seq obj loc F.e_one
-
(* -------------------------------------------------------------------------- *)
(* --- Initialized --- *)
(* -------------------------------------------------------------------------- *)
- let rec initialized_term obj term =
+ let rec on_initialized_terms map on_leave obj terms =
match obj with
- | C_int _ | C_float _ | C_pointer _ -> p_bool term
+ | C_int _ | C_float _ | C_pointer _ -> on_leave terms
| C_comp ci ->
let initialized_field f =
- initialized_term
+ on_initialized_terms map on_leave
(object_of f.ftype)
- (e_getfield term (Cfield (f, KInit)))
+ (map (fun t -> e_getfield t (Cfield (f, KInit))) terms)
in
p_conj (List.map initialized_field ci.cfields)
| C_array ai ->
let obj_e, ds = Matrix.of_array ai in
let denv = Matrix.denv ds in
- let values = List.fold_left e_get term denv.index_val in
+ let values =
+ map (fun t -> List.fold_left e_get t denv.index_val) terms
+ in
let make_subst var value p =
match value with
| None -> p
@@ -428,7 +411,16 @@ struct
let conj =
List.fold_left (fun p f -> f p) (p_conj denv.index_range) substs
in
- p_imply conj (initialized_term obj_e values)
+ p_forall denv.index_var
+ (p_imply conj (on_initialized_terms map on_leave obj_e values))
+
+ let initialized_term =
+ on_initialized_terms Extlib.id p_bool
+
+ let initialized_monotonic =
+ on_initialized_terms
+ (fun f (a, b) -> f a, f b)
+ (fun (a, b) -> p_imply (p_bool a) (p_bool b))
let initialized_loc sigma obj loc =
initialized_term obj (initvalue sigma obj loc)
@@ -446,21 +438,61 @@ struct
"Invalid infinite range @[<hov 2>+@,(%a@,..%a)@]"
Vset.pp_bound low Vset.pp_bound up
+ let initialized_loc_monotonic seq obj loc =
+ initialized_monotonic
+ obj ((initvalue seq.pre obj loc), (initvalue seq.post obj loc))
+
+ let initialized_range_monotonic s obj loc a b =
+ let i = Lang.freshvar ~basename:"i" Lang.t_int in
+ let init =
+ p_forall [i]
+ (p_imply
+ (p_and (p_leq a (e_var i)) (p_leq (e_var i) b))
+ (initialized_loc_monotonic s obj (M.shift loc obj (e_var i))))
+ in
+ Assert init
+
+ (* -------------------------------------------------------------------------- *)
+ (* --- Havocs --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ let havoc_length s obj loc length =
+ let ps = ref [] in
+ Domain.iter
+ (fun chunk ->
+ let pre = Sigma.value s.pre chunk in
+ let post = Sigma.value s.post chunk in
+ let tau = Chunk.tau_of_chunk chunk in
+ let basename = Chunk.basename_of_chunk chunk ^ "_undef" in
+ let fresh = F.e_var (Lang.freshvar ~basename tau) in
+ let havoc = M.havoc obj loc ~length chunk ~fresh ~current:pre in
+ ps := Set(post,havoc) :: !ps
+ ) (domain obj loc) ; !ps
+
+ let havoc seq obj loc = havoc_length seq obj loc F.e_one
+
(* -------------------------------------------------------------------------- *)
(* --- Stored & Copied --- *)
(* -------------------------------------------------------------------------- *)
- let updated seq phi_store alpha loc value =
- let chunk_store,mem_store = phi_store seq.pre alpha loc value in
- let chunk_init,mem_init = M.init_atom seq.pre loc in
- [Set(Sigma.value seq.post chunk_store,mem_store) ;
- Set(Sigma.value seq.post chunk_init,mem_init)]
+ let updated_init seq loc value =
+ let chunk_init,mem_init = M.set_init_atom seq.pre loc value in
+ Set(Sigma.value seq.post chunk_init,mem_init)
+
+ let updated_atom seq obj loc value =
+ let phi_store sigma = match obj with
+ | C_int i -> M.store_int sigma i
+ | C_float f -> M.store_float sigma f
+ | C_pointer ty -> M.store_pointer sigma ty
+ | _ -> failwith "MemLoader updated_atom called on a non atomic type"
+ in
+ let chunk_store,mem_store = phi_store seq.pre loc value in
+ Set(Sigma.value seq.post chunk_store,mem_store)
let stored seq obj loc value =
match obj with
- | C_int i -> updated seq M.store_int i loc value
- | C_float f -> updated seq M.store_float f loc value
- | C_pointer ty -> updated seq M.store_pointer ty loc value
+ | C_int _ | C_float _ | C_pointer _ ->
+ updated_init seq loc e_true :: [ updated_atom seq obj loc value ]
| C_comp _ | C_array _ ->
let init = Cvalues.initialized_obj obj in
Set(initvalue seq.post obj loc, init) ::
@@ -475,12 +507,17 @@ struct
let assigned_loc seq obj loc =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- let x = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
- stored seq obj loc (e_var x)
+ let value = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
+ let init = Lang.freshvar ~basename:"i" (Lang.init_of_object obj) in
+ [ Assert (initialized_loc_monotonic seq obj loc) ;
+ updated_init seq loc (e_var init) ;
+ updated_atom seq obj loc (e_var value) ]
| C_comp _ | C_array _ ->
+ Assert (initialized_loc_monotonic seq obj loc) ::
havoc seq obj loc
let assigned_range s obj l a b =
+ initialized_range_monotonic s obj l a b ::
havoc_length s obj (M.shift l obj a) (e_range a b)
let assigned seq obj = function
@@ -495,7 +532,12 @@ struct
let sep_from_all = F.p_forall xs (F.p_imply condition separated) in
let phi = F.p_forall p (F.p_imply sep_from_all equal) in
ps := Assert phi :: !ps
- ) (M.value_footprint obj loc) ; !ps
+ ) (domain obj loc) ;
+ let mono =
+ F.p_forall xs
+ (F.p_imply condition (initialized_loc_monotonic seq obj loc))
+ in
+ Assert mono :: !ps
| Sarray(loc,obj,n) ->
assigned_range seq obj loc e_zero (e_int (n-1))
| Srange(loc,obj,u,v) ->
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 7240bbcc920442864f2268a454177550a482b6e4..16cf3b31168362479905890be976b309df5044b1 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -75,7 +75,7 @@ sig
val store_float : Sigma.t -> c_float -> loc -> term -> Chunk.t * term
val store_pointer : Sigma.t -> typ -> loc -> term -> Chunk.t * term
- val init_atom : Sigma.t -> loc -> Chunk.t * term
+ val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
val is_init_atom : Sigma.t -> loc -> term
end
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index ec013da03bcc008997900d389705f7c2c4e29494..85f5d00e3503555d0383fdba13bc13234c81a455 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -813,7 +813,7 @@ struct
| Lmem(r,l,rt,(Pointer _ as v)) -> store_mem sigma r rt v l value
| _ -> error "Can not store pointer values into %a" pretty loc
- let init_atom _ _ = assert false
+ let set_init_atom _ _ _ = assert false
let is_init_atom _ _ = assert false
end
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 51d49141a7ed7131f5eb22ae3fc461a33ffac94c..3de96aa6c9d95f3f71a41fc0cd252fd3ee2deefa 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -984,7 +984,7 @@ struct
let store_float sigma f l v = updated sigma (m_float f) l v
let store_pointer sigma _ty l v = updated sigma M_pointer l v
- let init_atom sigma l = updated sigma T_init l e_true
+ let set_init_atom sigma l v = updated sigma T_init l v
let is_init_atom sigma l = F.e_get (Sigma.value sigma T_init) l
end