Performance regression with new rust toolchain

[celinval]

Our recent efforts to upgrade the rust toolchain to nightly-2023-01-23 #2149 is currently blocked due to a significant performance regression.

2 out of 3 tests added to measure the performance of Kani with Vectors seems to be highly affected. Here the analysis we added to the PR for tests/perf/vec/box_dyn.

Running the failing test in my local machine with cargo kani, I got the following:

Configuration	Time	Memory
main (CBMC 5.75)	5.74s	165MB
this PR (CBMC 5.75)	206s	16GB
main (CBMC 5.70)	200.s	16GB

Note that the time in this PR is very similar to the one I obtained when running main with an older CBMC version (before diffblue/cbmc#7230).

I wonder if whatever has changed neutralized the optimization that @tautschnig introduced. 😕

Originally posted by @celinval in #2149 (comment)

[celinval]

@tautschnig do you think you can take a look at this? Thanks!

[tautschnig]

It seems that the way null-ness is tested has been changed, and now CBMC no longer manages to simplify this. The following C snippet demonstrates the same problem (which we'll have to make CBMC solve solely via constant propagation and simplification):

union U
{
  void * ptr;
  __CPROVER_size_t n;
};

int main()
{
  int *p = __CPROVER_allocate(sizeof(int), 0);
  union U u = { .ptr = p };
  __CPROVER_assert(u.n != 0, "is not null");
}

Working on a fix.

[tautschnig]

Fixed in diffblue/cbmc#7556.

[celinval]

Thank you so much!! @tautschnig