Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unreachable code detection #1385

Open
wants to merge 42 commits into
base: master
Choose a base branch
from

Conversation

simon-hrabec
Copy link
Contributor

@simon-hrabec simon-hrabec commented Apr 3, 2023

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.

Simon Hrabec and others added 30 commits February 7, 2023 00:35
…er-without-signature

Feature/jni field getter setter without signature
@fpoli
Copy link
Member

fpoli commented Apr 4, 2023

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 #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:

let pos = if let Some(primary_span) = span.primary_span() {
let lines_info_res = self
.codemap
.span_to_lines(primary_span.source_callsite());
match lines_info_res {
Ok(lines_info) => {
if let Some(first_line_info) = lines_info.lines.get(0) {
let line = first_line_info.line_index as i32 + 1;
let column = first_line_info.start_col.0 as i32 + 1;
Position::new(line, column, pos_id)
} else {
debug!("Primary span of position id {} has no lines", pos_id);
Position::new(0, 0, pos_id)
}
}
Err(e) => {
debug!("Error converting primary span of position id {} to lines: {:?}", pos_id, e);
Position::new(0, 0, pos_id)
}
}
} else {
debug!("Position id {} has no primary span", pos_id);
Position::new(0, 0, pos_id)
};

@simon-hrabec
Copy link
Contributor Author

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.

@fpoli
Copy link
Member

fpoli commented Apr 5, 2023

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.

@fpoli
Copy link
Member

fpoli commented Apr 5, 2023

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?

@simon-hrabec
Copy link
Contributor Author

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.
#1389

@simon-hrabec
Copy link
Contributor Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants