Merge branch 'feature/blanchard/wp/physical-addr' into 'master'

[wp] fix integer/pointer conversion

See merge request frama-c/frama-c!4779

src/plugins/wp/MemAddr.ml

@@ -49,13 +49,12 @@ let p_addr_lt = Lang.extern_p ~library ~bool:"addr_lt_bool" ~prop:"addr_lt" ()
 let p_addr_le = Lang.extern_p ~library ~bool:"addr_le_bool" ~prop:"addr_le" ()
 
 let f_addr_of_int = Lang.extern_f
-    ~category:Qed.Logic.Injection
     ~library ~result:t_addr "addr_of_int"
 
 let f_int_of_addr = Lang.extern_f
-    ~category:Qed.Logic.Injection
     ~library ~result:Qed.Logic.Int "int_of_addr"
 
+let p_statically_allocated = Lang.extern_fp ~library "statically_allocated"
 
 let f_table_of_base = Lang.extern_f ~library
     ~category:Qed.Logic.Function ~result:t_table "table_of_base"
@@ -79,6 +78,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 +87,45 @@ 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 ]
 
+let static_alloc addr = p_call p_statically_allocated [ addr ]
+(* This last function is not exposed, it does not have a particular meaning in
+   ACSL, and is used only for int/addr conversions.
+*)
+
+let in_uintptr_range addr =
+  p_hyps [ static_alloc @@ base addr ] @@
+  Cint.range (Ctypes.c_ptr ()) @@ 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 +314,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                                        --- *)

src/plugins/wp/MemAddr.mli

@@ -52,12 +52,24 @@ val global : term -> term
 val shift : term -> term -> term
 (** [shift (a: addr) (k: int) : addr = { a with offset = a.offset + k } ]*)
 
+(** {2 Comparisons} *)
+
 val addr_lt : term -> term -> pred
 (** [addr_lt(a: addr) (b: addr) = a < b] *)
 
 val addr_le : term -> term -> pred
 (** [addr_le(a: addr) (b: addr) = a <= b] *)
 
+(** {2 Physical addresses} *)
+
+val static_alloc : term -> pred
+(** [statically_allocated (base: int)]
+    The base has an associated static allocation, guaranteeing that the
+    addresses that use this base can be translated to integers and back.
+
+    @since Frama-C+dev
+*)
+
 val addr_of_int : term -> term
 (** [addr_of_int(i: int) : addr]
     Abstract: Conversion from integer to address
@@ -68,6 +80,17 @@ val int_of_addr : term -> term
     Abstract: Conversion from address to integer
 *)
 
+val in_uintptr_range : term -> pred
+(** [in_uintptr_range (a: addr)] =
+    [statically_allocated(a.base) -> in_range(int_of_addr a)]
+
+    Assuming that the base of a statically exists, the conversion of the pointer
+    to a an integer produces a value that fits in [uintptr_t].
+
+    @since Frama-C+dev
+*)
+
+
 val base_offset : term -> term -> term
 (** [base_offset(base: int)(offset: int) : int]
     Converts a {i logic} offset (which is actually the address of a memory cell

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

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.0.res.oracle

-# frama-c -wp -wp-timeout 4 [...]
+# frama-c -wp -wp-timeout 6 [...]
 [kernel] Parsing user_init.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] [Valid] Goal init_exits (Cfg) (Unreachable)

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle

@@ -22,13 +22,13 @@
 [wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part2 (Tactics 2) (Qed 12/13) (Alt-Ergo 1/13) (Cached)
 [wp] [Valid] typed_init_t2_bis_v2_loop_assigns_part3 (Tactics 3) (Qed 34/34)
 [wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Tactic) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part2 (Tactics 2) (Qed 12/13) (Alt-Ergo 1/13) (Cached)
 [wp] [Valid] typed_init_t2_bis_v2_assigns_exit_part3 (Qed)
 [wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part1 (Qed)
-[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Tactic) (Alt-Ergo 2/2) (Cached)
+[wp] [Valid] typed_init_t2_bis_v2_assigns_normal_part2 (Tactics 2) (Qed 12/13) (Alt-Ergo 1/13) (Cached)
 [wp] Proved goals:   23 / 23
   Qed:            11
-  Script:         12 (Tactics 23) (Qed 162/175) (Alt-Ergo 13/175) (Cached)
+  Script:         12 (Tactics 25) (Qed 186/197) (Alt-Ergo 11/197) (Cached)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   init_t2_v2                3        -        8       100%

src/plugins/wp/tests/wp_typed/user_init.i

 /* run.config_qualif
 
-   OPT: -wp-prop=-lack,-tactic -wp-timeout 4
+   OPT: -wp-prop=-lack,-tactic -wp-timeout 6
    OPT: -wp-prop=tactic -wp-auto=wp:split,wp:range -wp-prover=tip,Alt-Ergo -wp-script dry
    OPT: -wp-prop=lack
  */