Update dependencies (rustc nightly-2022-05-01, viper v.22.04.17-relea…

…se) (#990) * [x] Update Viper version to `v.22.04.17-release`. * [x] Update rustc version to `nightly-2022-05-01`. * [x] Manualy update outdated dependencies (see the list below). * [x] Manualy run `cargo update`. <details><summary>List of direct outdated dependencies:</summary> ``` $ cargo outdated --root-deps-only --workspace info: syncing channel updates for 'nightly-2022-05-01-x86_64-unknown-linux-gnu' info: latest update on 2022-05-01, rust version 1.62.0-nightly (7c4b47696 2022-04-30) info: downloading component 'cargo' info: downloading component 'llvm-tools-preview' info: downloading component 'rust-std' info: downloading component 'rustc' info: downloading component 'rustc-dev' info: downloading component 'rustfmt' info: installing component 'cargo' info: installing component 'llvm-tools-preview' info: installing component 'rust-std' info: installing component 'rustc' info: installing component 'rustc-dev' info: installing component 'rustfmt' Updating git repository `https://github.com/rust-lang/cargo.git` analysis ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.136 --- 1.0.137 Normal --- serde_json 1.0.79 --- 1.0.80 Normal --- syn 1.0.91 --- 1.0.92 Normal --- prusti-common ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.136 --- 1.0.137 Normal --- uuid 0.8.2 --- 1.0.0 Normal --- viper ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.136 --- 1.0.137 Normal --- uuid 0.8.2 --- 1.0.0 Normal --- vir ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.136 --- 1.0.137 Normal --- syn 1.0.91 --- 1.0.92 Normal --- thiserror 1.0.30 --- 1.0.31 Normal --- uuid 0.8.2 --- 1.0.0 Normal --- vir-gen ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- syn 1.0.91 --- 1.0.92 Normal --- prusti-contracts ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- trybuild 1.0.59 --- 1.0.61 Development --- prusti-specs ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.136 --- 1.0.137 Normal --- serde_json 1.0.79 --- 1.0.80 Normal --- syn 1.0.91 --- 1.0.92 Normal --- uuid 0.8.2 --- 1.0.0 Normal --- prusti-interface ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- serde 1.0.136 --- 1.0.137 Normal --- prusti-viper ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- backtrace 0.3.64 --- 0.3.65 Normal --- serde 1.0.136 --- 1.0.137 Normal --- prusti-server ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- clap 3.1.8 --- 3.1.14 Normal --- reqwest 0.10.10 --- 0.11.10 Normal --- serde 1.0.136 --- 1.0.137 Normal --- tokio 0.2.25 --- 1.18.0 Normal --- warp 0.2.5 --- 0.3.2 Normal --- prusti-launch ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- ctrlc 3.2.1 --- 3.2.2 Normal --- nix 0.23.1 --- 0.24.1 Normal cfg(unix) serde 1.0.136 --- 1.0.137 Normal --- test-crates ================ Name Project Compat Latest Kind Platform ---- ------- ------ ------ ---- -------- clap 3.1.8 --- 3.1.14 Normal --- serde 1.0.136 --- 1.0.137 Normal --- ``` </details> @JonasAlaif could you take care of this? Co-authored-by: Jonas <[email protected]>
viperproject · May 17, 2022 · 70eda1c · 70eda1c
1 parent 7a5c782
commit 70eda1c
Show file tree

Hide file tree

Showing 20 changed files with 382 additions and 543 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/prusti-common/Cargo.toml b/prusti-common/Cargo.toml
@@ -15,7 +15,7 @@ config = "0.13"
 itertools = "0.10.3"
 serde = { version = "1.0", features = ["derive"] }
 lazy_static = "1.4.0"
-uuid = { version = "0.8", features = ["v4"] }
+uuid = { version = "1.0", features = ["v4"] }
 regex = "1.5"
 prusti-utils = { path = "../prusti-utils" }
 fxhash = "0.2.1"
diff --git a/prusti-launch/Cargo.toml b/prusti-launch/Cargo.toml
@@ -31,7 +31,7 @@ toml = "0.5"
 ctrlc = "3.1"
 
 [target.'cfg(unix)'.dependencies]
-nix = "0.23"
+nix = "0.24"
 
 [dev-dependencies]
 glob = "0.3"
diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml
@@ -26,12 +26,9 @@ bincode = "1.0"
 url = "2.2.2"
 num_cpus = "1.8.0"
 serde = { version = "1.0", features = ["derive"] }
-# More recent verions of reqwest and warp fail to compile
-# due to https://github.com/rust-lang/rust/issues/82151
-reqwest = { version = "0.10", features = ["json"] }
-warp = "0.2"
-# warp 0.2.x only works with tokio 0.2.x
-tokio = "0.2"
+reqwest = { version = "0.11", features = ["json"] }
+warp = "0.3"
+tokio = "1.18"
 
 [dev-dependencies]
 lazy_static = "1.4.0"
diff --git a/prusti-server/src/server.rs b/prusti-server/src/server.rs
@@ -101,8 +101,7 @@ where
     // Here we use a single thread because
     // 1. Viper is not thread safe yet (Silicon issue #578), and
     // 2. By default Silicon already uses as many cores as possible.
-    let mut runtime = Builder::new()
-        .basic_scheduler()
+    let runtime = Builder::new_current_thread()
         .thread_name("prusti-server")
         .enable_all()
         .build()

diff --git a/prusti-server/tests/basic_requests.rs b/prusti-server/tests/basic_requests.rs
@@ -63,8 +63,7 @@ where
         backend_config: Default::default(),
     };
 
