File 0003-Fix-correct-element-order-of-InsertElement... of Package klee

Overview Repositories Revisions Requests Users Attributes Meta

File 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch of Package klee (Revision fcc75a63c62ae583cd946efeba7b1f8e)

Currently displaying revision fcc75a63c62ae583cd946efeba7b1f8e , Show latest

From: Martin Nowack <martin_nowack@tu-dresden.de>
Date: Sun, 29 Oct 2017 22:12:30 +0100
Subject: Fix correct element order of InsertElement/ExtractElement
Patch-mainline: no

Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
 lib/Core/Executor.cpp | 21 ++++++---------------
 1 file changed, 6 insertions(+), 15 deletions(-)

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index d836598927ce..fd1da6478fb2 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2391,15 +2391,11 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
     const unsigned elementCount = vt->getNumElements();
     llvm::SmallVector<ref<Expr>, 8> elems;
     elems.reserve(elementCount);
-    for (unsigned i = 0; i < elementCount; ++i) {
-      // evalConstant() will use ConcatExpr to build vectors with the
-      // zero-th element leftmost (most significant bits), followed
-      // by the next element (second leftmost) and so on. This means
-      // that we have to adjust the index so we read left to right
-      // rather than right to left.
-      unsigned bitOffset = EltBits * (elementCount - i - 1);
-      elems.push_back(i == iIdx ? newElt
-                                : ExtractExpr::create(vec, bitOffset, EltBits));
+    for (unsigned i = elementCount; i != 0; --i) {
+      auto of = i - 1;
+      unsigned bitOffset = EltBits * of;
+      elems.push_back(
+          of == iIdx ? newElt : ExtractExpr::create(vec, bitOffset, EltBits));
     }
 
     ref<Expr> Result = ConcatExpr::createN(elementCount, elems.data());
@@ -2429,12 +2425,7 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) {
       return;
     }
 
-    // evalConstant() will use ConcatExpr to build vectors with the
-    // zero-th element left most (most significant bits), followed
-    // by the next element (second left most) and so on. This means
-    // that we have to adjust the index so we read left to right
-    // rather than right to left.
-    unsigned bitOffset = EltBits*(vt->getNumElements() - iIdx -1);
+    unsigned bitOffset = EltBits * iIdx;
     ref<Expr> Result = ExtractExpr::create(vec, bitOffset, EltBits);
     bindLocal(ki, state, Result);
     break;
-- 
2.15.1

Places

File 0003-Fix-correct-element-order-of-InsertElement-ExtractEl.patch of Package klee (Revision fcc75a63c62ae583cd946efeba7b1f8e)

Places