From af9ef1b8252e507b6ec543bf84bf17981e35faae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Christian=20M=C3=B6sl?= <christian.moesl@live.at>
Date: Fri, 6 Nov 2020 14:06:10 +0100
Subject: [PATCH] feat: add Z3 SMT solver support (#68)
- also refactor the solver interface
- fix small bug in boolector interface
- improve toolchain setup description
---
.gitignore | 1 +
Cargo.lock | 29 ++++++-
Cargo.toml | 19 +++--
README.md | 34 +++++---
src/boolector.rs | 152 ++++++++++++++-------------------
src/cli.rs | 5 +-
src/engine.rs | 14 ++-
src/lib.rs | 1 +
src/main.rs | 14 +--
src/solver.rs | 194 +++++++++++++++++++++---------------------
src/symbolic_state.rs | 19 ++++-
src/z3.rs | 118 +++++++++++++++++++++++++
tests/engine.rs | 6 ++
13 files changed, 385 insertions(+), 221 deletions(-)
create mode 100644 src/z3.rs
diff --git a/.gitignore b/.gitignore
index 6ad9b1bb..7b621d8f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -6,3 +6,4 @@
**/*.png
**/*.s
.DS_Store
+.z3-trace
diff --git a/Cargo.lock b/Cargo.lock
index d933aa03..3ae60423 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,9 +2,9 @@
# It is not intended for manual editing.
[[package]]
name = "aho-corasick"
-version = "0.7.14"
+version = "0.7.15"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b476ce7103678b0c6d3d395dbbae31d48ff910bd28be979ba5d48c6351131d0d"
+checksum = "7404febffaa47dac81aa44dba71523c9d069b1bdc50a77db41195149e17f68e5"
dependencies = [
"memchr",
]
@@ -283,6 +283,7 @@ dependencies = [
"rand",
"riscv-decode",
"serial_test",
+ "z3",
]
[[package]]
@@ -352,9 +353,9 @@ checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6"
[[package]]
name = "ppv-lite86"
-version = "0.2.9"
+version = "0.2.10"
source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c36fa947111f5c62a733b652544dd0016a43ce89619538a8ef92724a6f501a20"
+checksum = "ac74c624d6b2d21f425f752262f42188365d7b8ff1aff74c82e45136510a4857"
[[package]]
name = "proc-macro-error"
@@ -632,3 +633,23 @@ name = "winapi-x86_64-pc-windows-gnu"
version = "0.4.0"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
+
+[[package]]
+name = "z3"
+version = "0.7.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "aa17be9852c6c2a8de2ea0875350dc5f8626f3eaa6b683148753b827f1b39ce5"
+dependencies = [
+ "lazy_static",
+ "log",
+ "z3-sys",
+]
+
+[[package]]
+name = "z3-sys"
+version = "0.6.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "afa18ba5fbd4933e41ffb440c3fd91f91fe9cdb7310cce3ddfb6648563811de0"
+dependencies = [
+ "cmake",
+]
diff --git a/Cargo.toml b/Cargo.toml
index c0971942..da72ce19 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -6,20 +6,21 @@ edition = "2018"
description = "Monster is a symbolic execution engine for 64-bit RISC-V code"
[dependencies]
-goblin = "0.2"
-byteorder = "1.3.4"
+goblin = "~0.2.3"
+byteorder = "~1.3.4"
clap = "3.0.0-beta.2"
riscv-decode = { git = "https://github.com/cksystemsgroup/riscv-decode" }
-petgraph = "0.5.1"
-rand = "0.7.3"
+petgraph = "~0.5.1"
+rand = "~0.7.3"
boolector = { version = "0.4", git = "https://github.com/finga/boolector-rs", branch = "boolector-src", features = ["vendored"] }
-modinverse = "0.1.1"
-log = "0.4"
-env_logger = "0.8.1"
-bytesize = "1.0.1"
+z3 = { version = "~0.7.1", features = ["static-link-z3"] }
+modinverse = "~0.1.1"
+log = "~0.4.11"
+env_logger = "~0.8.1"
+bytesize = "~1.0.1"
[dev-dependencies]
-serial_test = "0.4.0"
+serial_test = "~0.4.0"
[dev-dependencies.cargo-husky]
version = "1"
diff --git a/README.md b/README.md
index 90a67941..547147c0 100644
--- a/README.md
+++ b/README.md
@@ -1,8 +1,9 @@
# monster
Monster is a symbolic execution engine for 64-bit RISC-V code
-# Toolchain setup
-## Install rust
+### Toolchain setup
+
+#### Linux and Unix-like OS
1. Bootstrap rust
```
$ curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
@@ -21,25 +22,31 @@ $ echo 'export PATH="$HOME/.cargo/bin:$PATH"' >> ~/.zshrc && source ~/.zshrc
$ cargo install cross
$ cargo install mdbook
$ cargo install mdbook-linkcheck
-$ cargo install --git https://github.com/christianmoesl/mdbook-graphviz
+$ cargo install mdbook-graphviz
```
+5. install Docker and LLVM with your favorite package manager
-## Docker and llvm
-### Debian based
-5. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/engine/install/debian/)
-6. Make sure you have a recent version of clang/llvm (>= v9) installed:
+##### MacOS
+6. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/docker-for-mac/install/)
```
-$ apt install llvm
+$ brew cask install docker
```
-
-### Mac
-5. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/docker-for-mac/install/)
-6. Make sure you have a recent version of clang/llvm (>= v9) installed:
+7. Make sure you have a recent version of clang/llvm (>= v9) installed:
```
$ brew install llvm
```
-## Build and test
+##### Debian based
+6. Install docker (needed by cross) with [this installation guide](https://docs.docker.com/engine/install/debian/)
+7. Make sure you have a recent version of clang/llvm (>= v9) installed:
+```
+$ apt install llvm
+```
+
+#### Windows
+We do not support Windows directly. But someone can use WSL2 to run/develop for Monster.
+
+### Build and Test from Source
7. Test your toolchain setup by compiling monster:
```
$ cargo build --locked
@@ -48,3 +55,4 @@ $ cargo build --locked
```
$ cargo test --locked
```
+
diff --git a/src/boolector.rs b/src/boolector.rs
index 4c9027d1..920ef15f 100644
--- a/src/boolector.rs
+++ b/src/boolector.rs
@@ -1,127 +1,101 @@
use crate::bitvec::BitVector;
use crate::solver::{Assignment, Solver};
use crate::symbolic_state::{
- BVOperator, Formula,
+ get_operands, BVOperator, Formula,
Node::{Constant, Input, Operator},
- OperandSide,
+ SymbolId,
};
use boolector::{
option::{BtorOption, ModelGen, OutputFileFormat},
Btor, SolverResult, BV,
};
-use log::debug;
-use petgraph::{graph::NodeIndex, Direction};
use std::collections::HashMap;
use std::rc::Rc;
-fn solve(graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
- let solver = Rc::new(Btor::new());
- solver.set_opt(BtorOption::ModelGen(ModelGen::All));
- solver.set_opt(BtorOption::Incremental(true));
- solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2));
-
- let mut bvs = HashMap::new();
- let bv = traverse(graph, root, &solver, &mut bvs);
- bv.assert();
+pub struct Boolector {}
- if let SolverResult::Sat = solver.sat() {
- let assignments = graph
- .node_indices()
- .map(|i| BitVector(bvs.get(&i).unwrap().get_a_solution().as_u64().unwrap()))
- .collect();
+impl Boolector {
+ pub fn new() -> Self {
+ Self {}
+ }
+}
- Some(assignments)
- } else {
- None
+impl Default for Boolector {
+ fn default() -> Self {
+ Self::new()
}
}
-fn get_operands(
- graph: &Formula,
- node: NodeIndex,
- solver: &Rc<Btor>,
- bvs: &mut HashMap<NodeIndex, BV<Rc<Btor>>>,
-) -> (BV<Rc<Btor>>, Option<BV<Rc<Btor>>>) {
- let mut operands = graph.neighbors_directed(node, Direction::Incoming).detach();
+impl Solver for Boolector {
+ fn name() -> &'static str {
+ "Boolector"
+ }
- match operands.next(graph) {
- Some(p) if graph[p.0] == OperandSide::Lhs => (traverse(graph, p.1, solver, bvs), {
- if let Some(node) = operands.next(graph) {
- Some(traverse(graph, node.1, solver, bvs))
- } else {
- None
- }
- }),
- Some(p) if graph[p.0] == OperandSide::Rhs => (
- traverse(graph, p.1, solver, bvs),
- if let Some(node) = operands.next(graph) {
- Some(traverse(graph, node.1, solver, bvs))
- } else {
- None
- },
- ),
- _ => unreachable!(),
+ fn solve_impl(&mut self, graph: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+ let solver = Rc::new(Btor::new());
+ solver.set_opt(BtorOption::ModelGen(ModelGen::All));
+ solver.set_opt(BtorOption::Incremental(true));
+ solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2));
+
+ let mut bvs = HashMap::new();
+ let bv = traverse(graph, root, &solver, &mut bvs);
+ bv.assert();
+
+ if let SolverResult::Sat = solver.sat() {
+ let assignments = graph
+ .node_indices()
+ .filter(|i| matches!(graph[*i], Input(_)))
+ .map(|i| BitVector(bvs.get(&i).unwrap().get_a_solution().as_u64().unwrap()))
+ .collect();
+
+ Some(assignments)
+ } else {
+ None
+ }
}
}
fn traverse<'a>(
graph: &Formula,
- node: NodeIndex,
+ node: SymbolId,
solver: &'a Rc<Btor>,
- bvs: &mut HashMap<NodeIndex, BV<Rc<Btor>>>,
+ bvs: &mut HashMap<SymbolId, BV<Rc<Btor>>>,
) -> BV<Rc<Btor>> {
- let bv = match &graph[node] {
- Operator(op) => {
- match get_operands(graph, node, solver, bvs) {
+ let bv =
+ match &graph[node] {
+ Operator(op) => match get_operands(graph, node) {
(lhs, Some(rhs)) => {
match op {
- BVOperator::Add => lhs.add(&rhs),
- BVOperator::Sub => lhs.sub(&rhs),
- BVOperator::Mul => lhs.mul(&rhs),
- BVOperator::Equals => lhs._eq(&rhs),
- BVOperator::BitwiseAnd => lhs.and(&rhs),
- //BVOperator::GreaterThan => lhs.ugt(&rhs),
+ BVOperator::Add => traverse(graph, lhs, solver, bvs)
+ .add(&traverse(graph, rhs, solver, bvs)),
+ BVOperator::Sub => traverse(graph, lhs, solver, bvs)
+ .sub(&traverse(graph, rhs, solver, bvs)),
+ BVOperator::Mul => traverse(graph, lhs, solver, bvs)
+ .mul(&traverse(graph, rhs, solver, bvs)),
+ BVOperator::Equals => traverse(graph, lhs, solver, bvs)
+ ._eq(&traverse(graph, rhs, solver, bvs)),
+ BVOperator::BitwiseAnd => traverse(graph, lhs, solver, bvs)
+ .and(&traverse(graph, rhs, solver, bvs)),
i => unimplemented!("binary operator: {:?}", i),
}
}
(lhs, None) => match op {
- BVOperator::Not => lhs._eq(&BV::from_u64(solver.clone(), 0, 1)),
+ BVOperator::Not => {
+ traverse(graph, lhs, solver, bvs)._eq(&BV::from_u64(solver.clone(), 0, 1))
+ }
i => unimplemented!("unary operator: {:?}", i),
},
+ },
+ Input(name) => {
+ if let Some(value) = bvs.get(&node) {
+ value.clone()
+ } else {
+ BV::new(solver.clone(), 64, Some(name))
+ }
}
- }
- Input(name) => {
- if let Some(value) = bvs.get(&node) {
- value.clone()
- } else {
- BV::new(solver.clone(), 64, Some(name))
- }
- }
- Constant(c) => BV::from_u64(solver.clone(), *c, 64),
- };
+ Constant(c) => BV::from_u64(solver.clone(), *c, 64),
+ };
bvs.insert(node, bv.clone());
bv
}
-
-pub struct Boolector {}
-
-impl Boolector {
- pub fn new() -> Self {
- Self {}
- }
-}
-
-impl Default for Boolector {
- fn default() -> Self {
- Self::new()
- }
-}
-
-impl Solver for Boolector {
- fn solve(&mut self, graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
- debug!("try to solve with Boolector");
-
- time_debug!("finished solving formula", { solve(graph, root) })
- }
-}
diff --git a/src/cli.rs b/src/cli.rs
index 494d7b79..ccc5ee75 100644
--- a/src/cli.rs
+++ b/src/cli.rs
@@ -1,6 +1,7 @@
use clap::{crate_authors, crate_description, crate_name, crate_version, App, AppSettings, Arg};
pub const LOGGING_LEVELS: [&str; 5] = ["trace", "debug", "info", "warn", "error"];
+pub const SOLVER: [&str; 3] = ["monster", "boolector", "z3"];
pub fn args() -> App<'static> {
App::new(crate_name!())
@@ -70,8 +71,8 @@ pub fn args() -> App<'static> {
.short('s')
.long("solver")
.takes_value(true)
- .possible_values(&["monster", "boolector"])
- .default_value("monster"),
+ .possible_values(&SOLVER)
+ .default_value(SOLVER[0]),
),
)
.setting(AppSettings::SubcommandRequiredElseHelp)
diff --git a/src/engine.rs b/src/engine.rs
index 9a6e7a01..0804d17b 100644
--- a/src/engine.rs
+++ b/src/engine.rs
@@ -4,8 +4,9 @@ use crate::{
cfg::build_cfg_from_file,
elf::Program,
exploration_strategy::{ExplorationStrategy, ShortestPathStrategy},
- solver::{NativeSolver, Solver},
+ solver::{MonsterSolver, Solver},
symbolic_state::{Query, SymbolId, SymbolicState},
+ z3::Z3,
};
use byteorder::{ByteOrder, LittleEndian};
use bytesize::ByteSize;
@@ -25,6 +26,7 @@ pub enum SyscallId {
pub enum Backend {
Monster,
Boolector,
+ Z3,
}
// TODO: What should the engine return as result?
@@ -35,7 +37,7 @@ pub fn execute(input: &Path, with: Backend) -> Result<(), String> {
match with {
Backend::Monster => {
- let solver = Rc::new(RefCell::new(NativeSolver::new()));
+ let solver = Rc::new(RefCell::new(MonsterSolver::new()));
let state = Box::new(SymbolicState::new(solver));
let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
@@ -48,6 +50,14 @@ pub fn execute(input: &Path, with: Backend) -> Result<(), String> {
let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
+ executor.run();
+ }
+ Backend::Z3 => {
+ let solver = Rc::new(RefCell::new(Z3::new()));
+ let state = Box::new(SymbolicState::new(solver));
+
+ let mut executor = Engine::new(ByteSize::mib(1), &program, &mut strategy, state);
+
executor.run();
}
}
diff --git a/src/lib.rs b/src/lib.rs
index 803a995d..cea785fc 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -12,3 +12,4 @@ pub mod exploration_strategy;
pub mod solver;
pub mod symbolic_state;
pub mod ternary;
+pub mod z3;
diff --git a/src/main.rs b/src/main.rs
index a4357e4a..fe9bfc3f 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -61,11 +61,15 @@ fn main() {
let input = Path::new(args.value_of("input-file").unwrap());
let solver = args.value_of("solver").unwrap();
- match solver {
- "monster" => engine::execute(input, engine::Backend::Monster),
- "boolector" => engine::execute(input, engine::Backend::Boolector),
- _ => unreachable!(),
- }
+ engine::execute(
+ input,
+ match solver {
+ "monster" => engine::Backend::Monster,
+ "boolector" => engine::Backend::Boolector,
+ "z3" => engine::Backend::Z3,
+ _ => unreachable!(),
+ },
+ )
});
}
_ => unreachable!(),
diff --git a/src/solver.rs b/src/solver.rs
index fb5638cf..922a8fcd 100644
--- a/src/solver.rs
+++ b/src/solver.rs
@@ -1,7 +1,7 @@
#![allow(clippy::many_single_char_names)]
use crate::bitvec::*;
-use crate::symbolic_state::{BVOperator, Formula, Node, OperandSide, SymbolId as NodeIndex};
+use crate::symbolic_state::{get_operands, BVOperator, Formula, Node, OperandSide, SymbolId};
use crate::ternary::*;
use log::{debug, log_enabled, trace, Level};
use petgraph::{visit::EdgeRef, Direction};
@@ -10,38 +10,46 @@ use rand::{random, Rng};
pub type Assignment<T> = Vec<T>;
pub trait Solver {
- fn solve(&mut self, formula: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>>;
+ fn name() -> &'static str;
+
+ fn solve(&mut self, formula: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+ debug!("try to solve with {} solver", Self::name());
+
+ time_debug!("finished solving formula", {
+ self.solve_impl(formula, root)
+ })
+ }
+
+ fn solve_impl(&mut self, formula: &Formula, root: SymbolId) -> Option<Assignment<BitVector>>;
}
-pub struct NativeSolver {}
+pub struct MonsterSolver {}
-impl Default for NativeSolver {
+impl Default for MonsterSolver {
fn default() -> Self {
Self::new()
}
}
-impl NativeSolver {
+impl MonsterSolver {
pub fn new() -> Self {
Self {}
}
}
-impl Solver for NativeSolver {
- fn solve(&mut self, formula: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
- debug!("try to solve with native solver");
-
- time_debug!("finished solving formula", { solve(formula, root) })
+impl Solver for MonsterSolver {
+ fn name() -> &'static str {
+ "Monster"
}
-}
-pub fn solve(formula: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> {
- let ab = initialize_ab(formula);
- let at = compute_at(formula);
+ fn solve_impl(&mut self, formula: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+ let ab = initialize_ab(formula);
+ let at = compute_at(formula);
- let result = sat(formula, root, at, ab);
+ let result = sat(formula, root, at, ab);
- Some(result)
+ Some(result)
+ }
}
// short-circuiting implies
@@ -107,7 +115,7 @@ fn is_consistent(op: BVOperator, x: TernaryBitVector, t: BitVector) -> bool {
}
}
-fn is_leaf(formula: &Formula, idx: NodeIndex) -> bool {
+fn is_leaf(formula: &Formula, idx: SymbolId) -> bool {
let incoming = formula.edges_directed(idx, Direction::Incoming).count();
incoming == 0
@@ -165,30 +173,32 @@ fn initialize_ab(formula: &Formula) -> Assignment<BitVector> {
// otherwise selects an input undeterministically
fn select(
f: &Formula,
- idx: NodeIndex,
+ idx: SymbolId,
t: BitVector,
at: &[TernaryBitVector],
ab: &[BitVector],
-) -> (NodeIndex, NodeIndex, OperandSide) {
- let (lhs, rhs) = parents(f, idx);
-
- fn is_constant(f: &Formula, n: NodeIndex) -> bool {
- matches!(f[n], Node::Constant(_))
- }
+) -> (SymbolId, SymbolId, OperandSide) {
+ if let (lhs, Some(rhs)) = get_operands(f, idx) {
+ fn is_constant(f: &Formula, n: SymbolId) -> bool {
+ matches!(f[n], Node::Constant(_))
+ }
- #[allow(clippy::if_same_then_else)]
- if is_constant(f, lhs) {
- (rhs, lhs, OperandSide::Rhs)
- } else if is_constant(f, rhs) {
- (lhs, rhs, OperandSide::Lhs)
- } else if is_essential(f, lhs, OperandSide::Lhs, rhs, t, at, ab) {
- (lhs, rhs, OperandSide::Lhs)
- } else if is_essential(f, rhs, OperandSide::Rhs, lhs, t, at, ab) {
- (rhs, lhs, OperandSide::Rhs)
- } else if random() {
- (rhs, lhs, OperandSide::Rhs)
+ #[allow(clippy::if_same_then_else)]
+ if is_constant(f, lhs) {
+ (rhs, lhs, OperandSide::Rhs)
+ } else if is_constant(f, rhs) {
+ (lhs, rhs, OperandSide::Lhs)
+ } else if is_essential(f, lhs, OperandSide::Lhs, rhs, t, at, ab) {
+ (lhs, rhs, OperandSide::Lhs)
+ } else if is_essential(f, rhs, OperandSide::Rhs, lhs, t, at, ab) {
+ (rhs, lhs, OperandSide::Rhs)
+ } else if random() {
+ (rhs, lhs, OperandSide::Rhs)
+ } else {
+ (lhs, rhs, OperandSide::Lhs)
+ }
} else {
- (lhs, rhs, OperandSide::Lhs)
+ panic!("can only select path for binary operators")
}
}
@@ -314,9 +324,9 @@ const CHOOSE_INVERSE: f64 = 0.90;
#[allow(clippy::too_many_arguments)]
fn value(
f: &Formula,
- n: NodeIndex,
- nx: NodeIndex,
- ns: NodeIndex,
+ n: SymbolId,
+ nx: SymbolId,
+ ns: SymbolId,
side: OperandSide,
t: BitVector,
at: &[TernaryBitVector],
@@ -349,9 +359,9 @@ fn value(
fn is_essential(
formula: &Formula,
- this: NodeIndex,
+ this: SymbolId,
on_side: OperandSide,
- other: NodeIndex,
+ other: SymbolId,
t: BitVector,
at: &[TernaryBitVector],
ab: &[BitVector],
@@ -366,28 +376,14 @@ fn is_essential(
}
}
-fn parent(f: &Formula, n: NodeIndex) -> NodeIndex {
+fn get_operand(f: &Formula, n: SymbolId) -> SymbolId {
f.edges_directed(n, Direction::Incoming)
.next()
.unwrap()
.source()
}
-fn parents(f: &Formula, n: NodeIndex) -> (NodeIndex, NodeIndex) {
- fn target_by_side(f: &Formula, n: NodeIndex, side: OperandSide) -> NodeIndex {
- f.edges_directed(n, Direction::Incoming)
- .find(|e| *e.weight() == side)
- .unwrap()
- .source()
- }
-
- let lhs = target_by_side(f, n, OperandSide::Lhs);
- let rhs = target_by_side(f, n, OperandSide::Rhs);
-
- (lhs, rhs)
-}
-
-fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex, v: BitVector) {
+fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, v: BitVector) {
ab[n.index()] = v;
trace!("update: x{} <- {:#x}", n.index(), v.0);
@@ -396,49 +392,53 @@ fn update_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex,
.for_each(|n| propagate_assignment(f, ab, n));
}
-fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex) {
- fn update_binary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex, s: &str, op: Op)
+fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId) {
+ fn update_binary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, s: &str, op: Op)
where
Op: FnOnce(BitVector, BitVector) -> BitVector,
{
- let (lhs, rhs) = parents(f, n);
-
- let result = op(ab[lhs.index()], ab[rhs.index()]);
-
- trace!(
- "propagate: x{} := x{}({:#x}) {} x{}({:#x}) |- x{} <- {:#x}",
- n.index(),
- lhs.index(),
- ab[lhs.index()].0,
- s,
- rhs.index(),
- ab[rhs.index()].0,
- n.index(),
- result.0
- );
+ if let (lhs, Some(rhs)) = get_operands(f, n) {
+ let result = op(ab[lhs.index()], ab[rhs.index()]);
+
+ trace!(
+ "propagate: x{} := x{}({:#x}) {} x{}({:#x}) |- x{} <- {:#x}",
+ n.index(),
+ lhs.index(),
+ ab[lhs.index()].0,
+ s,
+ rhs.index(),
+ ab[rhs.index()].0,
+ n.index(),
+ result.0
+ );
- ab[n.index()] = result;
+ ab[n.index()] = result;
+ } else {
+ panic!("can not update binary operator with 1 operand")
+ }
}
- fn update_unary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeIndex, s: &str, op: Op)
+ fn update_unary<Op>(f: &Formula, ab: &mut Assignment<BitVector>, n: SymbolId, s: &str, op: Op)
where
Op: FnOnce(BitVector) -> BitVector,
{
- let p = parent(f, n);
-
- let result = op(ab[p.index()]);
+ if let (p, None) = get_operands(f, n) {
+ let result = op(ab[p.index()]);
- trace!(
- "propagate: x{} := {}x{}({:#x}) |- x{} <- {:#x}",
- n.index(),
- s,
- p.index(),
- ab[p.index()].0,
- n.index(),
- result.0
- );
+ trace!(
+ "propagate: x{} := {}x{}({:#x}) |- x{} <- {:#x}",
+ n.index(),
+ s,
+ p.index(),
+ ab[p.index()].0,
+ n.index(),
+ result.0
+ );
- ab[n.index()] = result;
+ ab[n.index()] = result;
+ } else {
+ panic!("can not update unary operator with more than one operand")
+ }
}
match &f[n] {
@@ -474,7 +474,7 @@ fn propagate_assignment(f: &Formula, ab: &mut Assignment<BitVector>, n: NodeInde
// can only handle one Equals constrain with constant
fn sat(
formula: &Formula,
- root: NodeIndex,
+ root: SymbolId,
at: Assignment<TernaryBitVector>,
mut ab: Assignment<BitVector>,
) -> Assignment<BitVector> {
@@ -491,7 +491,7 @@ fn sat(
let (v, nx) = match formula[n] {
Node::Operator(op) => {
if op.is_unary() {
- let nx = parent(formula, n);
+ let nx = get_operand(formula, n);
let x = at[nx.index()];
@@ -575,7 +575,7 @@ fn sat(
mod tests {
use super::*;
- fn create_formula_with_input() -> (Formula, NodeIndex) {
+ fn create_formula_with_input() -> (Formula, SymbolId) {
let mut formula = Formula::new();
let input = Node::Input(String::from("x0"));
@@ -586,10 +586,10 @@ mod tests {
fn add_equals_constrain(
formula: &mut Formula,
- to: NodeIndex,
+ to: SymbolId,
on: OperandSide,
constant: u64,
- ) -> NodeIndex {
+ ) -> SymbolId {
let constrain = Node::Operator(BVOperator::Equals);
let constrain_idx = formula.add_node(constrain);
@@ -608,7 +608,8 @@ mod tests {
let root = add_equals_constrain(&mut formula, input_idx, OperandSide::Lhs, 10);
- let result = solve(&formula, root);
+ let mut solver = MonsterSolver::default();
+ let result = solver.solve(&formula, root);
assert!(result.is_some(), "has result for trivial equals constrain");
assert_eq!(
@@ -633,7 +634,8 @@ mod tests {
let root = add_equals_constrain(&mut formula, instr_idx, OperandSide::Lhs, 10);
- let result = solve(&formula, root);
+ let mut solver = MonsterSolver::default();
+ let result = solver.solve(&formula, root);
assert!(result.is_some(), "has result for trivial add op");
assert_eq!(
diff --git a/src/symbolic_state.rs b/src/symbolic_state.rs
index 401c1d1b..a60f019c 100644
--- a/src/symbolic_state.rs
+++ b/src/symbolic_state.rs
@@ -73,6 +73,7 @@ pub enum Node {
Operator(BVOperator),
}
+pub type Formula = Graph<Node, OperandSide>;
pub type SymbolId = NodeIndex;
fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator {
@@ -85,7 +86,23 @@ fn instruction_to_bv_operator(instruction: Instruction) -> BVOperator {
}
}
-pub type Formula = Graph<Node, OperandSide>;
+pub fn get_operands(graph: &Formula, sym: SymbolId) -> (SymbolId, Option<SymbolId>) {
+ let mut iter = graph.neighbors_directed(sym, Direction::Incoming).detach();
+
+ let lhs = iter
+ .next(graph)
+ .expect("get_operands() should not be called on operators without operands")
+ .1;
+
+ let rhs = iter.next(graph).map(|n| n.1);
+
+ assert!(
+ iter.next(graph) == None,
+ "operators with arity 1 or 2 are supported only"
+ );
+
+ (lhs, rhs)
+}
#[derive(Debug)]
pub struct SymbolicState<S>
diff --git a/src/z3.rs b/src/z3.rs
new file mode 100644
index 00000000..93942336
--- /dev/null
+++ b/src/z3.rs
@@ -0,0 +1,118 @@
+use crate::bitvec::BitVector;
+use crate::solver::{Assignment, Solver};
+use crate::symbolic_state::{
+ get_operands, BVOperator, Formula,
+ Node::{Constant, Input, Operator},
+ SymbolId,
+};
+use std::collections::HashMap;
+use z3::{
+ ast::{Ast, Dynamic, BV},
+ Config, Context, SatResult, Solver as Z3Solver,
+};
+
+pub struct Z3 {}
+
+impl Z3 {
+ pub fn new() -> Self {
+ Self {}
+ }
+}
+
+impl Default for Z3 {
+ fn default() -> Self {
+ Self::new()
+ }
+}
+
+impl Solver for Z3 {
+ fn name() -> &'static str {
+ "Z3"
+ }
+
+ fn solve_impl(&mut self, graph: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> {
+ let config = Config::default();
+ let ctx = Context::new(&config);
+
+ let mut bvs = HashMap::new();
+ let bv = traverse(graph, root, &ctx, &mut bvs);
+
+ let solver = Z3Solver::new(&ctx);
+
+ solver.assert(&bv.as_bool().unwrap());
+
+ match solver.check() {
+ SatResult::Sat => {
+ let m = solver.get_model().unwrap();
+
+ Some(
+ graph
+ .node_indices()
+ .filter(|i| matches!(graph[*i], Input(_)))
+ .map(|i| {
+ let input_bv = bvs.get(&i).unwrap().as_bv().unwrap();
+ let result_bv = m.eval(&input_bv).unwrap();
+ let result_value = result_bv.as_u64().unwrap();
+
+ BitVector(result_value)
+ })
+ .collect(),
+ )
+ }
+ _ => None,
+ }
+ }
+}
+
+macro_rules! traverse_binary {
+ ($lhs:expr, $op:ident, $rhs:expr, $graph:expr, $ctx:expr, $bvs:expr) => {
+ Dynamic::from(
+ traverse($graph, $lhs, $ctx, $bvs)
+ .as_bv()
+ .expect("An AST node of type BitVector should be at this position")
+ .$op(
+ &traverse($graph, $rhs, $ctx, $bvs)
+ .as_bv()
+ .expect("An AST node of type BitVector should be at this position"),
+ ),
+ )
+ };
+}
+
+fn traverse<'ctx>(
+ graph: &Formula,
+ node: SymbolId,
+ ctx: &'ctx Context,
+ bvs: &mut HashMap<SymbolId, Dynamic<'ctx>>,
+) -> Dynamic<'ctx> {
+ let bv = match &graph[node] {
+ Operator(op) => match get_operands(graph, node) {
+ (lhs, Some(rhs)) => match op {
+ BVOperator::Add => traverse_binary!(lhs, bvadd, rhs, graph, ctx, bvs),
+ BVOperator::Sub => traverse_binary!(lhs, bvsub, rhs, graph, ctx, bvs),
+ BVOperator::Mul => traverse_binary!(lhs, bvmul, rhs, graph, ctx, bvs),
+ BVOperator::Equals => traverse_binary!(lhs, _eq, rhs, graph, ctx, bvs),
+ BVOperator::BitwiseAnd => traverse_binary!(lhs, bvand, rhs, graph, ctx, bvs),
+ i => unimplemented!("binary operator: {:?}", i),
+ },
+ (lhs, None) => match op {
+ BVOperator::Not => {
+ let zero = BV::from_u64(ctx, 0, 64);
+ Dynamic::from(traverse(graph, lhs, ctx, bvs)._eq(&Dynamic::from(zero)))
+ }
+ i => unimplemented!("unary operator: {:?}", i),
+ },
+ },
+ Input(name) => {
+ if let Some(value) = bvs.get(&node) {
+ value.clone()
+ } else {
+ Dynamic::from(BV::new_const(ctx, name.clone(), 64))
+ }
+ }
+ Constant(cst) => Dynamic::from(BV::from_u64(ctx, *cst, 64)),
+ };
+
+ bvs.insert(node, bv.clone());
+ bv
+}
diff --git a/tests/engine.rs b/tests/engine.rs
index 09676117..4dad5a89 100644
--- a/tests/engine.rs
+++ b/tests/engine.rs
@@ -29,3 +29,9 @@ fn execute_riscu_with_boolector_solver() {
execute_riscu_with_monster("symbolic/arithmetic.c", engine::Backend::Boolector);
execute_riscu_with_monster("symbolic/if-else.c", engine::Backend::Boolector);
}
+
+#[test]
+fn execute_riscu_with_z3_solver() {
+ execute_riscu_with_monster("symbolic/arithmetic.c", engine::Backend::Z3);
+ execute_riscu_with_monster("symbolic/if-else.c", engine::Backend::Z3);
+}