carry on with verification if an unknown libcall is found
semantics are overapproximated; Alive2 can gracefully fail later
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1671,9 +1671,6 @@ void FnCall::print(ostream &os) const {
first = false;
}
os << ')' << attrs;
-
- if (!valid)
- os << "\t; WARNING: unknown known function";
}
static void unpack_inputs(State &s, Value &argv, Type &ty,
@@ -1762,10 +1759,8 @@ pack_return(State &s, Type &ty, vector<StateValue> &vals, const FnAttrs &attrs,
}
StateValue FnCall::toSMT(State &s) const {
- if (!valid) {
- s.addUB(expr());
- return {};
- }
+ if (approx)
+ s.doesApproximation("Unknown libcall: " + fnName);
vector<StateValue> inputs;
vector<Memory::PtrInput> ptr_inputs;
@@ -1843,7 +1838,7 @@ expr FnCall::getTypeConstraints(const Function &f) const {
unique_ptr<Instr> FnCall::dup(const string &suffix) const {
auto r = make_unique<FnCall>(getType(), getName() + suffix, string(fnName),
- FnAttrs(attrs), valid);
+ FnAttrs(attrs), approx);
r->args = args;
return r;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -786,12 +786,12 @@ private:
std::string fnName;
std::vector<std::pair<Value*, ParamAttrs>> args;
FnAttrs attrs;
- bool valid;
+ bool approx;
public:
FnCall(Type &type, std::string &&name, std::string &&fnName,
- FnAttrs &&attrs = FnAttrs::None, bool valid = true)
+ FnAttrs &&attrs = FnAttrs::None, bool approx = false)
: MemInstr(type, std::move(name)), fnName(std::move(fnName)),
- attrs(std::move(attrs)), valid(valid) {}
+ attrs(std::move(attrs)), approx(approx) {}
void addArg(Value &arg, ParamAttrs &&attrs);
const auto& getFnName() const { return fnName; }
const auto& getArgs() const { return args; }

MODIFY
ir/state.cpp
ir/state.cpp
@@ -870,8 +870,8 @@ void State::useUnsupported(const char *name) {
used_unsupported.emplace(name);
}
-void State::doesApproximation(const char *name) {
- used_approximations.emplace(name);
+void State::doesApproximation(string &&name) {
+ used_approximations.emplace(move(name));
}
void State::addQuantVar(const expr &var) {

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

MODIFY
llvm_util/known_fns.cpp
llvm_util/known_fns.cpp
using namespace IR;
using namespace std;
-#define RETURN_KNOWN(op) \
- return { op, move(attrs), move(param_attrs), true }
-#define RETURN_KNOWN_ATTRS() \
- return { nullptr, move(attrs), move(param_attrs), true }
-#define RETURN_UNKNOWN_KNOWN() \
+#define RETURN_VAL(op) \
+ return { op, move(attrs), move(param_attrs), false }
+#define RETURN_EXACT() \
return { nullptr, move(attrs), move(param_attrs), false }
-#define RETURN_UNKNOWN() \
+#define RETURN_APPROX() \
return { nullptr, move(attrs), move(param_attrs), true }
namespace llvm_util {
@@ -32,18 +30,18 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
auto ty = llvm_type2alive(i.getType());
if (!ty)
- RETURN_UNKNOWN();
+ RETURN_EXACT();
// TODO: add support for checking mismatch of C vs C++ alloc fns
if (llvm::isMallocLikeFn(&i, &TLI, false)) {
bool isNonNull = i.getCalledFunction()->getName() != "malloc";
- RETURN_KNOWN(make_unique<Malloc>(*ty, value_name(i), *args[0], isNonNull));
+ RETURN_VAL(make_unique<Malloc>(*ty, value_name(i), *args[0], isNonNull));
} else if (llvm::isCallocLikeFn(&i, &TLI, false)) {
- RETURN_KNOWN(make_unique<Calloc>(*ty, value_name(i), *args[0], *args[1]));
+ RETURN_VAL(make_unique<Calloc>(*ty, value_name(i), *args[0], *args[1]));
} else if (llvm::isReallocLikeFn(&i, &TLI, false)) {
- RETURN_KNOWN(make_unique<Malloc>(*ty, value_name(i), *args[0], *args[1]));
+ RETURN_VAL(make_unique<Malloc>(*ty, value_name(i), *args[0], *args[1]));
} else if (llvm::isFreeCall(&i, &TLI)) {
- RETURN_KNOWN(make_unique<Free>(*args[0]));
+ RETURN_VAL(make_unique<Free>(*args[0]));
}
auto set_param = [&](unsigned i, ParamAttrs::Attribute attr) {
@@ -70,12 +68,12 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
auto decl = i.getCalledFunction();
llvm::LibFunc libfn;
if (!decl || !TLI.getLibFunc(*decl, libfn) || !TLI.has(libfn))
- RETURN_UNKNOWN();
+ RETURN_EXACT();
switch (libfn) {
case llvm::LibFunc_memset: // void* memset(void *ptr, int val, size_t bytes)
BB.addInstr(make_unique<Memset>(*args[0], *args[1], *args[2], 1));
- RETURN_KNOWN(make_unique<UnaryOp>(*ty, value_name(i), *args[0],
+ RETURN_VAL(make_unique<UnaryOp>(*ty, value_name(i), *args[0],
UnaryOp::Copy));
case llvm::LibFunc_strlen:
if (auto BI = llvm::dyn_cast<llvm::BitCastInst>(i.getArgOperand(0))) {
@@ -83,16 +81,16 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
if (G && G->isConstant() && G->hasDefinitiveInitializer()) {
auto C = llvm::dyn_cast<llvm::ConstantDataArray>(G->getInitializer());
if (C && C->isCString()) {
- RETURN_KNOWN(make_unique<UnaryOp>(*ty, value_name(i),
+ RETURN_VAL(make_unique<UnaryOp>(*ty, value_name(i),
*make_intconst(C->getAsCString().size(), ty->bits()),
UnaryOp::Copy));
}
}
}
- RETURN_KNOWN(make_unique<Strlen>(*ty, value_name(i), *args[0]));
+ RETURN_VAL(make_unique<Strlen>(*ty, value_name(i), *args[0]));
case llvm::LibFunc_memcmp:
case llvm::LibFunc_bcmp: {
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<Memcmp>(*ty, value_name(i), *args[0], *args[1], *args[2],
libfn == llvm::LibFunc_bcmp));
}
@@ -104,54 +102,53 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
value_name(i) + (needs_trunc ? "#beftrunc" : ""),
*args[0], UnaryOp::FFS);
if (!needs_trunc)
- RETURN_KNOWN(unique_ptr<UnaryOp>(Op));
+ RETURN_VAL(unique_ptr<UnaryOp>(Op));
BB.addInstr(unique_ptr<UnaryOp>(Op));
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<ConversionOp>(*ty, value_name(i), *Op, ConversionOp::Trunc));
}
case llvm::LibFunc_abs:
case llvm::LibFunc_labs:
case llvm::LibFunc_llabs:
- RETURN_KNOWN(make_unique<BinOp>(*ty, value_name(i), *args[0],
+ RETURN_VAL(make_unique<BinOp>(*ty, value_name(i), *args[0],
*make_intconst(1, 1), BinOp::Abs));
case llvm::LibFunc_fabs:
case llvm::LibFunc_fabsf:
- RETURN_KNOWN(
- make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::FAbs,
+ RETURN_VAL(make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::FAbs,
parse_fmath(i)));
case llvm::LibFunc_ceil:
case llvm::LibFunc_ceilf:
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Ceil));
case llvm::LibFunc_floor:
case llvm::LibFunc_floorf:
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Floor));
case llvm::LibFunc_round:
case llvm::LibFunc_roundf:
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Round));
case llvm::LibFunc_roundeven:
case llvm::LibFunc_roundevenf:
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::RoundEven));
case llvm::LibFunc_trunc:
case llvm::LibFunc_truncf:
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Trunc));
case llvm::LibFunc_sqrt:
case llvm::LibFunc_sqrtf:
BB.addInstr(make_unique<Assume>(*args[0], Assume::WellDefined));
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i), *args[0], UnaryOp::Sqrt));
case llvm::LibFunc_fwrite: {
@@ -161,7 +158,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
auto bytes = *size * *count;
// size_t fwrite(const void *ptr, 0, 0, FILE *stream) -> 0
if (bytes == 0)
- RETURN_KNOWN(
+ RETURN_VAL(
make_unique<UnaryOp>(*ty, value_name(i),
*make_intconst(0, ty->bits()), UnaryOp::Copy));
@@ -182,7 +179,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
call->addArg(*args[3], move(param_attrs[1]));
BB.addInstr(move(load));
BB.addInstr(move(load_zext));
- RETURN_KNOWN(move(call));
+ RETURN_VAL(move(call));
}
}
}
@@ -195,7 +192,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
set_param(3, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_fopen:
ret_and_args_no_undef();
@@ -206,7 +203,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
set_param(0, ParamAttrs::ReadOnly);
set_param(1, ParamAttrs::NoCapture);
set_param(1, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_fdopen:
ret_and_args_no_undef();
@@ -215,13 +212,13 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoAlias);
set_param(1, ParamAttrs::NoCapture);
set_param(1, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_fputc:
case llvm::LibFunc_fputc_unlocked:
case llvm::LibFunc_fstat:
fputc_attr();
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_fputs_unlocked:
ret_and_args_no_undef();
@@ -230,7 +227,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
set_param(0, ParamAttrs::ReadOnly);
set_param(0, ParamAttrs::NoCapture);
set_param(1, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_clearerr:
case llvm::LibFunc_closedir:
@@ -248,7 +245,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
ret_and_args_no_undef();
attrs.set(FnAttrs::NoThrow);
set_param(0, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_fgets:
case llvm::LibFunc_fgets_unlocked:
@@ -257,7 +254,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
set_param(2, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_open:
case llvm::LibFunc_open64:
@@ -265,20 +262,20 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
set_param(0, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_read:
ret_and_args_no_undef();
attrs.set(FnAttrs::NoFree);
set_param(1, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_write:
ret_and_args_no_undef();
attrs.set(FnAttrs::NoFree);
set_param(1, ParamAttrs::NoCapture);
set_param(1, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_gets:
case llvm::LibFunc_getchar:
@@ -288,7 +285,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
ret_and_args_no_undef();
attrs.set(FnAttrs::NoThrow);
attrs.set(FnAttrs::NoFree);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_stat:
case llvm::LibFunc_lstat:
@@ -298,7 +295,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
set_param(0, ParamAttrs::NoCapture);
set_param(0, ParamAttrs::ReadOnly);
set_param(1, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_access:
case llvm::LibFunc_chmod:
@@ -315,7 +312,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
set_param(0, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_opendir:
ret_and_args_no_undef();
@@ -324,7 +321,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoAlias);
set_param(0, ParamAttrs::NoCapture);
set_param(0, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_rename:
case llvm::LibFunc_utime:
@@ -337,7 +334,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
set_param(0, ParamAttrs::ReadOnly);
set_param(1, ParamAttrs::NoCapture);
set_param(1, ParamAttrs::ReadOnly);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_getc:
case llvm::LibFunc_getc_unlocked:
@@ -349,7 +346,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoThrow);
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_gettimeofday:
ret_and_args_no_undef();
@@ -357,7 +354,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
set_param(1, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_atof:
case llvm::LibFunc_ferror:
@@ -367,7 +364,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoWrite);
attrs.set(FnAttrs::NoFree);
set_param(0, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_frexp:
case llvm::LibFunc_frexpf:
@@ -379,7 +376,7 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoThrow);
attrs.set(FnAttrs::NoFree);
set_param(1, ParamAttrs::NoCapture);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
case llvm::LibFunc_ldexp:
case llvm::LibFunc_ldexpf:
@@ -388,10 +385,10 @@ known_call(llvm::CallInst &i, const llvm::TargetLibraryInfo &TLI,
attrs.set(FnAttrs::NoThrow);
attrs.set(FnAttrs::NoFree);
attrs.set(FnAttrs::NoRead);
- RETURN_KNOWN_ATTRS();
+ RETURN_EXACT();
default:
- RETURN_UNKNOWN_KNOWN();
+ RETURN_APPROX();
}
}

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -253,7 +253,7 @@ public:
args.emplace_back(a);
}
- auto [call_val, attrs, param_attrs, valid] = known_call(i, TLI, *BB, args);
+ auto [call_val, attrs, param_attrs, approx] = known_call(i, TLI, *BB, args);
if (call_val)
RETURN_IDENTIFIER(move(call_val));
@@ -303,13 +303,9 @@ public:
auto call = make_unique<FnCall>(*ty, value_name(i),
'@' + fn->getName().str(), move(attrs),
- valid);
+ approx);
unique_ptr<Instr> ret_val;
- // avoid parsing arguments altogether for "unknown known" functions
- if (!valid)
- goto end;
-
for (uint64_t argidx = 0, nargs = i.arg_size(); argidx < nargs; ++argidx) {
auto *arg = args[argidx];
ParamAttrs attr = argidx < param_attrs.size() ? param_attrs[argidx]
@@ -376,7 +372,7 @@ public:
if (i.paramHasAttr(argidx, llvm::Attribute::Returned)) {
auto call2
= make_unique<FnCall>(Type::voidTy, "", string(call->getFnName()),
- FnAttrs(call->getAttributes()), valid);
+ FnAttrs(call->getAttributes()), approx);
for (auto &[arg, flags] : call->getArgs()) {
call2->addArg(*arg, ParamAttrs(flags));
}
@@ -399,7 +395,6 @@ public:
BB->addInstr(move(call));
RETURN_IDENTIFIER(move(ret_val));
}
-end:
RETURN_IDENTIFIER(move(call));
}

MODIFY
tests/alive-tv/bugs/pr29034-unroll.src.ll
tests/alive-tv/bugs/pr29034-unroll.src.ll
@@ -61,7 +61,7 @@ sw.bb: ; preds = %while.cond2
%5 = load %struct.__MUSIC_API*, %struct.__MUSIC_API** %dop_api4, align 8
%file_num5 = getelementptr inbounds %struct.__MUSIC_API, %struct.__MUSIC_API* %5, i64 0, i32 2
%6 = load i32, i32* %file_num5, align 1
- %call6 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([10 x i8], [10 x i8]* @.str, i64 0, i64 0), i32 %6) #6
+ %call6 = call i32 (i8*, ...) @myprintf(i8* getelementptr inbounds ([10 x i8], [10 x i8]* @.str, i64 0, i64 0), i32 %6) #6
br label %while.cond2.backedge
sw.bb7: ; preds = %while.cond2
@@ -102,6 +102,6 @@ declare i32 @music_decoder_init(%struct._MUSIC_OP_API_**)
declare i32 @music_play_api(%struct._MUSIC_OP_API_*, i32, i32, i32, i8*)
-declare i32 @printf(i8* nocapture readonly, ...)
+declare i32 @myprintf(i8* nocapture readonly, ...)
; ERROR: Source is more defined than target

DELETE
tests/alive-tv/bugs/pr36437.srctgt.ll
-; TEST-ARGS: -src-unroll=16 -tgt-unroll=16
-; ERROR: Source is more defined than target
-
-; https://bugs.llvm.org/show_bug.cgi?id=36437
-
-define i32 @src() local_unnamed_addr {
-entry:
- store i32 3, i32* @a, align 4
- br label %for.body
-
-for.body: ; preds = %entry, %for.body
- %d.05 = phi i32 [ 0, %entry ], [ -1, %for.body ]
- %0 = load i32*, i32** @c, align 8
- %1 = load i32, i32* %0, align 4
- %and = and i32 %1, %d.05
- store i32 %and, i32* %0, align 4
- %2 = load i32, i32* @a, align 4
- %sext = shl i32 %2, 16
- %conv3 = ashr exact i32 %sext, 16
- %sub = add nsw i32 %conv3, -1
- store i32 %sub, i32* @a, align 4
- %cmp = icmp eq i32 %sub, 5
- br i1 %cmp, label %for.end, label %for.body
-
-for.end: ; preds = %for.body
- %3 = load i32, i32* @b, align 4
- %call = tail call i32 (i8*, ...) @print(i8* nonnull dereferenceable(1) getelementptr inbounds ([15 x i8], [15 x i8]* @.str, i64 0, i64 0), i32 %3)
- ret i32 0
-}
-
-define i32 @tgt() local_unnamed_addr {
-entry:
- store i32 3, i32* @a, align 4
- br label %for.body
-
-for.body: ; preds = %entry, %for.body
- %phiofops = phi i32 [ 0, %entry ], [ %1, %for.body ]
- %d.05 = phi i32 [ 0, %entry ], [ -1, %for.body ]
- %0 = load i32*, i32** @c, align 8
- %1 = load i32, i32* %0, align 4
- store i32 %phiofops, i32* %0, align 4
- %2 = load i32, i32* @a, align 4
- %sext = shl i32 %2, 16
- %conv3 = ashr exact i32 %sext, 16
- %sub = add nsw i32 %conv3, -1
- store i32 %sub, i32* @a, align 4
- %cmp = icmp eq i32 %sub, 5
- br i1 %cmp, label %for.end, label %for.body
-
-for.end: ; preds = %for.body
- %3 = load i32, i32* @b, align 4
- %call = tail call i32 (i8*, ...) @print(i8* nonnull dereferenceable(1) getelementptr inbounds ([15 x i8], [15 x i8]* @.str, i64 0, i64 0), i32 %3)
- ret i32 0
-}
-
-@b = global i32 2, align 4
-@c = global i32* @b, align 8
-@a = common global i32 0, align 4
-@.str = private unnamed_addr constant [15 x i8] c"checksum = %X\0A\00", align 1
-declare i32 @print(i8*, ...)

MODIFY
tests/opt-tv/printf.opt.ll
tests/opt-tv/printf.opt.ll
@@ -8,4 +8,4 @@ define void @f() {
declare i32 @printf(i8*, ...)
-; ERROR: Invalid expr
+; ERROR: Couldn't prove the correctness of the transformation

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -156,7 +156,7 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
"Approximations done:\n";
auto approx = src_approx;
approx.insert(tgt_approx.begin(), tgt_approx.end());
- for (auto *a : approx) {
+ for (auto &a : approx) {
s << " - " << a << '\n';
}
errs.add(s.str(), false);

carry on with verification if an unknown libcall is found
semantics are overapproximated; Alive2 can gracefully fail later