Skip to content

Commit

Permalink
Fix spec that GhostPtrToken's don't contain null pointers to apply …
Browse files Browse the repository at this point in the history 
…to `Ref` and `Mut` variants
  • Loading branch information
@dewert99
dewert99 committed Aug 3, 2024
1 parent 97ba0c3 commit 27c38af
Show file tree
Hide file tree
Showing 5 changed files with 264 additions and 145 deletions.
5 changes: 4 additions & 1 deletion creusot-contracts/src/ghost_ptr.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@ impl<T: ?Sized> ShallowModel for GhostPtrToken<T> {

#[trusted]
#[logic]
#[ensures(result.get(GhostPtr::null_logic()) == None)]
#[open(self)]
fn shallow_model(self) -> Self::ShallowModelTy {
absurd
Expand Down Expand Up @@ -132,7 +133,6 @@ impl<T: ?Sized> GhostPtrExt<T> for GhostPtr<T> {
#[trusted]
#[open(self)]
#[logic]
#[ensures(forall<t: GhostPtrToken<T>> !t@.contains(result))]
#[ensures(result.addr_logic() == 0)]
#[ensures(forall<ptr: GhostPtr<T>> ptr.addr_logic() == result.addr_logic() ==> ptr == result)]
fn null_logic() -> Self {
Expand All @@ -153,6 +153,7 @@ impl<'a, T: ?Sized> ShallowModel for GhostPtrTokenRef<'a, T> {
#[trusted]
#[logic]
#[open(self)]
#[ensures(result.get(GhostPtr::null_logic()) == None)]
fn shallow_model(self) -> Self::ShallowModelTy {
absurd
}
Expand Down Expand Up @@ -197,13 +198,15 @@ impl<'a, T: ?Sized> GhostPtrTokenMut<'a, T> {
#[trusted]
#[logic]
#[open(self)]
#[ensures(result.get(GhostPtr::null_logic()) == None)]
pub fn cur(self) -> FMap<GhostPtr<T>, T> {
absurd
}

#[trusted]
#[logic(prophetic)]
#[open(self)]
#[ensures(result.get(GhostPtr::null_logic()) == None)]
pub fn fin(self) -> FMap<GhostPtr<T>, T> {
absurd
}
Expand Down
99 changes: 59 additions & 40 deletions creusot/tests/should_succeed/bug/949.coma
View file
Original file line number Diff line number Diff line change
Expand Up @@ -127,47 +127,55 @@ module C949_Main

let%span span26 = "../../../../../creusot-contracts/src/logic/fmap.rs" 62 8 62 27

let%span span27 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 96 4 96 39
let%span span27 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 136 14 136 38

let%span span28 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 97 14 97 54
let%span span28 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 137 4 137 98

let%span span29 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 98 14 98 46
let%span span29 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 32 14 32 56

let%span span30 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 99 4 99 57
let%span span30 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 34 4 34 50

let%span span31 = "../../../../../creusot-contracts/src/util.rs" 16 19 16 23
let%span span31 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 97 4 97 39

let%span span32 = "../../../../../creusot-contracts/src/util.rs" 15 14 15 30
let%span span32 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 98 14 98 54

let%span span33 = "../../../../../creusot-contracts/src/util.rs" 16 4 16 40
let%span span33 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 99 14 99 46

let%span span34 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 18 38 22
let%span span34 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 100 4 100 57

let%span span35 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 24 38 25
let%span span35 = "../../../../../creusot-contracts/src/util.rs" 16 19 16 23

let%span span36 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 30 38 31
let%span span36 = "../../../../../creusot-contracts/src/util.rs" 15 14 15 30

let%span span37 = "../../../../../creusot-contracts/src/logic/fmap.rs" 35 14 35 71
let%span span37 = "../../../../../creusot-contracts/src/util.rs" 16 4 16 40

let%span span38 = "../../../../../creusot-contracts/src/logic/fmap.rs" 36 4 36 63
let%span span38 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 18 38 22

let%span span39 = "../../../../../creusot-contracts/src/logic/fmap.rs" 37 4 37 68
let%span span39 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 24 38 25

let%span span40 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 4 38 43
let%span span40 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 30 38 31

let%span span41 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 70 35 70 38
let%span span41 = "../../../../../creusot-contracts/src/logic/fmap.rs" 35 14 35 71

let%span span42 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 66 4 66 42
let%span span42 = "../../../../../creusot-contracts/src/logic/fmap.rs" 36 4 36 63

let%span span43 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 69 14 69 55
let%span span43 = "../../../../../creusot-contracts/src/logic/fmap.rs" 37 4 37 68

let%span span44 = "../../../../../creusot-contracts/src/logic/fmap.rs" 85 14 85 31
let%span span44 = "../../../../../creusot-contracts/src/logic/fmap.rs" 38 4 38 43

let%span span45 = "../../../../../creusot-contracts/src/logic/fmap.rs" 86 14 86 49
let%span span45 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 71 35 71 38

let%span span46 = "../../../../../creusot-contracts/src/logic/fmap.rs" 87 4 87 26
let%span span46 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 67 4 67 42

let%span span47 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 40 14 40 38
let%span span47 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 70 14 70 55

let%span span48 = "../../../../../creusot-contracts/src/logic/fmap.rs" 85 14 85 31

let%span span49 = "../../../../../creusot-contracts/src/logic/fmap.rs" 86 14 86 49

let%span span50 = "../../../../../creusot-contracts/src/logic/fmap.rs" 87 4 87 26

let%span span51 = "../../../../../creusot-contracts/src/ghost_ptr.rs" 41 14 41 38

use prelude.prelude.Int32

Expand Down Expand Up @@ -283,51 +291,62 @@ module C949_Main
function lookup_unsized'0 [@inline:trivial] (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) : int32 =
[%#span26] unwrap'0 (get'0 self k)

function addr_logic'0 (self : opaque_ptr) : int

function null_logic'0 (_1 : ()) : opaque_ptr

axiom null_logic'0_spec : forall _1 : () . ([%#span28] forall ptr : opaque_ptr . addr_logic'0 ptr
= addr_logic'0 (null_logic'0 _1) -> ptr = null_logic'0 _1)
&& ([%#span27] addr_logic'0 (null_logic'0 _1) = 0)

function shallow_model'0 (self : GhostPtrToken'0.t_ghostptrtoken int32) : FMap'0.t_fmap opaque_ptr int32

axiom shallow_model'0_spec : forall self : GhostPtrToken'0.t_ghostptrtoken int32 . ([%#span30] inv'1 (shallow_model'0 self))
&& ([%#span29] get'0 (shallow_model'0 self) (null_logic'0 ()) = Option'0.C_None)

use prelude.prelude.Borrow

let rec ptr_to_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (ptr:opaque_ptr) (return' (ret:int32))= {[@expl:precondition] [%#span27] contains'0 (shallow_model'0 self.current) ptr}
let rec ptr_to_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (ptr:opaque_ptr) (return' (ret:int32))= {[@expl:precondition] [%#span31] contains'0 (shallow_model'0 self.current) ptr}
any
[ return' (result:int32)-> {[%#span30] inv'0 result}
{[%#span29] shallow_model'0 self.final = remove'0 (shallow_model'0 self.current) ptr}
{[%#span28] result = lookup_unsized'0 (shallow_model'0 self.current) ptr}
[ return' (result:int32)-> {[%#span34] inv'0 result}
{[%#span33] shallow_model'0 self.final = remove'0 (shallow_model'0 self.current) ptr}
{[%#span32] result = lookup_unsized'0 (shallow_model'0 self.current) ptr}
(! return' {result}) ]


function make_sized'0 (self : int32) : int32

axiom make_sized'0_spec : forall self : int32 . ([%#span31] inv'5 self)
-> ([%#span33] inv'0 (make_sized'0 self)) && ([%#span32] make_sized'0 self = self)
axiom make_sized'0_spec : forall self : int32 . ([%#span35] inv'5 self)
-> ([%#span37] inv'0 (make_sized'0 self)) && ([%#span36] make_sized'0 self = self)

function insert'0 (self : FMap'0.t_fmap opaque_ptr int32) (k : opaque_ptr) (v : int32) : FMap'0.t_fmap opaque_ptr int32


axiom insert'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr, v : int32 . ([%#span34] inv'1 self)
-> ([%#span35] inv'2 k)
-> ([%#span36] inv'3 v)
-> ([%#span40] inv'1 (insert'0 self k v))
&& ([%#span39] not contains'0 self k -> len'0 (insert'0 self k v) = len'0 self + 1)
&& ([%#span38] contains'0 self k -> len'0 (insert'0 self k v) = len'0 self)
&& ([%#span37] view'0 (insert'0 self k v) = Map.set (view'0 self) k (Option'0.C_Some (make_sized'0 v)))
axiom insert'0_spec : forall self : FMap'0.t_fmap opaque_ptr int32, k : opaque_ptr, v : int32 . ([%#span38] inv'1 self)
-> ([%#span39] inv'2 k)
-> ([%#span40] inv'3 v)
-> ([%#span44] inv'1 (insert'0 self k v))
&& ([%#span43] not contains'0 self k -> len'0 (insert'0 self k v) = len'0 self + 1)
&& ([%#span42] contains'0 self k -> len'0 (insert'0 self k v) = len'0 self)
&& ([%#span41] view'0 (insert'0 self k v) = Map.set (view'0 self) k (Option'0.C_Some (make_sized'0 v)))

let rec ptr_from_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (val':int32) (return' (ret:opaque_ptr))= {[@expl:precondition] [%#span41] inv'0 val'}
let rec ptr_from_box'0 (self:borrowed (GhostPtrToken'0.t_ghostptrtoken int32)) (val':int32) (return' (ret:opaque_ptr))= {[@expl:precondition] [%#span45] inv'0 val'}
any
[ return' (result:opaque_ptr)-> {[%#span43] shallow_model'0 self.final
[ return' (result:opaque_ptr)-> {[%#span47] shallow_model'0 self.final
= insert'0 (shallow_model'0 self.current) result val'}
{[%#span42] not contains'0 (shallow_model'0 self.current) result}
{[%#span46] not contains'0 (shallow_model'0 self.current) result}
(! return' {result}) ]


use map.Const

function empty'0 (_1 : ()) : FMap'0.t_fmap opaque_ptr int32

axiom empty'0_spec : forall _1 : () . ([%#span46] inv'1 (empty'0 _1))
&& ([%#span45] view'0 (empty'0 _1) = Const.const (Option'0.C_None)) && ([%#span44] len'0 (empty'0 _1) = 0)
axiom empty'0_spec : forall _1 : () . ([%#span50] inv'1 (empty'0 _1))
&& ([%#span49] view'0 (empty'0 _1) = Const.const (Option'0.C_None)) && ([%#span48] len'0 (empty'0 _1) = 0)

let rec new'0 (_1:()) (return' (ret:GhostPtrToken'0.t_ghostptrtoken int32))= any
[ return' (result:GhostPtrToken'0.t_ghostptrtoken int32)-> {[%#span47] shallow_model'0 result = empty'0 ()}
[ return' (result:GhostPtrToken'0.t_ghostptrtoken int32)-> {[%#span51] shallow_model'0 result = empty'0 ()}
(! return' {result}) ]


Expand Down
Loading

0 comments on commit 27c38af

Please sign in to comment.