fix printing counterexamples with constant inputs (e.g. C1)
fixes
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -95,7 +95,13 @@ expr AggregateConst::getTypeConstraints() const {
StateValue ConstantInput::toSMT(State &s) const {
- return { expr::mkVar(getName().c_str(), bits()), true };
+ auto type = getType().getDummyValue(false).value;
+ return { expr::mkVar(getName().c_str(), type), true };
+}
+
+expr ConstantInput::getTypeConstraints() const {
+ return Value::getTypeConstraints() &&
+ (getType().enforceIntType() || getType().enforceFloatType());
}

MODIFY
ir/constant.h
ir/constant.h
@@ -56,6 +56,7 @@ public:
ConstantInput(Type &type, std::string &&name)
: Constant(type, std::move(name)) {}
StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
};

MODIFY
ir/function.cpp
ir/function.cpp
@@ -94,7 +94,9 @@ void Function::addUndef(unique_ptr<UndefValue> &&u) {
undefs.emplace_back(move(u));
}
-void Function::addInput(unique_ptr<Input> &&i) {
+void Function::addInput(unique_ptr<Value> &&i) {
+ assert(dynamic_cast<Input *>(i.get()) ||
+ dynamic_cast<ConstantInput*>(i.get()));
inputs.emplace_back(move(i));
}

MODIFY
ir/function.h
ir/function.h
@@ -91,7 +91,7 @@ public:
return undefs;
}
- void addInput(std::unique_ptr<Input> &&c);
+ void addInput(std::unique_ptr<Value> &&c);
util::const_strip_unique_ptr<decltype(inputs)> getInputs() const {
return inputs;
}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -69,7 +69,7 @@ static Value& get_constant(string_view name, Type &type) {
auto c = make_unique<ConstantInput>(type, string(id));
auto ret = c.get();
- fn->addConstant(move(c));
+ fn->addInput(move(c));
identifiers.emplace(move(id), ret);
return *ret;
}
@@ -1070,6 +1070,10 @@ vector<Transform> parse(string_view buf) {
auto input = make_unique<Input>(val->getType(), string(name));
identifiers_tgt.emplace(name, input.get());
t.tgt.addInput(move(input));
+ } else if (dynamic_cast<ConstantInput*>(val)) {
+ auto input = make_unique<ConstantInput>(val->getType(), string(name));
+ identifiers_tgt.emplace(name, input.get());
+ t.tgt.addInput(move(input));
}
}
identifiers_src = move(identifiers);

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -128,7 +128,8 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
for (auto &[var, val, used] : src_state.getValues()) {
(void)used;
- if (!dynamic_cast<const Input*>(var))
+ if (!dynamic_cast<const Input*>(var) &&
+ !dynamic_cast<const ConstantInput*>(var))
continue;
s << *var << " = ";
print_varval(s, src_state, m, var, var->getType(), val.first);

fix printing counterexamples with constant inputs (e.g. C1)
fixes #125