From b32741af389b131973dfcbccf4cdf913a5c7df66 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 20 Sep 2024 15:42:17 +0200
Subject: [PATCH] [wp] addr_of_int only works for existing bases
---
src/plugins/wp/MemAddr.ml | 32 ++++++++++++-------
.../wp/share/why3/frama_c_wp/memaddr.mlw | 29 +++++++++++------
2 files changed, 41 insertions(+), 20 deletions(-)
diff --git a/src/plugins/wp/MemAddr.ml b/src/plugins/wp/MemAddr.ml
index a043d41b134..3ade44f81ba 100644
--- a/src/plugins/wp/MemAddr.ml
+++ b/src/plugins/wp/MemAddr.ml
@@ -79,6 +79,8 @@ let p_linked = Lang.extern_fp ~coloring:true ~library "linked"
(* --- API --- *)
(* -------------------------------------------------------------------------- *)
+(* Basic constructors and getters *)
+
let base addr = e_fun f_base [ addr ]
let offset addr = e_fun f_offset [ addr ]
let null = constant (e_fun f_null [])
@@ -86,25 +88,36 @@ let global base = e_fun f_global [ base ]
let shift addr offset = e_fun f_shift [ addr ; offset ]
let mk_addr base offset = shift (global base) offset
+(* Comparisons *)
+
let addr_lt addr1 addr2 = p_call p_addr_lt [ addr1 ; addr2 ]
let addr_le addr1 addr2 = p_call p_addr_le [ addr1 ; addr2 ]
+(* Regions *)
+
+let region base = e_fun f_region [ base ]
+let linked memory = p_call p_linked [ memory ]
+
+(* Validity *)
+
+let valid_rd alloc addr size = p_call p_valid_rd [ alloc ; addr ; size ]
+let valid_rw alloc addr size = p_call p_valid_rw [ alloc ; addr ; size ]
+let valid_obj alloc addr size = p_call p_valid_obj [ alloc ; addr ; size ]
+let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
+
+(* Physical addresses *)
+
let addr_of_int i = e_fun f_addr_of_int [ i ]
let int_of_addr addr = e_fun f_int_of_addr [ addr ]
+(* Table of offsets *)
+
let base_offset base offset =
let offset_index = e_fun f_table_of_base [base] in
e_fun f_table_to_offset [offset_index ; offset]
(** Returns the offset in {i bytes} from the {i logic} offset
(which is a memory cell index, actually) *)
-let valid_rd alloc addr size = p_call p_valid_rd [ alloc ; addr ; size ]
-let valid_rw alloc addr size = p_call p_valid_rw [ alloc ; addr ; size ]
-let valid_obj alloc addr size = p_call p_valid_obj [ alloc ; addr ; size ]
-let invalid alloc addr size = p_call p_invalid [ alloc ; addr ; size ]
-
-let region base = e_fun f_region [ base ]
-let linked memory = p_call p_linked [ memory ]
(* -------------------------------------------------------------------------- *)
(* --- Qed Simplifiers --- *)
@@ -293,10 +306,7 @@ let phi_int_of_addr p =
| _ -> raise Not_found
let phi_addr_of_int p =
- if p == e_zero then null else
- match repr p with
- | Fun(f,[a]) when f == f_int_of_addr -> a
- | _ -> raise Not_found
+ if p == e_zero then null else raise Not_found
(* -------------------------------------------------------------------------- *)
(* --- Simplifier for (in)validity --- *)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
index f6022c77526..200a8d7d902 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memaddr.mlw
@@ -136,9 +136,29 @@ theory MemAddr
(* Physical Address *)
+ function static_malloc int : int
+
+ predicate statically_allocated (base: int) =
+ base = 0 \/ static_malloc base > 0
+
+ (* Note: for now, we cannot prove that but Why3 does not see that the function
+ statically allocated uses static_malloc which is abstract. *)
+ lemma valid_pointers_are_statically_allocated:
+ forall a: addr, m: malloc, n: int.
+ valid_rd m a n -> statically_allocated (a.base)
+
function int_of_addr addr: int
function addr_of_int int: addr
+ axiom addr_of_null :
+ int_of_addr null = 0
+
+ axiom addr_of_int_bijection :
+ forall p:addr.
+ statically_allocated p.base -> addr_of_int (int_of_addr p) = p
+
+ (* Table of offsets *)
+
type table (* abstract for now, but can be more elaborated later on *)
function table_of_base int: table
function table_to_offset table int: int
@@ -150,13 +170,4 @@ theory MemAddr
forall t: table. forall o1 o2: int.
o1 <= o2 <-> table_to_offset t o1 <= table_to_offset t o2
- axiom int_of_addr_bijection :
- forall a:int. int_of_addr (addr_of_int a) = a
-
- axiom addr_of_int_bijection :
- forall p:addr. addr_of_int (int_of_addr p) = p
-
- axiom addr_of_null :
- int_of_addr null = 0
-
end
--
GitLab