fix crash when using vectors and returned paramter attr
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2836,6 +2836,19 @@ check_ret_attributes(State &s, StateValue &&sv, const Type &t,
return check_return_value(s, std::move(sv), t, attrs, true);
}
+static void eq_val_rec(State &s, const Type &t, const StateValue &a,
+ const StateValue &b) {
+ if (auto agg = t.getAsAggregateType()) {
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ if (agg->isPadding(i))
+ continue;
+ eq_val_rec(s, agg->getChild(i), agg->extract(a, i), agg->extract(b, i));
+ }
+ return;
+ }
+ s.addUB(a == b);
+}
+
StateValue Return::toSMT(State &s) const {
StateValue retval;
@@ -2851,12 +2864,8 @@ StateValue Return::toSMT(State &s) const {
if (attrs.has(FnAttrs::NoReturn))
s.addUB(expr(false));
- if (auto *val_returned = s.getFn().getReturnedInput()) {
- // LangRef states that return type must be valid operands for bitcasts,
- // which cannot be aggregate type.
- assert(!dynamic_cast<AggregateType *>(&val->getType()));
- s.addUB(retval == s[*val_returned]);
- }
+ if (auto &val_returned = s.getReturnedInput())
+ eq_val_rec(s, getType(), retval, *val_returned);
s.addReturn(std::move(retval));
return {};

MODIFY
ir/state.cpp
ir/state.cpp
@@ -997,6 +997,12 @@ void State::finishInitializer() {
is_initialization_phase = false;
}
+void State::saveReturnedInput() {
+ assert(isSource());
+ if (auto *ret = getFn().getReturnedInput())
+ returned_input = (*this)[*ret];
+}
+
expr State::sinkDomain() const {
auto I = predecessor_data.find(&f.getSinkBB());
if (I == predecessor_data.end())
@@ -1047,6 +1053,8 @@ void State::syncSEdataWithSrc(const State &src) {
for (auto &itm : glbvar_bids)
itm.second.second = false;
+ returned_input = src.returned_input;
+
fn_call_data = src.fn_call_data;
inaccessiblemem_bids = src.inaccessiblemem_bids;
memory.syncWithSrc(src.returnMemory());

MODIFY
ir/state.h
ir/state.h
@@ -123,6 +123,9 @@ private:
// Global variables' memory block ids & Memory::alloc has been called?
std::unordered_map<std::string, std::pair<unsigned, bool>> glbvar_bids;
+ // The value of a 'returned' input
+ std::optional<StateValue> returned_input;
+
// temp state
const BasicBlock *current_bb = nullptr;
CurrentDomain domain;
@@ -252,6 +255,11 @@ public:
const auto& getQuantVars() const { return quantified_vars; }
const auto& getFnQuantVars() const { return fn_call_qvars; }
+ void saveReturnedInput();
+ const std::optional<StateValue>& getReturnedInput() const {
+ return returned_input;
+ }
+
smt::expr sinkDomain() const;
Memory returnMemory() const { return *return_memory(); }

ADD
tests/alive-tv/attrs/returned-4.srctgt.ll
+define <2 x i4> @src(<2 x i4> %0) {
+ ret <2 x i4> %0
+}
+
+define <2 x i4> @tgt(<2 x i4> returned %0) {
+ ret <2 x i4> %0
+}

ADD
tests/alive-tv/attrs/returned-fail2.srctgt.ll
+; ERROR: Value mismatch
+
+define <2 x i4> @src(<2 x i4> %0) {
+ ret <2 x i4> %0
+}
+
+define <2 x i4> @tgt(<2 x i4> returned %0) {
+ ret <2 x i4> zeroinitializer
+}

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -36,6 +36,9 @@ void sym_exec(State &s) {
}
}
+ if (s.isSource())
+ s.saveReturnedInput();
+
s.exec(Value::voidVal);
bool first = true;

fix #815: crash when using vectors and returned paramter attr