diff --git a/.github/workflows/benchmarks.yaml b/.github/workflows/benchmarks.yaml index 61a24c2f14e..44a82d9dc5a 100644 --- a/.github/workflows/benchmarks.yaml +++ b/.github/workflows/benchmarks.yaml @@ -22,6 +22,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index 8dceb05cfa6..911191b04b3 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -22,6 +22,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml index 4312302bb11..187383617ee 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -23,6 +23,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo --release diff --git a/.github/workflows/test-on-crates.yml b/.github/workflows/test-on-crates.yml index dbc6c357d46..19097367525 100644 --- a/.github/workflows/test-on-crates.yml +++ b/.github/workflows/test-on-crates.yml @@ -17,6 +17,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo --release diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 4bb4a21412f..81b21e2d349 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -24,6 +24,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Cache cargo @@ -53,6 +56,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo @@ -75,6 +81,9 @@ jobs: uses: actions/setup-python@v2 with: python-version: '3.x' + - uses: actions/setup-java@v1 + with: + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo diff --git a/prusti-tests/tests/verify/pass/quick/knapsack.rs b/prusti-tests/tests/verify/pass/quick/knapsack.rs index eb24e9f3a94..23fd5313fef 100644 --- a/prusti-tests/tests/verify/pass/quick/knapsack.rs +++ b/prusti-tests/tests/verify/pass/quick/knapsack.rs @@ -16,7 +16,7 @@ //! + We could not express the postcondition that the result is //! correct because that requires support for comprehensions. -// ignore-test: this test it's flaky because it uses nonlinear arithmetic. +// ignore-test: this test is flaky because it uses nonlinear arithmetic. use prusti_contracts::*; diff --git a/prusti-tests/tests/verify/pass/quick/mut-borrows-binary-search.rs b/prusti-tests/tests/verify/pass/quick/mut-borrows-binary-search.rs index d11f28987df..84cb6f36ff4 100644 --- a/prusti-tests/tests/verify/pass/quick/mut-borrows-binary-search.rs +++ b/prusti-tests/tests/verify/pass/quick/mut-borrows-binary-search.rs @@ -1,6 +1,8 @@ //! Regression tests extracted from //! https://rosettacode.org/wiki/Binary_search#Rust +// ignore-test: this test is flaky. + use prusti_contracts::*; pub struct VecWrapperI32{ diff --git a/test-crates/src/main.rs b/test-crates/src/main.rs index f5d63a831cd..819c1d596c9 100644 --- a/test-crates/src/main.rs +++ b/test-crates/src/main.rs @@ -4,9 +4,11 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use std::path::{Path, PathBuf}; +use std::env; use std::error::Error; use std::fs; +use std::path::{Path, PathBuf}; +use std::process::Command; use rustwide::{ cmd, @@ -44,6 +46,7 @@ struct CargoPrusti { prusti_home: PathBuf, viper_home: PathBuf, z3_exe: PathBuf, + java_home: Option, } impl cmd::Runnable for CargoPrusti { @@ -52,9 +55,12 @@ impl cmd::Runnable for CargoPrusti { } fn prepare_command<'w, 'pl>(&self, cmd: cmd::Command<'w, 'pl>) -> cmd::Command<'w, 'pl> { + let java_home = self.java_home.as_ref() + .map(|p| p.to_str().unwrap()) + .unwrap_or("/usr/lib/jvm/default-java"); cmd.env("VIPER_HOME", self.viper_home.to_str().unwrap()) .env("Z3_EXE", self.z3_exe.join("z3").to_str().unwrap()) - .env("JAVA_HOME", "/usr/lib/jvm/java-8-openjdk-amd64") + .env("JAVA_HOME", java_home) .env("CARGO_PATH", "/opt/rustwide/cargo-home/bin/cargo") } } @@ -77,6 +83,27 @@ fn get_rust_toolchain() -> RustToolchain { rust_toolchain.toolchain } +/// Find the Java home directory +pub fn find_java_home() -> Option { + Command::new("java") + .arg("-XshowSettings:properties") + .arg("-version") + .output() + .ok() + .and_then(|output| { + let stdout = String::from_utf8_lossy(&output.stdout); + let stderr = String::from_utf8_lossy(&output.stderr); + for line in stdout.lines().chain(stderr.lines()) { + if line.contains("java.home") { + let pos = line.find('=').unwrap() + 1; + let path = line[pos..].trim(); + return Some(PathBuf::from(path)); + } + } + None + }) +} + fn main() -> Result<(), Box> { color_backtrace::install(); setup_logs(); @@ -85,14 +112,20 @@ fn main() -> Result<(), Box> { let host_prusti_home = Path::new("target/release"); let host_viper_home = Path::new("viper_tools/backends"); let host_z3_home = Path::new("viper_tools/z3/bin"); + let host_java_home = env::var("JAVA_HOME").ok().map(|s| s.into()) + .or_else(|| find_java_home()) + .expect("Please set JAVA_HOME"); let guest_prusti_home = Path::new("/opt/rustwide/prusti-home"); let guest_viper_home = Path::new("/opt/rustwide/viper-home"); let guest_z3_home = Path::new("/opt/rustwide/z3-home"); + let guest_java_home = Path::new("/opt/rustwide/java-home"); + info!("Using host's Java home {:?}", host_java_home); let cargo_prusti = CargoPrusti { prusti_home: guest_prusti_home.to_path_buf(), viper_home: guest_viper_home.to_path_buf(), z3_exe: guest_z3_home.to_path_buf(), + java_home: Some(guest_java_home.to_path_buf()), }; info!("Crate a new workspace..."); @@ -177,7 +210,8 @@ fn main() -> Result<(), Box> { .enable_networking(false) .mount(&host_prusti_home, &guest_prusti_home, cmd::MountKind::ReadOnly) .mount(&host_viper_home, &guest_viper_home, cmd::MountKind::ReadOnly) - .mount(&host_z3_home, &guest_z3_home, cmd::MountKind::ReadOnly); + .mount(&host_z3_home, &guest_z3_home, cmd::MountKind::ReadOnly) + .mount(&host_java_home, &guest_java_home, cmd::MountKind::ReadOnly); let mut storage = LogStorage::new(LevelFilter::Info); storage.set_max_size(1024 * 1024); diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 628021f2970..8161f694192 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -107,17 +107,21 @@ fn main() { java_class!("scala.math.BigInt", vec![ constructor!(), ]), - java_class!("scala.collection.mutable.ArraySeq", vec![ - constructor!(), - method!("update"), + java_class!("scala.collection.mutable.ArrayBuffer", vec![ + constructor!("(I)V"), + method!("append", "(Ljava/lang/Object;)Lscala/collection/mutable/Buffer;"), + method!("toSeq"), ]), java_class!("scala.collection.mutable.ListBuffer", vec![ constructor!(), ]), java_class!("scala.collection.immutable.HashMap", vec![ - constructor!(), + constructor!("()V"), method!("updated", "(Ljava/lang/Object;Ljava/lang/Object;)Lscala/collection/immutable/HashMap;"), ]), + java_class!("scala.collection.immutable.Nil$", vec![ + object_getter!(), + ]), java_class!("scala.collection.Seq", vec![ method!("length"), method!("apply", "(I)Ljava/lang/Object;"), @@ -129,7 +133,7 @@ fn main() { ]), // Silicon java_class!("viper.silicon.Silicon", vec![ - constructor!("(Lviper/silver/plugin/PluginAwareReporter;Lscala/collection/Seq;)V"), + constructor!("(Lviper/silver/plugin/PluginAwareReporter;Lscala/collection/immutable/Seq;)V"), ]), // Carbon java_class!("viper.carbon.CarbonVerifier", vec![ @@ -229,7 +233,7 @@ fn main() { ]), java_class!("viper.silver.ast.DomainFuncApp$", vec![ object_getter!(), - method!("apply", "(Lviper/silver/ast/DomainFunc;Lscala/collection/Seq;Lscala/collection/immutable/Map;Lviper/silver/ast/Position;Lviper/silver/ast/Info;Lviper/silver/ast/ErrorTrafo;)Lviper/silver/ast/DomainFuncApp;"), + method!("apply", "(Lviper/silver/ast/DomainFunc;Lscala/collection/immutable/Seq;Lscala/collection/immutable/Map;Lviper/silver/ast/Position;Lviper/silver/ast/Info;Lviper/silver/ast/ErrorTrafo;)Lviper/silver/ast/DomainFuncApp;"), ]), java_class!("viper.silver.ast.DomainType", vec![ constructor!(), @@ -299,11 +303,11 @@ fn main() { ]), java_class!("viper.silver.ast.FuncApp", vec![ constructor!(), - method!("apply", "(Ljava/lang/String;Lscala/collection/Seq;Lviper/silver/ast/Position;Lviper/silver/ast/Info;Lviper/silver/ast/Type;Lviper/silver/ast/ErrorTrafo;)Lviper/silver/ast/FuncApp;"), + method!("apply", "(Ljava/lang/String;Lscala/collection/immutable/Seq;Lviper/silver/ast/Position;Lviper/silver/ast/Info;Lviper/silver/ast/Type;Lviper/silver/ast/ErrorTrafo;)Lviper/silver/ast/FuncApp;"), ]), java_class!("viper.silver.ast.FuncApp$", vec![ object_getter!(), - method!("apply", "(Lviper/silver/ast/Function;Lscala/collection/Seq;Lviper/silver/ast/Position;Lviper/silver/ast/Info;Lviper/silver/ast/ErrorTrafo;)Lviper/silver/ast/FuncApp;"), + method!("apply", "(Lviper/silver/ast/Function;Lscala/collection/immutable/Seq;Lviper/silver/ast/Position;Lviper/silver/ast/Info;Lviper/silver/ast/ErrorTrafo;)Lviper/silver/ast/FuncApp;"), ]), java_class!("viper.silver.ast.Function", vec![ constructor!(), diff --git a/viper-sys/tests/verify_empty_program.rs b/viper-sys/tests/verify_empty_program.rs index e69025a9518..8869d8b6bf2 100644 --- a/viper-sys/tests/verify_empty_program.rs +++ b/viper-sys/tests/verify_empty_program.rs @@ -59,7 +59,7 @@ fn verify_empty_program() { env.with_local_frame(32, || { let reporter = viper::silver::reporter::NoopReporter_object::with(&env).singleton()?; let plugin_aware_reporter = viper::silver::plugin::PluginAwareReporter::with(&env).new(reporter)?; - let debug_info = scala::collection::mutable::ArraySeq::with(&env).new(0)?; + let debug_info = scala::collection::immutable::Nil_object::with(&env).singleton()?; let silicon = viper::silicon::Silicon::with(&env).new(plugin_aware_reporter, debug_info)?; let verifier = viper::silver::verifier::Verifier::with(&env); @@ -97,12 +97,12 @@ fn verify_empty_program() { verifier.call_start(silicon)?; let program = viper::silver::ast::Program::with(&env).new( - scala::collection::mutable::ArraySeq::with(&env).new(0)?, - scala::collection::mutable::ArraySeq::with(&env).new(0)?, - scala::collection::mutable::ArraySeq::with(&env).new(0)?, - scala::collection::mutable::ArraySeq::with(&env).new(0)?, - scala::collection::mutable::ArraySeq::with(&env).new(0)?, - scala::collection::mutable::ArraySeq::with(&env).new(0)?, + scala::collection::immutable::Nil_object::with(&env).singleton()?, + scala::collection::immutable::Nil_object::with(&env).singleton()?, + scala::collection::immutable::Nil_object::with(&env).singleton()?, + scala::collection::immutable::Nil_object::with(&env).singleton()?, + scala::collection::immutable::Nil_object::with(&env).singleton()?, + scala::collection::immutable::Nil_object::with(&env).singleton()?, viper::silver::ast::NoPosition_object::with(&env).singleton()?, viper::silver::ast::NoInfo_object::with(&env).singleton()?, viper::silver::ast::NoTrafos_object::with(&env).singleton()?, diff --git a/viper/src/jni_utils.rs b/viper/src/jni_utils.rs index 65dc9f21a1b..b7966a0d7c8 100644 --- a/viper/src/jni_utils.rs +++ b/viper/src/jni_utils.rs @@ -100,13 +100,13 @@ impl<'a> JniUtils<'a> { /// Converts a Rust Vec to a Scala Seq pub fn new_seq(&self, objects: &[JObject]) -> JObject { - let array_seq_wrapper = scala::collection::mutable::ArraySeq::with(self.env); + let array_buffer_wrapper = scala::collection::mutable::ArrayBuffer::with(self.env); let len = objects.len(); - let res = self.unwrap_result(array_seq_wrapper.new(len as i32)); - for (i, obj) in objects.iter().enumerate() { - self.unwrap_result(array_seq_wrapper.call_update(res, i as i32, *obj)); + let res = self.unwrap_result(array_buffer_wrapper.new(len as i32)); + for obj in objects.iter() { + self.unwrap_result(array_buffer_wrapper.call_append(res, *obj)); } - res + self.unwrap_result(array_buffer_wrapper.call_toSeq(res)) } /// Converts a Java String to a Rust String diff --git a/x.py b/x.py index 0c7ba01b4c6..df378635bb7 100755 --- a/x.py +++ b/x.py @@ -191,7 +191,7 @@ def setup_ubuntu(): shell('sudo apt-get update') shell('sudo apt-get install -y ' 'build-essential pkg-config ' - 'wget gcc libssl-dev openjdk-8-jdk') + 'wget gcc libssl-dev') # Download Viper. shell('wget -q http://viper.ethz.ch/downloads/ViperToolsNightlyLinux.zip') shell('unzip ViperToolsNightlyLinux.zip -d viper_tools')