From 322c97979107fe5654d7fb8d0729909d0dd90dfe Mon Sep 17 00:00:00 2001 From: Chen Ju Date: Thu, 9 Jul 2020 19:15:11 -0700 Subject: [PATCH 1/2] Restrictive constraints collecting Signed-off-by: Chen Ju --- llvm_mode/dfsan_rt/dfsan/dfsan.cc | 82 +++++++++++++++++++++++++++++-- 1 file changed, 78 insertions(+), 4 deletions(-) diff --git a/llvm_mode/dfsan_rt/dfsan/dfsan.cc b/llvm_mode/dfsan_rt/dfsan/dfsan.cc index ec84765b..d97089f5 100644 --- a/llvm_mode/dfsan_rt/dfsan/dfsan.cc +++ b/llvm_mode/dfsan_rt/dfsan/dfsan.cc @@ -51,6 +51,7 @@ #include #define OPTIMISTIC 1 +#define RESTRICT_CONSTRAINT 1 using namespace __dfsan; @@ -99,7 +100,16 @@ struct expr_equal { return lhs.id() == rhs.id(); } }; + +#if RESTRICT_CONSTRAINT +typedef struct { + std::unordered_set exprs; + std::unordered_set deps; +} branch_dep_t; +#else typedef std::unordered_set branch_dep_t; +#endif + static std::vector *__branch_deps; Flags __dfsan::flags_data; @@ -825,6 +835,30 @@ add_constraints(dfsan_label label) { try { std::unordered_set 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) { @@ -833,6 +867,7 @@ add_constraints(dfsan_label label) { } c->insert(cond); } +#endif } catch (z3::exception e) { Report("WARNING: adding constraints error: %s\n", e.msg()); } @@ -858,11 +893,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 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); @@ -894,7 +934,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); @@ -904,7 +968,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) { @@ -989,11 +1053,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 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); } @@ -1030,9 +1099,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) { From f7f53a2295a65a38632e2d04a047e3006db2d6e3 Mon Sep 17 00:00:00 2001 From: Chen Ju Date: Wed, 9 Sep 2020 22:58:54 -0700 Subject: [PATCH 2/2] Fix a bug in dependency tree Signed-off-by: Chen Ju --- llvm_mode/dfsan_rt/dfsan/dfsan.cc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/llvm_mode/dfsan_rt/dfsan/dfsan.cc b/llvm_mode/dfsan_rt/dfsan/dfsan.cc index 96adfb0e..2d475d6f 100644 --- a/llvm_mode/dfsan_rt/dfsan/dfsan.cc +++ b/llvm_mode/dfsan_rt/dfsan/dfsan.cc @@ -714,7 +714,9 @@ static z3::expr serialize(dfsan_label label, std::unordered_set &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 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); }