stub out phi nodes
MODIFY
.gitignore
.gitignore
.vs
+.vscode
build*/
*.pyc
CMakeSettings.json

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -487,6 +487,36 @@ expr CopyOp::getTypeConstraints(const Function &f) const {
}
+void Phi::print(ostream &os) const {
+ os << getName() << " = phi ";
+ auto t = getType().toString();
+ if (!t.empty())
+ os << t << ' ';
+
+ bool first = true;
+ for (auto &[val, bb] : values) {
+ if (!first)
+ os << ", ";
+ os << "[ " << val.getName() << ", " << bb << " ]";
+ first = false;
+ }
+}
+
+StateValue Phi::toSMT(State &s) const {
+ // TODO
+ return {};
+}
+
+expr Phi::getTypeConstraints(const Function &f) const {
+ auto c = Value::getTypeConstraints();
+ for (auto &[val, bb] : values) {
+ (void)bb;
+ c &= val.getType() == getType();
+ }
+ return c;
+}
+
+
void Branch::print(ostream &os) const {
os << "br ";
if (cond)

MODIFY
ir/instr.h
ir/instr.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/value.h"
+#include <string>
+#include <utility>
+#include <vector>
namespace IR {
@@ -133,6 +136,21 @@ public:
};
+class Phi final : public Instr {
+public:
+ typedef std::vector<std::pair<Value&, std::string>> ValTy;
+private:
+ ValTy values;
+public:
+ Phi(Type &type, std::string &&name, ValTy &&values)
+ : Instr(type, std::move(name)), values(std::move(values)) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
+};
+
+
class Branch final : public Instr {
Value *cond = nullptr;
const BasicBlock &dst_true, *dst_false = nullptr;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -879,7 +879,7 @@ expr expr::subst(const expr &from, const expr &to) const {
return Z3_substitute(ctx(), ast(), 1, &f, &t);
}
-void expr::printUnsigned(std::ostream &os) const {
+void expr::printUnsigned(ostream &os) const {
expr zero = mkUInt(0, sort());
expr ten = mkUInt(10, sort());
expr n = *this;
@@ -898,7 +898,7 @@ void expr::printUnsigned(std::ostream &os) const {
os << str;
}
-void expr::printSigned(std::ostream &os) const {
+void expr::printSigned(ostream &os) const {
if (isSigned()) {
os << '-';
(~*this + mkUInt(1, sort())).simplify().printUnsigned(os);
@@ -907,7 +907,7 @@ void expr::printSigned(std::ostream &os) const {
}
}
-void expr::printHexadecimal(std::ostream &os) const {
+void expr::printHexadecimal(ostream &os) const {
auto rem = bits() % 4;
os << (rem == 0 ? *this : zext(4 - rem)).simplify();
}

stub out phi nodes