From 9719d6794c0cb06d15ed618376da2ad95daac3c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Mon, 13 Jan 2025 09:22:49 +0100
Subject: [PATCH] [wp] copied (struct/array): None => Some lsrc
---
src/plugins/wp/MemBytes.ml | 8 +-------
src/plugins/wp/MemLoader.ml | 15 +++++++++++----
src/plugins/wp/MemMemory.ml | 3 +--
src/plugins/wp/Sigs.ml | 2 +-
4 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index 5272d97dfde..eb593e762bf 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -40,13 +40,7 @@ struct
let ty_fst_arg = function
| Some l :: _ -> l
| _ -> raise Not_found
- (*
- let l_havoc = Qed.Engine.F_call "havoc"
- let f_havoc =
- Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
- let havoc fresh current loc n =
- Lang.F.e_fun f_havoc [fresh;current;loc;n]
- *)
+
let l_memcpy = Qed.Engine.F_call "memcpy"
let f_memcpy =
Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 438544bbf54..d1bd6baa793 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -636,7 +636,13 @@ struct
| C_comp _ | C_array _ ->
Set(load_init seq.post obj loc, value) :: memcpy_init seq obj loc
- let copied s obj p q = stored s obj p (load_value s.pre obj q)
+ let copied s obj p q = match obj with
+ | C_int _ | C_float _ | C_pointer _ ->
+ stored s obj p (load_value s.pre obj q)
+ | C_comp _ | C_array _ ->
+ Set(load_value s.post obj p, load_value s.pre obj q)
+ :: memcpy s obj ~lsrc:q p
+
let copied_init s obj p q = stored_init s obj p (load_init s.pre obj q)
@@ -652,11 +658,12 @@ struct
[ updated_init_atom seq obj loc (e_var init) ;
updated_atom seq obj loc (e_var value) ]
| C_comp _ | C_array _ ->
- memcpy seq obj loc @ memcpy_init seq obj loc
+ memcpy seq obj ~lsrc:loc loc @ memcpy_init seq obj loc
let assigned_range s obj l a b =
- memcpy_length s obj (M.shift l obj a) (e_range a b) @
- memcpy_init_length s obj (M.shift l obj a) (e_range a b)
+ let loc = M.shift l obj a in
+ memcpy_length s obj loc (e_range a b) @
+ memcpy_init_length s obj loc (e_range a b)
let assigned seq obj sloc =
(* Assert (M.monotonic_init seq.pre seq.post) :: *)
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 93e0f2287f0..78a20c8d1fc 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -35,12 +35,11 @@ let ty_fst_arg = function
| Some l :: _ -> l
| _ -> raise Not_found
-(* let l_havoc = Qed.Engine.F_call "havoc"*)
+
let l_memcpy = Qed.Engine.F_call "memcpy"
let l_set_init = Qed.Engine.F_call "set_init"
let p_eqmem = Lang.extern_fp ~library "eqmem"
-(* let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc" *)
let f_memcpy = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 609645de518..da6c1eb517d 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -195,7 +195,7 @@ sig
Memory chunk variables are assigned lazily. Hence, the vector is
empty unless a chunk is accessed. Pay attention to this
- when you merge or havoc chunks.
+ when you merge or havoc chunks (using memcpy).
New chunks are generated from the context pool of {!Lang.freshvar}.
*)
--
GitLab