Add a zero_initializer function

[danielsn]

Description of changes:

Right now, we can only zero_init scalar types. This adds a recursive form to allow us to zero_init complex types as well.

Resolved issues:

Resolves #ISSUE-NUMBER

Call-outs:

Using this may improve performance, at a potential soundness cost. Since the tradeoff is not clear, putting it behind a flag to allow experimentation, but keeping the current default for now.

Testing:

• How is this change tested?

  1. Existing regression tests. Turned on the flag, all regressions still pass, except for ones testing maybe_uninit, which we would expect to fail.
  2. Existing regression tests. Flag off, all regressions still pass.
  3. New test which maybe_units a variable and checks that it is all 0.

• Is this a refactor change? No

Checklist

• [x] Each commit message has a non-empty body, explaining why the change was made
• [x] Methods or procedures are documented
• [x] Regression or unit tests are included, or existing tests cover the modified code
• [x] My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[tautschnig]

I re-enabled the RustRealloc hook that was removed in #1088 and then tried the examples from #702 with this PR. I got:

$ kani 702.rs --enable-unstable --zero-init-vars
thread 'rustc' panicked at 'Can't zero init Code { parameters: [Parameter { typ: Pointer { typ: CInteger(SizeT) }, identifier: None, base_name: None }, Parameter { typ: Pointer { typ: CInteger(SizeT) }, identifier: None, base_name: None }], return_type: StructTag("tag-_11659839863328250985") }', cprover_bindings/src/goto_program/typ.rs:1262:38
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
If you are seeing this message, please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: std::cmp::max_by
_RINvNtCs8yXqNEgggfL_4core3cmp6max_byjNvYjNtB2_3Ord3cmpECs1cE2uPJmwEu_3_702
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2022-05-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/cmp.rs", function: None, line: 1276, col: Some(1) }
Error: [...]/kani-compiler exited with status exit status: 101

[danielsn]

blocked on https://github.com/model-checking/kani/issues/1243

[fzaiser]

Looks good to me. Two things:

• Is there a way this could be tested? Specifically test that it does zero initialization? (Not sure it's worth the hassle.)
• Did you observe a performance improvement on any examples?

[fzaiser]

One more thing: shouldn't we zero-initialize StatementKind::DeInit as well? As far as I can tell, that part of the code still uses nondet. In particular, DeInit is used to "initialize" generators, so they wouldn't benefit from the PR as is.

[fzaiser]

Looks good to me, except I think this should have a test. Running Kani with the flag and checking that the value of an uninitialized variable is zero (or something to that effect). Or is there a reason not to test this?

[danielsn]

What about an --enable-unsound flag