correctly transfer all bindings when analysing a wrapped precondition.

Author: cemcebeci

lib/dialect/include/rlc/dialect/DynamicArgumentAnalysis.hpp

@@ -74,7 +74,7 @@ enum TermType {
     Example: arg = arg2, memberAddress = [2, 1] maps to MemberAccess(MemberAccess(arg,2), 1)
 */
 struct UnboundValue {
-    mlir::Value argument;
+    mlir::BlockArgument argument;
     llvm::SmallVector<uint64_t> memberAddress;
 
     /*

lib/dialect/src/DynamicArgumentAnalysisPass.cpp

@@ -272,6 +272,17 @@ DeducedConstraints DynamicArgumentAnalysis::findImposedConstraints(mlir::rlc::Ca
         }
         assert(argIndex != -1 && "Expected to find the argument.");
         DynamicArgumentAnalysis analysis(underlyingFunction, knownArgsOfUnderlyingFunction, argPicker, builder, loc);
+        for(auto binding: bindings) {
+            if(binding.first.memberAddress.size() != 0) {
+                // the binding does not just correspond to an argument.
+                auto indexOfArg = std::distance(
+                    call.getArgs().begin(),
+                    llvm::find(call.getArgs(), unbound.argument));
+                // add an equivalent binding using the callee's arg.
+                UnboundValue newUnboundValue {underlyingFunction.getPrecondition().getArgument(indexOfArg), binding.first.memberAddress};
+                analysis.bindings.emplace_back(std::pair(newUnboundValue, binding.second));
+            }
+        }
         UnboundValue correspongindUnboundValue {underlyingFunction.getPrecondition().getArgument(argIndex), unbound.memberAddress};
         return analysis.deduceIntegerUnboundValueConstraints(correspongindUnboundValue);
     }

tool/rlc/test/fuzzer_pick_struct.rl

@@ -19,7 +19,7 @@ act subact(ctx Test context_struct) -> Subact:
         t1.a == context_struct.b,
         t1.b > context_struct.a,
         t1.b < subact_frame_var,
-        t1.inner.c == context_struct.b 
+        t1.inner.c == context_struct.b + t1.b
     }
 
 act play() -> Play: