simplify code for unique fn smt name
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -726,7 +726,7 @@ StateValue FnCall::toSMT(State &s) const {
// create a new variable that can take any value if function is poison
expr val = expr::mkUF(fnName.c_str(), value_args, getType().getDummyValue());
if (!all_args_np.isTrue()) {
- auto var_name = fnName + '#' + to_string(s.nextFnCallId());
+ auto var_name = fnName + '#' + fresh_id();
auto var = expr::mkVar(var_name.c_str(), getType().getDummyValue());
s.addQuantVar(var);
val = expr::mkIf(all_args_np, val, var);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -18,12 +18,6 @@ State::State(const Function &f, bool source)
*this);
}
-void State::syncWithSrc(const State &src) {
- assert(src.isSource());
- assert(!isSource());
- next_fn_call_id = src.next_fn_call_id;
-}
-
const StateValue& State::exec(const Value &v) {
assert(undef_vars.empty());
auto val = v.toSMT(*this);

MODIFY
ir/state.h
ir/state.h
@@ -47,9 +47,6 @@ private:
predecessor_data;
std::unordered_set<const BasicBlock*> seen_bbs;
- // fn call id to be used when an argument is poison
- unsigned next_fn_call_id = 0;
-
// temp state
DomainTy domain;
Memory memory;
@@ -65,8 +62,6 @@ private:
public:
State(const Function &f, bool source);
- void syncWithSrc(const State &src);
-
const StateValue& exec(const Value &v);
const StateValue& operator[](const Value &val);
const ValTy& at(const Value &val) const;
@@ -85,8 +80,6 @@ public:
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
- unsigned nextFnCallId() { return next_fn_call_id++; }
-
void addQuantVar(const smt::expr &var);
void addUndefVar(const smt::expr &var);
void resetUndefVars();

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -272,7 +272,6 @@ Errors TransformVerify::verify() const {
try {
sym_exec(src_state);
- tgt_state.syncWithSrc(src_state);
sym_exec(tgt_state);
} catch (LoopInCFGDetected&) {
return "Loops are not supported yet! Skipping function.";

simplify code for unique fn smt name