support verification of functions with changed argument names (though same number and order)
MODIFY
ir/function.cpp
ir/function.cpp
#include "ir/function.h"
#include "ir/instr.h"
+#include "util/errors.h"
using namespace smt;
+using namespace util;
using namespace std;
namespace IR {
@@ -108,6 +110,20 @@ bool Function::hasReturn() const {
return false;
}
+void Function::syncDataWithSrc(const Function &src) {
+ auto IS = src.inputs.begin(), ES = src.inputs.end();
+ auto IT = inputs.begin(), ET = inputs.end();
+
+ for (; IS != ES && IT != ET; ++IS, ++IT) {
+ if (auto in_tgt = dynamic_cast<Input*>(IT->get()))
+ in_tgt->copySMTName(*dynamic_cast<Input*>(IS->get()));
+ }
+
+ if (IS != ES || IT != ET)
+ throw AliveException("Source and target have different number of args",
+ false);
+}
+
Function::instr_iterator::
instr_iterator(vector<BasicBlock*>::const_iterator &&BBI,
vector<BasicBlock*>::const_iterator &&BBE)

MODIFY
ir/function.h
ir/function.h
@@ -98,6 +98,8 @@ public:
bool hasReturn() const;
+ void syncDataWithSrc(const Function &src);
+
auto& getBBs() { return BB_order; }
const auto& getBBs() const { return BB_order; }

MODIFY
ir/value.cpp
ir/value.cpp
@@ -115,6 +115,13 @@ StateValue GlobalVariable::toSMT(State &s) const {
}
+Input::Input(Type &type, string &&name)
+ : Value(type, string(name)), smt_name(move(name)) {}
+
+void Input::copySMTName(const Input &other) {
+ smt_name = other.smt_name;
+}
+
void Input::print(ostream &os) const {
UNREACHABLE();
}
@@ -123,7 +130,7 @@ StateValue Input::toSMT(State &s) const {
// 00: normal, 01: undef, else: poison
expr type = getTyVar();
- auto [val, vars] = getType().mkInput(s, getName().c_str());
+ auto [val, vars] = getType().mkInput(s, smt_name.c_str());
if (!config::disable_undef_input) {
vector<pair<expr, expr>> repls;
@@ -148,7 +155,7 @@ StateValue Input::toSMT(State &s) const {
}
expr Input::getTyVar() const {
- string tyname = "ty_" + getName();
+ string tyname = "ty_" + smt_name;
return expr::mkVar(tyname.c_str(), 2);
}

MODIFY
ir/value.h
ir/value.h
@@ -105,9 +105,10 @@ public:
class Input final : public Value {
+ std::string smt_name;
public:
- Input(Type &type, std::string &&name) :
- Value(type, std::move(name)) {}
+ Input(Type &type, std::string &&name);
+ void copySMTName(const Input &other);
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
smt::expr getTyVar() const;

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -1069,13 +1069,15 @@ vector<Transform> parse(string_view buf) {
// copy inputs from src to target
decltype(identifiers) identifiers_tgt;
- for (auto &[name, val] : identifiers) {
- if (dynamic_cast<Input*>(val)) {
- auto input = make_unique<Input>(val->getType(), string(name));
+ for (auto &val : t.src.getInputs()) {
+ auto &name = val.getName();
+ if (dynamic_cast<const Input*>(&val)) {
+ 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));
+ } else {
+ assert(dynamic_cast<const ConstantInput*>(&val));
+ auto input = make_unique<ConstantInput>(val.getType(), string(name));
identifiers_tgt.emplace(name, input.get());
t.tgt.addInput(move(input));
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -298,6 +298,8 @@ TransformVerify::TransformVerify(Transform &t, bool check_each_var) :
tgt_instrs.emplace(i.getName(), &i);
}
}
+
+ t.tgt.syncDataWithSrc(t.src);
}
Errors TransformVerify::verify() const {
@@ -374,20 +376,6 @@ TypingAssignments TransformVerify::getTypings() const {
// return type
c &= t.src.getType() == t.tgt.getType();
- // input types
- {
- unordered_map<string, const Value*> tgt_inputs;
- for (auto &i : t.tgt.getInputs()) {
- tgt_inputs.emplace(i.getName(), &i);
- }
-
- for (auto &i : t.src.getInputs()) {
- auto tgt_i = tgt_inputs.find(i.getName());
- if (tgt_i != tgt_inputs.end())
- c &= i.getType() == tgt_i->second->getType();
- }
- }
-
if (check_each_var) {
for (auto &i : t.src.instrs()) {
c &= i.eqType(*tgt_instrs.at(i.getName()));

support verification of functions with changed argument names (though same number and order)