diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index f68f862f4e8..fc8a910aa7d 100644 --- a/.github/workflows/test.yml +++ b/.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 diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index 273f44ea5d9..f5b0b75919c 100644 --- a/prusti-server/src/verification_request.rs +++ b/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(), diff --git a/prusti-tests/tests/verify/fail/assert-false/error-position.rs b/prusti-tests/tests/verify/fail/assert-false/error-position.rs index b919befa2c5..24e9e5d98a3 100644 --- a/prusti-tests/tests/verify/fail/assert-false/error-position.rs +++ b/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() {} diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 01779ff4991..6ec69d9eb11 100644 --- a/viper-sys/build.rs +++ b/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"), diff --git a/viper-sys/tests/verify_empty_program.rs b/viper-sys/tests/verify_empty_program.rs index 8dcd2f94637..2893cfd0398 100644 --- a/viper-sys/tests/verify_empty_program.rs +++ b/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()) }) diff --git a/viper-toolchain b/viper-toolchain index 99decd43dbe..ec151ba4cff 100644 --- a/viper-toolchain +++ b/viper-toolchain @@ -1 +1 @@ -v-2023-05-17-0733 +v4.2.2 diff --git a/viper/src/verification_context.rs b/viper/src/verification_context.rs index 2537431c837..14fc03beb49 100644 --- a/viper/src/verification_context.rs +++ b/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) } } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index ea39719ee72..93f7b587d50 100644 --- a/viper/src/verifier.rs +++ b/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> { - 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::>(), ); 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)); }