diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index 3d0d814e6e7..8f0beac6ea9 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -93,7 +93,10 @@ impl<'v> ToViper<'v, viper::Position<'v>> for Position { line = %self.line(), column = %self.column(), id = %self.id() ))] fn to_viper(&self, _context: Context, ast: &AstFactory<'v>) -> viper::Position<'v> { - ast.identifier_position(self.line(), self.column(), self.id().to_string()) + // The line and column of a vir::Position refer to the source Rust program. + // Line and columns in Viper positions have a different semantics, because Silicon + // deduplicates error messages based on them. + ast.identifier_position(self.id() as i32, 0, self.id().to_string()) } } @@ -323,8 +326,7 @@ impl<'v> ToViper<'v, viper::Stmt<'v>> for Stmt { ), pos.to_viper(context, ast), ); - let position = - ast.identifier_position(pos.line(), pos.column(), pos.id().to_string()); + let position = pos.to_viper(context, ast); let apply = ast.apply(wand.to_viper(context, ast), position); ast.seqn(&[inhale, apply], &[]) } diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index 6f33840ea70..273f44ea5d9 100644 --- a/prusti-server/src/verification_request.rs +++ b/prusti-server/src/verification_request.rs @@ -37,6 +37,10 @@ impl ViperBackendConfig { let mut verifier_args = config::extra_verifier_args(); match backend { VerificationBackend::Silicon => { + verifier_args.push(format!( + "--numberOfErrorsToReport={}", + config::num_errors_per_function() + )); if config::use_more_complete_exhale() { verifier_args.push("--enableMoreCompleteExhale".to_string()); } diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index 65a6bc9e624..d27f0f992cd 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -129,6 +129,7 @@ lazy_static::lazy_static! { settings.set_default("use_new_encoder", true).unwrap(); settings.set_default::>("number_of_parallel_verifiers", None).unwrap(); settings.set_default::>("min_prusti_version", None).unwrap(); + settings.set_default("num_errors_per_function", 1).unwrap(); settings.set_default("print_desugared_specs", false).unwrap(); settings.set_default("print_typeckd_specs", false).unwrap(); @@ -1023,3 +1024,9 @@ pub fn cargo_command() -> String { pub fn enable_type_invariants() -> bool { read_setting("enable_type_invariants") } + +/// The maximum number of verification errors to report per function. This is only used by the +/// Silicon backend. A value of 0 means no limit. +pub fn num_errors_per_function() -> u32 { + read_setting("num_errors_per_function") +} diff --git a/prusti-viper/src/encoder/errors/position_manager.rs b/prusti-viper/src/encoder/errors/position_manager.rs index b1575ec0e0f..5b9757bd3dd 100644 --- a/prusti-viper/src/encoder/errors/position_manager.rs +++ b/prusti-viper/src/encoder/errors/position_manager.rs @@ -37,6 +37,8 @@ impl<'tcx> PositionManager<'tcx> } } + /// Registers a new span and returns the corresponding VIR position. + /// The line and column of the VIR position correspond to the start of the given span. #[tracing::instrument(level = "trace", skip(self), ret)] pub fn register_span + Debug>(&mut self, def_id: ProcedureDefId, span: T) -> Position { let span = span.into(); diff --git a/viper/tests/multiple_errors.rs b/viper/tests/multiple_errors.rs new file mode 100644 index 00000000000..e7391c3b1bf --- /dev/null +++ b/viper/tests/multiple_errors.rs @@ -0,0 +1,87 @@ +use std::{sync::Once, vec}; +use viper::*; + +static INIT: Once = Once::new(); + +lazy_static::lazy_static! { + static ref VIPER: Viper = Viper::new_for_tests(); +} + +/// Setup function that is only run once, even if called multiple times. +fn setup() { + INIT.call_once(|| { + env_logger::init(); + }); +} + +fn verify_multiple_errors(backend: viper::VerificationBackend, args: Vec) { + setup(); + + let verification_context: VerificationContext = VIPER.attach_current_thread(); + let ast = verification_context.new_ast_factory(); + + let pos_1 = ast.identifier_position(123, 0, "pos-id:123"); + let pos_1b = ast.identifier_position(1230, 0, "pos-id:1230"); + let assertion_1 = ast.assert( + ast.eq_cmp_with_pos(ast.local_var("x", ast.int_type()), ast.int_lit(0), pos_1b), + pos_1, + ); + + let havoc = ast.local_var_assign( + ast.local_var("x", ast.int_type()), + ast.local_var("v", ast.int_type()), + ); + + let pos_2 = ast.identifier_position(456, 0, "pos-id:456"); + let pos_2b = ast.identifier_position(4560, 0, "pos-id:4560"); + let assertion_2 = ast.assert( + ast.eq_cmp_with_pos(ast.local_var("x", ast.int_type()), ast.int_lit(0), pos_2b), + pos_2, + ); + + let body = ast.seqn( + &[assertion_1, havoc, assertion_2], + &[ast.local_var_decl("x", ast.int_type()).into()], + ); + let method = ast.method( + "foo", + &[ast.local_var_decl("v", ast.int_type())], + &[], + &[], + &[], + Some(body), + ); + let program = ast.program(&[], &[], &[], &[], &[method]); + + let mut verifier = + verification_context.new_verifier_with_default_smt_and_extra_args(backend, args); + + let verification_result = verifier.verify(program); + + if let VerificationResult::Failure(errors) = verification_result { + assert_eq!(errors.len(), 2); + assert_eq!( + errors[0].full_id, + "assert.failed:assertion.false".to_string() + ); + assert_eq!( + errors[1].full_id, + "assert.failed:assertion.false".to_string() + ); + assert_eq!(errors[0].offending_pos_id, Some("pos-id:123".to_string())); + assert_eq!(errors[1].offending_pos_id, Some("pos-id:456".to_string())); + } else { + unreachable!("{:?}", verification_result); + } +} + +#[test] +fn report_multiple_errors_with_silicon() { + verify_multiple_errors( + viper::VerificationBackend::Silicon, + vec![ + "--logLevel=INFO".to_string(), + "--numberOfErrorsToReport=0".to_string(), + ], + ); +}