diff options
28 files changed, 1717 insertions, 5 deletions
diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h new file mode 100644 index 00000000..c5eac212 --- /dev/null +++ b/include/klee/ArrayExprOptimizer.h @@ -0,0 +1,70 @@ +#ifndef KLEE_EXPROPTIMIZER_H +#define KLEE_EXPROPTIMIZER_H + +#include <cassert> +#include <iterator> +#include <map> +#include <string> +#include <utility> +#include <vector> + +#include "Expr.h" +#include "ExprBuilder.h" +#include "Constraints.h" +#include "Internal/Support/ErrorHandling.h" +#include "util/ArrayExprVisitor.h" +#include "util/Assignment.h" +#include "util/Ref.h" +#include "klee/AssignmentGenerator.h" +#include "klee/ExecutionState.h" + +#include "llvm/Support/TimeValue.h" +#include "klee/Internal/System/Time.h" + +#include <ciso646> + +#ifdef _LIBCPP_VERSION +#include <unordered_map> +#include <unordered_set> +#define unordered_map std::unordered_map +#define unordered_set std::unordered_set +#else +#include <tr1/unordered_map> +#include <tr1/unordered_set> +#define unordered_map std::tr1::unordered_map +#define unordered_set std::tr1::unordered_set +#endif + +namespace klee { + +enum ArrayOptimizationType { + NONE, + INDEX +}; + +extern llvm::cl::opt<ArrayOptimizationType> OptimizeArray; + +class Expr; +template <class T> class ref; +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; + +class ExprOptimizer { +private: + unordered_map<unsigned, ref<Expr> > cacheExprOptimized; + unordered_set<unsigned> cacheExprUnapplicable; + +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; + +}; +} + +#endif diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h new file mode 100644 index 00000000..dafcfef6 --- /dev/null +++ b/include/klee/ArrayExprRewriter.h @@ -0,0 +1,43 @@ +#ifndef LIB_EXPRREWRITER_H_ +#define LIB_EXPRREWRITER_H_ + +#include "klee/Expr.h" +#include "klee/CommandLine.h" +#include "klee/Constraints.h" +#include "klee/Internal/Support/ErrorHandling.h" +#include "klee/util/ArrayExprVisitor.h" +#include "klee/util/Assignment.h" +#include "klee/util/Ref.h" +#include "klee/AssignmentGenerator.h" + +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; + +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); + +private: + static ref<Expr> + rewrite(const ref<Expr> &e, const array2idx_ty &arrays, + 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); + + static ref<Expr> createEqExpr(const ref<Expr> &index, + const ref<Expr> &valIndex); + + static ref<Expr> createRangeExpr(const ref<Expr> &index, + const ref<Expr> &valStart, + const ref<Expr> &valEnd); +}; +} + +#endif /* LIB_EXPRREWRITER_H_ */ diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h new file mode 100644 index 00000000..835651b8 --- /dev/null +++ b/include/klee/AssignmentGenerator.h @@ -0,0 +1,58 @@ +#ifndef KLEE_ASSIGNMENTGENERATOR_H +#define KLEE_ASSIGNMENTGENERATOR_H + +#include <cassert> +#include <iterator> +#include <map> +#include <string> +#include <utility> +#include <vector> + +#include "Expr.h" +#include "Constraints.h" +#include "Internal/Support/ErrorHandling.h" +#include "util/ArrayExprVisitor.h" +#include "util/Assignment.h" +#include "util/Ref.h" + +#include "llvm/Support/TimeValue.h" +#include "klee/Internal/System/Time.h" + +namespace klee { + +class Expr; +template <class T> class ref; + +class AssignmentGenerator { +public: + static bool generatePartialAssignment(const ref<Expr> &e, ref<Expr> &val, + Assignment *&a); + +private: + static bool helperGenerateAssignment(const ref<Expr> &e, ref<Expr> &val, + Assignment *&a, Expr::Width width, + bool sign); + + static bool isReadExprAtOffset(ref<Expr> e, const ReadExpr *base, + ref<Expr> offset); + static ReadExpr *hasOrderedReads(ref<Expr> e); + + static ref<Expr> createSubExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createAddExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createMulExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createDivExpr(const ref<Expr> &l, ref<Expr> &r, bool sign); + static ref<Expr> createDivRem(const ref<Expr> &l, ref<Expr> &r, bool sign); + static ref<Expr> createShlExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createLShrExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createAndExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createExtractExpr(const ref<Expr> &l, ref<Expr> &r); + static ref<Expr> createExtendExpr(const ref<Expr> &l, ref<Expr> &r); + + static std::vector<unsigned char> getByteValue(ref<Expr> &val); + static std::vector<unsigned char> + getIndexedValue(const std::vector<unsigned char> &c_val, ConstantExpr &index, + const unsigned int size); +}; +} + +#endif diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h new file mode 100644 index 00000000..42eead84 --- /dev/null +++ b/include/klee/util/ArrayExprVisitor.h @@ -0,0 +1,91 @@ +#ifndef KLEE_ARRAYEXPRVISITOR_H_ +#define KLEE_ARRAYEXPRVISITOR_H_ + +#include "klee/util/ExprVisitor.h" +#include "klee/ExprBuilder.h" +#include "klee/CommandLine.h" + +#include <ciso646> +#ifdef _LIBCPP_VERSION +#include <unordered_map> +#include <unordered_set> +#define unordered_map std::unordered_map +#define unordered_set std::unordered_set +#else +#include <tr1/unordered_map> +#include <tr1/unordered_set> +#define unordered_map std::tr1::unordered_map +#define unordered_set std::tr1::unordered_set +#endif + +namespace klee { + +//------------------------------ HELPER FUNCTIONS ---------------------------// +class ArrayExprHelper { +private: + static bool isReadExprAtOffset(ref<Expr> e, const ReadExpr *base, + ref<Expr> offset); + +public: + static ReadExpr *hasOrderedReads(const ConcatExpr &ce); +}; + +//--------------------------- INDEX-BASED OPTIMIZATION-----------------------// +class ConstantArrayExprVisitor : public ExprVisitor { +private: + typedef std::map<const Array *, std::vector<ref<Expr> > > bindings_ty; + bindings_ty &arrays; + // Avoids adding the same index twice + unordered_set<unsigned> addedIndexes; + bool incompatible; + +protected: + Action visitConcat(const ConcatExpr &); + Action visitRead(const ReadExpr &); + +public: + ConstantArrayExprVisitor(bindings_ty &_arrays) + : arrays(_arrays), incompatible(false) {} + inline bool isIncompatible() { return incompatible; } +}; + +class IndexCompatibilityExprVisitor : public ExprVisitor { +private: + bool compatible; + bool inner; + +protected: + Action visitRead(const ReadExpr &); + Action visitURem(const URemExpr &); + Action visitSRem(const SRemExpr &); + Action visitOr(const OrExpr &); + +public: + IndexCompatibilityExprVisitor() : compatible(true), inner(false) {} + + inline bool isCompatible() { return compatible; } + inline bool hasInnerReads() { return inner; } +}; + +class IndexTransformationExprVisitor : public ExprVisitor { +private: + const Array *array; + Expr::Width width; + ref<Expr> mul; + +protected: + Action visitConcat(const ConcatExpr &); + Action visitMul(const MulExpr &); + +public: + IndexTransformationExprVisitor(const Array *_array) + : array(_array), width(Expr::InvalidWidth) {} + + inline Expr::Width getWidth() { + return width == Expr::InvalidWidth ? Expr::Int8 : width; + } + inline ref<Expr> getMul() { return mul; } +}; +} + +#endif diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4b57ccf9..613c51ae 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -24,6 +24,7 @@ #include "ExecutorTimerInfo.h" +#include "klee/ArrayExprOptimizer.h" #include "klee/ExecutionState.h" #include "klee/Expr.h" #include "klee/Interpreter.h" @@ -1085,11 +1086,20 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, ref<ConstantExpr> value; bool isTrue = false; - solver->setTimeout(coreSolverTimeout); - if (solver->getValue(state, e, value) && - solver->mustBeTrue(state, EqExpr::create(e, value), isTrue) && - isTrue) - result = value; + solver->setTimeout(coreSolverTimeout); + if (solver->getValue(state, e, value)) { + ref<Expr> cond = EqExpr::create(e, value); + if (OptimizeArray == INDEX && + !isa<ConstantExpr>(cond)) { + ref<Expr> res; + optimizer.optimizeExpr(cond, res); + if (res.get()) { + cond = res; + } + } + if (solver->mustBeTrue(state, cond, isTrue) && isTrue) + result = value; + } solver->setTimeout(0); } @@ -1573,6 +1583,16 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { assert(bi->getCondition() == bi->getOperand(0) && "Wrong operand index!"); ref<Expr> cond = eval(ki, 0, state).value; + + if (OptimizeArray == INDEX && + !isa<ConstantExpr>(cond)) { + ref<Expr> result; + optimizer.optimizeExpr(cond, result); + if (result.get()) { + cond = result; + } + } + Executor::StatePair branches = fork(state, cond, false); // NOTE: There is a hidden dependency here, markBranchVisited @@ -1716,6 +1736,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { // Check if control flow could take this case bool result; + if (OptimizeArray == INDEX && + !isa<ConstantExpr>(match)) { + ref<Expr> result; + optimizer.optimizeExpr(match, result); + if (result.get()) { + match = result; + } + } bool success = solver->mayBeTrue(state, match, result); assert(success && "FIXME: Unhandled solver failure"); (void) success; @@ -1742,6 +1770,14 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { } // Check if control could take the default case + if (OptimizeArray == INDEX && + !isa<ConstantExpr>(defaultValue)) { + ref<Expr> result; + optimizer.optimizeExpr(defaultValue, result); + if (result.get()) { + defaultValue = result; + } + } bool res; bool success = solver->mayBeTrue(state, defaultValue, res); assert(success && "FIXME: Unhandled solver failure"); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index ec2d49c0..6a640905 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -16,6 +16,7 @@ #define KLEE_EXECUTOR_H #include "klee/ExecutionState.h" +#include "klee/ArrayExprOptimizer.h" #include "klee/Interpreter.h" #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/KInstruction.h" @@ -228,6 +229,9 @@ private: // @brief buffer to store logs before flushing to file llvm::raw_string_ostream debugLogBuffer; + /// Optimizes expressions + ExprOptimizer optimizer; + llvm::Function* getTargetFunction(llvm::Value *calledVal, ExecutionState &state); diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp new file mode 100644 index 00000000..d3e8cbab --- /dev/null +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -0,0 +1,135 @@ +#include "klee/ArrayExprOptimizer.h" + +#include "klee/ArrayExprRewriter.h" +#include "klee/util/BitArray.h" + +#include <iostream> + +using namespace klee; + +namespace klee { +llvm::cl::opt<ArrayOptimizationType> OptimizeArray( + "optimize-array", + llvm::cl::values( + clEnumValN(INDEX, "index", "Index-based transformation"), + clEnumValEnd), + llvm::cl::init(NONE), + llvm::cl::desc("Optimize accesses to either concrete or concrete/symbolic " + "arrays. (default=off)")); +}; + +void ExprOptimizer::optimizeExpr(const ref<Expr> &e, ref<Expr> &result, + bool valueOnly) { + unsigned hash = e->hash(); + if (cacheExprUnapplicable.find(hash) != cacheExprUnapplicable.end()) { + return; + } + + // Find cached expressions + auto cached = cacheExprOptimized.find(hash); + if (cached != cacheExprOptimized.end()) { + result = cached->second; + return; + } + + // ----------------------- INDEX-BASED OPTIMIZATION ------------------------- + if (!valueOnly && OptimizeArray == INDEX) { + array2idx_ty arrays; + ConstantArrayExprVisitor aev(arrays); + aev.visit(e); + + if (arrays.size() == 0 || aev.isIncompatible()) { + // We do not optimize expressions other than those with concrete + // arrays with a symbolic index + // If we cannot optimize the expression, we return a failure only + // when we are not combining the optimizations + if (OptimizeArray == INDEX) { + cacheExprUnapplicable.insert(hash); + return; + } + } else { + mapIndexOptimizedExpr_ty idx_valIdx; + + // Compute those indexes s.t. orig_expr =equisat= (k==i|k==j|..) + if (computeIndexes(arrays, e, idx_valIdx)) { + if (idx_valIdx.size() > 0) { + // Create new expression on indexes + result = ExprRewriter::createOptExpr(e, arrays, idx_valIdx); + } else { + klee_warning("OPT_I: infeasible branch!"); + result = ConstantExpr::create(0, Expr::Bool); + } + // Add new expression to cache + if (result.get()) { + klee_warning("OPT_I: successful"); + cacheExprOptimized[hash] = result; + } else { + klee_warning("OPT_I: unsuccessful"); + } + } else { + klee_warning("OPT_I: unsuccessful"); + cacheExprUnapplicable.insert(hash); + } + } + } +} + +bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref<Expr> &e, + mapIndexOptimizedExpr_ty &idx_valIdx) const { + bool success = false; + // For each constant array found + for (auto &element : arrays) { + const Array *arr = element.first; + + assert(arr->isConstantArray() && "Array is not concrete"); + assert(element.second.size() == 1 && "Multiple indexes on the same array"); + + IndexTransformationExprVisitor idxt_v(arr); + idxt_v.visit(e); + assert((idxt_v.getWidth() % arr->range == 0) && "Read is not aligned"); + Expr::Width width = idxt_v.getWidth() / arr->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); + uint64_t mulVal = (*ce.getAPValue().getRawData()); + // 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 each concrete value 'i' stored in the array + 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; + + // For each symbolic index Expr(k) found + for (auto &index_it : element.second) { + ref<Expr> idx = index_it; + ref<Expr> val = ConstantExpr::alloc(aIdx, arr->getDomain()); + // We create a partial assignment on 'k' s.t. Expr(k)==i + bool assignmentSuccess = + AssignmentGenerator::generatePartialAssignment(idx, val, a); + success |= assignmentSuccess; + + // If the assignment satisfies both the expression 'e' and the PC + 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[idx] + .push_back(ConstantExpr::alloc(aIdx, arr->getDomain())); + } + } + delete a; + } + } + return success; +} diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp new file mode 100644 index 00000000..d4dc9a21 --- /dev/null +++ b/lib/Expr/ArrayExprRewriter.cpp @@ -0,0 +1,141 @@ +#include "klee/ArrayExprRewriter.h" + +#include "klee/util/BitArray.h" + +#include "llvm/Support/CommandLine.h" + +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::rewrite(const ref<Expr> &e, + const array2idx_ty &arrays, + const mapIndexOptimizedExpr_ty &idx_valIdx) { + ref<Expr> notFound; + std::vector<ref<Expr> > eqExprs; + bool invert = false; + for (auto &element : arrays) { + const Array* arr = element.first; + std::vector<ref<Expr> > indexes = element.second; + + IndexTransformationExprVisitor idxt_v(arr); + idxt_v.visit(e); + + 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; + } + + 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; + } 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]; + } 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); + } +} + +ref<Expr> ExprRewriter::concatenateOrExpr( + 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)); + } else { + return OrExpr::alloc(ZExtExpr::alloc((*begin), Expr::Int32), + concatenateOrExpr(begin + 1, end)); + } +} + +ref<Expr> ExprRewriter::createEqExpr(const ref<Expr> &index, + const ref<Expr> &valIndex) { + return EqExpr::alloc(valIndex, index); +} + +ref<Expr> ExprRewriter::createRangeExpr(const ref<Expr> &index, + const ref<Expr> &valStart, + const ref<Expr> &valEnd) { + return AndExpr::alloc(UleExpr::alloc(valStart, index), + UleExpr::alloc(index, valEnd)); +} diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp new file mode 100644 index 00000000..26ddbb95 --- /dev/null +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -0,0 +1,171 @@ +#include "klee/util/ArrayExprVisitor.h" + +#include "klee/Internal/Support/ErrorHandling.h" + +#include <algorithm> + +using namespace klee; + +//------------------------------ HELPER FUNCTIONS ---------------------------// +bool ArrayExprHelper::isReadExprAtOffset(ref<Expr> e, const ReadExpr *base, + ref<Expr> offset) { + const ReadExpr *re = dyn_cast<ReadExpr>(e.get()); + if (!re || (re->getWidth() != Expr::Int8)) + return false; + return SubExpr::create(re->index, base->index) == offset; +} + +ReadExpr *ArrayExprHelper::hasOrderedReads(const ConcatExpr &ce) { + const ReadExpr *base = dyn_cast<ReadExpr>(ce.getKid(0)); + + // right now, all Reads are byte reads but some + // transformations might change this + if (!base || base->getWidth() != Expr::Int8) + return NULL; + + // Get stride expr in proper index width. + Expr::Width idxWidth = base->index->getWidth(); + ref<Expr> strideExpr = ConstantExpr::alloc(-1, idxWidth); + ref<Expr> offset = ConstantExpr::create(0, idxWidth); + + ref<Expr> e = ce.getKid(1); + + // concat chains are unbalanced to the right + while (e->getKind() == Expr::Concat) { + offset = AddExpr::create(offset, strideExpr); + if (!isReadExprAtOffset(e->getKid(0), base, offset)) + return NULL; + e = e->getKid(1); + } + + offset = AddExpr::create(offset, strideExpr); + if (!isReadExprAtOffset(e, base, offset)) + return NULL; + + return cast<ReadExpr>(e.get()); +} + +//--------------------------- INDEX-BASED OPTIMIZATION-----------------------// +ExprVisitor::Action +ConstantArrayExprVisitor::visitConcat(const ConcatExpr &ce) { + ReadExpr *base = ArrayExprHelper::hasOrderedReads(ce); + if (base) { + // It is an interesting ReadExpr if it contains a concrete array + // that is read at a symbolic index + if (base->updates.root->isConstantArray() && + !isa<ConstantExpr>(base->index)) { + for (const UpdateNode *un = base->updates.head; un; un = un->next) { + if (!isa<ConstantExpr>(un->index) || !isa<ConstantExpr>(un->value)) { + incompatible = true; + return Action::skipChildren(); + } + } + IndexCompatibilityExprVisitor compatible; + compatible.visit(base->index); + if (compatible.isCompatible() && + addedIndexes.find(base->index.get()->hash()) == addedIndexes.end()) { + if (arrays.find(base->updates.root) == arrays.end()) { + arrays.insert( + std::make_pair(base->updates.root, std::vector<ref<Expr> >())); + } else { + // Another possible index to resolve, currently unsupported + incompatible = true; + return Action::skipChildren(); + } + arrays.find(base->updates.root)->second.push_back(base->index); + addedIndexes.insert(base->index.get()->hash()); + } else if (compatible.hasInnerReads()) { + // This Read has an inner Read, we want to optimize the inner one + // to create a cascading effect during assignment evaluation + return Action::doChildren(); + } + return Action::skipChildren(); + } + } + return Action::doChildren(); +} +ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) { + // It is an interesting ReadExpr if it contains a concrete array + // that is read at a symbolic index + if (re.updates.root->isConstantArray() && !isa<ConstantExpr>(re.index)) { + for (const UpdateNode *un = re.updates.head; un; un = un->next) { + if (!isa<ConstantExpr>(un->index) || !isa<ConstantExpr>(un->value)) { + incompatible = true; + return Action::skipChildren(); + } + } + IndexCompatibilityExprVisitor compatible; + compatible.visit(re.index); + if (compatible.isCompatible() && + addedIndexes.find(re.index.get()->hash()) == addedIndexes.end()) { + if (arrays.find(re.updates.root) == arrays.end()) { + arrays.insert( + std::make_pair(re.updates.root, std::vector<ref<Expr> >())); + } else { + // Another possible index to resolve, currently unsupported + incompatible = true; + return Action::skipChildren(); + } + arrays.find(re.updates.root)->second.push_back(re.index); + addedIndexes.insert(re.index.get()->hash()); + } else if (compatible.hasInnerReads()) { + // This Read has an inner Read, we want to optimize the inner one + // to create a cascading effect during assignment evaluation + return Action::doChildren(); + } + return Action::skipChildren(); + } else if (re.updates.root->isSymbolicArray()) { + incompatible = true; + } + + return Action::doChildren(); +} + +ExprVisitor::Action +IndexCompatibilityExprVisitor::visitRead(const ReadExpr &re) { + if (re.updates.head) { + compatible = false; + return Action::skipChildren(); + } else if (re.updates.root->isConstantArray() && + !isa<ConstantExpr>(re.index)) { + compatible = false; + inner = true; + return Action::skipChildren(); + } + return Action::doChildren(); +} +ExprVisitor::Action IndexCompatibilityExprVisitor::visitURem(const URemExpr &) { + compatible = false; + return Action::skipChildren(); +} +ExprVisitor::Action IndexCompatibilityExprVisitor::visitSRem(const SRemExpr &) { + compatible = false; + return Action::skipChildren(); +} +ExprVisitor::Action IndexCompatibilityExprVisitor::visitOr(const OrExpr &) { + compatible = false; + return Action::skipChildren(); +} + +ExprVisitor::Action +IndexTransformationExprVisitor::visitConcat(const ConcatExpr &ce) { + if (ReadExpr *re = dyn_cast<ReadExpr>(ce.getKid(0))) { + if (re->updates.root->hash() == array->hash() && width < ce.getWidth()) { + if (width == Expr::InvalidWidth) + width = ce.getWidth(); + } + } else if (ReadExpr *re = dyn_cast<ReadExpr>(ce.getKid(1))) { + if (re->updates.root->hash() == array->hash() && width < ce.getWidth()) { + if (width == Expr::InvalidWidth) + width = ce.getWidth(); + } + } + return Action::doChildren(); +} +ExprVisitor::Action IndexTransformationExprVisitor::visitMul(const MulExpr &e) { + if (isa<ConstantExpr>(e.getKid(0))) + mul = e.getKid(0); + else if (isa<ConstantExpr>(e.getKid(0))) + mul = e.getKid(1); + return Action::doChildren(); +} diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp new file mode 100644 index 00000000..755263f0 --- /dev/null +++ b/lib/Expr/AssignmentGenerator.cpp @@ -0,0 +1,327 @@ +#include "klee/AssignmentGenerator.h" + +#include "llvm/Support/raw_ostream.h" + +using namespace klee; + +bool AssignmentGenerator::generatePartialAssignment(const ref<Expr> &e, + ref<Expr> &val, + Assignment *&a) { + return helperGenerateAssignment(e, val, a, e->getWidth(), false); +} + +bool AssignmentGenerator::helperGenerateAssignment(const ref<Expr> &e, + ref<Expr> &val, + Assignment *&a, + Expr::Width width, + bool sign) { + Expr &ep = *e.get(); + switch (ep.getKind()) { + + // ARITHMETIC + case Expr::Add: { + // val = val - kid + ref<Expr> kid_val; + ref<Expr> kid_expr; + if (isa<ConstantExpr>(ep.getKid(0))) { + kid_val = ep.getKid(0); + kid_expr = ep.getKid(1); + } else if (isa<ConstantExpr>(ep.getKid(1))) { + kid_val = ep.getKid(1); + kid_expr = ep.getKid(0); + } else { + return false; + } + 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); + } else { + val = createSubExpr(kid_val, val); + } + return helperGenerateAssignment(kid_expr, val, a, width, sign); + } + case Expr::Sub: { + // val = val + kid + ref<Expr> kid_val; + ref<Expr> kid_expr; + if (isa<ConstantExpr>(ep.getKid(0))) { + kid_val = ep.getKid(0); + kid_expr = ep.getKid(1); + } else if (isa<ConstantExpr>(ep.getKid(1))) { + kid_val = ep.getKid(1); + kid_expr = ep.getKid(0); + } else { + return false; + } + val = createAddExpr(kid_val, val); + return helperGenerateAssignment(kid_expr, val, a, width, sign); + } + case Expr::Mul: { + // val = val / kid (check for sign) + ref<Expr> kid_val; + ref<Expr> kid_expr; + if (isa<ConstantExpr>(ep.getKid(0))) { + kid_val = ep.getKid(0); + kid_expr = ep.getKid(1); + } else if (isa<ConstantExpr>(ep.getKid(1))) { + kid_val = ep.getKid(1); + kid_expr = ep.getKid(0); + } else { + return false; + } + + if (kid_val.get()->isZero()) { + return false; + } else if (!createDivRem(kid_val, val, sign)->isZero()) { + return false; + } + val = createDivExpr(kid_val, val, sign); + return helperGenerateAssignment(kid_expr, val, a, width, sign); + } + case Expr::UDiv: + // val = val * kid + // no break, falling down to case SDiv + case Expr::SDiv: { + // val = val * kid + ref<Expr> kid_val; + ref<Expr> kid_expr; + if (isa<ConstantExpr>(ep.getKid(0))) { + kid_val = ep.getKid(0); + kid_expr = ep.getKid(1); + } else if (isa<ConstantExpr>(ep.getKid(1))) { + kid_val = ep.getKid(1); + kid_expr = ep.getKid(0); + } else { + return false; + } + val = createMulExpr(kid_val, val); + return helperGenerateAssignment(kid_expr, val, a, width, sign); + } + + // LOGICAL + case Expr::LShr: { + if (!isa<ConstantExpr>(ep.getKid(1))) { + return false; + } + ref<Expr> kid_val = ep.getKid(1); + val = createShlExpr(val, kid_val); + return helperGenerateAssignment(ep.getKid(0), val, a, width, sign); + } + case Expr::Shl: { + if (!isa<ConstantExpr>(ep.getKid(1))) { + return false; + } + ref<Expr> kid_val = ep.getKid(1); + val = createLShrExpr(val, kid_val); + return helperGenerateAssignment(ep.getKid(0), val, a, width, sign); + } + case Expr::Not: { + return helperGenerateAssignment(ep.getKid(0), val, a, width, sign); + } + case Expr::And: { + // val = val & kid + ref<Expr> kid_val; + ref<Expr> kid_expr; + if (isa<ConstantExpr>(ep.getKid(0))) { + kid_val = ep.getKid(0); + kid_expr = ep.getKid(1); + } else if (isa<ConstantExpr>(ep.getKid(1))) { + kid_val = ep.getKid(1); + kid_expr = ep.getKid(0); + } else { + return false; + } + val = createAndExpr(kid_val, val); + return helperGenerateAssignment(kid_expr, val, a, width, sign); + } + + // CASTING + case Expr::ZExt: { + val = createExtractExpr(ep.getKid(0), val); + return helperGenerateAssignment(ep.getKid(0), val, a, width, false); + } + case Expr::SExt: { + val = createExtractExpr(ep.getKid(0), val); + return helperGenerateAssignment(ep.getKid(0), val, a, width, true); + } + + // SPECIAL + case Expr::Concat: { + ReadExpr *base = hasOrderedReads(&ep); + if (base) { + return helperGenerateAssignment(ref<Expr>(base), val, a, ep.getWidth(), + sign); + } else { + klee_warning("Not supported"); + ep.printKind(llvm::errs(), ep.getKind()); + return false; + } + } + case Expr::Extract: { + val = createExtendExpr(ep.getKid(0), val); + return helperGenerateAssignment(ep.getKid(0), val, a, width, sign); + } + + // READ + case Expr::Read: { + ReadExpr &re = static_cast<ReadExpr &>(ep); + if (isa<ConstantExpr>(re.index)) { + if (re.updates.root->isSymbolicArray()) { + ConstantExpr &index = static_cast<ConstantExpr &>(*re.index.get()); + std::vector<unsigned char> c_value = + getIndexedValue(getByteValue(val), index, re.updates.root->size); + if (c_value.size() == 0) { + return false; + } + if (a->bindings.find(re.updates.root) == a->bindings.end()) { + a->bindings.insert(std::make_pair(re.updates.root, c_value)); + } else { + return false; + } + } + } else { + return helperGenerateAssignment(re.index, val, a, width, sign); + } + return true; + } + default: + std::string type_str; + llvm::raw_string_ostream rso(type_str); + ep.printKind(rso, ep.getKind()); + klee_warning("%s is not supported", rso.str().c_str()); + return false; + } +} + +bool AssignmentGenerator::isReadExprAtOffset(ref<Expr> e, const ReadExpr *base, + ref<Expr> offset) { + const ReadExpr *re = dyn_cast<ReadExpr>(e.get()); + if (!re || (re->getWidth() != Expr::Int8)) + return false; + return SubExpr::create(re->index, base->index) == offset; +} + +ReadExpr *AssignmentGenerator::hasOrderedReads(ref<Expr> e) { + assert(e->getKind() == Expr::Concat); + + const ReadExpr *base = dyn_cast<ReadExpr>(e->getKid(0)); + + // right now, all Reads are byte reads but some + // transformations might change this + if (!base || base->getWidth() != Expr::Int8) + return NULL; + + // Get stride expr in proper index width. + Expr::Width idxWidth = base->index->getWidth(); + ref<Expr> strideExpr = ConstantExpr::alloc(-1, idxWidth); + ref<Expr> offset = ConstantExpr::create(0, idxWidth); + + e = e->getKid(1); + + // concat chains are unbalanced to the right + while (e->getKind() == Expr::Concat) { + offset = AddExpr::create(offset, strideExpr); + if (!isReadExprAtOffset(e->getKid(0), base, offset)) + return NULL; + e = e->getKid(1); + } + + offset = AddExpr::create(offset, strideExpr); + if (!isReadExprAtOffset(e, base, offset)) + return NULL; + + return cast<ReadExpr>(e.get()); +} + +ref<Expr> AssignmentGenerator::createSubExpr(const ref<Expr> &l, ref<Expr> &r) { + return SubExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createAddExpr(const ref<Expr> &l, ref<Expr> &r) { + return AddExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createMulExpr(const ref<Expr> &l, ref<Expr> &r) { + return MulExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createDivRem(const ref<Expr> &l, ref<Expr> &r, + bool sign) { + if (sign) + return SRemExpr::create(r, l); + else + return URemExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createDivExpr(const ref<Expr> &l, ref<Expr> &r, + bool sign) { + if (sign) + return SDivExpr::create(r, l); + else + return UDivExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createShlExpr(const ref<Expr> &l, ref<Expr> &r) { + return ShlExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createLShrExpr(const ref<Expr> &l, + ref<Expr> &r) { + return LShrExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createAndExpr(const ref<Expr> &l, ref<Expr> &r) { + return AndExpr::create(r, l); +} + +ref<Expr> AssignmentGenerator::createExtractExpr(const ref<Expr> &l, + ref<Expr> &r) { + return ExtractExpr::create(r, 0, l.get()->getWidth()); +} + +ref<Expr> AssignmentGenerator::createExtendExpr(const ref<Expr> &l, + ref<Expr> &r) { + if (l.get()->getKind() == Expr::ZExt) { + return ZExtExpr::create(r, l.get()->getWidth()); + } else { + return SExtExpr::create(r, l.get()->getWidth()); + } +} + +std::vector<unsigned char> AssignmentGenerator::getByteValue(ref<Expr> &val) { + std::vector<unsigned char> toReturn; + if (ConstantExpr *value = dyn_cast<ConstantExpr>(val)) { + for (unsigned w = 0; w < val.get()->getWidth() / 8; ++w) { + ref<ConstantExpr> byte = value->Extract(w * 8, Expr::Int8); + unsigned char mem_val; + byte->toMemory(&mem_val); + toReturn.push_back(mem_val); + } + } + return toReturn; +} + +std::vector<unsigned char> +AssignmentGenerator::getIndexedValue(const std::vector<unsigned char> &c_val, + ConstantExpr &index, + const unsigned int size) { + std::vector<unsigned char> toReturn; + const llvm::APInt index_val = index.getAPValue(); + assert(!index_val.isSignBit() && "Negative index"); + const uint64_t id = index_val.getZExtValue() / c_val.size(); + uint64_t arraySize = size / c_val.size(); + for (uint64_t i = 0; i < arraySize; ++i) { + if (i == id) { + for (unsigned arr_i = 0; arr_i < c_val.size(); ++arr_i) { + toReturn.push_back(c_val[arr_i]); + } + } else { + for (unsigned arr_i = 0; arr_i < c_val.size(); ++arr_i) { + toReturn.push_back(0); + } + } + } + + return toReturn; +} diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt index 4c63fe5b..74407295 100644 --- a/lib/Expr/CMakeLists.txt +++ b/lib/Expr/CMakeLists.txt @@ -8,7 +8,11 @@ #===------------------------------------------------------------------------===# klee_add_component(kleaverExpr ArrayCache.cpp + ArrayExprOptimizer.cpp + ArrayExprRewriter.cpp + ArrayExprVisitor.cpp Assigment.cpp + AssignmentGenerator.cpp Constraints.cpp ExprBuilder.cpp Expr.cpp diff --git a/test/ArrayOpt/test-mix.c b/test/ArrayOpt/test-mix.c new file mode 100644 index 00000000..88cb595c --- /dev/null +++ b/test/ArrayOpt/test-mix.c @@ -0,0 +1,77 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,3,4,5}; +char arrayconc[4]; +char arraychar[3] = {'a','b','c'}; + +int main() { + char k, x; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + klee_assume(k >= 0); + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x < 2); + klee_assume(x >= 0); + klee_make_symbolic(&arrayconc, sizeof(arrayconc), "arrayconc"); + klee_make_symbolic(&arraychar, sizeof(arraychar), "arraychar"); + arraychar[0] = 'a'; + arraychar[2] = 'c'; + + // CHECK: Yes + // CHECK: No + // CHECK: Good + // CHECK: Char + // CHECK: Concrete + if (array[k] == 3) + printf("Yes\n"); + else if (array[k] > 4) + printf("No\n"); + else if (array[k] + k - 2 == 6) + printf("Good\n"); + + if (arraychar[x] > 2) + printf("Char\n"); + + int i = array[4] * 3 - 12; + if (arrayconc[i] > 3) { + printf("Concrete\n"); + } + + // CHECK: KLEE: done: completed paths = 12 + + return 0; +} diff --git a/test/ArrayOpt/test_and.c b/test/ArrayOpt/test_and.c new file mode 100644 index 00000000..310d2a9d --- /dev/null +++ b/test/ArrayOpt/test_and.c @@ -0,0 +1,35 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,-2,3,-4,-5}; + +int main() { + + unsigned char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k&1] > 0) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_array_index_array.c b/test/ArrayOpt/test_array_index_array.c new file mode 100644 index 00000000..7d5198e1 --- /dev/null +++ b/test/ArrayOpt/test_array_index_array.c @@ -0,0 +1,35 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,7,-4,5}; +char array2[5] = {0,3,4,1,2}; + +int main() { + unsigned char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[array2[k]] == 7) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_array_index_array_diffsize.c b/test/ArrayOpt/test_array_index_array_diffsize.c new file mode 100644 index 00000000..e331f909 --- /dev/null +++ b/test/ArrayOpt/test_array_index_array_diffsize.c @@ -0,0 +1,36 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,7,-4,5}; +char array2[5] = {0,3,4,1,2}; +char array3[10] = {0,0,0,0,0,4,0,0,0}; + +int main() { + unsigned char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 10); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[array2[array3[k]]] == 7) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_cache.c b/test/ArrayOpt/test_cache.c new file mode 100644 index 00000000..a2fe10da --- /dev/null +++ b/test/ArrayOpt/test_cache.c @@ -0,0 +1,61 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,3,4,5}; +char arrayconc[4] = {2,4,6,8}; +char arraychar[2] = {'a',127}; + +int main() { + char k, x; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + klee_assume(k >= 0); + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x < 2); + klee_assume(x >= 0); + + // CHECK: Yes + // CHECK: No + // CHECK: Good + // CHECK: Char + // CHECK: Concrete + if (array[k] == 3) + printf("Yes\n"); + else if (array[k] > 4) + printf("No\n"); + else if (array[k] + k - 2 == 6) + printf("Good\n"); + + if (arraychar[x] > 126) + printf("Char\n"); + + int i = array[4] * 3 - 12; + if (arrayconc[i] > 3) { + printf("Concrete\n"); + } + + // CHECK: KLEE: done: completed paths = 6 + + return 0; +} diff --git a/test/ArrayOpt/test_const_arr-idx.c b/test/ArrayOpt/test_const_arr-idx.c new file mode 100644 index 00000000..25f959a3 --- /dev/null +++ b/test/ArrayOpt/test_const_arr-idx.c @@ -0,0 +1,26 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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 + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +unsigned array[5] = {1,2,3,4,5}; +int arr[3] = {0,1,2}; + +int main() { + int x = 2; + unsigned k = arr[x]; + + // CHECK: Yes + if (array[k] == 3) + printf("Yes\n"); + + // CHECK: KLEE: done: completed paths = 1 + + return 0; +} diff --git a/test/ArrayOpt/test_expr_complex.c b/test/ArrayOpt/test_expr_complex.c new file mode 100644 index 00000000..2ae412b5 --- /dev/null +++ b/test/ArrayOpt/test_expr_complex.c @@ -0,0 +1,33 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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 + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +int array[10] = {1,2,3,-4,5,6,7,8,9,10}; + +int main() { + char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 4); + klee_assume(k >=0); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k*3] < 0) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_expr_simple.c b/test/ArrayOpt/test_expr_simple.c new file mode 100644 index 00000000..433b864f --- /dev/null +++ b/test/ArrayOpt/test_expr_simple.c @@ -0,0 +1,32 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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 + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,3,-4,5}; + +int main() { + unsigned char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k] == -4) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_feasible.c b/test/ArrayOpt/test_feasible.c new file mode 100644 index 00000000..17bfa523 --- /dev/null +++ b/test/ArrayOpt/test_feasible.c @@ -0,0 +1,39 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {0,1,0,1,0}; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + // CHECK: zero + // CHECK-NEXT: Correct! + // CHECK-NOT: Wrong! + if (array[k] == 0) { + printf("zero\n"); + if (k==0|k==2|k==4) { + printf("Correct!\n"); + } else { + printf("Wrong!\n"); + } + } + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_hybrid.c b/test/ArrayOpt/test_hybrid.c new file mode 100644 index 00000000..ab7becf4 --- /dev/null +++ b/test/ArrayOpt/test_hybrid.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: FileCheck %s -input-file=%t.log -check-prefix=CHECK-OPT_I +// RUN: test -f %t.klee-out/test000001.kquery +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[10] = {1,2,2,4,5,3,1,3,2,2}; + +int main() { + unsigned char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 10); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k] >= 1) + printf("Yes\n"); + + // CHECK: KLEE: done: completed paths = 1 + + return 0; +} diff --git a/test/ArrayOpt/test_multindex.c b/test/ArrayOpt/test_multindex.c new file mode 100644 index 00000000..4dada79d --- /dev/null +++ b/test/ArrayOpt/test_multindex.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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 + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {0,1,2,3,4}; + +int main() { + unsigned k; + unsigned x; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + klee_make_symbolic(&x, sizeof(x), "x"); + klee_assume(x < 5); + + // CHECK: Yes + if ((array[k] + array[x]) - 7 == 0) + printf("Yes\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_new.c b/test/ArrayOpt/test_new.c new file mode 100644 index 00000000..7e095e76 --- /dev/null +++ b/test/ArrayOpt/test_new.c @@ -0,0 +1,32 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: test -f %t.klee-out/test000001.kquery +// RUN: test -f %t.klee-out/test000002.kquery + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,3,-4,5}; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 4); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k] + array[k+1] < 0) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_nier.c b/test/ArrayOpt/test_nier.c new file mode 100644 index 00000000..93fb96aa --- /dev/null +++ b/test/ArrayOpt/test_nier.c @@ -0,0 +1,37 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include<stdio.h> +#include "klee/klee.h" + +int array[1000] = {0, 1, 8, 27, 64, 125, 216, 343, 512, 729, 1000, 1331, 1728, 2197, 2744, 3375, 4096, 4913, 5832, 6859, 8000, 9261, 10648, 12167, 13824, 15625, 17576, 19683, 21952, 24389, 27000, 29791, 32768, 35937, 39304, 42875, 46656, 50653, 54872, 59319, 64000, 68921, 74088, 79507, 85184, 91125, 97336, 103823, 110592, 117649, 125000, 132651, 140608, 148877, 157464, 166375, 175616, 185193, 195112, 205379, 216000, 226981, 238328, 250047, 262144, 274625, 287496, 300763, 314432, 328509, 343000, 357911, 373248, 389017, 405224, 421875, 438976, 456533, 474552, 493039, 512000, 531441, 551368, 571787, 592704, 614125, 636056, 658503, 681472, 704969, 729000, 753571, 778688, 804357, 830584, 857375, 884736, 912673, 941192, 970299, 1000000, 1030301, 1061208, 1092727, 1124864, 1157625, 1191016, 1225043, 1259712, 1295029, 1331000, 1367631, 1404928, 1442897, 1481544, 1520875, 1560896, 1601613, 1643032, 1685159, 1728000, 1771561, 1815848, 1860867, 1906624, 1953125, 2000376, 2048383, 2097152, 2146689, 2197000, 2248091, 2299968, 2352637, 2406104, 2460375, 2515456, 2571353, 2628072, 2685619, 2744000, 2803221, 2863288, 2924207, 2985984, 3048625, 3112136, 3176523, 3241792, 3307949, 3375000, 3442951, 3511808, 3581577, 3652264, 3723875, 3796416, 3869893, 3944312, 4019679, 4096000, 4173281, 4251528, 4330747, 4410944, 4492125, 4574296, 4657463, 4741632, 4826809, 4913000, 5000211, 5088448, 5177717, 5268024, 5359375, 5451776, 5545233, 5639752, 5735339, 5832000, 5929741, 6028568, 6128487, 6229504, 6331625, 6434856, 6539203, 6644672, 6751269, 6859000, 6967871, 7077888, 7189057, 7301384, 7414875, 7529536, 7645373, 7762392, 7880599, 8000000, 8120601, 8242408, 8365427, 8489664, 8615125, 8741816, 8869743, 8998912, 9129329, 9261000, 9393931, 9528128, 9663597, 9800344, 9938375, 10077696, 10218313, 10360232, 10503459, 10648000, 10793861, 10941048, 11089567, 11239424, 11390625, 11543176, 11697083, 11852352, 12008989, 12167000, 12326391, 12487168, 12649337, 12812904, 12977875, 13144256, 13312053, 13481272, 13651919, 13824000, 13997521, 14172488, 14348907, 14526784, 14706125, 14886936, 15069223, 15252992, 15438249, 15625000, 15813251, 16003008, 16194277, 16387064, 16581375, 16777216, 16974593, 17173512, 17373979, 17576000, 17779581, 17984728, 18191447, 18399744, 18609625, 18821096, 19034163, 19248832, 19465109, 19683000, 19902511, 20123648, 20346417, 20570824, 20796875, 21024576, 21253933, 21484952, 21717639, 21952000, 22188041, 22425768, 22665187, 22906304, 23149125, 23393656, 23639903, 23887872, 24137569, 24389000, 24642171, 24897088, 25153757, 25412184, 25672375, 25934336, 26198073, 26463592, 26730899, 27000000, 27270901, 27543608, 27818127, 28094464, 28372625, 28652616, 28934443, 29218112, 29503629, 29791000, 30080231, 30371328, 30664297, 30959144, 31255875, 31554496, 31855013, 32157432, 32461759, 32768000, 33076161, 33386248, 33698267, 34012224, 34328125, 34645976, 34965783, 35287552, 35611289, 35937000, 36264691, 36594368, 36926037, 37259704, 37595375, 37933056, 38272753, 38614472, 38958219, 39304000, 39651821, 40001688, 40353607, 40707584, 41063625, 41421736, 41781923, 42144192, 42508549, 42875000, 43243551, 43614208, 43986977, 44361864, 44738875, 45118016, 45499293, 45882712, 46268279, 46656000, 47045881, 47437928, 47832147, 48228544, 48627125, 49027896, 49430863, 49836032, 50243409, 50653000, 51064811, 51478848, 51895117, 52313624, 52734375, 53157376, 53582633, 54010152, 54439939, 54872000, 55306341, 55742968, 56181887, 56623104, 57066625, 57512456, 57960603, 58411072, 58863869, 59319000, 59776471, 60236288, 60698457, 61162984, 61629875, 62099136, 62570773, 63044792, 63521199, 64000000, 64481201, 64964808, 65450827, 65939264, 66430125, 66923416, 67419143, 67917312, 68417929, 68921000, 69426531, 69934528, 70444997, 70957944, 71473375, 71991296, 72511713, 73034632, 73560059, 74088000, 74618461, 75151448, 75686967, 76225024, 76765625, 77308776, 77854483, 78402752, 78953589, 79507000, 80062991, 80621568, 81182737, 81746504, 82312875, 82881856, 83453453, 84027672, 84604519, 85184000, 85766121, 86350888, 86938307, 87528384, 88121125, 88716536, 89314623, 89915392, 90518849, 91125000, 91733851, 92345408, 92959677, 93576664, 94196375, 94818816, 95443993, 96071912, 96702579, 97336000, 97972181, 98611128, 99252847, 99897344, 100544625, 101194696, 101847563, 102503232, 103161709, 103823000, 104487111, 105154048, 105823817, 106496424, 107171875, 107850176, 108531333, 109215352, 109902239, 110592000, 111284641, 111980168, 112678587, 113379904, 114084125, 114791256, 115501303, 116214272, 116930169, 117649000, 118370771, 119095488, 119823157, 120553784, 121287375, 122023936, 122763473, 123505992, 124251499, 125000000, 125751501, 126506008, 127263527, 128024064, 128787625, 129554216, 130323843, 131096512, 131872229, 132651000, 133432831, 134217728, 135005697, 135796744, 136590875, 137388096, 138188413, 138991832, 139798359, 140608000, 141420761, 142236648, 143055667, 143877824, 144703125, 145531576, 146363183, 147197952, 148035889, 148877000, 149721291, 150568768, 151419437, 152273304, 153130375, 153990656, 154854153, 155720872, 156590819, 157464000, 158340421, 159220088, 160103007, 160989184, 161878625, 162771336, 163667323, 164566592, 165469149, 166375000, 167284151, 168196608, 169112377, 170031464, 170953875, 171879616, 172808693, 173741112, 174676879, 175616000, 176558481, 177504328, 178453547, 179406144, 180362125, 181321496, 182284263, 183250432, 184220009, 185193000, 186169411, 187149248, 188132517, 189119224, 190109375, 191102976, 192100033, 193100552, 194104539, 195112000, 196122941, 197137368, 198155287, 199176704, 200201625, 201230056, 202262003, 203297472, 204336469, 205379000, 206425071, 207474688, 208527857, 209584584, 210644875, 211708736, 212776173, 213847192, 214921799, 216000000, 217081801, 218167208, 219256227, 220348864, 221445125, 222545016, 223648543, 224755712, 225866529, 226981000, 228099131, 229220928, 230346397, 231475544, 232608375, 233744896, 234885113, 236029032, 237176659, 238328000, 239483061, 240641848, 241804367, 242970624, 244140625, 245314376, 246491883, 247673152, 248858189, 250047000, 251239591, 252435968, 253636137, 254840104, 256047875, 257259456, 258474853, 259694072, 260917119, 262144000, 263374721, 264609288, 265847707, 267089984, 268336125, 269586136, 270840023, 272097792, 273359449, 274625000, 275894451, 277167808, 278445077, 279726264, 281011375, 282300416, 283593393, 284890312, 286191179, 287496000, 288804781, 290117528, 291434247, 292754944, 294079625, 295408296, 296740963, 298077632, 299418309, 300763000, 302111711, 303464448, 304821217, 306182024, 307546875, 308915776, 310288733, 311665752, 313046839, 314432000, 315821241, 317214568, 318611987, 320013504, 321419125, 322828856, 324242703, 325660672, 327082769, 328509000, 329939371, 331373888, 332812557, 334255384, 335702375, 337153536, 338608873, 340068392, 341532099, 343000000, 344472101, 345948408, 347428927, 348913664, 350402625, 351895816, 353393243, 354894912, 356400829, 357911000, 359425431, 360944128, 362467097, 363994344, 365525875, 367061696, 368601813, 370146232, 371694959, 373248000, 374805361, 376367048, 377933067, 379503424, 381078125, 382657176, 384240583, 385828352, 387420489, 389017000, 390617891, 392223168, 393832837, 395446904, 397065375, 398688256, 400315553, 401947272, 403583419, 405224000, 406869021, 408518488, 410172407, 411830784, 413493625, 415160936, 416832723, 418508992, 420189749, 421875000, 423564751, 425259008, 426957777, 428661064, 430368875, 432081216, 433798093, 435519512, 437245479, 438976000, 440711081, 442450728, 444194947, 445943744, 447697125, 449455096, 451217663, 452984832, 454756609, 456533000, 458314011, 460099648, 461889917, 463684824, 465484375, 467288576, 469097433, 470910952, 472729139, 474552000, 476379541, 478211768, 480048687, 481890304, 483736625, 485587656, 487443403, 489303872, 491169069, 493039000, 494913671, 496793088, 498677257, 500566184, 502459875, 504358336, 506261573, 508169592, 510082399, 512000000, 513922401, 515849608, 517781627, 519718464, 521660125, 523606616, 525557943, 527514112, 529475129, 531441000, 533411731, 535387328, 537367797, 539353144, 541343375, 543338496, 545338513, 547343432, 549353259, 551368000, 553387661, 555412248, 557441767, 559476224, 561515625, 563559976, 565609283, 567663552, 569722789, 571787000, 573856191, 575930368, 578009537, 580093704, 582182875, 584277056, 586376253, 588480472, 590589719, 592704000, 594823321, 596947688, 599077107, 601211584, 603351125, 605495736, 607645423, 609800192, 611960049, 614125000, 616295051, 618470208, 620650477, 622835864, 625026375, 627222016, 629422793, 631628712, 633839779, 636056000, 638277381, 640503928, 642735647, 644972544, 647214625, 649461896, 651714363, 653972032, 656234909, 658503000, 660776311, 663054848, 665338617, 667627624, 669921875, 672221376, 674526133, 676836152, 679151439, 681472000, 683797841, 686128968, 688465387, 690807104, 693154125, 695506456, 697864103, 700227072, 702595369, 704969000, 707347971, 709732288, 712121957, 714516984, 716917375, 719323136, 721734273, 724150792, 726572699, 729000000, 731432701, 733870808, 736314327, 738763264, 741217625, 743677416, 746142643, 748613312, 751089429, 753571000, 756058031, 758550528, 761048497, 763551944, 766060875, 768575296, 771095213, 773620632, 776151559, 778688000, 781229961, 783777448, 786330467, 788889024, 791453125, 794022776, 796597983, 799178752, 801765089, 804357000, 806954491, 809557568, 812166237, 814780504, 817400375, 820025856, 822656953, 825293672, 827936019, 830584000, 833237621, 835896888, 838561807, 841232384, 843908625, 846590536, 849278123, 851971392, 854670349, 857375000, 860085351, 862801408, 865523177, 868250664, 870983875, 873722816, 876467493, 879217912, 881974079, 884736000, 887503681, 890277128, 893056347, 895841344, 898632125, 901428696, 904231063, 907039232, 909853209, 912673000, 915498611, 918330048, 921167317, 924010424, 926859375, 929714176, 932574833, 935441352, 938313739, 941192000, 944076141, 946966168, 949862087, 952763904, 955671625, 958585256, 961504803, 964430272, 967361669, 970299000, 973242271, 976191488, 979146657, 982107784, 985074875, 988047936, 991026973, 994011992, 997002999}; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k > 0); + klee_assume(k<1000); + + // CHECK-NOT: memory error: out of bound pointer + // CHECK: Yes + // CHECK-NEXT: No + if (array[k] > 1000000 || + array[k-1] > 1000000) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_noncontiguous_idx.c b/test/ArrayOpt/test_noncontiguous_idx.c new file mode 100644 index 00000000..8eb16021 --- /dev/null +++ b/test/ArrayOpt/test_noncontiguous_idx.c @@ -0,0 +1,29 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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 + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {0,1,0,1,0}; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + // CHECK: Zero + if (array[k] == 0) + printf("zero\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_position.c b/test/ArrayOpt/test_position.c new file mode 100644 index 00000000..e42371b6 --- /dev/null +++ b/test/ArrayOpt/test_position.c @@ -0,0 +1,32 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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 + +// CHECK-OPT_I: KLEE: WARNING: OPT_I: successful +// CHECK-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +short array[5] = {1,2,3,-4,5}; + +int main() { + unsigned k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k] == 5) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_sub_idx.c b/test/ArrayOpt/test_sub_idx.c new file mode 100644 index 00000000..ef068427 --- /dev/null +++ b/test/ArrayOpt/test_sub_idx.c @@ -0,0 +1,35 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +char array[5] = {1,2,3,4,5}; + +int main() { + unsigned char k; + + klee_make_symbolic(&k, sizeof(k), "k"); + klee_assume(k < 5); + klee_assume(k > 0); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[k-1] == 1) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} diff --git a/test/ArrayOpt/test_var_idx.c b/test/ArrayOpt/test_var_idx.c new file mode 100644 index 00000000..4fbfe7ce --- /dev/null +++ b/test/ArrayOpt/test_var_idx.c @@ -0,0 +1,33 @@ +// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t.bc +// 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: 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-CONST_ARR: const_arr + +#include <stdio.h> +#include "klee/klee.h" + +unsigned array[5] = {1,2,3,4,5}; + +int main() { + unsigned idx; + klee_make_symbolic(&idx, sizeof(idx), "idx"); + klee_assume(idx < 5); + + // CHECK: Yes + // CHECK-NEXT: No + if (array[idx] == 3) + printf("Yes\n"); + else + printf("No\n"); + + // CHECK: KLEE: done: completed paths = 2 + + return 0; +} |