Skip to content

Commit

Permalink
Merge branch 'lithium-floats' into lithium
Browse files Browse the repository at this point in the history
  • Loading branch information
@JakuJ
JakuJ committed Mar 20, 2023
2 parents 1f5d2ea + 82fa7b8 commit 4838124
Show file tree
Hide file tree
Showing 17 changed files with 620 additions and 127 deletions.
3 changes: 1 addition & 2 deletions native-verifier/src/fol.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -132,8 +132,7 @@ fn vir_statement_to_fol_statements(
Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())],
Statement::LogEvent(_) => vec![], // TODO: Embed in SMT-LIB code
_ => {
log::warn!("Statement {:?} not yet supported", statement);
vec![]
unimplemented!("Statement {:?} not yet supported", statement);
}
}
}
Expand Down
154 changes: 131 additions & 23 deletions native-verifier/src/smt_lib.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ use vir::{
common::position::Positioned,
low::{
ast::{expression::*, ty::*},
operations::ty::Typed,
*,
},
};
Expand All @@ -19,24 +20,27 @@ lazy_static! {
static ref TWO_PARAM_RE: Regex = Regex::new(r"Map<([^>]+)\s*,\s*([^>]+)>").unwrap();
}

const SMT_PREAMBLE: &str = include_str!("theories/Preamble.smt2");
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<String>,
func_decls: Vec<String>,
code: Vec<String>,
methods: HashMap<String, MethodDecl>,
blocks: HashMap<String, BasicBlock>,
using_z3: bool,
}

impl SMTLib {
pub fn new() -> Self {
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) {
Expand Down Expand Up @@ -191,7 +195,11 @@ impl SMTLib {
impl ToString for SMTLib {
fn to_string(&self) -> String {
let mut result = String::new();
result.push_str(SMT_PREAMBLE);
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");
Expand Down Expand Up @@ -343,7 +351,7 @@ impl SMTTranslatable for DomainAxiomDecl {
smt.add_assert(format!("; {}", comment));
}

smt.add_assert(self.body.to_smt());
smt.add_code(format!("(assert {}) ; {}", self.body.to_smt(), self.name));
}
}

Expand Down Expand Up @@ -430,29 +438,80 @@ impl SMTTranslatable for Expression {
Expression::Constant(constant) => match &constant.value {
ConstantValue::Bool(bool) => bool.to_string(),
ConstantValue::Int(i64) => i64.to_string(),
ConstantValue::Float32(u32) => {
let bits = u32.to_le_bytes();
let bits = bits
.iter()
.rev()
.map(|b| format!("{:08b}", b))
.collect::<Vec<_>>()
.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::<Vec<_>>()
.join("");
format!(
"(fp #b{} #b{} #b{})",
&bits.chars().next().unwrap(),
&bits[1..=11],
&bits[12..=63]
)
}
ConstantValue::BigInt(s) => s.clone(),
},
Expression::MagicWand(_) => unimplemented!("Magic wands are not supported"),
Expression::MagicWand(wand) => {
warn!("MagicWand not supported: {}", wand);
format!("(=> {} {})", wand.left.to_smt(), wand.right.to_smt())
}
Expression::PredicateAccessPredicate(_access) => {
// TODO: access predicates for predicates
warn!("PredicateAccessPredicate not supported");
"".to_string()
warn!("PredicateAccessPredicate not supported: {}", _access);
format!(
"({} {})",
_access.name,
_access
.arguments
.iter()
.map(|x| x.to_smt())
.collect::<Vec<_>>()
.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!(
"({} {})",
unary_op.op_kind.to_smt(),
unary_op.argument.to_smt()
"({} {} {})",
op_smt,
binary_op.left.to_smt(),
binary_op.right.to_smt()
)
}
Expression::BinaryOp(binary_op) => format!(
"({} {} {})",
binary_op.op_kind.to_smt(),
binary_op.left.to_smt(),
binary_op.right.to_smt()
),
Expression::PermBinaryOp(perm_binary_op) => format!(
"({} {} {})",
perm_binary_op.op_kind.to_smt(),
Expand Down Expand Up @@ -481,15 +540,26 @@ impl SMTTranslatable for Expression {
);
quant.push_str(") ");

if quantifier.triggers.is_empty() {
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_str(")");
} else {
// triggers are :pattern
quant.push_str("(!");
quant.push_str(&quantifier.body.to_smt());

for trigger in &quantifier.triggers {
for trigger in &triggers {
quant.push_str(" :pattern (");

quant.push_str(
Expand Down Expand Up @@ -521,9 +591,12 @@ impl SMTTranslatable for Expression {
}
}

impl SMTTranslatable for BinaryOpKind {
struct IntBinaryOpKind(BinaryOpKind);
struct FloatBinaryOpKind(BinaryOpKind, Float);

impl SMTTranslatable for IntBinaryOpKind {
fn to_smt(&self) -> String {
match self {
match self.0 {
BinaryOpKind::EqCmp => "=",
BinaryOpKind::NeCmp => "distinct",
BinaryOpKind::GtCmp => ">",
Expand All @@ -543,6 +616,28 @@ impl SMTTranslatable for BinaryOpKind {
}
}

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 {
Expand All @@ -555,16 +650,29 @@ impl SMTTranslatable for PermBinaryOpKind {
}
}

impl SMTTranslatable for UnaryOpKind {
struct IntUnaryOpKind(UnaryOpKind);
struct FloatUnaryOpKind(UnaryOpKind);

impl SMTTranslatable for IntUnaryOpKind {
fn to_smt(&self) -> String {
match self {
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 {
Expand Down
38 changes: 6 additions & 32 deletions native-verifier/src/theories/Preamble.smt2
View file
Original file line number Diff line number Diff line change
@@ -1,37 +1,11 @@
; ===== Static preamble =====

(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 1000)
(set-logic ALL)

; --- Floating-point arithmetic ---

(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)))

; --- Snapshots ---

Expand Down
Loading

0 comments on commit 4838124

Please sign in to comment.