Use position IDs as Viper line numbers (#1418)

* Use position IDs as Viper line numbers

* Add flag to configure number of errors per function

* Test reporting of multiple errors

Author: fpoli

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], &[])
             }

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());
                 }

prusti-utils/src/config.rs

@@ -129,6 +129,7 @@ lazy_static::lazy_static! {
         settings.set_default("use_new_encoder", true).unwrap();
         settings.set_default::<Option<u8>>("number_of_parallel_verifiers", None).unwrap();
         settings.set_default::<Option<String>>("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")
+}

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<T: Into<MultiSpan> + Debug>(&mut self, def_id: ProcedureDefId, span: T) -> Position {
         let span = span.into();

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<String>) {
+    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(),
+        ],
+    );
+}