Merge pull request #317 from viperproject/upgrade-scala-2.13

Upgrade Java bindings for Scala 2.13

.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

.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

.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

.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

.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

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::*;
 

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{

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<PathBuf>,
 }
 
 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<PathBuf> {
+    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<dyn Error>> {
     color_backtrace::install();
     setup_logs();
@@ -85,14 +112,20 @@ fn main() -> Result<(), Box<dyn Error>> {
     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<dyn Error>> {
                 .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);

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!(),

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()?,

viper/src/jni_utils.rs

@@ -100,13 +100,13 @@ impl<'a> JniUtils<'a> {
 
     /// Converts a Rust Vec<JObject> 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

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')