diff options
-rw-r--r-- | include/klee/ArrayExprOptimizer.h | 23 | ||||
-rw-r--r-- | include/klee/Expr.h | 2 | ||||
-rw-r--r-- | include/klee/util/ArrayExprVisitor.h | 53 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 113 | ||||
-rw-r--r-- | lib/Expr/ArrayExprOptimizer.cpp | 456 | ||||
-rw-r--r-- | lib/Expr/ArrayExprVisitor.cpp | 93 | ||||
-rw-r--r-- | lib/Expr/Expr.cpp | 41 | ||||
-rw-r--r-- | test/ArrayOpt/test-mix.c | 56 | ||||
-rw-r--r-- | test/ArrayOpt/test_array_index_array.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_array_index_array_diffsize.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_cache.c | 31 | ||||
-rw-r--r-- | test/ArrayOpt/test_const_arr-idx.c | 7 | ||||
-rw-r--r-- | test/ArrayOpt/test_expr_complex.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_expr_simple.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_feasible.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_multindex.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_new.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_nier.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_noncontiguous_idx.c | 16 | ||||
-rw-r--r-- | test/ArrayOpt/test_position.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_sub_idx.c | 15 | ||||
-rw-r--r-- | test/ArrayOpt/test_var_idx.c | 15 |
22 files changed, 1043 insertions, 13 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h index c5eac212..982136fb 100644 --- a/include/klee/ArrayExprOptimizer.h +++ b/include/klee/ArrayExprOptimizer.h @@ -39,11 +39,17 @@ namespace klee { enum ArrayOptimizationType { NONE, - INDEX + ALL, + INDEX, + VALUE }; extern llvm::cl::opt<ArrayOptimizationType> OptimizeArray; +extern llvm::cl::opt<double> ArrayValueRatio; + +extern llvm::cl::opt<double> ArrayValueSymbRatio; + class Expr; template <class T> class ref; typedef std::map<const Array *, std::vector<ref<Expr> > > array2idx_ty; @@ -54,6 +60,7 @@ class ExprOptimizer { private: unordered_map<unsigned, ref<Expr> > cacheExprOptimized; unordered_set<unsigned> cacheExprUnapplicable; + unordered_map<unsigned, ref<Expr> > cacheReadExprOptimized; public: void optimizeExpr(const ref<Expr> &e, ref<Expr> &result, @@ -64,6 +71,20 @@ private: 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, + bool isSymbolic); + + ref<Expr> buildConstantSelectExpr(const ref<Expr> &index, + 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; + }; } diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 212053b4..8eccdf11 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -579,6 +579,8 @@ public: } static ref<Expr> create(const UpdateList &updates, ref<Expr> i); + static ref<Expr> extendRead(const UpdateList &updates, ref<Expr> i, + Expr::Width w); Width getWidth() const { assert(updates.root); return updates.root->getRange(); } Kind getKind() const { return Read; } diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h index 42eead84..70495989 100644 --- a/include/klee/util/ArrayExprVisitor.h +++ b/include/klee/util/ArrayExprVisitor.h @@ -86,6 +86,59 @@ public: } inline ref<Expr> getMul() { return mul; } }; + +//------------------------- VALUE-BASED OPTIMIZATION-------------------------// +class ArrayReadExprVisitor : public ExprVisitor { +private: + std::vector<const ReadExpr *> &reads; + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > &readInfo; + bool symbolic; + bool incompatible; + + Action inspectRead(unsigned hash, Expr::Width width, const ReadExpr &); + +protected: + Action visitConcat(const ConcatExpr &); + Action visitRead(const ReadExpr &); + +public: + ArrayReadExprVisitor( + std::vector<const ReadExpr *> &_reads, + 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; } + inline bool containsSymbolic() { return symbolic; } +}; + +class ArrayValueOptReplaceVisitor : public ExprVisitor { +private: + unordered_set<unsigned> visited; + std::map<unsigned, ref<Expr> > optimized; + +protected: + Action visitConcat(const ConcatExpr &); + Action visitRead(const ReadExpr &re); + +public: + ArrayValueOptReplaceVisitor(std::map<unsigned, ref<Expr> > &_optimized, + bool recursive = true) + : ExprVisitor(recursive), optimized(_optimized) {} +}; + +class IndexCleanerVisitor : public ExprVisitor { +private: + bool mul; + ref<Expr> index; + +protected: + Action visitMul(const MulExpr &); + Action visitRead(const ReadExpr &); + +public: + IndexCleanerVisitor() : ExprVisitor(true), mul(true) {} + inline ref<Expr> getIndex() { return index; } +}; } #endif diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 613c51ae..506fa12f 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1085,11 +1085,19 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, if (!isa<ConstantExpr>(e)) { ref<ConstantExpr> value; bool isTrue = false; - + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(e)) { + ref<Expr> res; + optimizer.optimizeExpr(e, res, true); + if (res.get()) { + e = res; + } + } solver->setTimeout(coreSolverTimeout); if (solver->getValue(state, e, value)) { ref<Expr> cond = EqExpr::create(e, value); - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa<ConstantExpr>(cond)) { ref<Expr> res; optimizer.optimizeExpr(cond, res); @@ -1146,6 +1154,14 @@ void Executor::executeGetValue(ExecutionState &state, seedMap.find(&state); if (it==seedMap.end() || isa<ConstantExpr>(e)) { ref<ConstantExpr> value; + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(e)) { + ref<Expr> result; + optimizer.optimizeExpr(e, result, true); + if (result.get()) { + e = result; + } + } bool success = solver->getValue(state, e, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; @@ -1154,9 +1170,17 @@ void Executor::executeGetValue(ExecutionState &state, std::set< ref<Expr> > values; for (std::vector<SeedInfo>::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { + ref<Expr> cond = siit->assignment.evaluate(e); + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(cond)) { + ref<Expr> result; + optimizer.optimizeExpr(cond, result, true); + if (result.get()) { + cond = result; + } + } ref<ConstantExpr> value; - bool success = - solver->getValue(state, siit->assignment.evaluate(e), value); + bool success = solver->getValue(state, cond, value); assert(success && "FIXME: Unhandled solver failure"); (void) success; values.insert(value); @@ -1584,7 +1608,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { "Wrong operand index!"); ref<Expr> cond = eval(ki, 0, state).value; - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa<ConstantExpr>(cond)) { ref<Expr> result; optimizer.optimizeExpr(cond, result); @@ -1736,7 +1761,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Check if control flow could take this case bool result; - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa<ConstantExpr>(match)) { ref<Expr> result; optimizer.optimizeExpr(match, result); @@ -1770,7 +1796,8 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } // Check if control could take the default case - if (OptimizeArray == INDEX && + if ((OptimizeArray == ALL || OptimizeArray == VALUE || + OptimizeArray == INDEX) && !isa<ConstantExpr>(defaultValue)) { ref<Expr> result; optimizer.optimizeExpr(defaultValue, result); @@ -1893,6 +1920,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { have already got a value. But in the end the caches should handle it for us, albeit with some overhead. */ do { + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(v)) { + ref<Expr> result; + optimizer.optimizeExpr(v, result, true); + if (result.get()) { + v = result; + } + } ref<ConstantExpr> value; bool success = solver->getValue(*free, v, value); assert(success && "FIXME: Unhandled solver failure"); @@ -3126,6 +3161,14 @@ void Executor::callExternalFunction(ExecutionState &state, for (std::vector<ref<Expr> >::iterator ai = arguments.begin(), ae = arguments.end(); ai!=ae; ++ai) { if (AllowExternalSymCalls) { // don't bother checking uniqueness + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(*ai)) { + ref<Expr> result; + optimizer.optimizeExpr(*ai, result, true); + if (result.get()) { + *ai = result; + } + } ref<ConstantExpr> ce; bool success = solver->getValue(state, *ai, ce); assert(success && "FIXME: Unhandled solver failure"); @@ -3312,6 +3355,15 @@ void Executor::executeAlloc(ExecutionState &state, // return argument first). This shows up in pcre when llvm // collapses the size expression with a select. + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(size)) { + ref<Expr> result; + optimizer.optimizeExpr(size, result, true); + if (result.get()) { + size = result; + } + } + ref<ConstantExpr> example; bool success = solver->getValue(state, size, example); assert(success && "FIXME: Unhandled solver failure"); @@ -3382,6 +3434,14 @@ void Executor::executeAlloc(ExecutionState &state, void Executor::executeFree(ExecutionState &state, ref<Expr> address, KInstruction *target) { + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(address)) { + ref<Expr> result; + optimizer.optimizeExpr(address, result, true); + if (result.get()) { + address = result; + } + } StatePair zeroPointer = fork(state, Expr::createIsZero(address), true); if (zeroPointer.first) { if (target) @@ -3413,6 +3473,14 @@ void Executor::resolveExact(ExecutionState &state, ref<Expr> p, ExactResolutionList &results, const std::string &name) { + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(p)) { + ref<Expr> result; + optimizer.optimizeExpr(p, result, true); + if (result.get()) { + p = result; + } + } // XXX we may want to be capping this? ResolutionList rl; state.addressSpace.resolve(state, solver, p, rl); @@ -3454,6 +3522,14 @@ void Executor::executeMemoryOperation(ExecutionState &state, value = state.constraints.simplifyExpr(value); } + if ((OptimizeArray == VALUE) && !isa<ConstantExpr>(address)) { + ref<Expr> result; + optimizer.optimizeExpr(address, result, true); + if (result.get()) { + address = result; + } + } + // fast path: single in-bounds resolution ObjectPair op; bool success; @@ -3472,12 +3548,19 @@ void Executor::executeMemoryOperation(ExecutionState &state, } ref<Expr> offset = mo->getOffsetExpr(address); + ref<Expr> check = mo->getBoundsCheckOffset(offset, bytes); + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(check)) { + ref<Expr> result; + optimizer.optimizeExpr(check, result, true); + if (result.get()) { + check = result; + } + } bool inBounds; solver->setTimeout(coreSolverTimeout); - bool success = solver->mustBeTrue(state, - mo->getBoundsCheckOffset(offset, bytes), - inBounds); + bool success = solver->mustBeTrue(state, check, inBounds); solver->setTimeout(0); if (!success) { state.pc = state.prevPC; @@ -3510,7 +3593,15 @@ void Executor::executeMemoryOperation(ExecutionState &state, // we are on an error path (no resolution, multiple resolution, one // resolution with out of bounds) - + + if ((OptimizeArray == ALL || OptimizeArray == VALUE) && + !isa<ConstantExpr>(address)) { + ref<Expr> result; + optimizer.optimizeExpr(address, result, true); + if (result.get()) { + address = result; + } + } ResolutionList rl; solver->setTimeout(coreSolverTimeout); bool incomplete = state.addressSpace.resolve(state, solver, address, rl, diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index d3e8cbab..86c19a81 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -11,11 +11,26 @@ namespace klee { llvm::cl::opt<ArrayOptimizationType> OptimizeArray( "optimize-array", llvm::cl::values( + clEnumValN(ALL, "all", "Combining index and value transformations"), clEnumValN(INDEX, "index", "Index-based transformation"), + clEnumValN(VALUE, "value", "Value-based transformation at branch (both " + "concrete and concrete/symbolic)"), clEnumValEnd), llvm::cl::init(NONE), llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " "arrays. (default=off)")); + +llvm::cl::opt<double> ArrayValueRatio( + "array-value-ratio", + llvm::cl::desc("Maximum ratio of unique values to array size for which the " + "value-based transformations are applied."), + llvm::cl::init(1.0), llvm::cl::value_desc("Unique Values / Array Size")); + +llvm::cl::opt<double> ArrayValueSymbRatio( + "array-value-symb-ratio", + llvm::cl::desc("Maximum ratio of symbolic values to array size for which " + "the mixed value-based transformations are applied."), + llvm::cl::init(1.0), llvm::cl::value_desc("Symbolic Values / Array Size")); }; void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, @@ -33,7 +48,7 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, } // ----------------------- INDEX-BASED OPTIMIZATION ------------------------- - if (!valueOnly && OptimizeArray == INDEX) { + if (!valueOnly && (OptimizeArray == ALL || OptimizeArray == INDEX)) { array2idx_ty arrays; ConstantArrayExprVisitor aev(arrays); aev.visit(e); @@ -72,6 +87,31 @@ void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, } } } + // ----------------------- VALUE-BASED OPTIMIZATION ------------------------- + if (OptimizeArray == VALUE || + (OptimizeArray == ALL && (!result.get() || valueOnly))) { + std::vector<const ReadExpr *> reads; + std::map<const ReadExpr *, std::pair<unsigned, Expr::Width> > readInfo; + ArrayReadExprVisitor are(reads, readInfo); + are.visit(e); + std::reverse(reads.begin(), reads.end()); + + if (reads.size() == 0 || are.isIncompatible()) { + cacheExprUnapplicable.insert(hash); + return; + } + + ref<Expr> selectOpt = + getSelectOptExpr(e, reads, readInfo, are.containsSymbolic()); + if (selectOpt.get()) { + klee_warning("OPT_V: successful"); + result = selectOpt; + cacheExprOptimized[hash] = result; + } else { + klee_warning("OPT_V: unsuccessful"); + cacheExprUnapplicable.insert(hash); + } + } } bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, @@ -133,3 +173,417 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, } return success; } + +ref<Expr> ExprOptimizer::getSelectOptExpr( + const ref<Expr> &e, std::vector<const ReadExpr *> &reads, + 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; + for (auto &read : reads) { + auto info = readInfo[read]; + auto cached = cacheReadExprOptimized.find(read->hash()); + if (cached != cacheReadExprOptimized.end()) { + optimized.insert(std::make_pair(info.first, (*cached).second)); + continue; + } + Expr::Width width = read->getWidth(); + if (info.second > width) { + width = info.second; + } + unsigned size = read->updates.root->getSize(); + unsigned bytesPerElement = width / 8; + unsigned elementsInArray = size / bytesPerElement; + + // Note: we already filtered the ReadExpr, so here we can safely + // assume that the UpdateNodes contain ConstantExpr indexes and values + assert(read->updates.root->isConstantArray() && + "Expected concrete array, found symbolic array"); + auto arrayConstValues = read->updates.root->constantValues; + for (const UpdateNode *un = read->updates.head; un; un = un->next) { + ConstantExpr *ce = static_cast<ConstantExpr *>(un->index.get()); + uint64_t index = ce->getAPValue().getZExtValue(); + assert(index < arrayConstValues.size()); + ConstantExpr *arrayValue = static_cast<ConstantExpr *>(un->value.get()); + arrayConstValues[index] = arrayValue; + } + std::vector<uint64_t> arrayValues; + // Get the concrete values from the array + for (unsigned i = 0; i < elementsInArray; i++) { + uint64_t val = 0; + for (unsigned j = 0; j < bytesPerElement; j++) { + val |= (*( + arrayConstValues[(i * bytesPerElement) + j] + .get() + ->getAPValue() + .getRawData()) + << (j * 8)); + } + arrayValues.push_back(val); + } + + ref<Expr> index = read->index; + IndexCleanerVisitor ice; + ice.visit(index); + if (ice.getIndex().get()) { + index = ice.getIndex(); + } + + ref<Expr> opt = + buildConstantSelectExpr(index, arrayValues, width, elementsInArray); + if (opt.get()) { + cacheReadExprOptimized[read->hash()] = opt; + optimized.insert(std::make_pair(info.first, opt)); + } + } + ArrayValueOptReplaceVisitor replacer(optimized); + toReturn = replacer.visit(e); + } + + // Array is mixed concrete/symbolic + // \pre: array is concrete && updatelist contains at least one symbolic value + // OR + // array is symbolic && updatelist contains at least one concrete value + else { + std::map<unsigned, ref<Expr> > optimized; + for (auto &read : reads) { + auto info = readInfo[read]; + auto cached = cacheReadExprOptimized.find(read->hash()); + if (cached != cacheReadExprOptimized.end()) { + optimized.insert(std::make_pair(info.first, (*cached).second)); + continue; + } + Expr::Width width = read->getWidth(); + if (info.second > width) { + width = info.second; + } + unsigned size = read->updates.root->getSize(); + unsigned bytesPerElement = width / 8; + unsigned elementsInArray = size / bytesPerElement; + bool symbArray = read->updates.root->isSymbolicArray(); + + BitArray ba(size, symbArray); + // Note: we already filtered the ReadExpr, so here we can safely + // assume that the UpdateNodes contain ConstantExpr indexes, but in + // this case we *cannot* assume anything on the values + auto arrayConstValues = read->updates.root->constantValues; + if (arrayConstValues.size() < size) { + // We need to "force" initialization of the values + for (size_t i = arrayConstValues.size(); i < size; i++) { + arrayConstValues.push_back(ConstantExpr::create(0, Expr::Int8)); + } + } + for (const UpdateNode *un = read->updates.head; un; un = un->next) { + ConstantExpr *ce = static_cast<ConstantExpr *>(un->index.get()); + uint64_t index = ce->getAPValue().getLimitedValue(); + if (!isa<ConstantExpr>(un->value)) { + ba.set(index); + } else { + ba.unset(index); + ConstantExpr *arrayValue = + static_cast<ConstantExpr *>(un->value.get()); + arrayConstValues[index] = arrayValue; + } + } + + std::vector<std::pair<uint64_t, bool> > arrayValues; + unsigned symByteNum = 0; + for (unsigned i = 0; i < elementsInArray; i++) { + uint64_t val = 0; + bool elementIsConcrete = true; + for (unsigned j = 0; j < bytesPerElement; j++) { + if (ba.get((i * bytesPerElement) + j)) { + elementIsConcrete = false; + break; + } else { + val |= (*( + arrayConstValues[(i * bytesPerElement) + j] + .get() + ->getAPValue() + .getRawData()) + << (j * 8)); + } + } + if (elementIsConcrete) { + arrayValues.push_back(std::make_pair(val, true)); + } else { + symByteNum++; + arrayValues.push_back(std::make_pair(0, false)); + } + } + + if (((double)symByteNum / (double)elementsInArray) <= ArrayValueSymbRatio) { + // If the optimization can be applied we apply it + // Build the dynamic select expression + ref<Expr> opt = + buildMixedSelectExpr(read, arrayValues, width, elementsInArray); + if (opt.get()) { + cacheReadExprOptimized[read->hash()] = opt; + optimized.insert(std::make_pair(info.first, opt)); + } + } + } + ArrayValueOptReplaceVisitor replacer(optimized, false); + toReturn = replacer.visit(e); + } + + return toReturn.get() ? toReturn : notFound; +} + +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<uint64_t> values; + std::set<uint64_t> unique_array_values; + ExprBuilder *builder = createDefaultExprBuilder(); + Expr::Width valWidth = width; + ref<Expr> result; + + ref<Expr> actualIndex; + if (index->getWidth() > Expr::Int32) { + actualIndex = ExtractExpr::alloc(index, 0, Expr::Int32); + } else { + actualIndex = index; + } + Expr::Width idxWidth = actualIndex->getWidth(); + + // Calculate the repeating values ranges in the constant array + unsigned curr_idx = 0; + uint64_t curr_val = arrayValues[0]; + for (unsigned i = 0; i < arraySize; i++) { + uint64_t temp = arrayValues[i]; + unique_array_values.insert(curr_val); + if (temp != curr_val) { + ranges.push_back(std::make_pair(curr_idx, i)); + values.push_back(curr_val); + curr_val = temp; + curr_idx = i; + if (i == (arraySize - 1)) { + ranges.push_back(std::make_pair(curr_idx, i + 1)); + values.push_back(curr_val); + } + } else if (i == (arraySize - 1)) { + ranges.push_back(std::make_pair(curr_idx, i + 1)); + values.push_back(curr_val); + } + } + + if (((double)unique_array_values.size() / (double)(arraySize)) >= ArrayValueRatio) { + return result; + } + + 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]] + .push_back(std::make_pair(ranges[i].first, ranges[i].second)); + } else { + if (exprMap.find(values[i]) == exprMap.end()) { + exprMap.insert(std::make_pair( + 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)); + } + } + + int ct = 0; + // For each range appropriately build the Select expression. + for (auto range : exprMap) { + ref<Expr> temp; + if (ct == 0) { + temp = builder->Constant(llvm::APInt(valWidth, range.first, false)); + } else { + if (range.second.size() == 1) { + if (range.second[0].first == (range.second[0].second - 1)) { + temp = SelectExpr::create( + EqExpr::create(actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[0].first, false))), + builder->Constant(llvm::APInt(valWidth, range.first, false)), + result); + + } else { + temp = SelectExpr::create( + AndExpr::create( + SgeExpr::create(actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[0].first, false))), + SltExpr::create( + actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[0].second, false)))), + builder->Constant(llvm::APInt(valWidth, range.first, false)), + result); + } + + } else { + ref<Expr> currOr; + if (range.second[0].first == (range.second[0].second - 1)) { + currOr = EqExpr::create(actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[0].first, false))); + } else { + currOr = AndExpr::create( + SgeExpr::create(actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[0].first, false))), + SltExpr::create(actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[0].second, false)))); + } + for (size_t i = 1; i < range.second.size(); i++) { + ref<Expr> tempOr; + if (range.second[i].first == (range.second[i].second - 1)) { + tempOr = OrExpr::create( + EqExpr::create(actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[i].first, false))), + currOr); + + } else { + tempOr = OrExpr::create( + AndExpr::create( + SgeExpr::create( + actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[i].first, false))), + SltExpr::create( + actualIndex, + builder->Constant(llvm::APInt( + idxWidth, range.second[i].second, false)))), + currOr); + } + currOr = tempOr; + } + temp = SelectExpr::create(currOr, builder->Constant(llvm::APInt( + valWidth, range.first, false)), + result); + } + } + result = temp; + ct++; + } + + delete (builder); + + return result; +} + +ref<Expr> ExprOptimizer::buildMixedSelectExpr( + 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<uint64_t> holes; + std::set<uint64_t> unique_array_values; + + unsigned arraySize = elementsInArray; + unsigned curr_idx = 0; + uint64_t curr_val = arrayValues[0].first; + + bool emptyRange = true; + // Calculate Range values + for (size_t i = 0; i < arrayValues.size(); i++) { + // If the value is concrete + if (arrayValues[i].second) { + // The range contains a concrete value + emptyRange = false; + uint64_t temp = arrayValues[i].first; + unique_array_values.insert(temp); + if (temp != curr_val) { + ranges.push_back(std::make_pair(curr_idx, i)); + values.push_back(curr_val); + curr_val = temp; + curr_idx = i; + if (i == (arraySize - 1)) { + ranges.push_back(std::make_pair(curr_idx, curr_idx + 1)); + values.push_back(curr_val); + } + } else if (i == (arraySize - 1)) { + ranges.push_back(std::make_pair(curr_idx, i + 1)); + values.push_back(curr_val); + } + } else { + holes.push_back(i); + // If this is not an empty range + if (!emptyRange) { + ranges.push_back(std::make_pair(curr_idx, i)); + values.push_back(curr_val); + } + curr_val = arrayValues[i + 1].first; + curr_idx = i + 1; + emptyRange = true; + } + } + + assert(unique_array_values.size() > 0 && "No unique values"); + assert(ranges.size() > 0 && "No ranges"); + + ref<Expr> result; + 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; + if (holes.size() == 0) { + result = builder->Constant(llvm::APInt(width, values[0], false)); + range_start = 1; + } else { + ref<Expr> firstIndex = MulExpr::create( + ConstantExpr::create(holes[0], re->index->getWidth()), + ConstantExpr::create(width / 8, re->index->getWidth())); + result = ReadExpr::extendRead(re->updates, firstIndex, width); + for (size_t i = 1; i < holes.size(); i++) { + ref<Expr> temp_idx = MulExpr::create( + ConstantExpr::create(holes[i], re->index->getWidth()), + ConstantExpr::create(width / 8, re->index->getWidth())); + ref<Expr> cond = EqExpr::create( + re->index, ConstantExpr::create(holes[i], re->index->getWidth())); + ref<Expr> temp = SelectExpr::create( + cond, ReadExpr::extendRead(re->updates, temp_idx, width), result); + result = temp; + } + } + + ref<Expr> new_index = re->index; + IndexCleanerVisitor ice; + ice.visit(new_index); + if (ice.getIndex().get()) { + new_index = ice.getIndex(); + } + + int new_index_width = new_index->getWidth(); + // Iterate through all the ranges + for (size_t i = range_start; i < ranges.size(); i++) { + ref<Expr> temp; + if (ranges[i].second - 1 == ranges[i].first) { + ref<Expr> cond = EqExpr::create( + new_index, ConstantExpr::create(ranges[i].first, new_index_width)); + ref<Expr> t = ConstantExpr::create(values[i], width); + ref<Expr> f = result; + temp = SelectExpr::create(cond, t, f); + } else { + // Create the select constraint + ref<Expr> cond = AndExpr::create( + SgeExpr::create(new_index, ConstantExpr::create(ranges[i].first, + new_index_width)), + SltExpr::create(new_index, ConstantExpr::create(ranges[i].second, + new_index_width))); + ref<Expr> t = ConstantExpr::create(values[i], width); + ref<Expr> f = result; + temp = SelectExpr::create(cond, t, f); + } + result = temp; + } + } + + delete (builder); + + return result; +} diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index 26ddbb95..fa92b66c 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -169,3 +169,96 @@ ExprVisitor::Action IndexTransformationExprVisitor::visitMul(const MulExpr &e) { mul = e.getKid(1); return Action::doChildren(); } + +//-------------------------- VALUE-BASED OPTIMIZATION------------------------// +ExprVisitor::Action ArrayReadExprVisitor::visitConcat(const ConcatExpr &ce) { + ReadExpr *base = ArrayExprHelper::hasOrderedReads(ce); + if (base) { + return inspectRead(ce.hash(), ce.getWidth(), *base); + } + return Action::doChildren(); +} +ExprVisitor::Action ArrayReadExprVisitor::visitRead(const ReadExpr &re) { + return inspectRead(re.hash(), re.getWidth(), re); +} +// This method is a mess because I want to avoid looping over the UpdateList +// values twice +ExprVisitor::Action ArrayReadExprVisitor::inspectRead(unsigned hash, + Expr::Width width, + const ReadExpr &re) { + // pre(*): index is symbolic + if (!isa<ConstantExpr>(re.index)) { + if (readInfo.find(&re) == readInfo.end()) { + if (re.updates.root->isSymbolicArray() && !re.updates.head) { + return Action::doChildren(); + } + if (re.updates.head) { + // Check preconditions on UpdateList nodes + bool hasConcreteValues = false; + for (const UpdateNode *un = re.updates.head; un; un = un->next) { + // Symbolic case - \inv(update): index is concrete + if (!isa<ConstantExpr>(un->index)) { + incompatible = true; + break; + } else if (!isa<ConstantExpr>(un->value)) { + // We tell the optimization that there is a symbolic value, + // otherwise we rely on the concrete optimization procedure + symbolic = true; + } else if (re.updates.root->isSymbolicArray() && + isa<ConstantExpr>(un->value)) { + // We can optimize symbolic array, but only if they have + // at least one concrete value + hasConcreteValues = true; + } + } + // Symbolic case - if array is symbolic, then we need at least one + // concrete value + if (re.updates.root->isSymbolicArray()) { + if (hasConcreteValues) + symbolic = true; + else + incompatible = true; + } + + if (incompatible) + return Action::skipChildren(); + } + symbolic |= re.updates.root->isSymbolicArray(); + reads.push_back(&re); + readInfo.emplace(&re, std::make_pair(hash, width)); + } + return Action::skipChildren(); + } + return Action::doChildren(); +} + +ExprVisitor::Action +ArrayValueOptReplaceVisitor::visitConcat(const ConcatExpr &ce) { + auto found = optimized.find(ce.hash()); + if (found != optimized.end()) { + return Action::changeTo((*found).second.get()); + } + return Action::doChildren(); +} +ExprVisitor::Action ArrayValueOptReplaceVisitor::visitRead(const ReadExpr &re) { + auto found = optimized.find(re.hash()); + if (found != optimized.end()) { + return Action::changeTo((*found).second.get()); + } + return Action::doChildren(); +} + +ExprVisitor::Action IndexCleanerVisitor::visitMul(const MulExpr &e) { + if (mul) { + if (!isa<ConstantExpr>(e.getKid(0))) + index = e.getKid(0); + else if (!isa<ConstantExpr>(e.getKid(1))) + index = e.getKid(1); + mul = false; + } + return Action::doChildren(); +} +ExprVisitor::Action IndexCleanerVisitor::visitRead(const ReadExpr &re) { + mul = false; + return Action::doChildren(); +} diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index a5c7f652..9e524f62 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -81,6 +81,47 @@ ref<Expr> Expr::createTempRead(const Array *array, Expr::Width w) { } } +ref<Expr> ReadExpr::extendRead(const UpdateList &ul, const ref<Expr> index, + Expr::Width w) { + switch (w) { + default: + assert(0 && "invalid width"); + case Expr::Int8: + return ReadExpr::alloc(ul, index); + case Expr::Int16: + return ConcatExpr::create( + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), + ReadExpr::alloc(ul, index)); + case Expr::Int32: + return ConcatExpr::create4( + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), + ReadExpr::alloc(ul, index)); + case Expr::Int64: + return ConcatExpr::create8( + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(7, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(6, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(5, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(4, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(3, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(2, Expr::Int32), index)), + ReadExpr::alloc( + ul, AddExpr::create(ConstantExpr::create(1, Expr::Int32), index)), + ReadExpr::alloc(ul, index)); + } +} + int Expr::compare(const Expr &b) const { static ExprEquivSet equivs; int r = compare(b, equivs); diff --git a/test/ArrayOpt/test-mix.c b/test/ArrayOpt/test-mix.c index 88cb595c..3b3d7a0f 100644 --- a/test/ArrayOpt/test-mix.c +++ b/test/ArrayOpt/test-mix.c @@ -26,8 +26,64 @@ // RUN: not FileCheck %s -input-file=%t.klee-out/test000010.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000011.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000012.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: test -f %t.klee-out/test000003.kquery +// RUN: test -f %t.klee-out/test000004.kquery +// RUN: test -f %t.klee-out/test000005.kquery +// RUN: test -f %t.klee-out/test000006.kquery +// RUN: test -f %t.klee-out/test000007.kquery +// RUN: test -f %t.klee-out/test000008.kquery +// RUN: test -f %t.klee-out/test000009.kquery +// RUN: test -f %t.klee-out/test000010.kquery +// RUN: test -f %t.klee-out/test000011.kquery +// RUN: test -f %t.klee-out/test000012.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000007.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000008.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000009.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000010.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000011.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000012.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: test -f %t.klee-out/test000003.kquery +// RUN: test -f %t.klee-out/test000004.kquery +// RUN: test -f %t.klee-out/test000005.kquery +// RUN: test -f %t.klee-out/test000006.kquery +// RUN: test -f %t.klee-out/test000007.kquery +// RUN: test -f %t.klee-out/test000008.kquery +// RUN: test -f %t.klee-out/test000009.kquery +// RUN: test -f %t.klee-out/test000010.kquery +// RUN: test -f %t.klee-out/test000011.kquery +// RUN: test -f %t.klee-out/test000012.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000007.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000008.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000009.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000010.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000011.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000012.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_array_index_array.c b/test/ArrayOpt/test_array_index_array.c index 7d5198e1..cf852494 100644 --- a/test/ArrayOpt/test_array_index_array.c +++ b/test/ArrayOpt/test_array_index_array.c @@ -6,8 +6,23 @@ // RUN: test -f %t.klee-out/test000002.kquery // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_array_index_array_diffsize.c b/test/ArrayOpt/test_array_index_array_diffsize.c index e331f909..76ac08b2 100644 --- a/test/ArrayOpt/test_array_index_array_diffsize.c +++ b/test/ArrayOpt/test_array_index_array_diffsize.c @@ -6,8 +6,23 @@ // RUN: test -f %t.klee-out/test000002.kquery // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_cache.c b/test/ArrayOpt/test_cache.c index a2fe10da..2bc64fa4 100644 --- a/test/ArrayOpt/test_cache.c +++ b/test/ArrayOpt/test_cache.c @@ -14,8 +14,39 @@ // RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: test -f %t.klee-out/test000003.kquery +// RUN: test -f %t.klee-out/test000004.kquery +// RUN: test -f %t.klee-out/test000005.kquery +// RUN: test -f %t.klee-out/test000006.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: test -f %t.klee-out/test000003.kquery +// RUN: test -f %t.klee-out/test000004.kquery +// RUN: test -f %t.klee-out/test000005.kquery +// RUN: test -f %t.klee-out/test000006.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000003.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000004.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000005.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000006.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_const_arr-idx.c b/test/ArrayOpt/test_const_arr-idx.c index 25f959a3..9b8a7272 100644 --- a/test/ArrayOpt/test_const_arr-idx.c +++ b/test/ArrayOpt/test_const_arr-idx.c @@ -2,8 +2,15 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=index %t.bc > %t.log 2>&1 // RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_expr_complex.c b/test/ArrayOpt/test_expr_complex.c index 2ae412b5..ea2d8e52 100644 --- a/test/ArrayOpt/test_expr_complex.c +++ b/test/ArrayOpt/test_expr_complex.c @@ -4,8 +4,23 @@ // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I // RUN: test -f %t.klee-out/test000001.kquery // RUN: test -f %t.klee-out/test000002.kquery +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_expr_simple.c b/test/ArrayOpt/test_expr_simple.c index 433b864f..53af9a2b 100644 --- a/test/ArrayOpt/test_expr_simple.c +++ b/test/ArrayOpt/test_expr_simple.c @@ -4,8 +4,23 @@ // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I // RUN: test -f %t.klee-out/test000001.kquery // RUN: test -f %t.klee-out/test000002.kquery +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_feasible.c b/test/ArrayOpt/test_feasible.c index 17bfa523..1bbb341b 100644 --- a/test/ArrayOpt/test_feasible.c +++ b/test/ArrayOpt/test_feasible.c @@ -6,8 +6,23 @@ // RUN: test -f %t.klee-out/test000002.kquery // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_multindex.c b/test/ArrayOpt/test_multindex.c index 4dada79d..91519466 100644 --- a/test/ArrayOpt/test_multindex.c +++ b/test/ArrayOpt/test_multindex.c @@ -2,8 +2,23 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=index %t.bc > %t.log 2>&1 // RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_new.c b/test/ArrayOpt/test_new.c index 7e095e76..8a66d1f6 100644 --- a/test/ArrayOpt/test_new.c +++ b/test/ArrayOpt/test_new.c @@ -4,8 +4,23 @@ // RUN: not FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I // RUN: test -f %t.klee-out/test000001.kquery // RUN: test -f %t.klee-out/test000002.kquery +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_nier.c b/test/ArrayOpt/test_nier.c index 93fb96aa..40e36a3d 100644 --- a/test/ArrayOpt/test_nier.c +++ b/test/ArrayOpt/test_nier.c @@ -6,8 +6,23 @@ // RUN: test -f %t.klee-out/test000002.kquery // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include<stdio.h> diff --git a/test/ArrayOpt/test_noncontiguous_idx.c b/test/ArrayOpt/test_noncontiguous_idx.c index 8eb16021..380c3aea 100644 --- a/test/ArrayOpt/test_noncontiguous_idx.c +++ b/test/ArrayOpt/test_noncontiguous_idx.c @@ -4,10 +4,26 @@ // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I // RUN: test -f %t.klee-out/test000001.kquery // RUN: test -f %t.klee-out/test000002.kquery +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr + #include <stdio.h> #include "klee/klee.h" diff --git a/test/ArrayOpt/test_position.c b/test/ArrayOpt/test_position.c index e42371b6..fcf5aeaa 100644 --- a/test/ArrayOpt/test_position.c +++ b/test/ArrayOpt/test_position.c @@ -4,8 +4,23 @@ // RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I // RUN: test -f %t.klee-out/test000001.kquery // RUN: test -f %t.klee-out/test000002.kquery +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_sub_idx.c b/test/ArrayOpt/test_sub_idx.c index ef068427..34201274 100644 --- a/test/ArrayOpt/test_sub_idx.c +++ b/test/ArrayOpt/test_sub_idx.c @@ -6,8 +6,23 @@ // RUN: test -f %t.klee-out/test000002.kquery // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> diff --git a/test/ArrayOpt/test_var_idx.c b/test/ArrayOpt/test_var_idx.c index 4fbfe7ce..e9f159c1 100644 --- a/test/ArrayOpt/test_var_idx.c +++ b/test/ArrayOpt/test_var_idx.c @@ -6,8 +6,23 @@ // RUN: test -f %t.klee-out/test000002.kquery // RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=value %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_V +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: rm -rf %t.klee-out +// RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc > %t.log 2>&1 +// RUN: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-OPT_V: KLEE: WARNING: OPT_V: successful // CHECK-CONST_ARR: const_arr #include <stdio.h> |