diff options
author | Martin Nowack <martin_nowack@tu-dresden.de> | 2017-10-29 22:12:30 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-02-18 12:49:41 +0000 |
commit | e98449fff404a88305869849eb066def1bc0323b (patch) | |
tree | e0d4b8f828517a113bd4267fd04c359c72558a2b /lib/Core | |
parent | f751f9351f0176a3109e260a6e8e9727fc9fb4ea (diff) | |
download | klee-e98449fff404a88305869849eb066def1bc0323b.tar.gz |
Fix correct element order of InsertElement/ExtractElement
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 21 |
1 files changed, 6 insertions, 15 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index fe53fc9b..2afa6958 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2396,15 +2396,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()); @@ -2434,12 +2430,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; |