From 4d57a5a829124106a4ef81e5131a50d1e7caed7f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 22 Feb 2016 19:10:39 +0000 Subject: Move Array constructor out of ``Expr.h`` and into ``Expr.cpp``. The implementation of the constructor calls a method on a ``ConstantExpr`` which means the type must be complete (i.e. a forward declaration of ``ConstantExpr`` is insufficient) which creates an unnecessary ordering Dependency in ``Expr.h``. --- include/klee/Expr.h | 19 +++---------------- lib/Expr/Expr.cpp | 18 ++++++++++++++++++ 2 files changed, 21 insertions(+), 16 deletions(-) diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 731aa446..2f24ffa4 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -636,22 +636,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 *constantValuesBegin = 0, - const ref *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 *it = constantValuesBegin; - it != constantValuesEnd; ++it) - assert((*it)->getWidth() == getRange() && - "Invalid initial constant value!"); -#endif //NDEBUG - } + const ref *constantValuesBegin = 0, + const ref *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8); public: bool isSymbolicArray() const { return constantValues.empty(); } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 2c64aff4..ccd757af 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -483,6 +483,24 @@ ref NotOptimizedExpr::create(ref src) { extern "C" void vc_DeleteExpr(void*); +Array::Array(const std::string &_name, uint64_t _size, + const ref *constantValuesBegin, + const ref *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 *it = constantValuesBegin; + it != constantValuesEnd; ++it) + assert((*it)->getWidth() == getRange() && + "Invalid initial constant value!"); +#endif // NDEBUG +} + Array::~Array() { } -- cgit 1.4.1 From c75ee65f632d7ee0e810a612ea100aa1b0e3f418 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 22 Feb 2016 19:31:08 +0000 Subject: Make the declaration of ``ConstantExpr`` the last declared ``Expr`` sub-class rather than the first. Whilst I'm here clang-format the moved code. The motivation for this is that ``ConstantExpr`` may need to refer to a type that cannot be forward declared (e.g. some kind of enum) in the other ``Expr`` sub-classes. For example if an Expr sub-class is ever introduced that has contains an enum that is used for its constructor then the previous ordering would prevent a Constant evaluation method (e.g. ``ConstantExpr::MyNewExprType(const ref &RHS, MyNewType::SpecialEnum p)``) from being implemented because the ``MyNewType::SpecialEnum`` type has not yet been declared. --- include/klee/Expr.h | 308 ++++++++++++++++++++++++++-------------------------- 1 file changed, 151 insertions(+), 157 deletions(-) diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 2f24ffa4..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 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(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 rebuild(ref kids[]) const { - assert(0 && "rebuild() on ConstantExpr"); - return const_cast(this); - } - - virtual unsigned computeHash(); - - static ref fromMemory(void *address, Width w); - void toMemory(void *address); - - static ref alloc(const llvm::APInt &v) { - ref r(new ConstantExpr(v)); - r->computeHash(); - return r; - } - - static ref alloc(const llvm::APFloat &f) { - return alloc(f.bitcastToAPInt()); - } - - static ref alloc(uint64_t v, Width w) { - return alloc(llvm::APInt(w, v)); - } - - static ref 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 Concat(const ref &RHS); - ref Extract(unsigned offset, Width W); - ref ZExt(Width W); - ref SExt(Width W); - ref Add(const ref &RHS); - ref Sub(const ref &RHS); - ref Mul(const ref &RHS); - ref UDiv(const ref &RHS); - ref SDiv(const ref &RHS); - ref URem(const ref &RHS); - ref SRem(const ref &RHS); - ref And(const ref &RHS); - ref Or(const ref &RHS); - ref Xor(const ref &RHS); - ref Shl(const ref &RHS); - ref LShr(const ref &RHS); - ref AShr(const ref &RHS); - - // Comparisons return a constant expression of width 1. - - ref Eq(const ref &RHS); - ref Ne(const ref &RHS); - ref Ult(const ref &RHS); - ref Ule(const ref &RHS); - ref Ugt(const ref &RHS); - ref Uge(const ref &RHS); - ref Slt(const ref &RHS); - ref Sle(const ref &RHS); - ref Sgt(const ref &RHS); - ref Sge(const ref &RHS); - - ref Neg(); - ref Not(); -}; - - // Utility classes class NonConstantExpr : public Expr { @@ -1089,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 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(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 rebuild(ref kids[]) const { + assert(0 && "rebuild() on ConstantExpr"); + return const_cast(this); + } + + virtual unsigned computeHash(); + + static ref fromMemory(void *address, Width w); + void toMemory(void *address); + + static ref alloc(const llvm::APInt &v) { + ref r(new ConstantExpr(v)); + r->computeHash(); + return r; + } + + static ref alloc(const llvm::APFloat &f) { + return alloc(f.bitcastToAPInt()); + } + + static ref alloc(uint64_t v, Width w) { + return alloc(llvm::APInt(w, v)); + } + + static ref 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 Concat(const ref &RHS); + ref Extract(unsigned offset, Width W); + ref ZExt(Width W); + ref SExt(Width W); + ref Add(const ref &RHS); + ref Sub(const ref &RHS); + ref Mul(const ref &RHS); + ref UDiv(const ref &RHS); + ref SDiv(const ref &RHS); + ref URem(const ref &RHS); + ref SRem(const ref &RHS); + ref And(const ref &RHS); + ref Or(const ref &RHS); + ref Xor(const ref &RHS); + ref Shl(const ref &RHS); + ref LShr(const ref &RHS); + ref AShr(const ref &RHS); + + // Comparisons return a constant expression of width 1. + + ref Eq(const ref &RHS); + ref Ne(const ref &RHS); + ref Ult(const ref &RHS); + ref Ule(const ref &RHS); + ref Ugt(const ref &RHS); + ref Uge(const ref &RHS); + ref Slt(const ref &RHS); + ref Sle(const ref &RHS); + ref Sgt(const ref &RHS); + ref Sge(const ref &RHS); + + ref Neg(); + ref Not(); +}; + // Implementations inline bool Expr::isZero() const { -- cgit 1.4.1 From 7f67a03988b6c0c5976d8b0aceb5406fd858c216 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 22 Feb 2016 19:13:12 +0000 Subject: Remove stray STP function declaration. --- lib/Expr/Expr.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index ccd757af..182093b9 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -481,8 +481,6 @@ ref NotOptimizedExpr::create(ref src) { /***/ -extern "C" void vc_DeleteExpr(void*); - Array::Array(const std::string &_name, uint64_t _size, const ref *constantValuesBegin, const ref *constantValuesEnd, Expr::Width _domain, -- cgit 1.4.1 From 238998f8e17b554d0c28931a61271619310a098f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 23 Feb 2016 17:21:42 +0000 Subject: Move ``Assignment::dump()`` into its own implementation file so that it's possible to call it from gdb. --- include/klee/util/Assignment.h | 10 +--------- lib/Expr/Assigment.cpp | 21 +++++++++++++++++++++ 2 files changed, 22 insertions(+), 9 deletions(-) create mode 100644 lib/Expr/Assigment.cpp 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 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(); jname << "\n["; + for (int j = 0, k = (*i).second.size(); j < k; ++j) + llvm::errs() << (int)(*i).second[j] << ","; + llvm::errs() << "]\n"; + } +} +} -- cgit 1.4.1 From 9bc1d11162403e331e99d5d0494feab70ace6fbc Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 23 Feb 2016 17:25:07 +0000 Subject: When calling ``Assignment::dump()`` if there are no bindings emit a message stating this. --- lib/Expr/Assigment.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp index 900c6d10..635362d4 100644 --- a/lib/Expr/Assigment.cpp +++ b/lib/Expr/Assigment.cpp @@ -10,6 +10,10 @@ 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["; -- cgit 1.4.1