diff --git a/creusot-contracts/src/ptr_own.rs b/creusot-contracts/src/ptr_own.rs index 13f0e9ebe9..a6ff9b0efe 100644 --- a/creusot-contracts/src/ptr_own.rs +++ b/creusot-contracts/src/ptr_own.rs @@ -101,9 +101,11 @@ impl PtrOwn { /// If one owns two `PtrOwn`s in ghost code, then they are for different pointers. #[trusted] + #[pure] #[ensures(own1.ptr().addr_logic() != own2.ptr().addr_logic())] + #[ensures(*own1 == ^own1)] #[allow(unused_variables)] - pub fn disjoint_lemma(own1: &mut PtrOwn, own2: &mut PtrOwn) { + pub fn disjoint_lemma(own1: &mut PtrOwn, own2: &PtrOwn) { panic!() } } diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.coma b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.coma new file mode 100644 index 0000000000..a90bb0110f --- /dev/null +++ b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.coma @@ -0,0 +1,317 @@ +module M_disjoint_raw_ptr__foo [#"disjoint_raw_ptr.rs" 4 0 4 12] + let%span sdisjoint_raw_ptr0 = "disjoint_raw_ptr.rs" 5 37 5 41 + let%span sdisjoint_raw_ptr1 = "disjoint_raw_ptr.rs" 6 33 6 37 + let%span sdisjoint_raw_ptr2 = "disjoint_raw_ptr.rs" 11 18 11 30 + let%span sdisjoint_raw_ptr3 = "disjoint_raw_ptr.rs" 12 18 12 26 + let%span sptr_own4 = "../../../../creusot-contracts/src/ptr_own.rs" 52 15 52 16 + let%span sptr_own5 = "../../../../creusot-contracts/src/ptr_own.rs" 52 4 52 56 + let%span sptr_own6 = "../../../../creusot-contracts/src/ptr_own.rs" 51 14 51 64 + let%span sghost7 = "../../../../creusot-contracts/src/ghost.rs" 217 9 217 15 + let%span sghost8 = "../../../../creusot-contracts/src/ghost.rs" 138 27 138 31 + let%span sghost9 = "../../../../creusot-contracts/src/ghost.rs" 138 4 138 52 + let%span sghost10 = "../../../../creusot-contracts/src/ghost.rs" 137 14 137 39 + let%span sghost11 = "../../../../creusot-contracts/src/ghost.rs" 85 22 85 26 + let%span sghost12 = "../../../../creusot-contracts/src/ghost.rs" 85 4 85 48 + let%span sghost13 = "../../../../creusot-contracts/src/ghost.rs" 84 14 84 36 + let%span sghost14 = "../../../../creusot-contracts/src/ghost.rs" 124 19 124 23 + let%span sghost15 = "../../../../creusot-contracts/src/ghost.rs" 124 4 124 40 + let%span sghost16 = "../../../../creusot-contracts/src/ghost.rs" 123 14 123 35 + let%span sghost17 = "../../../../creusot-contracts/src/ghost.rs" 69 14 69 18 + let%span sghost18 = "../../../../creusot-contracts/src/ghost.rs" 69 4 69 36 + let%span sghost19 = "../../../../creusot-contracts/src/ghost.rs" 68 14 68 35 + let%span sptr_own20 = "../../../../creusot-contracts/src/ptr_own.rs" 108 26 108 30 + let%span sptr_own21 = "../../../../creusot-contracts/src/ptr_own.rs" 108 48 108 52 + let%span sptr_own22 = "../../../../creusot-contracts/src/ptr_own.rs" 105 14 105 64 + let%span sptr_own23 = "../../../../creusot-contracts/src/ptr_own.rs" 106 14 106 28 + let%span sghost24 = "../../../../creusot-contracts/src/ghost.rs" 181 15 181 16 + let%span sghost25 = "../../../../creusot-contracts/src/ghost.rs" 181 4 181 28 + let%span sghost26 = "../../../../creusot-contracts/src/ghost.rs" 179 14 179 28 + let%span sghost27 = "../../../../creusot-contracts/src/ghost.rs" 110 8 110 24 + let%span sresolve28 = "../../../../creusot-contracts/src/resolve.rs" 54 20 54 34 + let%span sresolve29 = "../../../../creusot-contracts/src/resolve.rs" 68 8 68 23 + + use prelude.prelude.Int32 + + predicate inv'0 (_1 : int32) + + axiom inv_axiom'0 [@rewrite] : forall x : int32 [inv'0 x] . inv'0 x = true + + use prelude.prelude.Opaque + + type t_PtrOwn'0 + + type t_GhostBox'0 = + { t_GhostBox__0'0: t_PtrOwn'0 } + + predicate inv'1 (_1 : (opaque_ptr, t_GhostBox'0)) + + axiom inv_axiom'1 [@rewrite] : forall x : (opaque_ptr, t_GhostBox'0) [inv'1 x] . inv'1 x = true + + function inner_logic'0 (self : t_GhostBox'0) : t_PtrOwn'0 = + [%#sghost7] self.t_GhostBox__0'0 + + use prelude.prelude.Borrow + + function ptr'0 (self : t_PtrOwn'0) : opaque_ptr + + function val'0 (self : t_PtrOwn'0) : int32 + + let rec new'0 (v:int32) (return' (ret:(opaque_ptr, t_GhostBox'0)))= {[@expl:new 'v' type invariant] [%#sptr_own4] inv'0 v} + any + [ return' (result:(opaque_ptr, t_GhostBox'0))-> {[%#sptr_own5] inv'1 result} + {[%#sptr_own6] ptr'0 (inner_logic'0 (let (_, a) = result in a)) = (let (a, _) = result in a) + /\ val'0 (inner_logic'0 (let (_, a) = result in a)) = v} + (! return' {result}) ] + + + predicate inv'2 (_1 : borrowed (t_GhostBox'0)) + + axiom inv_axiom'2 [@rewrite] : forall x : borrowed (t_GhostBox'0) [inv'2 x] . inv'2 x = true + + type t_GhostBox'2 = + { t_GhostBox__0'2: borrowed (t_PtrOwn'0) } + + predicate inv'3 (_1 : t_GhostBox'2) + + axiom inv_axiom'3 [@rewrite] : forall x : t_GhostBox'2 [inv'3 x] . inv'3 x = true + + let rec borrow_mut'0 (self:borrowed (t_GhostBox'0)) (return' (ret:t_GhostBox'2))= {[@expl:borrow_mut 'self' type invariant] [%#sghost8] inv'2 self} + any + [ return' (result:t_GhostBox'2)-> {[%#sghost9] inv'3 result} + {[%#sghost10] result.t_GhostBox__0'2 + = Borrow.borrow_logic (self.current).t_GhostBox__0'0 (self.final).t_GhostBox__0'0 (Borrow.inherit_id (Borrow.get_id self) 1)} + (! return' {result}) ] + + + predicate inv'4 (_1 : borrowed (t_GhostBox'2)) + + axiom inv_axiom'4 [@rewrite] : forall x : borrowed (t_GhostBox'2) [inv'4 x] . inv'4 x = true + + predicate inv'5 (_1 : borrowed (borrowed (t_PtrOwn'0))) + + axiom inv_axiom'5 [@rewrite] : forall x : borrowed (borrowed (t_PtrOwn'0)) [inv'5 x] . inv'5 x = true + + let rec deref_mut'0 (self:borrowed (t_GhostBox'2)) (return' (ret:borrowed (borrowed (t_PtrOwn'0))))= {[@expl:deref_mut 'self' type invariant] [%#sghost11] inv'4 self} + any + [ return' (result:borrowed (borrowed (t_PtrOwn'0)))-> {[%#sghost12] inv'5 result} + {[%#sghost13] result + = Borrow.borrow_logic (self.current).t_GhostBox__0'2 (self.final).t_GhostBox__0'2 (Borrow.inherit_id (Borrow.get_id self) 1)} + (! return' {result}) ] + + + predicate inv'6 (_1 : t_GhostBox'0) + + axiom inv_axiom'6 [@rewrite] : forall x : t_GhostBox'0 [inv'6 x] . inv'6 x = true + + type t_GhostBox'3 = + { t_GhostBox__0'3: t_PtrOwn'0 } + + predicate inv'7 (_1 : t_GhostBox'3) + + axiom inv_axiom'7 [@rewrite] : forall x : t_GhostBox'3 [inv'7 x] . inv'7 x = true + + let rec borrow'0 (self:t_GhostBox'0) (return' (ret:t_GhostBox'3))= {[@expl:borrow 'self' type invariant] [%#sghost14] inv'6 self} + any + [ return' (result:t_GhostBox'3)-> {[%#sghost15] inv'7 result} + {[%#sghost16] result.t_GhostBox__0'3 = self.t_GhostBox__0'0} + (! return' {result}) ] + + + predicate inv'8 (_1 : t_GhostBox'3) + + axiom inv_axiom'8 [@rewrite] : forall x : t_GhostBox'3 [inv'8 x] . inv'8 x = true + + predicate inv'9 (_1 : t_PtrOwn'0) + + axiom inv_axiom'9 [@rewrite] : forall x : t_PtrOwn'0 [inv'9 x] . inv'9 x = true + + let rec deref'0 (self:t_GhostBox'3) (return' (ret:t_PtrOwn'0))= {[@expl:deref 'self' type invariant] [%#sghost17] inv'8 self} + any + [ return' (result:t_PtrOwn'0)-> {[%#sghost18] inv'9 result} + {[%#sghost19] self.t_GhostBox__0'3 = result} + (! return' {result}) ] + + + predicate resolve'13 (_1 : t_PtrOwn'0) = + true + + predicate resolve'11 (self : t_PtrOwn'0) = + [%#sresolve29] resolve'13 self + + predicate resolve'8 (_1 : t_PtrOwn'0) = + resolve'11 _1 + + predicate resolve'4 (self : t_GhostBox'3) = + [%#sghost27] resolve'8 self.t_GhostBox__0'3 + + predicate resolve'0 (_1 : t_GhostBox'3) = + resolve'4 _1 + + predicate inv'10 (_1 : borrowed (t_PtrOwn'0)) + + axiom inv_axiom'10 [@rewrite] : forall x : borrowed (t_PtrOwn'0) [inv'10 x] . inv'10 x = true + + predicate inv'11 (_1 : t_PtrOwn'0) + + axiom inv_axiom'11 [@rewrite] : forall x : t_PtrOwn'0 [inv'11 x] . inv'11 x = true + + use prelude.prelude.Int + + function addr_logic'0 (self : opaque_ptr) : int + + let rec disjoint_lemma'0 (own1:borrowed (t_PtrOwn'0)) (own2:t_PtrOwn'0) (return' (ret:()))= {[@expl:disjoint_lemma 'own1' type invariant] [%#sptr_own20] inv'10 own1} + {[@expl:disjoint_lemma 'own2' type invariant] [%#sptr_own21] inv'11 own2} + any + [ return' (result:())-> {[%#sptr_own22] addr_logic'0 (ptr'0 own1.current) <> addr_logic'0 (ptr'0 own2)} + {[%#sptr_own23] own1.current = own1.final} + (! return' {result}) ] + + + predicate resolve'15 (self : borrowed (t_PtrOwn'0)) = + [%#sresolve28] self.final = self.current + + predicate resolve'14 (_1 : borrowed (t_PtrOwn'0)) = + resolve'15 _1 + + predicate resolve'12 (self : borrowed (t_PtrOwn'0)) = + [%#sresolve29] resolve'14 self + + predicate resolve'9 (_1 : borrowed (t_PtrOwn'0)) = + resolve'12 _1 + + predicate resolve'5 (self : t_GhostBox'2) = + [%#sghost27] resolve'9 self.t_GhostBox__0'2 + + predicate resolve'1 (_1 : t_GhostBox'2) = + resolve'5 _1 + + predicate resolve'6 (self : borrowed (borrowed (t_PtrOwn'0))) = + [%#sresolve28] self.final = self.current + + predicate resolve'2 (_1 : borrowed (borrowed (t_PtrOwn'0))) = + resolve'6 _1 + + type closure0'1 = + { field_0'0: borrowed (t_GhostBox'0); field_1'0: t_GhostBox'0 } + + predicate resolve'10 (self : borrowed (t_GhostBox'0)) = + [%#sresolve28] self.final = self.current + + predicate resolve'7 (_1 : borrowed (t_GhostBox'0)) = + resolve'10 _1 + + predicate resolve'3 (_1 : closure0'1) = + resolve'7 _1.field_0'0 + + predicate inv'12 (_1 : ()) + + axiom inv_axiom'12 [@rewrite] : forall x : () [inv'12 x] . inv'12 x = true + + type t_GhostBox'1 = + { t_GhostBox__0'1: () } + + predicate inv'13 (_1 : t_GhostBox'1) + + axiom inv_axiom'13 [@rewrite] : forall x : t_GhostBox'1 [inv'13 x] . inv'13 x = true + + let rec new'1 (x:()) (return' (ret:t_GhostBox'1))= {[@expl:new 'x' type invariant] [%#sghost24] inv'12 x} + any + [ return' (result:t_GhostBox'1)-> {[%#sghost25] inv'13 result} + {[%#sghost26] result.t_GhostBox__0'1 = x} + (! return' {result}) ] + + + use prelude.prelude.Intrinsic + + let rec closure0'0 (_1:closure0'1) (return' (ret:t_GhostBox'1))= bb0 + [ bb0 = s0 + [ s0 = Borrow.borrow_final {(_1.field_0'0).current} {Borrow.get_id _1.field_0'0} + (fun (_ret':borrowed (t_GhostBox'0)) -> + [ &_8 <- _ret' ] + [ &_1 <- { _1 with field_0'0 = { _1.field_0'0 with current = _ret'.final } } ] + s1) + | s1 = borrow_mut'0 {_8} (fun (_ret':t_GhostBox'2) -> [ &_7 <- _ret' ] s2) + | s2 = bb1 ] + + | bb1 = s0 + [ s0 = Borrow.borrow_mut {_7} + (fun (_ret':borrowed (t_GhostBox'2)) -> [ &_6 <- _ret' ] [ &_7 <- _ret'.final ] s1) + | s1 = deref_mut'0 {_6} (fun (_ret':borrowed (borrowed (t_PtrOwn'0))) -> [ &_5 <- _ret' ] s2) + | s2 = bb2 ] + + | bb2 = s0 + [ s0 = Borrow.borrow_mut {(_5.current).current} + (fun (_ret':borrowed (t_PtrOwn'0)) -> + [ &_4 <- _ret' ] + [ &_5 <- { _5 with current = { _5.current with current = _ret'.final } } ] + s1) + | s1 = borrow'0 {_1.field_1'0} (fun (_ret':t_GhostBox'3) -> [ &_12 <- _ret' ] s2) + | s2 = bb3 ] + + | bb3 = s0 [ s0 = deref'0 {_12} (fun (_ret':t_PtrOwn'0) -> [ &_10 <- _ret' ] s1) | s1 = bb4 ] + | bb4 = s0 + [ s0 = -{resolve'0 _12}- s1 + | s1 = disjoint_lemma'0 {_4} {_10} (fun (_ret':()) -> [ &_3 <- _ret' ] s2) + | s2 = bb5 ] + + | bb5 = s0 [ s0 = -{resolve'1 _7}- s1 | s1 = -{resolve'2 _5}- s2 | s2 = -{resolve'3 _1}- s3 | s3 = bb6 ] + | bb6 = bb7 + | bb7 = s0 [ s0 = new'1 {_2} (fun (_ret':t_GhostBox'1) -> [ &_0 <- _ret' ] s1) | s1 = bb8 ] + | bb8 = return' {_0} ] + + [ & _0 : t_GhostBox'1 = any_l () + | & _1 : closure0'1 = _1 + | & _2 : () = any_l () + | & _3 : () = any_l () + | & _4 : borrowed (t_PtrOwn'0) = any_l () + | & _5 : borrowed (borrowed (t_PtrOwn'0)) = any_l () + | & _6 : borrowed (t_GhostBox'2) = any_l () + | & _7 : t_GhostBox'2 = any_l () + | & _8 : borrowed (t_GhostBox'0) = any_l () + | & _10 : t_PtrOwn'0 = any_l () + | & _12 : t_GhostBox'3 = any_l () ] + [ return' (result:t_GhostBox'1)-> return' {result} ] + + meta "compute_max_steps" 1000000 + + let rec foo'0 (_1:()) (return' (ret:()))= (! bb0 + [ bb0 = s0 + [ s0 = new'0 {[%#sdisjoint_raw_ptr0] (1 : int32)} (fun (_ret':(opaque_ptr, t_GhostBox'0)) -> [ &_3 <- _ret' ] s1) + | s1 = bb1 ] + + | bb1 = s0 + [ s0 = [ &p1 <- let (r'0, _) = _3 in r'0 ] s1 | s1 = [ &own1 <- let (_, r'1) = _3 in r'1 ] s2 | s2 = bb2 ] + + | bb2 = s0 + [ s0 = new'0 {[%#sdisjoint_raw_ptr1] (1 : int32)} (fun (_ret':(opaque_ptr, t_GhostBox'0)) -> [ &_6 <- _ret' ] s1) + | s1 = bb3 ] + + | bb3 = s0 + [ s0 = [ &p2 <- let (r'0, _) = _6 in r'0 ] s1 | s1 = [ &own2 <- let (_, r'1) = _6 in r'1 ] s2 | s2 = bb4 ] + + | bb4 = s0 + [ s0 = Borrow.borrow_mut {own1} + (fun (_ret':borrowed (t_GhostBox'0)) -> [ &_9 <- _ret' ] [ &own1 <- _ret'.final ] s1) + | s1 = [ &_8 <- { field_0'0 = _9; field_1'0 = own2 } ] s2 + | s2 = closure0'0 {_8} (fun (_ret':t_GhostBox'1) -> [ &_7 <- _ret' ] s3) + | s3 = bb5 ] + + | bb5 = bb6 + | bb6 = s0 [ s0 = {[@expl:assertion] [%#sdisjoint_raw_ptr2] own1 <> own2} s1 | s1 = bb7 ] + | bb7 = s0 [ s0 = {[@expl:assertion] [%#sdisjoint_raw_ptr3] p1 <> p2} s1 | s1 = bb8 ] + | bb8 = bb9 + | bb9 = return' {_0} ] + ) + [ & _0 : () = any_l () + | & p1 : opaque_ptr = any_l () + | & own1 : t_GhostBox'0 = any_l () + | & _3 : (opaque_ptr, t_GhostBox'0) = any_l () + | & p2 : opaque_ptr = any_l () + | & own2 : t_GhostBox'0 = any_l () + | & _6 : (opaque_ptr, t_GhostBox'0) = any_l () + | & _7 : t_GhostBox'1 = any_l () + | & _8 : closure0'1 = any_l () + | & _9 : borrowed (t_GhostBox'0) = any_l () + | & _11 : () = any_l () ] + [ return' (result:())-> (! return' {result}) ] +end diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.rs b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.rs new file mode 100644 index 0000000000..e652b0677e --- /dev/null +++ b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr.rs @@ -0,0 +1,13 @@ +extern crate creusot_contracts; +use creusot_contracts::{ptr_own::PtrOwn, *}; + +pub fn foo() { + let (p1, mut own1) = PtrOwn::new(1i32); + let (p2, own2) = PtrOwn::new(1i32); + + ghost! { + let _ = PtrOwn::disjoint_lemma(*own1.borrow_mut(), *own2.borrow()); + }; + proof_assert!(own1 != own2); + proof_assert!(p1 != p2); +} diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3session.xml b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3session.xml new file mode 100644 index 0000000000..b84c1fca39 --- /dev/null +++ b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3session.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3shapes.gz b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3shapes.gz new file mode 100644 index 0000000000..934ea64a7b Binary files /dev/null and b/creusot/tests/should_succeed/ghost/disjoint_raw_ptr/why3shapes.gz differ