Let's try to accept large constant initializers
these are not passed down to the memory, but are skipped.
This is an over-approximation of the function's behavior.
Add infrastructure to track over-approximations and print a note when
verification fails.
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2984,6 +2984,14 @@ void Store::print(std::ostream &os) const {
}
StateValue Store::toSMT(State &s) const {
+ // skip large initializers. FIXME: this should be moved to memory so it can
+ // fold subsequent trivial loads
+ if (s.isInitializationPhase() &&
+ Memory::getStoreByteSize(val->getType()) > 128) {
+ s.doesApproximation("Large constant initializer removed");
+ return {};
+ }
+
auto &p = s.getAndAddPoisonUB(*ptr).value;
auto &v = s[*val];
s.getMemory().store(p, v, val->getType(), align, s.getUndefVars());

MODIFY
ir/state.cpp
ir/state.cpp
@@ -842,6 +842,10 @@ void State::useUnsupported(const char *name) {
used_unsupported.emplace(name);
}
+void State::doesApproximation(const char *name) {
+ used_approximations.emplace(name);
+}
+
void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}

MODIFY
ir/state.h
ir/state.h
@@ -78,6 +78,7 @@ private:
smt::AndExpr axioms;
std::set<const char*> used_unsupported;
+ std::set<const char*> used_approximations;
const BasicBlock *current_bb = nullptr;
std::set<smt::expr> quantified_vars;
@@ -186,6 +187,9 @@ public:
void useUnsupported(const char *name);
auto& getUnsupported() const { return used_unsupported; }
+ void doesApproximation(const char *name);
+ auto& getApproximations() const { return used_approximations; }
+
void addQuantVar(const smt::expr &var);
void addFnQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);

MODIFY
llvm_util/utils.cpp
llvm_util/utils.cpp
@@ -184,7 +184,7 @@ Type* llvm_type2alive(const llvm::Type *ty) {
auto vty = cast<llvm::VectorType>(ty);
auto elems = vty->getElementCount().getKnownMinValue();
auto ety = llvm_type2alive(vty->getElementType());
- if (!ety || elems > 128)
+ if (!ety)
return nullptr;
cache = make_unique<VectorType>("ty_" + to_string(type_id_counter++),
elems, *ety);
@@ -198,7 +198,7 @@ Type* llvm_type2alive(const llvm::Type *ty) {
auto elemty = aty->getElementType();
auto elems = aty->getNumElements();
auto ety = llvm_type2alive(elemty);
- if (!ety || elems > 128)
+ if (!ety)
return nullptr;
auto sz_with_padding = DL->getTypeAllocSize(elemty);

ADD
tests/alive-tv/constexpr/large-const-opt.srctgt.ll
+; FIXME: this should work some day..
+
+; ERROR: Value mismatch
+; CHECK: Alive2 approximated the semantics
+
+@str = constant [129 x i8] c"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\00", align 16
+
+define i8 @src(i32 %idx) {
+ %arrayidx = getelementptr inbounds [129 x i8], [129 x i8]* @str, i64 0, i32 %idx
+ %v = load i8, i8* %arrayidx, align 1
+ ret i8 %v
+}
+
+define i8 @tgt(i32 %idx) {
+ ret i8 97
+}

ADD
tests/alive-tv/constexpr/large-const.srctgt.ll
+@str = constant [129 x i8] c"aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa\00", align 16
+
+define i8 @src(i32 %idx) {
+ %arrayidx = getelementptr inbounds [129 x i8], [129 x i8]* @str, i64 0, i32 %idx
+ %v = load i8, i8* %arrayidx, align 1
+ ret i8 %v
+}
+
+define i8 @tgt(i32 %idx) {
+ %idxp = sext i32 %idx to i64
+ %arrayidx = getelementptr inbounds [129 x i8], [129 x i8]* @str, i64 0, i64 %idxp
+ %v = load i8, i8* %arrayidx, align 1
+ ret i8 %v
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -150,6 +150,19 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
s << msg;
if (!var_name.empty())
s << " for " << *var;
+
+ auto &src_approx = src_state.getApproximations();
+ auto &tgt_approx = tgt_state.getApproximations();
+ if (!src_approx.empty() || !tgt_approx.empty()) {
+ s << "\n\nNOTE: Alive2 approximated the semantics of this program.\n"
+ "The bug found may be spurious. Approximations done:\n";
+ auto approx = src_approx;
+ approx.insert(tgt_approx.begin(), tgt_approx.end());
+ for (auto *a : approx) {
+ s << " - " << a << '\n';
+ }
+ }
+
s << "\n\nExample:\n";
for (auto &[var, val] : src_state.getValues()) {

Let's try to accept large constant initializers
these are not passed down to the memory, but are skipped.
This is an over-approximation of the function's behavior.
Add infrastructure to track over-approximations and print a note when
verification fails.