From de4c7793187af93a2ce642bd9d4b027ed7053d15 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 26 Mar 2020 11:03:27 +0100
Subject: [PATCH] [wp] implement OBJ validity access mode
---
src/plugins/wp/Cvalues.ml | 5 ++
src/plugins/wp/Cvalues.mli | 1 +
src/plugins/wp/LogicSemantics.ml | 6 +-
src/plugins/wp/MemMemory.ml | 1 +
src/plugins/wp/MemMemory.mli | 1 +
src/plugins/wp/MemTyped.ml | 6 +-
src/plugins/wp/MemVar.ml | 60 +++++++++++++------
src/plugins/wp/Sigs.ml | 1 +
.../wp/share/why3/frama_c_wp/memory.mlw | 5 +-
9 files changed, 61 insertions(+), 25 deletions(-)
diff --git a/src/plugins/wp/Cvalues.ml b/src/plugins/wp/Cvalues.ml
index 5440affcb5d..10fa328fa1b 100644
--- a/src/plugins/wp/Cvalues.ml
+++ b/src/plugins/wp/Cvalues.ml
@@ -357,6 +357,11 @@ let plain lt e =
type 'a printer = Format.formatter -> 'a -> unit
+let pp_acs fmt = function
+ | RW -> Format.pp_print_string fmt "RW"
+ | RD -> Format.pp_print_string fmt "RD"
+ | OBJ -> Format.pp_print_string fmt "OBJ"
+
let pp_bound fmt = function None -> () | Some p -> F.pp_term fmt p
let pp_value pp fmt = function
diff --git a/src/plugins/wp/Cvalues.mli b/src/plugins/wp/Cvalues.mli
index 1393505ab5a..f98a7923cb5 100644
--- a/src/plugins/wp/Cvalues.mli
+++ b/src/plugins/wp/Cvalues.mli
@@ -35,6 +35,7 @@ val equation : Sigs.equation -> pred
type 'a printer = Format.formatter -> 'a -> unit
+val pp_acs : acs printer
val pp_bound : term option printer
val pp_value : 'a printer -> 'a value printer
val pp_logic : 'a printer -> 'a logic printer
diff --git a/src/plugins/wp/LogicSemantics.ml b/src/plugins/wp/LogicSemantics.ml
index 825ace458d1..2a90684fe56 100644
--- a/src/plugins/wp/LogicSemantics.ml
+++ b/src/plugins/wp/LogicSemantics.ml
@@ -871,11 +871,7 @@ struct
| Pvalid(label,t) -> valid env RW label t
| Pvalid_read(label,t) -> valid env RD label t
-
- | Pobject_pointer(_label,_t) ->
- Warning.error
- "\\object_pointer not yet implemented@\n\
- @[<hov 0>(%a)@]" Printer.pp_predicate p
+ | Pobject_pointer(label,t) -> valid env OBJ label t
| Pvalid_function _t ->
Warning.error
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 4551f143c0d..8352296e1df 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -62,6 +62,7 @@ let l_havoc = Qed.Engine.{
let p_valid_rd = Lang.extern_fp ~library "valid_rd"
let p_valid_rw = Lang.extern_fp ~library "valid_rw"
+let p_valid_obj = Lang.extern_fp ~library "valid_obj"
let p_invalid = Lang.extern_fp ~library "invalid"
let p_separated = Lang.extern_fp ~library "separated"
let p_included = Lang.extern_fp ~library "included"
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index 0a92156a9ed..ab60842d69a 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -62,6 +62,7 @@ val p_separated : lfun
val p_included : lfun
val p_valid_rd : lfun
val p_valid_rw : lfun
+val p_valid_obj : lfun
val p_invalid : lfun
val p_eqmem : lfun
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 9dce8f268df..e1317a92d94 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -954,7 +954,11 @@ let loc_diff obj p q =
(* -------------------------------------------------------------------------- *)
let s_valid sigma acs p n =
- let p_valid = match acs with RW -> p_valid_rw | RD -> p_valid_rd in
+ let p_valid = match acs with
+ | RW -> p_valid_rw
+ | RD -> p_valid_rd
+ | OBJ -> p_valid_obj
+ in
p_call p_valid [Sigma.value sigma T_alloc;p;n]
let s_invalid sigma p n =
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index ca7a5873b1d..fd09f824c2c 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -739,6 +739,9 @@ struct
let fits_inside cond a b n =
p_leq e_zero a :: p_lt b (e_int n) :: cond
+ let fits_off_by_one cond a b n =
+ p_leq e_zero a :: p_leq b (e_int n) :: cond
+
let stay_outside cond a b n =
p_lt b e_zero :: p_leq (e_int n) a :: cond
@@ -754,6 +757,13 @@ struct
| Some( _ , None ) -> unsized_array ()
| None -> raise ShiftMismatch
+ (* Append conditions for and array offset (te,k) to fits in obj *)
+ let array_check fitting cond te k obj =
+ match Ctypes.get_array obj with
+ | Some( e , Some n ) when Ctypes.equal e te -> fitting cond k k n
+ | Some( _ , None ) -> unsized_array ()
+ | _ -> block_check fitting cond (obj,1) (te,k,k)
+
(* Append conditions for [offset] to fits [object], provided [a<=b]. *)
let rec offset_fits cond obj offset =
match offset with
@@ -761,14 +771,8 @@ struct
| Field fd :: ofs ->
offset_fits cond (Ctypes.object_of fd.ftype) ofs
| Shift(te,k) :: ofs ->
- match Ctypes.get_array obj with
- | Some( e , Some n ) when Ctypes.equal e te ->
- let cond = p_leq e_zero k :: p_lt k (e_int n) :: cond in
- offset_fits cond e ofs
- | Some( _ , None ) -> unsized_array ()
- | _ ->
- let cond = block_check fits_inside cond (obj,1) (te,k,k) in
- offset_fits cond te ofs
+ let cond = array_check fits_inside cond te k obj in
+ offset_fits cond te ofs
(* Append conditions to [cond] for [range=(elt,a,b)], starting at [offset],
consisting of [a..b] elements with type [elt] to fits inside the block,
@@ -796,19 +800,39 @@ struct
(* --- Validity --- *)
(* -------------------------------------------------------------------------- *)
- let valid_offset obj ofs =
- F.p_conj (offset_fits [] obj ofs)
-
- let valid_range obj ofs range =
- F.p_conj (range_check fits_inside [] (obj,1) ofs range)
+ let rec last_field_shift acs obj ofs =
+ match acs , obj , ofs with
+ | OBJ , _ , [Shift(te,k)] -> Some(te,k,obj)
+ | OBJ , C_comp c , (Field fd :: ofs) ->
+ begin
+ match List.rev c.cfields with
+ | fd0::_ when Fieldinfo.equal fd fd0 ->
+ last_field_shift acs (Ctypes.object_of fd.ftype) ofs
+ | _ -> None
+ end
+ | _ -> None
+
+ let valid_offset acs obj ofs =
+ match last_field_shift acs obj ofs with
+ | Some(te,k,obj) ->
+ F.p_conj (array_check fits_off_by_one [] te k obj)
+ | None ->
+ F.p_conj (offset_fits [] obj ofs)
+
+ let valid_range acs obj ofs range =
+ match last_field_shift acs obj ofs with
+ | Some _ ->
+ F.p_conj (range_check fits_off_by_one [] (obj,1) ofs range)
+ | _ ->
+ F.p_conj (range_check fits_inside [] (obj,1) ofs range)
(* varinfo *)
let valid_base sigma acs mem x =
if x.vglob then
- if acs = RW && Cil.typeHasQualifier "const" x.vtype
- then p_false
- else p_true
+ match acs with
+ | RW -> if Cil.typeHasQualifier "const" x.vtype then p_false else p_true
+ | RD | OBJ -> p_true
else
match mem with
| CVAL | HEAP -> p_bool (ALLOC.value sigma.alloc x)
@@ -819,12 +843,12 @@ struct
let valid_offset_path sigma acs mem x ofs =
p_and
(valid_base sigma acs mem x)
- (valid_offset (vobject mem x) ofs)
+ (valid_offset acs (vobject mem x) ofs)
let valid_range_path sigma acs mem x ofs rg =
p_and
(valid_base sigma acs mem x)
- (valid_range (vobject mem x) ofs rg)
+ (valid_range acs (vobject mem x) ofs rg)
(* in-model validation *)
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index c296519519c..72d1972ac59 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -46,6 +46,7 @@ type equation =
type acs =
| RW (** Read-Write Access *)
| RD (** Read-Only Access *)
+ | OBJ (** Valid Object Pointer *)
(** Abstract location or concrete value *)
type 'a value =
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 1dd6a2d7234..e91550d73ce 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -75,6 +75,9 @@ theory Memory
predicate valid_rd (m : map int int) (p:addr) (n:int) =
n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
+ predicate valid_obj (m : map int int) (p:addr) (n:int) =
+ n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] )
+
predicate invalid (m : map int int) (p:addr) (n:int) =
n > 0 -> ( m[p.base] <= p.offset \/ p.offset + n <= 0 )
@@ -170,4 +173,4 @@ theory Memory
axiom addr_of_null :
int_of_addr null = 0
-end
\ No newline at end of file
+end
--
GitLab