Use new VerificationResult type

Ported change from PR viperproject#1334

prusti-server/src/backend.rs

@@ -3,14 +3,14 @@ use prusti_utils::{
     config,
     Stopwatch,
 };
-use viper::{VerificationContext, VerificationResult};
+use viper::{VerificationContext, VerificationResultKind};
 
 pub enum Backend<'a> {
     Viper(viper::Verifier<'a>, &'a VerificationContext<'a>),
 }
 
 impl<'a> Backend<'a> {
-    pub fn verify(&mut self, program: vir::ProgramRef) -> VerificationResult {
+    pub fn verify(&mut self, program: vir::ProgramRef) -> VerificationResultKind {
         match self {
             Backend::Viper(viper, context) => {
                 let mut stopwatch =

prusti-server/src/process_verification.rs

@@ -14,7 +14,7 @@ use prusti_utils::{
 };
 use std::{fs::create_dir_all, path::PathBuf};
 use viper::{
-    smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult,
+    smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult, VerificationResultKind
 };
 
 #[tracing::instrument(level = "debug", skip_all, fields(program = %request.program.get_name()))]
@@ -116,10 +116,19 @@ pub fn process_verification_request<'v, 't: 'v>(
     };
 
     stopwatch.start_next("backend verification");
-    let result = backend.verify(request.program);
+    // let result = backend.verify(request.program);
+    let mut result = VerificationResult {
+        item_name: request.program.get_name().to_string(),
+        kind: VerificationResultKind::Success,
+        cached: false,
+        time_ms: 0,
+    };
+    // result.kind = backend.verify(request.program, sender.clone());
+    result.kind = backend.verify(request.program);
+    result.time_ms = stopwatch.finish().as_millis();
 
     // Don't cache Java exceptions, which might be due to misconfigured paths.
-    if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) {
+    if config::enable_cache() && !matches!(result.kind, VerificationResultKind::JavaException(_)) {
         info!(
             "Storing new cached result {:?} for program {}",
             &result,

prusti-server/tests/basic_requests.rs

@@ -4,7 +4,7 @@ use prusti_server::{
     spawn_server_thread, tokio::runtime::Builder, PrustiClient, VerificationRequest,
     ViperBackendConfig,
 };
-use viper::VerificationResult;
+use viper::VerificationResultKind;
 
 lazy_static! {
     // only start the jvm & server once
@@ -21,7 +21,7 @@ fn consistency_error() {
     });
 
     match result {
-        VerificationResult::ConsistencyErrors(errors) => assert_eq!(errors.len(), 1),
+        VerificationResultKind::ConsistencyErrors(errors) => assert_eq!(errors.len(), 1),
         other => panic!("consistency errors not identified, instead found {other:?}"),
     }
 }
@@ -31,12 +31,12 @@ fn empty_program() {
     let result = process_program(|_| ());
 
     match result {
-        VerificationResult::Success => {}
+        VerificationResultKind::Success => {}
         other => panic!("empty program not verified successfully, instead found {other:?}"),
     }
 }
 
-fn process_program<F>(configure: F) -> VerificationResult
+fn process_program<F>(configure: F) -> VerificationResultKind
 where
     F: FnOnce(&mut Program),
 {

prusti/src/verifier.rs

@@ -55,7 +55,7 @@ pub fn verify(env: Environment<'_>, def_spec: typed::DefSpecificationMap) {
 
         let results = prusti_server::verify_programs(vec![program]);
         println!("verification results: {results:?}");
-        if !results.iter().all(|(_, r)| matches!(r, viper::VerificationResult::Success)) {
+        if !results.iter().all(|(_, r)| matches!(r.kind, viper::VerificationResultKind::Success)) {
             // TODO: This will be unnecessary if diagnostic errors are emitted
             // earlier, it's useful for now to ensure that Prusti returns an
             // error code when verification fails

viper/src/verification_result.rs

@@ -6,9 +6,32 @@
 
 use crate::{silicon_counterexample::SiliconCounterexample, JavaException};
 
+#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
+pub struct VerificationResult {
+    pub item_name: String,
+    pub kind: VerificationResultKind,
+    pub cached: bool,
+    pub time_ms: u128,
+}
+
+impl VerificationResult {
+    pub fn is_success(&self) -> bool {
+        self.kind.is_success()
+    }
+
+    pub fn dummy_success() -> Self {
+        VerificationResult {
+            item_name: "".to_string(),
+            kind: VerificationResultKind::Success,
+            cached: false,
+            time_ms: 0,
+        }
+    }
+}
+
 /// The result of a verification request on a Viper program.
 #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)]
-pub enum VerificationResult {
+pub enum VerificationResultKind {
     /// The program verified.
     Success,
     /// The program did not verify.
@@ -25,7 +48,7 @@ pub struct ConsistencyError {
     pub pos_id: Option<String>
 }
 
-impl VerificationResult {
+impl VerificationResultKind {
     pub fn is_success(&self) -> bool {
         matches!(self, Self::Success)
     }

viper/src/verifier.rs

@@ -11,7 +11,7 @@ use crate::{
     silicon_counterexample::SiliconCounterexample,
     smt_manager::SmtManager,
     verification_backend::VerificationBackend,
-    verification_result::{VerificationError, VerificationResult}, ConsistencyError,
+    verification_result::{VerificationError, VerificationResultKind}, ConsistencyError,
 };
 use jni::{errors::Result, objects::JObject, JNIEnv};
 use log::{debug, error, info};
@@ -184,7 +184,7 @@ impl<'a> Verifier<'a> {
     }
 
     #[tracing::instrument(name = "viper::verify", level = "debug", skip_all)]
-    pub fn verify(&mut self, program: Program) -> VerificationResult {
+    pub fn verify(&mut self, program: Program) -> VerificationResultKind {
         let ast_utils = self.ast_utils;
         ast_utils.with_local_frame(16, || {
             debug!(
@@ -196,7 +196,7 @@ impl<'a> Verifier<'a> {
                 let consistency_errors = match self.ast_utils.check_consistency(program) {
                     Ok(errors) => errors,
                     Err(java_exception) => {
-                        return VerificationResult::JavaException(java_exception);
+                        return VerificationResultKind::JavaException(java_exception);
                     }
                 };
             );
@@ -209,7 +209,7 @@ impl<'a> Verifier<'a> {
                     "The provided Viper program has {} consistency errors.",
                     consistency_errors.len()
                 );
-                return VerificationResult::ConsistencyErrors(
+                return VerificationResultKind::ConsistencyErrors(
                     consistency_errors
                         .into_iter()
                         .map(|e| {
@@ -399,9 +399,9 @@ impl<'a> Verifier<'a> {
                     ))
                 }
 
-                VerificationResult::Failure(errors)
+                VerificationResultKind::Failure(errors)
             } else {
-                VerificationResult::Success
+                VerificationResultKind::Success
             }
         })
     }

viper/tests/invalid_programs.rs

@@ -32,7 +32,7 @@ fn runtime_error() {
 
     assert!(matches!(
         verification_result,
-        VerificationResult::JavaException(_)
+        VerificationResultKind::JavaException(_)
     ));
 }
 
@@ -99,7 +99,7 @@ where
 
     let verification_result = verifier.verify(program);
     match verification_result {
-        VerificationResult::ConsistencyErrors(_) => (),
+        VerificationResultKind::ConsistencyErrors(_) => (),
         other => panic!("consistency errors not identified, instead found {other:?}"),
     }
 }

viper/tests/simple_programs.rs

@@ -56,7 +56,7 @@ fn failure_with_assert_false() {
 
     let verification_result = verifier.verify(program);
 
-    if let VerificationResult::Failure(errors) = verification_result {
+    if let VerificationResultKind::Failure(errors) = verification_result {
         assert_eq!(errors.len(), 1);
         assert_eq!(
             errors[0].full_id,
@@ -204,7 +204,7 @@ fn failure_with_assign_if_and_assert() {
 
     let verification_result = verifier.verify(program);
 
-    if let VerificationResult::Failure(errors) = verification_result {
+    if let VerificationResultKind::Failure(errors) = verification_result {
         assert_eq!(errors.len(), 1);
         assert_eq!(
             errors[0].full_id,