Skip to content
This repository was archived by the owner on May 14, 2024. It is now read-only.

Restrictive constraints collecting #5

Open
chenju2k6 wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Restrictive constraints collecting #5

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
322c979
Restrictive constraints collecting
Jul 10, 2020
9df3379
Merge https://github.com/chengyusong/Kirenenko
Sep 10, 2020
f7f53a2
Fix a bug in dependency tree
Sep 10, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
86 changes: 81 additions & 5 deletions llvm_mode/dfsan_rt/dfsan/dfsan.cc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,6 +51,7 @@
#include <vector>

#define OPTIMISTIC 1
#define RESTRICT_CONSTRAINT 1

using namespace __dfsan;

Expand Down Expand Up @@ -99,7 +100,16 @@ struct expr_equal {
return lhs.id() == rhs.id();
}
};

#if RESTRICT_CONSTRAINT
typedef struct {
std::unordered_set<z3::expr,expr_hash,expr_equal> exprs;
std::unordered_set<dfsan_label> deps;
} branch_dep_t;
#else
typedef std::unordered_set<z3::expr, expr_hash, expr_equal> branch_dep_t;
#endif

static std::vector<branch_dep_t*> *__branch_deps;

Flags __dfsan::flags_data;
Expand Down Expand Up @@ -704,7 +714,9 @@ static z3::expr serialize(dfsan_label label, std::unordered_set<u32> &deps) {
}
z3::expr op2 = __z3_context.bv_val((uint64_t)info->op2, size);
if (info->l2 >= CONST_OFFSET) {
op2 = serialize(info->l2, deps).simplify();
std::unordered_set<u32> deps2;
op2 = serialize(info->l2, deps2).simplify();
deps.insert(deps2.begin(),deps2.end());
} else if (info->size == 1) {
op2 = __z3_context.bool_val(info->op2 == 1);
}
Expand Down Expand Up @@ -800,6 +812,30 @@ add_constraints(dfsan_label label) {
try {
std::unordered_set<dfsan_label> inputs;
z3::expr cond = serialize(label, inputs);
#if RESTRICT_CONSTRAINT
branch_dep_t* the_tree = nullptr;
for (auto off : inputs) {
auto c = __branch_deps->at(off);
if (c == nullptr) {
c = new branch_dep_t();
}
if (the_tree == nullptr) {
the_tree = c;
}
else {
the_tree->exprs.insert(c->exprs.begin(),c->exprs.end());
the_tree->deps.insert(c->deps.begin(),c->deps.end());
for (auto &idx : c->deps) {
__branch_deps->at(idx) = the_tree;
}
}
__branch_deps->at(off) = the_tree;
}
the_tree->exprs.insert(cond);
for (auto off : inputs) {
the_tree->deps.insert(off);
}
#else
for (auto off : inputs) {
auto c = __branch_deps->at(off);
if (c == nullptr) {
Expand All @@ -808,6 +844,7 @@ add_constraints(dfsan_label label) {
}
c->insert(cond);
}
#endif
} catch (z3::exception e) {
Report("WARNING: adding constraints error: %s\n", e.msg());
}
Expand All @@ -833,11 +870,16 @@ static void __solve_cond(dfsan_label label, z3::expr &result, void *addr) {

__z3_solver.reset();
// add dependencies
branch_dep_t added;
//branch_dep_t added;
std::unordered_set<z3::expr,expr_hash,expr_equal> added;
for (auto off : inputs) {
auto c = __branch_deps->at(off);
if (c) {
#if RESTRICT_CONSTRAINT
for (auto &expr : c->exprs) {
#else
for (auto &expr : *c) {
#endif
if (added.insert(expr).second) {
//AOUT("adding expr: %s\n", expr.to_string().c_str());
__z3_solver.add(expr);
Expand Down Expand Up @@ -869,7 +911,31 @@ static void __solve_cond(dfsan_label label, z3::expr &result, void *addr) {
}
#endif
}

#if RESTRICT_CONSTRAINT
// nested branch
branch_dep_t* the_tree = nullptr;
for (auto off : inputs) {
auto c = __branch_deps->at(off);
if (c == nullptr) {
c = new branch_dep_t();
}
if (the_tree == nullptr) {
the_tree = c;
}
else {
the_tree->exprs.insert(c->exprs.begin(),c->exprs.end());
the_tree->deps.insert(c->deps.begin(),c->deps.end());
for (auto &idx : c->deps) {
__branch_deps->at(idx) = the_tree;
}
}
__branch_deps->at(off) = the_tree;
}
the_tree->exprs.insert(cond);
for (auto off : inputs) {
the_tree->deps.insert(off);
}
#else
// nested branch
for (auto off : inputs) {
auto c = __branch_deps->at(off);
Expand All @@ -879,7 +945,7 @@ static void __solve_cond(dfsan_label label, z3::expr &result, void *addr) {
}
c->insert(cond == result);
}

#endif
// mark as flipped
get_label_info(label)->flags |= B_FLIPPED;
} catch (z3::exception e) {
Expand Down Expand Up @@ -964,11 +1030,16 @@ __taint_trace_gep(dfsan_label label, u64 r) {

__z3_solver.reset();
// add dependencies
branch_dep_t added;
//branch_dep_t added;
std::unordered_set<z3::expr,expr_hash,expr_equal> added;
for (auto off : inputs) {
auto c = __branch_deps->at(off);
if (c) {
#if RESTRICT_CONSTRAINT
for (auto &expr : c->exprs) {
#else
for (auto &expr : *c) {
#endif
if (added.insert(expr).second) {
__z3_solver.add(expr);
}
Expand Down Expand Up @@ -1005,9 +1076,14 @@ __taint_trace_gep(dfsan_label label, u64 r) {
c = new branch_dep_t();
__branch_deps->at(off) = c;
}
#if RESTRICT_CONSTRAINT
c->exprs.insert(index == result);
#else
c->insert(index == result);
#endif
}


// mark as visited
get_label_info(label)->flags |= B_FLIPPED;
} catch (z3::exception e) {
Expand Down