From 16610f5d6787ed10b284656abdcea905836a32c2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Thu, 12 Dec 2024 10:39:25 +0100
Subject: [PATCH] [wp] replace havoc by memcpy
---
src/plugins/wp/MemBytes.ml | 15 +---
src/plugins/wp/MemLoader.ml | 73 ++++++-------------
src/plugins/wp/MemLoader.mli | 10 +--
src/plugins/wp/MemMemory.ml | 39 +++++-----
src/plugins/wp/MemMemory.mli | 2 +-
src/plugins/wp/MemRegion.ml | 19 ++---
src/plugins/wp/MemRegion.mli | 6 +-
src/plugins/wp/MemTyped.ml | 10 +--
src/plugins/wp/TacHavoc.ml | 8 +-
.../wp/share/why3/frama_c_wp/memory.mlw | 6 +-
10 files changed, 69 insertions(+), 119 deletions(-)
diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index da54a47b5d7..30db3c524d2 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -49,8 +49,8 @@ struct
let l_memcpy = Qed.Engine.F_call "memcpy"
let f_memcpy =
Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
- let memcpy mdst msrc ldst lsrc n =
- Lang.F.e_fun f_memcpy [mdst;msrc;ldst;lsrc;n]
+ let memcpy mtgt msrc ltgt lsrc length =
+ Lang.F.e_fun f_memcpy [mtgt;msrc;ltgt;lsrc;length]
let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits"
let cinits m = p_call p_cinits [m]
@@ -674,16 +674,10 @@ module Model = struct
let n = protected_sizeof_object obj in
e_sub (e_div (allocated sigma l) n) e_one
- let havoc obj loc ~length chunk ~fresh ~current =
+ let memcpy obj ~mtgt ~msrc ~ltgt ~lsrc ~length chunk =
if chunk <> Chunk.Alloc then
let n = e_mul (e_int @@ sizeof_object obj) length in
- Why3.havoc fresh current loc n
- else fresh
-
- let memcpy obj ~lsrc ~ldst ~length chunk ~msrc ~mdst =
- if chunk <> Chunk.Alloc then
- let n = e_mul (e_int @@ sizeof_object obj) length in
- Why3.memcpy mdst msrc ldst lsrc n
+ Why3.memcpy mtgt msrc ltgt lsrc n
else msrc
let eqmem_forall obj loc _chunk m1 m2 =
@@ -1150,5 +1144,4 @@ let set_init = Model.set_init
let is_init_range = Model.is_init_range
let value_footprint = Model.value_footprint
let init_footprint = Model.init_footprint
-let havoc = Model.havoc
let memcpy = Model.memcpy
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index b450512c3bf..438544bbf54 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -63,10 +63,8 @@ sig
val last : Sigma.t -> c_object -> loc -> term
- val havoc : c_object -> loc -> length:term ->
- Chunk.t -> fresh:term -> current:term -> term
- val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
- Chunk.t -> msrc:term -> mdst:term -> term
+ val memcpy : c_object -> mtgt:term -> msrc:term -> ltgt:loc -> lsrc:loc ->
+ length:term -> Chunk.t -> term
val eqmem_forall :
c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
@@ -579,60 +577,33 @@ struct
let () = INIT_LOAD_INFO.load_rec := load_init
(* -------------------------------------------------------------------------- *)
- (* --- Memcpy --- *)
+ (* --- Mem Copies \ Havocs --- *)
(* -------------------------------------------------------------------------- *)
- (*let gen_memcpy_length get_domain s obj ~lsrc ~ldst 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 mdst = F.e_var (Lang.freshvar ~basename tau) in
- let havoc = M.memcpy obj ~ldst ~lsrc ~length chunk ~mdst ~msrc:pre in
- ps := Set(post,havoc) :: !ps
- ) (get_domain obj ldst) ; !ps
- *)
- (* -------------------------------------------------------------------------- *)
- (* --- Havocs --- *)
- (* -------------------------------------------------------------------------- *)
-
- let gen_havoc_length get_domain s obj loc length =
-(*
- gen_memcpy_length get_domain s obj ~ldst:loc ~lsrc:loc length
-*)
+ let gen_memcpy_length get_domain s obj ?lsrc 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
+ let updated =
+ match lsrc with
+ | None ->
+ let basename = Chunk.basename_of_chunk chunk ^ "_undef" in
+ let fresh = F.e_var (Lang.freshvar ~basename tau) in
+ M.memcpy obj ~mtgt:pre ~msrc:fresh ~ltgt:loc ~lsrc:loc ~length chunk
+ | Some lsrc ->
+ M.memcpy obj ~mtgt:pre ~msrc:pre ~ltgt:loc ~lsrc ~length chunk
+ in ps := Set(post,updated) :: !ps
) (get_domain obj loc) ; !ps
- let havoc_length = gen_havoc_length M.value_footprint
- let havoc seq obj loc = havoc_length seq obj loc F.e_one
+ let memcpy_length = gen_memcpy_length M.value_footprint
+ let memcpy seq obj ?lsrc ltgt = memcpy_length seq obj ltgt ?lsrc F.e_one
- let havoc_init_length = gen_havoc_length M.init_footprint
- let havoc_init seq obj loc = havoc_init_length seq obj loc F.e_one
-(*
- let set_init_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 set = M.set_init obj loc ~length chunk ~current:pre in
- ps := Set(post,set) :: !ps
- ) (M.init_footprint obj loc) ; !ps
+ let memcpy_init_length = gen_memcpy_length M.init_footprint
+ let memcpy_init seq obj ?lsrc ltgt = memcpy_init_length seq obj ltgt ?lsrc F.e_one
- let set_init seq obj loc = set_init_length seq obj loc F.e_one
-*)
(* -------------------------------------------------------------------------- *)
(* --- Stored & Copied --- *)
(* -------------------------------------------------------------------------- *)
@@ -656,14 +627,14 @@ struct
| C_int _ | C_float _ | C_pointer _ ->
[ updated_atom seq obj loc value ]
| C_comp _ | C_array _ ->
- Set(load_value seq.post obj loc, value) :: havoc seq obj loc
+ Set(load_value seq.post obj loc, value) :: memcpy seq obj loc
let stored_init seq obj loc value =
match obj with
| C_int _ | C_float _ | C_pointer _ ->
[ updated_init_atom seq obj loc value ]
| C_comp _ | C_array _ ->
- Set(load_init seq.post obj loc, value) :: havoc_init seq obj loc
+ 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)
@@ -681,11 +652,11 @@ struct
[ 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
+ memcpy seq obj loc @ memcpy_init seq obj loc
let assigned_range s obj l a b =
- havoc_length s obj (M.shift l obj a) (e_range a b) @
- havoc_init_length s obj (M.shift l obj a) (e_range 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 assigned seq obj sloc =
(* Assert (M.monotonic_init seq.pre seq.post) :: *)
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 3d56fa90c97..18a8b7acf48 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -59,10 +59,8 @@ sig
val last : Sigma.t -> c_object -> loc -> term
- val havoc : c_object -> loc -> length:term ->
- Chunk.t -> fresh:term -> current:term -> term
- val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
- Chunk.t -> msrc:term -> mdst:term -> term
+ val memcpy : c_object -> mtgt:term -> msrc:term -> ltgt:loc -> lsrc:loc ->
+ length:term -> Chunk.t -> term
val eqmem_forall :
c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
@@ -93,8 +91,8 @@ sig
val load_init : M.Sigma.t -> c_object -> M.loc -> term
val load_value : M.Sigma.t -> c_object -> M.loc -> term
- val havoc : M.Sigma.t sequence -> c_object -> M.loc -> equation list
- val havoc_length : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
+ val memcpy : M.Sigma.t sequence -> c_object -> ?lsrc:M.loc -> M.loc -> equation list
+ val memcpy_length : M.Sigma.t sequence -> c_object -> ?lsrc:M.loc -> M.loc -> term -> equation list
val stored : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
val stored_init : M.Sigma.t sequence -> c_object -> M.loc -> term -> equation list
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 1882b4b4fe2..93e0f2287f0 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -35,12 +35,12 @@ let ty_fst_arg = function
| Some l :: _ -> l
| _ -> raise Not_found
-let l_havoc = Qed.Engine.F_call "havoc"
+(* 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_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 *)
@@ -69,15 +69,18 @@ let framed memory = p_call p_framed [ memory ]
(* havoc(m_undef, havoc(_undef,m0,p0,a0), p1,a1) =
- havoc(m_undef, m0, p1,a1) WHEN included (p1,a1,p0,a0) *)
let r_havoc = function
- | [undef1;m1;p1;a1] -> begin
- match F.repr m1 with
- | L.Fun( f , [_undef0;m0;p0;a0] ) when f == f_havoc -> begin
- let open Qed.Logic in
- match MemAddr.is_included [p0;a0;p1;a1] with
- | Yes -> F.e_fun f_havoc [undef1;m0;p1;a1]
- | _ -> raise Not_found
- end
- | _ -> raise Not_found
+ | [m1;undef1;p1;p2;a1] -> begin
+ if equal p1 p2 then
+ match F.repr m1 with
+ | L.Fun( f , [m0;_undef0;p01;p02;a0] ) when f == f_memcpy ->
+ if equal p01 p02 then begin
+ let open Qed.Logic in
+ match MemAddr.is_included [p01;a0;p1;a1] with
+ | Yes -> F.e_fun f_memcpy [m0;undef1;p1;p2;a1]
+ | _ -> raise Not_found
+ end else raise Not_found
+ | _ -> raise Not_found
+ else raise Not_found
end
| _ -> raise Not_found
@@ -87,13 +90,13 @@ let r_havoc = function
*)
let r_get_havoc es ks =
match es, ks with
- | [undef;m;p;a],[k] ->
- begin
- match MemAddr.is_separated [p;a;k;e_one] with
+ | [m;undef;p1;p2;a],[k] ->
+ if equal p1 p2 then begin
+ match MemAddr.is_separated [p1;a;k;e_one] with
| L.Yes -> F.e_get m k
| L.No -> F.e_get undef k
| _ -> raise Not_found
- end
+ end else raise Not_found
| _ -> raise Not_found
(* -------------------------------------------------------------------------- *)
@@ -102,8 +105,8 @@ let r_get_havoc es ks =
let () = Context.register
begin fun () ->
- F.set_builtin f_havoc r_havoc ;
- F.set_builtin_get f_havoc r_get_havoc ;
+ F.set_builtin f_memcpy r_havoc ;
+ F.set_builtin_get f_memcpy r_get_havoc ;
end
(* -------------------------------------------------------------------------- *)
@@ -118,7 +121,7 @@ let frames ~addr:p ~offset:n ~sizeof:s ?(basename="mem") tau =
let m' = F.e_var (Lang.freshvar ~basename t_mem) in
let p' = F.e_var (Lang.freshvar ~basename:"q" MemAddr.t_addr) in
let n' = F.e_var (Lang.freshvar ~basename:"n" L.Int) in
- let mh = F.e_fun f_havoc [m';m;p';n'] in
+ let mh = F.e_fun f_memcpy [m;m';p';p';n'] in
let v' = F.e_var (Lang.freshvar ~basename:"v" tau) in
let meq = F.p_call p_eqmem [m;m';p';n'] in
let diff = F.p_call MemAddr.p_separated [p;n;p';s] in
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index 3e5cb9ad732..ed0cd5ecd87 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -35,7 +35,7 @@ val t_init : tau (** initialization tables *)
val t_mem : tau -> tau (** t_addr indexed array *)
-val f_havoc : lfun
+(* val f_havoc : lfun *)
val f_memcpy : lfun
val f_set_init : lfun
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 3d33335c0a7..24d8175a3ac 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -82,9 +82,8 @@ module type ModelWithLoader = sig
val last : sigma -> c_object -> loc -> term
val frames : c_object -> loc -> chunk -> frame list
- val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
- val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
- chunk -> msrc:term -> mdst:term -> term
+ val memcpy : c_object -> mtgt:term -> msrc:term -> ltgt:loc -> lsrc:loc ->
+ length:term -> Chunk.t -> term
val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
@@ -363,23 +362,15 @@ struct
MemMemory.frames ~addr:(to_addr l) ~offset ~sizeof ~basename tau
| _ -> []
- let havoc ty l ~length chunk ~fresh ~current =
- match chunk with
- | M c -> M.havoc ty (loc l) ~length c ~fresh ~current
- | R c ->
- match c.mu with
- | Value _ | ValInit -> fresh
- | Array _ | ArrInit -> e_fun f_havoc [fresh;current;to_addr l;length]
-
- let memcpy ty ~lsrc ~ldst ~length chunk ~msrc ~mdst =
+ let memcpy ty ~mtgt ~msrc ~ltgt ~lsrc ~length chunk =
match chunk with
| M c ->
- M.memcpy ty ~lsrc:(loc lsrc) ~ldst:(loc ldst) ~length c ~msrc ~mdst
+ M.memcpy ty ~mtgt ~msrc ~ltgt:(loc ltgt) ~lsrc:(loc lsrc) ~length c
| R c ->
match c.mu with
| Value _ | ValInit -> msrc
| Array _ | ArrInit ->
- e_fun f_memcpy [mdst;msrc;to_addr ldst;to_addr lsrc;length]
+ e_fun f_memcpy [mtgt;msrc;to_addr ltgt;to_addr lsrc;length]
let eqmem_forall ty l chunk m1 m2 =
match chunk with
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index e35fedf766b..98549024368 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -59,10 +59,8 @@ sig
val last : sigma -> c_object -> loc -> term
val frames : c_object -> loc -> chunk -> frame list
- val havoc : c_object -> loc -> length:term ->
- chunk -> fresh:term -> current:term -> term
- val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
- chunk -> msrc:term -> mdst:term -> term
+ val memcpy : c_object -> mtgt:term -> msrc:term -> ltgt:loc -> lsrc:loc ->
+ length:term -> Chunk.t -> term
val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 146cce9b681..1fb70e45818 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1042,16 +1042,10 @@ struct
let n = length_of_object obj in
e_sub (F.e_div (allocated sigma l) n) e_one
- let havoc obj loc ~length chunk ~fresh ~current =
+ let memcpy obj ~mtgt ~msrc ~ltgt ~lsrc ~length chunk =
if chunk <> T_alloc then
let n = F.e_mul (length_of_object obj) length in
- F.e_fun f_havoc [fresh;current;loc;n]
- else fresh
-
- let memcpy obj ~lsrc ~ldst ~length chunk ~msrc ~mdst =
- if chunk <> T_alloc then
- let n = F.e_mul (length_of_object obj) length in
- F.e_fun f_memcpy [mdst;msrc;ldst;lsrc;n]
+ F.e_fun f_memcpy [mtgt;msrc;ltgt;lsrc;n]
else msrc
let eqmem_forall obj loc _chunk m1 m2 =
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index ed475f9dae4..840a83a56bd 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -35,8 +35,10 @@ let lookup_havoc e =
| L.Aget( m , p ) ->
begin
match F.repr m with
- | L.Fun( f , [m_undef;m_sep;a;n] ) when f == MemMemory.f_havoc ->
- Some( m_undef , m_sep , a , n , p )
+ | L.Fun( f , [m_sep;m_undef;a;b;n] )
+ when f == MemMemory.f_memcpy ->
+ if F.equal a b then Some( m_sep , m_undef , a , n , p )
+ else None
| _ -> None
end
| _ -> None
@@ -53,7 +55,7 @@ class havoc =
let e = Tactical.selected sel in
match lookup_havoc e with
| None -> Not_applicable
- | Some(mr,m0,a,n,p) ->
+ | Some(m0,mr,a,n,p) ->
let separated =
F.p_call MemAddr.p_separated
[ p ; F.e_int 1 ; a ; n ] in
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index f0baf1c96d4..66e83667e96 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -43,10 +43,10 @@ theory Memory
if separated p 1 b0 s then m0 p else
let offset = b1.offset - b0.offset + p.offset in
m1 { b1 with offset = offset }
-
+(*
function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a =
memcpy m1 m0 p p a
-
+*)
lemma eqmem_included :
forall m1 m2 : map addr 'a.
forall p q : addr.
@@ -64,7 +64,7 @@ theory Memory
forall m0 m1 : map addr 'a.
forall q p : addr.
forall a : int.
- (Map.([]) (havoc m0 m1 p a) (q)) =
+ (Map.([]) (memcpy m1 m0 p p a) (q)) =
(if (separated q 1 p a) then (Map.([]) (m1) (q)) else (Map.([]) (m0) (q)))
(* Initialization memory *)
--
GitLab