Investigate slow generator tests #1406

fzaiser · 2022-07-25T20:02:40Z

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:


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);
}

The text was updated successfully, but these errors were encountered:

fzaiser · 2022-07-25T20:21:50Z

Apparently it works with the right unwind bounds. Now I'm wondering why the unwind bound is needed.

fzaiser mentioned this issue Jul 25, 2022

Implement support for generators #1378

Merged

4 tasks

fzaiser mentioned this issue Jul 25, 2022

Fix slow generator tests by adding kani::unwind annotation #1408

Merged

4 tasks

fzaiser closed this as completed in #1408 Jul 25, 2022

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Investigate slow generator tests #1406

Investigate slow generator tests #1406

fzaiser commented Jul 25, 2022

fzaiser commented Jul 25, 2022

Investigate slow generator tests #1406

Investigate slow generator tests #1406

Comments

fzaiser commented Jul 25, 2022

fzaiser commented Jul 25, 2022