Change prusti-server workflow

Port basic functionality for the new prusti-server work flow according
to PR viperproject#1334 .

prusti-server/Cargo.toml

@@ -20,20 +20,32 @@ doctest = false
 log = { version = "0.4", features = ["release_max_level_info"] }
 vir = { path = "../vir" }
 viper = { path = "../viper" }
+prusti-interface = { path = "../prusti-interface" }
 prusti-viper = { path = "../prusti-viper" }
 prusti-utils = { path = "../prusti-utils" }
+prusti-rustc-interface = { path = "../prusti-rustc-interface" }
+viper-sys = { path = "../viper-sys" }
 tracing = { path = "../tracing" }
 env_logger = "0.10"
 clap = { version = "4.0", features = ["derive"] }
 bincode = "1.0"
 url = "2.2.2"
 num_cpus = "1.14"
 serde = { version = "1.0", features = ["derive"] }
+serde_json = { version = "1.0" }
+jni = { version = "0.20", features = ["invocation"] }
+# the tungstenite version used by warp 0.3
+tokio-tungstenite = "0.13"
+futures = "0.3.25"
+futures-util = "0.3.25"
+async-stream = "0.3.3"
 reqwest = { version = "0.11", default-features = false, features = ["json", "rustls-tls"] }
 warp = "0.3"
-tokio = "1.20"
+# tokio = "1.20"
+tokio = { version = "1.20", features = ["io-util", "net", "rt", "sync"] }
 rustc-hash = "1.1.0"
 once_cell = "1.17.1"
 
+
 [dev-dependencies]
 lazy_static = "1.4.0"

prusti-server/src/backend.rs

@@ -1,18 +1,32 @@
-use crate::dump_viper_program;
+use crate::{dump_viper_program, ServerMessage};
+use log::{debug, info};
 use prusti_utils::{
     config,
     Stopwatch,
 };
-use viper::{VerificationContext, VerificationResultKind};
+use std::{
+    sync::{mpsc, Arc},
+    thread, time,
+};
+use viper::{jni_utils::JniUtils, VerificationContext, VerificationResultKind, Viper};
+use viper_sys::wrappers::{java, viper::*};
 
 pub enum Backend<'a> {
-    Viper(viper::Verifier<'a>, &'a VerificationContext<'a>),
+    Viper(
+        viper::Verifier<'a>,
+        &'a VerificationContext<'a>,
+        &'a Arc<Viper>,
+    ),
 }
 
 impl<'a> Backend<'a> {
-    pub fn verify(&mut self, program: vir::ProgramRef) -> VerificationResultKind {
+    pub fn verify(
+        &mut self,
+        program: vir::ProgramRef,
+        sender: mpsc::Sender<ServerMessage>,
+    ) -> VerificationResultKind {
         match self {
-            Backend::Viper(viper, context) => {
+            Backend::Viper(ref mut verifier, context, viper_arc) => {
                 let mut stopwatch =
                     Stopwatch::start("prusti-server backend", "construction of JVM objects");
 
@@ -36,9 +50,10 @@ impl<'a> Backend<'a> {
                     }
 
                     stopwatch.start_next("viper verification");
-                    viper.verify(viper_program)
+
+                    verifier.verify(viper_program)
                 })
             }
         }
     }
-}
+}