try to explain the reason behind an 'invalid expr' message
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -308,14 +308,22 @@ static StateValue fm_poison(State &s, expr a, const expr &ap, expr b,
if (!only_input)
non_poison &= !val.isInf();
}
- if (fmath.flags & FastMathFlags::ARCP)
+ if (fmath.flags & FastMathFlags::ARCP) {
+ s.useUnsupported("arcp");
non_poison &= expr(); // TODO
- if (fmath.flags & FastMathFlags::Contract)
+ }
+ if (fmath.flags & FastMathFlags::Contract) {
+ s.useUnsupported("contract");
non_poison &= expr(); // TODO
- if (fmath.flags & FastMathFlags::Reassoc)
+ }
+ if (fmath.flags & FastMathFlags::Reassoc) {
+ s.useUnsupported("reassoc");
non_poison &= expr(); // TODO
- if (fmath.flags & FastMathFlags::AFN)
+ }
+ if (fmath.flags & FastMathFlags::AFN) {
+ s.useUnsupported("afn");
non_poison &= expr(); // TODO
+ }
if (fmath.flags & FastMathFlags::NSZ && !only_input)
val = any_fp_zero(s, move(val));
@@ -579,6 +587,7 @@ StateValue BinOp::toSMT(State &s) const {
case FRem:
fn = [&](auto a, auto ap, auto b, auto bp) -> StateValue {
// TODO; Z3 has no support for LLVM's frem which is actually an fmod
+ s.useUnsupported("frem");
return fm_poison(s, a, ap, b, bp, [](expr &a, expr &b) { return expr(); },
fmath, false);
};
@@ -1204,6 +1213,7 @@ StateValue ConversionOp::toSMT(State &s) const {
break;
case Int2Ptr:
fn = [&](auto &&val, auto &to_type) -> StateValue {
+ s.useUnsupported("inttoptr");
return { s.getMemory().int2ptr(val), true };
};
break;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -357,6 +357,10 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return I->second.retvals;
}
+void State::useUnsupported(const char *name) {
+ used_unsupported.emplace(name);
+}
+
void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}

MODIFY
ir/state.h
ir/state.h
@@ -68,6 +68,8 @@ private:
smt::AndExpr precondition;
smt::AndExpr axioms;
+ std::set<const char*> used_unsupported;
+
const BasicBlock *current_bb = nullptr;
std::set<smt::expr> quantified_vars;
@@ -155,6 +157,9 @@ public:
std::vector<Memory::PtrInput> &&ptr_inputs,
const std::vector<Type*> &out_types, const FnAttrs &attrs);
+ void useUnsupported(const char *name);
+ auto& getUnsupported() const { return used_unsupported; }
+
void addQuantVar(const smt::expr &var);
void addUndefVar(smt::expr &&var);
auto& getUndefVars() const { return undef_vars; }

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -109,6 +109,18 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
if (r.isInvalid()) {
errs.add("Invalid expr", false);
+ auto &unsupported = src_state.getUnsupported();
+ if (!unsupported.empty()) {
+ string str = "The program uses the following unsupported features: ";
+ bool first = true;
+ for (auto name : unsupported) {
+ if (!first)
+ str += ", ";
+ str += name;
+ first = false;
+ }
+ errs.add(move(str), false);
+ }
return;
}

try to explain the reason behind an 'invalid expr' message