Skip to content

Commit b75a627

Browse files
butterunderflowbutterunderflow
committed
call z3 to solve constraints
1 parent 9ab162f commit b75a627

File tree

3 files changed

+145
-27
lines changed

3 files changed

+145
-27
lines changed

‎headers/wasm/concolic_driver.hpp‎

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,13 @@
11
#ifndef CONCOLIC_DRIVER_HPP
22
#define CONCOLIC_DRIVER_HPP
33

4+
#include "concrete_rt.hpp"
45
#include "smt_solver.hpp"
56
#include "symbolic_rt.hpp"
67
#include <functional>
78
#include <ostream>
89
#include <string>
10+
#include <vector>
911

1012
class ConcolicDriver {
1113
friend class ManagedConcolicCleanup;
@@ -45,16 +47,19 @@ inline void ConcolicDriver::run() {
4547
return;
4648
}
4749
auto cond = unexplored->collect_path_conds();
48-
auto new_env = solver.solve(cond);
49-
if (!new_env.has_value()) {
50+
std::vector<Num> new_env;
51+
std::set<int> valid_ids;
52+
auto result = solver.solve(cond);
53+
if (!result.has_value()) {
5054
// TODO: current implementation is buggy, there could be other reachable
5155
// unexplored paths
5256
std::cout << "Found an unreachable path, marking it as unreachable..."
5357
<< std::endl;
5458
unexplored->fillUnreachableNode();
55-
continue;
59+
continue;
5660
}
57-
SymEnv.update(std::move(new_env.value()));
61+
std::tie(new_env, valid_ids) = std::move(result.value());
62+
SymEnv.update(std::move(new_env), std::move(valid_ids));
5863
try {
5964
entrypoint();
6065
std::cout << "Execution finished successfully with symbolic environment:"

‎headers/wasm/smt_solver.hpp‎

Lines changed: 109 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -3,26 +3,124 @@
33

44
#include "concrete_rt.hpp"
55
#include "symbolic_rt.hpp"
6+
#include "z3++.h"
67
#include <array>
8+
#include <set>
9+
#include <string>
10+
#include <tuple>
711
#include <vector>
812

913
class Solver {
1014
public:
11-
Solver() : count(0) {
12-
envs[0] = {Num(0), Num(0)};
13-
envs[1] = {Num(1), Num(2)};
14-
}
15-
std::optional<std::vector<Num>> solve(const std::vector<SymVal> &conditions) {
16-
// here is just a placeholder implementation to simulate solving result
17-
if (count >= envs.size()) {
18-
return std::nullopt; // No more environments to return
15+
Solver() {}
16+
std::optional<std::tuple<std::vector<Num>, std::set<int>>>
17+
solve(const std::vector<SymVal> &conditions) {
18+
// make an conjunction of all conditions
19+
z3::expr conjunction = z3_ctx.bool_val(true);
20+
for (const auto &cond : conditions) {
21+
auto z3_cond = build_z3_expr(cond);
22+
conjunction = conjunction && z3_cond != z3_ctx.bv_val(0, 32);
23+
}
24+
#ifdef DEBUG
25+
std::cout << "Symbolic conditions size: " << conditions.size() << std::endl;
26+
std::cout << "Solving conditions: " << conjunction << std::endl;
27+
#endif
28+
// call z3 to solve the condition
29+
z3::solver z3_solver(z3_ctx);
30+
z3_solver.add(conjunction);
31+
switch (z3_solver.check()) {
32+
case z3::unsat:
33+
return std::nullopt; // No solution found
34+
case z3::sat: {
35+
z3::model model = z3_solver.get_model();
36+
std::vector<Num> result(max_id + 1, Num(0));
37+
// Reference:
38+
// https://github.com/Z3Prover/z3/blob/master/examples/c%2B%2B/example.cpp#L59
39+
40+
std::cout << "Solved Z3 model" << model << std::endl;
41+
std::set<int> seen_ids;
42+
for (unsigned i = 0; i < model.size(); ++i) {
43+
z3::func_decl var = model[i];
44+
z3::expr value = model.get_const_interp(var);
45+
std::string name = var.name().str();
46+
if (name.starts_with("s_")) {
47+
int id = std::stoi(name.substr(2));
48+
seen_ids.insert(id);
49+
result[id] = Num(value.get_numeral_int());
50+
} else {
51+
std::cout << "Find a variable that is not created by GenSym: " << name
52+
<< std::endl;
53+
}
54+
}
55+
return std::make_tuple(result, seen_ids);
1956
}
20-
return envs[count++ % envs.size()];
57+
case z3::unknown:
58+
throw std::runtime_error("Z3 solver returned unknown status");
59+
}
60+
return std::nullopt; // Should not reach here
2161
}
2262

2363
private:
24-
std::array<std::vector<Num>, 5> envs;
25-
int count;
64+
z3::context z3_ctx;
65+
z3::expr build_z3_expr(const SymVal &sym_val);
2666
};
2767

68+
inline z3::expr Solver::build_z3_expr(const SymVal &sym_val) {
69+
if (auto sym = std::dynamic_pointer_cast<Symbol>(sym_val.symptr)) {
70+
return z3_ctx.bv_const(("s_" + std::to_string(sym->get_id())).c_str(), 32);
71+
} else if (auto concrete =
72+
std::dynamic_pointer_cast<SymConcrete>(sym_val.symptr)) {
73+
return z3_ctx.bv_val(concrete->value.value, 32);
74+
} else if (auto binary =
75+
std::dynamic_pointer_cast<SymBinary>(sym_val.symptr)) {
76+
auto bit_width = 32;
77+
z3::expr zero_bv =
78+
z3_ctx.bv_val(0, bit_width); // Represents 0 as a 32-bit bitvector
79+
z3::expr one_bv =
80+
z3_ctx.bv_val(1, bit_width); // Represents 1 as a 32-bit bitvector
81+
82+
z3::expr left = build_z3_expr(binary->lhs);
83+
z3::expr right = build_z3_expr(binary->rhs);
84+
// TODO: make sure the semantics of these operations are aligned with wasm
85+
switch (binary->op) {
86+
case EQ: {
87+
auto temp_bool = left == right;
88+
return z3::ite(temp_bool, one_bv, zero_bv);
89+
}
90+
case NEQ: {
91+
auto temp_bool = left != right;
92+
return z3::ite(temp_bool, one_bv, zero_bv);
93+
}
94+
case LT: {
95+
auto temp_bool = left < right;
96+
return z3::ite(temp_bool, one_bv, zero_bv);
97+
}
98+
case LEQ: {
99+
auto temp_bool = left <= right;
100+
return z3::ite(temp_bool, one_bv, zero_bv);
101+
}
102+
case GT: {
103+
auto temp_bool = left > right;
104+
return z3::ite(temp_bool, one_bv, zero_bv);
105+
}
106+
case GEQ: {
107+
auto temp_bool = left >= right;
108+
return z3::ite(temp_bool, one_bv, zero_bv);
109+
}
110+
case ADD: {
111+
return left + right;
112+
}
113+
case SUB: {
114+
return left - right;
115+
}
116+
case MUL: {
117+
return left * right;
118+
}
119+
case DIV: {
120+
return left / right;
121+
}
122+
}
123+
}
124+
throw std::runtime_error("Unsupported symbolic value type");
125+
}
28126
#endif // SMT_SOLVER_HPP

‎headers/wasm/symbolic_rt.hpp‎

Lines changed: 27 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@
99
#include <memory>
1010
#include <optional>
1111
#include <ostream>
12+
#include <set>
1213
#include <string>
1314
#include <variant>
1415
#include <vector>
@@ -19,9 +20,13 @@ class Symbolic {
1920
virtual ~Symbolic() = default; // Make Symbolic polymorphic
2021
};
2122

23+
static int max_id = 0;
24+
2225
class Symbol : public Symbolic {
2326
public:
24-
Symbol(int id) : id(id) {}
27+
// TODO: add type information to determine the size of bitvector
28+
// for now we just assume that only i32 will be used
29+
Symbol(int id) : id(id) { max_id = std::max(max_id, id); }
2530
int get_id() const { return id; }
2631

2732
private:
@@ -190,7 +195,7 @@ static SymFrames_t SymFrames;
190195
struct Node;
191196

192197
struct NodeBox {
193-
explicit NodeBox();
198+
explicit NodeBox(NodeBox *parent);
194199
std::unique_ptr<Node> node;
195200
NodeBox *parent;
196201

@@ -247,9 +252,9 @@ struct IfElseNode : Node {
247252
std::unique_ptr<NodeBox> true_branch;
248253
std::unique_ptr<NodeBox> false_branch;
249254

250-
IfElseNode(SymVal cond)
251-
: cond(cond), true_branch(std::make_unique<NodeBox>()),
252-
false_branch(std::make_unique<NodeBox>()) {}
255+
IfElseNode(SymVal cond, NodeBox *parent)
256+
: cond(cond), true_branch(std::make_unique<NodeBox>(parent)),
257+
false_branch(std::make_unique<NodeBox>(parent)) {}
253258

254259
std::string to_string() override {
255260
std::string result = "IfElseNode {\n";
@@ -357,15 +362,15 @@ struct Unreachable : Node {
357362
}
358363
};
359364

360-
inline NodeBox::NodeBox()
365+
inline NodeBox::NodeBox(NodeBox *parent)
361366
: node(std::make_unique<UnExploredNode>()),
362367
/* TODO: avoid allocation of unexplored node */
363-
parent(nullptr) {}
368+
parent(parent) {}
364369

365370
inline std::monostate NodeBox::fillIfElseNode(SymVal cond) {
366371
// fill the current NodeBox with an ifelse branch node it's unexplored
367372
if (dynamic_cast<UnExploredNode *>(node.get())) {
368-
node = std::make_unique<IfElseNode>(cond);
373+
node = std::make_unique<IfElseNode>(cond, this);
369374
}
370375
assert(dynamic_cast<IfElseNode *>(node.get()) != nullptr &&
371376
"Current node is not an IfElseNode, cannot fill it!");
@@ -425,7 +430,7 @@ inline std::vector<SymVal> NodeBox::collect_path_conds() {
425430
class ExploreTree_t {
426431
public:
427432
explicit ExploreTree_t()
428-
: root(std::make_unique<NodeBox>()), cursor(root.get()) {}
433+
: root(std::make_unique<NodeBox>(nullptr)), cursor(root.get()) {}
429434

430435
void reset_cursor() {
431436
// Reset the cursor to the root of the tree
@@ -513,13 +518,22 @@ static ExploreTree_t ExploreTree;
513518
class SymEnv_t {
514519
public:
515520
Num read(SymVal sym) {
516-
return Num(0);
517521
auto symbol = dynamic_cast<Symbol *>(sym.symptr.get());
518522
assert(symbol);
523+
if (symbol->get_id() >= map.size()) {
524+
map.resize(symbol->get_id() + 1);
525+
}
526+
#if DEBUG
527+
std::cout << "Read symbol: " << symbol->get_id()
528+
<< " from symbolic environment" << std::endl;
529+
std::cout << "Current symbolic environment: " << to_string() << std::endl;
530+
#endif
519531
return map[symbol->get_id()];
520532
}
521533

522-
void update(std::vector<Num> new_env) { map = std::move(new_env); }
534+
void update(std::vector<Num> new_env, std::set<int> valid_ids) {
535+
map = std::move(new_env);
536+
}
523537

524538
std::string to_string() const {
525539
std::string result;
@@ -534,7 +548,8 @@ class SymEnv_t {
534548
}
535549

536550
private:
537-
std::vector<Num> map; // The symbolic environment, a vector of Num
551+
std::vector<Num> map; // The symbolic environment, a vector of Num
552+
std::set<int> valid_ids; // The set of valid IDs in the symbolic environment
538553
};
539554

540555
static SymEnv_t SymEnv;

0 commit comments

Comments
 (0)