Merge remote-tracking branch 'upstream/master' into iterators-feature…

…-flag

.github/workflows/test.yml

@@ -155,6 +155,46 @@ jobs:
           # python x.py test --all --verbose pass/pure-fn/ref-mut-arg.rs
           # python x.py test --all --verbose pass/rosetta/Ackermann_function.rs
           # python x.py test --all --verbose pass/rosetta/Heapsort.rs
+      - name: Run with purification.
+        env:
+          PRUSTI_VIPER_BACKEND: silicon
+          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
+          PRUSTI_VERIFY_CORE_PROOF: true
+          PRUSTI_VERIFY_SPECIFICATIONS: true
+          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
+          PRUSTI_INLINE_CALLER_FOR: false
+        run: |
+          python x.py test core_proof
+      - name: Run with purification with Carbon.
+        env:
+          PRUSTI_VIPER_BACKEND: silicon
+          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: carbon
+          PRUSTI_VERIFY_CORE_PROOF: true
+          PRUSTI_VERIFY_SPECIFICATIONS: true
+          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
+          PRUSTI_INLINE_CALLER_FOR: false
+        run: |
+          python x.py test core_proof
+      - name: Run without purification.
+        env:
+          PRUSTI_VIPER_BACKEND: silicon
+          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
+          PRUSTI_VERIFY_CORE_PROOF: true
+          PRUSTI_VERIFY_SPECIFICATIONS: true
+          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: true
+          PRUSTI_INLINE_CALLER_FOR: false
+        run: |
+          python x.py test core_proof
+      - name: Inline caller for functions
+        env:
+          PRUSTI_VIPER_BACKEND: silicon
+          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
+          PRUSTI_VERIFY_CORE_PROOF: true
+          PRUSTI_VERIFY_SPECIFICATIONS: true
+          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
+          PRUSTI_INLINE_CALLER_FOR: true
+        run: |
+          python x.py test core_proof
 
   # Run all the tests.
   all-tests:

analysis/src/mir_utils.rs

@@ -195,47 +195,34 @@ pub fn expand_struct_place<'tcx, P: PlaceImpl<'tcx> + std::marker::Copy>(
 /// Expand `current_place` one level down by following the `guide_place`.
 /// Returns the new `current_place` and a vector containing other places that
 /// could have resulted from the expansion.
-pub(crate) fn expand_one_level<'tcx>(
+pub fn expand_one_level<'tcx>(
     mir: &mir::Body<'tcx>,
     tcx: TyCtxt<'tcx>,
     current_place: Place<'tcx>,
     guide_place: Place<'tcx>,
 ) -> (Place<'tcx>, Vec<Place<'tcx>>) {
     let index = current_place.projection.len();
-    match guide_place.projection[index] {
-        mir::ProjectionElem::Field(projected_field, field_ty) => {
-            let places =
-                expand_struct_place(current_place, mir, tcx, Some(projected_field.index()));
-            let new_current_place = tcx
-                .mk_place_field(*current_place, projected_field, field_ty)
-                .into();
-            debug_assert!(
-                !places.contains(&new_current_place),
-                "{:?} unexpectedly contains {:?}",
-                places,
-                new_current_place
-            );
-            (new_current_place, places)
-        }
-        mir::ProjectionElem::Downcast(_symbol, variant) => {
-            let kind = &current_place.ty(mir, tcx).ty.kind();
-            if let ty::TyKind::Adt(adt, _) = kind {
-                (
-                    tcx.mk_place_downcast(*current_place, *adt, variant).into(),
-                    Vec::new(),
-                )
-            } else {
-                unreachable!();
-            }
-        }
-        mir::ProjectionElem::Deref => (tcx.mk_place_deref(*current_place).into(), Vec::new()),
-        mir::ProjectionElem::Index(idx) => {
-            (tcx.mk_place_index(*current_place, idx).into(), Vec::new())
-        }
-        elem => {
-            unimplemented!("elem = {:?}", elem);
+    let new_projection = tcx.mk_place_elems(
+        current_place
+            .projection
+            .iter()
+            .chain([guide_place.projection[index]]),
+    );
+    let new_current_place = Place(mir::Place {
+        local: current_place.local,
+        projection: new_projection,
+    });
+    let other_places = match guide_place.projection[index] {
+        mir::ProjectionElem::Field(projected_field, _field_ty) => {
+            expand_struct_place(current_place, mir, tcx, Some(projected_field.index()))
         }
-    }
+        mir::ProjectionElem::Deref
+        | mir::ProjectionElem::Index(..)
+        | mir::ProjectionElem::ConstantIndex { .. }
+        | mir::ProjectionElem::Subslice { .. }
+        | mir::ProjectionElem::Downcast(..) => vec![],
+    };
+    (new_current_place, other_places)
 }
 
 /// Subtract the `subtrahend` place from the `minuend` place. The

docs/dev-guide/src/config/flags.md

@@ -46,7 +46,6 @@
 | [`MAX_LOG_FILE_NAME_LENGTH`](#max_log_file_name_length) | `usize` | `60` |
 | [`NO_VERIFY`](#no_verify) | `bool` | `false` |
 | [`NO_VERIFY_DEPS`](#no_verify_deps) | `bool` | `false` |
-| [`ONLY_MEMORY_SAFETY`](#only_memory_safety) | `bool` | `false` |
 | [`OPTIMIZATIONS`](#optimizations) | `Vec<String>` | "all" |
 | [`PRESERVE_SMT_TRACE_FILES`](#preserve_smt_trace_files) | `bool` | `false` |
 | [`PRINT_COLLECTED_VERIFICATION_ITEMS`](#print_collected_verification_items) | `bool` | `false` |

prusti-common/src/config.rs

@@ -113,7 +113,11 @@ lazy_static::lazy_static! {
         settings.set_default("enable_purification_optimization", false).unwrap();
         // settings.set_default("enable_manual_axiomatization", false).unwrap();
         settings.set_default("unsafe_core_proof", false).unwrap();
-        settings.set_default("only_memory_safety", false).unwrap();
+        settings.set_default("verify_core_proof", true).unwrap();
+        settings.set_default("verify_specifications", true).unwrap();
+        settings.set_default("verify_specifications_with_core_proof", false).unwrap();
+        settings.set_default("verify_specifications_backend", "Silicon").unwrap();
+        settings.set_default("inline_caller_for", false).unwrap();
         settings.set_default("check_no_drops", false).unwrap();
         settings.set_default("enable_type_invariants", false).unwrap();
         settings.set_default("use_new_encoder", true).unwrap();
@@ -274,11 +278,12 @@ pub fn check_foldunfold_state() -> bool {
 ///   [Carbon](https://github.com/viperproject/carbon).
 /// - `Silicon` - symbolic-execution-based backend
 ///   [Silicon](https://github.com/viperproject/silicon/).
-pub fn viper_backend() -> String {
-    read_setting::<String>("viper_backend")
+pub fn viper_backend() -> viper::VerificationBackend {
+    let verification_backend_name = read_setting::<String>("viper_backend")
         .to_lowercase()
         .trim()
-        .to_string()
+        .to_string();
+    <viper::VerificationBackend as std::str::FromStr>::from_str(&verification_backend_name).unwrap()
 }
 
 /// The path to the SMT solver to use. `prusti-rustc` is expected to set this
@@ -756,20 +761,52 @@ pub fn unsafe_core_proof() -> bool {
     read_setting("unsafe_core_proof")
 }
 
+/// Whether the core proof (memory safety) should be verified.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` to
+/// be true.
+pub fn verify_core_proof() -> bool {
+    read_setting("verify_core_proof")
+}
+
+/// Whether the functional specifications should be verified.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` to
+/// be true.
+pub fn verify_specifications() -> bool {
+    read_setting("verify_specifications")
+}
+
+/// Whether when verifying functional specifications, the core proof should be
+/// also included.
+///
+/// **Note:** This option is taken into account only when `unsafe_core_proof` to
+/// be true.
+pub fn verify_specifications_with_core_proof() -> bool {
+    read_setting("verify_specifications_with_core_proof")
+}
+
+/// Verification backend to use for functional specification only.
+pub fn verify_specifications_backend() -> viper::VerificationBackend {
+    let verification_backend_name = read_setting::<String>("verify_specifications_backend")
+        .to_lowercase()
+        .trim()
+        .to_string();
+    <viper::VerificationBackend as std::str::FromStr>::from_str(&verification_backend_name).unwrap()
+}
+
+/// When enabled, inlines `caller_for` heap dependent functions.
+pub fn inline_caller_for() -> bool {
+    read_setting("inline_caller_for")
+}
+
 /// When enabled, replaces calls to the drop function with `assert false`.
 ///
 /// **Note:** This option is used only for testing.
 pub fn check_no_drops() -> bool {
     read_setting("check_no_drops")
 }
 
-/// When enabled, only the core proof is verified.
-///
-/// **Note:** This should be used only when `UNSAFE_CORE_PROOF` is enabled.
-pub fn only_memory_safety() -> bool {
-    read_setting("only_memory_safety")
-}
-
 /// When enabled, Prusti uses the new VIR encoder.
 ///
 /// This is a temporary configuration flag.

prusti-common/src/vir/low_to_viper/program.rs

@@ -6,6 +6,7 @@ impl<'v> ToViper<'v, viper::Program<'v>> for Program {
     fn to_viper(&self, context: Context, ast: &AstFactory<'v>) -> viper::Program<'v> {
         let Program {
             name: _,
+            check_mode: _,
             domains,
             procedures,
             predicates,

prusti-common/src/vir/program.rs

@@ -20,6 +20,15 @@ impl Program {
             Program::Low(program) => program.name = name,
         }
     }
+    pub fn get_check_mode(&self) -> vir::common::check_mode::CheckMode {
+        match self {
+            Program::Legacy(_) => vir::common::check_mode::CheckMode::Both,
+            Program::Low(program) => program.check_mode,
+        }
+    }
+    pub fn get_name_with_check_mode(&self) -> String {
+        format!("{}-{}", self.get_name(), self.get_check_mode())
+    }
 }
 
 impl<'v> ToViper<'v, viper::Program<'v>> for Program {

prusti-interface/src/environment/mod.rs

@@ -16,6 +16,7 @@ use prusti_rustc_interface::middle::ty::TypeSuperFoldable;
 use std::path::PathBuf;
 use prusti_rustc_interface::errors::{DiagnosticBuilder, EmissionGuarantee, MultiSpan};
 use prusti_rustc_interface::span::{Span, symbol::Symbol};
+use prusti_common::config;
 use std::collections::HashSet;
 use log::{debug, trace};
 use std::rc::Rc;
@@ -383,6 +384,11 @@ impl<'tcx> Environment<'tcx> {
             .is_some()
     }
 
+    /// Returns true iff `def_id` is an unsafe function.
+    pub fn is_unsafe_function(&self, def_id: ProcedureDefId) -> bool {
+        self.tcx.fn_sig(def_id).unsafety() == prusti_rustc_interface::hir::Unsafety::Unsafe
+    }
+
     /// Returns the `DefId` of the corresponding trait method, if any.
     /// This should not be used to resolve calls (where substs are known): use
     /// `find_trait_method_substs` instead!

prusti-interface/src/utils.rs

@@ -14,8 +14,6 @@ use prusti_rustc_interface::middle::{
     mir,
     ty::{self, TyCtxt},
 };
-use analysis::mir_utils::expand_struct_place;
-use prusti_utils::force_matches;
 
 /// Check if the place `potential_prefix` is a prefix of `place`. For example:
 ///
@@ -45,26 +43,9 @@ pub fn expand_one_level<'tcx>(
     current_place: mir::Place<'tcx>,
     guide_place: mir::Place<'tcx>,
 ) -> (mir::Place<'tcx>, Vec<mir::Place<'tcx>>) {
-    let index = current_place.projection.len();
-    match guide_place.projection[index] {
-        mir::ProjectionElem::Field(projected_field, field_ty) => {
-            let places =
-                expand_struct_place(current_place, mir, tcx, Some(projected_field.index()));
-            let new_current_place = tcx.mk_place_field(current_place, projected_field, field_ty);
-            (new_current_place, places)
-        }
-        mir::ProjectionElem::Downcast(_symbol, variant) => {
-            let kind = &current_place.ty(mir, tcx).ty.kind();
-            force_matches!(kind, ty::TyKind::Adt(adt, _) =>
-                (tcx.mk_place_downcast(current_place, *adt, variant), Vec::new())
-            )
-        }
-        mir::ProjectionElem::Deref => (tcx.mk_place_deref(current_place), Vec::new()),
-        mir::ProjectionElem::Index(idx) => (tcx.mk_place_index(current_place, idx), Vec::new()),
-        elem => {
-            unimplemented!("elem = {:?}", elem);
-        }
-    }
+    use analysis::mir_utils::{expand_one_level, PlaceImpl};
+    let res = expand_one_level(mir, tcx, current_place.into(), guide_place.into());
+    (res.0.to_mir_place(), res.1.into_iter().map(PlaceImpl::to_mir_place).collect())
 }
 
 /// Pop the last projection from the place and return the new place with the popped element.

prusti-server/src/process_verification.rs

@@ -40,7 +40,11 @@ pub fn process_verification_request<'v, 't: 'v>(
 
         if config::dump_viper_program() {
             stopwatch.start_next("dumping viper program");
-            dump_viper_program(&ast_utils, viper_program, request.program.get_name());
+            dump_viper_program(
+                &ast_utils,
+                viper_program,
+                &request.program.get_name_with_check_mode(),
+            );
         }
 
         viper_program

prusti-server/src/verification_request.rs

@@ -8,7 +8,6 @@ use prusti_common::{config, vir::program::Program};
 use std::{
     collections::hash_map::DefaultHasher,
     hash::{Hash, Hasher},
-    str::FromStr,
 };
 use viper::{self, VerificationBackend};
 
@@ -35,9 +34,8 @@ pub struct ViperBackendConfig {
     pub verifier_args: Vec<String>,
 }
 
-impl Default for ViperBackendConfig {
-    fn default() -> Self {
-        let backend = VerificationBackend::from_str(&config::viper_backend()).unwrap();
+impl ViperBackendConfig {
+    pub fn new(backend: VerificationBackend) -> Self {
         let mut verifier_args = config::extra_verifier_args();
         match backend {
             VerificationBackend::Silicon => {

prusti-server/tests/basic_requests.rs

@@ -2,6 +2,7 @@ use lazy_static::lazy_static;
 use prusti_common::vir::*;
 use prusti_server::{
     spawn_server_thread, tokio::runtime::Builder, PrustiClient, VerificationRequest,
+    ViperBackendConfig,
 };
 use viper::VerificationResult;
 
@@ -60,7 +61,7 @@ where
 
     let request = VerificationRequest {
         program: prusti_common::vir::program::Program::Legacy(program),
-        backend_config: Default::default(),
+        backend_config: ViperBackendConfig::new(prusti_common::config::viper_backend()),
     };
 
     Builder::new_current_thread()