diff options
| -rw-r--r-- | include/klee/ArrayExprOptimizer.h | 35 | ||||
| -rw-r--r-- | include/klee/ArrayExprRewriter.h | 25 | ||||
| -rw-r--r-- | include/klee/AssignmentGenerator.h | 9 | ||||
| -rw-r--r-- | include/klee/util/ArrayExprVisitor.h | 19 | ||||
| -rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 42 | ||||
| -rw-r--r-- | lib/Expr/ArrayExprRewriter.cpp | 209 | ||||
| -rw-r--r-- | lib/Expr/ArrayExprVisitor.cpp | 10 | ||||
| -rw-r--r-- | lib/Expr/AssignmentGenerator.cpp | 12 |
8 files changed, 223 insertions, 138 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h index 982136fb..9b62571f 100644 --- a/include/klee/ArrayExprOptimizer.h +++ b/include/klee/ArrayExprOptimizer.h @@ -1,3 +1,12 @@ +//===-- ArrayExprOptimizer.h ----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #ifndef KLEE_EXPROPTIMIZER_H #define KLEE_EXPROPTIMIZER_H @@ -52,39 +61,39 @@ extern llvm::cl::opt<double> ArrayValueSymbRatio; class Expr; template <class T> class ref; -typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty; +typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty; typedef std::vector<const Array *> v_arr_ty; -typedef std::map<ref<Expr>, std::vector<ref<Expr> > > mapIndexOptimizedExpr_ty; +typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty; class ExprOptimizer { private: - unordered_map<unsigned, ref<Expr> > cacheExprOptimized; + unordered_map<unsigned, ref<Expr>> cacheExprOptimized; unordered_set<unsigned> cacheExprUnapplicable; - unordered_map<unsigned, ref<Expr> > cacheReadExprOptimized; + unordered_map<unsigned, ref<Expr>> cacheReadExprOptimized; public: void optimizeExpr(const ref<Expr> &e, ref<Expr> &result, bool valueOnly = false); private: - bool computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, - std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx) - const; + bool + computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, + std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx) const; ref<Expr> getSelectOptExpr( const ref<Expr> &e, std::vector<const ReadExpr *> &reads, - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo, + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo, bool isSymbolic); ref<Expr> buildConstantSelectExpr(const ref<Expr> &index, - std::vector<uint64_t> &arrayValues, - Expr::Width width, unsigned elementsInArray) const; + std::vector<uint64_t> &arrayValues, + Expr::Width width, + unsigned elementsInArray) const; ref<Expr> buildMixedSelectExpr(const ReadExpr *re, - std::vector<std::pair<uint64_t, bool> > &arrayValues, - Expr::Width width, unsigned elementsInArray) const; - + std::vector<std::pair<uint64_t, bool>> &arrayValues, + Expr::Width width, unsigned elementsInArray) const; }; } diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h index dafcfef6..3828262a 100644 --- a/include/klee/ArrayExprRewriter.h +++ b/include/klee/ArrayExprRewriter.h @@ -1,3 +1,12 @@ +//===-- ArrayExprRewriter.h -----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #ifndef LIB_EXPRREWRITER_H_ #define LIB_EXPRREWRITER_H_ @@ -13,23 +22,23 @@ namespace klee { typedef std::vector<const Array *> v_arr_ty; -typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty; -typedef std::map<ref<Expr>, std::vector<ref<Expr> > > mapIndexOptimizedExpr_ty; +typedef std::map<const Array *, std::vector<ref<Expr>>> array2idx_ty; +typedef std::map<ref<Expr>, std::vector<ref<Expr>>> mapIndexOptimizedExpr_ty; class ExprRewriter { public: - static ref<Expr> createOptExpr( - const ref<Expr> &e, const array2idx_ty &arrays, - const std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx); + static ref<Expr> + createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays, + const std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx); private: static ref<Expr> rewrite(const ref<Expr> &e, const array2idx_ty &arrays, - const std::map<ref<Expr>, std::vector<ref<Expr> > > &idx_valIdx); + const std::map<ref<Expr>, std::vector<ref<Expr>>> &idx_valIdx); static ref<Expr> - concatenateOrExpr(const std::vector<ref<Expr> >::const_iterator begin, - const std::vector<ref<Expr> >::const_iterator end); + concatenateOrExpr(const std::vector<ref<Expr>>::const_iterator begin, + const std::vector<ref<Expr>>::const_iterator end); static ref<Expr> createEqExpr(const ref<Expr> &index, const ref<Expr> &valIndex); diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h index 835651b8..aa228755 100644 --- a/include/klee/AssignmentGenerator.h +++ b/include/klee/AssignmentGenerator.h @@ -1,3 +1,12 @@ +//===-- AssignmentGenerator.h ---------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #ifndef KLEE_ASSIGNMENTGENERATOR_H #define KLEE_ASSIGNMENTGENERATOR_H diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h index 70495989..6d7529e9 100644 --- a/include/klee/util/ArrayExprVisitor.h +++ b/include/klee/util/ArrayExprVisitor.h @@ -1,3 +1,12 @@ +//===-- ArrayExprVisitor.h ------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #ifndef KLEE_ARRAYEXPRVISITOR_H_ #define KLEE_ARRAYEXPRVISITOR_H_ @@ -33,7 +42,7 @@ public: //--------------------------- INDEX-BASED OPTIMIZATION-----------------------// class ConstantArrayExprVisitor : public ExprVisitor { private: - typedef std::map<const Array *, std::vector<ref<Expr> > > bindings_ty; + typedef std::map<const Array *, std::vector<ref<Expr>>> bindings_ty; bindings_ty &arrays; // Avoids adding the same index twice unordered_set<unsigned> addedIndexes; @@ -91,7 +100,7 @@ public: class ArrayReadExprVisitor : public ExprVisitor { private: std::vector<const ReadExpr *> &reads; - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo; + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo; bool symbolic; bool incompatible; @@ -104,7 +113,7 @@ protected: public: ArrayReadExprVisitor( std::vector<const ReadExpr *> &_reads, - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &_readInfo) + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &_readInfo) : ExprVisitor(true), reads(_reads), readInfo(_readInfo), symbolic(false), incompatible(false) {} inline bool isIncompatible() { return incompatible; } @@ -114,14 +123,14 @@ public: class ArrayValueOptReplaceVisitor : public ExprVisitor { private: unordered_set<unsigned> visited; - std::map<unsigned, ref<Expr> > optimized; + std::map<unsigned, ref<Expr>> optimized; protected: Action visitConcat(const ConcatExpr &); Action visitRead(const ReadExpr &re); public: - ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr> > &_optimized, + ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr>> &_optimized, bool recursive = true) : ExprVisitor(recursive), optimized(_optimized) {} }; diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 86c19a81..b3e8bca0 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -1,3 +1,12 @@ +//===-- ArrayExprOptimizer.cpp --------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "klee/ArrayExprOptimizer.h" #include "klee/ArrayExprRewriter.h" @@ -91,7 +100,7 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, if (OptimizeArray == VALUE || (OptimizeArray == ALL && (!result.get() || valueOnly))) { std::vector<const ReadExpr *> reads; - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > readInfo; + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> readInfo; ArrayReadExprVisitor are(reads, readInfo); are.visit(e); std::reverse(reads.begin(), reads.end()); @@ -147,7 +156,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, for (size_t aIdx = 0; aIdx < arr->constantValues.size(); aIdx += width) { Assignment *a = new Assignment(); v_arr_ty objects; - std::vector<std::vector<unsigned char> > values; + std::vector<std::vector<unsigned char>> values; // For each symbolic index Expr(k) found for (auto &index_it : element.second) { @@ -162,7 +171,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, ref<Expr> evaluation = a->evaluate(e); if (assignmentSuccess && evaluation->isTrue()) { if (idx_valIdx.find(idx) == idx_valIdx.end()) { - idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr> >())); + idx_valIdx.insert(std::make_pair(idx, std::vector<ref<Expr>>())); } idx_valIdx[idx] .push_back(ConstantExpr::alloc(aIdx, arr->getDomain())); @@ -176,14 +185,14 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, ref<Expr> ExprOptimizer::getSelectOptExpr( const ref<Expr> &e, std::vector<const ReadExpr *> &reads, - std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo, + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width>> &readInfo, bool isSymbolic) { ref<Expr> notFound; ref<Expr> toReturn; // Array is concrete if (!isSymbolic) { - std::map<unsigned, ref<Expr> > optimized; + std::map<unsigned, ref<Expr>> optimized; for (auto &read : reads) { auto info = readInfo[read]; auto cached = cacheReadExprOptimized.find(read->hash()); @@ -249,7 +258,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( // OR // array is symbolic && updatelist contains at least one concrete value else { - std::map<unsigned, ref<Expr> > optimized; + std::map<unsigned, ref<Expr>> optimized; for (auto &read : reads) { auto info = readInfo[read]; auto cached = cacheReadExprOptimized.find(read->hash()); @@ -290,7 +299,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( } } - std::vector<std::pair<uint64_t, bool> > arrayValues; + std::vector<std::pair<uint64_t, bool>> arrayValues; unsigned symByteNum = 0; for (unsigned i = 0; i < elementsInArray; i++) { uint64_t val = 0; @@ -316,7 +325,8 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( } } - if (((double)symByteNum / (double)elementsInArray) <= ArrayValueSymbRatio) { + if (((double)symByteNum / (double)elementsInArray) <= + ArrayValueSymbRatio) { // If the optimization can be applied we apply it // Build the dynamic select expression ref<Expr> opt = @@ -337,7 +347,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr( ref<Expr> ExprOptimizer::buildConstantSelectExpr( const ref<Expr> &index, std::vector<uint64_t> &arrayValues, Expr::Width width, unsigned arraySize) const { - std::vector<std::pair<uint64_t, uint64_t> > ranges; + std::vector<std::pair<uint64_t, uint64_t>> ranges; std::vector<uint64_t> values; std::set<uint64_t> unique_array_values; ExprBuilder *builder = createDefaultExprBuilder(); @@ -373,11 +383,12 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr( } } - if (((double)unique_array_values.size() / (double)(arraySize)) >= ArrayValueRatio) { + if (((double)unique_array_values.size() / (double)(arraySize)) >= + ArrayValueRatio) { return result; } - std::map<uint64_t, std::vector<std::pair<uint64_t, uint64_t> > > exprMap; + std::map<uint64_t, std::vector<std::pair<uint64_t, uint64_t>>> exprMap; for (size_t i = 0; i < ranges.size(); i++) { if (exprMap.find(values[i]) != exprMap.end()) { exprMap[values[i]] @@ -385,7 +396,7 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr( } else { if (exprMap.find(values[i]) == exprMap.end()) { exprMap.insert(std::make_pair( - values[i], std::vector<std::pair<uint64_t, uint64_t> >())); + values[i], std::vector<std::pair<uint64_t, uint64_t>>())); } exprMap.find(values[i]) ->second.push_back(std::make_pair(ranges[i].first, ranges[i].second)); @@ -476,11 +487,11 @@ ref<Expr> ExprOptimizer::buildConstantSelectExpr( } ref<Expr> ExprOptimizer::buildMixedSelectExpr( - const ReadExpr *re, std::vector<std::pair<uint64_t, bool> > &arrayValues, + const ReadExpr *re, std::vector<std::pair<uint64_t, bool>> &arrayValues, Expr::Width width, unsigned elementsInArray) const { ExprBuilder *builder = createDefaultExprBuilder(); std::vector<uint64_t> values; - std::vector<std::pair<uint64_t, uint64_t> > ranges; + std::vector<std::pair<uint64_t, uint64_t>> ranges; std::vector<uint64_t> holes; std::set<uint64_t> unique_array_values; @@ -527,7 +538,8 @@ ref<Expr> ExprOptimizer::buildMixedSelectExpr( assert(ranges.size() > 0 && "No ranges"); ref<Expr> result; - if (((double)unique_array_values.size() / (double)(arraySize)) <= ArrayValueRatio) { + if (((double)unique_array_values.size() / (double)(arraySize)) <= + ArrayValueRatio) { // The final "else" expression will be the original unoptimized array read // expression unsigned range_start = 0; diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp index d4dc9a21..5e5dac0d 100644 --- a/lib/Expr/ArrayExprRewriter.cpp +++ b/lib/Expr/ArrayExprRewriter.cpp @@ -1,3 +1,12 @@ +//===-- ArrayExprRewriter.cpp ---------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "klee/ArrayExprRewriter.h" #include "klee/util/BitArray.h" @@ -6,119 +15,127 @@ using namespace klee; -ref<Expr> ExprRewriter::createOptExpr(const ref<Expr> &e, - const array2idx_ty &arrays, - const mapIndexOptimizedExpr_ty &idx_valIdx) { - return rewrite(e, arrays, idx_valIdx); +ref<Expr> +ExprRewriter::createOptExpr(const ref<Expr> &e, const array2idx_ty &arrays, + const mapIndexOptimizedExpr_ty &idx_valIdx) { + return rewrite(e, arrays, idx_valIdx); } -ref<Expr> -ExprRewriter::rewrite(const ref<Expr> &e, - const array2idx_ty &arrays, - const mapIndexOptimizedExpr_ty &idx_valIdx) { +ref<Expr> ExprRewriter::rewrite(const ref<Expr> &e, const array2idx_ty &arrays, + const mapIndexOptimizedExpr_ty &idx_valIdx) { ref<Expr> notFound; - std::vector<ref<Expr> > eqExprs; + std::vector<ref<Expr>> eqExprs; bool invert = false; for (auto &element : arrays) { - const Array* arr = element.first; - std::vector<ref<Expr> > indexes = element.second; + const Array *arr = element.first; + std::vector<ref<Expr>> indexes = element.second; - IndexTransformationExprVisitor idxt_v(arr); - idxt_v.visit(e); + IndexTransformationExprVisitor idxt_v(arr); + idxt_v.visit(e); - assert((idxt_v.getWidth() % element.first->range == 0) && "Read is not aligned"); + assert((idxt_v.getWidth() % element.first->range == 0) && + "Read is not aligned"); - Expr::Width width = idxt_v.getWidth() / element.first->range; - if (idxt_v.getMul().get()) { - // If we have a MulExpr in the index, we can optimize our search by - // skipping all those indexes that are not multiple of such value. - // In fact, they will be rejected by the MulExpr interpreter since it - // will not find any integer solution - Expr &e = *idxt_v.getMul(); - ConstantExpr &ce = static_cast<ConstantExpr &>(e); - llvm::APInt val = ce.getAPValue(); - uint64_t mulVal = val.getZExtValue(); - // So far we try to limit this optimization, but we may try some more - // aggressive conditions (i.e. mulVal > width) - if (width == 1 && mulVal > 1) - width = mulVal; - } + Expr::Width width = idxt_v.getWidth() / element.first->range; + if (idxt_v.getMul().get()) { + // If we have a MulExpr in the index, we can optimize our search by + // skipping all those indexes that are not multiple of such value. + // In fact, they will be rejected by the MulExpr interpreter since it + // will not find any integer solution + Expr &e = *idxt_v.getMul(); + ConstantExpr &ce = static_cast<ConstantExpr &>(e); + llvm::APInt val = ce.getAPValue(); + uint64_t mulVal = val.getZExtValue(); + // So far we try to limit this optimization, but we may try some more + // aggressive conditions (i.e. mulVal > width) + if (width == 1 && mulVal > 1) + width = mulVal; + } - for (std::vector<ref<Expr> >::const_iterator index_it = indexes.begin(); - index_it != indexes.end(); ++index_it) { - if (idx_valIdx.find((*index_it)) == idx_valIdx.end()) { - continue; - } - auto opt_indexes = idx_valIdx.at((*index_it)); - if (opt_indexes.size() == 0) { - // We continue with other solutions - continue; - } else if (opt_indexes.size() == 1) { - // We treat this case as a special one, and we create an EqExpr (e.g. k==i) - eqExprs.push_back(createEqExpr((*index_it), opt_indexes[0])); - } else { - Expr::Width idxWidth = (*index_it).get()->getWidth(); - unsigned set = 0; - BitArray ba(arr->size/width); - for (auto &vals : opt_indexes) { - ConstantExpr &ce = static_cast<ConstantExpr &>(*vals); - llvm::APInt v = ce.getAPValue(); - ba.set(v.getZExtValue() / width); - set++; - } - if (set > 0 && set < arr->size/width) - invert = ((float)set / (float)(arr->size/width)) > 0.5 ? true : false; - int start = -1; - for (unsigned i = 0; i < arr->size/width; ++i) { - if ((!invert && ba.get(i)) || (invert && !ba.get(i))) { - if (start < 0) - start = i; - } else { - if (start >= 0) { - if (i - start == 1) { - eqExprs.push_back(createEqExpr((*index_it), ConstantExpr::create(start*width, idxWidth))); - } else { - // create range expr - ref<Expr> s = ConstantExpr::create(start*width, idxWidth); - ref<Expr> e = ConstantExpr::create((i-1)*width, idxWidth); - eqExprs.push_back(createRangeExpr((*index_it), s, e)); - } - start = -1; - } - } - } - if (start >= 0) { - if ((arr->size/width) - start == 1) { - eqExprs.push_back(createEqExpr((*index_it), ConstantExpr::create(start*width, idxWidth))); - } else { - // create range expr - ref<Expr> s = ConstantExpr::create(start*width, idxWidth); - ref<Expr> e = ConstantExpr::create(((arr->size/width) - 1)*width, idxWidth); - eqExprs.push_back(createRangeExpr((*index_it), s, e)); - } - } - } - } + for (std::vector<ref<Expr>>::const_iterator index_it = indexes.begin(); + index_it != indexes.end(); ++index_it) { + if (idx_valIdx.find((*index_it)) == idx_valIdx.end()) { + continue; + } + auto opt_indexes = idx_valIdx.at((*index_it)); + if (opt_indexes.size() == 0) { + // We continue with other solutions + continue; + } else if (opt_indexes.size() == 1) { + // We treat this case as a special one, and we create an EqExpr (e.g. + // k==i) + eqExprs.push_back(createEqExpr((*index_it), opt_indexes[0])); + } else { + Expr::Width idxWidth = (*index_it).get()->getWidth(); + unsigned set = 0; + BitArray ba(arr->size / width); + for (auto &vals : opt_indexes) { + ConstantExpr &ce = static_cast<ConstantExpr &>(*vals); + llvm::APInt v = ce.getAPValue(); + ba.set(v.getZExtValue() / width); + set++; + } + if (set > 0 && set < arr->size / width) + invert = + ((float)set / (float)(arr->size / width)) > 0.5 ? true : false; + int start = -1; + for (unsigned i = 0; i < arr->size / width; ++i) { + if ((!invert && ba.get(i)) || (invert && !ba.get(i))) { + if (start < 0) + start = i; + } else { + if (start >= 0) { + if (i - start == 1) { + eqExprs.push_back(createEqExpr( + (*index_it), + ConstantExpr::create(start * width, idxWidth))); + } else { + // create range expr + ref<Expr> s = ConstantExpr::create(start * width, idxWidth); + ref<Expr> e = ConstantExpr::create((i - 1) * width, idxWidth); + eqExprs.push_back(createRangeExpr((*index_it), s, e)); + } + start = -1; + } + } + } + if (start >= 0) { + if ((arr->size / width) - start == 1) { + eqExprs.push_back(createEqExpr( + (*index_it), ConstantExpr::create(start * width, idxWidth))); + } else { + // create range expr + ref<Expr> s = ConstantExpr::create(start * width, idxWidth); + ref<Expr> e = ConstantExpr::create( + ((arr->size / width) - 1) * width, idxWidth); + eqExprs.push_back(createRangeExpr((*index_it), s, e)); + } + } + } + } } if (eqExprs.size() == 0) { - return notFound; + return notFound; } else if (eqExprs.size() == 1) { - if (isa<AndExpr>(eqExprs[0])) { - return EqExpr::alloc(ConstantExpr::alloc(invert ? 0 : 1, (eqExprs[0])->getWidth()), - eqExprs[0]); - } - return invert ? NotExpr::alloc(eqExprs[0]) : eqExprs[0]; + if (isa<AndExpr>(eqExprs[0])) { + return EqExpr::alloc( + ConstantExpr::alloc(invert ? 0 : 1, (eqExprs[0])->getWidth()), + eqExprs[0]); + } + return invert ? NotExpr::alloc(eqExprs[0]) : eqExprs[0]; } else { - // We have found at least 2 indexes, we combine them using an OrExpr (e.g. k==i|k==j) - ref<Expr> orExpr = concatenateOrExpr(eqExprs.begin(), eqExprs.end()); - // Create Eq expression for true branch - return EqExpr::alloc(ConstantExpr::alloc(invert ? 0 : 1, (orExpr)->getWidth()), orExpr); + // We have found at least 2 indexes, we combine them using an OrExpr (e.g. + // k==i|k==j) + ref<Expr> orExpr = concatenateOrExpr(eqExprs.begin(), eqExprs.end()); + // Create Eq expression for true branch + return EqExpr::alloc( + ConstantExpr::alloc(invert ? 0 : 1, (orExpr)->getWidth()), orExpr); } } ref<Expr> ExprRewriter::concatenateOrExpr( - const std::vector<ref<Expr> >::const_iterator begin, - const std::vector<ref<Expr> >::const_iterator end) { + const std::vector<ref<Expr>>::const_iterator begin, + const std::vector<ref<Expr>>::const_iterator end) { if (begin + 2 == end) { return OrExpr::alloc(ZExtExpr::alloc((*begin), Expr::Int32), ZExtExpr::alloc((*(begin + 1)), Expr::Int32)); diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index fa92b66c..dae4c451 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -1,3 +1,12 @@ +//===-- ArrayExprVisitor.cpp ----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "klee/util/ArrayExprVisitor.h" #include "klee/Internal/Support/ErrorHandling.h" @@ -258,6 +267,7 @@ ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) { } return Action::doChildren(); } + ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &re) { mul = false; return Action::doChildren(); diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp index 755263f0..4a1d68d8 100644 --- a/lib/Expr/AssignmentGenerator.cpp +++ b/lib/Expr/AssignmentGenerator.cpp @@ -1,3 +1,12 @@ +//===-- AssignmentGenerator.cpp -------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + #include "klee/AssignmentGenerator.h" #include "llvm/Support/raw_ostream.h" @@ -32,7 +41,8 @@ bool AssignmentGenerator::helperGenerateAssignment(const ref<Expr> &e, } else { return false; } - if (!ExtractExpr::create(kid_val, kid_val.get()->getWidth() - 1, 1).get()->isZero()) { + if (!ExtractExpr::create(kid_val, kid_val.get()->getWidth() - 1, + 1).get()->isZero()) { // FIXME: really bad hack to support those cases in which KLEE creates // Add expressions with negative values val = createAddExpr(kid_val, val); |