Unreachable code detection

[simon-hrabec]

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.

[fpoli]

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:

prusti-dev/prusti-viper/src/encoder/errors/position_manager.rs

Lines 46 to 69 in c1d3447

	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]

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]

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]

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]

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]

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