From e13f4d5ea1201361ec96aa96afec7b5604c52082 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 18 Oct 2018 12:59:04 +0100 Subject: Move optimization specific headers away from the project include directory Don't pollute the project include directory with optimization specific headers. --- lib/Expr/ArrayExprOptimizer.cpp | 8 +-- lib/Expr/ArrayExprOptimizer.h | 64 ++++++++++++++++++ lib/Expr/ArrayExprRewriter.cpp | 4 +- lib/Expr/ArrayExprRewriter.h | 47 +++++++++++++ lib/Expr/ArrayExprVisitor.cpp | 2 +- lib/Expr/ArrayExprVisitor.h | 143 +++++++++++++++++++++++++++++++++++++++ lib/Expr/AssignmentGenerator.cpp | 2 +- lib/Expr/AssignmentGenerator.h | 59 ++++++++++++++++ 8 files changed, 321 insertions(+), 8 deletions(-) create mode 100644 lib/Expr/ArrayExprOptimizer.h create mode 100644 lib/Expr/ArrayExprRewriter.h create mode 100644 lib/Expr/ArrayExprVisitor.h create mode 100644 lib/Expr/AssignmentGenerator.h (limited to 'lib/Expr') diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index dc0b2002..63a9fb96 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/ArrayExprOptimizer.h" +#include "ArrayExprOptimizer.h" #include #include @@ -17,12 +17,12 @@ #include #include -#include "klee/ArrayExprRewriter.h" -#include "klee/AssignmentGenerator.h" +#include "ArrayExprRewriter.h" +#include "ArrayExprVisitor.h" +#include "AssignmentGenerator.h" #include "klee/Config/Version.h" #include "klee/ExprBuilder.h" #include "klee/Internal/Support/ErrorHandling.h" -#include "klee/util/ArrayExprVisitor.h" #include "klee/util/Assignment.h" #include "klee/util/BitArray.h" diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h new file mode 100644 index 00000000..7d895a48 --- /dev/null +++ b/lib/Expr/ArrayExprOptimizer.h @@ -0,0 +1,64 @@ +//===-- ArrayExprOptimizer.h ----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_EXPROPTIMIZER_H +#define KLEE_EXPROPTIMIZER_H + +#include +#include +#include +#include +#include +#include + +#include "klee/Expr.h" +#include "klee/util/Ref.h" + +namespace klee { + +enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE }; + +typedef std::map>> array2idx_ty; +typedef std::map, std::vector>> mapIndexOptimizedExpr_ty; + +class ExprOptimizer { +private: + std::unordered_map> cacheExprOptimized; + std::unordered_set cacheExprUnapplicable; + std::unordered_map> cacheReadExprOptimized; + +public: + /// Returns the optimised version of e. + /// @param e expression to optimise + /// @param valueOnly XXX document + /// @return optimised expression + ref optimizeExpr(const ref &e, bool valueOnly); + +private: + bool computeIndexes(array2idx_ty &arrays, const ref &e, + mapIndexOptimizedExpr_ty &idx_valIdx) const; + + ref getSelectOptExpr( + const ref &e, std::vector &reads, + std::map> &readInfo, + bool isSymbolic); + + ref buildConstantSelectExpr(const ref &index, + std::vector &arrayValues, + Expr::Width width, + unsigned elementsInArray) const; + + ref + buildMixedSelectExpr(const ReadExpr *re, + std::vector> &arrayValues, + Expr::Width width, unsigned elementsInArray) const; +}; +} // namespace klee + +#endif diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp index 26aef1ff..507ea753 100644 --- a/lib/Expr/ArrayExprRewriter.cpp +++ b/lib/Expr/ArrayExprRewriter.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/ArrayExprRewriter.h" +#include "ArrayExprRewriter.h" #include #include @@ -16,7 +16,7 @@ #include #include -#include "klee/util/ArrayExprVisitor.h" +#include "ArrayExprVisitor.h" #include "klee/util/BitArray.h" using namespace klee; diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h new file mode 100644 index 00000000..310ae8dd --- /dev/null +++ b/lib/Expr/ArrayExprRewriter.h @@ -0,0 +1,47 @@ +//===-- ArrayExprRewriter.h -----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef LIB_EXPRREWRITER_H_ +#define LIB_EXPRREWRITER_H_ + +#include +#include +#include + +#include "klee/Expr.h" +#include "klee/util/Ref.h" + +namespace klee { + +typedef std::map>> array2idx_ty; +typedef std::map, std::vector>> mapIndexOptimizedExpr_ty; + +class ExprRewriter { +public: + static ref createOptExpr(const ref &e, const array2idx_ty &arrays, + const mapIndexOptimizedExpr_ty &idx_valIdx); + +private: + static ref rewrite(const ref &e, const array2idx_ty &arrays, + const mapIndexOptimizedExpr_ty &idx_valIdx); + + static ref + concatenateOrExpr(const std::vector>::const_iterator begin, + const std::vector>::const_iterator end); + + static ref createEqExpr(const ref &index, + const ref &valIndex); + + static ref createRangeExpr(const ref &index, + const ref &valStart, + const ref &valEnd); +}; +} // namespace klee + +#endif /* LIB_EXPRREWRITER_H_ */ diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index dae4c451..407c4c64 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ArrayExprVisitor.h" +#include "ArrayExprVisitor.h" #include "klee/Internal/Support/ErrorHandling.h" diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h new file mode 100644 index 00000000..c1eb7f58 --- /dev/null +++ b/lib/Expr/ArrayExprVisitor.h @@ -0,0 +1,143 @@ +//===-- ArrayExprVisitor.h ------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_ARRAYEXPRVISITOR_H_ +#define KLEE_ARRAYEXPRVISITOR_H_ + +#include "klee/CommandLine.h" +#include "klee/ExprBuilder.h" +#include "klee/util/ExprVisitor.h" + +#include +#include + +namespace klee { + +//------------------------------ HELPER FUNCTIONS ---------------------------// +class ArrayExprHelper { +private: + static bool isReadExprAtOffset(ref e, const ReadExpr *base, + ref offset); + +public: + static ReadExpr *hasOrderedReads(const ConcatExpr &ce); +}; + +//--------------------------- INDEX-BASED OPTIMIZATION-----------------------// +class ConstantArrayExprVisitor : public ExprVisitor { +private: + typedef std::map>> bindings_ty; + bindings_ty &arrays; + // Avoids adding the same index twice + std::unordered_set 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 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 getMul() { return mul; } +}; + +//------------------------- VALUE-BASED OPTIMIZATION-------------------------// +class ArrayReadExprVisitor : public ExprVisitor { +private: + std::vector &reads; + std::map> &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 &_reads, + std::map> &_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: + std::unordered_set visited; + std::map> optimized; + +protected: + Action visitConcat(const ConcatExpr &); + Action visitRead(const ReadExpr &re); + +public: + ArrayValueOptReplaceVisitor(std::map> &_optimized, + bool recursive = true) + : ExprVisitor(recursive), optimized(_optimized) {} +}; + +class IndexCleanerVisitor : public ExprVisitor { +private: + bool mul; + ref index; + +protected: + Action visitMul(const MulExpr &); + Action visitRead(const ReadExpr &); + +public: + IndexCleanerVisitor() : ExprVisitor(true), mul(true) {} + inline ref getIndex() { return index; } +}; +} // namespace klee + +#endif diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp index a906f796..87b75820 100644 --- a/lib/Expr/AssignmentGenerator.cpp +++ b/lib/Expr/AssignmentGenerator.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "../../include/klee/AssignmentGenerator.h" +#include "AssignmentGenerator.h" #include #include diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h new file mode 100644 index 00000000..fea1168a --- /dev/null +++ b/lib/Expr/AssignmentGenerator.h @@ -0,0 +1,59 @@ +//===-- AssignmentGenerator.h ---------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_ASSIGNMENTGENERATOR_H +#define KLEE_ASSIGNMENTGENERATOR_H + +#include + +#include "klee/Expr.h" +#include "klee/util/Ref.h" + +namespace klee { +class Assignment; +} /* namespace klee */ + +namespace klee { + +class Expr; +template class ref; + +class AssignmentGenerator { +public: + static bool generatePartialAssignment(const ref &e, ref &val, + Assignment *&a); + +private: + static bool helperGenerateAssignment(const ref &e, ref &val, + Assignment *&a, Expr::Width width, + bool sign); + + static bool isReadExprAtOffset(ref e, const ReadExpr *base, + ref offset); + static ReadExpr *hasOrderedReads(ref e); + + static ref createSubExpr(const ref &l, ref &r); + static ref createAddExpr(const ref &l, ref &r); + static ref createMulExpr(const ref &l, ref &r); + static ref createDivExpr(const ref &l, ref &r, bool sign); + static ref createDivRem(const ref &l, ref &r, bool sign); + static ref createShlExpr(const ref &l, ref &r); + static ref createLShrExpr(const ref &l, ref &r); + static ref createAndExpr(const ref &l, ref &r); + static ref createExtractExpr(const ref &l, ref &r); + static ref createExtendExpr(const ref &l, ref &r); + + static std::vector getByteValue(ref &val); + static std::vector + getIndexedValue(const std::vector &c_val, ConstantExpr &index, + const unsigned int size); +}; +} // namespace klee + +#endif -- cgit 1.4.1