Skip to content

Commit 4838124

Browse files
JakuJJakuJ
committed
Merge branch 'lithium-floats' into lithium
2 parents 1f5d2ea + 82fa7b8 commit 4838124

File tree

17 files changed

+620
-127
lines changed

17 files changed

+620
-127
lines changed

‎native-verifier/src/fol.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -132,8 +132,7 @@ fn vir_statement_to_fol_statements(
132132
Statement::Comment(comment) => vec![FolStatement::Comment(comment.comment.clone())],
133133
Statement::LogEvent(_) => vec![], // TODO: Embed in SMT-LIB code
134134
_ => {
135-
log::warn!("Statement {:?} not yet supported", statement);
136-
vec![]
135+
unimplemented!("Statement {:?} not yet supported", statement);
137136
}
138137
}
139138
}

‎native-verifier/src/smt_lib.rs

Lines changed: 131 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ use vir::{
1010
common::position::Positioned,
1111
low::{
1212
ast::{expression::*, ty::*},
13+
operations::ty::Typed,
1314
*,
1415
},
1516
};
@@ -19,24 +20,27 @@ lazy_static! {
1920
static ref TWO_PARAM_RE: Regex = Regex::new(r"Map<([^>]+)\s*,\s*([^>]+)>").unwrap();
2021
}
2122

22-
const SMT_PREAMBLE: &str = include_str!("theories/Preamble.smt2");
23+
const NO_Z3_PREAMBLE: &str = include_str!("theories/Preamble.smt2");
24+
const Z3_PREAMBLE: &str = include_str!("theories/PreambleZ3.smt2");
2325

2426
pub struct SMTLib {
2527
sort_decls: Vec<String>,
2628
func_decls: Vec<String>,
2729
code: Vec<String>,
2830
methods: HashMap<String, MethodDecl>,
2931
blocks: HashMap<String, BasicBlock>,
32+
using_z3: bool,
3033
}
3134

