Jiri Slaby
3afdc30a7b
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=32
53 lines
2.2 KiB
Diff
53 lines
2.2 KiB
Diff
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 0b7aa1a97f68..dcb8d30e0ffa 100644
|
|
--- a/lib/Core/Executor.cpp
|
|
+++ b/lib/Core/Executor.cpp
|
|
@@ -2392,15 +2392,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());
|
|
@@ -2430,12 +2426,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.0
|
|
|