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

Author: nunoplopes

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 {};

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());

ir/state.h

@@ -123,6 +123,9 @@ class State {
   // 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 @@ class State {
   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(); }
 

tests/alive-tv/attrs/returned-4.srctgt.ll

@@ -0,0 +1,7 @@
+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
+}

tests/alive-tv/attrs/returned-fail2.srctgt.ll

@@ -0,0 +1,9 @@
+; 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
+}

util/symexec.cpp

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