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. --- include/klee/ArrayExprOptimizer.h | 69 ----------------- include/klee/ArrayExprRewriter.h | 47 ------------ include/klee/AssignmentGenerator.h | 59 --------------- include/klee/util/ArrayExprVisitor.h | 143 ----------------------------------- 4 files changed, 318 deletions(-) delete mode 100644 include/klee/ArrayExprOptimizer.h delete mode 100644 include/klee/ArrayExprRewriter.h delete mode 100644 include/klee/AssignmentGenerator.h delete mode 100644 include/klee/util/ArrayExprVisitor.h (limited to 'include') diff --git a/include/klee/ArrayExprOptimizer.h b/include/klee/ArrayExprOptimizer.h deleted file mode 100644 index aafe1d27..00000000 --- a/include/klee/ArrayExprOptimizer.h +++ /dev/null @@ -1,69 +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_EXPROPTIMIZER_H -#define KLEE_EXPROPTIMIZER_H - -#include -#include -#include -#include -#include -#include - -#include "Expr.h" -#include "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; -}; -} - -#endif diff --git a/include/klee/ArrayExprRewriter.h b/include/klee/ArrayExprRewriter.h deleted file mode 100644 index 2b6c78b4..00000000 --- a/include/klee/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 LIB_EXPRREWRITER_H_ -#define LIB_EXPRREWRITER_H_ - -#include -#include -#include - -#include "Expr.h" -#include "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); -}; -} - -#endif /* LIB_EXPRREWRITER_H_ */ diff --git a/include/klee/AssignmentGenerator.h b/include/klee/AssignmentGenerator.h deleted file mode 100644 index 404c8632..00000000 --- a/include/klee/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 - -#include "Expr.h" -#include "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); -}; -} - -#endif diff --git a/include/klee/util/ArrayExprVisitor.h b/include/klee/util/ArrayExprVisitor.h deleted file mode 100644 index d8c64c2d..00000000 --- a/include/klee/util/ArrayExprVisitor.h +++ /dev/null @@ -1,143 +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/util/ExprVisitor.h" -#include "klee/ExprBuilder.h" -#include "klee/CommandLine.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; } -}; -} - -#endif -- cgit v1.2.3