Commit de4c7793 authored by Loïc Correnson's avatar Loïc Correnson Committed by David Bühler
Browse files

[wp] implement OBJ validity access mode

parent ac4373cc
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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"
......
......@@ -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
......
......@@ -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 =
......
......@@ -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 *)
......
......@@ -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 =
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment