Add -enable-approx-int2ptr for an unsound int2ptr approximation
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1989,7 +1989,24 @@ expr Memory::ptr2int(const expr &ptr) const {
expr Memory::int2ptr(const expr &val) const {
assert(!memory_unused() && observesAddresses());
- // TODO
+ // TODO: missing pointer escaping
+ if (config::enable_approx_int2ptr) {
+ DisjointExpr<expr> ret;
+ ret.add(Pointer::mkNullPointer(*this).release(), val == 0);
+
+ auto add = [&](unsigned limit, bool local) {
+ for (unsigned i = 0; i != limit; ++i) {
+ Pointer p(*this, i, local);
+ Pointer p_end = p + p.blockSize();
+ ret.add((p + (val - p.getAddress())).release(),
+ val.uge(p.getAddress()) && val.ult(p_end.getAddress()));
+ }
+ };
+ add(numLocals(), true);
+ add(numNonlocals(), false);
+ return *std::move(ret)();
+ }
+
expr null = Pointer::mkNullPointer(*this).release();
expr fn = expr::mkUF("int2ptr", { val }, null);
state->doesApproximation("inttoptr", fn);

MODIFY
llvm_util/cmd_args_def.h
llvm_util/cmd_args_def.h
@@ -10,6 +10,7 @@ config::src_unroll_cnt = opt_unrolling_factor;
#endif
config::disable_undef_input = opt_disable_undef;
config::disable_poison_input = opt_disable_poison;
+config::enable_approx_int2ptr = opt_enable_approx_int2ptr;
config::symexec_print_each_value = opt_se_verbose;
smt::set_query_timeout(to_string(opt_smt_to));
smt::set_memory_limit((uint64_t)opt_smt_max_mem * 1024 * 1024);

MODIFY
llvm_util/cmd_args_list.h
llvm_util/cmd_args_list.h
@@ -40,6 +40,11 @@ llvm::cl::opt<bool> opt_disable_poison(LLVM_ARGS_PREFIX "disable-poison-input",
llvm::cl::desc("Assume inputs are not poison (default=false)"),
llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
+llvm::cl::opt<bool> opt_enable_approx_int2ptr(
+ LLVM_ARGS_PREFIX "enable-approx-int2ptr",
+ llvm::cl::desc("Enable unsound approximation of int2ptr (default=false)"),
+ llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
+
llvm::cl::opt<bool> opt_error_fatal(LLVM_ARGS_PREFIX "exit-on-error",
llvm::cl::desc("Exit on error"),
llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));

MODIFY
util/config.cpp
util/config.cpp
@@ -15,6 +15,7 @@ bool skip_smt = false;
string smt_benchmark_dir;
bool disable_poison_input = false;
bool disable_undef_input = false;
+bool enable_approx_int2ptr = false;
bool debug = false;
unsigned src_unroll_cnt = 0;
unsigned tgt_unroll_cnt = 0;

MODIFY
util/config.h
util/config.h
@@ -19,6 +19,8 @@ extern bool disable_poison_input;
extern bool disable_undef_input;
+extern bool enable_approx_int2ptr;
+
extern bool debug;
extern unsigned src_unroll_cnt;

Add -enable-approx-int2ptr for an unsound int2ptr approximation