Skip to content

Commit

Permalink
bless
Browse files Browse the repository at this point in the history
  • Loading branch information
@dewert99
dewert99 committed Jul 26, 2024
1 parent 15512bc commit 13ac222
Show file tree
Hide file tree
Showing 58 changed files with 12,026 additions and 19,579 deletions.
122 changes: 38 additions & 84 deletions creusot/tests/should_fail/bug/01_resolve_unsoundness.coma
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,22 +101,7 @@ module Alloc_Alloc_Global_Type

end
module CreusotContracts_Logic_Seq2_Seq_Type
use seq.Seq

type t_seq 't =
| C_Seq (Seq.seq 't)

function any_l (_ : 'b) : 'a

let rec t_seq < 't > (input:t_seq 't) (ret (field_0:Seq.seq 't))= any
[ good (field_0:Seq.seq 't)-> {C_Seq field_0 = input} (! ret {field_0})
| bad (field_0:Seq.seq 't)-> {C_Seq field_0 <> input} {false} any ]


function seq_0 [@inline:trivial] (self : t_seq 't) : Seq.seq 't =
match self with
| C_Seq a -> a
end
type t_seq 't
end
module C01ResolveUnsoundness_MakeVecOfSize
let%span s01_resolve_unsoundness0 = "../01_resolve_unsoundness.rs" 10 29 10 39
Expand All @@ -135,55 +120,39 @@ module C01ResolveUnsoundness_MakeVecOfSize

let%span span7 = "" 0 0 0 0

let%span span8 = "../../../../../creusot-contracts/src/logic/seq2.rs" 72 15 72 19

let%span span9 = "../../../../../creusot-contracts/src/logic/seq2.rs" 71 14 71 25

let%span span10 = "../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25

let%span span11 = "../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41

let%span span12 = "../../../../../creusot-contracts/src/std/vec.rs" 19 4 19 36
let%span span8 = "../../../../../creusot-contracts/src/logic/seq2.rs" 68 14 68 25

let%span span13 = "../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41
let%span span9 = "../../../../../creusot-contracts/src/std/vec.rs" 19 21 19 25

let%span span14 = "../../../../../creusot-contracts/src/logic/seq2.rs" 19 4 19 25
let%span span10 = "../../../../../creusot-contracts/src/std/vec.rs" 18 14 18 41

let%span span15 = "../../../../../creusot-contracts/src/logic/seq2.rs" 23 14 23 36
let%span span11 = "../../../../../creusot-contracts/src/std/vec.rs" 60 20 60 41

let%span span16 = "../../../../../creusot-contracts/src/logic/seq2.rs" 21 4 21 10
let%span span12 = "../../../../../creusot-contracts/src/logic/seq2.rs" 16 14 16 36

let%span span17 = "../../../../../creusot-contracts/src/logic/seq2.rs" 107 18 107 22
let%span span13 = "../../../../../creusot-contracts/src/logic/seq2.rs" 104 14 104 54

let%span span18 = "../../../../../creusot-contracts/src/logic/seq2.rs" 107 24 107 29
let%span span14 = "../../../../../creusot-contracts/src/logic/seq2.rs" 105 4 106 62

let%span span19 = "../../../../../creusot-contracts/src/logic/seq2.rs" 104 14 104 54
let%span span15 = "../../../../../creusot-contracts/src/logic/seq2.rs" 54 21 54 22

let%span span20 = "../../../../../creusot-contracts/src/logic/seq2.rs" 105 4 106 62
let%span span16 = "../../../../../creusot-contracts/src/logic/seq2.rs" 52 14 52 31

let%span span21 = "../../../../../creusot-contracts/src/logic/seq2.rs" 107 4 107 44
let%span span17 = "../../../../../creusot-contracts/src/logic/seq2.rs" 53 14 53 28

let%span span22 = "../../../../../creusot-contracts/src/logic/seq2.rs" 58 21 58 22
let%span span18 = "../../../../../creusot-contracts/src/logic/seq2.rs" 98 8 98 39

let%span span23 = "../../../../../creusot-contracts/src/logic/seq2.rs" 56 14 56 31
let%span span19 = "../../../../../creusot-contracts/src/model.rs" 108 8 108 31

let%span span24 = "../../../../../creusot-contracts/src/logic/seq2.rs" 57 14 57 28
let%span span20 = "" 0 0 0 0

let%span span25 = "../../../../../creusot-contracts/src/logic/seq2.rs" 58 4 58 34
let%span span21 = "" 0 0 0 0

let%span span26 = "../../../../../creusot-contracts/src/logic/seq2.rs" 99 8 99 39
let%span span22 = "../../../../../creusot-contracts/src/std/vec.rs" 82 26 82 51

let%span span27 = "../../../../../creusot-contracts/src/model.rs" 108 8 108 31
let%span span23 = "../../../../../creusot-contracts/src/std/vec.rs" 69 26 69 44

let%span span28 = "" 0 0 0 0

let%span span29 = "" 0 0 0 0

let%span span30 = "../../../../../creusot-contracts/src/std/vec.rs" 82 26 82 51

let%span span31 = "../../../../../creusot-contracts/src/std/vec.rs" 69 26 69 44

let%span span32 = "" 0 0 0 0
let%span span24 = "" 0 0 0 0

use CreusotContracts_Logic_Seq2_Seq_Type as Seq'0

Expand Down Expand Up @@ -222,76 +191,61 @@ module C01ResolveUnsoundness_MakeVecOfSize

constant max'0 : usize = [%#span7] (18446744073709551615 : usize)

use seq.Seq

use CreusotContracts_Logic_Seq2_Seq_Type as CreusotContracts_Logic_Seq2_Seq_Type

function len'0 (self : Seq'0.t_seq bool) : int

axiom len'0_spec : forall self : Seq'0.t_seq bool . ([%#span8] inv'3 self) -> ([%#span9] len'0 self >= 0)
axiom len'0_spec : forall self : Seq'0.t_seq bool . [%#span8] len'0 self >= 0

predicate inv'0 (_x : Vec'0.t_vec bool (Global'0.t_global))

function shallow_model'0 (self : Vec'0.t_vec bool (Global'0.t_global)) : Seq'0.t_seq bool

axiom shallow_model'0_spec : forall self : Vec'0.t_vec bool (Global'0.t_global) . ([%#span10] inv'0 self)
-> ([%#span12] inv'3 (shallow_model'0 self))
&& ([%#span11] len'0 (shallow_model'0 self) <= UIntSize.to_int (max'0 : usize))
axiom shallow_model'0_spec : forall self : Vec'0.t_vec bool (Global'0.t_global) . ([%#span9] inv'0 self)
-> ([%#span10] len'0 (shallow_model'0 self) <= UIntSize.to_int (max'0 : usize))

predicate invariant'0 (self : Vec'0.t_vec bool (Global'0.t_global)) =
[%#span13] inv'3 (shallow_model'0 self)
[%#span11] inv'3 (shallow_model'0 self)

axiom inv'0 : forall x : Vec'0.t_vec bool (Global'0.t_global) . inv'0 x = true

constant empty'0 : Seq'0.t_seq bool = [%#span14] ()
constant empty'0 : Seq'0.t_seq bool

function empty_len'0 (_1 : ()) : () =
[%#span16] ()
function empty_len'0 (_1 : ()) : ()

axiom empty_len'0_spec : forall _1 : () . [%#span15] len'0 (empty'0 : Seq'0.t_seq bool) = 0
axiom empty_len'0_spec : forall _1 : () . [%#span12] len'0 (empty'0 : Seq'0.t_seq bool) = 0

use prelude.prelude.Intrinsic

use seq.Seq

use seq.Seq

function index_logic'0 (self : Seq'0.t_seq bool) (x : int) : bool
function index_logic'0 (self : Seq'0.t_seq bool) (_2 : int) : bool

function concat'0 (self : Seq'0.t_seq bool) (other : Seq'0.t_seq bool) : Seq'0.t_seq bool

axiom concat'0_spec : forall self : Seq'0.t_seq bool, other : Seq'0.t_seq bool . ([%#span17] inv'3 self)
-> ([%#span18] inv'3 other)
-> ([%#span21] inv'3 (concat'0 self other))
&& ([%#span20] forall i : int . 0 <= i /\ i < len'0 (concat'0 self other)
axiom concat'0_spec : forall self : Seq'0.t_seq bool, other : Seq'0.t_seq bool . ([%#span14] forall i : int . 0 <= i
/\ i < len'0 (concat'0 self other)
-> index_logic'0 (concat'0 self other) i
= (if i < len'0 self then index_logic'0 self i else index_logic'0 other (i - len'0 self)))
&& ([%#span19] len'0 (concat'0 self other) = len'0 self + len'0 other)

use seq.Seq
&& ([%#span13] len'0 (concat'0 self other) = len'0 self + len'0 other)

function singleton'0 (v : bool) : Seq'0.t_seq bool

axiom singleton'0_spec : forall v : bool . ([%#span22] inv'2 v)
-> ([%#span25] inv'3 (singleton'0 v))
&& ([%#span24] index_logic'0 (singleton'0 v) 0 = v) && ([%#span23] len'0 (singleton'0 v) = 1)
axiom singleton'0_spec : forall v : bool . ([%#span15] inv'2 v)
-> ([%#span17] index_logic'0 (singleton'0 v) 0 = v) && ([%#span16] len'0 (singleton'0 v) = 1)

function push'1 [@inline:trivial] (self : Seq'0.t_seq bool) (v : bool) : Seq'0.t_seq bool =
[%#span26] concat'0 self (singleton'0 v)
[%#span18] concat'0 self (singleton'0 v)

function shallow_model'1 (self : borrowed (Vec'0.t_vec bool (Global'0.t_global))) : Seq'0.t_seq bool =
[%#span27] shallow_model'0 ( * self)
[%#span19] shallow_model'0 ( * self)

let rec push'0 (self:borrowed (Vec'0.t_vec bool (Global'0.t_global))) (value:bool) (return' (ret:()))= {[@expl:precondition] [%#span29] inv'2 value}
{[@expl:precondition] [%#span28] inv'1 self}
let rec push'0 (self:borrowed (Vec'0.t_vec bool (Global'0.t_global))) (value:bool) (return' (ret:()))= {[@expl:precondition] [%#span21] inv'2 value}
{[@expl:precondition] [%#span20] inv'1 self}
any
[ return' (result:())-> {[%#span30] shallow_model'0 ( ^ self) = push'1 (shallow_model'1 self) value}
[ return' (result:())-> {[%#span22] shallow_model'0 ( ^ self) = push'1 (shallow_model'1 self) value}
(! return' {result}) ]


let rec new'0 (_1:()) (return' (ret:Vec'0.t_vec bool (Global'0.t_global)))= any
[ return' (result:Vec'0.t_vec bool (Global'0.t_global))-> {[%#span32] inv'0 result}
{[%#span31] len'0 (shallow_model'0 result) = 0}
[ return' (result:Vec'0.t_vec bool (Global'0.t_global))-> {[%#span24] inv'0 result}
{[%#span23] len'0 (shallow_model'0 result) = 0}
(! return' {result}) ]


Expand Down
88 changes: 88 additions & 0 deletions creusot/tests/should_fail/bug/436_2.coma
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,88 @@

module CreusotContracts_Snapshot_Snapshot_Type
type t_snapshot 't
end
module C4362_Bad_Type
use prelude.prelude.Borrow

use CreusotContracts_Snapshot_Snapshot_Type as Snapshot'0

type t_bad =
| C_None
| C_Some (Snapshot'0.t_snapshot (borrowed (t_bad)))

function any_l (_ : 'b) : 'a

let rec none (input:t_bad) (ret )= any [ good -> {C_None = input} (! ret) | bad -> {C_None <> input} {false} any ]

let rec some (input:t_bad) (ret (field_0:Snapshot'0.t_snapshot (borrowed (t_bad))))= any
[ good (field_0:Snapshot'0.t_snapshot (borrowed (t_bad)))-> {C_Some field_0 = input} (! ret {field_0})
| bad (field_0:Snapshot'0.t_snapshot (borrowed (t_bad)))-> {C_Some field_0 <> input} {false} any ]

end
module C4362_TestBad
let%span s436_20 = "../436_2.rs" 12 12 12 24

let%span s436_21 = "../436_2.rs" 14 18 14 36

let%span s436_22 = "../436_2.rs" 15 18 15 27

let%span s436_23 = "../436_2.rs" 17 18 17 37

let%span span4 = "../../../../../creusot-contracts/src/invariant.rs" 8 8 8 12

let%span span5 = "../../../../../creusot-contracts/src/resolve.rs" 26 20 26 34

let%span span6 = "../../../../../creusot-contracts/src/snapshot.rs" 45 15 45 16

let%span span7 = "../../../../../creusot-contracts/src/snapshot.rs" 43 14 43 28

use C4362_Bad_Type as Bad'0

use prelude.prelude.Borrow

predicate invariant'0 (self : borrowed (Bad'0.t_bad)) =
[%#span4] true

predicate inv'0 (_x : borrowed (Bad'0.t_bad))

axiom inv'0 : forall x : borrowed (Bad'0.t_bad) . inv'0 x = true

use CreusotContracts_Snapshot_Snapshot_Type as Snapshot'0

use prelude.prelude.Intrinsic

predicate resolve'0 (self : borrowed (Bad'0.t_bad)) =
[%#span5] ^ self = * self

function deref'0 (self : Snapshot'0.t_snapshot (borrowed (Bad'0.t_bad))) : borrowed (Bad'0.t_bad)

function new'0 (x : borrowed (Bad'0.t_bad)) : Snapshot'0.t_snapshot (borrowed (Bad'0.t_bad))

axiom new'0_spec : forall x : borrowed (Bad'0.t_bad) . ([%#span6] inv'0 x) -> ([%#span7] deref'0 (new'0 x) = x)

let rec test_bad (_1:()) (return' (ret:()))= (! bb0
[ bb0 = s0
[ s0 = [ &x <- Bad'0.C_None ] s1
| s1 = Borrow.borrow_mut <Bad'0.t_bad> {x}
(fun (_ret':borrowed (Bad'0.t_bad)) -> [ &m <- _ret' ] [ &x <- ^ m ] s2)
| s2 = [ &g <- [%#s436_20] new'0 m ] s3
| s3 = bb1 ]

| bb1 = s0
[ s0 = [ &_5 <- Bad'0.C_Some g ] s1
| s1 = [ &m <- { m with current = _5 ; } ] (any [ any_ (_any:Bad'0.t_bad)-> (! [ &_5 <- _any ] s2) ] )
| s2 = {[@expl:assertion] [%#s436_21] * m = Bad'0.C_Some g} s3
| s3 = {[@expl:assertion] [%#s436_22] ^ deref'0 g = ^ m} s4
| s4 = -{resolve'0 m}- s5
| s5 = {[@expl:assertion] [%#s436_23] ^ deref'0 g = Bad'0.C_Some g} s6
| s6 = return' {_0} ]
]
)
[ & _0 : () = any_l ()
| & x : Bad'0.t_bad = any_l ()
| & m : borrowed (Bad'0.t_bad) = any_l ()
| & g : Snapshot'0.t_snapshot (borrowed (Bad'0.t_bad)) = any_l ()
| & _5 : Bad'0.t_bad = any_l () ]
[ return' (result:())-> (! return' {result}) ]
end
Loading

0 comments on commit 13ac222

Please sign in to comment.