diff options
| -rw-r--r-- | include/klee/Expr.h | 327 | ||||
| -rw-r--r-- | include/klee/util/Assignment.h | 10 | ||||
| -rw-r--r-- | lib/Expr/Assigment.cpp | 25 | ||||
| -rw-r--r-- | lib/Expr/Expr.cpp | 18 |
4 files changed, 197 insertions, 183 deletions
diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 731aa446..9ad1b49a 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -324,163 +324,6 @@ inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kin return os; } -// Terminal Exprs - -class ConstantExpr : public Expr { -public: - static const Kind kind = Constant; - static const unsigned numKids = 0; - -private: - llvm::APInt value; - - ConstantExpr(const llvm::APInt &v) : value(v) {} - -public: - ~ConstantExpr() {} - - Width getWidth() const { return value.getBitWidth(); } - Kind getKind() const { return Constant; } - - unsigned getNumKids() const { return 0; } - ref<Expr> getKid(unsigned i) const { return 0; } - - /// getAPValue - Return the arbitrary precision value directly. - /// - /// Clients should generally not use the APInt value directly and instead use - /// native ConstantExpr APIs. - const llvm::APInt &getAPValue() const { return value; } - - /// getZExtValue - Returns the constant value zero extended to the - /// return type of this method. - /// - ///\param bits - optional parameter that can be used to check that the - ///number of bits used by this constant is <= to the parameter - ///value. This is useful for checking that type casts won't truncate - ///useful bits. - /// - /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8); - uint64_t getZExtValue(unsigned bits = 64) const { - assert(getWidth() <= bits && "Value may be out of range!"); - return value.getZExtValue(); - } - - /// getLimitedValue - If this value is smaller than the specified limit, - /// return it, otherwise return the limit value. - uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const { - return value.getLimitedValue(Limit); - } - - /// toString - Return the constant value as a string - /// \param Res specifies the string for the result to be placed in - /// \param radix specifies the base (e.g. 2,10,16). The default is base 10 - void toString(std::string &Res, unsigned radix=10) const; - - - - int compareContents(const Expr &b) const { - const ConstantExpr &cb = static_cast<const ConstantExpr&>(b); - if (getWidth() != cb.getWidth()) - return getWidth() < cb.getWidth() ? -1 : 1; - if (value == cb.value) - return 0; - return value.ult(cb.value) ? -1 : 1; - } - - virtual ref<Expr> rebuild(ref<Expr> kids[]) const { - assert(0 && "rebuild() on ConstantExpr"); - return const_cast<ConstantExpr*>(this); - } - - virtual unsigned computeHash(); - - static ref<Expr> fromMemory(void *address, Width w); - void toMemory(void *address); - - static ref<ConstantExpr> alloc(const llvm::APInt &v) { - ref<ConstantExpr> r(new ConstantExpr(v)); - r->computeHash(); - return r; - } - - static ref<ConstantExpr> alloc(const llvm::APFloat &f) { - return alloc(f.bitcastToAPInt()); - } - - static ref<ConstantExpr> alloc(uint64_t v, Width w) { - return alloc(llvm::APInt(w, v)); - } - - static ref<ConstantExpr> create(uint64_t v, Width w) { - assert(v == bits64::truncateToNBits(v, w) && - "invalid constant"); - return alloc(v, w); - } - - static bool classof(const Expr *E) { - return E->getKind() == Expr::Constant; - } - static bool classof(const ConstantExpr *) { return true; } - - /* Utility Functions */ - - /// isZero - Is this a constant zero. - bool isZero() const { return getAPValue().isMinValue(); } - - /// isOne - Is this a constant one. - bool isOne() const { return getLimitedValue() == 1; } - - /// isTrue - Is this the true expression. - bool isTrue() const { - return (getWidth() == Expr::Bool && value.getBoolValue()==true); - } - - /// isFalse - Is this the false expression. - bool isFalse() const { - return (getWidth() == Expr::Bool && value.getBoolValue()==false); - } - - /// isAllOnes - Is this constant all ones. - bool isAllOnes() const { return getAPValue().isAllOnesValue(); } - - /* Constant Operations */ - - ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Extract(unsigned offset, Width W); - ref<ConstantExpr> ZExt(Width W); - ref<ConstantExpr> SExt(Width W); - ref<ConstantExpr> Add(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sub(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Mul(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> UDiv(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> SDiv(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> URem(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> SRem(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> And(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Or(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Xor(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS); - - // Comparisons return a constant expression of width 1. - - ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ule(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Ugt(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Uge(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Slt(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS); - ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS); - - ref<ConstantExpr> Neg(); - ref<ConstantExpr> Not(); -}; - - // Utility classes class NonConstantExpr : public Expr { @@ -636,22 +479,9 @@ private: /// not parse correctly since two arrays with the same name cannot be /// distinguished once printed. Array(const std::string &_name, uint64_t _size, - const ref<ConstantExpr> *constantValuesBegin = 0, - const ref<ConstantExpr> *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) - : name(_name), size(_size), domain(_domain), range(_range), - constantValues(constantValuesBegin, constantValuesEnd) { - - assert((isSymbolicArray() || constantValues.size() == size) && - "Invalid size for constant array!"); - computeHash(); -#ifndef NDEBUG - for (const ref<ConstantExpr> *it = constantValuesBegin; - it != constantValuesEnd; ++it) - assert((*it)->getWidth() == getRange() && - "Invalid initial constant value!"); -#endif //NDEBUG - } + const ref<ConstantExpr> *constantValuesBegin = 0, + const ref<ConstantExpr> *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8); public: bool isSymbolicArray() const { return constantValues.empty(); } @@ -1102,6 +932,157 @@ COMPARISON_EXPR_CLASS(Sle) COMPARISON_EXPR_CLASS(Sgt) COMPARISON_EXPR_CLASS(Sge) +// Terminal Exprs + +class ConstantExpr : public Expr { +public: + static const Kind kind = Constant; + static const unsigned numKids = 0; + +private: + llvm::APInt value; + + ConstantExpr(const llvm::APInt &v) : value(v) {} + +public: + ~ConstantExpr() {} + + Width getWidth() const { return value.getBitWidth(); } + Kind getKind() const { return Constant; } + + unsigned getNumKids() const { return 0; } + ref<Expr> getKid(unsigned i) const { return 0; } + + /// getAPValue - Return the arbitrary precision value directly. + /// + /// Clients should generally not use the APInt value directly and instead use + /// native ConstantExpr APIs. + const llvm::APInt &getAPValue() const { return value; } + + /// getZExtValue - Returns the constant value zero extended to the + /// return type of this method. + /// + ///\param bits - optional parameter that can be used to check that the + /// number of bits used by this constant is <= to the parameter + /// value. This is useful for checking that type casts won't truncate + /// useful bits. + /// + /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8); + uint64_t getZExtValue(unsigned bits = 64) const { + assert(getWidth() <= bits && "Value may be out of range!"); + return value.getZExtValue(); + } + + /// getLimitedValue - If this value is smaller than the specified limit, + /// return it, otherwise return the limit value. + uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const { + return value.getLimitedValue(Limit); + } + + /// toString - Return the constant value as a string + /// \param Res specifies the string for the result to be placed in + /// \param radix specifies the base (e.g. 2,10,16). The default is base 10 + void toString(std::string &Res, unsigned radix = 10) const; + + int compareContents(const Expr &b) const { + const ConstantExpr &cb = static_cast<const ConstantExpr &>(b); + if (getWidth() != cb.getWidth()) + return getWidth() < cb.getWidth() ? -1 : 1; + if (value == cb.value) + return 0; + return value.ult(cb.value) ? -1 : 1; + } + + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + assert(0 && "rebuild() on ConstantExpr"); + return const_cast<ConstantExpr *>(this); + } + + virtual unsigned computeHash(); + + static ref<Expr> fromMemory(void *address, Width w); + void toMemory(void *address); + + static ref<ConstantExpr> alloc(const llvm::APInt &v) { + ref<ConstantExpr> r(new ConstantExpr(v)); + r->computeHash(); + return r; + } + + static ref<ConstantExpr> alloc(const llvm::APFloat &f) { + return alloc(f.bitcastToAPInt()); + } + + static ref<ConstantExpr> alloc(uint64_t v, Width w) { + return alloc(llvm::APInt(w, v)); + } + + static ref<ConstantExpr> create(uint64_t v, Width w) { + assert(v == bits64::truncateToNBits(v, w) && "invalid constant"); + return alloc(v, w); + } + + static bool classof(const Expr *E) { return E->getKind() == Expr::Constant; } + static bool classof(const ConstantExpr *) { return true; } + + /* Utility Functions */ + + /// isZero - Is this a constant zero. + bool isZero() const { return getAPValue().isMinValue(); } + + /// isOne - Is this a constant one. + bool isOne() const { return getLimitedValue() == 1; } + + /// isTrue - Is this the true expression. + bool isTrue() const { + return (getWidth() == Expr::Bool && value.getBoolValue() == true); + } + + /// isFalse - Is this the false expression. + bool isFalse() const { + return (getWidth() == Expr::Bool && value.getBoolValue() == false); + } + + /// isAllOnes - Is this constant all ones. + bool isAllOnes() const { return getAPValue().isAllOnesValue(); } + + /* Constant Operations */ + + ref<ConstantExpr> Concat(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Extract(unsigned offset, Width W); + ref<ConstantExpr> ZExt(Width W); + ref<ConstantExpr> SExt(Width W); + ref<ConstantExpr> Add(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sub(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Mul(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> UDiv(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> SDiv(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> URem(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> SRem(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> And(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Or(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Xor(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Shl(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> LShr(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> AShr(const ref<ConstantExpr> &RHS); + + // Comparisons return a constant expression of width 1. + + ref<ConstantExpr> Eq(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ne(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ult(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ule(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Ugt(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Uge(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Slt(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sle(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sgt(const ref<ConstantExpr> &RHS); + ref<ConstantExpr> Sge(const ref<ConstantExpr> &RHS); + + ref<ConstantExpr> Neg(); + ref<ConstantExpr> Not(); +}; + // Implementations inline bool Expr::isZero() const { diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index e7478d33..5d8aa1ab 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -49,15 +49,7 @@ namespace klee { template<typename InputIterator> bool satisfies(InputIterator begin, InputIterator end); - - void dump() { - for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e; ++i) { - llvm::errs() << (*i).first->name << "\n["; - for (int j = 0, k =(*i).second.size(); j<k; ++j ) - llvm::errs() << (int)(*i).second[j] << ","; - llvm::errs() << "]\n"; - } - } + void dump(); }; class AssignmentEvaluator : public ExprEvaluator { diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp new file mode 100644 index 00000000..635362d4 --- /dev/null +++ b/lib/Expr/Assigment.cpp @@ -0,0 +1,25 @@ +//===-- Assignment.cpp ----------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// +#include "klee/util/Assignment.h" +namespace klee { + +void Assignment::dump() { + if (bindings.size() == 0) { + llvm::errs() << "No bindings\n"; + return; + } + for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e; + ++i) { + llvm::errs() << (*i).first->name << "\n["; + for (int j = 0, k = (*i).second.size(); j < k; ++j) + llvm::errs() << (int)(*i).second[j] << ","; + llvm::errs() << "]\n"; + } +} +} diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 2c64aff4..182093b9 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -481,7 +481,23 @@ ref<Expr> NotOptimizedExpr::create(ref<Expr> src) { /***/ -extern "C" void vc_DeleteExpr(void*); +Array::Array(const std::string &_name, uint64_t _size, + const ref<ConstantExpr> *constantValuesBegin, + const ref<ConstantExpr> *constantValuesEnd, Expr::Width _domain, + Expr::Width _range) + : name(_name), size(_size), domain(_domain), range(_range), + constantValues(constantValuesBegin, constantValuesEnd) { + + assert((isSymbolicArray() || constantValues.size() == size) && + "Invalid size for constant array!"); + computeHash(); +#ifndef NDEBUG + for (const ref<ConstantExpr> *it = constantValuesBegin; + it != constantValuesEnd; ++it) + assert((*it)->getWidth() == getRange() && + "Invalid initial constant value!"); +#endif // NDEBUG +} Array::~Array() { } |