-    Builder::new()
-        .basic_scheduler()
+    Builder::new_current_thread()
         .enable_all()
         .build()
         .expect("failed to construct Tokio runtime")

diff --git a/prusti-specs/Cargo.toml b/prusti-specs/Cargo.toml
@@ -11,7 +11,7 @@ doctest = false # we have no doc tests
 syn = { version = "1.0", features = ["full", "extra-traits", "visit-mut", "parsing", "printing"] }
 quote = "1.0"
 proc-macro2 = "1.0"
-uuid = { version = "0.8", features = ["v4", "serde"] }
+uuid = { version = "1.0", features = ["v4", "serde"] }
 serde_json = "1.0"
 serde = { version = "1.0", features = ["derive"] }
 prusti-utils = { path = "../prusti-utils" }
diff --git a/prusti-specs/src/common.rs b/prusti-specs/src/common.rs
@@ -407,7 +407,7 @@ pub(crate) fn add_phantom_data_for_generic_params(item_struct: &mut syn::ItemStr
 
     let generate_field_ident = |span: proc_macro2::Span| {
         if need_named_fields {
-            let uuid = Uuid::new_v4().to_simple();
+            let uuid = Uuid::new_v4().simple();
             let field_name = format!("prusti_injected_phantom_field_{}", uuid);
             return Some(syn::Ident::new(field_name.as_str(), span));
         }

diff --git a/prusti-specs/src/specifications/common.rs b/prusti-specs/src/specifications/common.rs
@@ -67,7 +67,7 @@ impl Display for SpecificationId {
         write!(
             f,
             "{}",
-            self.0.to_simple().encode_lower(&mut Uuid::encode_buffer()),
+            self.0.simple().encode_lower(&mut Uuid::encode_buffer()),
         )
     }
 }
@@ -97,18 +97,18 @@ impl SpecificationIdGenerator {
 }
 
 pub(crate) fn generate_struct_name(item: &syn::ItemImpl) -> String {
-    let uuid = Uuid::new_v4().to_simple();
+    let uuid = Uuid::new_v4().simple();
     let name_ty = generate_name_for_type(&*item.self_ty).unwrap_or_default();
     format!("PrustiStruct{}_{}", name_ty, uuid)
 }
 
 pub(crate) fn generate_struct_name_for_trait(item: &syn::ItemTrait) -> String {
-    let uuid = Uuid::new_v4().to_simple();
+    let uuid = Uuid::new_v4().simple();
     format!("PrustiTrait{}_{}", item.ident, uuid)
 }
 
 pub(crate) fn generate_mod_name(ident: &syn::Ident) -> String {
-    let uuid = Uuid::new_v4().to_simple();
+    let uuid = Uuid::new_v4().simple();
     format!("{}_{}", ident, uuid)
 }
 

diff --git a/prusti-specs/src/type_model/mod.rs b/prusti-specs/src/type_model/mod.rs
@@ -216,7 +216,7 @@ impl GeneratedIdents {
             }
         }
 
