count leading zeros failures disappear with --reachability-slice

[zhassan-aws]

(Could not reopen #6394 so filing a new issue).

On the attached test generated by Kani, the "count leading zeros" failures disappear if the goto binary is processed through goto-instrument --reachability-slice.

Steps to reproduce:

1. tar xvzf bounds.out.tar.gz
2. cbmc --bounds-check bounds.out :

** Results:
[assertion.1] Code generation sanity check: Correct CBMC vtable size for StructTag("tag-_13509187325931132202") (MIR type Closure(DefId(2:9481 ~ std[b2e3]::rt::lang_start::{closure#0}), [(), i8, extern "rust-call" fn(()) -> i32, (fn(),)])). Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS
[bit_count.1] count leading zeros is undefined for value zero in __builtin_clz(var_10): FAILURE
[bit_count.2] count leading zeros is undefined for value zero in __builtin_clz(var_12): FAILURE
[bit_count.3] count leading zeros is undefined for value zero in __builtin_clz(var_14): FAILURE
[bit_count.4] count leading zeros is undefined for value zero in __builtin_clz(var_16): FAILURE
[bit_count.5] count leading zeros is undefined for value zero in __builtin_clz(var_18): FAILURE
[bit_count.6] count leading zeros is undefined for value zero in __builtin_clz(var_20): FAILURE
[bit_count.7] count leading zeros is undefined for value zero in __builtin_clz(var_22): FAILURE
[bit_count.8] count leading zeros is undefined for value zero in __builtin_clz(var_24): FAILURE

3. goto-instrument --reachability-slice bounds.out bounds_after.out
4. cbmc --bounds-check bounds_after.out

** Results:
[assertion.1] Code generation sanity check: Correct CBMC vtable size for StructTag("tag-_13509187325931132202") (MIR type Closure(DefId(2:9481 ~ std[b2e3]::rt::lang_start::{closure#0}), [(), i8, extern "rust-call" fn(()) -> i32, (fn(),)])). Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL

** 8 of 9 failed (2 iterations)
VERIFICATION FAILED

CBMC version: 5.52.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: See above
What behaviour did you expect: Failures to remain with --reachability-slice
What happened instead: Failures disappear

[zhassan-aws]

bounds.out.tar.gz

[tautschnig]

Fortunately this might just be matter of documentation not being sufficiently clear:

 --reachability-slice         remove instructions that cannot appear on a trace
                                         from entry point to a property

In your use of goto-instrument, however, you did not specify the --bounds-check property, so your user-specified assertion was the only property that was left. Hence, the slicer removed all instructions that this user-specified assertion wasn't reachable from. What you would want to do instead is the following:

goto-instrument --bounds-check --reachability-slice bounds.out bounds_after.out
cbmc bounds_after.out
CBMC version 5.52.0 (cbmc-5.52.0-58-g807cd41cc5) 64-bit x86_64 linux
Reading GOTO program from file bounds_after.out
[...]
** Results:
[assertion.1] Code generation sanity check: Correct CBMC vtable size for StructTag("tag-_13509187325931132202") (MIR type Closure(DefId(2:9481 ~ std[b2e3]::rt::lang_start::{closure#0}), [(), i8, extern "rust-call" fn(()) -> i32, (fn(),)])). Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS
[bit_count.1] count leading zeros is undefined for value zero in __builtin_clz(var_10): FAILURE
[bit_count.2] count leading zeros is undefined for value zero in __builtin_clz(var_12): FAILURE
[bit_count.3] count leading zeros is undefined for value zero in __builtin_clz(var_14): FAILURE
[bit_count.4] count leading zeros is undefined for value zero in __builtin_clz(var_16): FAILURE
[bit_count.5] count leading zeros is undefined for value zero in __builtin_clz(var_18): FAILURE
[bit_count.6] count leading zeros is undefined for value zero in __builtin_clz(var_20): FAILURE
[bit_count.7] count leading zeros is undefined for value zero in __builtin_clz(var_22): FAILURE
[bit_count.8] count leading zeros is undefined for value zero in __builtin_clz(var_24): FAILURE

** 8 of 9 failed (2 iterations)
VERIFICATION FAILED

That is to say: if you want to re-enable --reachability-slice, any --*-check specifications should be moved to the goto-instrument call as well.

Edit: Another option is to invoke cbmc with --reachability-slice instead of using goto-instrument for this purpose. This option may be easier in the short-term, but be warned that with a future major-version upgrade of CBMC that option might go away for we intend to have all program transformation in goto-instrument only.

[zhassan-aws]

Closing the issue since CBMC is functioning as designed.