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 ----------------------------------- lib/Core/Executor.cpp | 2 +- lib/Core/Executor.h | 6 +- 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 +++++++++++++++ 14 files changed, 325 insertions(+), 330 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 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 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 diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 9e53c340..ecebe916 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -24,7 +24,6 @@ #include "ExecutorTimerInfo.h" -#include "klee/ArrayExprOptimizer.h" #include "klee/ExecutionState.h" #include "klee/Expr.h" #include "klee/Interpreter.h" @@ -50,6 +49,7 @@ #include "klee/Internal/System/MemoryUsage.h" #include "klee/SolverStats.h" +#include "../Expr/ArrayExprOptimizer.h" #include "llvm/ADT/SmallPtrSet.h" #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Attributes.h" diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 6a640905..d9e20f1e 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -16,7 +16,6 @@ #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" @@ -26,10 +25,11 @@ #include "llvm/ADT/Twine.h" -#include -#include +#include "../Expr/ArrayExprOptimizer.h" #include #include +#include +#include struct KTest; 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