Skip to content

Commit

Permalink
Improve test
Browse files Browse the repository at this point in the history
  • Loading branch information
@voidc
voidc committed Jun 14, 2023
1 parent 251db3d commit f41ad35
Show file tree
Hide file tree
Showing 4 changed files with 177 additions and 66 deletions.
207 changes: 144 additions & 63 deletions creusot/tests/should_succeed/type_invariants/generated.mlcfg
View file
Original file line number Diff line number Diff line change
@@ -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
Expand All @@ -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
Expand All @@ -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
Expand All @@ -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
22 changes: 19 additions & 3 deletions creusot/tests/should_succeed/type_invariants/generated.rs
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,24 @@
#![allow(incomplete_features)]
#![feature(specialization)]
extern crate creusot_contracts;
use creusot_contracts::{invariant, *};

pub struct List<T>(T, Option<Box<List<T>>>);
pub struct Sum10(i32, i32);

pub fn use_list(l: List<i32>) {
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));
}
14 changes: 14 additions & 0 deletions creusot/tests/should_succeed/type_invariants/generated/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Alt-Ergo" version="2.4.2" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="mlcfg" proved="true">
<path name=".."/><path name="generated.mlcfg"/>
<theory name="Generated_UseFoo" proved="true">
<goal name="use_foo&#39;vc" expl="VC for use_foo" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
</file>
</why3session>
Binary file added creusot/tests/should_succeed/type_invariants/generated/why3shapes.gz
View file
Binary file not shown.

0 comments on commit f41ad35

Please sign in to comment.