-        let uuid = Uuid::new_v4().to_simple();
+        let uuid = Uuid::new_v4().simple();
 
         GeneratedIdents {
             model_struct_ident: Ident::new(

diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs
@@ -217,14 +217,14 @@ impl<'tcx> ErrorManager<'tcx> {
     }
 
     pub fn get_def_id(&self, ver_error: &VerificationError) -> Option<ProcedureDefId> {
-        ver_error.pos_id.as_ref()
+        ver_error.offending_pos_id.as_ref()
             .and_then(|id| id.parse().ok())
             .and_then(|id| self.position_manager.def_id.get(&id).copied())
     }
 
     pub fn translate_verification_error(&self, ver_error: &VerificationError) -> PrustiError {
         debug!("Verification error: {:?}", ver_error);
-        let opt_pos_id: Option<u64> = match ver_error.pos_id {
+        let opt_pos_id: Option<u64> = match ver_error.offending_pos_id {
             Some(ref viper_pos_id) => {
                 match viper_pos_id.parse() {
                     Ok(pos_id) => Some(pos_id),

diff --git a/prusti-viper/src/verifier.rs b/prusti-viper/src/verifier.rs
@@ -397,8 +397,7 @@ fn verify_programs(env: &Environment, programs: Vec<Program>)
         // Here we construct a Tokio runtime to block until completion of the futures returned by
         // `client.verify`. However, to report verification errors as early as possible,
         // `verify_programs` should return an asynchronous stream of verification results.
-        let mut runtime = Builder::new()
-            .basic_scheduler()
+        let runtime = Builder::new_current_thread()
             .thread_name("prusti-viper")
             .enable_all()
             .build()

diff --git a/rust-toolchain b/rust-toolchain
@@ -1,4 +1,4 @@
 [toolchain]
-channel = "nightly-2022-04-15"
+channel = "nightly-2022-05-01"
 components = [ "rustc-dev", "llvm-tools-preview", "rust-std", "rustfmt" ]
 profile = "minimal"
diff --git a/viper-sys/build.rs b/viper-sys/build.rs
@@ -577,6 +577,9 @@ fn main() {
             java_class!("viper.silver.ast.PermDiv", vec![
                 constructor!(),
             ]),
+            java_class!("viper.silver.ast.Positioned", vec![
+                method!("pos"),
+            ]),
             java_class!("viper.silver.ast.Predicate", vec![
                 constructor!(),
             ]),
@@ -712,6 +715,7 @@ fn main() {
             ]),
             java_class!("viper.silver.verifier.VerificationError", vec![
                 method!("id"),
+                method!("offendingNode"),
                 method!("pos"),
                 method!("fullId"),
                 method!("reason"),

diff --git a/viper-toolchain b/viper-toolchain
@@ -1 +1 @@
-v-2022-02-14-1454
+v.22.04.17-release
diff --git a/viper/Cargo.toml b/viper/Cargo.toml
@@ -11,7 +11,7 @@ log = { version = "0.4", features = ["release_max_level_info"] }
 error-chain = "0.12"
 viper-sys = { path = "../viper-sys" }
 jni = { version = "0.19", features = ["invocation"] }
-uuid = { version = "0.8", features = ["v4"] }
+uuid = { version = "1.0", features = ["v4"] }
 serde = { version = "1.0", features = ["derive"] }
 bincode = "1.3.3"
 rustc-hash = "1.1.0"

diff --git a/viper/src/verification_result.rs b/viper/src/verification_result.rs
@@ -30,7 +30,11 @@ impl VerificationResult {
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
 pub struct VerificationError {
     pub full_id: String,
+    // Unused since we get pos from the offending_node instead.
+    // Currently calling pos on e.g. `ExhaleFailed` of Silver returns
+    // the exhale expression pos, rather than the Exhale node pos.
     pub pos_id: Option<String>,
+    pub offending_pos_id: Option<String>,
     pub reason_pos_id: Option<String>,
     pub message: String,
     pub counterexample: Option<SiliconCounterexample>,
@@ -40,13 +44,15 @@ impl VerificationError {
     pub fn new(
         full_id: String,
         pos_id: Option<String>,
+        offending_pos_id: Option<String>,
         reason_pos_id: Option<String>,
         message: String,
         counterexample: Option<SiliconCounterexample>,
     ) -> Self {
         VerificationError {
             full_id,
             pos_id,
+            offending_pos_id,
             reason_pos_id,
             message,
             counterexample,

diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs
@@ -149,6 +149,8 @@ impl<'a> Verifier<'a> {
 
                 let verification_error_wrapper = silver::verifier::VerificationError::with(self.env);
 
+                let error_node_positioned_wrapper = silver::ast::Positioned::with(self.env);
+
                 let failure_context_wrapper = silver::verifier::FailureContext::with(self.env);
 
                 let has_identifier_wrapper = silver::ast::HasIdentifier::with(self.env);
@@ -282,9 +284,34 @@ impl<'a> Verifier<'a> {
                             None
                         };
 
+                    let offending_node = self
+                        .jni
+                        .unwrap_result(verification_error_wrapper.call_offendingNode(viper_error));
+
+                    let offending_pos = self
+                        .jni
+                        .unwrap_result(error_node_positioned_wrapper.call_pos(offending_node));
+
+                    let offending_pos_id =
+                        if self
+                            .jni
+                            .is_instance_of(offending_pos, "viper/silver/ast/HasIdentifier")
+                        {
+                            Some(self.jni.get_string(
+                                self.jni.unwrap_result(has_identifier_wrapper.call_id(offending_pos)),
+                            ))
+                        } else {
+                            debug!(
+                                "The verifier returned an error whose position has no identifier: {:?}",
+                                self.jni.to_string(viper_error)
+                            );
+                            None
+                        };
+
                     errors.push(VerificationError::new(
                         error_full_id,
                         pos_id,
+                        offending_pos_id,
                         reason_pos_id,
                         message,
                         counterexample,

diff --git a/viper/tests/simple_programs.rs b/viper/tests/simple_programs.rs
@@ -66,7 +66,7 @@ fn failure_with_assert_false() {
             errors[0].full_id,
             "assert.failed:assertion.false".to_string()
         );
-        assert_eq!(errors[0].pos_id, Some("pos-id:123".to_string()));
+        assert_eq!(errors[0].offending_pos_id, Some("pos-id:123".to_string()));
     } else {
         unreachable!()
     }
@@ -210,7 +210,7 @@ fn failure_with_assign_if_and_assert() {
             errors[0].full_id,
             "assert.failed:assertion.false".to_string()
         );
-        assert_eq!(errors[0].pos_id, Some("then".to_string()));
+        assert_eq!(errors[0].offending_pos_id, Some("then".to_string()));
     } else {
         unreachable!()
     }

diff --git a/vir/Cargo.toml b/vir/Cargo.toml
@@ -13,7 +13,7 @@ regex = "1.5"
 syn = { version = "1.0", features = ["full", "fold", "parsing", "derive"] }
 quote = "1.0"
 proc-macro2 = { version = "1.0", features = ["span-locations"] }
-uuid = { version = "0.8", features = ["v4"] }
+uuid = { version = "1.0", features = ["v4"] }
 log = { version = "0.4", features = ["release_max_level_info"] }
 lazy_static = "1.4.0"
 itertools = "0.10.3"