From 382de941118c12434410df0c5d4e1ecd28e4636f Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Fri, 3 Apr 2020 17:55:58 +0100 Subject: Move header files from lib/Expr to include/klee/Expr to eliminate includes using "../" --- include/klee/Expr/ArrayExprOptimizer.h | 65 ++++++++++++++++ include/klee/Expr/ArrayExprRewriter.h | 47 ++++++++++++ include/klee/Expr/ArrayExprVisitor.h | 129 ++++++++++++++++++++++++++++++++ include/klee/Expr/AssignmentGenerator.h | 59 +++++++++++++++ lib/Core/Executor.cpp | 5 +- lib/Core/Executor.h | 3 +- lib/Expr/ArrayExprOptimizer.cpp | 10 +-- lib/Expr/ArrayExprOptimizer.h | 65 ---------------- lib/Expr/ArrayExprRewriter.cpp | 13 ++-- lib/Expr/ArrayExprRewriter.h | 47 ------------ lib/Expr/ArrayExprVisitor.cpp | 2 +- lib/Expr/ArrayExprVisitor.h | 129 -------------------------------- lib/Expr/AssignmentGenerator.cpp | 2 +- lib/Expr/AssignmentGenerator.h | 59 --------------- unittests/Expr/ArrayExprTest.cpp | 6 +- 15 files changed, 322 insertions(+), 319 deletions(-) create mode 100644 include/klee/Expr/ArrayExprOptimizer.h create mode 100644 include/klee/Expr/ArrayExprRewriter.h create mode 100644 include/klee/Expr/ArrayExprVisitor.h create mode 100644 include/klee/Expr/AssignmentGenerator.h delete mode 100644 lib/Expr/ArrayExprOptimizer.h delete mode 100644 lib/Expr/ArrayExprRewriter.h delete mode 100644 lib/Expr/ArrayExprVisitor.h delete mode 100644 lib/Expr/AssignmentGenerator.h diff --git a/include/klee/Expr/ArrayExprOptimizer.h b/include/klee/Expr/ArrayExprOptimizer.h new file mode 100644 index 00000000..8fc040e5 --- /dev/null +++ b/include/klee/Expr/ArrayExprOptimizer.h @@ -0,0 +1,65 @@ +//===-- 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_ARRAYEXPROPTIMIZER_H +#define KLEE_ARRAYEXPROPTIMIZER_H + +#include +#include +#include +#include +#include +#include + +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/util/Ref.h" + +namespace klee { + +enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE }; + +using array2idx_ty = std::map>>; +using mapIndexOptimizedExpr_ty = std::map, std::vector>>; + +class ExprOptimizer { +private: + ExprHashMap> cacheExprOptimized; + ExprHashSet cacheExprUnapplicable; + ExprHashMap> 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, Expr::Width>> &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 /* KLEE_ARRAYEXPROPTIMIZER_H */ diff --git a/include/klee/Expr/ArrayExprRewriter.h b/include/klee/Expr/ArrayExprRewriter.h new file mode 100644 index 00000000..098cb0a6 --- /dev/null +++ b/include/klee/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 KLEE_ARRAYEXPRREWRITER_H +#define KLEE_ARRAYEXPRREWRITER_H + +#include +#include +#include + +#include "klee/Expr/Expr.h" +#include "klee/util/Ref.h" + +namespace klee { + +using array2idx_ty = std::map>>; +using mapIndexOptimizedExpr_ty = std::map, std::vector>>; + +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 /* KLEE_ARRAYEXPRREWRITER_H */ diff --git a/include/klee/Expr/ArrayExprVisitor.h b/include/klee/Expr/ArrayExprVisitor.h new file mode 100644 index 00000000..28f485d9 --- /dev/null +++ b/include/klee/Expr/ArrayExprVisitor.h @@ -0,0 +1,129 @@ +//===-- 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/Expr/ExprBuilder.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/ExprVisitor.h" +#include "klee/Solver/SolverCmdLine.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: + using bindings_ty = std::map>>; + bindings_ty &arrays; + // Avoids adding the same index twice + std::unordered_set addedIndexes; + bool incompatible; + +protected: + Action visitConcat(const ConcatExpr &) override; + Action visitRead(const ReadExpr &) override; + +public: + explicit ConstantArrayExprVisitor(bindings_ty &_arrays) + : arrays(_arrays), incompatible(false) {} + inline bool isIncompatible() { return incompatible; } +}; + +class IndexCompatibilityExprVisitor : public ExprVisitor { +private: + bool compatible{true}; + bool inner{false}; + +protected: + Action visitRead(const ReadExpr &) override; + Action visitURem(const URemExpr &) override; + Action visitSRem(const SRemExpr &) override; + Action visitOr(const OrExpr &) override; + +public: + IndexCompatibilityExprVisitor() = default; + + 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 &) override; + Action visitMul(const MulExpr &) override; + +public: + explicit 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, Expr::Width>> &readInfo; + bool symbolic; + bool incompatible; + + Action inspectRead(ref hash, Expr::Width width, const ReadExpr &); + +protected: + Action visitConcat(const ConcatExpr &) override; + Action visitRead(const ReadExpr &) override; + +public: + ArrayReadExprVisitor( + std::vector &_reads, + std::map, 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: + ExprHashMap> optimized; + +protected: + Action visitConcat(const ConcatExpr &) override; + Action visitRead(const ReadExpr &re) override; + +public: + explicit ArrayValueOptReplaceVisitor(ExprHashMap> &_optimized, + bool recursive = true) + : ExprVisitor(recursive), optimized(_optimized) {} +}; +} // namespace klee + +#endif /* KLEE_ARRAYEXPRVISITOR_H */ diff --git a/include/klee/Expr/AssignmentGenerator.h b/include/klee/Expr/AssignmentGenerator.h new file mode 100644 index 00000000..173b863e --- /dev/null +++ b/include/klee/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 "klee/Expr/Expr.h" +#include "klee/util/Ref.h" + +#include + +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 /* KLEE_ASSIGNMENTGENERATOR_H */ diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index a3e84486..74965625 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -9,9 +9,9 @@ #include "Executor.h" -#include "../Expr/ArrayExprOptimizer.h" #include "Context.h" #include "CoreStats.h" +#include "ExecutionState.h" #include "ExternalDispatcher.h" #include "ImpliedValue.h" #include "Memory.h" @@ -26,7 +26,8 @@ #include "klee/Common.h" #include "klee/Config/Version.h" -#include "klee/ExecutionState.h" +#include "klee/Core/Interpreter.h" +#include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 374dd30b..cd6b173a 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -17,6 +17,7 @@ #include "klee/ExecutionState.h" #include "klee/Expr/ArrayCache.h" +#include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Module/Cell.h" #include "klee/Module/KInstruction.h" #include "klee/Module/KModule.h" @@ -26,8 +27,6 @@ #include "llvm/ADT/Twine.h" #include "llvm/Support/raw_ostream.h" -#include "../Expr/ArrayExprOptimizer.h" - #include #include #include diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index c3be0690..6e10461f 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -7,16 +7,16 @@ // //===----------------------------------------------------------------------===// -#include "ArrayExprOptimizer.h" -#include "ArrayExprRewriter.h" -#include "ArrayExprVisitor.h" -#include "AssignmentGenerator.h" +#include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Config/Version.h" +#include "klee/Expr/ArrayExprRewriter.h" +#include "klee/Expr/ArrayExprVisitor.h" #include "klee/Expr/Assignment.h" +#include "klee/Expr/AssignmentGenerator.h" #include "klee/Expr/ExprBuilder.h" -#include "klee/Support/ErrorHandling.h" #include "klee/OptionCategories.h" +#include "klee/Support/ErrorHandling.h" #include "klee/util/BitArray.h" #include diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h deleted file mode 100644 index 8fc040e5..00000000 --- a/lib/Expr/ArrayExprOptimizer.h +++ /dev/null @@ -1,65 +0,0 @@ -//===-- 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_ARRAYEXPROPTIMIZER_H -#define KLEE_ARRAYEXPROPTIMIZER_H - -#include -#include -#include -#include -#include -#include - -#include "klee/Expr/Expr.h" -#include "klee/Expr/ExprHashMap.h" -#include "klee/util/Ref.h" - -namespace klee { - -enum ArrayOptimizationType { NONE, ALL, INDEX, VALUE }; - -using array2idx_ty = std::map>>; -using mapIndexOptimizedExpr_ty = std::map, std::vector>>; - -class ExprOptimizer { -private: - ExprHashMap> cacheExprOptimized; - ExprHashSet cacheExprUnapplicable; - ExprHashMap> 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, Expr::Width>> &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 /* KLEE_ARRAYEXPROPTIMIZER_H */ diff --git a/lib/Expr/ArrayExprRewriter.cpp b/lib/Expr/ArrayExprRewriter.cpp index 8306e20a..32851679 100644 --- a/lib/Expr/ArrayExprRewriter.cpp +++ b/lib/Expr/ArrayExprRewriter.cpp @@ -7,18 +7,19 @@ // //===----------------------------------------------------------------------===// -#include "ArrayExprRewriter.h" +#include "klee/Expr/ArrayExprRewriter.h" + +#include "klee/Expr/ArrayExprVisitor.h" +#include "klee/util/BitArray.h" -#include -#include #include #include + +#include +#include #include #include -#include "ArrayExprVisitor.h" -#include "klee/util/BitArray.h" - using namespace klee; ref diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h deleted file mode 100644 index 098cb0a6..00000000 --- a/lib/Expr/ArrayExprRewriter.h +++ /dev/null @@ -1,47 +0,0 @@ -//===-- 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 KLEE_ARRAYEXPRREWRITER_H -#define KLEE_ARRAYEXPRREWRITER_H - -#include -#include -#include - -#include "klee/Expr/Expr.h" -#include "klee/util/Ref.h" - -namespace klee { - -using array2idx_ty = std::map>>; -using mapIndexOptimizedExpr_ty = std::map, std::vector>>; - -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 /* KLEE_ARRAYEXPRREWRITER_H */ diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp index dd82c4d6..d3119754 100644 --- a/lib/Expr/ArrayExprVisitor.cpp +++ b/lib/Expr/ArrayExprVisitor.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "ArrayExprVisitor.h" +#include "klee/Expr/ArrayExprVisitor.h" #include "klee/Support/ErrorHandling.h" diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h deleted file mode 100644 index 28f485d9..00000000 --- a/lib/Expr/ArrayExprVisitor.h +++ /dev/null @@ -1,129 +0,0 @@ -//===-- 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/Expr/ExprBuilder.h" -#include "klee/Expr/ExprHashMap.h" -#include "klee/Expr/ExprVisitor.h" -#include "klee/Solver/SolverCmdLine.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: - using bindings_ty = std::map>>; - bindings_ty &arrays; - // Avoids adding the same index twice - std::unordered_set addedIndexes; - bool incompatible; - -protected: - Action visitConcat(const ConcatExpr &) override; - Action visitRead(const ReadExpr &) override; - -public: - explicit ConstantArrayExprVisitor(bindings_ty &_arrays) - : arrays(_arrays), incompatible(false) {} - inline bool isIncompatible() { return incompatible; } -}; - -class IndexCompatibilityExprVisitor : public ExprVisitor { -private: - bool compatible{true}; - bool inner{false}; - -protected: - Action visitRead(const ReadExpr &) override; - Action visitURem(const URemExpr &) override; - Action visitSRem(const SRemExpr &) override; - Action visitOr(const OrExpr &) override; - -public: - IndexCompatibilityExprVisitor() = default; - - 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 &) override; - Action visitMul(const MulExpr &) override; - -public: - explicit 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, Expr::Width>> &readInfo; - bool symbolic; - bool incompatible; - - Action inspectRead(ref hash, Expr::Width width, const ReadExpr &); - -protected: - Action visitConcat(const ConcatExpr &) override; - Action visitRead(const ReadExpr &) override; - -public: - ArrayReadExprVisitor( - std::vector &_reads, - std::map, 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: - ExprHashMap> optimized; - -protected: - Action visitConcat(const ConcatExpr &) override; - Action visitRead(const ReadExpr &re) override; - -public: - explicit ArrayValueOptReplaceVisitor(ExprHashMap> &_optimized, - bool recursive = true) - : ExprVisitor(recursive), optimized(_optimized) {} -}; -} // namespace klee - -#endif /* KLEE_ARRAYEXPRVISITOR_H */ diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp index 0301b702..e7d2eb61 100644 --- a/lib/Expr/AssignmentGenerator.cpp +++ b/lib/Expr/AssignmentGenerator.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "AssignmentGenerator.h" +#include "klee/Expr/AssignmentGenerator.h" #include "klee/Expr/Assignment.h" #include "klee/Support/ErrorHandling.h" diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h deleted file mode 100644 index 173b863e..00000000 --- a/lib/Expr/AssignmentGenerator.h +++ /dev/null @@ -1,59 +0,0 @@ -//===-- 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 "klee/Expr/Expr.h" -#include "klee/util/Ref.h" - -#include - -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 /* KLEE_ASSIGNMENTGENERATOR_H */ diff --git a/unittests/Expr/ArrayExprTest.cpp b/unittests/Expr/ArrayExprTest.cpp index 47375abd..c7f3806a 100644 --- a/unittests/Expr/ArrayExprTest.cpp +++ b/unittests/Expr/ArrayExprTest.cpp @@ -8,14 +8,16 @@ //===----------------------------------------------------------------------===// #include "gtest/gtest.h" -#include -#include "../../lib/Expr/ArrayExprOptimizer.h" #include "klee/Expr/ArrayCache.h" +#include "klee/Expr/ArrayExprOptimizer.h" #include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" + #include +#include + using namespace klee; namespace klee { extern llvm::cl::opt OptimizeArray; -- cgit 1.4.1