memory: mark pointers with undef offset as undereferenceable
MODIFY
ir/globals.cpp
ir/globals.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/globals.h"
+#include "smt/expr.h"
+#include <string_view>
+
+using namespace smt;
+using namespace std;
namespace IR {
@@ -28,4 +33,10 @@ bool does_ptr_mem_access;
bool does_ptr_store;
bool does_sub_byte_access;
+
+bool isUndef(const expr &e) {
+ auto name = e.fn_name();
+ return string_view(name).substr(0, 6) == "undef!";
+}
+
}

MODIFY
ir/globals.h
ir/globals.h
// Copyright (c) 2018-present The Alive2 Authors.
// Distributed under the MIT license that can be found in the LICENSE file.
+namespace smt { class expr; }
+
namespace IR {
/// Upperbound of the number of non-local pointers returned by instructions
@@ -59,4 +61,7 @@ extern bool does_ptr_store;
/// Whether the programs do memory accesses of less than bits_byte
extern bool does_sub_byte_access;
+
+bool isUndef(const smt::expr &e);
+
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -541,7 +541,8 @@ static pair<expr, expr> is_dereferenceable(const Pointer &p,
// try some constant folding; these are implied by the conditions above
if (bytes.ugt(block_sz).isTrue() ||
- offset.sextOrTrunc(bits_size_t).uge(block_sz).isTrue())
+ offset.sextOrTrunc(bits_size_t).uge(block_sz).isTrue() ||
+ isUndef(offset))
cond = false;
return { move(cond), p.is_aligned(align) };
@@ -802,16 +803,24 @@ ostream& operator<<(ostream &os, const Pointer &p) {
if (p.isNull().isTrue())
return os << "null";
+#define P(field, fn) \
+ if (field.isConst()) \
+ field.fn(os); \
+ else \
+ os << field
+
os << "pointer(" << (p.is_local().isTrue() ? "local" : "non-local")
<< ", block_id=";
- p.get_bid().printUnsigned(os);
+ P(p.get_bid(), printUnsigned);
+
os << ", offset=";
- p.get_offset().printSigned(os);
+ P(p.get_offset(), printSigned);
if (bits_for_ptrattrs && !p.get_attrs().isZero()) {
os << ", attrs=";
- p.get_attrs().printUnsigned(os);
+ P(p.get_attrs(), printUnsigned);
}
+#undef P
return os << ')';
}

MODIFY
ir/state.cpp
ir/state.cpp
#include "ir/state.h"
#include "ir/function.h"
+#include "ir/globals.h"
#include "smt/smt.h"
#include "util/errors.h"
#include <cassert>
-#include <string_view>
using namespace smt;
using namespace util;
@@ -271,7 +271,7 @@ void State::resetUndefVars() {
StateValue State::rewriteUndef(StateValue &&val) {
vector<pair<expr, expr>> repls;
for (auto &var : val.vars()) {
- if (string_view(var.fn_name()).substr(0, 6) == "undef!") {
+ if (isUndef(var)) {
auto newvar = expr::mkFreshVar("undef", var);
repls.emplace_back(var, newvar);
addUndefVar(move(newvar));

MODIFY
tests/alive-tv/memory/alloca-removal-fail.src.ll
tests/alive-tv/memory/alloca-removal-fail.src.ll
-; TEST-ARGS: -disable-undef-input
define i8* @f_observed(i64 %size) {
entry:
%items.addr = alloca i32, align 4

MODIFY
tools/transform.cpp
tools/transform.cpp
#include <map>
#include <set>
#include <sstream>
-#include <string_view>
using namespace IR;
using namespace smt;
@@ -72,8 +71,8 @@ static void print_single_varval(ostream &os, State &st, const Model &m,
// needed, not because it's undef
bool found_undef = false;
for (auto &var : partial.vars()) {
- auto name = var.fn_name();
- found_undef |= string_view(name).substr(0, 6) == "undef!";
+ if ((found_undef = isUndef(var)))
+ break;
}
if (found_undef)
os << "\t[based on undef value]";

memory: mark pointers with undef offset as undereferenceable