From 330457ef512124124c18ac67dbb00c5fbd466475 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 11 Dec 2020 16:27:39 +0100 Subject: [PATCH 1/6] Upgrade Java bindings for Scala 2.13 --- viper-sys/build.rs | 16 ++++++++-------- viper-sys/tests/verify_empty_program.rs | 14 +++++++------- viper/src/jni_utils.rs | 8 ++++---- 3 files changed, 19 insertions(+), 19 deletions(-) diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 628021f2970..705a1c3212e 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -107,15 +107,15 @@ 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;"), ]), 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.Seq", vec![ @@ -129,7 +129,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 +229,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 +299,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..ad7b7b02c69 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::mutable::ArrayBuffer::with(&env).new(0)?; 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::mutable::ArrayBuffer::with(&env).new(0)?, + scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, + scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, + scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, + scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, + scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, 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..e2e1f900475 100644 --- a/viper/src/jni_utils.rs +++ b/viper/src/jni_utils.rs @@ -100,11 +100,11 @@ 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 } From bae285c33920ce567519830358da8400a080f4cc Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 11 Dec 2020 17:02:16 +0100 Subject: [PATCH 2/6] Fix Java type error --- viper-sys/build.rs | 4 ++++ viper-sys/tests/verify_empty_program.rs | 14 +++++++------- viper/src/jni_utils.rs | 2 +- 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/viper-sys/build.rs b/viper-sys/build.rs index 705a1c3212e..8161f694192 100644 --- a/viper-sys/build.rs +++ b/viper-sys/build.rs @@ -110,6 +110,7 @@ fn main() { 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!(), @@ -118,6 +119,9 @@ fn main() { 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;"), diff --git a/viper-sys/tests/verify_empty_program.rs b/viper-sys/tests/verify_empty_program.rs index ad7b7b02c69..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::ArrayBuffer::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::ArrayBuffer::with(&env).new(0)?, - scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, - scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, - scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, - scala::collection::mutable::ArrayBuffer::with(&env).new(0)?, - scala::collection::mutable::ArrayBuffer::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 e2e1f900475..b7966a0d7c8 100644 --- a/viper/src/jni_utils.rs +++ b/viper/src/jni_utils.rs @@ -106,7 +106,7 @@ impl<'a> JniUtils<'a> { 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 From 7e1466804938a3825d95fc6956ef213502cf6bad Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 11 Dec 2020 19:22:13 +0100 Subject: [PATCH 3/6] Use Java 11 --- .github/workflows/benchmarks.yaml | 3 +++ .github/workflows/coverage.yml | 3 +++ .github/workflows/deploy.yml | 3 +++ .github/workflows/test-on-crates.yml | 3 +++ .github/workflows/test.yml | 9 +++++++++ x.py | 2 +- 6 files changed, 22 insertions(+), 1 deletion(-) diff --git a/.github/workflows/benchmarks.yaml b/.github/workflows/benchmarks.yaml index 61a24c2f14e..57b1fde8961 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: '11' - 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..91194a33a7e 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: '11' - 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..43985c1ca08 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: '11' - 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..636cf130b89 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: '11' - 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..1d48c689b5a 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: '11' - 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: '11' - 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: '11' - name: Set up the environment run: python x.py setup - name: Build with cargo diff --git a/x.py b/x.py index 0c7ba01b4c6..e063b8fca70 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 openjdk-11-jdk') # Download Viper. shell('wget -q http://viper.ethz.ch/downloads/ViperToolsNightlyLinux.zip') shell('unzip ViperToolsNightlyLinux.zip -d viper_tools') From beef4ddce9a3693fd6cf548f605bbcd0610cfc55 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Fri, 11 Dec 2020 19:34:53 +0100 Subject: [PATCH 4/6] Use Java 15 --- .github/workflows/benchmarks.yaml | 2 +- .github/workflows/coverage.yml | 2 +- .github/workflows/deploy.yml | 2 +- .github/workflows/test-on-crates.yml | 2 +- .github/workflows/test.yml | 6 +++--- x.py | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/benchmarks.yaml b/.github/workflows/benchmarks.yaml index 57b1fde8961..44a82d9dc5a 100644 --- a/.github/workflows/benchmarks.yaml +++ b/.github/workflows/benchmarks.yaml @@ -24,7 +24,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + 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 91194a33a7e..911191b04b3 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -24,7 +24,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + 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 43985c1ca08..187383617ee 100644 --- a/.github/workflows/deploy.yml +++ b/.github/workflows/deploy.yml @@ -25,7 +25,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + 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 636cf130b89..19097367525 100644 --- a/.github/workflows/test-on-crates.yml +++ b/.github/workflows/test-on-crates.yml @@ -19,7 +19,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + 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 1d48c689b5a..81b21e2d349 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -26,7 +26,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + java-version: '15' - name: Set up the environment run: python x.py setup - name: Cache cargo @@ -58,7 +58,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo @@ -83,7 +83,7 @@ jobs: python-version: '3.x' - uses: actions/setup-java@v1 with: - java-version: '11' + java-version: '15' - name: Set up the environment run: python x.py setup - name: Build with cargo diff --git a/x.py b/x.py index e063b8fca70..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-11-jdk') + 'wget gcc libssl-dev') # Download Viper. shell('wget -q http://viper.ethz.ch/downloads/ViperToolsNightlyLinux.zip') shell('unzip ViperToolsNightlyLinux.zip -d viper_tools') From 329aaadbb43cccb4dd6f9db37fce1a89bd887ae2 Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 14 Dec 2020 11:15:34 +0100 Subject: [PATCH 5/6] Disable flaky test --- prusti-tests/tests/verify/pass/quick/knapsack.rs | 2 +- .../tests/verify/pass/quick/mut-borrows-binary-search.rs | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) 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{ From a1743a3892768b0b08ef480aea6a86c4a07ccc8d Mon Sep 17 00:00:00 2001 From: Federico Poli Date: Mon, 14 Dec 2020 12:07:39 +0100 Subject: [PATCH 6/6] Use host's JAVA_HOME when running test-crates --- test-crates/src/main.rs | 40 +++++++++++++++++++++++++++++++++++++--- 1 file changed, 37 insertions(+), 3 deletions(-) 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);