Achieve verification of very simple programs in Lithium

Author: JakuJ

Diff for: viper/src/lib.rs

@@ -5,6 +5,7 @@
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
 #![feature(try_blocks)]
+#![feature(let_chains)]
 #![deny(unused_must_use)]
 
 mod ast_factory;

Diff for: viper/src/native_backend/fol.rs

@@ -1,6 +1,5 @@
 use std::collections::HashMap;
 use vir::{
-    common::position::Positioned,
     low::{
         ast::{expression::*, statement::*},
         *,
@@ -11,16 +10,9 @@ pub enum FolStatement {
     Comment(String),
     Assume(Expression),
     Assert(Expression),
-    Sequence(Box<FolStatement>, Box<FolStatement>),
     Choice(Box<FolStatement>, Box<FolStatement>),
 }
 
-#[derive(Clone)]
-pub enum SMTGenTarget {
-    Predicate(Expression),
-    Comment(String),
-}
-
 fn vir_statement_to_fol_statements(
     statement: &Statement,
     known_methods: &HashMap<String, MethodDecl>,
@@ -140,59 +132,13 @@ fn vir_statement_to_fol_statements(
     }
 }
 
-pub fn vir_statements_to_predicates(
+pub fn vir_to_fol(
     statements: &Vec<Statement>,
     known_methods: &HashMap<String, MethodDecl>,
-) -> Vec<SMTGenTarget> {
+) -> Vec<FolStatement> {
     // reduce so that the order in the vector is now the Sequence operator
-    let sequence = statements
+    statements
         .iter()
         .flat_map(|s| vir_statement_to_fol_statements(s, known_methods))
-        .reduce(|a, b| FolStatement::Sequence(Box::new(a), Box::new(b)));
-
-    match sequence {
-        None => Vec::new(),
-        Some(seq) => fold_statement_to_formula_set(&seq, Vec::new()),
-    }
-}
-
-fn fold_statement_to_formula_set(
-    statement: &FolStatement,
-    set: Vec<SMTGenTarget>,
-) -> Vec<SMTGenTarget> {
-    match statement {
-        FolStatement::Comment(comment) => {
-            let mut set = set;
-            set.push(SMTGenTarget::Comment(comment.clone()));
-            set
-        }
-        FolStatement::Assert(expr) => {
-            let mut set = set;
-            set.push(SMTGenTarget::Predicate(expr.clone()));
-            set
-        }
-        FolStatement::Assume(expr) => set
-            .into_iter()
-            .map(|e| match e {
-                SMTGenTarget::Predicate(e) => {
-                    SMTGenTarget::Predicate(Expression::BinaryOp(BinaryOp {
-                        op_kind: BinaryOpKind::Implies,
-                        left: Box::new(expr.clone()),
-                        right: Box::new(e.clone()),
-                        position: e.position(),
-                    }))
-                }
-                x => x,
-            })
-            .collect(),
-        FolStatement::Sequence(fst, snd) => {
-            fold_statement_to_formula_set(fst, fold_statement_to_formula_set(snd, set))
-        }
-        FolStatement::Choice(fst, snd) => {
-            let mut fst_set = fold_statement_to_formula_set(fst, set.clone());
-            let snd_set = fold_statement_to_formula_set(snd, set);
-            fst_set.extend(snd_set);
-            fst_set
-        }
-    }
+        .collect()
 }

Diff for: viper/src/native_backend/native_verifier.rs

@@ -78,7 +78,11 @@ impl<'a> Verifier<'a> for NativeVerifier {
 
                 if output.status.success() {
                     let raw_output = String::from_utf8(output.stdout)?;
-                    raw_output
+                    if raw_output.lines().any(|line| line == "sat" || line == "unknown") {
+                        Err(raw_output)?
+                    } else {
+                        raw_output
+                    }
                 } else {
                     let err = String::from_utf8(output.stdout)?;
                     Err(err)?
@@ -100,11 +104,11 @@ impl<'a> Verifier<'a> for NativeVerifier {
         if is_failure {
             let mut errors: Vec<VerificationError> = vec![];
 
-            let error_full_id = "1".to_string();
+            let error_full_id = "verification.error".to_string();
             let pos_id = None;
             let offending_pos_id = None;
             let reason_pos_id = None;
-            let message = "Lithium backend not implemented".to_string();
+            let message = "At least one assertion was 'sat' or 'unknown'".to_string();
             let counterexample = None;
 
             errors.push(VerificationError::new(

Diff for: viper/src/native_backend/smt_lib.rs

@@ -1,9 +1,11 @@
-use super::theory_provider::*;
-use crate::native_backend::fol::*;
+use super::{
+    fol::{vir_to_fol, FolStatement},
+    theory_provider::*,
+};
 use lazy_static::lazy_static;
 use log::warn;
 use regex::Regex;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use vir::{
     common::position::Positioned,
     low::{
@@ -24,6 +26,7 @@ pub struct SMTLib {
     func_decls: Vec<String>,
     code: Vec<String>,
     methods: HashMap<String, MethodDecl>,
+    blocks: HashMap<String, BasicBlock>,
 }
 
 impl SMTLib {
@@ -33,6 +36,7 @@ impl SMTLib {
             func_decls: Vec::new(),
             code: Vec::new(),
             methods: HashMap::new(),
+            blocks: Default::default(),
         }
     }
     fn add_sort_decl(&mut self, sort_decl: String) {
@@ -48,8 +52,66 @@ impl SMTLib {
     fn add_code(&mut self, text: String) {
         self.code.push(text);
     }
-    fn add_code_lines(&mut self, texts: impl Iterator<Item = String>) {
-        self.code.extend(texts);
+    fn follow(&mut self, block_label: &String, precond: Option<&Expression>) {
+        let block = self
+            .blocks
+            .get(block_label)
+            .expect("Block not found")
+            .clone();
+
+        if block.statements.is_empty() {
+            return;
+        }
+
+        self.add_code(format!("; Basic block: {}", block.label));
+        self.add_code("(push)".to_string());
+
+        // assume precond if any
+        if let Some(precond) = precond {
+            self.add_code("; Branch precond:".to_string());
+            self.add_code(format!("(assert {})", precond.to_smt()));
+        }
+
+        // verify body
+        let predicates = vir_to_fol(&block.statements, &self.methods);
+
+        for predicate in predicates.into_iter() {
+            match predicate {
+                FolStatement::Comment(comment) => self.add_code(format!("; {}", comment)),
+                FolStatement::Assume(expression) => {
+                    // assert predicate
+                    self.add_code(format!("(assert {})", expression.to_smt()));
+                }
+                FolStatement::Assert(expression) => {
+                    // negate predicate
+                    let position = expression.position();
+                    let negated = Expression::UnaryOp(UnaryOp {
+                        op_kind: UnaryOpKind::Not,
+                        argument: Box::new(expression),
+                        position,
+                    });
+                    // assert negated predicate
+                    self.add_code("(push)".to_string());
+                    self.add_code(format!("(assert {})", negated.to_smt()));
+                    self.add_code("(check-sat)".to_string());
+                    self.add_code("(pop)".to_string());
+                }
+                FolStatement::Choice(_, _) => unimplemented!("Choice"),
+            }
+        }
+
+        // process successor
+        match &block.successor {
+            Successor::Goto(label) => {
+                self.follow(&label.name, None);
+            }
+            Successor::GotoSwitch(mapping) => mapping.iter().for_each(|(expr, label)| {
+                self.follow(&label.name, Some(expr));
+            }),
+            Successor::Return => {}
+        }
+
+        self.add_code(format!("(pop); End basic block: {}", block.label));
     }
 }
 
@@ -117,12 +179,19 @@ impl ToString for SMTLib {
         }
 
         result.push_str(&main);
+
+        // strip all lines containing "$marker"
+        // TODO: SSO form for marker variables?
         result
+            .lines()
+            .filter(|line| !line.contains("$marker"))
+            .collect::<Vec<_>>()
+            .join("\n")
     }
 }
 
 pub trait SMTTranslatable {
-    fn build_smt(&self, smt: &mut SMTLib) {
+    fn build_smt(&self, _: &mut SMTLib) {
         unimplemented!()
     }
     fn to_smt(&self) -> String {
@@ -230,7 +299,37 @@ impl SMTTranslatable for ProcedureDecl {
         self.locals.iter().for_each(|l| l.build_smt(smt));
 
         // process basic blocks
-        self.basic_blocks.iter().for_each(|b| b.build_smt(smt));
+        smt.blocks.clear();
+
+        self.basic_blocks.iter().for_each(|b| {
+            smt.blocks.insert(b.label.name.clone(), b.clone()); // TODO: Inefficient copy
+        });
+
+        // find a starting block
+        let mut start_blocks = smt.blocks.keys().collect::<HashSet<_>>();
+
+        for (_, block) in &smt.blocks {
+            match &block.successor {
+                Successor::Goto(label) => {
+                    start_blocks.remove(&label.name);
+                }
+                Successor::GotoSwitch(labels) => {
+                    labels.iter().for_each(|(_, l)| {
+                        start_blocks.remove(&l.name);
+                    });
+                }
+                Successor::Return => {}
+            }
+        }
+
+        assert!(
+            start_blocks.len() == 1,
+            "Expected exactly one start block, found {}",
+            start_blocks.len()
+        );
+
+        let start = start_blocks.drain().next().unwrap().clone();
+        smt.follow(&start, None);
 
         smt.add_code("(pop)".to_string());
     }
@@ -246,51 +345,6 @@ impl SMTTranslatable for VariableDecl {
     }
 }
 
-impl SMTTranslatable for BasicBlock {
-    fn build_smt(&self, smt: &mut SMTLib) {
-        if self.statements.is_empty() {
-            return;
-        }
-
-        let mut code = Vec::new();
-
-        code.push(format!("; Basic block: {}", self.label));
-        code.push("(push)".to_string());
-
-        // verify body
-        let predicates = vir_statements_to_predicates(&self.statements, &smt.methods);
-
-        let mut assertions = 0;
-        for predicate in predicates.into_iter() {
-            match predicate {
-                SMTGenTarget::Predicate(expression) => {
-                    // negate predicate
-                    let position = expression.position();
-                    let negated = Expression::UnaryOp(UnaryOp {
-                        op_kind: UnaryOpKind::Not,
-                        argument: Box::new(expression),
-                        position,
-                    });
-                    // assert negated predicate
-                    code.push(format!("(assert {})", negated.to_smt()));
-                    assertions += 1;
-                }
-                SMTGenTarget::Comment(comment) => code.push(format!("; {}", comment)),
-            }
-        }
-
-        // check if the negated predicates are satisfiable
-        // TODO: each in its own scope?
-        if assertions > 0 {
-            code.push("(check-sat)".to_string());
-            code.push("(pop)".to_string());
-            smt.add_code_lines(code.into_iter());
-        }
-
-        // TODO: Goto
-    }
-}
-
 /* #endregion */
 
 impl SMTTranslatable for Expression {