Investigate slow generator tests #1406
Description
Some tests involving generators are very slow (didn't terminate in a couple of minutes), for example tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs, which had to be disabled:
#![feature(generators, generator_trait)]
use std::ops::{Generator, GeneratorState};
use std::pin::Pin;
fn take<T>(_: T) {}
#[kani::proof]
fn main() {
let x = false;
let mut gen1 = || {
yield;
take(x);
};
assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(()));
assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(()));
}The reason for that may be the use of unions, which can be challenging for CBMC, if i understood @tautschnig correctly. The generator is translated to the following datastructure:
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::DirectFields
{
// generator_field_0
_Bool *generator_field_0;
// case
unsigned char case;
};
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Unresumed
{
};
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Returned
{
};
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Panicked
{
};
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Suspend0
{
};
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]
{
// direct_fields
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::DirectFields direct_fields;
// generator_variant_Unresumed
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Unresumed generator_variant_Unresumed;
// generator_variant_Returned
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Returned generator_variant_Returned;
// generator_variant_Panicked
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Panicked generator_variant_Panicked;
// generator_variant_Suspend0
struct [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]::Suspend0 generator_variant_Suspend0;
};
The demangled GotoC output for the functions looks like this:
Details
struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc13::struct
{
// 0
unsigned char 0[1];
};
struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc14::struct
{
// 0
unsigned char 0[1];
};
struct &str
{
// data
unsigned char *data;
// len
unsigned long int len;
};
// Void()
//
struct () Void();
// niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc13
//
struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc13::struct niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc13;
// niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc14
//
struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc14::struct niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc14;
// take::<bool>
// file /Users/fzaiser/ws/kani/tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs line 20 column 1 function take::<bool>
struct () take::<bool>(_Bool var_1)
{
struct () var_0;
bb0:
;
bb1:
;
return Void();
}
// main::{closure#0}
// file /Users/fzaiser/ws/kani/tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs line 25 column 20 function main::{closure#0}
struct std::ops::GeneratorState<(), ()> main::{closure#0}(struct std::pin::Pin<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]> var_1, struct () var_2)
{
struct std::ops::GeneratorState<(), ()> var_0;
struct () var_3;
struct () var_4;
_Bool var_5;
_Bool *var_6;
struct () var_7;
unsigned int var_8;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_9;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_10;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_11;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_12;
bb0:
;
var_9 = var_1.pointer;
var_8 = (unsigned int)var_9->direct_fields.case;
switch(var_8)
{
case 0:
break;
case 1:
goto bb4;
case 3:
goto bb3;
default:
goto bb5;
}
bb1:
;
var_0 = nondet_0();
var_0.case = 0;
var_10 = var_1.pointer;
var_10->direct_fields.case = 3;
return var_0;
bb2:
;
var_0 = nondet_0();
var_0.case = 1;
var_12 = var_1.pointer;
var_12->direct_fields.case = 1;
return var_0;
bb3:
;
var_11 = var_1.pointer;
var_6 = var_11->direct_fields.generator_field_0;
var_5 = *var_6;
take::<bool>(var_5);
goto bb2;
/* [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_2 */
do
{
bb4:
;
assert(!1);
assert(0);
}
while(1);
/* unreachable code */
bb5:
;
/* unreachable code */
assert(0);
__CPROVER_assume(0);
}
// std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new
// file /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/pin.rs line 491 column 5 function std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new
struct std::pin::Pin<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]> std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new(union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *pointer)
{
struct std::pin::Pin<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]> var_0;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new$$1$$var_2$$pointer;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_3;
bb0:
;
std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new$$1$$var_2$$pointer = pointer;
var_3 = std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new$$1$$var_2$$pointer;
var_0 = nondet_1();
var_0.pointer = var_3;
return var_0;
}
// std::cmp::impls::<impl std::cmp::PartialEq for ()>::eq
// file /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/cmp.rs line 1319 column 9 function std::cmp::impls::<impl std::cmp::PartialEq for ()>::eq
_Bool std::cmp::impls::<impl std::cmp::PartialEq for ()>::eq(struct () *self, struct () *_other)
{
bb0:
;
_Bool var_0=1;
return var_0;
}
// <std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq
// file /Users/fzaiser/.rustup/toolchains/nightly-2022-07-19-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/ops/generator.rs line 9 column 23 function <std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq
_Bool <std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq(struct std::ops::GeneratorState<(), ()> *self, struct std::ops::GeneratorState<(), ()> *other)
{
_Bool var_0;
long int __self_tag;
struct std::ops::GeneratorState<(), ()> *var_4;
long int __arg1_tag;
struct std::ops::GeneratorState<(), ()> *var_6;
_Bool var_7;
long int var_8;
long int var_9;
_Bool var_10;
struct (&std::ops::GeneratorState<(), ()>, &std::ops::GeneratorState<(), ()>) var_11;
struct std::ops::GeneratorState<(), ()> *var_12;
struct std::ops::GeneratorState<(), ()> *var_13;
long int var_14;
long int var_15;
long int var_16;
struct () *<std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq$$1$$var_17$$__self_0;
struct () *__arg1_0;
struct () *var_19;
struct () *var_20;
struct () *__self_0;
struct () *<std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq$$1$$var_22$$__arg1_0;
struct () *var_23;
struct () *var_24;
struct std::ops::GeneratorState<(), ()> *var_25;
struct std::ops::GeneratorState<(), ()> *var_26;
struct std::ops::GeneratorState<(), ()> *var_27;
struct std::ops::GeneratorState<(), ()> *var_28;
struct std::ops::GeneratorState<(), ()> *var_29;
struct std::ops::GeneratorState<(), ()> *var_30;
struct std::ops::GeneratorState<(), ()> *var_31;
bb0:
;
var_4 = self;
__self_tag = (long int)var_4->case;
var_6 = other;
__arg1_tag = (long int)var_6->case;
var_8 = __self_tag;
var_9 = __arg1_tag;
var_7 = var_8 == var_9;
if(!(var_7 == 0))
goto bb2;
bb1:
;
var_0 = 0;
goto bb3;
bb2:
;
var_12 = self;
var_13 = other;
var_11 = nondet_2();
var_11.0 = var_12;
var_11.1 = var_13;
var_25 = var_11.0;
var_16 = (long int)var_25->case;
switch(var_16)
{
case 0:
goto bb4;
case 1:
goto bb6;
default:
goto bb5;
}
bb3:
;
return var_0;
bb4:
;
var_26 = var_11.1;
var_14 = (long int)var_26->case;
if(!(var_14 == 0))
{
goto bb5;
/* unreachable code */
bb5:
;
/* unreachable code */
assert(0);
__CPROVER_assume(0);
bb6:
;
var_27 = var_11.1;
var_15 = (long int)var_27->case;
if(var_15 == 1)
goto bb9;
goto bb5;
}
bb7:
;
var_28 = var_11.0;
<std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq$$1$$var_17$$__self_0 = &var_28->cases.Yielded.0;
var_29 = var_11.1;
__arg1_0 = &var_29->cases.Yielded.0;
var_19 = <std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq$$1$$var_17$$__self_0;
var_20 = __arg1_0;
var_10=std::cmp::impls::<impl std::cmp::PartialEq for ()>::eq(var_19, var_20);
bb8:
;
goto bb11;
bb9:
;
var_30 = var_11.0;
__self_0 = &var_30->cases.Complete.0;
var_31 = var_11.1;
<std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq$$1$$var_22$$__arg1_0 = &var_31->cases.Complete.0;
var_23 = __self_0;
var_24 = <std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq$$1$$var_22$$__arg1_0;
var_10=std::cmp::impls::<impl std::cmp::PartialEq for ()>::eq(var_23, var_24);
bb10:
;
bb11:
;
var_0 = var_10;
goto bb3;
}
// main
// file /Users/fzaiser/ws/kani/tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs line 23 column 1 function main
struct () main(void)
{
struct () var_0;
_Bool x;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] gen1;
_Bool *var_3;
struct () var_4;
_Bool var_5;
struct std::ops::GeneratorState<(), ()> *var_6;
struct std::ops::GeneratorState<(), ()> var_7;
struct std::pin::Pin<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]> var_8;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_9;
struct () var_10;
struct std::ops::GeneratorState<(), ()> *var_11;
struct () var_12;
_Bool var_13;
struct std::ops::GeneratorState<(), ()> *var_14;
struct std::ops::GeneratorState<(), ()> var_15;
struct std::pin::Pin<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]> var_16;
union [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22] *var_17;
struct () var_18;
struct std::ops::GeneratorState<(), ()> *var_19;
struct std::ops::GeneratorState<(), ()> *var_20;
struct std::ops::GeneratorState<(), ()> *var_21;
bb0:
;
x = 0;
var_3 = &x;
gen1 = nondet_3();
gen1.direct_fields.generator_field_0 = var_3;
gen1.direct_fields.case = 0;
var_9 = &gen1;
var_8=std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new(var_9);
bb1:
;
var_7=main::{closure#0}(var_8, var_10);
bb2:
;
var_6 = &var_7;
var_21 = byte_extract_little_endian((struct std::ops::GeneratorState<(), ()> *)((unsigned char *)&niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc13 + 0), 0, struct std::ops::GeneratorState<(), ()> *);
var_11 = var_21;
var_5=<std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq(var_6, var_11);
/* [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_0 */
bb3:
;
/* [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_0 */
assert(!1);
__CPROVER_bool temp_0=var_5 != 0;
/* [KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_0] assertion failed: Pin::new(&mut gen1).resume(()) == GeneratorState::Yielded(()) */
assert(temp_0);
__CPROVER_assume(temp_0);
goto bb4;
bb4:
;
var_17 = &gen1;
var_16=std::pin::Pin::<&mut [generator@niche-in-generator-slow_fixme.rs:25:20: 25:22]>::new(var_17);
bb5:
;
var_15=main::{closure#0}(var_16, var_18);
bb6:
;
var_14 = &var_15;
var_20 = byte_extract_little_endian((struct std::ops::GeneratorState<(), ()> *)((unsigned char *)&niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc14 + 0), 0, struct std::ops::GeneratorState<(), ()> *);
var_19 = var_20;
var_13=<std::ops::GeneratorState<(), ()> as std::cmp::PartialEq>::eq(var_14, var_19);
/* [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_1 */
bb7:
;
/* [KANI_REACHABILITY_CHECK] KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_1 */
assert(!1);
__CPROVER_bool temp_1=var_13 != 0;
/* [KANI_CHECK_ID_niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme_1] assertion failed: Pin::new(&mut gen1).resume(()) == GeneratorState::Complete(()) */
assert(temp_1);
__CPROVER_assume(temp_1);
goto bb8;
bb8:
;
return Void();
}
// niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc13::init
//
static __attribute__((constructor)) void niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc13_init(void)
{
struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc13::struct var_0={ .0={ 0 } };
niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc13 = byte_extract_little_endian(var_0, 0, struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc13::struct);
}
// niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc14::init
//
static __attribute__((constructor)) void niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc14_init(void)
{
struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc14::struct var_0={ .0={ 1 } };
niche_in_generator_slow_fixme_f154e118$$niche_in_generator_slow_fixme$$alloc14 = byte_extract_little_endian(var_0, 0, struct niche_in_generator_slow_fixme.f154e118::niche_in_generator_slow_fixme::alloc14::struct);
}