From 16a2ab4d100ce31f54b3f3e21c614e702e65bacb Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 18 Sep 2024 10:45:48 +0200
Subject: [PATCH] [wp] MemLoader: require obj for init
---
src/plugins/wp/MemLoader.ml | 22 ++++++++++------------
src/plugins/wp/MemLoader.mli | 6 ++----
src/plugins/wp/MemTyped.ml | 7 ++-----
3 files changed, 14 insertions(+), 21 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 27e8c434e5c..bf2d6b187cd 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -66,8 +66,6 @@ sig
val havoc : c_object -> loc -> length:term ->
Chunk.t -> fresh:term -> current:term -> term
- val eqmem : c_object -> loc -> Chunk.t -> term -> term -> pred
-
val eqmem_forall :
c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
@@ -79,9 +77,9 @@ 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 is_init_atom : Sigma.t -> loc -> term
+ val is_init_atom : Sigma.t -> c_object -> loc -> term
val is_init_range : Sigma.t -> c_object -> loc -> term -> pred
- val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
+ val set_init_atom : Sigma.t -> c_object -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
(* val monotonic_init : Sigma.t -> Sigma.t -> pred *)
@@ -549,7 +547,7 @@ struct
let initialized_loc sigma obj loc =
match obj with
- | C_int _ | C_float _ | C_pointer _ -> p_bool (M.is_init_atom sigma loc)
+ | C_int _ | C_float _ | C_pointer _ -> p_bool (M.is_init_atom sigma obj loc)
| C_comp ci -> initialized_comp sigma ci loc
| C_array a -> initialized_array sigma a loc
@@ -571,9 +569,9 @@ struct
module INIT_LOADER =
LOADER_GEN
(struct
- let load_int sigma _ = M.is_init_atom sigma
- let load_float sigma _ = M.is_init_atom sigma
- let load_pointer sigma _ = M.is_init_atom sigma
+ let load_int sigma ikind = M.is_init_atom sigma (C_int ikind)
+ let load_float sigma fkind = M.is_init_atom sigma (C_float fkind)
+ let load_pointer sigma typ = M.is_init_atom sigma (C_pointer typ)
end)(COMP_INIT)(ARRAY_INIT)
let load_init = INIT_LOADER.load
@@ -618,8 +616,8 @@ struct
(* --- Stored & Copied --- *)
(* -------------------------------------------------------------------------- *)
- let updated_init_atom seq loc value =
- let chunk_init,mem_init = M.set_init_atom seq.pre loc value in
+ let updated_init_atom seq obj loc value =
+ let chunk_init,mem_init = M.set_init_atom seq.pre obj loc value in
Set(Sigma.value seq.post chunk_init,mem_init)
let updated_atom seq obj loc value =
@@ -642,7 +640,7 @@ struct
let stored_init seq obj loc value =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
- [ updated_init_atom seq loc value ]
+ [ updated_init_atom seq obj loc value ]
| C_comp _ | C_array _ ->
Set(load_init seq.post obj loc, value) :: havoc_init seq obj loc
@@ -659,7 +657,7 @@ struct
| C_int _ | C_float _ | C_pointer _ ->
let value = Lang.freshvar ~basename:"v" (Lang.tau_of_object obj) in
let init = Lang.freshvar ~basename:"i" (Lang.init_of_object obj) in
- [ updated_init_atom seq loc (e_var init) ;
+ [ updated_init_atom seq obj loc (e_var init) ;
updated_atom seq obj loc (e_var value) ]
| C_comp _ | C_array _ ->
havoc seq obj loc @ havoc_init seq obj loc
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index c460d3cae0b..46d62359db3 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -62,8 +62,6 @@ sig
val havoc : c_object -> loc -> length:term ->
Chunk.t -> fresh:term -> current:term -> term
- val eqmem : c_object -> loc -> Chunk.t -> term -> term -> pred
-
val eqmem_forall :
c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
@@ -75,9 +73,9 @@ 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 is_init_atom : Sigma.t -> loc -> term
+ val is_init_atom : Sigma.t -> c_object -> loc -> term
val is_init_range : Sigma.t -> c_object -> loc -> term -> pred
- val set_init_atom : Sigma.t -> loc -> term -> Chunk.t * term
+ val set_init_atom : Sigma.t -> c_object -> loc -> term -> Chunk.t * term
val set_init : c_object -> loc -> length:term ->
Chunk.t -> current:term -> term
(* val monotonic_init : Sigma.t -> Sigma.t -> pred *)
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index dbfafb02cb6..473a678b004 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1048,9 +1048,6 @@ struct
F.e_fun f_havoc [fresh;current;loc;n]
else fresh
- let eqmem obj loc _chunk m1 m2 =
- F.p_call p_eqmem [m1;m2;loc;length_of_object obj]
-
let eqmem_forall obj loc _chunk m1 m2 =
let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
let p = F.e_var xp in
@@ -1065,8 +1062,8 @@ 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 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
+ let set_init_atom sigma _obj l v = updated sigma T_init l v
+ let is_init_atom sigma _ l = F.e_get (Sigma.value sigma T_init) l
let is_init_range sigma obj loc length =
let n = F.e_mul (length_of_object obj) length in
--
GitLab