small tweaks to error tracking
MODIFY
ir/state.cpp
ir/state.cpp
#include "ir/state.h"
#include "ir/function.h"
#include "smt/smt.h"
+#include "util/errors.h"
#include <cassert>
using namespace smt;
+using namespace util;
using namespace std;
namespace IR {
@@ -53,7 +55,7 @@ const StateValue& State::operator[](const Value &val) {
}
if (hit_half_memory_limit())
- throw OutOfMemory();
+ throw AliveException("Out of memory; skipping function.", false);
auto sval_new = sval.subst(repls);
if (sval_new.eq(sval)) {
@@ -115,7 +117,8 @@ bool State::startBB(const BasicBlock &bb) {
void State::addJump(const BasicBlock &dst, expr &&cond) {
if (seen_bbs.count(&dst))
- throw LoopInCFGDetected();
+ throw AliveException("Loops are not supported yet! Skipping function.",
+ false);
cond &= domain.first;
auto p = predecessor_data[&dst].try_emplace(current_bb, DomainTy({}, {}),

MODIFY
ir/state.h
ir/state.h
namespace IR {
-struct LoopInCFGDetected : public std::exception {};
-struct OutOfMemory : public std::exception {};
-
class Value;
class BasicBlock;
class Function;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -107,12 +107,12 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
const char *msg, bool check_each_var) {
if (r.isInvalid()) {
- errs.add("Invalid expr");
+ errs.add("Invalid expr", false);
return;
}
if (r.isUnknown()) {
- errs.add("Timeout");
+ errs.add("Timeout", false);
return;
}
@@ -171,7 +171,7 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
print_varval(s, tgt_state, m, var, type, tgt);
}
- errs.add(s.str());
+ errs.add(s.str(), true);
}
@@ -264,7 +264,7 @@ static void check_refinement(Errors &errs, Transform &t,
pre &= src_state.getPre() && tgt_state.getPre();
if (check_expr(axioms && preprocess(t, qvars, uvars, expr(pre))).isUnsat()) {
- errs.add("Precondition is always false");
+ errs.add("Precondition is always false", false);
return;
}
@@ -308,10 +308,8 @@ Errors TransformVerify::verify() const {
sym_exec(src_state);
tgt_state.copyGlobalVarBidsFromSrc(src_state);
sym_exec(tgt_state);
- } catch (LoopInCFGDetected&) {
- return "Loops are not supported yet! Skipping function.";
- } catch (OutOfMemory&) {
- return "Out of memory; skipping function.";
+ } catch (AliveException e) {
+ return move(e);
}
Errors errs;

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -125,11 +125,7 @@ struct TVPass : public llvm::FunctionPass {
if (Errors errs = verifier.verify()) {
*out << "Transformation doesn't verify!\n" << errs << endl;
- if (opt_error_fatal &&
- !errs.isTimeout() &&
- !errs.isInvalidExpr() &&
- !errs.isOOM() &&
- !errs.isLoopyCFG())
+ if (opt_error_fatal && errs.isUnsound())
llvm::report_fatal_error("Alive2: Transform doesn't verify; aborting!");
} else {
*out << "Transformation seems to be correct!\n\n";

MODIFY
util/errors.cpp
util/errors.cpp
@@ -7,42 +7,43 @@ using namespace std;
namespace util {
-Errors::Errors(const char *str) {
- add(str);
+Errors::Errors(const char *str, bool is_unsound) {
+ add(str, is_unsound);
}
-Errors::Errors(string &&str) {
- add(move(str));
+Errors::Errors(string &&str, bool is_unsound) {
+ add(move(str), is_unsound);
}
-void Errors::add(const char *str) {
- errs.emplace_back(str);
+Errors::Errors(AliveException &&e) {
+ add(move(e));
}
-void Errors::add(string &&str) {
- errs.emplace_back(str);
+void Errors::add(const char *str, bool is_unsound) {
+ errs.emplace_back(str, is_unsound);
}
-bool Errors::isTimeout() const {
- return errs.size() == 1 && errs[0] == "Timeout";
+void Errors::add(string &&str, bool is_unsound) {
+ errs.emplace_back(move(str), is_unsound);
}
-bool Errors::isInvalidExpr() const {
- return errs.size() == 1 && errs[0] == "Invalid expr";
+void Errors::add(AliveException &&e) {
+ add(move(e.msg), e.is_unsound);
}
-bool Errors::isOOM() const {
- return errs.size() == 1 && errs[0] == "Out of memory; skipping function.";
+bool Errors::isUnsound() const {
+ for (auto &[msg, unsound] : errs) {
+ (void)msg;
+ if (unsound)
+ return true;
}
-
-bool Errors::isLoopyCFG() const {
- return errs.size() == 1 &&
- errs[0] == "Loops are not supported yet! Skipping function.";
+ return false;
}
ostream& operator<<(ostream &os, const Errors &errs) {
- for (auto &err : errs.errs) {
- os << "ERROR: " << err << '\n';
+ for (auto &[msg, unsound] : errs.errs) {
+ (void)unsound;
+ os << "ERROR: " << msg << '\n';
}
return os;
}

MODIFY
util/errors.h
util/errors.h
#include <ostream>
#include <string>
+#include <utility>
#include <vector>
namespace util {
+struct AliveException {
+ std::string msg;
+ bool is_unsound;
+
+public:
+ AliveException(std::string &&msg, bool is_unsound)
+ : msg(std::move(msg)), is_unsound(is_unsound) {}
+};
+
+
class Errors {
- std::vector<std::string> errs;
+ std::vector<std::pair<std::string, bool>> errs;
public:
Errors() = default;
- Errors(const char *str);
- Errors(std::string &&str);
- void add(const char *str);
- void add(std::string &&str);
+ Errors(const char *str, bool is_unsound);
+ Errors(std::string &&str, bool is_unsound);
+ Errors(AliveException &&e);
+
+ void add(const char *str, bool is_unsound);
+ void add(std::string &&str, bool is_unsound);
+ void add(AliveException &&e);
+
explicit operator bool() const { return !errs.empty(); }
- bool isTimeout() const;
- bool isInvalidExpr() const;
- bool isOOM() const;
- bool isLoopyCFG() const; // FIXME
+ bool isUnsound() const;
friend std::ostream& operator<<(std::ostream &os, const Errors &e);
};

small tweaks to error tracking