diff --git a/.gitignore b/.gitignore index 55f21d7cb51..514fb3305de 100644 --- a/.gitignore +++ b/.gitignore @@ -10,6 +10,7 @@ callgrind.* core report.csv *.profraw +.DS_Store *.lock !/Cargo.lock diff --git a/Cargo.lock b/Cargo.lock index e070c4b73aa..ca5672dbb26 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -291,6 +291,15 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" +[[package]] +name = "backend-common" +version = "0.1.0" +dependencies = [ + "rustc-hash", + "serde", + "vir", +] + [[package]] name = "backtrace" version = "0.3.69" @@ -1900,6 +1909,22 @@ dependencies = [ "tempfile", ] +[[package]] +name = "native-verifier" +version = "0.1.0" +dependencies = [ + "backend-common", + "error-chain", + "lazy_static", + "log", + "prusti-common", + "prusti-utils", + "regex", + "serde", + "uuid", + "vir", +] + [[package]] name = "nix" version = "0.25.1" @@ -2279,6 +2304,7 @@ dependencies = [ name = "prusti-common" version = "0.1.0" dependencies = [ + "backend-common", "config", "itertools 0.11.0", "lazy_static", @@ -2338,11 +2364,13 @@ version = "0.1.0" name = "prusti-server" version = "0.1.0" dependencies = [ + "backend-common", "bincode", "clap", "env_logger", "lazy_static", "log", + "native-verifier", "num_cpus", "once_cell", "prusti-common", @@ -2413,6 +2441,7 @@ dependencies = [ name = "prusti-viper" version = "0.1.0" dependencies = [ + "backend-common", "backtrace", "derive_more", "diffy", @@ -3680,6 +3709,7 @@ checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" name = "viper" version = "0.1.0" dependencies = [ + "backend-common", "bencher", "bincode", "env_logger", @@ -3688,6 +3718,7 @@ dependencies = [ "jni", "lazy_static", "log", + "prusti-utils", "rustc-hash", "serde", "smt-log-analyzer", diff --git a/backend-common/Cargo.toml b/backend-common/Cargo.toml new file mode 100644 index 00000000000..e596456518a --- /dev/null +++ b/backend-common/Cargo.toml @@ -0,0 +1,10 @@ +[package] +name = "backend-common" +version = "0.1.0" +authors = ["Prusti Devs "] +edition = "2021" + +[dependencies] +serde = { version = "1.0", features = ["derive"] } +rustc-hash = "1.1.0" +vir = { path = "../vir" } diff --git a/viper/src/java_exception.rs b/backend-common/src/java_exception.rs similarity index 100% rename from viper/src/java_exception.rs rename to backend-common/src/java_exception.rs diff --git a/backend-common/src/lib.rs b/backend-common/src/lib.rs new file mode 100644 index 00000000000..6fa91868a14 --- /dev/null +++ b/backend-common/src/lib.rs @@ -0,0 +1,5 @@ +mod verification_result; +mod java_exception; +mod silicon_counterexample; + +pub use crate::{java_exception::*, silicon_counterexample::*, verification_result::*}; diff --git a/backend-common/src/silicon_counterexample.rs b/backend-common/src/silicon_counterexample.rs new file mode 100644 index 00000000000..8eba6d8f3ff --- /dev/null +++ b/backend-common/src/silicon_counterexample.rs @@ -0,0 +1,69 @@ +use rustc_hash::FxHashMap; + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct SiliconCounterexample { + //pub heap: Heap, + //pub old_heaps: FxHashMap, + pub model: Model, + pub functions: Functions, + pub domains: Domains, + pub old_models: FxHashMap, + // label_order because HashMaps do not guarantee order of elements + // whereas the Map used in scala does guarantee it + pub label_order: Vec, +} + +// Model Definitions +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct Model { + pub entries: FxHashMap, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub enum ModelEntry { + LitInt(String), + LitFloat(String), + LitBool(bool), + LitPerm(String), + Ref(String, FxHashMap), + NullRef(String), + RecursiveRef(String), + Var(String), + Seq(String, Vec), + Other(String, String), + DomainValue(String, String), + UnprocessedModel, //used for Silicon's Snap type +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct Functions { + pub entries: FxHashMap, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct FunctionEntry { + pub options: Vec<(Vec>, Option)>, + pub default: Option, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct Domains { + pub entries: FxHashMap, +} + +#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] +pub struct DomainEntry { + pub functions: Functions, +} + +impl FunctionEntry { + /// Given a vec of params it finds the correct entry in a function. + pub fn get_function_value(&self, params: &Vec>) -> &Option { + for option in &self.options { + if &option.0 == params { + return &option.1; + } + } + &None + } +} diff --git a/viper/src/verification_result.rs b/backend-common/src/verification_result.rs similarity index 71% rename from viper/src/verification_result.rs rename to backend-common/src/verification_result.rs index 4bf847217df..ac3786a62a3 100644 --- a/viper/src/verification_result.rs +++ b/backend-common/src/verification_result.rs @@ -4,7 +4,7 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::{silicon_counterexample::SiliconCounterexample, JavaException}; +use crate::{JavaException, SiliconCounterexample}; /// The result of a verification request on a Viper program. #[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] @@ -57,21 +57,3 @@ impl VerificationError { } } } - -/// The consistency error reported by the verifier. -#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct ConsistencyError { - /// To which method corresponds the program that triggered the error. - pub method: String, - /// The actual error. - pub error: String, -} - -/// The Java exception reported by the verifier. -#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct JavaExceptionWithOrigin { - /// To which method corresponds the program that triggered the exception. - pub method: String, - /// The actual exception. - pub exception: JavaException, -} diff --git a/native-verifier/Cargo.toml b/native-verifier/Cargo.toml new file mode 100644 index 00000000000..40f7bd85bb1 --- /dev/null +++ b/native-verifier/Cargo.toml @@ -0,0 +1,20 @@ +[package] +name = "native-verifier" +version = "0.1.0" +authors = ["Prusti Devs "] +edition = "2021" +readme = "README.md" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +log = { version = "0.4", features = ["release_max_level_info"] } +error-chain = "0.12" +uuid = { version = "1.0", features = ["v4"] } +serde = { version = "1.0", features = ["derive"] } +prusti-common = { path = "../prusti-common" } +backend-common = { path = "../backend-common" } +prusti-utils = { path = "../prusti-utils" } +vir = { path = "../vir" } +lazy_static = "1.4" +regex = "1.7.1" \ No newline at end of file diff --git a/native-verifier/src/fol.rs b/native-verifier/src/fol.rs new file mode 100644 index 00000000000..93b177d0485 --- /dev/null +++ b/native-verifier/src/fol.rs @@ -0,0 +1,252 @@ +use std::collections::HashMap; +use vir::{ + common::position::Positioned, + low::{ + ast::{expression::*, statement::*}, + expression::visitors::ExpressionFolder, + *, + }, +}; + +pub enum FolStatement { + Comment(String), + Assume(Expression), + Assert { + expression: Expression, + reason: Option, + }, +} + +pub fn set_position(expr: Expression, new_position: Position) -> Expression { + struct PositionReplacer { + new_position: Position, + } + impl ExpressionFolder for PositionReplacer { + fn fold_position(&mut self, _: Position) -> Position { + self.new_position + } + } + PositionReplacer { new_position }.fold_expression(expr) +} + +fn vir_statement_to_fol_statements( + statement: &Statement, + known_methods: &HashMap, +) -> Vec { + match statement { + Statement::Assume(expr) => vec![FolStatement::Assume(expr.expression.clone())], + Statement::Inhale(expr) => vec![FolStatement::Assume(expr.expression.clone())], + Statement::Assert(expr) => { + let reason_pos = expr.expression.position(); + let failure_pos = expr.position; + + if reason_pos != failure_pos { + vec![FolStatement::Assert { + expression: set_position(expr.expression.clone(), failure_pos), + reason: Some(reason_pos), + }] + } else { + vec![FolStatement::Assert { + expression: expr.expression.clone(), + reason: None, + }] + } + } + Statement::Exhale(expr) => { + let reason_pos = expr.expression.position(); + let failure_pos = expr.position; + + if reason_pos != failure_pos { + vec![FolStatement::Assert { + expression: set_position(expr.expression.clone(), failure_pos), + reason: Some(reason_pos), + }] + } else { + vec![FolStatement::Assert { + expression: expr.expression.clone(), + reason: None, + }] + } + } + Statement::Assign(assign) => { + let eq = Expression::BinaryOp(BinaryOp { + op_kind: BinaryOpKind::EqCmp, + left: Box::new(Expression::Local(Local { + variable: assign.target.clone(), + position: assign.position, + })), + right: Box::new(assign.value.clone()), + position: assign.position, + }); + + vec![FolStatement::Assume(eq)] + } + Statement::Conditional(cond) => { + let negate_guard = Expression::UnaryOp(UnaryOp { + op_kind: UnaryOpKind::Not, + argument: Box::new(cond.guard.clone()), + position: cond.guard.position(), + }); + + let mut statements = vec![]; + for (guard, branch) in [ + (cond.guard.clone(), &cond.then_branch), + (negate_guard, &cond.else_branch), + ] { + for s in branch { + if let Statement::Assert(assert) = s { + let implication = Expression::BinaryOp(BinaryOp { + op_kind: BinaryOpKind::Implies, + left: Box::new(guard.clone()), + right: Box::new(assert.expression.clone()), + position: assert.position, + }); + statements.push(FolStatement::Assert { + expression: implication, + reason: None, // TODO: Reason? + }); + } else if let Statement::Exhale(exhale) = s { + let exhaling = Expression::BinaryOp(BinaryOp { + op_kind: BinaryOpKind::Implies, + left: Box::new(guard.clone()), + right: Box::new(exhale.expression.clone()), + position: exhale.position, + }); + statements.push(FolStatement::Assert { + expression: exhaling, + reason: None, // TODO: Reason? + }); + } else if let Statement::Inhale(inhale) = s { + let implication = Expression::BinaryOp(BinaryOp { + op_kind: BinaryOpKind::Implies, + left: Box::new(guard.clone()), + right: Box::new(inhale.expression.clone()), + position: inhale.position, + }); + statements.push(FolStatement::Assume(implication)); + } else if let Statement::Assume(assume) = s { + let assumption = Expression::BinaryOp(BinaryOp { + op_kind: BinaryOpKind::Implies, + left: Box::new(guard.clone()), + right: Box::new(assume.expression.clone()), + position: assume.position, + }); + statements.push(FolStatement::Assume(assumption)); + } else { + statements.push(FolStatement::Comment( + "Generated within a conditional:".to_string(), + )); + statements.extend(vir_statement_to_fol_statements(s, known_methods)); + } + } + } + statements + } + Statement::MethodCall(method_call) => { + let method_decl = known_methods + .get(&method_call.method_name) + .expect("Method not found"); + + let mut params_to_args = method_decl + .parameters + .iter() + .zip(method_call.arguments.iter()) + .map(|(target, arg)| (target.clone(), arg.clone())) + .collect::>(); + + let returns_to_targets = method_decl + .targets + .iter() + .zip(method_call.targets.iter()) + .map(|(target, arg)| (target.clone(), arg.clone())) + .collect::>(); + + params_to_args.extend(returns_to_targets); + + fn substitute( + expr: &Expression, + mapping: &HashMap, + ) -> Expression { + match expr { + Expression::Local(local) => { + if let Some(arg) = mapping.get(&local.variable) { + arg.clone() + } else { + Expression::Local(local.clone()) + } + } + Expression::BinaryOp(op) => Expression::BinaryOp(BinaryOp { + op_kind: op.op_kind, + left: Box::new(substitute(&op.left, mapping)), + right: Box::new(substitute(&op.right, mapping)), + position: op.position, + }), + Expression::UnaryOp(op) => Expression::UnaryOp(UnaryOp { + op_kind: op.op_kind, + argument: Box::new(substitute(&op.argument, mapping)), + position: op.position, + }), + Expression::ContainerOp(op) => Expression::ContainerOp(ContainerOp { + kind: op.kind, + container_type: op.container_type.clone(), + operands: op + .operands + .iter() + .map(|arg| substitute(arg, mapping)) + .collect(), + position: op.position, + }), + Expression::Constant(constant) => Expression::Constant(constant.clone()), + Expression::DomainFuncApp(func) => Expression::DomainFuncApp(DomainFuncApp { + domain_name: func.domain_name.clone(), + function_name: func.function_name.clone(), + arguments: func + .arguments + .iter() + .map(|arg| substitute(arg, mapping)) + .collect(), + parameters: func.parameters.clone(), + return_type: func.return_type.clone(), + position: func.position, + }), + Expression::MagicWand(magic_wand) => Expression::MagicWand(MagicWand { + left: Box::new(substitute(&magic_wand.left, mapping)), + right: Box::new(substitute(&magic_wand.right, mapping)), + position: magic_wand.position, + }), + _ => unimplemented!("substitute not implemented for {:?}", expr), + } + } + + let preconds = method_decl.pres.iter().map(|pre| { + // substitute parameters for arguments + FolStatement::Assert { + expression: substitute(pre, ¶ms_to_args), + reason: None, + } + }); + + let postconds = method_decl.posts.iter().map(|post| { + // substitute parameters for arguments + FolStatement::Assume(substitute(post, ¶ms_to_args)) + }); + + preconds.chain(postconds).collect::>() + } + Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())], + Statement::LogEvent(_) => vec![], // ignored + _ => { + unimplemented!("Statement {:?} not yet supported", statement); + } + } +} + +pub fn vir_to_fol( + statements: &[Statement], + known_methods: &HashMap, +) -> Vec { + statements + .iter() + .flat_map(|s| vir_statement_to_fol_statements(s, known_methods)) + .collect() +} diff --git a/native-verifier/src/lib.rs b/native-verifier/src/lib.rs new file mode 100644 index 00000000000..a396e480131 --- /dev/null +++ b/native-verifier/src/lib.rs @@ -0,0 +1,10 @@ +#![feature(try_blocks)] +#![feature(let_chains)] + +pub mod verifier; +mod smt_lib; +mod theory_provider; +mod optimization; +mod fol; + +pub use crate::verifier::*; diff --git a/native-verifier/src/optimization.rs b/native-verifier/src/optimization.rs new file mode 100644 index 00000000000..c454985a776 --- /dev/null +++ b/native-verifier/src/optimization.rs @@ -0,0 +1,264 @@ +use vir::{ + common::position::Positioned, + low::{ + expression::{visitors::ExpressionFolder, BinaryOp, Constant, MagicWand, UnaryOp}, + Expression, Position, + }, +}; + +use crate::fol::FolStatement; + +struct Optimizer {} + +fn constant_at(value: bool, position: Position) -> Expression { + vir::low::Expression::Constant(Constant { + value: value.into(), + ty: vir::low::Type::Bool, + position, + }) +} + +fn equal_to_const(value: &Expression, constant: bool) -> bool { + if let vir::low::Expression::Constant(Constant { + value: vir::low::ConstantValue::Bool(b), + ty: vir::low::Type::Bool, + .. + }) = value + { + *b == constant + } else { + false + } +} + +impl ExpressionFolder for Optimizer { + fn fold_binary_op_enum(&mut self, binary_op: BinaryOp) -> Expression { + let new_left = self.fold_expression(*binary_op.left); + let new_right = self.fold_expression(*binary_op.right); + + match binary_op.op_kind { + vir::low::BinaryOpKind::EqCmp => { + if new_left == new_right { + constant_at(true, binary_op.position) + } else { + vir::low::Expression::BinaryOp(BinaryOp { + left: Box::new(new_left), + right: Box::new(new_right), + ..binary_op + }) + } + } + vir::low::BinaryOpKind::NeCmp => { + if new_left == new_right { + constant_at(false, binary_op.position) + } else { + vir::low::Expression::BinaryOp(BinaryOp { + left: Box::new(new_left), + right: Box::new(new_right), + ..binary_op + }) + } + } + vir::low::BinaryOpKind::And => { + if equal_to_const(&new_left, true) { + new_right + } else if equal_to_const(&new_right, true) { + new_left + } else if equal_to_const(&new_left, false) { + constant_at(false, new_right.position()) + } else if equal_to_const(&new_right, false) { + constant_at(false, new_left.position()) + } else { + vir::low::Expression::BinaryOp(BinaryOp { + left: Box::new(new_left), + right: Box::new(new_right), + ..binary_op + }) + } + } + vir::low::BinaryOpKind::Or => { + if equal_to_const(&new_left, true) { + constant_at(true, new_right.position()) + } else if equal_to_const(&new_right, true) { + constant_at(true, new_left.position()) + } else if equal_to_const(&new_left, false) { + new_right + } else if equal_to_const(&new_right, false) { + new_left + } else { + vir::low::Expression::BinaryOp(BinaryOp { + left: Box::new(new_left), + right: Box::new(new_right), + ..binary_op + }) + } + } + vir::low::BinaryOpKind::Implies => { + if equal_to_const(&new_left, true) { + new_right + } else if equal_to_const(&new_right, false) { + self.fold_unary_op_enum(UnaryOp { + op_kind: vir::low::UnaryOpKind::Not, + position: new_left.position(), + argument: Box::new(new_left), + }) + } else if equal_to_const(&new_left, false) { + constant_at(true, new_right.position()) + } else if equal_to_const(&new_right, true) { + constant_at(true, new_left.position()) + } else { + vir::low::Expression::BinaryOp(BinaryOp { + left: Box::new(new_left), + right: Box::new(new_right), + ..binary_op + }) + } + } + _ => vir::low::Expression::BinaryOp(BinaryOp { + left: Box::new(new_left), + right: Box::new(new_right), + ..binary_op + }), + } + } + + fn fold_unary_op_enum(&mut self, unary_op: UnaryOp) -> Expression { + let new_argument = self.fold_expression(*unary_op.argument); + + match unary_op.op_kind { + vir::low::UnaryOpKind::Not => { + if equal_to_const(&new_argument, true) { + constant_at(false, new_argument.position()) + } else if equal_to_const(&new_argument, false) { + constant_at(true, new_argument.position()) + } else if let vir::low::Expression::UnaryOp(UnaryOp { + op_kind: vir::low::UnaryOpKind::Not, + argument, + .. + }) = new_argument + { + *argument + } else { + vir::low::Expression::UnaryOp(UnaryOp { + argument: Box::new(new_argument), + ..unary_op + }) + } + } + _ => vir::low::Expression::UnaryOp(UnaryOp { + argument: Box::new(new_argument), + ..unary_op + }), + } + } + + fn fold_quantifier_enum( + &mut self, + quantifier: vir::low::expression::Quantifier, + ) -> vir::low::Expression { + if quantifier.triggers.is_empty() { + let new_body = self.fold_expression(*quantifier.body); + if equal_to_const(&new_body, true) + && quantifier.kind == vir::low::expression::QuantifierKind::ForAll + { + constant_at(true, new_body.position()) + } else if equal_to_const(&new_body, false) + && quantifier.kind == vir::low::expression::QuantifierKind::Exists + { + constant_at(false, new_body.position()) + } else { + vir::low::Expression::Quantifier(vir::low::expression::Quantifier { + body: Box::new(new_body), + ..quantifier + }) + } + } else { + quantifier.into() // cannot optimize because we might remove something that is in a trigger + } + } + + fn fold_magic_wand_enum(&mut self, magic_wand: vir::low::expression::MagicWand) -> Expression { + // magic wand (--*) is basically implication, so we can simplify accordingly + let new_left = self.fold_expression(*magic_wand.left); + let new_right = self.fold_expression(*magic_wand.right); + + if equal_to_const(&new_left, true) { + new_right + } else if equal_to_const(&new_right, false) { + self.fold_unary_op_enum(UnaryOp { + op_kind: vir::low::UnaryOpKind::Not, + position: new_left.position(), + argument: Box::new(new_left), + }) + } else if equal_to_const(&new_left, false) { + constant_at(true, new_right.position()) + } else if equal_to_const(&new_right, true) { + constant_at(true, new_left.position()) + } else { + vir::low::Expression::MagicWand(MagicWand { + left: Box::new(new_left), + right: Box::new(new_right), + position: magic_wand.position, + }) + } + } + + fn fold_conditional_enum( + &mut self, + conditional: vir::low::expression::Conditional, + ) -> Expression { + let new_cond = self.fold_expression(*conditional.guard); + let new_true = self.fold_expression(*conditional.then_expr); + let new_false = self.fold_expression(*conditional.else_expr); + + if equal_to_const(&new_cond, true) { + new_true + } else if equal_to_const(&new_cond, false) { + new_false + } else if new_true == new_false { + new_true + } else if equal_to_const(&new_true, true) && equal_to_const(&new_false, false) { + new_cond + } else if equal_to_const(&new_true, false) && equal_to_const(&new_false, true) { + self.fold_unary_op_enum(UnaryOp { + op_kind: vir::low::UnaryOpKind::Not, + position: new_cond.position(), + argument: Box::new(new_cond), + }) + } else { + vir::low::Expression::Conditional(vir::low::expression::Conditional { + guard: Box::new(new_cond), + then_expr: Box::new(new_true), + else_expr: Box::new(new_false), + position: conditional.position, + }) + } + } +} + +pub fn optimize_statements(statements: Vec) -> Vec { + statements + .into_iter() + .filter_map(|statement| match statement { + FolStatement::Assume(expr) => { + let mut optimizer = Optimizer {}; + let expr = optimizer.fold_expression(expr); + if equal_to_const(&expr, true) { + None + } else { + Some(FolStatement::Assume(expr)) + } + } + FolStatement::Assert { expression, reason } => { + let mut optimizer = Optimizer {}; + let expression = optimizer.fold_expression(expression); + if equal_to_const(&expression, true) { + None + } else { + Some(FolStatement::Assert { expression, reason }) + } + } + x => Some(x), + }) + .collect() +} diff --git a/native-verifier/src/smt_lib.rs b/native-verifier/src/smt_lib.rs new file mode 100644 index 00000000000..1bee320efb0 --- /dev/null +++ b/native-verifier/src/smt_lib.rs @@ -0,0 +1,820 @@ +use crate::optimization::optimize_statements; + +use super::{ + fol::{vir_to_fol, FolStatement}, + theory_provider::*, +}; +use lazy_static::lazy_static; +use log::warn; +use regex::Regex; +use std::collections::{HashMap, HashSet}; +use vir::{ + common::position::Positioned, + low::{ + ast::{expression::*, ty::*}, + operations::ty::Typed, + *, + }, +}; + +lazy_static! { + static ref ONE_PARAM_RE: Regex = Regex::new(r"(Set|Seq|MultiSet)<([^>]+)>").unwrap(); + static ref TWO_PARAM_RE: Regex = Regex::new(r"Map<([^>]+)\s*,\s*([^>]+)>").unwrap(); + static ref MARKER_RE: Regex = Regex::new(r"label.*\$marker\b\s").unwrap(); +} + +const NO_Z3_PREAMBLE: &str = include_str!("theories/Preamble.smt2"); +const Z3_PREAMBLE: &str = include_str!("theories/PreambleZ3.smt2"); + +pub struct SMTLib { + sort_decls: Vec, + func_decls: Vec, + code: Vec, + methods: HashMap, + blocks: HashMap, + using_z3: bool, +} + +impl SMTLib { + pub fn new(using_z3: bool) -> Self { + Self { + sort_decls: Vec::new(), + func_decls: Vec::new(), + code: Vec::new(), + methods: HashMap::new(), + blocks: Default::default(), + using_z3, + } + } + fn add_sort_decl(&mut self, sort_decl: String) { + self.sort_decls + .push(format!("(declare-sort {} 0)", sort_decl)); + } + fn add_func(&mut self, func_decl: String) { + self.func_decls.push(func_decl); + } + fn add_assert(&mut self, assert: String) { + self.code.push(format!("(assert {})", assert)); + } + fn add_code(&mut self, text: String) { + self.code.push(text); + } + fn emit(&mut self, predicate: FolStatement) { + 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, reason } => { + let position = expression.position(); + + if position.id == 0 { + return; + } + + // negate predicate + let negated = Expression::UnaryOp(UnaryOp { + op_kind: UnaryOpKind::Not, + argument: Box::new(expression.clone()), + position, + }); + + // assert negated predicate + self.add_code("(push)".to_string()); + self.add_code(format!("(assert {})", negated.to_smt())); + if let Some(res) = reason { + self.add_code(format!( + "(echo \"position: {}, reason: {}\")", + position.id, res.id + )); + } else { + self.add_code(format!("(echo \"position: {}\")", position.id)); + } + + self.add_code("(check-sat)".to_string()); + self.add_code("(pop)".to_string()); + + // assume predicate afterwards + self.add_code(format!( + "(assert {}) ; assumed after assert\n", + expression.to_smt() + )); + } + } + } + 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; + } + + let is_branch = precond.is_some(); + + self.add_code(format!("; Basic block: {}", block.label)); + if is_branch { + self.add_code("(push)".to_string()); + } + + // assume precond if any + if let Some(precond) = precond { + // TODO: Location of the call site + self.add_code("; Branch precond:".to_string()); + self.add_assert(precond.to_smt()); + } + + // verify body + let predicates = vir_to_fol(&block.statements, &self.methods); + let predicates = optimize_statements(predicates); + + predicates.into_iter().for_each(|predicate| { + self.emit(predicate); + }); + + // process successor + match &block.successor { + Successor::Goto(label) => { + self.follow(&label.name, None); + } + Successor::GotoSwitch(mapping) => { + // if last branch is "true", it is the "otherwise" branch + // see: prusti-viper/src/encoder/mir/procedures/encoder/mod.rs + let (last_expr, last_label) = mapping.iter().last().unwrap(); + + if let Expression::Constant(Constant { + value: ConstantValue::Bool(true), + .. + }) = last_expr + { + // create an "and" of all negations of previous expressions + let and = mapping + .iter() + .take(mapping.len() - 1) + .map(|(expr, _)| expr) + .fold(None, |acc, expr| { + if let Some(acc) = acc { + Some(Expression::BinaryOp(BinaryOp { + op_kind: BinaryOpKind::And, + left: Box::new(acc), + right: Box::new(Expression::UnaryOp(UnaryOp { + op_kind: UnaryOpKind::Not, + argument: Box::new(expr.clone()), + position: expr.position(), + })), + position: expr.position(), + })) + } else { + Some(Expression::UnaryOp(UnaryOp { + op_kind: UnaryOpKind::Not, + argument: Box::new(expr.clone()), + position: expr.position(), + })) + } + }); + + self.follow(&last_label.name, and.as_ref()); + } else { + self.follow(&last_label.name, Some(last_expr)); + } + + mapping + .iter() + .take(mapping.len() - 1) + .for_each(|(expr, label)| { + self.follow(&label.name, Some(expr)); + }) + } + Successor::Return => {} + } + + if is_branch { + self.add_code(format!("(pop); End basic block: {}", block.label)); + } + } +} + +impl ToString for SMTLib { + fn to_string(&self) -> String { + let mut result = String::new(); + result.push_str(if self.using_z3 { + Z3_PREAMBLE + } else { + NO_Z3_PREAMBLE + }); + result.push_str("\n\n"); + result.push_str(&self.sort_decls.join("\n")); + result.push_str("\n\n"); + + let mut main: String = "\n\n".to_string(); + main.push_str(&self.func_decls.join("\n")); + main.push_str("\n\n"); + main.push_str(&self.code.join("\n")); + + // initialize the theory providers + let set_provider = ContainerTheoryProvider::new("Set"); + let seq_provider = ContainerTheoryProvider::new("Seq"); + let multiset_provider = ContainerTheoryProvider::new("MultiSet"); + let map_provider = MapTheoryProvider::new(); + + // set of seen combinations + let mut seen = std::collections::HashSet::new(); + + for cap in ONE_PARAM_RE.captures_iter(&main) { + let container = &cap[1]; + let element_type: &str = &cap[2]; + + // check if seen so far + if seen.contains(&(container.to_string(), element_type.to_string())) { + continue; + } + + match container { + "Set" => result.push_str(&set_provider.get_theory(element_type)), + "Seq" => result.push_str(&seq_provider.get_theory(element_type)), + "MultiSet" => result.push_str(&multiset_provider.get_theory(element_type)), + _ => panic!("Unknown container type: {}", container), + } + + // add the combination to the set of seen combinations + seen.insert((container.to_string(), element_type.to_string())); + } + + // set of seen combinations + let mut seen = std::collections::HashSet::new(); + + // same for Map in TWO_PARAM_RE + for cap in TWO_PARAM_RE.captures_iter(&main) { + let key_type = &cap[1]; + let value_type = &cap[2]; + + // check if seen so far + if seen.contains(&(key_type.to_string(), value_type.to_string())) { + continue; + } + + result.push_str(&map_provider.get_theory(key_type, value_type)); + + // add the combination to the set of seen combinations + seen.insert((key_type.to_string(), value_type.to_string())); + } + + result.push_str(&main); + + result + .lines() + .filter(|&line| !MARKER_RE.is_match(line)) // TODO: SSO form for marker variables? + .collect::>() + .join("\n") + } +} + +pub trait SMTTranslatable { + fn build_smt(&self, _: &mut SMTLib) { + unimplemented!() + } + fn to_smt(&self) -> String { + unimplemented!() + } +} + +// args are any collection of SMTTranslatable +fn mk_app(name: &String, args: &Vec) -> String +where + T: SMTTranslatable, +{ + if args.is_empty() { + name.clone() + } else { + format!( + "({} {})", + name, + args.iter() + .map(|a| a.to_smt()) + .collect::>() + .join(" ") + ) + } +} + +impl SMTTranslatable for Program { + fn build_smt(&self, smt: &mut SMTLib) { + self.domains.iter().for_each(|d| d.build_smt(smt)); + self.methods.iter().for_each(|d| d.build_smt(smt)); + self.procedures.iter().for_each(|d| d.build_smt(smt)); + + // the following are empty in vir::low + snapshot-based encoding + assert!(self.functions.is_empty()); + assert!(self.predicates.is_empty()); + } +} + +/* #region Domains */ + +impl SMTTranslatable for DomainDecl { + fn build_smt(&self, smt: &mut SMTLib) { + smt.add_sort_decl(self.name.clone()); + + if !self.functions.is_empty() { + smt.add_func(format!("; Functions for domain {}", self.name)); + self.functions.iter().for_each(|f| f.build_smt(smt)); + } + + if !self.axioms.is_empty() { + smt.add_code(format!("; Axioms for domain {}", self.name)); + self.axioms.iter().for_each(|a| a.build_smt(smt)); + } + } +} + +impl SMTTranslatable for DomainFunctionDecl { + // TODO: self.is_unique + fn build_smt(&self, smt: &mut SMTLib) { + let mut fun = String::new(); + + fun.push_str(&format!("(declare-fun {} (", self.name)); + fun.push_str( + &self + .parameters + .iter() + .map(|p| p.ty.to_smt()) + .collect::>() + .join(" "), + ); + fun.push_str(&format!(") {})", self.return_type.to_smt())); + + smt.add_func(fun); + } +} + +impl SMTTranslatable for DomainAxiomDecl { + fn build_smt(&self, smt: &mut SMTLib) { + if let Some(comment) = &self.comment { + smt.add_assert(format!("; {}", comment)); + } + + smt.add_code(format!("(assert {}) ; {}", self.body.to_smt(), self.name)); + } +} + +/* #endregion */ + +/* #region Methods and Procedures */ + +impl SMTTranslatable for MethodDecl { + fn build_smt(&self, smt: &mut SMTLib) { + // if body is None, we have a body-less method with only pre- and postconditions + // we assume these to be correct by default and collect their signatures + if self.body.is_none() { + smt.methods.insert(self.name.clone(), self.clone()); + } else { + unimplemented!("Method bodies are not yet supported"); + } + } +} + +impl SMTTranslatable for ProcedureDecl { + fn build_smt(&self, smt: &mut SMTLib) { + smt.add_code(format!("; Procedure {}", self.name)); + + smt.add_code("(push)".to_string()); + + // declare locals + self.locals.iter().for_each(|l| l.build_smt(smt)); + + // process basic blocks + smt.blocks.clear(); + + self.basic_blocks.iter().for_each(|b| { + smt.blocks.insert(b.label.name.clone(), b.clone()); + }); + + // find a starting block + let mut start_blocks = smt.blocks.keys().collect::>(); + + for block in smt.blocks.values() { + 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()); + } +} + +impl SMTTranslatable for VariableDecl { + fn build_smt(&self, smt: &mut SMTLib) { + smt.add_code(format!( + "(declare-const {} {})", + self.name, + self.ty.to_smt() + )); + } +} + +/* #endregion */ + +impl SMTTranslatable for Expression { + fn to_smt(&self) -> String { + match self { + Expression::Local(local) => local.variable.name.clone(), + Expression::Field(_) => unimplemented!(), + Expression::LabelledOld(_) => unimplemented!("old expressions"), + Expression::Constant(constant) => match &constant.value { + ConstantValue::Bool(bool) => bool.to_string(), + ConstantValue::Int(i) => { + if let Some(abs_val) = i.to_string().strip_prefix('-') { + format!("(- {})", abs_val) + } else { + i.to_string() + } + } + ConstantValue::Float32(u32) => { + let bits = u32.to_le_bytes(); + let bits = bits + .iter() + .rev() + .map(|b| format!("{:08b}", b)) + .collect::>() + .join(""); + format!( + "(fp #b{} #b{} #b{})", + &bits.chars().next().unwrap(), + &bits[1..=8], + &bits[9..=31] + ) + } + ConstantValue::Float64(u64) => { + let bits = u64.to_le_bytes(); + let bits = bits + .iter() + .rev() + .map(|b| format!("{:08b}", b)) + .collect::>() + .join(""); + format!( + "(fp #b{} #b{} #b{})", + &bits.chars().next().unwrap(), + &bits[1..=11], + &bits[12..=63] + ) + } + ConstantValue::BigInt(s) => { + if let Some(abs_val) = s.strip_prefix('-') { + format!("(- {})", abs_val) + } else { + s.clone() + } + } + }, + Expression::MagicWand(wand) => { + // if left is just constant true, we can ignore it + if let Expression::Constant(Constant { + value: ConstantValue::Bool(true), + .. + }) = *wand.left + { + format!("(=> {} {})", wand.left.to_smt(), wand.right.to_smt()) + } else { + unimplemented!("Non-trivial MagicWand not supported: {}", wand); + } + } + Expression::PredicateAccessPredicate(_access) => { + warn!("PredicateAccessPredicate not supported: {}", _access); + format!( + "({} {})", + _access.name, + _access + .arguments + .iter() + .map(|x| x.to_smt()) + .collect::>() + .join(" ") + ) + } + Expression::FieldAccessPredicate(_) => unimplemented!(), + Expression::Unfolding(_) => unimplemented!(), + Expression::UnaryOp(unary_op) => { + let op_smt = if unary_op.argument.get_type().is_float() { + FloatUnaryOpKind(unary_op.op_kind).to_smt() + } else { + IntUnaryOpKind(unary_op.op_kind).to_smt() + }; + + format!("({} {})", op_smt, unary_op.argument.to_smt()) + } + Expression::BinaryOp(binary_op) => { + let op_smt = if let Type::Float(fsize) = binary_op.left.get_type() { + FloatBinaryOpKind(binary_op.op_kind, *fsize).to_smt() + } else { + IntBinaryOpKind(binary_op.op_kind).to_smt() + }; + + format!( + "({} {} {})", + op_smt, + binary_op.left.to_smt(), + binary_op.right.to_smt() + ) + } + Expression::PermBinaryOp(perm_binary_op) => format!( + "({} {} {})", + perm_binary_op.op_kind.to_smt(), + perm_binary_op.left.to_smt(), + perm_binary_op.right.to_smt() + ), + Expression::ContainerOp(container_op) => container_op.to_smt(), + Expression::Conditional(conditional) => format!( + "(ite {} {} {})", + conditional.guard.to_smt(), + conditional.then_expr.to_smt(), + conditional.else_expr.to_smt() + ), + // TODO: Quantifier triggers + Expression::Quantifier(quantifier) => { + let mut quant = String::new(); + + match quantifier.kind { + QuantifierKind::ForAll => quant.push_str("(forall ("), + QuantifierKind::Exists => quant.push_str("(exists ("), + } + + quant.push_str( + &quantifier + .variables + .iter() + .map(|v| format!("({} {})", v.name, v.ty.to_smt())) + .collect::>() + .join(" "), + ); + quant.push_str(") "); + + let triggers: Vec<_> = quantifier + .triggers + .iter() + .filter(|t| { + !t.terms + .iter() + .any(|t| matches!(t, Expression::PredicateAccessPredicate(_))) + // TODO: Support triggers with predicate access predicates? + }) + .collect(); + + if triggers.is_empty() { + quant.push_str(&quantifier.body.to_smt()); + quant.push(')'); + } else { + // triggers are :pattern + quant.push_str("(! "); + quant.push_str(&quantifier.body.to_smt()); + + for trigger in &triggers { + quant.push_str(" :pattern ("); + + quant.push_str( + &trigger + .terms + .iter() + .map(|expr| expr.to_smt()) + .collect::>() + .join(" "), + ); + + quant.push(')'); + } + + quant.push_str("))"); + } + + quant + } + Expression::LetExpr(_) => unimplemented!(), + Expression::FuncApp(func) => { + let mut app = "(".to_string(); + + app.push_str(&func.function_name); + app.push(' '); + + app.push_str( + &func + .arguments + .iter() + .map(|arg| arg.to_smt()) + .collect::>() + .join(" "), + ); + + app.push(')'); + app + } + Expression::DomainFuncApp(domain_func_app) => { + mk_app(&domain_func_app.function_name, &domain_func_app.arguments) + } + Expression::InhaleExhale(_) => unimplemented!(), + } + } +} + +struct IntBinaryOpKind(BinaryOpKind); +struct FloatBinaryOpKind(BinaryOpKind, Float); + +impl SMTTranslatable for IntBinaryOpKind { + fn to_smt(&self) -> String { + match self.0 { + BinaryOpKind::EqCmp => "=", + BinaryOpKind::NeCmp => "distinct", + BinaryOpKind::GtCmp => ">", + BinaryOpKind::GeCmp => ">=", + BinaryOpKind::LtCmp => "<", + BinaryOpKind::LeCmp => "<=", + BinaryOpKind::Add => "+", + BinaryOpKind::Sub => "-", + BinaryOpKind::Mul => "*", + BinaryOpKind::Div => "div", + BinaryOpKind::Mod => "rust_mod", + BinaryOpKind::And => "and", + BinaryOpKind::Or => "or", + BinaryOpKind::Implies => "=>", + } + .to_string() + } +} + +impl SMTTranslatable for FloatBinaryOpKind { + fn to_smt(&self) -> String { + match (self.0, self.1) { + // BinaryOpKind::EqCmp => "fp.eq", // TODO: = in axioms, fp.eq in arithmetic? + (BinaryOpKind::EqCmp, _) => "=", + (BinaryOpKind::NeCmp, Float::F32) => "fp.neq32", // Not in SMT-LIB 2.6 standard, part of static preamble + (BinaryOpKind::NeCmp, Float::F64) => "fp.neq64", // Not in SMT-LIB 2.6 standard, part of static preamble + (BinaryOpKind::GtCmp, _) => "fp.gt", + (BinaryOpKind::GeCmp, _) => "fp.geq", + (BinaryOpKind::LtCmp, _) => "fp.lt", + (BinaryOpKind::LeCmp, _) => "fp.leq", + (BinaryOpKind::Add, _) => "fp.add roundNearestTiesToAway", + (BinaryOpKind::Sub, _) => "fp.sub roundNearestTiesToAway", + (BinaryOpKind::Mul, _) => "fp.mul roundNearestTiesToAway", + (BinaryOpKind::Div, _) => "fp.div roundNearestTiesToAway", + (BinaryOpKind::Mod, _) => "fp.rem", + (other, _) => unreachable!("FP {}", other), + } + .to_string() + } +} + +impl SMTTranslatable for PermBinaryOpKind { + fn to_smt(&self) -> String { + match self { + PermBinaryOpKind::Add => "+", + PermBinaryOpKind::Sub => "-", + PermBinaryOpKind::Mul => "*", + PermBinaryOpKind::Div => "/", + } + .to_string() + } +} + +struct IntUnaryOpKind(UnaryOpKind); +struct FloatUnaryOpKind(UnaryOpKind); + +impl SMTTranslatable for IntUnaryOpKind { + fn to_smt(&self) -> String { + match self.0 { + UnaryOpKind::Not => "not", + UnaryOpKind::Minus => "-", + } + .to_string() + } +} + +impl SMTTranslatable for FloatUnaryOpKind { + fn to_smt(&self) -> String { + match self.0 { + UnaryOpKind::Not => unreachable!("FP not"), + UnaryOpKind::Minus => "fp.neg", + } + .to_string() + } +} + +impl SMTTranslatable for ContainerOp { + fn to_smt(&self) -> String { + match &self.kind { + ContainerOpKind::SetConstructor => { + if self.operands.len() == 1 { + return format!("(Set_singleton {})", self.operands[0].to_smt()); + } + + fn recurse(set: String, arg: &Expression) -> String { + format!("(Set_unionone {} {})", set, arg.to_smt()) + } + self.operands.iter().fold("Set_empty".to_string(), recurse) + } + ContainerOpKind::SeqConstructor => { + if self.operands.len() == 1 { + return format!("(Seq_singleton {})", self.operands[0].to_smt()); + } + + fn recurse(seq: String, arg: &Expression) -> String { + format!("(Seq_build {} {})", seq, arg.to_smt()) + } + self.operands.iter().fold("Seq_empty".to_string(), recurse) + } + kind => format!( + "({} {})", + kind.to_smt(), + self.operands + .iter() + .map(|a| a.to_smt()) + .collect::>() + .join(" ") + ), + } + } +} + +impl SMTTranslatable for ContainerOpKind { + fn to_smt(&self) -> String { + match self { + ContainerOpKind::SetCardinality => "Set_card", + ContainerOpKind::SetConstructor => "Set_singleton", + ContainerOpKind::SetContains => "Set_in", + ContainerOpKind::SetEmpty => "Set_empty", + ContainerOpKind::SetIntersection => "Set_intersection", + ContainerOpKind::SetMinus => "Set_difference", + ContainerOpKind::SetSubset => "Set_subset", + ContainerOpKind::SetUnion => "Set_union", + + ContainerOpKind::SeqEmpty => "Seq_empty", + ContainerOpKind::SeqConstructor => "Seq_singleton", + ContainerOpKind::SeqIndex => "Seq_index", + ContainerOpKind::SeqConcat => "Seq_concat", + ContainerOpKind::SeqLen => "Seq_length", + + x => unimplemented!("ContainerOpKind::{}::to_smt()", x), + } + .to_string() + } +} + +impl SMTTranslatable for Type { + fn to_smt(&self) -> String { + match self { + Type::Int => "Int".to_string(), + Type::Bool => "Bool".to_string(), + Type::Perm => "$Perm".to_string(), + Type::Float(float) => match float { + Float::F32 => "Float32".to_string(), + Float::F64 => "Float64".to_string(), + }, + Type::BitVector(bitvec) => match bitvec { + // TODO: Should they map to the same type? + BitVector::Signed(size) => { + format!("(_ BitVec {})", size.to_smt()) + } + BitVector::Unsigned(size) => { + format!("(_ BitVec {})", size.to_smt()) + } + }, + Type::Seq(seq) => format!("Seq<{}>", seq.element_type.to_smt()), + Type::Set(set) => format!("Set<{}>", set.element_type.to_smt()), + Type::MultiSet(_) => unimplemented!("MultiSet"), + Type::Map(_) => unimplemented!("Map"), + Type::Ref => unimplemented!("Ref"), + Type::Domain(domain) => domain.name.to_string(), + } + } +} + +impl SMTTranslatable for BitVectorSize { + fn to_smt(&self) -> String { + match self { + BitVectorSize::BV8 => "8".to_string(), + BitVectorSize::BV16 => "16".to_string(), + BitVectorSize::BV32 => "32".to_string(), + BitVectorSize::BV64 => "64".to_string(), + BitVectorSize::BV128 => "128".to_string(), + } + } +} diff --git a/native-verifier/src/theories/Map.smt2 b/native-verifier/src/theories/Map.smt2 new file mode 100644 index 00000000000..b428f3e2df4 --- /dev/null +++ b/native-verifier/src/theories/Map.smt2 @@ -0,0 +1,2 @@ + +; ===== Map theory for types KEYTYPENAME and VALUETYPENAME ===== \ No newline at end of file diff --git a/native-verifier/src/theories/MultiSet.smt2 b/native-verifier/src/theories/MultiSet.smt2 new file mode 100644 index 00000000000..04ea0b55fb5 --- /dev/null +++ b/native-verifier/src/theories/MultiSet.smt2 @@ -0,0 +1,2 @@ + +; ===== MultiSet theory for type TYPENAME ===== \ No newline at end of file diff --git a/native-verifier/src/theories/Preamble.smt2 b/native-verifier/src/theories/Preamble.smt2 new file mode 100644 index 00000000000..6dd18112f79 --- /dev/null +++ b/native-verifier/src/theories/Preamble.smt2 @@ -0,0 +1,27 @@ +; ===== Static preamble ===== + +(set-info :smt-lib-version 2.6) +(set-logic ALL) +(set-option :tlimit-per 10000) +(set-option :produce-models true) ; equivalent to model.v2 in Z3 +(set-option :produce-assignments false) ; similar to model.partial in Z3 + +; --- Modelling Rust's implementation of % --- + +(define-fun rust_mod ((dividend Int) (divisor Int)) Int + (ite (>= dividend 0) + (mod dividend (abs divisor)) + (- (mod (- dividend) (abs divisor))) + ) +) + +; --- Inequality operator for FloatingPoint bit-vectors --- + +(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y))) +(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y))) + +; --- Legacy permission sort --- + +(define-sort $Perm () Real) + +; ===== End static preamble ===== \ No newline at end of file diff --git a/native-verifier/src/theories/PreambleZ3.smt2 b/native-verifier/src/theories/PreambleZ3.smt2 new file mode 100644 index 00000000000..19dc0d32fdc --- /dev/null +++ b/native-verifier/src/theories/PreambleZ3.smt2 @@ -0,0 +1,56 @@ +; ===== Static preamble ===== + +(set-info :smt-lib-version 2.6) + +(set-option :global-decls true) ; Boogie: default +(set-option :auto_config false) ; Usually a good idea +(set-option :smt.restart_strategy 0) +(set-option :smt.restart_factor |1.5|) +(set-option :smt.case_split 3) +(set-option :smt.delay_units true) +(set-option :smt.delay_units_threshold 16) +(set-option :nnf.sk_hack true) +(set-option :type_check true) +(set-option :smt.bv.reflect true) +(set-option :smt.mbqi false) +(set-option :smt.qi.cost "(+ weight generation)") +(set-option :smt.qi.eager_threshold 1000) +(set-option :smt.qi.max_multi_patterns 1000) +(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0 +(set-option :sat.phase caching) +(set-option :sat.random_seed 0) +(set-option :nlsat.randomize true) +(set-option :nlsat.seed 0) +(set-option :nlsat.shuffle_vars false) +(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5 +(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5 +(set-option :smt.arith.random_initial_value true) ; Boogie: true +(set-option :smt.random_seed 0) +(set-option :sls.random_offset true) +(set-option :sls.random_seed 0) +(set-option :sls.restart_init false) +(set-option :sls.walksat_ucb true) +(set-option :model.v2 true) +(set-option :model.partial false) + +(set-option :timeout 10000) + +; --- Modelling Rust's implementation of % --- + +(define-fun rust_mod ((dividend Int) (divisor Int)) Int + (ite (>= dividend 0) + (mod dividend (abs divisor)) + (- (mod (- dividend) (abs divisor))) + ) +) + +; --- Inequality operator for FloatingPoint bit-vectors --- + +(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y))) +(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y))) + +; --- Legacy permission sort --- + +(define-sort $Perm () Real) + +; ===== End static preamble ===== \ No newline at end of file diff --git a/native-verifier/src/theories/Seq.smt2 b/native-verifier/src/theories/Seq.smt2 new file mode 100644 index 00000000000..7cfb355bd58 --- /dev/null +++ b/native-verifier/src/theories/Seq.smt2 @@ -0,0 +1,239 @@ + +; ===== Sequence theory for type TYPENAME ===== + +(declare-sort Seq 0) + +(declare-fun Seq_length (Seq) Int) +(declare-const Seq_empty Seq) +(declare-fun Seq_singleton (TYPENAME) Seq) +(declare-fun Seq_build (Seq TYPENAME) Seq) +(declare-fun Seq_index (Seq Int) TYPENAME) +(declare-fun Seq_append (Seq Seq) Seq) +(declare-fun Seq_update (Seq Int TYPENAME) Seq) +(declare-fun Seq_contains (Seq TYPENAME) Bool) +(declare-fun Seq_take (Seq Int) Seq) +(declare-fun Seq_drop (Seq Int) Seq) +(declare-fun Seq_equal (Seq Seq) Bool) +(declare-fun Seq_sameuntil (Seq Seq Int) Bool) + +(assert (forall ((s Seq)) (! + (<= 0 (Seq_length s)) + :pattern ((Seq_length s)) + :qid |$Seq[TYPENAME]_prog.seq_length_non_negative|))) +(assert (= (Seq_length (as Seq_empty Seq)) 0)) +(assert (forall ((s Seq)) (! + (=> (= (Seq_length s) 0) (= s (as Seq_empty Seq))) + :pattern ((Seq_length s)) + :qid |$Seq[TYPENAME]_prog.only_empty_seq_length_zero|))) +(assert (forall ((e TYPENAME)) (! + (= (Seq_length (Seq_singleton e)) 1) + :pattern ((Seq_length (Seq_singleton e))) + :qid |$Seq[TYPENAME]_prog.length_singleton_seq|))) +(assert (forall ((s Seq) (e TYPENAME)) (! + (= (Seq_length (Seq_build s e)) (+ 1 (Seq_length s))) + :pattern ((Seq_length (Seq_build s e))) + :qid |$Seq[TYPENAME]_prog.length_seq_build_inc_by_one|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME)) (! + (ite + (= i (Seq_length s)) + (= (Seq_index (Seq_build s e) i) e) + (= (Seq_index (Seq_build s e) i) (Seq_index s i))) + :pattern ((Seq_index (Seq_build s e) i)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_build|))) +(assert (forall ((s1 Seq) (s2 Seq)) (! + (=> + (and + (not (= s1 (as Seq_empty Seq))) + (not (= s2 (as Seq_empty Seq)))) + (= (Seq_length (Seq_append s1 s2)) (+ (Seq_length s1) (Seq_length s2)))) + :pattern ((Seq_length (Seq_append s1 s2))) + :qid |$Seq[TYPENAME]_prog.seq_length_over_append|))) +(assert (forall ((e TYPENAME)) (! + (= (Seq_index (Seq_singleton e) 0) e) + :pattern ((Seq_singleton e)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_singleton|))) +(assert (forall ((e1 TYPENAME) (e2 TYPENAME)) (! + (= (Seq_contains (Seq_singleton e1) e2) (= e1 e2)) + :pattern ((Seq_contains (Seq_singleton e1) e2)) + :qid |$Seq[TYPENAME]_prog.seq_contains_over_singleton|))) +(assert (forall ((s Seq)) (! + (= (Seq_append (as Seq_empty Seq) s) s) + :pattern ((Seq_append (as Seq_empty Seq) s)) + :qid |$Seq[TYPENAME]_prog.seq_append_empty_left|))) +(assert (forall ((s Seq)) (! + (= (Seq_append s (as Seq_empty Seq)) s) + :pattern ((Seq_append s (as Seq_empty Seq))) + :qid |$Seq[TYPENAME]_prog.seq_append_empty_right|))) +(assert (forall ((s1 Seq) (s2 Seq) (i Int)) (! + (=> + (and + (not (= s1 (as Seq_empty Seq))) + (not (= s2 (as Seq_empty Seq)))) + (ite + (< i (Seq_length s1)) + (= (Seq_index (Seq_append s1 s2) i) (Seq_index s1 i)) + (= (Seq_index (Seq_append s1 s2) i) (Seq_index s2 (- i (Seq_length s1)))))) + :pattern ((Seq_index (Seq_append s1 s2) i)) + :pattern ((Seq_index s1 i) (Seq_append s1 s2)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_append|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME)) (! + (=> + (and (<= 0 i) (< i (Seq_length s))) + (= (Seq_length (Seq_update s i e)) (Seq_length s))) + :pattern ((Seq_length (Seq_update s i e))) + :qid |$Seq[TYPENAME]_prog.seq_length_invariant_over_update|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME) (j Int)) (! + (ite + (=> (and (<= 0 i) (< i (Seq_length s))) (= i j)) + (= (Seq_index (Seq_update s i e) j) e) + (= (Seq_index (Seq_update s i e) j) (Seq_index s j))) + :pattern ((Seq_index (Seq_update s i e) j)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_update|))) +(assert (forall ((s Seq) (e TYPENAME)) (! + (= + (Seq_contains s e) + (exists ((i Int)) (! + (and (<= 0 i) (and (< i (Seq_length s)) (= (Seq_index s i) e))) + :pattern ((Seq_index s i)) + ))) + :pattern ((Seq_contains s e)) + :qid |$Seq[TYPENAME]_prog.seq_element_contains_index_exists|))) +(assert (forall ((e TYPENAME)) (! + (not (Seq_contains (as Seq_empty Seq) e)) + :pattern ((Seq_contains (as Seq_empty Seq) e)) + :qid |$Seq[TYPENAME]_prog.empty_seq_contains_nothing|))) +(assert (forall ((s1 Seq) (s2 Seq) (e TYPENAME)) (! + (= + (Seq_contains (Seq_append s1 s2) e) + (or (Seq_contains s1 e) (Seq_contains s2 e))) + :pattern ((Seq_contains (Seq_append s1 s2) e)) + :qid |$Seq[TYPENAME]_prog.seq_contains_over_append|))) +(assert (forall ((s Seq) (e1 TYPENAME) (e2 TYPENAME)) (! + (= (Seq_contains (Seq_build s e1) e2) (or (= e1 e2) (Seq_contains s e2))) + :pattern ((Seq_contains (Seq_build s e1) e2)) + :qid |$Seq[TYPENAME]_prog.seq_contains_over_build|))) +(assert (forall ((s Seq) (n Int)) (! + (=> (<= n 0) (= (Seq_take s n) (as Seq_empty Seq))) + :pattern ((Seq_take s n)) + :qid |$Seq[TYPENAME]_prog.seq_take_negative_length|))) +(assert (forall ((s Seq) (n Int) (e TYPENAME)) (! + (= + (Seq_contains (Seq_take s n) e) + (exists ((i Int)) (! + (and + (<= 0 i) + (and (< i n) (and (< i (Seq_length s)) (= (Seq_index s i) e)))) + :pattern ((Seq_index s i)) + ))) + :pattern ((Seq_contains (Seq_take s n) e)) + :qid |$Seq[TYPENAME]_prog.seq_contains_over_take_index_exists|))) +(assert (forall ((s Seq) (n Int)) (! + (=> (<= n 0) (= (Seq_drop s n) s)) + :pattern ((Seq_drop s n)) + :qid |$Seq[TYPENAME]_prog.seq_drop_negative_length|))) +(assert (forall ((s Seq) (n Int) (e TYPENAME)) (! + (= + (Seq_contains (Seq_drop s n) e) + (exists ((i Int)) (! + (and + (<= 0 i) + (and (<= n i) (and (< i (Seq_length s)) (= (Seq_index s i) e)))) + :pattern ((Seq_index s i)) + ))) + :pattern ((Seq_contains (Seq_drop s n) e)) + :qid |$Seq[TYPENAME]_prog.seq_contains_over_drop_index_exists|))) +(assert (forall ((s1 Seq) (s2 Seq)) (! + (= + (Seq_equal s1 s2) + (and + (= (Seq_length s1) (Seq_length s2)) + (forall ((i Int)) (! + (=> + (and (<= 0 i) (< i (Seq_length s1))) + (= (Seq_index s1 i) (Seq_index s2 i))) + :pattern ((Seq_index s1 i)) + :pattern ((Seq_index s2 i)) + )))) + :pattern ((Seq_equal s1 s2)) + :qid |$Seq[TYPENAME]_prog.extensional_seq_equality|))) +(assert (forall ((s1 Seq) (s2 Seq)) (! + (=> (Seq_equal s1 s2) (= s1 s2)) + :pattern ((Seq_equal s1 s2)) + :qid |$Seq[TYPENAME]_prog.seq_equality_identity|))) +(assert (forall ((s1 Seq) (s2 Seq) (n Int)) (! + (= + (Seq_sameuntil s1 s2 n) + (forall ((i Int)) (! + (=> (and (<= 0 i) (< i n)) (= (Seq_index s1 i) (Seq_index s2 i))) + :pattern ((Seq_index s1 i)) + :pattern ((Seq_index s2 i)) + ))) + :pattern ((Seq_sameuntil s1 s2 n)) + :qid |$Seq[TYPENAME]_prog.extensional_seq_equality_prefix|))) +(assert (forall ((s Seq) (n Int)) (! + (=> + (<= 0 n) + (ite + (<= n (Seq_length s)) + (= (Seq_length (Seq_take s n)) n) + (= (Seq_length (Seq_take s n)) (Seq_length s)))) + :pattern ((Seq_length (Seq_take s n))) + :qid |$Seq[TYPENAME]_prog.seq_length_over_take|))) +(assert (forall ((s Seq) (n Int) (i Int)) (! + (=> + (and (<= 0 i) (and (< i n) (< i (Seq_length s)))) + (= (Seq_index (Seq_take s n) i) (Seq_index s i))) + :pattern ((Seq_index (Seq_take s n) i)) + :pattern ((Seq_index s i) (Seq_take s n)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_take|))) +(assert (forall ((s Seq) (n Int)) (! + (=> + (<= 0 n) + (ite + (<= n (Seq_length s)) + (= (Seq_length (Seq_drop s n)) (- (Seq_length s) n)) + (= (Seq_length (Seq_drop s n)) 0))) + :pattern ((Seq_length (Seq_drop s n))) + :qid |$Seq[TYPENAME]_prog.seq_length_over_drop|))) +(assert (forall ((s Seq) (n Int) (i Int)) (! + (=> + (and (<= 0 n) (and (<= 0 i) (< i (- (Seq_length s) n)))) + (= (Seq_index (Seq_drop s n) i) (Seq_index s (+ i n)))) + :pattern ((Seq_index (Seq_drop s n) i)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_drop_1|))) +(assert (forall ((s Seq) (n Int) (i Int)) (! + (=> + (and (<= 0 n) (and (<= n i) (< i (Seq_length s)))) + (= (Seq_index (Seq_drop s n) (- i n)) (Seq_index s i))) + :pattern ((Seq_index s i) (Seq_drop s n)) + :qid |$Seq[TYPENAME]_prog.seq_index_over_drop_2|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME) (n Int)) (! + (=> + (and (<= 0 i) (and (< i n) (< n (Seq_length s)))) + (= (Seq_take (Seq_update s i e) n) (Seq_update (Seq_take s n) i e))) + :pattern ((Seq_take (Seq_update s i e) n)) + :qid |$Seq[TYPENAME]_prog.seq_take_over_update_1|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME) (n Int)) (! + (=> + (and (<= n i) (< i (Seq_length s))) + (= (Seq_take (Seq_update s i e) n) (Seq_take s n))) + :pattern ((Seq_take (Seq_update s i e) n)) + :qid |$Seq[TYPENAME]_prog.seq_take_over_update_2|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME) (n Int)) (! + (=> + (and (<= 0 n) (and (<= n i) (< i (Seq_length s)))) + (= (Seq_drop (Seq_update s i e) n) (Seq_update (Seq_drop s n) (- i n) e))) + :pattern ((Seq_drop (Seq_update s i e) n)) + :qid |$Seq[TYPENAME]_prog.seq_drop_over_update_1|))) +(assert (forall ((s Seq) (i Int) (e TYPENAME) (n Int)) (! + (=> + (and (<= 0 i) (and (< i n) (< n (Seq_length s)))) + (= (Seq_drop (Seq_update s i e) n) (Seq_drop s n))) + :pattern ((Seq_drop (Seq_update s i e) n)) + :qid |$Seq[TYPENAME]_prog.seq_drop_over_update_2|))) +(assert (forall ((s Seq) (e TYPENAME) (n Int)) (! + (=> + (and (<= 0 n) (<= n (Seq_length s))) + (= (Seq_drop (Seq_build s e) n) (Seq_build (Seq_drop s n) e))) + :pattern ((Seq_drop (Seq_build s e) n)) + :qid |$Seq[TYPENAME]_prog.seq_drop_over_build|))) \ No newline at end of file diff --git a/native-verifier/src/theories/Set.smt2 b/native-verifier/src/theories/Set.smt2 new file mode 100644 index 00000000000..58dc901da2a --- /dev/null +++ b/native-verifier/src/theories/Set.smt2 @@ -0,0 +1,163 @@ + +; ===== Set theory for type TYPENAME ===== + +(declare-sort Set 0) + +(declare-fun Set_in (TYPENAME Set) Bool) +(declare-fun Set_card (Set) Int) +(declare-const Set_empty Set) +(declare-fun Set_singleton (TYPENAME) Set) +(declare-fun Set_unionone (Set TYPENAME) Set) +(declare-fun Set_union (Set Set) Set) +(declare-fun Set_disjoint (Set Set) Bool) +(declare-fun Set_difference (Set Set) Set) +(declare-fun Set_intersection (Set Set) Set) +(declare-fun Set_subset (Set Set) Bool) +(declare-fun Set_equal (Set Set) Bool) + +(assert (forall ((s Set)) (! + (<= 0 (Set_card s)) + :pattern ((Set_card s)) + :qid |$Set[TYPENAME]_prog.card_non_negative|))) +(assert (forall ((e TYPENAME)) (! + (not (Set_in e (as Set_empty Set))) + :pattern ((Set_in e (as Set_empty Set))) + :qid |$Set[TYPENAME]_prog.in_empty_set|))) +(assert (forall ((s Set)) (! + (and + (= (= (Set_card s) 0) (= s (as Set_empty Set))) + (=> + (not (= (Set_card s) 0)) + (exists ((e TYPENAME)) (! + (Set_in e s) + :pattern ((Set_in e s)) + )))) + :pattern ((Set_card s)) + :qid |$Set[TYPENAME]_prog.empty_set_cardinality|))) +(assert (forall ((e TYPENAME)) (! + (Set_in e (Set_singleton e)) + :pattern ((Set_singleton e)) + :qid |$Set[TYPENAME]_prog.in_singleton_set|))) +(assert (forall ((e1 TYPENAME) (e2 TYPENAME)) (! + (= (Set_in e1 (Set_singleton e2)) (= e1 e2)) + :pattern ((Set_in e1 (Set_singleton e2))) + :qid |$Set[TYPENAME]_prog.in_singleton_set_equality|))) +(assert (forall ((e TYPENAME)) (! + (= (Set_card (Set_singleton e)) 1) + :pattern ((Set_card (Set_singleton e))) + :qid |$Set[TYPENAME]_prog.singleton_set_cardinality|))) +(assert (forall ((s Set) (e TYPENAME)) (! + (Set_in e (Set_unionone s e)) + :pattern ((Set_unionone s e)) + :qid |$Set[TYPENAME]_prog.in_unionone_same|))) +(assert (forall ((s Set) (e1 TYPENAME) (e2 TYPENAME)) (! + (= (Set_in e1 (Set_unionone s e2)) (or (= e1 e2) (Set_in e1 s))) + :pattern ((Set_in e1 (Set_unionone s e2))) + :qid |$Set[TYPENAME]_prog.in_unionone_other|))) +(assert (forall ((s Set) (e1 TYPENAME) (e2 TYPENAME)) (! + (=> (Set_in e1 s) (Set_in e1 (Set_unionone s e2))) + :pattern ((Set_in e1 s) (Set_unionone s e2)) + :qid |$Set[TYPENAME]_prog.invariance_in_unionone|))) +(assert (forall ((s Set) (e TYPENAME)) (! + (=> (Set_in e s) (= (Set_card (Set_unionone s e)) (Set_card s))) + :pattern ((Set_card (Set_unionone s e))) + :qid |$Set[TYPENAME]_prog.unionone_cardinality_invariant|))) +(assert (forall ((s Set) (e TYPENAME)) (! + (=> (not (Set_in e s)) (= (Set_card (Set_unionone s e)) (+ (Set_card s) 1))) + :pattern ((Set_card (Set_unionone s e))) + :qid |$Set[TYPENAME]_prog.unionone_cardinality_changed|))) +(assert (forall ((s1 Set) (s2 Set) (e TYPENAME)) (! + (= (Set_in e (Set_union s1 s2)) (or (Set_in e s1) (Set_in e s2))) + :pattern ((Set_in e (Set_union s1 s2))) + :qid |$Set[TYPENAME]_prog.in_union_in_one|))) +(assert (forall ((s1 Set) (s2 Set) (e TYPENAME)) (! + (=> (Set_in e s1) (Set_in e (Set_union s1 s2))) + :pattern ((Set_in e s1) (Set_union s1 s2)) + :qid |$Set[TYPENAME]_prog.in_left_in_union|))) +(assert (forall ((s1 Set) (s2 Set) (e TYPENAME)) (! + (=> (Set_in e s2) (Set_in e (Set_union s1 s2))) + :pattern ((Set_in e s2) (Set_union s1 s2)) + :qid |$Set[TYPENAME]_prog.in_right_in_union|))) +(assert (forall ((s1 Set) (s2 Set) (e TYPENAME)) (! + (= (Set_in e (Set_intersection s1 s2)) (and (Set_in e s1) (Set_in e s2))) + :pattern ((Set_in e (Set_intersection s1 s2))) + :pattern ((Set_intersection s1 s2) (Set_in e s1)) + :pattern ((Set_intersection s1 s2) (Set_in e s2)) + :qid |$Set[TYPENAME]_prog.in_intersection_in_both|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= (Set_union s1 (Set_union s1 s2)) (Set_union s1 s2)) + :pattern ((Set_union s1 (Set_union s1 s2))) + :qid |$Set[TYPENAME]_prog.union_left_idempotency|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= (Set_union (Set_union s1 s2) s2) (Set_union s1 s2)) + :pattern ((Set_union (Set_union s1 s2) s2)) + :qid |$Set[TYPENAME]_prog.union_right_idempotency|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= (Set_intersection s1 (Set_intersection s1 s2)) (Set_intersection s1 s2)) + :pattern ((Set_intersection s1 (Set_intersection s1 s2))) + :qid |$Set[TYPENAME]_prog.intersection_left_idempotency|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= (Set_intersection (Set_intersection s1 s2) s2) (Set_intersection s1 s2)) + :pattern ((Set_intersection (Set_intersection s1 s2) s2)) + :qid |$Set[TYPENAME]_prog.intersection_right_idempotency|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= + (+ (Set_card (Set_union s1 s2)) (Set_card (Set_intersection s1 s2))) + (+ (Set_card s1) (Set_card s2))) + :pattern ((Set_card (Set_union s1 s2))) + :pattern ((Set_card (Set_intersection s1 s2))) + :qid |$Set[TYPENAME]_prog.cardinality_sums|))) +(assert (forall ((s1 Set) (s2 Set) (e TYPENAME)) (! + (= (Set_in e (Set_difference s1 s2)) (and (Set_in e s1) (not (Set_in e s2)))) + :pattern ((Set_in e (Set_difference s1 s2))) + :qid |$Set[TYPENAME]_prog.in_difference|))) +(assert (forall ((s1 Set) (s2 Set) (e TYPENAME)) (! + (=> (Set_in e s2) (not (Set_in e (Set_difference s1 s2)))) + :pattern ((Set_difference s1 s2) (Set_in e s2)) + :qid |$Set[TYPENAME]_prog.not_in_difference|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= + (Set_subset s1 s2) + (forall ((e TYPENAME)) (! + (=> (Set_in e s1) (Set_in e s2)) + :pattern ((Set_in e s1)) + :pattern ((Set_in e s2)) + ))) + :pattern ((Set_subset s1 s2)) + :qid |$Set[TYPENAME]_prog.subset_definition|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= + (Set_equal s1 s2) + (forall ((e TYPENAME)) (! + (= (Set_in e s1) (Set_in e s2)) + :pattern ((Set_in e s1)) + :pattern ((Set_in e s2)) + ))) + :pattern ((Set_equal s1 s2)) + :qid |$Set[TYPENAME]_prog.equality_definition|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (=> (Set_equal s1 s2) (= s1 s2)) + :pattern ((Set_equal s1 s2)) + :qid |$Set[TYPENAME]_prog.native_equality|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (= + (Set_disjoint s1 s2) + (forall ((e TYPENAME)) (! + (or (not (Set_in e s1)) (not (Set_in e s2))) + :pattern ((Set_in e s1)) + :pattern ((Set_in e s2)) + ))) + :pattern ((Set_disjoint s1 s2)) + :qid |$Set[TYPENAME]_prog.disjointness_definition|))) +(assert (forall ((s1 Set) (s2 Set)) (! + (and + (= + (+ + (+ (Set_card (Set_difference s1 s2)) (Set_card (Set_difference s2 s1))) + (Set_card (Set_intersection s1 s2))) + (Set_card (Set_union s1 s2))) + (= + (Set_card (Set_difference s1 s2)) + (- (Set_card s1) (Set_card (Set_intersection s1 s2))))) + :pattern ((Set_card (Set_difference s1 s2))) + :qid |$Set[TYPENAME]_prog.cardinality_difference|))) diff --git a/native-verifier/src/theory_provider.rs b/native-verifier/src/theory_provider.rs new file mode 100644 index 00000000000..2423d8818a5 --- /dev/null +++ b/native-verifier/src/theory_provider.rs @@ -0,0 +1,36 @@ +pub struct ContainerTheoryProvider<'a> { + template: &'a str, +} + +impl ContainerTheoryProvider<'_> { + pub fn new(theory: &str) -> Self { + let template = match theory { + "Set" => include_str!("theories/Set.smt2"), + "MultiSet" => include_str!("theories/MultiSet.smt2"), + "Seq" => include_str!("theories/Seq.smt2"), + _ => panic!("Theory {} not supported", theory), + }; + Self { template } + } + + pub fn get_theory(&self, element_type: &str) -> String { + self.template.replace("TYPENAME", element_type) + } +} + +pub struct MapTheoryProvider<'a> { + template: &'a str, +} + +impl MapTheoryProvider<'_> { + pub fn new() -> Self { + let template = include_str!("theories/Map.smt2"); + Self { template } + } + + pub fn get_theory(&self, key_type: &str, value_type: &str) -> String { + self.template + .replace("KEYTYPE", key_type) + .replace("VALUETYPE", value_type) + } +} diff --git a/native-verifier/src/verifier.rs b/native-verifier/src/verifier.rs new file mode 100644 index 00000000000..074428a7923 --- /dev/null +++ b/native-verifier/src/verifier.rs @@ -0,0 +1,150 @@ +// © 2022, Jakub Janaszkiewicz +// +// This Source Code Form is subject to the terms of the Mozilla Public +// License, v. 2.0. If a copy of the MPL was not distributed with this +// file, You can obtain one at http://mozilla.org/MPL/2.0/. + +use crate::smt_lib::*; +use backend_common::{VerificationError, VerificationResult}; +use core::panic; +use lazy_static::lazy_static; +use log::{self, debug}; +use prusti_common::vir::program::Program; +use prusti_utils::{config, report::log::report_with_writer, run_timed}; +use regex::Regex; +use std::{ + error::Error, + io::Write, + process::{Command, Stdio}, +}; + +// lazy regex for parsing z3 output +lazy_static! { + static ref POSITION_REGEX: Regex = + Regex::new(r#"^"?position: (\d+)(?:, reason: (\d+))?"?"#).unwrap(); +} + +pub struct Verifier { + smt_solver_exe: String, +} + +impl Verifier { + pub fn new(z3_exe: String) -> Self { + Self { + smt_solver_exe: z3_exe, + } + } + + pub fn verify(&mut self, program: &Program) -> VerificationResult { + let Program::Low(program) = program else { + panic!("Lithium backend only supports low programs"); + }; + + if !config::unsafe_core_proof() { + panic!("Lithium backend only supports unsafe_core_proof=true"); + } + + let is_z3 = self.smt_solver_exe.ends_with("z3"); + let solver_name = if is_z3 { "Z3" } else { "CVC5" }; + + let program_name = prusti_common::report::log::to_legal_file_name(&program.name); + let program_name = format!("{}.smt2", program_name); // TODO: path mismatch when over config length + + run_timed!("Translation to SMT-LIB", debug, + let mut smt = SMTLib::new(is_z3); + program.build_smt(&mut smt); + let smt_program = smt.to_string(); + + report_with_writer( + "smt", + program_name.clone(), + |writer| { + writer.write_all(smt_program.as_bytes()).unwrap(); + }, + ); + ); + + run_timed!(format!("SMT verification with {}", solver_name), debug, + let result: Result> = try { + let mut command = Command::new(self.smt_solver_exe.clone()); + + let path = config::log_dir().join("smt").join(program_name); + let path = path.to_str().unwrap(); + + if is_z3 { + command.args(["-smt2", path]); + } else { + command.args(["--incremental", path]); + } + + let mut child = command.stderr(Stdio::piped()) + .stdout(Stdio::piped()) + .spawn()?; + + // Check if child process is running + let child_status = child.try_wait()?; + if let Some(exit_status) = child_status { + if exit_status.success() { + Err::("Child process terminated prematurely.".into())?; + } else { + let err = format!("Child process failed to start with exit status: {}", exit_status); + Err::(err)?; + } + } + + let output = child.wait_with_output()?; + + if output.status.success() { + String::from_utf8(output.stdout)? + } else { + let err = String::from_utf8(output.stdout)?; + + // only lines that contain "error" are actual errors + let err = err.lines().filter(|line| line.contains("error")).collect::>().join("\n"); + + Err(err)? + } + }; + ); + + let mut errors = vec![]; + + // TODO: Actual unexpected error handling + if let Err(err) = result { + errors.push(VerificationError::new( + "assert.failed:assertion.false".to_string(), + Some("0".to_string()), + Some("0".to_string()), + Some("0".to_string()), + format!("{} failed with unexpected error: {}", solver_name, err), + None, + )); + + return VerificationResult::Failure(errors); + } + + let mut last_pos: (i32, Option) = (0, None); + for line in result.unwrap().lines() { + if let Some(caps) = POSITION_REGEX.captures(line) { + let pos = caps[1].parse().unwrap(); + let res = caps.get(2).map(|r| r.as_str().parse().unwrap()); + last_pos = (pos, res); + } else if line == "sat" || line == "unknown" { + errors.push(VerificationError::new( + "assert.failed:assertion.false".to_string(), + Some("0".to_string()), + Some(last_pos.0.to_string()), + last_pos.1.map(|r| r.to_string()), + "Assert might fail. Assertion might not hold.".to_string(), + None, + )); + } + } + + if errors.is_empty() { + VerificationResult::Success + } else { + VerificationResult::Failure(errors) + } + } +} diff --git a/prusti-common/Cargo.toml b/prusti-common/Cargo.toml index a27a0f9dc2e..6d5f99e7dca 100644 --- a/prusti-common/Cargo.toml +++ b/prusti-common/Cargo.toml @@ -10,6 +10,7 @@ doctest = false # we have no doc tests [dependencies] prusti-utils = { path = "../prusti-utils" } viper = { path = "../viper" } +backend-common = { path = "../backend-common" } vir = { path = "../vir" } log = { version = "0.4", features = ["release_max_level_info"] } config = "0.13" diff --git a/prusti-common/src/vir/low_to_viper/ast.rs b/prusti-common/src/vir/low_to_viper/ast.rs index 6e56e887b01..933a6330bbe 100644 --- a/prusti-common/src/vir/low_to_viper/ast.rs +++ b/prusti-common/src/vir/low_to_viper/ast.rs @@ -287,6 +287,8 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for expression::Constant { expression::ConstantValue::Int(value) => { ast.int_lit_with_pos(*value, self.position.to_viper(context, ast)) } + expression::ConstantValue::Float32(_) => unimplemented!("Float32 to Viper"), + expression::ConstantValue::Float64(_) => unimplemented!("Float64 to Viper"), expression::ConstantValue::BigInt(value) => { ast.int_lit_from_ref_with_pos(value, self.position.to_viper(context, ast)) } @@ -308,7 +310,9 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for expression::Constant { Type::Map(_) => unimplemented!(), Type::Ref => unimplemented!(), Type::Perm => match &self.value { - expression::ConstantValue::Bool(_) => { + expression::ConstantValue::Float32(_) + | expression::ConstantValue::Float64(_) + | expression::ConstantValue::Bool(_) => { unreachable!() } expression::ConstantValue::Int(value) => match value { diff --git a/prusti-common/src/vir/program_normalization.rs b/prusti-common/src/vir/program_normalization.rs index 5420e9c3635..d5425cb40b7 100644 --- a/prusti-common/src/vir/program_normalization.rs +++ b/prusti-common/src/vir/program_normalization.rs @@ -5,9 +5,9 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::vir::{program::Program, Position}; +use backend_common::VerificationResult; use log::{debug, trace}; use rustc_hash::{FxHashMap, FxHashSet}; -use viper::VerificationResult; pub enum NormalizationInfo { LegacyProgram { original_position_ids: Vec }, diff --git a/prusti-common/src/vir/to_viper.rs b/prusti-common/src/vir/to_viper.rs index 568d04489ad..505749fb41c 100644 --- a/prusti-common/src/vir/to_viper.rs +++ b/prusti-common/src/vir/to_viper.rs @@ -455,6 +455,19 @@ impl<'v> ToViper<'v, viper::Expr<'v>> for Expr { Float::F32 => viper::FloatSizeViper::F32, Float::F64 => viper::FloatSizeViper::F64, }; + + if *op == BinaryOpKind::NeCmp { + return ast.not_with_pos( + ast.float_binop( + viper::BinOpFloat::Eq, + size, + left.to_viper(context, ast), + right.to_viper(context, ast), + ), + pos.to_viper(context, ast), + ); + } + let float_op_kind = match op { BinaryOpKind::Add => viper::BinOpFloat::Add, BinaryOpKind::Sub => viper::BinOpFloat::Sub, diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml index 6fb906a0a10..851f728d0fb 100644 --- a/prusti-server/Cargo.toml +++ b/prusti-server/Cargo.toml @@ -21,6 +21,8 @@ log = { version = "0.4", features = ["release_max_level_info"] } viper = { path = "../viper" } prusti-common = { path = "../prusti-common" } prusti-utils = { path = "../prusti-utils" } +native-verifier = { path = "../native-verifier" } +backend-common = { path = "../backend-common" } tracing = { path = "../tracing" } env_logger = "0.10" clap = { version = "4.0", features = ["derive"] } diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs index 5a36ad6c399..6841563c2ea 100644 --- a/prusti-server/src/backend.rs +++ b/prusti-server/src/backend.rs @@ -1,13 +1,15 @@ use crate::dump_viper_program; +use backend_common::VerificationResult; use prusti_common::{ config, vir::{LoweringContext, ToViper}, Stopwatch, }; -use viper::{VerificationContext, VerificationResult}; +use viper::VerificationContext; pub enum Backend<'a> { Viper(viper::Verifier<'a>, &'a VerificationContext<'a>), + Lithium(native_verifier::Verifier), } impl<'a> Backend<'a> { @@ -36,6 +38,10 @@ impl<'a> Backend<'a> { viper.verify(viper_program) }) } + Backend::Lithium(lithium) => { + let _stopwatch = Stopwatch::start("prusti-server", "vir verification"); + lithium.verify(program) + } } } } diff --git a/prusti-server/src/client.rs b/prusti-server/src/client.rs index d1b53ea63bf..c5bd69b7ddb 100644 --- a/prusti-server/src/client.rs +++ b/prusti-server/src/client.rs @@ -5,10 +5,10 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::VerificationRequest; +use backend_common::VerificationResult; use prusti_common::config; use reqwest::Client; use url::{ParseError, Url}; -use viper::VerificationResult; pub struct PrustiClient { client: Client, diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs index 446407c5087..dab28e2f6ce 100644 --- a/prusti-server/src/process_verification.rs +++ b/prusti-server/src/process_verification.rs @@ -5,6 +5,7 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::{Backend, VerificationRequest, ViperBackendConfig}; +use backend_common::VerificationResult; use log::info; use once_cell::sync::Lazy; use prusti_common::{ @@ -14,16 +15,14 @@ use prusti_common::{ Stopwatch, }; use std::{fs::create_dir_all, path::PathBuf}; -use viper::{ - smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext, VerificationResult, -}; +use viper::{smt_manager::SmtManager, Cache, VerificationBackend, VerificationContext}; #[tracing::instrument(level = "debug", skip_all, fields(program = %request.program.get_name()))] pub fn process_verification_request<'v, 't: 'v>( verification_context: &'v Lazy, impl Fn() -> VerificationContext<'t>>, mut request: VerificationRequest, cache: impl Cache, -) -> viper::VerificationResult { +) -> VerificationResult { let ast_utils = verification_context.new_ast_utils(); // Only for testing: Check that the normalization is reversible. @@ -78,7 +77,7 @@ pub fn process_verification_request<'v, 't: 'v>( let _ = build_or_dump_viper_program(); }); } - return viper::VerificationResult::Success; + return VerificationResult::Success; } // Early return in case of cache hit @@ -112,6 +111,10 @@ pub fn process_verification_request<'v, 't: 'v>( ), verification_context, ), + VerificationBackend::Lithium => { + Backend::Lithium(native_verifier::Verifier::new(config::smt_solver_path())) + // TODO: SMT Wrapper support + } }; stopwatch.start_next("backend verification"); @@ -170,6 +173,7 @@ fn new_viper_verifier<'v, 't: 'v>( format!("/logPrefix {log_dir_str}"), //"--print".to_string(), "./log/boogie_program/program.bpl".to_string(), ]), + VerificationBackend::Lithium => unreachable!("Lithium is not a Viper backend"), } } else { report_path = None; diff --git a/prusti-server/src/verification_request.rs b/prusti-server/src/verification_request.rs index f5b0b75919c..4dda17c32c2 100644 --- a/prusti-server/src/verification_request.rs +++ b/prusti-server/src/verification_request.rs @@ -77,6 +77,9 @@ impl ViperBackendConfig { VerificationBackend::Carbon => { verifier_args.extend(vec!["--disableAllocEncoding".to_string()]); } + VerificationBackend::Lithium => { + // TODO: add lithium-specific arguments + } } Self { backend, diff --git a/prusti-server/tests/basic_requests.rs b/prusti-server/tests/basic_requests.rs index edb7aca6768..f63a87e5d2b 100644 --- a/prusti-server/tests/basic_requests.rs +++ b/prusti-server/tests/basic_requests.rs @@ -1,10 +1,10 @@ +use backend_common::VerificationResult; use lazy_static::lazy_static; use prusti_common::vir::*; use prusti_server::{ spawn_server_thread, tokio::runtime::Builder, PrustiClient, VerificationRequest, ViperBackendConfig, }; -use viper::VerificationResult; lazy_static! { // only start the jvm & server once diff --git a/prusti-tests/tests/verify/fail/native/arithmetic.rs b/prusti-tests/tests/verify/fail/native/arithmetic.rs new file mode 100644 index 00000000000..68e62a77586 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/arithmetic.rs @@ -0,0 +1,7 @@ +// compile-flags: -Pviper_backend=Lithium + +fn test(m: i32, c: i32, d: i32) { + assert!(m * c - m * d == m * (c - d + 1)); //~ ERROR might not hold +} + +fn main() {} diff --git a/prusti-tests/tests/verify/fail/native/assert-seq.rs b/prusti-tests/tests/verify/fail/native/assert-seq.rs new file mode 100644 index 00000000000..6bb24a51743 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/assert-seq.rs @@ -0,0 +1,6 @@ +// compile-flags: -Pviper_backend=Lithium + +fn main() { + assert!(true); + assert!(false); //~ ERROR might not hold +} diff --git a/prusti-tests/tests/verify/fail/native/floating-point.rs b/prusti-tests/tests/verify/fail/native/floating-point.rs new file mode 100644 index 00000000000..3a06fe9f66f --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/floating-point.rs @@ -0,0 +1,140 @@ +// compile-flags: -Pviper_backend=Lithium + +use prusti_contracts::*; + +#[pure] +#[terminates] +fn is_nan_32(f: f32) -> bool { + f != f +} + +#[pure] +#[terminates] +fn is_nan_64(f: f64) -> bool { + f != f +} + +#[pure] +#[terminates] +fn is_infinite_32(f: f32) -> bool { + f == f32::INFINITY || f == f32::NEG_INFINITY +} + +#[pure] +#[terminates] +fn is_infinite_64(f: f64) -> bool { + f == f64::INFINITY || f == f64::NEG_INFINITY +} + +fn test_nan_32_is_nan() { + let a = 0.0f32 / 0.0f32; + assert!(is_nan_32(a)); +} + +fn test_nan_32_is_inf() { + let a = 0.0f32 / 0.0f32; + assert!(is_infinite_32(a)); //~ ERROR might not hold +} + +fn test_nan_64_is_nan() { + let a = 0.0f64 / 0.0f64; + assert!(is_nan_64(a)); +} + +fn test_nan_64_is_inf() { + let a = 0.0f64 / 0.0f64; + assert!(is_infinite_64(a)); //~ ERROR might not hold +} + +fn test_inf_32_is_inf() { + let a = 1.0f32 / 0.0f32; + assert!(is_infinite_32(a)); +} + +fn test_inf_32_is_nan() { + let a = 1.0f32 / 0.0f32; + assert!(is_nan_32(a)); //~ ERROR might not hold +} + +fn test_inf_64_is_inf() { + let a = 1.0f64 / 0.0f64; + assert!(is_infinite_64(a)); +} + +fn test_inf_64_is_nan() { + let a = 1.0f64 / 0.0f64; + assert!(is_nan_64(a)); //~ ERROR might not hold +} + +fn test_neg_inf_32_is_inf() { + let a = -1.0f32 / 0.0f32; + assert!(is_infinite_32(a)); +} + +fn test_neg_inf_32_is_nan() { + let a = -1.0f32 / 0.0f32; + assert!(is_nan_32(a)); //~ ERROR might not hold +} + +fn test_neg_inf_64_is_inf() { + let a = -1.0f64 / 0.0f64; + assert!(is_infinite_64(a)); +} + +fn test_neg_inf_64_is_nan() { + let a = -1.0f64 / 0.0f64; + assert!(is_nan_64(a)); //~ ERROR might not hold +} + +// THEORY OF INIFINITY + +#[requires(is_nan_32(f))] +#[ensures(!is_infinite_32(f))] +fn axiom1(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(!is_nan_32(f))] +fn axiom2(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f + 1_f32))] +fn axiom3(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f - 1_f32))] +fn axiom4(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f * 2_f32))] +fn axiom5(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f / 2_f32))] +fn axiom6(f: f32) {} + +// THEORY OF NAN + +#[requires(is_infinite_32(f))] +#[ensures(!is_nan_32(f))] +fn axiom7(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f + 1_f32))] +fn axiom8(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f - 1_f32))] +fn axiom9(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f * 2_f32))] +fn axiom10(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f / 2_f32))] +fn axiom11(f: f32) {} + +#[ensures(is_nan_32(f32::NAN))] +fn axiom12() {} + +fn main() {} diff --git a/prusti-tests/tests/verify/fail/native/if-else-1.rs b/prusti-tests/tests/verify/fail/native/if-else-1.rs new file mode 100644 index 00000000000..78da16316dd --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/if-else-1.rs @@ -0,0 +1,10 @@ +// compile-flags: -Pviper_backend=Lithium + +fn main() { + let x: i32 = 37; + if x == 17 { + assert!(x == 3); + } else { + assert!(x == 3); //~ ERROR might not hold + } +} diff --git a/prusti-tests/tests/verify/fail/native/if-else-2.rs b/prusti-tests/tests/verify/fail/native/if-else-2.rs new file mode 100644 index 00000000000..2b2a0ab2cad --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/if-else-2.rs @@ -0,0 +1,10 @@ +// compile-flags: -Pviper_backend=Lithium + +fn main() { + let x: i32 = 37; + if x == 37 { + assert!(x == 3); //~ ERROR might not hold + } else { + assert!(x == 3); + } +} diff --git a/prusti-tests/tests/verify/fail/native/quantifier_closures.rs b/prusti-tests/tests/verify/fail/native/quantifier_closures.rs new file mode 100644 index 00000000000..3a0045f3592 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/quantifier_closures.rs @@ -0,0 +1,20 @@ +// compile-flags: -Pviper_backend=Lithium +use prusti_contracts::*; + +#[requires(forall(|x: i32| x * x >= foo * bar))] +fn test_closure_1(foo: i32, bar: i32) -> i32 { + foo + bar + 1 +} + +#[requires(forall(|x: i32| x * x >= foo * bar))] +fn test_closure_2(foo: i32, bar: i32) -> i32 { + foo + bar + 1 +} + +fn main() { + test_closure_1(5, 3); //~ ERROR precondition might not hold + + let arg1 = 1; + let arg2 = 2; + test_closure_2(arg1, arg2); //TODO: error reported here +} diff --git a/prusti-tests/tests/verify/fail/native/structure_quantifiers.rs b/prusti-tests/tests/verify/fail/native/structure_quantifiers.rs new file mode 100644 index 00000000000..456ce4c0732 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/structure_quantifiers.rs @@ -0,0 +1,30 @@ +// compile-flags: -Pviper_backend=Lithium +use prusti_contracts::*; + +pub struct MyStructure {} + +impl MyStructure { + #[pure] + #[terminates] + #[ensures (0 <= result)] + pub fn len(&self) -> i32 { + 17 + } +} + +#[pure] +#[terminates] +#[ensures (0 <= result)] +#[ensures(result == s.len())] +fn len_of(s: &MyStructure) -> i32 { + 17 +} + +#[ensures(forall(|s: MyStructure| s.len() == 3))] //~ ERROR postcondition might not hold +fn test1(min: i32) {} + +#[ensures(forall(|s: MyStructure| len_of(&s) >= 17))] +#[ensures(forall(|s: MyStructure| len_of(&s) >= 18))] //~ ERROR postcondition might not hold +fn test2(min: i32) {} + +fn main() {} diff --git a/prusti-tests/tests/verify/fail/native/switchInt-2.rs b/prusti-tests/tests/verify/fail/native/switchInt-2.rs new file mode 100644 index 00000000000..0abe86c2e30 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/switchInt-2.rs @@ -0,0 +1,20 @@ +// compile-flags: -Pviper_backend=Lithium + +fn test(x: i32) { + match x { + 0..=100 => { + assert!(x >= 0); + assert!(x <= 100); + assert!(x == 7); //~ ERROR might not hold + } + 50 => { + unreachable!(); + } + _ => { + assert!(x != 0); + assert!(x < 0); //~ ERROR might not hold + } + } +} + +fn main() {} diff --git a/prusti-tests/tests/verify/fail/native/switchInt.rs b/prusti-tests/tests/verify/fail/native/switchInt.rs new file mode 100644 index 00000000000..993a0d3475c --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/switchInt.rs @@ -0,0 +1,20 @@ +// compile-flags: -Pviper_backend=Lithium + +fn test(x: i32) { + match x { + 0 => { + assert!(false); //~ ERROR might not hold + } + 1 => { + assert!(false); //~ ERROR might not hold + } + 2 => { + assert!(true); + } + _ => { + assert!(false); //~ ERROR might not hold + } + } +} + +fn main() {} diff --git a/prusti-tests/tests/verify/fail/native/trivial.rs b/prusti-tests/tests/verify/fail/native/trivial.rs new file mode 100644 index 00000000000..7b590083b85 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/trivial.rs @@ -0,0 +1,5 @@ +// compile-flags: -Pviper_backend=Lithium + +fn main() { + assert!(false); //~ ERROR might not hold +} diff --git a/prusti-tests/tests/verify/fail/native/while.rs b/prusti-tests/tests/verify/fail/native/while.rs new file mode 100644 index 00000000000..710e2d521d6 --- /dev/null +++ b/prusti-tests/tests/verify/fail/native/while.rs @@ -0,0 +1,29 @@ +// compile-flags: -Pviper_backend=Lithium + +use prusti_contracts::*; + +const N: i32 = 10; + +#[requires(i <= N)] +#[ensures(result == N)] +fn wrong_invariant(i: i32) -> i32 { + let mut ret = i; + while ret < N { + body_invariant!(ret == i); //~ ERROR loop invariant might not hold + ret += 1; + } + ret +} + +#[requires(i <= N)] +#[ensures(result == N)] //~ ERROR might not hold +fn weak_invariant(i: i32) -> i32 { + let mut ret = i; + while ret < N { + body_invariant!(ret <= N); + ret += 1; + } + ret +} + +fn main() {} diff --git a/prusti-tests/tests/verify/pass/native/ackermann.rs b/prusti-tests/tests/verify/pass/native/ackermann.rs new file mode 100644 index 00000000000..9acb7a7bd56 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/ackermann.rs @@ -0,0 +1,53 @@ +// compile-flags: -Pviper_backend=Lithium + +use prusti_contracts::*; + +#[pure] +#[terminates(trusted)] +#[requires(0 <= m && 0 <= n)] +#[ensures(result >= 0)] +fn ack_pure(m: i64, n: i64) -> i64 { + if m == 0 { + n + 1 + } else if n == 0 { + ack_pure(m - 1, 1) + } else { + ack_pure(m - 1, ack_pure(m, n - 1)) + } +} + +#[requires(0 <= m && 0 <= n)] +#[ensures(result == ack_pure(m, n))] +#[ensures(result >= 0)] +fn ack1(m: i64, n: i64) -> i64 { + if m == 0 { + n + 1 + } else if n == 0 { + ack1(m - 1, 1) + } else { + ack1(m - 1, ack1(m, n - 1)) + } +} + +#[requires(0 <= m && 0 <= n)] +#[ensures(result == ack_pure(m, n))] +#[ensures(result >= 0)] +fn ack2(m: i64, n: i64) -> i64 { + match (m, n) { + (0, n) => n + 1, + (m, 0) => ack2(m - 1, 1), + (m, n) => ack2(m - 1, ack2(m, n - 1)), + } +} + +#[trusted] +fn print_i64(a: i64) { + println!("{}", a); // 125 +} + +fn main() { + let a1 = ack1(3, 4); + let a2 = ack2(3, 4); + assert!(a1 == a2); + print_i64(a1); +} diff --git a/prusti-tests/tests/verify/pass/native/arithmetic.rs b/prusti-tests/tests/verify/pass/native/arithmetic.rs new file mode 100644 index 00000000000..a029a191594 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/arithmetic.rs @@ -0,0 +1,7 @@ +// compile-flags: -Pviper_backend=Lithium + +fn test(m: i32, c: i32, d: i32) { + assert!(m * c - m * d == m * (c - d)); +} + +fn main() {} diff --git a/prusti-tests/tests/verify/pass/native/euclid.rs b/prusti-tests/tests/verify/pass/native/euclid.rs new file mode 100644 index 00000000000..1e59182e6b5 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/euclid.rs @@ -0,0 +1,114 @@ +// compile-flags: -Pviper_backend=Lithium + +use prusti_contracts::*; + +macro_rules! divides_prop { + ($x:expr, $y:expr, $z:expr) => { + $z >= 0 && $x * $z == $y + }; +} + +#[pure] +#[terminates] +#[trusted] +#[requires(x > 0 && y > 0)] +#[ensures(x <= y)] +fn divides(x: i32, y: i32) -> bool { + unimplemented!() +} + +#[pure] +#[terminates] +#[trusted] +#[requires(x > 0 && y > 0)] +#[ensures(result >= 1)] +#[ensures(divides(result, x))] +#[ensures(divides(result, y))] +#[ensures(forall(|z: i32| z >= 1 && divides(z, x) && divides(z, y) ==> z <= result))] +fn gcd(x: i32, y: i32) -> i32 { + if x > y { + gcd(x - y, y) + } else if x < y { + gcd(x, y - x) + } else { + x + } +} + +#[trusted] +#[requires(x > 0 && y > 0)] +#[requires(divides_prop!(x, y, z))] +#[ensures(divides(x, y))] +fn lemma_show_divides(x: i32, y: i32, z: i32) {} + +#[trusted] +#[requires(x > 0 && y > 0)] +#[requires(divides(x, y))] +#[ensures(divides_prop!(x, y, result))] +fn lemma_divides(x: i32, y: i32) -> i32 { + unimplemented!() +} + +#[requires(x > 0 && y > 0)] +#[ensures(gcd(x + y, y) == gcd(x, y))] +fn lemma_gcd(x: i32, y: i32) { + lemma_gcd_lower(x, y); + lemma_gcd_upper(x, y); +} + +#[requires(x > 0 && y > 0)] +#[ensures(gcd(x + y, y) >= gcd(x, y))] +fn lemma_gcd_upper(x: i32, y: i32) { + let z: i32 = x + y; + let m: i32 = gcd(z, y); + let n: i32 = gcd(y, x); + + let c: i32 = lemma_divides(n, y); + let d: i32 = lemma_divides(n, x); + + lemma_show_divides(n, z, c + d); +} + +#[requires(x > 0 && y > 0)] +#[ensures(gcd(x + y, y) <= gcd(x, y))] +fn lemma_gcd_lower(x: i32, y: i32) { + let z: i32 = x + y; + let m: i32 = gcd(z, y); + + let c: i32 = lemma_divides(m, z); + let d: i32 = lemma_divides(m, y); + + lemma_show_divides(m, x, c - d); +} + +#[requires(x > 0)] +#[ensures(gcd(x, x) == x)] +fn lemma_gcd_idempotent(x: i32) { + lemma_show_divides(x, x, 1); +} + +#[requires(n > 0 && m > 0)] +#[ensures(result == gcd(n, m))] +fn euclid(n: i32, m: i32) -> i32 { + let mut a: i32 = n; + let mut b: i32 = m; + + while a != b { + body_invariant!(a > 0 && b > 0); + body_invariant!(gcd(a, b) == gcd(n, m)); + + if a > b { + a -= b; + lemma_gcd(a, b); + } else { + b -= a; + lemma_gcd(b, a); + } + } + + lemma_gcd_idempotent(a); + + a +} + +fn main() {} diff --git a/prusti-tests/tests/verify/pass/native/floating.rs b/prusti-tests/tests/verify/pass/native/floating.rs new file mode 100644 index 00000000000..e5815ff492d --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/floating.rs @@ -0,0 +1,153 @@ +// compile-flags: -Pviper_backend=Lithium + +use prusti_contracts::*; + +#[pure] +#[terminates] +fn is_nan_32(f: f32) -> bool { + f != f +} + +#[pure] +#[terminates] +fn is_nan_64(f: f64) -> bool { + f != f +} + +#[pure] +#[terminates] +fn is_infinite_32(f: f32) -> bool { + f == f32::INFINITY || f == f32::NEG_INFINITY +} + +#[pure] +#[terminates] +fn is_infinite_64(f: f64) -> bool { + f == f64::INFINITY || f == f64::NEG_INFINITY +} + +fn test_nan_32_is_nan() { + let a = 0.0f32 / 0.0f32; + assert!(is_nan_32(a)); +} + +fn test_nan_32_is_inf() { + let a = 0.0f32 / 0.0f32; + assert!(!is_infinite_32(a)); +} + +fn test_nan_64_is_nan() { + let a = 0.0f64 / 0.0f64; + assert!(is_nan_64(a)); +} + +fn test_nan_64_is_inf() { + let a = 0.0f64 / 0.0f64; + assert!(!is_infinite_64(a)); +} + +fn test_inf_32_is_inf() { + let a = 1.0f32 / 0.0f32; + assert!(is_infinite_32(a)); +} + +fn test_inf_32_is_nan() { + let a = 1.0f32 / 0.0f32; + assert!(!is_nan_32(a)); +} + +fn test_inf_64_is_inf() { + let a = 1.0f64 / 0.0f64; + assert!(is_infinite_64(a)); +} + +fn test_inf_64_is_nan() { + let a = 1.0f64 / 0.0f64; + assert!(!is_nan_64(a)); +} + +fn test_neg_inf_32_is_inf() { + let a = -1.0f32 / 0.0f32; + assert!(is_infinite_32(a)); +} + +fn test_neg_inf_32_is_nan() { + let a = -1.0f32 / 0.0f32; + assert!(!is_nan_32(a)); +} + +fn test_neg_inf_64_is_inf() { + let a = -1.0f64 / 0.0f64; + assert!(is_infinite_64(a)); +} + +fn test_neg_inf_64_is_nan() { + let a = -1.0f64 / 0.0f64; + assert!(!is_nan_64(a)); +} + +// THEORY OF INFINITY + +#[requires(is_nan_32(f))] +#[ensures(!is_infinite_32(f))] +fn axiom1(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(!is_nan_32(f))] +fn axiom2(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f + 1_f32))] +fn axiom3(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f - 1_f32))] +fn axiom4(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f * 2_f32))] +fn axiom5(f: f32) {} + +#[requires(is_infinite_32(f))] +#[ensures(is_infinite_32(f / 2_f32))] +fn axiom6(f: f32) {} + +// THEORY OF NAN + +#[requires(is_infinite_32(f))] +#[ensures(!is_nan_32(f))] +fn axiom7(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f + 1_f32))] +fn axiom8(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f - 1_f32))] +fn axiom9(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f * 2_f32))] +fn axiom10(f: f32) {} + +#[requires(is_nan_32(f))] +#[ensures(is_nan_32(f / 2_f32))] +fn axiom11(f: f32) {} + +#[ensures(is_nan_32(f32::NAN))] +fn axiom12() {} + +fn main() { + test_nan_32_is_nan(); + test_nan_32_is_inf(); + test_nan_64_is_nan(); + test_nan_64_is_inf(); + test_inf_32_is_inf(); + test_inf_32_is_nan(); + test_inf_64_is_inf(); + test_inf_64_is_nan(); + test_neg_inf_32_is_nan(); + test_neg_inf_32_is_inf(); + test_neg_inf_64_is_inf(); + test_neg_inf_64_is_nan(); +} diff --git a/prusti-tests/tests/verify/pass/native/quantifier_closures.rs b/prusti-tests/tests/verify/pass/native/quantifier_closures.rs new file mode 100644 index 00000000000..820c3fd91f6 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/quantifier_closures.rs @@ -0,0 +1,15 @@ +// compile-flags: -Pviper_backend=Lithium +use prusti_contracts::*; + +#[requires(forall(|x: i32| x * x >= foo * bar))] +fn test_closure(foo: i32, bar: i32) -> i32 { + foo + bar + 1 +} + +fn main() { + test_closure(0, 0); + + let arg1 = 0; + let arg2 = 0; + test_closure(arg1, arg2); +} diff --git a/prusti-tests/tests/verify/pass/native/structure_quantifiers.rs b/prusti-tests/tests/verify/pass/native/structure_quantifiers.rs new file mode 100644 index 00000000000..18109da9fa6 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/structure_quantifiers.rs @@ -0,0 +1,27 @@ +// compile-flags: -Pviper_backend=Lithium +use prusti_contracts::*; + +pub struct MyStructure {} + +impl MyStructure { + #[pure] + #[terminates] + #[ensures (0 <= result)] + pub fn len(&self) -> i32 { + 17 + } +} + +#[pure] +#[terminates] +#[ensures (0 <= result)] +#[ensures(result == s.len())] +fn len_of(s: &MyStructure) -> i32 { + 17 +} + +#[ensures(forall(|s: MyStructure| len_of(&s) >= 0))] +#[ensures(forall(|s: MyStructure| s.len() >= 10))] +fn test(min: i32) {} + +fn main() {} diff --git a/prusti-tests/tests/verify/pass/native/switchInt.rs b/prusti-tests/tests/verify/pass/native/switchInt.rs new file mode 100644 index 00000000000..aaea4b4c491 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/switchInt.rs @@ -0,0 +1,18 @@ +// compile-flags: -Pviper_backend=Lithium + +fn test(x: i32) { + match x { + 0..=5 => { + assert!(x >= 0); + assert!(x <= 5); + } + 1 => { + assert!(x == 1); + } + _ => { + assert!(x < 0 || x >= 0); + } + } +} + +fn main() {} diff --git a/prusti-tests/tests/verify/pass/native/trivial.rs b/prusti-tests/tests/verify/pass/native/trivial.rs new file mode 100644 index 00000000000..77947467bbd --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/trivial.rs @@ -0,0 +1,5 @@ +// compile-flags: -Pviper_backend=Lithium + +fn main() { + assert!(true); +} diff --git a/prusti-tests/tests/verify/pass/native/while.rs b/prusti-tests/tests/verify/pass/native/while.rs new file mode 100644 index 00000000000..90d1de2f199 --- /dev/null +++ b/prusti-tests/tests/verify/pass/native/while.rs @@ -0,0 +1,20 @@ +// compile-flags: -Pviper_backend=Lithium + +use prusti_contracts::*; + +const N: i32 = 10; + +#[requires(i <= N)] +#[ensures(result == N)] +fn test(i: i32) -> i32 { + let mut ret = i; + while ret < N { + body_invariant!(ret < N); + ret += 1; + } + ret +} + +fn main() { + assert!(test(3) == N); +} diff --git a/prusti-tests/tests/verify_overflow/fail/native/bisect.rs b/prusti-tests/tests/verify_overflow/fail/native/bisect.rs new file mode 100644 index 00000000000..4f4f3570f85 --- /dev/null +++ b/prusti-tests/tests/verify_overflow/fail/native/bisect.rs @@ -0,0 +1,42 @@ +use prusti_contracts::*; + +/// A monotonically increasing discrete function, with domain [0, domain_size) +struct Function; + +impl Function { + #[pure] + #[trusted] // abstract, actual implementation doesn't matter + fn domain_size(&self) -> usize { + 42 + } + + #[pure] + #[trusted] + #[requires(x < self.domain_size())] + fn eval(&self, x: usize) -> i32 { + x as i32 + } +} + +/// Find the `x` s.t. `f(x) == target` +#[ensures(if let Some(x) = result { f.eval(x) == target } else { true })] +fn bisect(f: &Function, target: i32) -> Option { + let mut low = 0; + let mut high = f.domain_size(); + assert!(high == f.domain_size()); + while low < high { + body_invariant!(low < high && high <= f.domain_size()); + let mid = (low + high) / 2; //~ ERROR attempt to add with overflow + let mid_val = f.eval(mid); + if mid_val < target { + low = mid + 1; + } else if mid_val > target { + high = mid; + } else { + return Some(mid); + } + } + None +} + +fn main() {} diff --git a/prusti-utils/src/config.rs b/prusti-utils/src/config.rs index b137f929c6e..3ecde175aae 100644 --- a/prusti-utils/src/config.rs +++ b/prusti-utils/src/config.rs @@ -180,6 +180,7 @@ lazy_static::lazy_static! { allowed_keys.insert("rustc_log_args".to_string()); allowed_keys.insert("rustc_log_env".to_string()); allowed_keys.insert("original_smt_solver_path".to_string()); + allowed_keys.insert("native_verifier".to_string()); // TODO: reduce this to something more sensible: static MAX_CONFIG_LEN: usize = 40; @@ -190,6 +191,17 @@ lazy_static::lazy_static! { allowed_keys.iter().filter(|key| key.len() > MAX_CONFIG_LEN).collect::>() ); + // 0. Apply Lithium overrides if necessary + if let Ok(true) = env::var("PRUSTI_NATIVE_VERIFIER").map(|s| s.parse::().unwrap_or(false)) { + settings.set_default("viper_backend", "Lithium").unwrap(); + settings.set_default("verify_specifications_backend", "Lithium").unwrap(); + settings.set_default("encode_bitvectors", true).unwrap(); + settings.set_default("enable_purification_optimization", true).unwrap(); + settings.set_default("unsafe_core_proof", true).unwrap(); + settings.set_default("verify_core_proof", false).unwrap(); + settings.set_default("inline_caller_for", true).unwrap(); + } + // 1. Override with default env variables (e.g. `DEFAULT_PRUSTI_CACHE_PATH`, ...) settings.merge( Environment::with_prefix("DEFAULT_PRUSTI").ignore_empty(true) diff --git a/prusti-utils/src/utils/mod.rs b/prusti-utils/src/utils/mod.rs index d64afd98f06..19174783b01 100644 --- a/prusti-utils/src/utils/mod.rs +++ b/prusti-utils/src/utils/mod.rs @@ -6,3 +6,4 @@ pub mod identifiers; pub mod to_string; +pub mod run_timed; diff --git a/prusti-utils/src/utils/run_timed.rs b/prusti-utils/src/utils/run_timed.rs new file mode 100644 index 00000000000..08ab869de60 --- /dev/null +++ b/prusti-utils/src/utils/run_timed.rs @@ -0,0 +1,20 @@ +// copied from prusti-common to avoid illogical dependency. +/// Runs statements on the same level as the macro call, timing and logging (info-level by default) how long it took. +#[macro_export] +macro_rules! run_timed { + ($desc:expr, $($s:stmt;)*) => { + run_timed!($desc, info, $($s;)*); + }; + ($desc:expr, $log_level:ident, $($s:stmt;)*) => { + $log_level!("Starting: {}", $desc); + let start = ::std::time::Instant::now(); + $($s)* + let duration = start.elapsed(); + $log_level!( + "Completed: {} ({}.{} seconds)", + $desc, + duration.as_secs(), + duration.subsec_millis() / 10 + ); + }; +} diff --git a/prusti-viper/Cargo.toml b/prusti-viper/Cargo.toml index 9606064ad01..0f176dd2101 100644 --- a/prusti-viper/Cargo.toml +++ b/prusti-viper/Cargo.toml @@ -15,6 +15,7 @@ log = { version = "0.4", features = ["release_max_level_info"] } viper = { path = "../viper" } prusti-interface = { path = "../prusti-interface" } prusti-common = { path = "../prusti-common" } +backend-common = { path = "../backend-common" } prusti-server = { path = "../prusti-server" } prusti-rustc-interface = { path = "../prusti-rustc-interface" } vir-crate = { package = "vir", path = "../vir" } diff --git a/prusti-viper/src/encoder/builtin_encoder.rs b/prusti-viper/src/encoder/builtin_encoder.rs index 4892355cd95..7631e4ce845 100644 --- a/prusti-viper/src/encoder/builtin_encoder.rs +++ b/prusti-viper/src/encoder/builtin_encoder.rs @@ -277,12 +277,20 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinEncoder<'p, 'v, 'tcx> { let mut functions = vec![]; let mut axioms = vec![]; - for t in &[vir::Type::Bool, vir::Type::Int] { + for t in &[ + vir::Type::Bool, + vir::Type::Int, + vir::Type::Float(vir::Float::F32), + vir::Type::Float(vir::Float::F64), + ] { //let f = snapshot::valid_func_for_type(t); let f = { let domain_name: String = match t { // vir::Type::Domain(name) => name.clone(), - vir::Type::Bool | vir::Type::Int => domain_name.to_string(), + vir::Type::Bool + | vir::Type::Int + | vir::Type::Float(vir::Float::F32) + | vir::Type::Float(vir::Float::F64) => domain_name.to_string(), // vir::Type::TypedRef(_) => unreachable!(), // vir::Type::TypeVar(_) => unreachable!(), // vir::Type::Snapshot(_) => unreachable!(), @@ -293,6 +301,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> BuiltinEncoder<'p, 'v, 'tcx> { // vir::Type::Domain(vir::DomainType{label, ..}) => vir::Type::domain(label.clone()), vir::Type::Bool => vir::Type::Bool, vir::Type::Int => vir::Type::Int, + vir::Type::Float(vir::Float::F32) => vir::Type::Float(vir::Float::F32), + vir::Type::Float(vir::Float::F64) => vir::Type::Float(vir::Float::F64), // vir::Type::TypedRef(_) => unreachable!(), // vir::Type::TypeVar(_) => unreachable!(), // vir::Type::Snapshot(_) => unreachable!(), diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs index 66fff62fcf0..85517bab984 100644 --- a/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs +++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation.rs @@ -4,6 +4,7 @@ use crate::encoder::{ places::{Local, LocalVariableManager}, Encoder, }; +use backend_common::{DomainEntry, ModelEntry, SiliconCounterexample}; use prusti_interface::{ data::ProcedureDefId, environment::{body::MirBody, EnvQuery}, @@ -17,7 +18,6 @@ use prusti_rustc_interface::{ }; use rustc_hash::FxHashMap; use std::iter; -use viper::silicon_counterexample::*; use DiscriminantsStateInterface; pub fn backtranslate( diff --git a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs index 159cf1a39af..4f74b496265 100644 --- a/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs +++ b/prusti-viper/src/encoder/counterexamples/counterexample_translation_refactored.rs @@ -6,6 +6,7 @@ use crate::encoder::{ places::{Local, LocalVariableManager}, Encoder, }; +use backend_common::{DomainEntry, ModelEntry, SiliconCounterexample}; use prusti_common::config; use prusti_interface::data::ProcedureDefId; use prusti_rustc_interface::{ @@ -20,7 +21,6 @@ use prusti_rustc_interface::{ }; use rustc_hash::FxHashMap; use std::{iter, vec}; -use viper::silicon_counterexample::*; pub fn backtranslate( encoder: &Encoder, diff --git a/prusti-viper/src/encoder/errors/error_manager.rs b/prusti-viper/src/encoder/errors/error_manager.rs index 4f350f644c9..f216f1a5a22 100644 --- a/prusti-viper/src/encoder/errors/error_manager.rs +++ b/prusti-viper/src/encoder/errors/error_manager.rs @@ -4,14 +4,13 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use std::fmt::Debug; - use super::PositionManager; +use backend_common::VerificationError; +use core::fmt::Debug; use log::debug; use prusti_interface::{data::ProcedureDefId, PrustiError}; use prusti_rustc_interface::{errors::MultiSpan, span::source_map::SourceMap}; use rustc_hash::FxHashMap; -use viper::VerificationError; use vir_crate::polymorphic::Position; const ASSERTION_TIMEOUT_HELP_MESSAGE: &str = @@ -231,19 +230,19 @@ impl<'tcx> ErrorManager<'tcx> { Position::default(), "Trying to register an error on a default position" ); - if let Some(existing_error_ctxt) = self.error_contexts.get(&pos.id()) { - debug_assert_eq!( - existing_error_ctxt, - &error_ctxt, - "An existing error context would be overwritten.\n\ - Position id: {}\n\ - Existing error context: {:?}\n\ - New error context: {:?}", - pos.id(), - existing_error_ctxt, - error_ctxt - ); - } + // if let Some(existing_error_ctxt) = self.error_contexts.get(&pos.id()) { + // debug_assert_eq!( + // existing_error_ctxt, + // &error_ctxt, + // "An existing error context would be overwritten.\n\ + // Position id: {}\n\ + // Existing error context: {:?}\n\ + // New error context: {:?}", + // pos.id(), + // existing_error_ctxt, + // error_ctxt + // ); + // } self.error_contexts.insert(pos.id(), error_ctxt); } diff --git a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs index 9828f510e12..8ce8c4fffb6 100644 --- a/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/builtin_methods/interface.rs @@ -690,8 +690,15 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> { // For some reason, division is not CheckedBinaryOp, but the // regular one. Therefore, we need to put the checks for // overflows into the precondition. - let type_decl = self.encoder.get_type_decl_mid(result_type)?.unwrap_int(); - if let Some(lower) = type_decl.lower_bound { + let type_decl = self.encoder.get_type_decl_mid(result_type)?; + + let lower_bound = if result_type.is_float() { + type_decl.unwrap_float().lower_bound + } else { + type_decl.unwrap_int().lower_bound + }; + + if let Some(lower) = lower_bound { let zero = self.construct_constant_snapshot(result_type, 0.into(), position)?; pres.push(expr! {operand_right != [zero]}); diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs index f88ff2b7ac6..09214142d5a 100644 --- a/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs +++ b/prusti-viper/src/encoder/middle/core_proof/snapshots/into_snapshot/common/mod.rs @@ -6,7 +6,10 @@ use crate::encoder::{ lifetimes::*, lowerer::DomainsLowererInterface, references::ReferencesInterface, - snapshots::{IntoSnapshot, SnapshotDomainsInterface, SnapshotValuesInterface}, + snapshots::{ + IntoSnapshot, SnapshotDomainsInterface, SnapshotValidityInterface, + SnapshotValuesInterface, + }, types::TypesInterface, }, }; @@ -75,7 +78,9 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> { vir_mid::Expression::Conditional(expression) => { self.conditional_to_snapshot(lowerer, expression, expect_math_bool) } - // vir_mid::Expression::Quantifier(expression) => self.quantifier_to_snapshot(lowerer, expression, expect_math_bool), + vir_mid::Expression::Quantifier(expression) => { + self.quantifier_to_snapshot(lowerer, expression, expect_math_bool) + } // vir_mid::Expression::LetExpr(expression) => self.letexpr_to_snapshot(lowerer, expression, expect_math_bool), vir_mid::Expression::FuncApp(expression) => { self.func_app_to_snapshot(lowerer, expression, expect_math_bool) @@ -103,6 +108,103 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> { } } + fn quantifier_to_snapshot( + &mut self, + lowerer: &mut Lowerer<'p, 'v, 'tcx>, + quantifier: &vir_mid::Quantifier, + expect_math_bool: bool, + ) -> SpannedEncodingResult { + let vir_mid::Quantifier { + kind, + variables, + triggers, + body, + position, + } = quantifier; + + let vars = variables + .iter() + .map(|variable| self.variable_to_snapshot(lowerer, variable)) + .collect::>>()?; + + let trigs = triggers + .iter() + .map(|trigger| { + let trig = self + .expression_vec_to_snapshot(lowerer, &trigger.terms, expect_math_bool) + .unwrap(); + vir_low::Trigger { terms: trig } + }) + .collect(); + + let body = self.expression_to_snapshot(lowerer, body, true)?; + + // generate validity calls for all variables we quantify over + // this is needed to ensure that the quantifier is well-formed + // because most axioms assume valid arguments + // for some reason they are added in the outer scope as assertions, as if the program thought that these are global variables + // TODO: Find a way to make this less cursed + // TODO: do not generate the validity calls for variables outside the quantifier + let mut validity_calls = Vec::new(); + for variable in vars.iter() { + let call = lowerer.encode_snapshot_valid_call( + &variable.ty.to_string(), + vir_low::Expression::Local(vir_low::expression::Local { + variable: variable.clone(), + position: quantifier.position(), + }), + )?; + validity_calls.push(call); + } + + let recursive_apply_and = |mut exprs: Vec| { + let mut result = exprs.pop().unwrap(); + for expr in exprs.into_iter().rev() { + result = vir_low::Expression::BinaryOp(vir_low::expression::BinaryOp { + left: Box::new(expr), + right: Box::new(result), + position: *position, + op_kind: vir_low::expression::BinaryOpKind::And, + }); + } + result + }; + + let validity_call_imply_body = + vir_low::Expression::BinaryOp(vir_low::expression::BinaryOp { + left: Box::new(recursive_apply_and(validity_calls)), + right: Box::new(body), + position: *position, + op_kind: vir_low::expression::BinaryOpKind::Implies, + }); + + let kind = match kind { + vir_mid::expression::QuantifierKind::ForAll => { + vir_low::expression::QuantifierKind::ForAll + } + vir_mid::expression::QuantifierKind::Exists => { + vir_low::expression::QuantifierKind::Exists + } + }; + + // no call to ensure_bool_expression since quantifiers are always math bool and forall is built-in to SMT solvers + let qtfy = vir_low::Expression::Quantifier(vir_low::expression::Quantifier { + kind, + variables: vars, + triggers: trigs, + body: Box::new(validity_call_imply_body), + position: *position, + }); + + // wrap in snapshot bool constructor if not expect_math_bool + if !expect_math_bool { + let pos = qtfy.position(); + lowerer.construct_struct_snapshot(quantifier.get_type(), vec![qtfy], pos) + } else { + Ok(qtfy) + } + } + fn variable_to_snapshot( &mut self, lowerer: &mut Lowerer<'p, 'v, 'tcx>, @@ -236,6 +338,12 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> { vir_mid::Type::MFloat64 => unimplemented!(), vir_mid::Type::Bool => vir_low::Type::Bool, vir_mid::Type::Int(_) => vir_low::Type::Int, + vir_mid::Type::Float(vir_mid::ty::Float::F32) => { + vir_low::Type::Float(vir_low::ty::Float::F32) + } + vir_mid::Type::Float(vir_mid::ty::Float::F64) => { + vir_low::Type::Float(vir_low::ty::Float::F64) + } vir_mid::Type::MPerm => vir_low::Type::Perm, _ => unimplemented!("constant: {:?}", constant), }; @@ -274,9 +382,12 @@ pub(super) trait IntoSnapshotLowerer<'p, 'v: 'p, 'tcx: 'v> { vir_mid::expression::ConstantValue::BigInt(value) => { vir_low::expression::ConstantValue::BigInt(value.clone()) } - vir_mid::expression::ConstantValue::Float(_value) => { - unimplemented!(); - } + vir_mid::expression::ConstantValue::Float(vir_crate::polymorphic::FloatConst::F32( + value, + )) => vir_low::expression::ConstantValue::Float32(*value), + vir_mid::expression::ConstantValue::Float(vir_crate::polymorphic::FloatConst::F64( + value, + )) => vir_low::expression::ConstantValue::Float64(*value), vir_mid::expression::ConstantValue::FnPtr => { unimplemented!(); } diff --git a/prusti-viper/src/encoder/middle/core_proof/snapshots/values/interface.rs b/prusti-viper/src/encoder/middle/core_proof/snapshots/values/interface.rs index 98af319413c..b09a20813d1 100644 --- a/prusti-viper/src/encoder/middle/core_proof/snapshots/values/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/snapshots/values/interface.rs @@ -105,6 +105,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotValuesInterface for Lowerer<'p, 'v, 'tcx> { let return_type = match &ty { vir_mid::Type::Bool => vir_low::Type::Bool, vir_mid::Type::Int(_) => vir_low::Type::Int, + vir_mid::Type::Float(vir_mid::ty::Float::F32) => { + vir_low::Type::Float(vir_low::ty::Float::F32) + } + vir_mid::Type::Float(vir_mid::ty::Float::F64) => { + vir_low::Type::Float(vir_low::ty::Float::F64) + } vir_mid::Type::Pointer(_) => self.address_type()?, x => unimplemented!("{:?}", x), }; @@ -205,6 +211,12 @@ impl<'p, 'v: 'p, 'tcx: 'v> SnapshotValuesInterface for Lowerer<'p, 'v, 'tcx> { let low_type = match &ty { vir_mid::Type::Bool => vir_low::Type::Bool, vir_mid::Type::Int(_) => vir_low::Type::Int, + vir_mid::Type::Float(vir_mid::ty::Float::F32) => { + vir_low::Type::Float(vir_low::ty::Float::F32) + } + vir_mid::Type::Float(vir_mid::ty::Float::F64) => { + vir_low::Type::Float(vir_low::ty::Float::F64) + } vir_mid::Type::Pointer(_) => self.address_type()?, vir_mid::Type::Reference(_) => self.address_type()?, x => unimplemented!("{:?}", x), diff --git a/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs b/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs index c89e1fcd606..8b62e843127 100644 --- a/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs +++ b/prusti-viper/src/encoder/middle/core_proof/transformations/inline_functions.rs @@ -86,6 +86,29 @@ impl<'a> ExpressionFolder for Inliner<'a> { binary_op } + fn fold_quantifier( + &mut self, + mut quantifier: vir_low::expression::Quantifier, + ) -> vir_low::expression::Quantifier { + quantifier.triggers = quantifier + .triggers + .iter() + .map(|trigger| { + let mut trigger = trigger.clone(); + trigger.terms = trigger + .terms + .into_iter() + .map(|term| *self.fold_expression_boxed(Box::new(term))) + .collect(); + trigger + }) + .collect(); + + quantifier.body = self.fold_expression_boxed(quantifier.body); + + quantifier + } + fn fold_conditional( &mut self, mut conditional: vir_low::expression::Conditional, diff --git a/prusti-viper/src/encoder/middle/core_proof/types/interface.rs b/prusti-viper/src/encoder/middle/core_proof/types/interface.rs index aa2b046f5dd..899619b46e3 100644 --- a/prusti-viper/src/encoder/middle/core_proof/types/interface.rs +++ b/prusti-viper/src/encoder/middle/core_proof/types/interface.rs @@ -98,6 +98,33 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> { let validity = conjuncts.into_iter().conjoin(); self.encode_validity_axioms_primitive(&domain_name, vir_low::Type::Int, validity)?; } + vir_mid::TypeDecl::Float(decl) => { + let is_f64 = domain_name.contains("F64"); + let float_type = || { + if is_f64 { + vir_low::Type::Float(vir_low::ty::Float::F64) + } else { + vir_low::Type::Float(vir_low::ty::Float::F32) + } + }; + + self.ensure_type_definition(&vir_mid::Type::Bool)?; + self.register_constant_constructor(&domain_name, float_type())?; + + let value = vir_low::ast::variable::VariableDecl::new("value", float_type()); + + let mut conjuncts = Vec::new(); + if let Some(lower_bound) = &decl.lower_bound { + conjuncts + .push(expr! { [lower_bound.clone().to_pure_snapshot(self)? ] <= value }); + } + if let Some(upper_bound) = &decl.upper_bound { + conjuncts + .push(expr! { value <= [upper_bound.clone().to_pure_snapshot(self)? ] }); + } + let validity = conjuncts.into_iter().conjoin(); + self.encode_validity_axioms_primitive(&domain_name, float_type(), validity)?; + } vir_mid::TypeDecl::Trusted(_) => { // FIXME: ensure type definition for trusted } @@ -199,6 +226,21 @@ impl<'p, 'v: 'p, 'tcx: 'v> Private for Lowerer<'p, 'v, 'tcx> { self.register_struct_constructor(&domain_name, Vec::new())?; self.encode_validity_axioms_struct(&domain_name, Vec::new(), false.into())?; } + vir_mid::TypeDecl::Closure(closure) => { + // closure has a name and array of arguments, which represent the "saved" parameters of the function + // it is not a function, just a struct that remembers the arguments at entry time + let mut parameters = Vec::new(); + for (ix, argument) in closure.arguments.iter().enumerate() { + self.ensure_type_definition(argument)?; + parameters.push(vir_low::VariableDecl::new( + format!("_{}", ix), + argument.to_snapshot(self)?, + )); + } + + self.register_struct_constructor(&domain_name, parameters.clone())?; + self.encode_validity_axioms_struct(&domain_name, parameters, true.into())?; + } _ => unimplemented!("type: {:?}", type_decl), }; Ok(()) @@ -367,6 +409,16 @@ impl<'p, 'v: 'p, 'tcx: 'v> TypesInterface for Lowerer<'p, 'v, 'tcx> { var_decls! { constant: Int }; Some((expr! { -constant }, constant)) } + vir_mid::Type::Float(vir_mid::ty::Float::F32) => { + assert_eq!(op, vir_low::UnaryOpKind::Minus); + var_decls! { constant: Float32 }; + Some((expr! { -constant }, constant)) + } + vir_mid::Type::Float(vir_mid::ty::Float::F64) => { + assert_eq!(op, vir_low::UnaryOpKind::Minus); + var_decls! { constant: Float64 }; + Some((expr! { -constant }, constant)) + } _ => None, }; if let Some((simplification_result, parameter)) = simplification { @@ -422,6 +474,8 @@ impl<'p, 'v: 'p, 'tcx: 'v> TypesInterface for Lowerer<'p, 'v, 'tcx> { let constant_type = match argument_type { vir_mid::Type::Bool => Some(ty! { Bool }), vir_mid::Type::Int(_) => Some(ty! {Int}), + vir_mid::Type::Float(vir_mid::ty::Float::F32) => Some(ty! {Float32}), + vir_mid::Type::Float(vir_mid::ty::Float::F64) => Some(ty! {Float64}), vir_mid::Type::Pointer(_) => Some(ty!(Address)), _ => None, }; diff --git a/prusti-viper/src/encoder/mir/constants/interface.rs b/prusti-viper/src/encoder/mir/constants/interface.rs index 41b3dd1e814..f78861a0fcc 100644 --- a/prusti-viper/src/encoder/mir/constants/interface.rs +++ b/prusti-viper/src/encoder/mir/constants/interface.rs @@ -55,6 +55,26 @@ impl<'v, 'tcx: 'v> ConstantsEncoderInterface<'tcx> for super::super::super::Enco .unwrap(); number.into() } + ty::TyKind::Float(ty::FloatTy::F32) => { + let ty = self.encode_type_high(mir_type)?; + let bits = scalar_value()?.to_u32().unwrap(); + vir_high::Expression::constant_no_pos( + vir_high::expression::ConstantValue::Float( + vir_high::expression::FloatConst::F32(bits), + ), + ty, + ) + } + ty::TyKind::Float(ty::FloatTy::F64) => { + let ty = self.encode_type_high(mir_type)?; + let bits = scalar_value()?.to_u64().unwrap(); + vir_high::Expression::constant_no_pos( + vir_high::expression::ConstantValue::Float( + vir_high::expression::FloatConst::F64(bits), + ), + ty, + ) + } ty::TyKind::FnDef(..) => { let ty = self.encode_type_high(mir_type)?; vir_high::Expression::constant_no_pos( diff --git a/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs b/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs index 71409b307ac..6ee6fc6dd0e 100644 --- a/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs +++ b/prusti-viper/src/encoder/mir/pure/specifications/encoder_high.rs @@ -147,9 +147,16 @@ pub(super) fn encode_quantifier_high<'tcx>( if config::check_overflows() { bounds.extend(encoder.encode_type_bounds_high(&encoded_qvar.clone().into(), arg_ty)); } else if config::encode_unsigned_num_constraint() { - if let ty::TyKind::Uint(_) = arg_ty.kind() { - let expr = - vir_high::Expression::less_equals(0u32.into(), encoded_qvar.clone().into()); + if let ty::TyKind::Uint(utype) = arg_ty.kind() { + let zero = match utype { + ty::UintTy::U8 => 0u8.into(), + ty::UintTy::U16 => 0u16.into(), + ty::UintTy::U32 => 0u32.into(), + ty::UintTy::U64 => 0u64.into(), + ty::UintTy::U128 => 0u128.into(), + ty::UintTy::Usize => 0usize.into(), + }; + let expr = vir_high::Expression::less_equals(zero, encoded_qvar.clone().into()); bounds.push(expr); } } diff --git a/prusti-viper/src/verifier.rs b/prusti-viper/src/verifier.rs index 019abb0ed40..0ae50ba4e68 100644 --- a/prusti-viper/src/verifier.rs +++ b/prusti-viper/src/verifier.rs @@ -103,18 +103,18 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> { let mut java_exceptions: Vec<_> = vec![]; for (method_name, result) in verification_results.into_iter() { match result { - viper::VerificationResult::Success => {} - viper::VerificationResult::ConsistencyErrors(errors) => { + backend_common::VerificationResult::Success => {} + backend_common::VerificationResult::ConsistencyErrors(errors) => { for error in errors.into_iter() { consistency_errors.push((method_name.clone(), error)); } } - viper::VerificationResult::Failure(errors) => { + backend_common::VerificationResult::Failure(errors) => { for error in errors.into_iter() { verification_errors.push((method_name.clone(), error)); } } - viper::VerificationResult::JavaException(exception) => { + backend_common::VerificationResult::JavaException(exception) => { java_exceptions.push((method_name, exception)); } } @@ -214,7 +214,7 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> { fn verify_programs( env: &Environment, programs: Vec, -) -> Vec<(String, viper::VerificationResult)> { +) -> Vec<(String, backend_common::VerificationResult)> { let source_path = env.name.source_path(); let rust_program_name = source_path .file_name() diff --git a/test.sh b/test.sh new file mode 100755 index 00000000000..c1b264d5785 --- /dev/null +++ b/test.sh @@ -0,0 +1,50 @@ +#!/bin/bash + +# ANSI escape codes for colors +RED='\033[0;31m' +GREEN='\033[0;32m' +YELLOW='\033[1;33m' +NC='\033[0m' # No Color + +# Initialize or clear the files +> passing.txt +> failing.txt +> panicking.txt + +# Initialize counters +passed=0 +failed=0 +panicked=0 + +for i in prusti-tests/tests/verify/pass/**/*.rs; do + echo -n "Testing file: $i" + + # Run the test + output=$(PRUSTI_FULL_COMPILATION=false target/release/prusti-rustc --edition=2021 $i -Pcheck_overflows=false 2>&1) + + # Check the exit status of the test + if [ $? -eq 0 ]; then + # Test passed, append to passing.txt + echo "$i" >> passing.txt + echo -e " ...${GREEN}ok${NC}" + ((passed++)) + else + # Test failed + if echo "$output" | grep -q "^thread 'rustc' panicked at"; then + # There was a panic, append output to panicking.txt + echo -e "\n---- $i ----\n$output" >> panicking.txt + echo -e " ...${YELLOW}PANICKED${NC}" + ((panicked++)) + else + # Other error, append output to failing.txt + echo -e "\n---- $i ----\n$output" >> failing.txt + echo -e " ...${RED}FAILED${NC}" + ((failed++)) + fi + fi +done + +# Print test statistics +echo -e "${GREEN}$passed tests passed${NC}" +echo -e "${RED}$failed tests failed${NC}" +echo -e "${YELLOW}$panicked tests panicked${NC}" diff --git a/viper/Cargo.toml b/viper/Cargo.toml index 0715e82be61..0e6a3fd1cdd 100644 --- a/viper/Cargo.toml +++ b/viper/Cargo.toml @@ -11,6 +11,7 @@ license = "MPL-2.0" log = { version = "0.4", features = ["release_max_level_debug"] } error-chain = "0.12" viper-sys = { path = "../viper-sys" } +backend-common = { path = "../backend-common" } jni = { version = "0.20", features = ["invocation"] } uuid = { version = "1.0", features = ["v4"] } serde = { version = "1.0", features = ["derive"] } @@ -19,6 +20,7 @@ rustc-hash = "1.1.0" tokio = { version = "1.20", features = ["io-util", "net", "rt", "sync"] } futures = "0.3.21" smt-log-analyzer = { path = "../smt-log-analyzer"} +prusti-utils = { path = "../prusti-utils"} tracing = { path = "../tracing" } [dev-dependencies] diff --git a/viper/src/ast_utils.rs b/viper/src/ast_utils.rs index 55120e17539..6bfa8b33ebb 100644 --- a/viper/src/ast_utils.rs +++ b/viper/src/ast_utils.rs @@ -4,7 +4,8 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::{ast_factory::Program, jni_utils::JniUtils, JavaException}; +use crate::{ast_factory::Program, jni_utils::JniUtils}; +use backend_common::JavaException; use jni::{objects::JObject, JNIEnv}; use viper_sys::wrappers::viper::*; diff --git a/viper/src/cache.rs b/viper/src/cache.rs index 4b78dc3d1fc..3a02145e932 100644 --- a/viper/src/cache.rs +++ b/viper/src/cache.rs @@ -6,7 +6,7 @@ use log::{error, info, warn}; -use crate::verification_result::VerificationResult; +use backend_common::VerificationResult; use rustc_hash::FxHashMap; use std::{ fs, io, diff --git a/viper/src/jni_utils.rs b/viper/src/jni_utils.rs index f99623611b1..752c436fb28 100644 --- a/viper/src/jni_utils.rs +++ b/viper/src/jni_utils.rs @@ -4,7 +4,7 @@ // License, v. 2.0. If a copy of the MPL was not distributed with this // file, You can obtain one at http://mozilla.org/MPL/2.0/. -use crate::java_exception::JavaException; +use backend_common::JavaException; use jni::{ errors::{Error, Result as JniResult}, objects::{JObject, JString}, diff --git a/viper/src/lib.rs b/viper/src/lib.rs index 747f7fc1261..ebc70f58049 100644 --- a/viper/src/lib.rs +++ b/viper/src/lib.rs @@ -14,17 +14,14 @@ mod jni_utils; #[macro_use] pub mod utils; mod cache; -mod java_exception; -pub mod silicon_counterexample; pub mod smt_manager; mod verification_backend; +pub mod silicon_counterexample; mod verification_context; -mod verification_result; mod verifier; mod viper; pub use crate::{ - ast_factory::*, ast_utils::*, cache::*, java_exception::*, silicon_counterexample::*, - verification_backend::*, verification_context::*, verification_result::*, verifier::*, - viper::*, + ast_factory::*, ast_utils::*, cache::*, silicon_counterexample::*, verification_backend::*, + verification_context::*, verifier::*, viper::*, }; diff --git a/viper/src/silicon_counterexample.rs b/viper/src/silicon_counterexample.rs index 0ad438a963e..5e1708bc33f 100644 --- a/viper/src/silicon_counterexample.rs +++ b/viper/src/silicon_counterexample.rs @@ -1,112 +1,18 @@ use rustc_hash::FxHashMap; use crate::jni_utils::JniUtils; +use backend_common::{ + DomainEntry, Domains, FunctionEntry, Functions, Model, ModelEntry, SiliconCounterexample, +}; use jni::{objects::JObject, JNIEnv}; use viper_sys::wrappers::{scala, viper::silicon}; -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct SiliconCounterexample { - //pub heap: Heap, - //pub old_heaps: FxHashMap, - pub model: Model, - pub functions: Functions, - pub domains: Domains, - pub old_models: FxHashMap, - // label_order because HashMaps do not guarantee order of elements - // whereas the Map used in scala does guarantee it - pub label_order: Vec, -} - -impl SiliconCounterexample { - pub fn new<'a>( - env: &'a JNIEnv<'a>, - jni: JniUtils<'a>, - counterexample: JObject<'a>, - ) -> SiliconCounterexample { - unwrap_counterexample(env, jni, counterexample) - } -} - -// Heap Definitions -/* -this stuff might be useful at a later stage, when we can actually -trigger unfolding of certain predicates, but for now there is -nothing to be used stored in the heap -*/ -/* -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct Heap { - pub entries: Vec, -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub enum HeapEntry { - FieldEntry { - recv: ModelEntry, - //perm & sort omitted - field: String, - entry: ModelEntry, - }, - PredicateEntry { - name: String, - args: Vec, - }, -} -*/ - -// Model Definitions -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct Model { - pub entries: FxHashMap, -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub enum ModelEntry { - LitInt(String), - LitFloat(String), - LitBool(bool), - LitPerm(String), - Ref(String, FxHashMap), - NullRef(String), - RecursiveRef(String), - Var(String), - Seq(String, Vec), - Other(String, String), - DomainValue(String, String), - UnprocessedModel, //used for Silicon's Snap type -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct Functions { - pub entries: FxHashMap, -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct FunctionEntry { - pub options: Vec<(Vec>, Option)>, - pub default: Option, -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct Domains { - pub entries: FxHashMap, -} - -#[derive(Debug, Clone, PartialEq, serde::Serialize, serde::Deserialize)] -pub struct DomainEntry { - pub functions: Functions, -} - -impl FunctionEntry { - /// Given a vec of params it finds the correct entry in a function. - pub fn get_function_value(&self, params: &Vec>) -> &Option { - for option in &self.options { - if &option.0 == params { - return &option.1; - } - } - &None - } +pub fn silicon_counterexample<'a>( + env: &'a JNIEnv<'a>, + jni: JniUtils<'a>, + counterexample: JObject<'a>, +) -> SiliconCounterexample { + unwrap_counterexample(env, jni, counterexample) } // methods unwrapping scala converter to newly defined structures diff --git a/viper/src/utils.rs b/viper/src/utils.rs index e532573f9e8..71891b52654 100644 --- a/viper/src/utils.rs +++ b/viper/src/utils.rs @@ -30,24 +30,3 @@ where self.fold(init, |acc, conjunct| ast.and(acc, conjunct)) } } - -// copied from prusti-common to avoid illogical dependency. -/// Runs statements on the same level as the macro call, timing and logging (info-level by default) how long it took. -#[macro_export] -macro_rules! run_timed { - ($desc:expr, $($s:stmt;)*) => { - run_timed!($desc, info, $($s;)*); - }; - ($desc:expr, $log_level:ident, $($s:stmt;)*) => { - $log_level!("Starting: {}", $desc); - let start = ::std::time::Instant::now(); - $($s)* - let duration = start.elapsed(); - $log_level!( - "Completed: {} ({}.{} seconds)", - $desc, - duration.as_secs(), - duration.subsec_millis() / 10 - ); - }; -} diff --git a/viper/src/verification_backend.rs b/viper/src/verification_backend.rs index 0746a73b29d..086c7311a88 100644 --- a/viper/src/verification_backend.rs +++ b/viper/src/verification_backend.rs @@ -10,6 +10,7 @@ use std::fmt; pub enum VerificationBackend { Silicon, Carbon, + Lithium, } #[derive(Clone, Debug)] @@ -31,6 +32,7 @@ impl std::str::FromStr for VerificationBackend { match backend.to_lowercase().as_str() { "silicon" => Ok(VerificationBackend::Silicon), "carbon" => Ok(VerificationBackend::Carbon), + "lithium" => Ok(VerificationBackend::Lithium), _ => Err(UknownBackendError(backend.to_string())), } } @@ -41,6 +43,7 @@ impl fmt::Display for VerificationBackend { match self { VerificationBackend::Silicon => write!(f, "Silicon"), VerificationBackend::Carbon => write!(f, "Carbon"), + VerificationBackend::Lithium => write!(f, "Lithium"), } } } diff --git a/viper/src/verifier.rs b/viper/src/verifier.rs index 93f7b587d50..3a91512bcd5 100644 --- a/viper/src/verifier.rs +++ b/viper/src/verifier.rs @@ -5,16 +5,13 @@ // file, You can obtain one at http://mozilla.org/MPL/2.0/. use crate::{ - ast_factory::*, - ast_utils::AstUtils, - jni_utils::JniUtils, - silicon_counterexample::SiliconCounterexample, - smt_manager::SmtManager, - verification_backend::VerificationBackend, - verification_result::{VerificationError, VerificationResult}, + ast_factory::*, ast_utils::AstUtils, jni_utils::JniUtils, silicon_counterexample, + smt_manager::SmtManager, verification_backend::VerificationBackend, }; +use backend_common::{SiliconCounterexample, VerificationError, VerificationResult}; use jni::{objects::JObject, JNIEnv}; use log::{debug, error, info}; +use prusti_utils::run_timed; use std::path::PathBuf; use viper_sys::wrappers::{scala, viper::*}; @@ -56,6 +53,9 @@ impl<'a> Verifier<'a> { VerificationBackend::Carbon => { carbon::CarbonFrontendAPI::with(env).new(reporter) } + VerificationBackend::Lithium => { + unreachable!("Lithium is not a JVM-based backend") + } } }; let frontend_instance = jni.unwrap_result(unwrapped_frontend_instance); @@ -222,7 +222,7 @@ impl<'a> Verifier<'a> { "viper/silicon/interfaces/SiliconMappedCounterexample", ) { // only mapped counterexamples are processed - Some(SiliconCounterexample::new( + Some(silicon_counterexample( self.env, self.jni, original_counterexample, diff --git a/viper/tests/invalid_programs.rs b/viper/tests/invalid_programs.rs index 13fb3caa2ad..707df652b08 100644 --- a/viper/tests/invalid_programs.rs +++ b/viper/tests/invalid_programs.rs @@ -1,3 +1,4 @@ +use backend_common::VerificationResult; use std::sync::Once; use viper::*; diff --git a/viper/tests/multiple_errors.rs b/viper/tests/multiple_errors.rs index e7391c3b1bf..ec1472e207c 100644 --- a/viper/tests/multiple_errors.rs +++ b/viper/tests/multiple_errors.rs @@ -1,3 +1,4 @@ +use backend_common::VerificationResult; use std::{sync::Once, vec}; use viper::*; diff --git a/viper/tests/simple_programs.rs b/viper/tests/simple_programs.rs index 798f284c63a..7514453a408 100644 --- a/viper/tests/simple_programs.rs +++ b/viper/tests/simple_programs.rs @@ -1,3 +1,4 @@ +use backend_common::VerificationResult; use std::sync::Once; use viper::*; diff --git a/vir/defs/high/operations_internal/expression.rs b/vir/defs/high/operations_internal/expression.rs index 72cdd733cdc..e87b62f0458 100644 --- a/vir/defs/high/operations_internal/expression.rs +++ b/vir/defs/high/operations_internal/expression.rs @@ -354,7 +354,7 @@ impl Expression { // (2) rename with a fresh name the quantified variables that conflict with `dst`. for (src, dst) in self.replacements.iter() { if quantifier.variables.contains(&src.get_base()) - || quantifier.variables.contains(&dst.get_base()) + || (dst.is_place() && quantifier.variables.contains(&dst.get_base())) { unimplemented!( "replace_multiple_places doesn't handle replacements that conflict \ @@ -429,6 +429,11 @@ impl Expression { base: box Expression::AddrOf(AddrOf { base, .. }), .. }) => *base, + Expression::Deref(Deref { + base, + ty: Type::Closure(_), + .. + }) => *base, Expression::Field(Field { field, base: box Expression::Constructor(Constructor { arguments, .. }), diff --git a/vir/defs/low/ast/expression.rs b/vir/defs/low/ast/expression.rs index 90cefcd028c..d8148d235ef 100644 --- a/vir/defs/low/ast/expression.rs +++ b/vir/defs/low/ast/expression.rs @@ -65,6 +65,8 @@ pub struct Constant { pub enum ConstantValue { Bool(bool), Int(i64), + Float32(u32), + Float64(u64), BigInt(String), } @@ -105,6 +107,7 @@ pub struct Unfolding { pub position: Position, } +#[derive(Copy)] pub enum UnaryOpKind { Not, Minus, @@ -172,6 +175,7 @@ pub struct ContainerOp { pub position: Position, } +#[derive(Copy)] pub enum ContainerOpKind { SeqEmpty, SeqConstructor, diff --git a/vir/defs/low/ast/ty.rs b/vir/defs/low/ast/ty.rs index c8952156e63..a824f0768a3 100644 --- a/vir/defs/low/ast/ty.rs +++ b/vir/defs/low/ast/ty.rs @@ -17,6 +17,7 @@ pub enum Type { Domain(Domain), } +#[derive(Copy)] pub enum Float { F32, F64, diff --git a/vir/src/low/macros.rs b/vir/src/low/macros.rs index 302071ab05c..ad2e2cb49f5 100644 --- a/vir/src/low/macros.rs +++ b/vir/src/low/macros.rs @@ -1,5 +1,7 @@ pub macro ty { (Int) => {$crate::low::ast::ty::Type::Int}, + (Float32) => {$crate::low::ast::ty::Type::Float(crate::low::ast::ty::Float::F32)}, + (Float64) => {$crate::low::ast::ty::Type::Float(crate::low::ast::ty::Float::F64)}, (Bool) => {$crate::low::ast::ty::Type::Bool}, (Perm) => {$crate::low::ast::ty::Type::Perm}, (Place) => {$crate::low::ast::ty::Type::domain("Place".to_string())},