Test Viper release and usage of updated API

.github/workflows/test.yml

@@ -250,7 +250,7 @@ jobs:
           # Restore from the most recent cache that matches a shared prefix of the key
           restore-keys: ${{ env.VER_CACHE_KEY_SHARED }}
       - name: Build with cargo
-        run: python x.py build --all
+        run: python x.py build --all --jobs 1
       - name: Run cargo tests
         run: python x.py test --all
       - name: Run a subset of tests with Carbon

prusti-server/src/verification_request.rs

@@ -54,6 +54,7 @@ impl ViperBackendConfig {
                 }
 
                 verifier_args.extend(vec![
+                    "--disableTerminationPlugin".to_string(),
                     "--assertTimeout".to_string(),
                     config::assert_timeout().to_string(),
                     "--proverConfigArgs".to_string(),

prusti-tests/tests/verify/fail/assert-false/error-position.rs

@@ -27,16 +27,22 @@ fn foo8(x: bool) {}
 #[ensures(x || true ==> !(x || !x))] //~ ERROR postcondition might not hold
 fn foo9(x: bool) {}
 
-#[ensures(x == x)]
-#[ensures(false)] //~ ERROR postcondition might not hold
+// The exact error position reported in some of the cases below depends on AST
+// optimisations performed within Silver; in particular, the `x == x` part is
+// no longer optimised to `true` (since Silver commit 86d3ab9). `foo14` below
+// was added to make sure precise error positions can be reported in
+// postconditions without depending on AST optimisations.
+
+#[ensures(x == x)] //~ ERROR postcondition might not hold
+#[ensures(false)]
 fn foo10(x: bool) {}
 
 #[ensures(false)] //~ ERROR postcondition might not hold
 #[ensures(x == x)]
 fn foo11(x: bool) {}
 
-#[ensures(x == x)]
-#[ensures(!true)] //~ ERROR postcondition might not hold
+#[ensures(x == x)] //~ ERROR postcondition might not hold
+#[ensures(!true)]
 #[ensures(x == x)]
 fn foo12(x: bool) {}
 
@@ -46,4 +52,15 @@ pub fn foo13(x: u32) -> u32 {
     x
 }
 
+#[trusted] #[pure] fn unk1() -> bool { unimplemented!() }
+#[trusted] #[pure] fn unk2() -> bool { unimplemented!() }
+#[trusted] #[pure] fn unk3() -> bool { unimplemented!() }
+
+#[requires(unk1())]
+#[requires(unk3())]
+#[ensures(unk1())]
+#[ensures(unk2())] //~ ERROR postcondition might not hold
+#[ensures(unk3())]
+fn foo14() {}
+
 fn main() {}

viper-sys/build.rs

@@ -129,28 +129,19 @@ fn main() {
                 method!("apply"),
             ]),
             // Silicon
-            java_class!("viper.silicon.Silicon", vec![
-                constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"),
-            ]),
-            java_class!("viper.silicon.SiliconFrontend", vec![
-                constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"),
+            java_class!("viper.silicon.SiliconFrontendAPI", vec![
+                constructor!("(Lviper/silver/reporter/Reporter;)V"),
             ]),
             // Carbon
-            java_class!("viper.carbon.CarbonVerifier", vec![
-                constructor!("(Lviper/silver/reporter/Reporter;Lscala/collection/immutable/Seq;)V"),
-            ]),
-            java_class!("viper.carbon.CarbonFrontend", vec![
-                constructor!("(Lviper/silver/reporter/Reporter;Lch/qos/logback/classic/Logger;)V"),
+            java_class!("viper.carbon.CarbonFrontendAPI", vec![
+                constructor!("(Lviper/silver/reporter/Reporter;)V"),
             ]),
             // Silver
-            java_class!("viper.silver.frontend.SilFrontend", vec![
-                method!("setVerifier"),
-                method!("verification"),
-                method!("getVerificationResult"),
-                method!("setState"),
+            java_class!("viper.silver.frontend.ViperFrontendAPI", vec![
+                method!("initialize"),
+                method!("verify"),
+                method!("stop"),
                 method!("verifier"),
-                trait_field!("_verifier"),
-                trait_field!("_program"),
             ]),
             java_class!("viper.silver.reporter.CSVReporter", vec![
                 constructor!("(Ljava/lang/String;Ljava/lang/String;)V"),
@@ -161,10 +152,6 @@ fn main() {
             java_class!("viper.silver.verifier.Verifier", vec![
                 method!("name"),
                 method!("buildVersion"),
-                method!("parseCommandLine"),
-                method!("start"),
-                method!("stop"),
-                method!("verify"),
             ]),
             java_class!("viper.silver.frontend.DefaultStates", vec![
                 method!("ConsistencyCheck"),

viper-sys/tests/verify_empty_program.rs

@@ -48,9 +48,8 @@ fn verify_empty_program() {
 
     env.with_local_frame(32, || {
         let reporter = viper::silver::reporter::NoopReporter_object::with(&env).singleton()?;
-        let debug_info = scala::collection::immutable::Nil_object::with(&env).singleton()?;
-        let silicon = viper::silicon::Silicon::with(&env).new(reporter, debug_info)?;
-        let verifier = viper::silver::verifier::Verifier::with(&env);
+        let silicon = viper::silicon::SiliconFrontendAPI::with(&env).new(reporter)?;
+        let frontend = viper::silver::frontend::ViperFrontendAPI::with(&env);
 
         let array_buffer_wrapper = scala::collection::mutable::ArrayBuffer::with(&env);
         let silicon_args_array = array_buffer_wrapper.new(4)?;
@@ -59,15 +58,9 @@ fn verify_empty_program() {
 
         array_buffer_wrapper.call_append(silicon_args_array, *env.new_string(&z3_path)?)?;
 
-        array_buffer_wrapper.call_append(silicon_args_array, *env.new_string("--ignoreFile")?)?;
-
-        array_buffer_wrapper.call_append(silicon_args_array, *env.new_string("dummy.vpr")?)?;
-
         let silicon_args_seq = array_buffer_wrapper.call_toSeq(silicon_args_array)?;
 
-        verifier.call_parseCommandLine(silicon, silicon_args_seq)?;
-
-        verifier.call_start(silicon)?;
+        frontend.call_initialize(silicon, silicon_args_seq)?;
 
         let program = viper::silver::ast::Program::with(&env).new(
             scala::collection::immutable::Nil_object::with(&env).singleton()?,
@@ -81,13 +74,13 @@ fn verify_empty_program() {
             viper::silver::ast::NoTrafos_object::with(&env).singleton()?,
         )?;
 
-        let verification_result = verifier.call_verify(silicon, program)?;
+        let verification_result = frontend.call_verify(silicon, program)?;
 
         let system_out = get_system_out(&env)?;
 
         java::io::PrintStream::with(&env).call_println(system_out, verification_result)?;
 
-        verifier.call_stop(silicon)?;
+        frontend.call_stop(silicon)?;
 
         Ok(JObject::null())
     })

viper-toolchain

@@ -1 +1 @@
-v-2023-05-17-0733
+v4.2.2

viper/src/verification_context.rs

@@ -90,13 +90,9 @@ impl<'a> VerificationContext<'a> {
         }
 
         verifier_args.extend(extra_args);
-        verifier_args.push("--ignoreFile".to_string());
-        verifier_args.push("dummy.vpr".to_string());
 
         debug!("Verifier arguments: '{}'", verifier_args.to_vec().join(" "));
 
-        Verifier::new(&self.env, backend, report_path, smt_manager)
-            .parse_command_line(&verifier_args)
-            .start()
+        Verifier::new(&self.env, backend, report_path, smt_manager).initialize(&verifier_args)
     }
 }

viper/src/verifier.rs

@@ -13,16 +13,14 @@ use crate::{
     verification_backend::VerificationBackend,
     verification_result::{VerificationError, VerificationResult},
 };
-use jni::{errors::Result, objects::JObject, JNIEnv};
+use jni::{objects::JObject, JNIEnv};
 use log::{debug, error, info};
 use std::path::PathBuf;
 use viper_sys::wrappers::{scala, viper::*};
 
 pub struct Verifier<'a> {
     env: &'a JNIEnv<'a>,
-    verifier_wrapper: silver::verifier::Verifier<'a>,
-    verifier_instance: JObject<'a>,
-    frontend_wrapper: silver::frontend::SilFrontend<'a>,
+    frontend_wrapper: silver::frontend::ViperFrontendAPI<'a>,
     frontend_instance: JObject<'a>,
     jni: JniUtils<'a>,
     ast_utils: AstUtils<'a>,
@@ -38,8 +36,7 @@ impl<'a> Verifier<'a> {
     ) -> Self {
         let jni = JniUtils::new(env);
         let ast_utils = AstUtils::new(env);
-        let verifier_wrapper = silver::verifier::Verifier::with(env);
-        let frontend_wrapper = silver::frontend::SilFrontend::with(env);
+        let frontend_wrapper = silver::frontend::ViperFrontendAPI::with(env);
 
         let frontend_instance = jni.unwrap_result(env.with_local_frame(16, || {
             let reporter = if let Some(real_report_path) = report_path {
@@ -51,68 +48,23 @@ impl<'a> Verifier<'a> {
                 jni.unwrap_result(silver::reporter::NoopReporter_object::with(env).singleton())
             };
 
-            let debug_info = jni.new_seq(&[]);
-
-            let backend_unwrapped = Self::instantiate_verifier(backend, env, reporter, debug_info);
-            let backend_instance = jni.unwrap_result(backend_unwrapped);
-
-            let logger_singleton =
-                jni.unwrap_result(silver::logger::SilentLogger_object::with(env).singleton());
-            let logger_factory = jni.unwrap_result(
-                silver::logger::SilentLogger_object::with(env).call_apply(logger_singleton),
-            );
-            let logger =
-                jni.unwrap_result(silver::logger::ViperLogger::with(env).call_get(logger_factory));
-
             let unwrapped_frontend_instance = {
                 match backend {
                     VerificationBackend::Silicon => {
-                        silicon::SiliconFrontend::with(env).new(reporter, logger)
+                        silicon::SiliconFrontendAPI::with(env).new(reporter)
                     }
                     VerificationBackend::Carbon => {
-                        carbon::CarbonFrontend::with(env).new(reporter, logger)
+                        carbon::CarbonFrontendAPI::with(env).new(reporter)
                     }
                 }
             };
             let frontend_instance = jni.unwrap_result(unwrapped_frontend_instance);
 
-            frontend_wrapper
-                .call_setVerifier(frontend_instance, backend_instance)
-                .unwrap();
-            let verifier_option = jni.new_option(Some(backend_instance));
-
-            frontend_wrapper
-                .set___verifier(frontend_instance, verifier_option)
-                .unwrap();
-
             Ok(frontend_instance)
         }));
 
-        let verifier_instance = jni.unwrap_result(env.with_local_frame(16, || {
-            let verifier_instance =
-                jni.unwrap_result(frontend_wrapper.call_verifier(frontend_instance));
-
-            let consistency_check_state = silver::frontend::DefaultStates::with(env)
-                .call_ConsistencyCheck()
-                .unwrap();
-
-            frontend_wrapper
-                .call_setState(frontend_instance, consistency_check_state)
-                .unwrap();
-
-            let name =
-                jni.to_string(jni.unwrap_result(verifier_wrapper.call_name(verifier_instance)));
-            let build_version = jni.to_string(
-                jni.unwrap_result(verifier_wrapper.call_buildVersion(verifier_instance)),
-            );
-            info!("Using backend {} version {}", name, build_version);
-            Ok(verifier_instance)
-        }));
-
         Verifier {
             env,
-            verifier_wrapper,
-            verifier_instance,
             frontend_wrapper,
             frontend_instance,
             jni,
@@ -121,24 +73,9 @@ impl<'a> Verifier<'a> {
         }
     }
 
-    #[tracing::instrument(level = "debug", skip_all)]
-    fn instantiate_verifier(
-        backend: VerificationBackend,
-        env: &'a JNIEnv,
-        reporter: JObject,
-        debug_info: JObject,
-    ) -> Result<JObject<'a>> {
-        match backend {
-            VerificationBackend::Silicon => silicon::Silicon::with(env).new(reporter, debug_info),
-            VerificationBackend::Carbon => {
-                carbon::CarbonVerifier::with(env).new(reporter, debug_info)
-            }
-        }
-    }
-
     #[must_use]
     #[tracing::instrument(level = "debug", skip_all)]
-    pub fn parse_command_line(self, args: &[String]) -> Self {
+    pub fn initialize(self, args: &[String]) -> Self {
         self.ast_utils.with_local_frame(16, || {
             let args = self.jni.new_seq(
                 &args
@@ -147,19 +84,23 @@ impl<'a> Verifier<'a> {
                     .collect::<Vec<JObject>>(),
             );
             self.jni.unwrap_result(
-                self.verifier_wrapper
-                    .call_parseCommandLine(self.verifier_instance, args),
+                self.frontend_wrapper
+                    .call_initialize(self.frontend_instance, args),
             );
-        });
-        self
-    }
+            let verifier_wrapper = silver::verifier::Verifier::with(self.env);
+            let verifier_instance = self
+                .jni
+                .unwrap_result(self.frontend_wrapper.call_verifier(self.frontend_instance));
 
-    #[must_use]
-    #[tracing::instrument(level = "debug", skip_all)]
-    pub fn start(self) -> Self {
-        self.ast_utils.with_local_frame(16, || {
-            self.jni
-                .unwrap_result(self.verifier_wrapper.call_start(self.verifier_instance));
+            let name = self.jni.to_string(
+                self.jni
+                    .unwrap_result(verifier_wrapper.call_name(verifier_instance)),
+            );
+            let build_version = self.jni.to_string(
+                self.jni
+                    .unwrap_result(verifier_wrapper.call_buildVersion(verifier_instance)),
+            );
+            info!("Using backend {} version {}", name, build_version);
         });
         self
     }
@@ -195,13 +136,8 @@ impl<'a> Verifier<'a> {
                 );
             }
 
-            let program_option = self.jni.new_option(Some(program.to_jobject()));
-            self.jni.unwrap_result(self.frontend_wrapper.set___program(self.frontend_instance, program_option));
-
             run_timed!("Viper verification", debug,
-                self.jni.unwrap_result(self.frontend_wrapper.call_verification(self.frontend_instance));
-                let viper_result_option = self.jni.unwrap_result(self.frontend_wrapper.call_getVerificationResult(self.frontend_instance));
-                let viper_result = self.jni.unwrap_result(scala::Some::with(self.env).call_get(viper_result_option));
+                let viper_result = self.jni.unwrap_result(self.frontend_wrapper.call_verify(self.frontend_instance, program.to_jobject()));
             );
             debug!(
                 "Viper verification result: {}",
@@ -404,11 +340,9 @@ impl<'a> Drop for Verifier<'a> {
     fn drop(&mut self) {
         // Tell the verifier to stop its threads.
         self.jni
-            .unwrap_result(self.verifier_wrapper.call_stop(self.verifier_instance));
+            .unwrap_result(self.frontend_wrapper.call_stop(self.frontend_instance));
         // Delete the local reference to the verifier in the JVM
         // so that the JVM garbage collector can clean it up.
-        self.jni
-            .unwrap_result(self.env.delete_local_ref(self.verifier_instance));
         self.jni
             .unwrap_result(self.env.delete_local_ref(self.frontend_instance));
     }