viperproject
Unreachable code detection
Description
This PR adds an optional flag DETECT_UNREACHABLE_CODE, which allows the user to detect code that cannot be reached.
Implementation
The whole logic is based on adding refute false statements into basic blocks. Should the block be unreachable, the verification should fail. However, certain blocks are committed - an assert statement and unreachable!() call generate code that we expect not to execute.
However, there was an issue with locations/spans. Rust translates the code into more MIR basic blocks than a naive look would suggest. When creating an assert statement, a location/span needs to be provided. Multiple basic blocks can first statement that is registered for the same location. For some reason, when using the same location for multiple refute statements, the verification will fail on those statements. In such a case, the generated viper code/dump will verify without a problem. As a workaround, I use a HashSet to remember line/column (just remembering spans is not sufficient) to add only one refute statement referring to such position.
Performance analysis (benchmark running time - seconds)
| Test | Normal | Detection Enabled | Slowdown |
|---|---|---|---|
| prusti-tests/tests/verify/pass/rosetta/Knuth_shuffle.rs: | 2.775 | 4.194 | 51% |
| prusti-tests/tests/verify/pass/demos/account.rs: | 2.600 | 2.683 | 3% |
| prusti-tests/tests/verify/pass/rosetta/Knights_tour.rs | 86.544 | 985.014 | 1038% |
| prusti-tests/tests/verify/pass/quick/fold-unfold.rs: | 1.734 | 1.755 | 1% |
| prusti-tests/tests/verify/pass/quick/moves.rs: | 2.120 | 2.156 | 2% |
| prusti-tests/tests/verify/pass/quick/mut-borrows.rs: | 4.221 | 4.385 | 4% |
| prusti-tests/tests/verify/pass/quick/shared-borrows.rs: | 2.699 | 2.678 | -1% |
| prusti-tests/tests/verify/pass/quick/trait-contracts-refinement.rs: | 2.222 | 2.264 | 2% |
| prusti-tests/tests/verify/pass/quick/routes.rs: | 6.315 | 6.539 | 4% |
| prusti-tests/tests/verify/pass/quick/fibonacci.rs: | 8.288 | 11.177 | 35% |
| prusti-tests/tests/verify/pass/pure-fn/len-lookup.rs: | 5.089 | 5.253 | 3% |
| prusti-tests/tests/verify/pass/pure-fn/quantifiers.rs: | 2.984 | 3.066 | 3% |
| prusti-tests/tests/verify/pass/pure-fn/recursive-pure-fn.rs: | 2.691 | 2.754 | 2% |
| prusti-tests/tests/verify/pass/pure-fn/ref-mut-arg.rs: | 3.805 | 4.038 | 6% |
| prusti-tests/tests/verify/pass/rosetta/Ackermann_function.rs: | 2.466 | 3.082 | 25% |
| prusti-tests/tests/verify/pass/rosetta/Heapsort.rs: | 11.060 | 46.223 | 318% |
Note: Knights_tour.rs had high variance - basically 8x 620 and 2x 2450.
dead-code-detection-measurements.zip
Note/Disclaimer
This flag works well when only one block is unreachable, however, in the current version, if the whole function is unreachable (i.g. contradictory preconditions), it will generate multiple warnings for different blocks.
For some reason, when using the same location for multiple refute statements, the verification will fail on those statements.
That sounds like a bug in Viper, related to https://github.com/viperproject/prusti-dev/issues/1213. @Aurel300 once looked into that. Viper probably reports at most one error for each (line, column) pair. There is no strong reason for Prusti to generate positions using the line and column of the source Rust code. The error manager can easily generate unique line-column pairs. For example, Position::new(self.def_id.len(), 0, pos_id) in this file instead of querying the source code info: https://github.com/viperproject/prusti-dev/blob/c1d3447652c675e40884039c6b83489a7188892d/prusti-viper/src/encoder/errors/position_manager.rs#L46-L69
el300 once looked into that. Viper probably reports at most one error for each
(line, column)pair. There is no strong reason for Prusti to generate positions using the line and column of the source Rust code. The error manager can easily generate unique line-column pairs. For example,Position::new(self.def_id.len(), 0, pos_id)in this file instead of querying the source code info:
Thanks for the info. I did not know the position's line/column can be any numbers. Did you mean I should change my code or the error_manager (I made a change in my code now)?
BTW the issue would show up also when I have multiple refutes with the same line/column but none of them should fail - i.e. not some errors not being shown/triggered, but errors/warnings being triggered when they should not be. Although, I am not sure if this is not some edge case of the refute statement and how it is converted by the refute plugin.
Did you mean I should change my code or the error_manager (I made a change in my code now)?
The error manager, because (1) the change in your code is harder to maintain and because (2) the change will probably fix #1213.
BTW the issue would show up also when I have multiple refutes with the same line/column but none of them should fail
The change to the error manager should fix that, right?
BTW the issue would show up also when I have multiple refutes with the same line/column but none of them should fail
The change to the error manager should fix that, right?
Indeed :)
Made a separate PR to separate the changes and keep it clean/simple to review. https://github.com/viperproject/prusti-dev/pull/1389
I uploaded the measured data (running times of the benchmark files) and the generated .vpr (with the unreachable code detection turned both on and off) to another branch into my repository - https://github.com/simon-hrabec/prusti-dev/tree/feature/unreachable-code-detection-measurements-and-vpr-data/dead-code-detection-measurements