Allow disabling poison/undef inputs
MODIFY
ir/value.cpp
ir/value.cpp
#include "ir/value.h"
#include "smt/expr.h"
#include "util/compiler.h"
+#include "util/config.h"
using namespace smt;
using namespace std;
+using namespace util;
static unsigned gbl_fresh_id = 0;
@@ -83,6 +85,7 @@ StateValue Input::toSMT(State &s) const {
auto bw = bits();
string uname = UndefValue::getFreshName();
expr undef = expr::mkVar(uname.c_str(), bw);
+ if (!config::disable_undef_input)
s.addUndefVar(undef);
return { expr::mkIf(type == expr::mkUInt(0, 2),

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -22,14 +22,16 @@ static void show_help() {
cerr <<
"Usage: alive2 <options> <files.opt>\n"
"Options:\n"
- " -root-only\tCheck the expression's root only\n"
- " -v\t\tVerbose mode\n"
- " -smt-stats\tShow SMT statistics\n"
- " -smt-to:x\tTimeout for SMT queries in ms\n"
- " -max-mem:x\tMax memory consumption in MB (aprox)\n"
- " -smt-verbose\tPrint all SMT queries\n"
- " -skip-smt\tSkip all SMT queries\n"
- " -h / --help\tShow this help\n";
+ " -root-only\t\tCheck the expression's root only\n"
+ " -v\t\t\tVerbose mode\n"
+ " -smt-stats\t\tShow SMT statistics\n"
+ " -smt-to:x\t\tTimeout for SMT queries in ms\n"
+ " -max-mem:x\t\tMax memory consumption in MB (aprox)\n"
+ " -smt-verbose\t\tPrint all SMT queries\n"
+ " -skip-smt\t\tSkip all SMT queries\n"
+ " -disable-poison-input\tAssume input variables can never be poison\n"
+ " -disable-undef-input\tAssume input variables can never be undef\n"
+ " -h / --help\t\tShow this help\n";
}
@@ -62,6 +64,10 @@ int main(int argc, char **argv) {
smt::solver_tactic_verbose(true);
else if (arg == "-skip-smt")
config::skip_smt = true;
+ else if (arg == "-disable-undef-input")
+ config::disable_undef_input = true;
+ else if (arg == "-disable-poison-input")
+ config::disable_poison_input = true;
else if (arg == "-h" || arg == "--help") {
show_help();
return 0;

MODIFY
tools/transform.cpp
tools/transform.cpp
#include "smt/expr.h"
#include "smt/smt.h"
#include "smt/solver.h"
+#include "util/config.h"
#include "util/errors.h"
#include "util/symexec.h"
#include <map>
@@ -132,6 +133,17 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
static expr preprocess(Transform &t, const set<expr> &qvars,
const set<expr> &undef_qvars, expr && e) {
+
+ // restrict type variable from taking disabled values
+ for (auto &i : t.src.getInputs()) {
+ auto var = static_cast<const Input &>(i).getTyVar();
+
+ if (config::disable_undef_input)
+ e &= var != expr::mkUInt(1, 2);
+ if (config::disable_poison_input)
+ e &= var.extract(1, 1) == expr::mkUInt(0, 1);
+ }
+
if (qvars.empty() || e.isFalse())
return move(e);

MODIFY
util/config.cpp
util/config.cpp
@@ -7,5 +7,7 @@ namespace util::config {
bool symexec_print_each_value = false;
bool skip_smt = false;
+bool disable_poison_input = false;
+bool disable_undef_input = false;
}

MODIFY
util/config.h
util/config.h
@@ -9,4 +9,8 @@ extern bool symexec_print_each_value;
extern bool skip_smt;
+extern bool disable_poison_input;
+
+extern bool disable_undef_input;
+
}

Allow disabling poison/undef inputs