diff --git a/creusot/tests/should_succeed/type_invariants/generated.mlcfg b/creusot/tests/should_succeed/type_invariants/generated.mlcfg index 1c70b03b03..7ba47f00d6 100644 --- a/creusot/tests/should_succeed/type_invariants/generated.mlcfg +++ b/creusot/tests/should_succeed/type_invariants/generated.mlcfg @@ -1,14 +1,38 @@ -module Core_Option_Option_Type - type t_option 't = - | C_None - | C_Some 't +module Generated_Sum10_Type + use prelude.Int + use prelude.Int32 + type t_sum10 = + | C_Sum10 int32 int32 + + let function sum10_0 (self : t_sum10) : int32 = [@vc:do_not_keep_trace] [@vc:sp] + match (self) with + | C_Sum10 a _ -> a + end + let function sum10_1 (self : t_sum10) : int32 = [@vc:do_not_keep_trace] [@vc:sp] + match (self) with + | C_Sum10 _ a -> a + end +end +module Generated_Impl0_UserInv_Stub + use Generated_Sum10_Type as Generated_Sum10_Type + predicate user_inv [#"../generated.rs" 11 4 11 29] (self : Generated_Sum10_Type.t_sum10) +end +module Generated_Impl0_UserInv_Interface + use Generated_Sum10_Type as Generated_Sum10_Type + predicate user_inv [#"../generated.rs" 11 4 11 29] (self : Generated_Sum10_Type.t_sum10) + val user_inv [#"../generated.rs" 11 4 11 29] (self : Generated_Sum10_Type.t_sum10) : bool + ensures { result = user_inv self } end -module Generated_List_Type - use Core_Option_Option_Type as Core_Option_Option_Type - type t_list 't = - | C_List 't (Core_Option_Option_Type.t_option (t_list 't)) +module Generated_Impl0_UserInv + use prelude.Int32 + use prelude.Int + use Generated_Sum10_Type as Generated_Sum10_Type + predicate user_inv [#"../generated.rs" 11 4 11 29] (self : Generated_Sum10_Type.t_sum10) = + [#"../generated.rs" 12 20 12 43] Int32.to_int (Generated_Sum10_Type.sum10_0 self) + Int32.to_int (Generated_Sum10_Type.sum10_1 self) = 10 + val user_inv [#"../generated.rs" 11 4 11 29] (self : Generated_Sum10_Type.t_sum10) : bool + ensures { result = user_inv self } end module CreusotContracts_Invariant_Inv_Stub @@ -29,6 +53,16 @@ module CreusotContracts_Invariant_Inv val inv (_x : t) : bool ensures { result = inv _x } +end +module Generated_Foo_Type + use prelude.Borrow + use prelude.Int + use prelude.UIntSize + use Generated_Sum10_Type as Generated_Sum10_Type + type t_foo 't = + | C_A (borrowed (Generated_Sum10_Type.t_sum10)) usize + | C_B 't + end module CreusotContracts_Invariant_UserInv_UserInv_Stub type self @@ -48,20 +82,22 @@ module CreusotContracts_Invariant_UserInv_UserInv ensures { result = user_inv self } end -module Generated_List_Type_Inv +module Generated_Foo_Type_Inv type t - use Generated_List_Type as Generated_List_Type - use Core_Option_Option_Type as Core_Option_Option_Type + use prelude.Borrow + use Generated_Sum10_Type as Generated_Sum10_Type clone CreusotContracts_Invariant_Inv_Stub as Inv2 with - type t = Core_Option_Option_Type.t_option (Generated_List_Type.t_list t) - clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = t + use Generated_Foo_Type as Generated_Foo_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = borrowed (Generated_Sum10_Type.t_sum10) clone CreusotContracts_Invariant_UserInv_UserInv_Stub as UserInv0 with - type self = Generated_List_Type.t_list t + type self = Generated_Foo_Type.t_foo t clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = Generated_List_Type.t_list t - axiom inv_t_list : forall self : Generated_List_Type.t_list t . Inv0.inv self = (UserInv0.user_inv self /\ match (self) with - | Generated_List_Type.C_List a_0 a_1 -> Inv1.inv a_0 /\ Inv2.inv a_1 + type t = Generated_Foo_Type.t_foo t + axiom inv_t_foo : forall self : Generated_Foo_Type.t_foo t . Inv0.inv self = (UserInv0.user_inv self /\ match (self) with + | Generated_Foo_Type.C_A f1 _ -> Inv1.inv f1 + | Generated_Foo_Type.C_B a_0 -> Inv2.inv a_0 end) end module CreusotContracts_Invariant_Impl0_UserInv_Stub @@ -83,84 +119,129 @@ module CreusotContracts_Invariant_Impl0_UserInv ensures { result = user_inv self } end -module TyInv_Trivial - type t - clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = t - axiom inv_trivial : forall self : t . Inv0.inv self = true -end -module Core_Option_Option_Type_Inv +module TyInv_Borrow type t + use prelude.Borrow clone CreusotContracts_Invariant_Inv_Stub as Inv1 with type t = t - use Core_Option_Option_Type as Core_Option_Option_Type clone CreusotContracts_Invariant_UserInv_UserInv_Stub as UserInv0 with - type self = Core_Option_Option_Type.t_option t + type self = borrowed t clone CreusotContracts_Invariant_Inv_Stub as Inv0 with - type t = Core_Option_Option_Type.t_option t - axiom inv_t_option : forall self : Core_Option_Option_Type.t_option t . Inv0.inv self = (UserInv0.user_inv self /\ match (self) with - | Core_Option_Option_Type.C_None -> true - | Core_Option_Option_Type.C_Some a_0 -> Inv1.inv a_0 - end) + type t = borrowed t + axiom inv_borrow : forall self : borrowed t . Inv0.inv self = (UserInv0.user_inv self /\ (let a = * self in Inv1.inv a)) end -module Generated_UseList_Interface +module TyInv_Tuple2 + type t0 + type t1 + clone CreusotContracts_Invariant_Inv_Stub as Inv2 with + type t = t1 + clone CreusotContracts_Invariant_Inv_Stub as Inv1 with + type t = t0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = (t0, t1) + axiom inv_tuple2 : forall self : (t0, t1) . Inv0.inv self = (let (a_0, a_1) = self in Inv1.inv a_0 /\ Inv2.inv a_1) +end +module Generated_Sum10_Type_Inv + use Generated_Sum10_Type as Generated_Sum10_Type + clone Generated_Impl0_UserInv_Stub as UserInv0 + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Generated_Sum10_Type.t_sum10 + axiom inv_t_sum10 : forall self : Generated_Sum10_Type.t_sum10 . Inv0.inv self = UserInv0.user_inv self +end +module TyInv_Trivial + type t + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = t + axiom inv_trivial : forall self : t . Inv0.inv self = true +end +module Generated_UseFoo_Interface use prelude.Int - use prelude.Int32 - use Generated_List_Type as Generated_List_Type - val use_list [#"../generated.rs" 6 0 6 29] (l : Generated_List_Type.t_list int32) : () + use prelude.UInt32 + use prelude.Borrow + use Generated_Sum10_Type as Generated_Sum10_Type + use Generated_Foo_Type as Generated_Foo_Type + clone CreusotContracts_Invariant_Inv_Stub as Inv0 with + type t = Generated_Foo_Type.t_foo (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10)) + val use_foo [#"../generated.rs" 22 0 22 61] (x : Generated_Foo_Type.t_foo (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10))) : () + requires {[#"../generated.rs" 21 11 21 28] Inv0.inv x} + end -module Generated_UseList +module Generated_UseFoo use prelude.Int - use prelude.Int32 - use Generated_List_Type as Generated_List_Type + use prelude.UInt32 + use prelude.Borrow + clone CreusotContracts_Invariant_Inv_Interface as Inv5 with + type t = uint32 + clone TyInv_Trivial as TyInv_Trivial0 with + type t = uint32, + predicate Inv0.inv = Inv5.inv, + axiom . + use Generated_Foo_Type as Generated_Foo_Type + clone CreusotContracts_Invariant_Impl0_UserInv as UserInv3 with + type t = Generated_Foo_Type.t_foo uint32 + use Generated_Sum10_Type as Generated_Sum10_Type + clone Generated_Impl0_UserInv as UserInv2 + clone CreusotContracts_Invariant_Inv_Interface as Inv1 with + type t = borrowed (Generated_Sum10_Type.t_sum10) + clone CreusotContracts_Invariant_Inv_Interface as Inv4 with + type t = Generated_Foo_Type.t_foo uint32 + clone Generated_Foo_Type_Inv as Generated_Foo_Type_Inv1 with + type t = uint32, + predicate Inv0.inv = Inv4.inv, + predicate UserInv0.user_inv = UserInv3.user_inv, + predicate Inv1.inv = Inv1.inv, + predicate Inv2.inv = Inv5.inv, + axiom . clone CreusotContracts_Invariant_Inv_Interface as Inv3 with - type t = Generated_List_Type.t_list int32 - use Core_Option_Option_Type as Core_Option_Option_Type + type t = Generated_Sum10_Type.t_sum10 + clone Generated_Sum10_Type_Inv as Generated_Sum10_Type_Inv0 with + predicate Inv0.inv = Inv3.inv, + predicate UserInv0.user_inv = UserInv2.user_inv, + axiom . clone CreusotContracts_Invariant_Impl0_UserInv as UserInv1 with - type t = Core_Option_Option_Type.t_option (Generated_List_Type.t_list int32) + type t = borrowed (Generated_Sum10_Type.t_sum10) clone CreusotContracts_Invariant_Inv_Interface as Inv2 with - type t = Core_Option_Option_Type.t_option (Generated_List_Type.t_list int32) - clone Core_Option_Option_Type_Inv as Core_Option_Option_Type_Inv0 with - type t = Generated_List_Type.t_list int32, + type t = (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10)) + clone TyInv_Tuple2 as TyInv_Tuple20 with + type t0 = Generated_Foo_Type.t_foo uint32, + type t1 = borrowed (Generated_Sum10_Type.t_sum10), predicate Inv0.inv = Inv2.inv, - predicate UserInv0.user_inv = UserInv1.user_inv, - predicate Inv1.inv = Inv3.inv, + predicate Inv1.inv = Inv4.inv, + predicate Inv2.inv = Inv1.inv, axiom . - clone CreusotContracts_Invariant_Inv_Interface as Inv1 with - type t = int32 - clone TyInv_Trivial as TyInv_Trivial0 with - type t = int32, + clone TyInv_Borrow as TyInv_Borrow0 with + type t = Generated_Sum10_Type.t_sum10, predicate Inv0.inv = Inv1.inv, + predicate UserInv0.user_inv = UserInv1.user_inv, + predicate Inv1.inv = Inv3.inv, axiom . clone CreusotContracts_Invariant_Impl0_UserInv as UserInv0 with - type t = Generated_List_Type.t_list int32 + type t = Generated_Foo_Type.t_foo (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10)) clone CreusotContracts_Invariant_Inv_Interface as Inv0 with - type t = Generated_List_Type.t_list int32 - clone Generated_List_Type_Inv as Generated_List_Type_Inv0 with - type t = int32, + type t = Generated_Foo_Type.t_foo (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10)) + clone Generated_Foo_Type_Inv as Generated_Foo_Type_Inv0 with + type t = (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10)), predicate Inv0.inv = Inv0.inv, predicate UserInv0.user_inv = UserInv0.user_inv, predicate Inv1.inv = Inv1.inv, predicate Inv2.inv = Inv2.inv, axiom . - let rec cfg use_list [#"../generated.rs" 6 0 6 29] [@cfg:stackify] [@cfg:subregion_analysis] (l : Generated_List_Type.t_list int32) : () + let rec cfg use_foo [#"../generated.rs" 22 0 22 61] [@cfg:stackify] [@cfg:subregion_analysis] (x : Generated_Foo_Type.t_foo (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10))) : () + requires {[#"../generated.rs" 21 11 21 28] Inv0.inv x} = [@vc:do_not_keep_trace] [@vc:sp] var _0 : (); - var l : Generated_List_Type.t_list int32 = l; + var x : Generated_Foo_Type.t_foo (Generated_Foo_Type.t_foo uint32, borrowed (Generated_Sum10_Type.t_sum10)) = x; { goto BB0 } BB0 { - assert { [@expl:assertion] [#"../generated.rs" 7 18 7 35] Inv0.inv l }; - goto BB1 - } - BB1 { + assert { [@expl:assertion] [#"../generated.rs" 23 18 23 35] Inv0.inv x }; _0 <- (); - goto BB2 - } - BB2 { return _0 } end +module Generated_Impl0 + +end diff --git a/creusot/tests/should_succeed/type_invariants/generated.rs b/creusot/tests/should_succeed/type_invariants/generated.rs index 1b5a0af53c..76e792e5fc 100644 --- a/creusot/tests/should_succeed/type_invariants/generated.rs +++ b/creusot/tests/should_succeed/type_invariants/generated.rs @@ -1,8 +1,24 @@ +#![allow(incomplete_features)] +#![feature(specialization)] extern crate creusot_contracts; use creusot_contracts::{invariant, *}; -pub struct List(T, Option>>); +pub struct Sum10(i32, i32); -pub fn use_list(l: List) { - proof_assert!(invariant::inv(l)) +impl invariant::UserInv for Sum10 { + #[predicate] + #[open] + fn user_inv(self) -> bool { + pearlite! { self.0@ + self.1@ == 10 } + } +} + +pub enum Foo<'a, T> { + A { f1: &'a mut Sum10, f2: usize }, + B(T), +} + +#[requires(invariant::inv(x))] +pub fn use_foo<'a>(x: Foo<'a, (Foo<'a, u32>, &'a mut Sum10)>) { + proof_assert!(invariant::inv(x)); } diff --git a/creusot/tests/should_succeed/type_invariants/generated/why3session.xml b/creusot/tests/should_succeed/type_invariants/generated/why3session.xml new file mode 100644 index 0000000000..d3e44c3fcb --- /dev/null +++ b/creusot/tests/should_succeed/type_invariants/generated/why3session.xml @@ -0,0 +1,14 @@ + + + + + + + + + + + + + diff --git a/creusot/tests/should_succeed/type_invariants/generated/why3shapes.gz b/creusot/tests/should_succeed/type_invariants/generated/why3shapes.gz new file mode 100644 index 0000000000..f540409ede Binary files /dev/null and b/creusot/tests/should_succeed/type_invariants/generated/why3shapes.gz differ