The expansion for Read{MSB,LSB} needs to continue to use the folding methods,

otherwise we build expressions that won't be matched later when we print them.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73347 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 9 insertions, 7 deletions

diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp
index c978fe0b..2b9777cb 100644
--- a/lib/Expr/Parser.cpp
+++ b/lib/Expr/Parser.cpp
@@ -1255,14 +1255,16 @@ ExprResult ParserImpl::ParseAnyReadParenExpr(const Token &Name,
       Error("invalid ordered read (not multiple of range type).", Name);
       return Builder->Constant(0, ResTy);
     }
-    std::vector<ExprHandle> Kids;
-    Kids.reserve(NumReads);
+    std::vector<ExprHandle> Kids(NumReads);
     ExprHandle Index = IndexExpr.get();
-    for (unsigned i=0; i<NumReads; ++i) {
-      // FIXME: using folding here
-      ExprHandle OffsetIndex = Builder->Add(IndexExpr.get(),
-                                            Builder->Constant(i, ArrayDomainType));
-      Kids.push_back(Builder->Read(Array.get(), OffsetIndex));
+    for (unsigned i=0; i != NumReads; ++i) {
+      // FIXME: We rely on folding here to not complicate things to where the
+      // Read macro pattern fails to match.
+      ExprHandle OffsetIndex = Index;
+      if (i)
+        OffsetIndex = AddExpr::create(OffsetIndex,
+                                      Builder->Constant(i, ArrayDomainType));
+      Kids[i] = Builder->Read(Array.get(), OffsetIndex);
     }
     if (Kind == eMacroKind_ReadLSB)
       std::reverse(Kids.begin(), Kids.end());