Ugly commit 30.01

.devcontainer/devcontainer.json

@@ -52,7 +52,6 @@
 
   // See https://containers.dev/features for a list of all available features
   "features": {
-    "fish": "latest",
     "java": "17",
     "python": "latest"
   },

prusti-utils/src/config.rs

@@ -200,6 +200,10 @@ lazy_static::lazy_static! {
         settings.set_default::<Vec<String>>("verify_only_basic_block_path", vec![]).unwrap();
         settings.set_default::<Vec<String>>("delete_basic_blocks", vec![]).unwrap();
 
+        // Svirpti settings.
+        settings.set_default("svirpti_smt_solver", "z3").unwrap();
+        settings.set_default::<Option<String>>("svirpti_smt_solver_log", None).unwrap();
+
         // Get the list of all allowed flags.
         let mut allowed_keys = get_keys(&settings);
         allowed_keys.insert("server_max_stored_verifiers".to_string());
@@ -1286,6 +1290,16 @@ pub fn delete_basic_blocks() -> Vec<String> {
     read_setting("delete_basic_blocks")
 }
 
+/// The path to the SMT solver to be used by Svirpti.
+pub fn svirpti_smt_solver() -> String {
+    read_setting("svirpti_smt_solver")
+}
+
+/// The path to the log file in which Svirpti should log all communications with the SMT solver.
+pub fn svirpti_smt_solver_log() -> Option<String> {
+    read_setting("svirpti_smt_solver_log")
+}
+
 /// When enabled, features not supported by Prusti will be reported as warnings
 /// rather than errors.
 pub fn skip_unsupported_features() -> bool {

prusti-viper/Cargo.toml

@@ -31,6 +31,7 @@ itertools = "0.10.3"
 once_cell = "1.17.1"
 egg = { git = "https://github.com/vakaras/egg.git", branch = "from_enodes_with_explanations" }
 ena = { version = "0.14.2", features = ["persistent"] }
+rsmt2 = "0.16.2"
 
 [dev-dependencies]
 lazy_static = "1.4"

prusti-viper/src/encoder/encoder.rs

@@ -258,8 +258,8 @@ impl<'v, 'tcx> Encoder<'v, 'tcx> {
         }
     }
 
-    pub fn verify_core_programs(&mut self) -> prusti_interface::data::VerificationResult {
-        crate::encoder::middle::svirpti::verify_core_programs(self)
+    pub fn verify_core_proof_programs(&mut self) -> prusti_interface::data::VerificationResult {
+        crate::encoder::middle::svirpti::verify_core_proof_programs(self)
     }
 
     #[tracing::instrument(level = "debug", skip(self))]

prusti-viper/src/encoder/middle/mod.rs

@@ -1,2 +1,2 @@
 pub(crate) mod core_proof;
-pub(crate) mod svirpti;
+pub(crate) mod svirpti;

prusti-viper/src/encoder/middle/svirpti/mod.rs

@@ -1,5 +1,28 @@
 use crate::encoder::Encoder;
+use prusti_common::vir::program::Program;
+use vir_crate::low as vir_low;
 
-pub(crate) fn verify_core_programs(encoder: &mut Encoder) -> prusti_interface::data::VerificationResult {
+mod smt;
+
+pub(crate) fn verify_core_proof_programs(
+    encoder: &mut Encoder,
+) -> prusti_interface::data::VerificationResult {
+    let programs = encoder.get_core_proof_programs();
+    for program in programs {
+        let Program::Low(program) = program else {
+            unimplemented!("TODO: A proper error message here.");
+        };
+        let result = verify_program(encoder, program);
+        unimplemented!();
+    }
+    unimplemented!();
+}
+
+struct VerificationResult {}
+
+fn verify_program(encoder: &mut Encoder, program: vir_low::Program) -> VerificationResult {
+    let mut smt_solver = smt::SmtSolver::default().unwrap();
+    let result = smt_solver.check_sat().unwrap();
+    assert!(result.is_sat());
     unimplemented!();
-}
+}

prusti-viper/src/verifier.rs

@@ -79,7 +79,7 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> {
         let polymorphic_programs = self.encoder.get_viper_programs();
 
         if config::viper_backend() == "svirpti" {
-            return self.encoder.verify_core_programs();
+            return self.encoder.verify_core_proof_programs();
         }
 
         let mut programs: Vec<Program> = if config::simplify_encoding() {