refactor value printing in counterexamples
MODIFY
ir/type.cpp
ir/type.cpp
@@ -167,6 +167,10 @@ pair<expr, vector<expr>> VoidType::mkInput(State &s, const char *name) const {
UNREACHABLE();
}
+void VoidType::printVal(ostream &os, const expr &e) const {
+ UNREACHABLE();
+}
+
void VoidType::print(ostream &os) const {
os << "void";
}
@@ -223,6 +227,17 @@ pair<expr, vector<expr>> IntType::mkInput(State &s, const char *name) const {
return { var, { var } };
}
+void IntType::printVal(ostream &os, const expr &e) const {
+ e.printHexadecimal(os);
+ os << " (";
+ e.printUnsigned(os);
+ if (e.bits() > 1 && e.isSigned()) {
+ os << ", ";
+ e.printSigned(os);
+ }
+ os << ')';
+}
+
void IntType::print(ostream &os) const {
if (bits())
os << 'i' << bits();
@@ -320,6 +335,10 @@ pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
return { var, { var } };
}
+void FloatType::printVal(ostream &os, const expr &e) const {
+ os << e;
+}
+
void FloatType::print(ostream &os) const {
switch (fpType) {
case Quarter:
@@ -400,6 +419,10 @@ pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
return s.getMemory().mkInput(name);
}
+void PtrType::printVal(ostream &os, const expr &e) const {
+ // TODO
+}
+
void PtrType::print(ostream &os) const {
if (addr_space != 0)
os << "as(" << addr_space << ")*";
@@ -446,6 +469,10 @@ pair<expr, vector<expr>> ArrayType::mkInput(State &s, const char *name) const {
return {};
}
+void ArrayType::printVal(ostream &os, const expr &e) const {
+ // TODO
+}
+
void ArrayType::print(ostream &os) const {
os << "TODO";
}
@@ -495,6 +522,10 @@ pair<expr, vector<expr>> VectorType::mkInput(State &s, const char *name) const {
return {};
}
+void VectorType::printVal(ostream &os, const expr &e) const {
+ // TODO
+}
+
void VectorType::print(ostream &os) const {
os << "TODO";
}
@@ -589,6 +620,10 @@ pair<expr, vector<expr>> StructType::mkInput(State &s, const char *name) const {
return { move(val), move(vars) };
}
+void StructType::printVal(ostream &os, const expr &e) const {
+ // TODO
+}
+
void StructType::print(ostream &os) const {
os << '{';
bool first = true;
@@ -795,6 +830,18 @@ pair<expr, vector<expr>>
UNREACHABLE();
}
+void SymbolicType::printVal(ostream &os, const expr &e) const {
+ switch (typ) {
+ case Int: i.printVal(os, e); break;
+ case Float: f.printVal(os, e); break;
+ case Ptr: p.printVal(os, e); break;
+ case Array: a.printVal(os, e); break;
+ case Vector: v.printVal(os, e); break;
+ case Struct: s.printVal(os, e); break;
+ case Undefined: UNREACHABLE();
+ }
+}
+
void SymbolicType::print(ostream &os) const {
if (named) {
os << name;

MODIFY
ir/type.h
ir/type.h
@@ -58,6 +58,7 @@ public:
virtual std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const = 0;
+ virtual void printVal(std::ostream &os, const smt::expr &e) const = 0;
virtual void print(std::ostream &os) const = 0;
friend std::ostream& operator<<(std::ostream &os, const Type &t);
@@ -78,6 +79,7 @@ public:
void fixup(const smt::Model &m) override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -103,6 +105,7 @@ public:
smt::expr enforceIntOrPtrOrVectorType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -133,6 +136,7 @@ public:
const FloatType* getAsFloatType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -157,6 +161,7 @@ public:
smt::expr enforcePtrType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -173,6 +178,7 @@ public:
smt::expr enforceAggregateType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -190,6 +196,7 @@ public:
smt::expr enforceIntOrPtrOrVectorType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -213,6 +220,7 @@ public:
const StructType* getAsStructType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
smt::expr numElements() const;
@@ -255,6 +263,7 @@ public:
const FloatType* getAsFloatType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
mkInput(State &s, const char *name) const override;
+ void printVal(std::ostream &os, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -47,19 +47,8 @@ static void print_varval(ostream &s, const Model &m, const Value *var,
s << "undef";
return;
}
- // print floating point
- if (var->getType().getAsFloatType()) {
- s << e;
- } else {
- e.printHexadecimal(s);
- s << " (";
- e.printUnsigned(s);
- if (e.bits() > 1 && e.isSigned()) {
- s << ", ";
- e.printSigned(s);
- }
- s << ')';
- }
+
+ var->getType().printVal(s, e);
}

refactor value printing in counterexamples