3235
impl SMTLib {
33-
pub fn new() -> Self {
36+
pub fn new(using_z3: bool) -> Self {
3437
Self {
3538
sort_decls: Vec::new(),
3639
func_decls: Vec::new(),
3740
code: Vec::new(),
3841
methods: HashMap::new(),
3942
blocks: Default::default(),
43+
using_z3,
4044
}
4145
}
4246
fn add_sort_decl(&mut self, sort_decl: String) {
@@ -191,7 +195,11 @@ impl SMTLib {
191195
impl ToString for SMTLib {
192196
fn to_string(&self) -> String {
193197
let mut result = String::new();
194-
result.push_str(SMT_PREAMBLE);
198+
result.push_str(if self.using_z3 {
199+
Z3_PREAMBLE
200+
} else {
201+
NO_Z3_PREAMBLE
202+
});
195203
result.push_str("\n\n");
196204
result.push_str(&self.sort_decls.join("\n"));
197205
result.push_str("\n\n");
@@ -343,7 +351,7 @@ impl SMTTranslatable for DomainAxiomDecl {
343351
smt.add_assert(format!("; {}", comment));
344352
}
345353

346-
smt.add_assert(self.body.to_smt());
354+
smt.add_code(format!("(assert {}) ; {}", self.body.to_smt(), self.name));
347355
}
348356
}
349357

@@ -430,29 +438,80 @@ impl SMTTranslatable for Expression {
430438
Expression::Constant(constant) => match &constant.value {
431439
ConstantValue::Bool(bool) => bool.to_string(),
432440
ConstantValue::Int(i64) => i64.to_string(),
441+
ConstantValue::Float32(u32) => {
442+
let bits = u32.to_le_bytes();
443+
let bits = bits
444+
.iter()
445+
.rev()
446+
.map(|b| format!("{:08b}", b))
447+
.collect::<Vec<_>>()
448+
.join("");
449+
format!(
450+
"(fp #b{} #b{} #b{})",
451+
&bits.chars().next().unwrap(),
452+
&bits[1..=8],
453+
&bits[9..=31]
454+
)
455+
}
456+
ConstantValue::Float64(u64) => {
457+
let bits = u64.to_le_bytes();
458+
let bits = bits
459+
.iter()
460+
.rev()
461+
.map(|b| format!("{:08b}", b))
462+
.collect::<Vec<_>>()
463+
.join("");
464+
format!(
465+
"(fp #b{} #b{} #b{})",
466+
&bits.chars().next().unwrap(),
467+
&bits[1..=11],
468+
&bits[12..=63]
469+
)
470+
}
433471
ConstantValue::BigInt(s) => s.clone(),
434472
},
435-
Expression::MagicWand(_) => unimplemented!("Magic wands are not supported"),
473+
Expression::MagicWand(wand) => {
474+
warn!("MagicWand not supported: {}", wand);
475+
format!("(=> {} {})", wand.left.to_smt(), wand.right.to_smt())
476+
}
436477
Expression::PredicateAccessPredicate(_access) => {
437-
// TODO: access predicates for predicates
438-
warn!("PredicateAccessPredicate not supported");
439-
"".to_string()
478+
warn!("PredicateAccessPredicate not supported: {}", _access);
479+
format!(
480+
"({} {})",
481+
_access.name,
482+
_access
483+
.arguments
484+
.iter()
485+
.map(|x| x.to_smt())
486+
.collect::<Vec<_>>()
487+
.join(" ")
488+
)
440489
}
441490
Expression::FieldAccessPredicate(_) => unimplemented!(),
442491
Expression::Unfolding(_) => unimplemented!(),
443492
Expression::UnaryOp(unary_op) => {
493+
let op_smt = if unary_op.argument.get_type().is_float() {
494+
FloatUnaryOpKind(unary_op.op_kind).to_smt()
495+
} else {
496+
IntUnaryOpKind(unary_op.op_kind).to_smt()
497+
};
498+
499+
format!("({} {})", op_smt, unary_op.argument.to_smt())
500+
}
501+
Expression::BinaryOp(binary_op) => {
502+
let op_smt = if let Type::Float(fsize) = binary_op.left.get_type() {
503+
FloatBinaryOpKind(binary_op.op_kind, *fsize).to_smt()
504+
} else {
505+
IntBinaryOpKind(binary_op.op_kind).to_smt()
506+
};
507+
444508
format!(
445-
"({} {})",
446-
unary_op.op_kind.to_smt(),
447-
unary_op.argument.to_smt()
509+
"({} {} {})",
510+
op_smt,
511+
binary_op.left.to_smt(),
512+
binary_op.right.to_smt()
448513
)
449514
}
450-
Expression::BinaryOp(binary_op) => format!(
451-
"({} {} {})",
452-
binary_op.op_kind.to_smt(),
453-
binary_op.left.to_smt(),
454-
binary_op.right.to_smt()
455-
),
456515
Expression::PermBinaryOp(perm_binary_op) => format!(
457516
"({} {} {})",
458517
perm_binary_op.op_kind.to_smt(),
@@ -481,15 +540,26 @@ impl SMTTranslatable for Expression {
481540
);
482541
quant.push_str(") ");
483542

484-
if quantifier.triggers.is_empty() {
543+
let triggers: Vec<_> = quantifier
544+
.triggers
545+
.iter()
546+
.filter(|t| {
547+
!t.terms
548+
.iter()
549+
.any(|t| matches!(t, Expression::PredicateAccessPredicate(_)))
550+
// TODO: Support triggers with predicate access predicates?
551+
})
552+
.collect();
553+
554+
if triggers.is_empty() {
485555
quant.push_str(&quantifier.body.to_smt());
486556
quant.push_str(")");
487557
} else {
488558
// triggers are :pattern
489559
quant.push_str("(!");
490560
quant.push_str(&quantifier.body.to_smt());
491561

492-
for trigger in &quantifier.triggers {
562+
for trigger in &triggers {
493563
quant.push_str(" :pattern (");
494564

495565
quant.push_str(
@@ -521,9 +591,12 @@ impl SMTTranslatable for Expression {
521591
}
522592
}
523593

524-
impl SMTTranslatable for BinaryOpKind {
594+
struct IntBinaryOpKind(BinaryOpKind);
595+
struct FloatBinaryOpKind(BinaryOpKind, Float);
596+
597+
impl SMTTranslatable for IntBinaryOpKind {
525598
fn to_smt(&self) -> String {
526-
match self {
599+
match self.0 {
527600
BinaryOpKind::EqCmp => "=",
528601
BinaryOpKind::NeCmp => "distinct",
529602
BinaryOpKind::GtCmp => ">",
@@ -543,6 +616,28 @@ impl SMTTranslatable for BinaryOpKind {
543616
}
544617
}
545618

619+
impl SMTTranslatable for FloatBinaryOpKind {
620+
fn to_smt(&self) -> String {
621+
match (self.0, self.1) {
622+
// BinaryOpKind::EqCmp => "fp.eq", // TODO: = in axioms, fp.eq in arithmetic?
623+
(BinaryOpKind::EqCmp, _) => "=",
624+
(BinaryOpKind::NeCmp, Float::F32) => "fp.neq32", // Not in SMT-LIB 2.6 standard, part of static preamble
625+
(BinaryOpKind::NeCmp, Float::F64) => "fp.neq64", // Not in SMT-LIB 2.6 standard, part of static preamble
626+
(BinaryOpKind::GtCmp, _) => "fp.gt",
627+
(BinaryOpKind::GeCmp, _) => "fp.geq",
628+
(BinaryOpKind::LtCmp, _) => "fp.lt",
629+
(BinaryOpKind::LeCmp, _) => "fp.leq",
630+
(BinaryOpKind::Add, _) => "fp.add roundNearestTiesToAway",
631+
(BinaryOpKind::Sub, _) => "fp.sub roundNearestTiesToAway",
632+
(BinaryOpKind::Mul, _) => "fp.mul roundNearestTiesToAway",
633+
(BinaryOpKind::Div, _) => "fp.div roundNearestTiesToAway",
634+
(BinaryOpKind::Mod, _) => "fp.rem",
635+
(other, _) => unreachable!("FP {}", other),
636+
}
637+
.to_string()
638+
}
639+
}
640+
546641
impl SMTTranslatable for PermBinaryOpKind {
547642
fn to_smt(&self) -> String {
548643
match self {
@@ -555,16 +650,29 @@ impl SMTTranslatable for PermBinaryOpKind {
555650
}
556651
}
557652

558-
impl SMTTranslatable for UnaryOpKind {
653+
struct IntUnaryOpKind(UnaryOpKind);
654+
struct FloatUnaryOpKind(UnaryOpKind);
655+
656+
impl SMTTranslatable for IntUnaryOpKind {
559657
fn to_smt(&self) -> String {
560-
match self {
658+
match self.0 {
561659
UnaryOpKind::Not => "not",
562660
UnaryOpKind::Minus => "-",
563661
}
564662
.to_string()
565663
}
566664
}
567665

666+
impl SMTTranslatable for FloatUnaryOpKind {
667+
fn to_smt(&self) -> String {
668+
match self.0 {
669+
UnaryOpKind::Not => unreachable!("FP not"),
670+
UnaryOpKind::Minus => "fp.neg",
671+
}
672+
.to_string()
673+
}
674+
}
675+
568676
impl SMTTranslatable for ContainerOp {
569677
fn to_smt(&self) -> String {
570678
match &self.kind {

‎native-verifier/src/theories/Preamble.smt2

Lines changed: 6 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,11 @@
11
; ===== Static preamble =====
22

3-
(set-option :global-decls true) ; Boogie: default
4-
(set-option :auto_config false) ; Usually a good idea
5-
(set-option :smt.restart_strategy 0)
6-
(set-option :smt.restart_factor |1.5|)
7-
(set-option :smt.case_split 3)
8-
(set-option :smt.delay_units true)
9-
(set-option :smt.delay_units_threshold 16)
10-
(set-option :nnf.sk_hack true)
11-
(set-option :type_check true)
12-
(set-option :smt.bv.reflect true)
13-
(set-option :smt.mbqi false)
14-
(set-option :smt.qi.cost "(+ weight generation)")
15-
(set-option :smt.qi.eager_threshold 1000)
16-
(set-option :smt.qi.max_multi_patterns 1000)
17-
(set-option :smt.phase_selection 0) ; default: 3, Boogie: 0
18-
(set-option :sat.phase caching)
19-
(set-option :sat.random_seed 0)
20-
(set-option :nlsat.randomize true)
21-
(set-option :nlsat.seed 0)
22-
(set-option :nlsat.shuffle_vars false)
23-
(set-option :fp.spacer.order_children 0) ; Not available with Z3 4.5
24-
(set-option :fp.spacer.random_seed 0) ; Not available with Z3 4.5
25-
(set-option :smt.arith.random_initial_value true) ; Boogie: true
26-
(set-option :smt.random_seed 0)
27-
(set-option :sls.random_offset true)
28-
(set-option :sls.random_seed 0)
29-
(set-option :sls.restart_init false)
30-
(set-option :sls.walksat_ucb true)
31-
(set-option :model.v2 true)
32-
(set-option :model.partial false)
33-
34-
(set-option :timeout 1000)
3+
(set-logic ALL)
4+
5+
; --- Floating-point arithmetic ---
6+
7+
(define-fun fp.neq32 ((x (_ FloatingPoint 8 24)) (y (_ FloatingPoint 8 24))) Bool (not (fp.eq x y)))
8+
(define-fun fp.neq64 ((x (_ FloatingPoint 11 53)) (y (_ FloatingPoint 11 53))) Bool (not (fp.eq x y)))
359

3610
; --- Snapshots ---
3711

0 commit comments

Comments
 (0)