From ab2cd9ddff027797d47a2159ff52af9429ce9333 Mon Sep 17 00:00:00 2001 From: Aleksei Babushkin Date: Wed, 11 Oct 2023 20:05:54 +0300 Subject: [PATCH] [wip] Uninitialized Memory --- include/klee/ADT/Ref.h | 8 +- include/klee/ADT/SparseStorage.h | 71 ++-- include/klee/Expr/Expr.h | 5 +- include/klee/Expr/Parser/Lexer.h | 2 + include/klee/Expr/SourceBuilder.h | 14 +- include/klee/Expr/SymbolicSource.h | 133 +++++--- include/klee/Module/KInstruction.h | 77 ++++- include/klee/Module/KModule.h | 2 +- include/klee/Support/PrintContext.h | 4 + lib/ADT/SparseStorage.cpp | 73 ++++- lib/Core/AddressSpace.cpp | 21 +- lib/Core/AddressSpace.h | 10 +- lib/Core/Executor.cpp | 103 ++++-- lib/Core/Executor.h | 2 +- lib/Core/Memory.cpp | 306 +++++++----------- lib/Core/Memory.h | 53 +-- lib/Core/SpecialFunctionHandler.cpp | 11 +- lib/Expr/ArrayExprOptimizer.cpp | 8 +- lib/Expr/Assignment.cpp | 6 +- lib/Expr/Expr.cpp | 47 +-- lib/Expr/ExprEvaluator.cpp | 9 +- lib/Expr/ExprPPrinter.cpp | 11 +- lib/Expr/ExprSMTLIBPrinter.cpp | 10 +- lib/Expr/Lexer.cpp | 9 + lib/Expr/Parser.cpp | 53 +-- lib/Expr/SourceBuilder.cpp | 23 +- lib/Expr/SymbolicSource.cpp | 29 +- lib/Module/KInstruction.cpp | 8 + lib/Module/KModule.cpp | 2 +- lib/Solver/FastCexSolver.cpp | 15 +- lib/Solver/STPBuilder.cpp | 18 +- lib/Solver/Z3Builder.cpp | 42 ++- lib/Solver/Z3Solver.cpp | 6 +- test/Expr/Evaluate.kquery | 2 +- test/Expr/print-smt-let.kquery | 10 +- test/Expr/print-smt-named.kquery | 10 +- test/Expr/print-smt-none.kquery | 10 +- .../SymbolicSizes/UninitializedMemory.c | 25 ++ test/Feature/UninitializedConstantMemory.c | 30 ++ .../2023-08-28-invalid-pointer-dereference.c | 22 ++ 40 files changed, 811 insertions(+), 489 deletions(-) create mode 100644 test/Feature/SymbolicSizes/UninitializedMemory.c create mode 100644 test/Feature/UninitializedConstantMemory.c create mode 100644 test/regression/2023-08-28-invalid-pointer-dereference.c diff --git a/include/klee/ADT/Ref.h b/include/klee/ADT/Ref.h index 008580cc7e0..c09fd13ba75 100644 --- a/include/klee/ADT/Ref.h +++ b/include/klee/ADT/Ref.h @@ -205,7 +205,13 @@ template class ref { // assumes non-null arguments bool equals(const ref &rhs) const { - assert(!isNull() && !rhs.isNull() && "Invalid call to compare()"); + if (isNull() && rhs.isNull()) { + return true; + } + if (isNull() || rhs.isNull()) { + return false; + } + // assert(!isNull() && !rhs.isNull() && "Invalid call to compare()"); return get()->equals(*rhs.get()); } diff --git a/include/klee/ADT/SparseStorage.h b/include/klee/ADT/SparseStorage.h index c3c81fd5642..0283d4cfc74 100644 --- a/include/klee/ADT/SparseStorage.h +++ b/include/klee/ADT/SparseStorage.h @@ -1,6 +1,8 @@ #ifndef KLEE_SPARSESTORAGE_H #define KLEE_SPARSESTORAGE_H +#include "klee/ADT/Ref.h" +#include #include #include #include @@ -12,13 +14,18 @@ namespace llvm { class raw_ostream; }; + namespace klee { +enum class Density { + Sparse, + Dense, +}; + template class SparseStorage { private: std::unordered_map internalStorage; ValueType defaultValue; - size_t rangeSize = 0; bool contains(size_t key) const { return internalStorage.count(key) != 0; } @@ -26,17 +33,28 @@ template class SparseStorage { SparseStorage(const ValueType &defaultValue = ValueType()) : defaultValue(defaultValue) {} + SparseStorage(const std::unordered_map &internalStorage, + const ValueType &defaultValue) + : defaultValue(defaultValue) { + for (auto &[index, value] : internalStorage) { + store(index, value); + } + } + SparseStorage(const std::vector &values, const ValueType &defaultValue = ValueType()) : defaultValue(defaultValue) { for (size_t idx = 0; idx < values.size(); ++idx) { - internalStorage[idx] = values[idx]; + store(idx, values[idx]); } } void store(size_t idx, const ValueType &value) { + if (value == defaultValue) { + internalStorage.erase(idx); + } else { internalStorage[idx] = value; - rangeSize = std::max(rangeSize, idx + 1); + } } template @@ -52,12 +70,15 @@ template class SparseStorage { } size_t sizeOfSetRange() const { - return rangeSize; + size_t sizeOfRange = 0; + for (auto i : internalStorage) { + sizeOfRange = std::max(i.first, sizeOfRange); + } + return sizeOfRange; } bool operator==(const SparseStorage &another) const { - return defaultValue == another.defaultValue && - compare(another) == 0; + return defaultValue == another.defaultValue && compare(another) == 0; } bool operator!=(const SparseStorage &another) const { @@ -73,46 +94,56 @@ template class SparseStorage { } int compare(const SparseStorage &other) const { - std::map thisMap; - std::map otherMap; - for (auto i : internalStorage) { - thisMap.insert(i); - } - for (auto i : other.internalStorage) { - otherMap.insert(i); - } - if (thisMap == otherMap) { + auto ordered = calculateOrderedStorage(); + auto otherOrdered = other.calculateOrderedStorage(); + + if (ordered == otherOrdered) { return 0; } else { - return thisMap < otherMap ? -1 : 1; + return ordered < otherOrdered ? -1 : 1; } } + std::map calculateOrderedStorage() const { + std::map ordered; + for (const auto &i : internalStorage) { + ordered.insert(i); + } + return ordered; + } + + std::vector getFirstNIndexes(size_t n) const { + std::vector vectorized(n); + for (size_t i = 0; i < n; i++) { + vectorized[i] = load(i); + } + return vectorized; + } + const std::unordered_map &storage() const { return internalStorage; }; + const ValueType &defaultV() const { return defaultValue; }; void reset() { internalStorage.clear(); - rangeSize = 0; } void reset(ValueType newDefault) { defaultValue = newDefault; internalStorage.clear(); - rangeSize = 0; } // Specialized for unsigned char in .cpp - void print(llvm::raw_ostream &os) const; + void print(llvm::raw_ostream &os, Density) const; }; template SparseStorage sparseBytesFromValue(const U &value) { const unsigned char *valueUnsignedCharIterator = reinterpret_cast(&value); - SparseStorage result(sizeof(value)); + SparseStorage result; result.store(0, valueUnsignedCharIterator, valueUnsignedCharIterator + sizeof(value)); return result; diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index ab6826e25d9..eea90a23fee 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -629,10 +629,7 @@ class Array { public: bool isSymbolicArray() const { return !isConstantArray(); } - bool isConstantArray() const { - return isa(source) || - isa(source); - } + bool isConstantArray() const; const std::string getName() const { return source->toString(); } const std::string getIdentifier() const { diff --git a/include/klee/Expr/Parser/Lexer.h b/include/klee/Expr/Parser/Lexer.h index 8b3fe53a306..33bb277ea87 100644 --- a/include/klee/Expr/Parser/Lexer.h +++ b/include/klee/Expr/Parser/Lexer.h @@ -32,6 +32,8 @@ struct Token { KWFalse, ///< 'false' KWQuery, ///< 'query' KWPath, ///< 'path' + KWDV, ///< 'DV' + KWNull, ///< 'null' KWReserved, ///< fp[0-9]+([.].*)?, i[0-9]+ KWSymbolic, ///< 'symbolic' KWTrue, ///< 'true' diff --git a/include/klee/Expr/SourceBuilder.h b/include/klee/Expr/SourceBuilder.h index 7b57e2f8c9f..2c81d7d0a73 100644 --- a/include/klee/Expr/SourceBuilder.h +++ b/include/klee/Expr/SourceBuilder.h @@ -2,6 +2,7 @@ #define KLEE_SOURCEBUILDER_H #include "klee/ADT/Ref.h" +#include "klee/ADT/SparseStorage.h" #include "klee/Expr/SymbolicSource.h" #include "klee/Module/KModule.h" @@ -12,10 +13,14 @@ class SourceBuilder { SourceBuilder() = delete; static ref - constant(const std::vector> &constantValues); - static ref symbolicSizeConstant(unsigned defaultValue); - static ref symbolicSizeConstantAddress(unsigned defaultValue, - unsigned version); + constant(SparseStorage> constantValues); + + static ref uninitialized(unsigned version, + const KInstruction *allocSite); + static ref + symbolicSizeConstantAddress(unsigned version, + const KInstruction *allocSite, + ref size); static ref makeSymbolic(const std::string &name, unsigned version); static ref lazyInitializationAddress(ref pointer); @@ -27,6 +32,7 @@ class SourceBuilder { int _index, KModule *km); static ref value(const llvm::Value &_allocSite, int _index, KModule *km); + static ref global(const llvm::GlobalVariable &name); static ref irreproducible(const std::string &name); }; diff --git a/include/klee/Expr/SymbolicSource.h b/include/klee/Expr/SymbolicSource.h index be65580f7bd..5e93847f79a 100644 --- a/include/klee/Expr/SymbolicSource.h +++ b/include/klee/Expr/SymbolicSource.h @@ -3,12 +3,16 @@ #include "klee/ADT/Ref.h" +#include "klee/ADT/SparseStorage.h" +#include "klee/Module/KInstruction.h" #include "klee/Support/CompilerWarning.h" + DISABLE_WARNING_PUSH DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/ADT/StringExtras.h" #include "llvm/IR/Argument.h" #include "llvm/IR/Instruction.h" +#include "llvm/IR/GlobalVariable.h" DISABLE_WARNING_POP #include @@ -33,7 +37,8 @@ class SymbolicSource { enum Kind { Constant = 3, - SymbolicSizeConstant, + Uninitialied, + Global, SymbolicSizeConstantAddress, MakeSymbolic, LazyInitializationContent, @@ -61,26 +66,29 @@ class SymbolicSource { bool equals(const SymbolicSource &b) const; }; + class ConstantSource : public SymbolicSource { public: - /// constantValues - The constant initial values for this array, or empty for - /// a symbolic array. If non-empty, this size of this array is equivalent to - /// the array size. - const std::vector> constantValues; + const SparseStorage> constantValues; + + ConstantSource(SparseStorage> _constantValues) + : constantValues(std::move(_constantValues)) { + assert(constantValues.defaultV() && "Constant must be constant!"); + } - ConstantSource(const std::vector> &_constantValues) - : constantValues(_constantValues){}; Kind getKind() const override { return Kind::Constant; } - virtual std::string getName() const override { return "constant"; } - uint64_t size() const { return constantValues.size(); } + + std::string getName() const override { return "constant"; } static bool classof(const SymbolicSource *S) { return S->getKind() == Kind::Constant; } + static bool classof(const ConstantSource *) { return true; } - virtual unsigned computeHash() override; - virtual int internalCompare(const SymbolicSource &b) const override { + unsigned computeHash() override; + + int internalCompare(const SymbolicSource &b) const override { if (getKind() != b.getKind()) { return getKind() < b.getKind() ? -1 : 1; } @@ -92,43 +100,51 @@ class ConstantSource : public SymbolicSource { } }; -class SymbolicSizeConstantSource : public SymbolicSource { +class UninitializedSource : public SymbolicSource { public: - const unsigned defaultValue; - SymbolicSizeConstantSource(unsigned _defaultValue) - : defaultValue(_defaultValue) {} + const unsigned version; + const KInstruction *allocSite; - Kind getKind() const override { return Kind::SymbolicSizeConstant; } - virtual std::string getName() const override { - return "symbolicSizeConstant"; - } + UninitializedSource(unsigned version, const KInstruction *allocSite) + : version(version), allocSite(allocSite) {} + + Kind getKind() const override { return Kind::Uninitialied; } + + std::string getName() const override { return "uninitialized"; } static bool classof(const SymbolicSource *S) { - return S->getKind() == Kind::SymbolicSizeConstant; + return S->getKind() == Kind::Uninitialied; } - static bool classof(const SymbolicSizeConstantSource *) { return true; } - virtual unsigned computeHash() override; + static bool classof(const UninitializedSource *) { return true; } - virtual int internalCompare(const SymbolicSource &b) const override { + unsigned computeHash() override; + + int internalCompare(const SymbolicSource &b) const override { if (getKind() != b.getKind()) { return getKind() < b.getKind() ? -1 : 1; } - const SymbolicSizeConstantSource &ssb = - static_cast(b); - if (defaultValue != ssb.defaultValue) { - return defaultValue < ssb.defaultValue ? -1 : 1; + const UninitializedSource &ub = static_cast(b); + + if (version == ub.version && allocSite == ub.allocSite) { + return 0; } - return 0; + + return std::tie(version, allocSite) < std::tie(ub.version, ub.allocSite) + ? -1 + : 1; } }; class SymbolicSizeConstantAddressSource : public SymbolicSource { public: - const unsigned defaultValue; const unsigned version; - SymbolicSizeConstantAddressSource(unsigned _defaultValue, unsigned _version) - : defaultValue(_defaultValue), version(_version) {} + const KInstruction *allocSite; + ref size; + SymbolicSizeConstantAddressSource(unsigned _version, + const KInstruction *_allocSite, + ref _size) + : version(_version), allocSite(_allocSite), size(_size) {} Kind getKind() const override { return Kind::SymbolicSizeConstantAddress; } virtual std::string getName() const override { @@ -148,15 +164,17 @@ class SymbolicSizeConstantAddressSource : public SymbolicSource { if (getKind() != b.getKind()) { return getKind() < b.getKind() ? -1 : 1; } - const SymbolicSizeConstantAddressSource &ssb = + const SymbolicSizeConstantAddressSource &ub = static_cast(b); - if (defaultValue != ssb.defaultValue) { - return defaultValue < ssb.defaultValue ? -1 : 1; - } - if (version != ssb.version) { - return version < ssb.version ? -1 : 1; + + if (version == ub.version && allocSite == ub.allocSite && size == ub.size) { + return 0; } - return 0; + + return std::tie(version, allocSite, size) < + std::tie(ub.version, ub.allocSite, size) + ? -1 + : 1; } }; @@ -326,6 +344,45 @@ class InstructionSource : public ValueSource { virtual int internalCompare(const SymbolicSource &b) const override; }; +class GlobalSource : public SymbolicSource { +public: + const llvm::GlobalVariable &gv; + GlobalSource(const llvm::GlobalVariable &_gv) : gv(_gv) {} + + Kind getKind() const override { return Kind::Global; } + virtual std::string getName() const override { return "global"; } + + static bool classof(const SymbolicSource *S) { + return S->getKind() == Kind::Global; + } + static bool classof(const GlobalSource *) { return true; } + + virtual unsigned computeHash() override { + auto name = gv.getName(); + unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT); + for (unsigned i = 0, e = name.size(); i != e; ++i) { + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + name[i]; + } + hashValue = res; + return hashValue; + } + + virtual int internalCompare(const SymbolicSource &b) const override { + if (getKind() != b.getKind()) { + return getKind() < b.getKind() ? -1 : 1; + } + const GlobalSource &gb = + static_cast(b); + auto name = gv.getName(); + auto bName = gb.gv.getName(); + if (name != bName) { + return name < bName ? -1 : 1; + } + return 0; + } + +}; + class IrreproducibleSource : public SymbolicSource { public: const std::string name; diff --git a/include/klee/Module/KInstruction.h b/include/klee/Module/KInstruction.h index 5c64de152c6..2cffceffcda 100644 --- a/include/klee/Module/KInstruction.h +++ b/include/klee/Module/KInstruction.h @@ -13,7 +13,7 @@ #include "KModule.h" #include "klee/Config/Version.h" #include "klee/Support/CompilerWarning.h" - +#include "llvm/IR/Argument.h" DISABLE_WARNING_PUSH DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/DataTypes.h" @@ -31,10 +31,37 @@ namespace klee { class Executor; class KModule; struct KBlock; +struct KFunction; + +static const unsigned MAGIC_HASH_CONSTANT = 39; /// KInstruction - Intermediate instruction representation used /// during execution. struct KInstruction { + + struct Index { + unsigned long instID; + unsigned long blockID; + unsigned long funcID; + + bool operator==(const Index &other) const { + return std::tie(instID, blockID, funcID) == + std::tie(other.instID, other.blockID, other.funcID); + } + + bool operator<(const Index &other) const { + return std::tie(instID, blockID, funcID) < + std::tie(other.instID, other.blockID, other.funcID); + } + + unsigned hash() const { + unsigned res = instID; + res = res * MAGIC_HASH_CONSTANT + blockID; + res = res * MAGIC_HASH_CONSTANT + funcID; + return res; + } + }; + llvm::Instruction *inst; /// Value numbers for each operand. -1 is an invalid value, @@ -65,21 +92,69 @@ struct KInstruction { KInstruction() = delete; explicit KInstruction(const KInstruction &ki) = delete; virtual ~KInstruction(); + std::string getSourceLocation() const; [[nodiscard]] size_t getLine() const; [[nodiscard]] size_t getColumn() const; [[nodiscard]] std::string getSourceFilepath() const; + Index getID() const; [[nodiscard]] std::string getSourceLocationString() const; [[nodiscard]] std::string toString() const; + bool operator==(const KInstruction &other) const { + return getID() == other.getID(); + } [[nodiscard]] inline KBlock *getKBlock() const { return parent; } [[nodiscard]] inline KFunction *getKFunction() const { return getKBlock()->parent; } + bool operator<(const KInstruction &other) const { + return getID() < other.getID(); + } [[nodiscard]] inline KModule *getKModule() const { return getKFunction()->parent; } + + unsigned hash() const { + return getID().hash(); + } +}; + +struct KArgument { + + struct Index { + unsigned long argNo; + unsigned long funcID; + + bool operator==(const Index &other) const { + return std::tie(argNo, funcID) == std::tie(other.argNo, other.funcID); + } + + bool operator<(const Index &other) const { + return std::tie(argNo, funcID) < std::tie(other.argNo, other.funcID); + } + + unsigned hash() const { + unsigned res = argNo; + res = res * MAGIC_HASH_CONSTANT + funcID; + return res; + } + }; + + llvm::Argument *arg; + unsigned argNo; + KFunction *parent; + + Index getID() const; + + bool operator==(const KArgument &other) { return getID() == other.getID(); } + + bool operator<(const KArgument &other) { return getID() < other.getID(); } + + unsigned hash() { + return getID().hash(); + } }; struct KGEPInstruction : KInstruction { diff --git a/include/klee/Module/KModule.h b/include/klee/Module/KModule.h index 50949908b66..83cef2cce53 100644 --- a/include/klee/Module/KModule.h +++ b/include/klee/Module/KModule.h @@ -296,7 +296,7 @@ class KModule { /// expected by KLEE's Executor hold. void checkModule(); - KBlock *getKBlock(llvm::BasicBlock *bb); + KBlock *getKBlock(const llvm::BasicBlock *bb); bool inMainModule(const llvm::Function &f); diff --git a/include/klee/Support/PrintContext.h b/include/klee/Support/PrintContext.h index e397367683e..ae76119bce6 100644 --- a/include/klee/Support/PrintContext.h +++ b/include/klee/Support/PrintContext.h @@ -72,6 +72,10 @@ class PrintContext { return *this; } + llvm::raw_ostream &getStream() { + return os; + } + /// Pop the top off the indent stack /// \return The PrintContext object so the method is chainable PrintContext &popIndent() { diff --git a/lib/ADT/SparseStorage.cpp b/lib/ADT/SparseStorage.cpp index bdbd14c76b2..0c177a46265 100644 --- a/lib/ADT/SparseStorage.cpp +++ b/lib/ADT/SparseStorage.cpp @@ -1,17 +1,41 @@ #include "klee/ADT/SparseStorage.h" +#include "klee/Expr/Expr.h" #include "llvm/Support/raw_ostream.h" #include "llvm/ADT/StringExtras.h" namespace klee { +// template <> class SparseStorageEq { +// public: +// static bool cmp(const unsigned char &a, const unsigned char &b) { +// return a == b; +// } +// }; + +// template <> class SparseStorageEq> { +// public: +// static bool cmp(const ref &a, const ref &b) { +// // both are null +// if (a.isNull() && b.isNull()) { +// return true; +// } +// // Some is null, some is not +// if (a.isNull() || b.isNull()) { +// return false; +// } +// return a == b; +// } +// }; + template <> -void SparseStorage::print(llvm::raw_ostream &os) const { - if (internalStorage.size() * 2 < sizeOfSetRange()) { +void SparseStorage::print(llvm::raw_ostream &os, Density d) const { + if (d == Density::Sparse) { // "Sparse representation" os << "["; bool firstPrinted = false; - for (const auto &element : internalStorage) { + auto ordered = calculateOrderedStorage(); + for (const auto &element : ordered) { if (firstPrinted) { os << ", "; } @@ -35,4 +59,47 @@ void SparseStorage::print(llvm::raw_ostream &os) const { os << llvm::utostr(defaultValue); } } + +template<> +void SparseStorage>::print(llvm::raw_ostream &os, Density d) const { + os << "["; + if (d == Density::Sparse) { + // "Sparse representation" + bool firstPrinted = false; + auto ordered = calculateOrderedStorage(); + for (const auto &element : ordered) { + if (firstPrinted) { + os << ", "; + } + os << element.first << ": "; + if (element.second) { + os << element.second; + } else { + os << "null"; + } + firstPrinted = true; + } + } else { + // "Dense representation" + bool firstPrinted = false; + for (size_t i = 0; i < sizeOfSetRange(); i++) { + if (firstPrinted) { + os << ", "; + } + auto expr = load(i); + if (expr) { + os << expr; + } else { + os << "null"; + } + firstPrinted = true; + } + } + os << "] DV: "; + if (defaultValue) { + os << defaultValue; + } else { + os << "null"; + } +} } diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 4aed7dbc4ae..bf7e1e01b57 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -364,34 +364,35 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, // transparently avoid screwing up symbolics (if the byte is symbolic // then its concrete cache byte isn't being used) but is just a hack. -void AddressSpace::copyOutConcretes() { +void AddressSpace::copyOutConcretes(const Assignment &assignment) { for (const auto &object : objects) { auto &mo = object.first; auto &os = object.second; if (!mo->isUserSpecified && !os->readOnly && mo->size != 0) { - copyOutConcrete(mo, os.get()); + copyOutConcrete(mo, os.get(), assignment); } } } void AddressSpace::copyOutConcrete(const MemoryObject *mo, - const ObjectState *os) const { + const ObjectState *os, const Assignment &assignment) const { auto address = reinterpret_cast(mo->address); std::vector concreteStore(mo->size); for (size_t i = 0; i < mo->size; i++) { - concreteStore[i] = os->concreteStore.load(i); + auto byte = assignment.evaluate(os->read8(i), false); + concreteStore[i] = cast(byte)->getZExtValue(8); } std::memcpy(address, concreteStore.data(), mo->size); } -bool AddressSpace::copyInConcretes() { +bool AddressSpace::copyInConcretes(const Assignment &assignment) { for (auto &obj : objects) { const MemoryObject *mo = obj.first; if (!mo->isUserSpecified) { const auto &os = obj.second; - if (!copyInConcrete(mo, os.get(), mo->address)) + if (!copyInConcrete(mo, os.get(), mo->address, assignment)) return false; } } @@ -400,11 +401,13 @@ bool AddressSpace::copyInConcretes() { } bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os, - uint64_t src_address) { + uint64_t src_address, + const Assignment &assignment) { auto address = reinterpret_cast(src_address); std::vector concreteStore(mo->size); for (size_t i = 0; i < mo->size; i++) { - concreteStore[i] = os->concreteStore.load(i); + auto byte = assignment.evaluate(os->read8(i), false); + concreteStore[i] = cast(byte)->getZExtValue(8); } if (memcmp(address, concreteStore.data(), mo->size) != 0) { if (os->readOnly) { @@ -412,7 +415,7 @@ bool AddressSpace::copyInConcrete(const MemoryObject *mo, const ObjectState *os, } else { ObjectState *wos = getWriteable(mo, os); for (size_t i = 0; i < mo->size; i++) { - wos->concreteStore.store(i, address[i]); + wos->write(i, ConstantExpr::create(address[i], Expr::Int8)); } } } diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index 0acd1c1208d..11d2de81307 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -13,6 +13,7 @@ #include "Memory.h" #include "klee/ADT/ImmutableMap.h" +#include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/System/Time.h" @@ -137,9 +138,10 @@ class AddressSpace { /// actual system memory location they were allocated at. /// Returns the (hypothetical) number of pages needed provided each written /// object occupies (at least) a single page. - void copyOutConcretes(); + void copyOutConcretes(const Assignment &assignment); - void copyOutConcrete(const MemoryObject *mo, const ObjectState *os) const; + void copyOutConcrete(const MemoryObject *mo, const ObjectState *os, + const Assignment &assignment) const; /// \brief Obtain an ObjectState suitable for writing. /// @@ -161,7 +163,7 @@ class AddressSpace { /// /// \retval true The copy succeeded. /// \retval false The copy failed because a read-only object was modified. - bool copyInConcretes(); + bool copyInConcretes(const Assignment &assignment); /// Updates the memory object with the raw memory from the address /// @@ -170,7 +172,7 @@ class AddressSpace { /// @param src_address the address to copy from /// @return bool copyInConcrete(const MemoryObject *mo, const ObjectState *os, - uint64_t src_address); + uint64_t src_address, const Assignment &assignment); }; } // namespace klee diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ccb1ad2d32d..1f4d05db0ed 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -32,6 +32,7 @@ #include "TimingSolver.h" #include "TypeManager.h" #include "UserSearcher.h" +#include "klee/ADT/SparseStorage.h" #include "klee/Core/Context.h" #include "klee/ADT/KTest.h" @@ -676,7 +677,10 @@ MemoryObject *Executor::addExternalObject(ExecutionState &state, void *addr, bool isReadOnly) { auto mo = memory->allocateFixed(reinterpret_cast(addr), size, nullptr); - ObjectState *os = bindObjectInState(state, mo, type, false); + auto array = makeArray(ConstantExpr::createPointer(size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + ObjectState *os = bindObjectInState(state, mo, type, false, array); for (unsigned i = 0; i < size; i++) os->write8(i, ((uint8_t *)addr)[i]); if (isReadOnly) @@ -743,10 +747,13 @@ void Executor::allocateGlobalObjects(ExecutionState &state) { true, nullptr, 8); errnoObj->isFixed = true; - // TODO: unused variable - ObjectState *os = bindObjectInState( - state, errnoObj, typeSystemManager->getWrappedType(pointerErrnoAddr), - false); + auto array = makeArray(Expr::createPointer(sizeof(*errno_addr)), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + + bindObjectInState(state, errnoObj, + typeSystemManager->getWrappedType(pointerErrnoAddr), + false, array); errno_addr = reinterpret_cast(errnoObj->address); } else { errno_addr = getErrnoLocation(state); @@ -898,8 +905,13 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { for (const GlobalVariable &v : m->globals()) { MemoryObject *mo = globalObjects.find(&v)->second; + // auto array = + // makeArray(Expr::createPointer(mo->size), SourceBuilder::global(v)); + auto array = makeArray(Expr::createPointer(mo->size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); ObjectState *os = bindObjectInState( - state, mo, typeSystemManager->getWrappedType(v.getType()), false); + state, mo, typeSystemManager->getWrappedType(v.getType()), false, array); if (v.isDeclaration() && mo->size) { // Program already running -> object already initialized. @@ -933,11 +945,9 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { if (v.isConstant()) { os->setReadOnly(true); // initialise constant memory that may be used with external calls - state.addressSpace.copyOutConcrete(mo, os); + state.addressSpace.copyOutConcrete(mo, os, {}); } } - } else { - os->initializeToRandom(); } } } @@ -1738,6 +1748,7 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, return nullptr; } + llvm::GlobalValue const *clause_value = dyn_cast(bitcast->getOperand(0)); if (!clause_value) { @@ -1761,8 +1772,13 @@ MemoryObject *Executor::serializeLandingpad(ExecutionState &state, MemoryObject *mo = allocate(state, Expr::createPointer(serialized.size()), true, false, nullptr, 1); - ObjectState *os = - bindObjectInState(state, mo, typeSystemManager->getUnknownType(), false); + + auto array = makeArray(Expr::createPointer(serialized.size()), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + + ObjectState *os = bindObjectInState( + state, mo, typeSystemManager->getUnknownType(), false, array); for (unsigned i = 0; i < serialized.size(); i++) { os->write8(i, serialized[i]); } @@ -2319,8 +2335,12 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, 0, "While allocating varargs: malloc did not align to 16 bytes."); } + auto array = makeArray(Expr::createPointer(mo->size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + ObjectState *os = bindObjectInState( - state, mo, typeSystemManager->getUnknownType(), true); + state, mo, typeSystemManager->getUnknownType(), true, array); llvm::Function::arg_iterator ati = std::next(f->arg_begin(), funcArgs); llvm::Type *argType = (ati == f->arg_end()) ? nullptr : ati->getType(); @@ -4880,12 +4900,12 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, if (ati != functionType->param_end()) { argumentType = const_cast(*ati); } - if (ce->getWidth() == Context::get().getPointerWidth() && - state.addressSpace.resolveOne( - ce, typeSystemManager->getWrappedType(argumentType), result)) { - state.addressSpace.findObject(result).second->flushToConcreteStore( - solver.get(), state); - } + // if (ce->getWidth() == Context::get().getPointerWidth() && + // state.addressSpace.resolveOne( + // ce, typeSystemManager->getWrappedType(argumentType), result)) { + // state.addressSpace.findObject(result).second->flushToConcreteStore( + // solver.get(), state); + // } wordIndex += (ce->getWidth() + 63) / 64; } else { ref arg = toUnique(state, *ai); @@ -4910,7 +4930,11 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, } // Prepare external memory for invoking the function - state.addressSpace.copyOutConcretes(); + auto arrays = state.constraints.cs().gatherArrays(); + std::vector> values; + solver->getInitialValues(state.constraints.cs(), arrays, values, state.queryMetaData); + Assignment assignment(arrays, values); + state.addressSpace.copyOutConcretes(assignment); #ifndef WINDOWS // Update external errno state with local state value IDType idResult; @@ -4982,7 +5006,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, return; } - if (!state.addressSpace.copyInConcretes()) { + if (!state.addressSpace.copyInConcretes(assignment)) { terminateStateOnExecError(state, "external modified read-only object", StateTerminationType::External); return; @@ -4992,7 +5016,7 @@ void Executor::callExternalFunction(ExecutionState &state, KInstruction *target, // Update errno memory object with the errno value from the call int error = externalDispatcher->getLastErrno(); state.addressSpace.copyInConcrete(result.first, result.second, - (uint64_t)&error); + (uint64_t)&error, assignment); #endif Type *resultType = target->inst->getType(); @@ -5053,8 +5077,7 @@ ObjectState *Executor::bindObjectInState(ExecutionState &state, const MemoryObject *mo, KType *dynamicType, bool isLocal, const Array *array) { - ObjectState *os = array ? new ObjectState(mo, array, dynamicType) - : new ObjectState(mo, dynamicType); + ObjectState *os = new ObjectState(mo, array, dynamicType); state.addressSpace.bindObject(mo, os); // Its possible that multiple bindings of the same mo in the state @@ -5071,6 +5094,7 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, KInstruction *target, KType *type, bool zeroMemory, const ObjectState *reallocFrom, size_t allocationAlignment, bool checkOutOfMemory) { + static unsigned allocations = 0; const llvm::Value *allocSite = state.prevPC->inst; if (allocationAlignment == 0) { allocationAlignment = getAllocationAlignment(allocSite); @@ -5112,12 +5136,14 @@ void Executor::executeAlloc(ExecutionState &state, ref size, bool isLocal, if (!mo) { bindLocal(target, state, Expr::createPointer(0)); } else { - ObjectState *os = bindObjectInState(state, mo, type, isLocal); + ref source = nullptr; if (zeroMemory) { - os->initializeToZero(); + source = SourceBuilder::constant(SparseStorage(ConstantExpr::create(0, Expr::Int8))); } else { - os->initializeToRandom(); + source = SourceBuilder::uninitialized(allocations++, target); } + auto array = makeArray(size, source); + ObjectState *os = bindObjectInState(state, mo, type, isLocal, array); ref address = mo->getBaseExpr(); if (checkOutOfMemory) { @@ -5431,13 +5457,18 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref size, Expr::Width pointerWidthInBits = Context::get().getPointerWidth(); /* Create symbol for array */ + KInstruction *ki = nullptr; + if (!lazyInitializationSource) { + auto inst = cast(allocSite); + ki = kmodule->getKBlock(inst->getParent())->parent->instructionMap[inst]; + } const Array *addressArray = makeArray( Expr::createPointer(pointerWidthInBits / CHAR_BIT), lazyInitializationSource ? SourceBuilder::lazyInitializationAddress(lazyInitializationSource) : SourceBuilder::symbolicSizeConstantAddress( - 0, updateNameVersion(state, "const_arr"))); + updateNameVersion(state, "const_arr"), ki, size)); ref addressExpr = Expr::createTempRead(addressArray, pointerWidthInBits); @@ -6512,7 +6543,10 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } } else { - ObjectState *os = bindObjectInState(state, mo, type, false); + auto array = makeArray(Expr::createPointer(mo->size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + ObjectState *os = bindObjectInState(state, mo, type, false, array); if (replayPosition >= replayKTest->numObjects) { terminateStateOnUserError(state, "replay count mismatch"); } else { @@ -6595,8 +6629,13 @@ ExecutionState *Executor::formState(Function *f, int argc, char **argv, llvm::Type *argvType = llvm::ArrayType::get(argumentType, 1); + auto array = makeArray(Expr::createPointer(argvMO->size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + ObjectState *argvOS = bindObjectInState( - *state, argvMO, typeSystemManager->getWrappedType(argvType), false); + *state, argvMO, typeSystemManager->getWrappedType(argvType), false, + array); for (int i = 0; i < argc + 1 + envc + 1 + 1; i++) { if (i == argc || i >= argc + 1 + envc) { @@ -6613,9 +6652,13 @@ ExecutionState *Executor::formState(Function *f, int argc, char **argv, if (!arg) klee_error("Could not allocate memory for function arguments"); + auto array = makeArray(Expr::createPointer(arg->size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + ObjectState *os = bindObjectInState( *state, arg, typeSystemManager->getWrappedType(argumentType), - false); + false, array); for (j = 0; j < len + 1; j++) os->write8(j, s[j]); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index a7e0df7160a..81eef98488d 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -287,7 +287,7 @@ class Executor : public Interpreter { ObjectState *bindObjectInState(ExecutionState &state, const MemoryObject *mo, KType *dynamicType, bool IsAlloca, - const Array *array = 0); + const Array *array); /// Resolve a pointer to the memory objects it could point to the /// start of, forking execution when necessary and generating errors diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 02d53d594e3..8b06ef7afb2 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -73,28 +73,22 @@ void MemoryObject::getAllocInfo(std::string &result) const { /***/ -ObjectState::ObjectState(const MemoryObject *mo, KType *dt) - : copyOnWriteOwner(0), object(mo), concreteStore(0), concreteMask(true), - knownSymbolics(nullptr), unflushedMask(false), updates(nullptr, nullptr), - lastUpdate(nullptr), dynamicType(dt), readOnly(false) {} - ObjectState::ObjectState(const Array *array, KType *dt) - : copyOnWriteOwner(0), object(nullptr), concreteStore(0), - concreteMask(false), knownSymbolics(nullptr), unflushedMask(false), - updates(array, nullptr), lastUpdate(nullptr), dynamicType(dt), - readOnly(false) {} + : copyOnWriteOwner(0), object(nullptr), knownSymbolics(nullptr), + concreteKnownSymbolics(0), unflushedMask(false), updates(array, nullptr), + lastUpdate(nullptr), dynamicType(dt), readOnly(false) {} ObjectState::ObjectState(const MemoryObject *mo, const Array *array, KType *dt) - : copyOnWriteOwner(0), object(mo), concreteStore(0), concreteMask(false), - knownSymbolics(nullptr), unflushedMask(false), updates(array, nullptr), + : copyOnWriteOwner(0), object(mo), knownSymbolics(nullptr), + concreteKnownSymbolics(0), unflushedMask(false), updates(array, nullptr), lastUpdate(nullptr), dynamicType(dt), readOnly(false) {} ObjectState::ObjectState(const ObjectState &os) - : copyOnWriteOwner(0), object(os.object), concreteStore(os.concreteStore), - concreteMask(os.concreteMask), knownSymbolics(os.knownSymbolics), + : copyOnWriteOwner(0), object(os.object), knownSymbolics(os.knownSymbolics), + concreteKnownSymbolics(os.concreteKnownSymbolics), unflushedMask(os.unflushedMask), updates(os.updates), - wasZeroInitialized(os.wasZeroInitialized), lastUpdate(os.lastUpdate), - dynamicType(os.dynamicType), readOnly(os.readOnly) {} + lastUpdate(os.lastUpdate), dynamicType(os.dynamicType), + readOnly(os.readOnly) {} ArrayCache *ObjectState::getArrayCache() const { assert(object && "object was NULL"); @@ -105,184 +99,123 @@ ArrayCache *ObjectState::getArrayCache() const { const UpdateList &ObjectState::getUpdates() const { // Constant arrays are created lazily. - if (!updates.root) { - // Collect the list of writes, with the oldest writes first. - - // FIXME: We should be able to do this more efficiently, we just need to be - // careful to get the interaction with the cache right. In particular we - // should avoid creating UpdateNode instances we never use. - unsigned NumWrites = updates.head ? updates.head->getSize() : 0; - std::vector, ref>> Writes(NumWrites); - const auto *un = updates.head.get(); - for (unsigned i = NumWrites; i != 0; un = un->next.get()) { - --i; - Writes[i] = std::make_pair(un->index, un->value); - } - /* For objects of symbolic size we will leave last constant - sizes for every index and create constant array (in terms of - Z3 solver) filled with zeros. This part is required for reads - from unitialzed memory. */ - SparseStorage> Contents( - ConstantExpr::create(concreteStore.defaultV(), Expr::Int8)); - - // Pull off as many concrete writes as we can. - unsigned Begin = 0, End = Writes.size(); - for (; Begin != End; ++Begin) { - // Push concrete writes into the constant array. - ConstantExpr *Index = dyn_cast(Writes[Begin].first); - if (!Index) - break; - - ConstantExpr *Value = dyn_cast(Writes[Begin].second); - if (!Value) - break; - - Contents.store(Index->getZExtValue(), Value); - } + assert(updates.root); - static unsigned id = 0; - std::string arrayName = "const_arr" + llvm::utostr(++id); - const Array *array = nullptr; - - if (object->hasSymbolicSize()) { - /* Extend updates with last written non-zero constant values. - ConstantValues must be empty in constant array. */ - array = getArrayCache()->CreateArray( - object->getSizeExpr(), - SourceBuilder::symbolicSizeConstant(concreteStore.defaultV())); - updates = UpdateList(array, 0); - for (auto entry : Contents.storage()) { - updates.extend(ConstantExpr::create(entry.first, Expr::Int32), entry.second); - } - } else { - std::vector> FixedSizeContents(object->size); - for (size_t i = 0; i < object->size; i++) { - FixedSizeContents[i] = Contents.load(i); + if (auto sizeExpr = dyn_cast(updates.root->size)) { + auto size = sizeExpr->getZExtValue(); + if (concreteKnownSymbolics == size) { + SparseStorage> values( + ConstantExpr::create(0, Expr::Int8)); + for (unsigned i = 0; i < size; i++) { + auto value = knownSymbolics.load(i); + values.store(i, cast(value)); } - array = getArrayCache()->CreateArray( - object->getSizeExpr(), SourceBuilder::constant(FixedSizeContents)); - updates = UpdateList(array, 0); + auto array = getArrayCache()->CreateArray( + updates.root->size, SourceBuilder::constant(values)); + updates = UpdateList(array, nullptr); + knownSymbolics.reset(); + concreteKnownSymbolics = 0; + unflushedMask.reset(); } - - // Apply the remaining (non-constant) writes. - for (; Begin != End; ++Begin) - updates.extend(Writes[Begin].first, Writes[Begin].second); } - return updates; -} + // if (!updates.root) { + // // Collect the list of writes, with the oldest writes first. + + // // FIXME: We should be able to do this more efficiently, we just need to be + // // careful to get the interaction with the cache right. In particular we + // // should avoid creating UpdateNode instances we never use. + // unsigned NumWrites = updates.head ? updates.head->getSize() : 0; + // std::vector, ref>> Writes(NumWrites); + // const auto *un = updates.head.get(); + // for (unsigned i = NumWrites; i != 0; un = un->next.get()) { + // --i; + // Writes[i] = std::make_pair(un->index, un->value); + // } + + // /* For objects of symbolic size we will leave last constant + // sizes for every index and create constant array (in terms of + // Z3 solver) filled with zeros. This part is required for reads + // from unitialzed memory. */ + // SparseStorage> Contents(defaultConstant); + + // // Pull off as many concrete writes as we can. + // unsigned Begin = 0, End = Writes.size(); + // for (; Begin != End; ++Begin) { + // // Push concrete writes into the constant array. + // ConstantExpr *Index = dyn_cast(Writes[Begin].first); + // if (!Index) + // break; + + // ConstantExpr *Value = dyn_cast(Writes[Begin].second); + // if (!Value) + // break; + + // Contents.store(Index->getZExtValue(), Value); + // } + + // static unsigned id = 0; + // std::string arrayName = "const_arr" + llvm::utostr(++id); + // const Array *array = nullptr; + + // array = getArrayCache()->CreateArray( + // object->getSizeExpr(), SourceBuilder::constant(std::move(Contents))); + // updates = UpdateList(array, 0); + + // // Apply the remaining (non-constant) writes. + // for (; Begin != End; ++Begin) + // updates.extend(Writes[Begin].first, Writes[Begin].second); + + // // if (object->hasSymbolicSize()) { + // // /* Extend updates with last written non-zero constant values. + // // ConstantValues must be empty in constant array. */ + // // array = getArrayCache()->CreateArray( + // // object->getSizeExpr(), + // // SourceBuilder::symbolicSizeConstant(concreteStore.defaultV())); + // // updates = UpdateList(array, 0); + // // for (auto entry : Contents.storage()) { + // // updates.extend(ConstantExpr::create(entry.first, Expr::Int32), entry.second); + // // } + // // } else { + // // std::vector> FixedSizeContents(object->size); + // // for (size_t i = 0; i < object->size; i++) { + // // FixedSizeContents[i] = Contents.load(i); + // // } + // // array = getArrayCache()->CreateArray( + // // object->getSizeExpr(), SourceBuilder::constant(FixedSizeContents)); + // // updates = UpdateList(array, 0); + // // } + + // } -void ObjectState::flushToConcreteStore(TimingSolver *solver, - const ExecutionState &state) const { - for (auto i : knownSymbolics.storage()) { - ref ce; - bool success = solver->getValue(state.constraints.cs(), read8(i.first), ce, - state.queryMetaData); - if (!success) { - klee_warning("Solver timed out when getting a value for external call, " - "byte %p+%lu will have random value", - (void *)object->address, i.first); - } - assert(ce->getWidth() == Expr::Int8); - uint8_t value = ce->getZExtValue(8); - concreteStore.store(i.first, value); - } -} - -void ObjectState::makeConcrete() { - concreteMask.reset(true); - knownSymbolics.reset(nullptr); -} - -void ObjectState::initializeToZero() { - makeConcrete(); - wasZeroInitialized = true; - concreteStore.reset(0); -} - -void ObjectState::initializeToRandom() { - makeConcrete(); - wasZeroInitialized = false; - concreteStore.reset(0xAB); + return updates; } -/* -Cache Invariants --- -isByteKnownSymbolic(i) => !isByteConcrete(i) -isByteConcrete(i) => !isByteKnownSymbolic(i) -isByteUnflushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i)) - */ - void ObjectState::flushForRead() const { for (const auto &unflushed : unflushedMask.storage()) { - if (!unflushed.second) { - continue; - } auto offset = unflushed.first; - if (isByteConcrete(offset)) { - updates.extend( - ConstantExpr::create(offset, Expr::Int32), - ConstantExpr::create(concreteStore.load(offset), Expr::Int8)); - } else { - assert(isByteKnownSymbolic(offset) && "invalid bit set in unflushedMask"); - updates.extend(ConstantExpr::create(offset, Expr::Int32), - knownSymbolics.load(offset)); - } + assert(knownSymbolics.load(offset)); + updates.extend(ConstantExpr::create(offset, Expr::Int32), + knownSymbolics.load(offset)); } unflushedMask.reset(false); } void ObjectState::flushForWrite() { flushForRead(); - concreteMask.reset(false); + // The write is symbolic offset and might overwrite any byte knownSymbolics.reset(nullptr); -} - -bool ObjectState::isByteConcrete(unsigned offset) const { - return concreteMask.load(offset); -} - -bool ObjectState::isByteUnflushed(unsigned offset) const { - return unflushedMask.load(offset); -} - -bool ObjectState::isByteKnownSymbolic(unsigned offset) const { - return knownSymbolics.load(offset).get(); -} - -void ObjectState::markByteConcrete(unsigned offset) { - concreteMask.store(offset, true); -} - -void ObjectState::markByteSymbolic(unsigned offset) { - concreteMask.store(offset, false); -} - -void ObjectState::markByteUnflushed(unsigned offset) { - unflushedMask.store(offset, true); -} - -void ObjectState::markByteFlushed(unsigned offset) { - unflushedMask.store(offset, false); -} - -void ObjectState::setKnownSymbolic(unsigned offset, - Expr *value /* can be null */) { - knownSymbolics.store(offset, value); + concreteKnownSymbolics = 0; } /***/ ref ObjectState::read8(unsigned offset) const { - if (isByteConcrete(offset)) { - return ConstantExpr::create(concreteStore.load(offset), Expr::Int8); - } else if (isByteKnownSymbolic(offset)) { - return knownSymbolics.load(offset); + if (auto byte = knownSymbolics.load(offset)) { + return byte; } else { - assert(!isByteUnflushed(offset) && "unflushed byte without cache value"); - + assert(!unflushedMask.load(offset) && "unflushed byte without cache value"); return ReadExpr::create(getUpdates(), ConstantExpr::create(offset, Expr::Int32)); } @@ -308,12 +241,19 @@ ref ObjectState::read8(ref offset) const { } void ObjectState::write8(unsigned offset, uint8_t value) { - // assert(read_only == false && "writing to read-only object!"); - concreteStore.store(offset, value); - setKnownSymbolic(offset, 0); - - markByteConcrete(offset); - markByteUnflushed(offset); + auto byte = knownSymbolics.load(offset); + if (byte) { + auto ce = dyn_cast(byte); + if (ce && ce->getZExtValue(8) == value) { + return; + } + if (ce) { + concreteKnownSymbolics--; + } + } + knownSymbolics.store(offset, ConstantExpr::create(value, Expr::Int8)); + unflushedMask.store(offset, true); + concreteKnownSymbolics++; } void ObjectState::write8(unsigned offset, ref value) { @@ -321,10 +261,15 @@ void ObjectState::write8(unsigned offset, ref value) { if (ConstantExpr *CE = dyn_cast(value)) { write8(offset, (uint8_t)CE->getZExtValue(8)); } else { - setKnownSymbolic(offset, value.get()); - - markByteSymbolic(offset); - markByteUnflushed(offset); + auto byte = knownSymbolics.load(offset); + if (byte && byte == value) { + return; + } + if (byte && isa(byte)) { + concreteKnownSymbolics--; + } + knownSymbolics.store(offset, value); + unflushedMask.store(offset, true); } } @@ -500,9 +445,8 @@ void ObjectState::print() const { llvm::errs() << "\tBytes:\n"; for (unsigned i = 0; i < object->size; i++) { llvm::errs() << "\t\t[" << i << "]" - << " concrete? " << isByteConcrete(i) << " known-sym? " - << isByteKnownSymbolic(i) << " unflushed? " - << isByteUnflushed(i) << " = "; + << " known? " << !knownSymbolics.load(i).isNull() + << " unflushed? " << unflushedMask.load(i) << " = "; ref e = read8(i); llvm::errs() << e << "\n"; } diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index bddd2007a99..fee35fe1b34 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -210,15 +210,10 @@ class ObjectState { ref object; - /// @brief Holds all known concrete bytes - mutable SparseStorage concreteStore; - - /// @brief concreteMask[byte] is set if byte is known to be concrete - mutable SparseStorage concreteMask; - - /// knownSymbolics[byte] holds the symbolic expression for byte, - /// if byte is known to be symbolic + /// knownSymbolics[byte] holds the expression for byte, + /// if byte is known mutable SparseStorage> knownSymbolics; + mutable unsigned concreteKnownSymbolics; /// unflushedMask[byte] is set if byte is unflushed /// mutable because may need flushed during read of const @@ -227,8 +222,6 @@ class ObjectState { // mutable because we may need flush during read of const mutable UpdateList updates; - bool wasZeroInitialized = true; - ref lastUpdate; KType *dynamicType; @@ -237,18 +230,10 @@ class ObjectState { bool readOnly; public: - /// Create a new object state for the given memory object with concrete - /// contents. The object might be either symbolic or constant size. - /// The initial contents are defined by the array source. The array - /// itself is constructed lazily unless UseConstantArrays is unset. - ObjectState(const MemoryObject *mo, KType *dt); - - /// Create a new object state for the given memory object with symbolic - /// contents. - + /// Create a new object state for the given memory // For objects in memory ObjectState(const MemoryObject *mo, const Array *array, KType *dt); - // For symbolic objects not in memory + // For symbolic objects not in memory (hack) ObjectState(const Array *array, KType *dt); ObjectState(const ObjectState &os); @@ -258,12 +243,6 @@ class ObjectState { void setReadOnly(bool ro) { readOnly = ro; } - /// Make contents all concrete and zero - void initializeToZero(); - - /// Make contents all concrete and random - void initializeToRandom(); - void swapObjectHack(MemoryObject *mo) { object = mo; } @@ -281,13 +260,6 @@ class ObjectState { void write64(unsigned offset, uint64_t value); void print() const; - /* - Looks at all the symbolic bytes of this object, gets a value for them - from the solver and puts them in the concreteStore. - */ - void flushToConcreteStore(TimingSolver *solver, - const ExecutionState &state) const; - bool isAccessableFrom(KType *) const; KType *getDynamicType() const; @@ -304,21 +276,6 @@ class ObjectState { void flushForRead() const; void flushForWrite(); - /// isByteConcrete ==> !isByteKnownSymbolic - bool isByteConcrete(unsigned offset) const; - - /// isByteKnownSymbolic ==> !isByteConcrete - bool isByteKnownSymbolic(unsigned offset) const; - - /// isByteUnflushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i)) - bool isByteUnflushed(unsigned offset) const; - - void markByteConcrete(unsigned offset); - void markByteSymbolic(unsigned offset); - void markByteFlushed(unsigned offset); - void markByteUnflushed(unsigned offset); - void setKnownSymbolic(unsigned offset, Expr *value); - ArrayCache *getArrayCache() const; }; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index a9d7457a888..a81fbbd8199 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -865,8 +865,15 @@ void SpecialFunctionHandler::handleDefineFixedObject( uint64_t size = cast(arguments[1])->getZExtValue(); MemoryObject *mo = executor.memory->allocateFixed(address, size, state.prevPC->inst); - executor.bindObjectInState( - state, mo, executor.typeSystemManager->getUnknownType(), false); + + auto array = executor.makeArray(ConstantExpr::createPointer(size), + SourceBuilder::constant(SparseStorage( + ConstantExpr::create(0, Expr::Int8)))); + + executor.bindObjectInState(state, mo, + executor.typeSystemManager->getUnknownType(), + false, array); + mo->isUserSpecified = true; // XXX hack; } diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index d67bd3ddbd0..016e1711cc0 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -198,6 +198,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref &e, // For each constant array found for (auto &element : arrays) { const Array *arr = element.first; + auto arraySize = cast(arr->size)->getZExtValue(); assert(arr->isConstantArray() && "Array is not concrete"); assert(element.second.size() == 1 && "Multiple indexes on the same array"); @@ -224,7 +225,7 @@ bool ExprOptimizer::computeIndexes(array2idx_ty &arrays, const ref &e, // For each concrete value 'i' stored in the array if (ref constantSource = cast(arr->source)) { - for (size_t aIdx = 0; aIdx < constantSource->constantValues.size(); + for (size_t aIdx = 0; aIdx < arraySize; aIdx += width) { auto *a = new Assignment(); std::vector objects; @@ -302,7 +303,8 @@ ref ExprOptimizer::getSelectOptExpr( std::vector> arrayConstValues; if (ref constantSource = dyn_cast(read->updates.root->source)) { - arrayConstValues = constantSource->constantValues; + arrayConstValues = + constantSource->constantValues.getFirstNIndexes(size); } for (auto it = us.rbegin(); it != us.rend(); it++) { const UpdateNode *un = *it; @@ -377,7 +379,7 @@ ref ExprOptimizer::getSelectOptExpr( std::vector> arrayConstValues; if (ref constantSource = dyn_cast(read->updates.root->source)) { - arrayConstValues = constantSource->constantValues; + arrayConstValues = constantSource->constantValues.getFirstNIndexes(size); } if (arrayConstValues.size() < size) { // We need to "force" initialization of the values diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp index a0b4d63fe21..860f1a0a505 100644 --- a/lib/Expr/Assignment.cpp +++ b/lib/Expr/Assignment.cpp @@ -23,7 +23,11 @@ void Assignment::dump() const { for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e; ++i) { llvm::errs() << (*i).first->getName() << "\n"; - (*i).second.print(llvm::errs()); + Density d = + ((*i).second.storage().size() * 2 < (*i).second.sizeOfSetRange()) + ? Density::Sparse + : Density::Dense; + (*i).second.print(llvm::errs(), d); llvm::errs() << "\n"; } } diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index ccf6eab730a..09661dced92 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -1465,22 +1465,22 @@ Array::Array(ref _size, ref _source, Expr::Width _domain, Expr::Width _range, unsigned _id) : size(_size), source(_source), domain(_domain), range(_range), id(_id) { ref constantSize = dyn_cast(size); - assert( - (!isa(_source) || - cast(_source)->size() == constantSize->getZExtValue()) && - "Invalid size for constant array!"); + // assert( + // (!isa(_source) || + // cast(_source)->size() == constantSize->getZExtValue()) && + // "Invalid size for constant array!"); computeHash(); -#ifndef NDEBUG - if (isa(_source)) { - for (const ref * - it = cast(_source)->constantValues.data(), - *end = cast(_source)->constantValues.data() + - cast(_source)->constantValues.size(); - it != end; ++it) - assert((*it)->getWidth() == getRange() && - "Invalid initial constant value!"); - } -#endif // NDEBUG +// #ifndef NDEBUG +// if (isa(_source)) { +// for (const ref * +// it = cast(_source)->constantValues.data(), +// *end = cast(_source)->constantValues.data() + +// cast(_source)->constantValues.size(); +// it != end; ++it) +// assert((*it)->getWidth() == getRange() && +// "Invalid initial constant value!"); +// } +// #endif // NDEBUG std::set allArrays = _source->getRelatedArrays(); std::vector sizeArrays; @@ -1496,6 +1496,10 @@ Array::Array(ref _size, ref _source, Expr::Width _domain, } } +bool Array::isConstantArray() const { + return isa(source); +} + Array::~Array() {} unsigned Array::computeHash() { @@ -1536,9 +1540,8 @@ ref ReadExpr::create(const UpdateList &ul, ref index) { ref constantSource = cast(ul.root->source); uint64_t concreteIndex = CE->getZExtValue(); - uint64_t size = constantSource->constantValues.size(); - if (concreteIndex < size) { - return constantSource->constantValues[concreteIndex]; + if (auto value = constantSource->constantValues.load(concreteIndex)) { + return value; } } } @@ -2251,12 +2254,14 @@ static ref TryConstArrayOpt(const ref &cl, ReadExpr *rd) { // for now, just assume standard "flushing" of a concrete array, // where the concrete array has one update for each index, in order + auto arraySize = dyn_cast(rd->updates.root->size); + assert(arraySize); + auto size = arraySize->getZExtValue(); ref res = ConstantExpr::alloc(0, Expr::Bool); if (ref constantSource = dyn_cast(rd->updates.root->source)) { - for (unsigned i = 0, e = constantSource->constantValues.size(); i != e; - ++i) { - if (cl == constantSource->constantValues[i]) { + for (unsigned i = 0, e = size; i != e; ++i) { + if (cl == constantSource->constantValues.load(i)) { // Arbitrary maximum on the size of disjunction. if (++numMatches > 100) return EqExpr_create(cl, rd); diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp index bcadb591560..418640769a6 100644 --- a/lib/Expr/ExprEvaluator.cpp +++ b/lib/Expr/ExprEvaluator.cpp @@ -32,15 +32,10 @@ ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul, if (ref constantSource = dyn_cast(ul.root->source)) { - if (index < constantSource->constantValues.size()) { - return Action::changeTo(constantSource->constantValues[index]); + if (auto value = constantSource->constantValues.load(index)) { + return Action::changeTo(value); } } - if (ref symbolicSizeConstantSource = - dyn_cast(ul.root->source)) { - return Action::changeTo(ConstantExpr::create( - symbolicSizeConstantSource->defaultValue, ul.root->getRange())); - } return Action::changeTo(getInitialValue(*ul.root, index)); } diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 165b438025f..fc51291601a 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -387,17 +387,10 @@ class PPrinter : public ExprPPrinter { PC << source->getName() << " "; if (auto s = dyn_cast(source)) { PC << " ["; - for (unsigned i = 0; i < s->constantValues.size(); i++) { - PC << s->constantValues[i]; - if (i != s->constantValues.size() - 1) { - PC << " "; - } - } + s->constantValues.print(PC.getStream(), Density::Sparse); PC << "]"; - } else if (auto s = dyn_cast(source)) { - PC << s->defaultValue; } else if (auto s = dyn_cast(source)) { - PC << s->defaultValue << " " << s->version; + PC << "UNIMPLEMENTED"; } else if (auto s = dyn_cast(source)) { PC << s->name << " " << s->version; } else if (auto s = dyn_cast(source)) { diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index e1a9b9aa89c..6167a8e0c42 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -613,14 +613,8 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { << " " << array->getDomain() << ") )"; printSeperator(); - if (ref symbolicSizeConstantSource = - dyn_cast(array->source)) { - printConstant(ConstantExpr::create( - symbolicSizeConstantSource->defaultValue, array->getRange())); - } else if (ref constantSource = - cast(array->source)) { - printConstant(constantSource->constantValues[byteIndex]); - } + auto source = dyn_cast(array->source); + printConstant(source->constantValues.load(byteIndex)); p->popIndent(); printSeperator(); diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index 9be58ae5ce5..79ff86470dd 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -54,6 +54,10 @@ const char *Token::getKindName() const { return "KWQuery"; case KWPath: return "KWPath"; + case KWDV: + return "KWDV"; + case KWNull: + return "KWNull"; case KWReserved: return "KWReserved"; case KWSymbolic: @@ -168,6 +172,9 @@ static bool isWidthKW(const char *Str, unsigned N) { Token &Lexer::SetIdentifierTokenKind(Token &Result) { unsigned Length = BufferPos - Result.start; switch (Length) { + case 2: + if (memcmp("DV", Result.start, 2) == 0) + return SetTokenKind(Result, Token::KWDV); case 3: if (memcmp("def", Result.start, 3) == 0) return SetTokenKind(Result, Token::KWReserved); @@ -180,6 +187,8 @@ Token &Lexer::SetIdentifierTokenKind(Token &Result) { return SetTokenKind(Result, Token::KWTrue); if (memcmp("path", Result.start, 4) == 0) return SetTokenKind(Result, Token::KWPath); + if (memcmp("null", Result.start, 4) == 0) + return SetTokenKind(Result, Token::KWNull); break; case 5: diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index b072cec8261..a870ba9f0c5 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -322,7 +322,6 @@ class ParserImpl : public Parser { SourceResult ParseSource(); SourceResult ParseConstantSource(); - SourceResult ParseSymbolicSizeConstantSource(); SourceResult ParseSymbolicSizeConstantAddressSource(); SourceResult ParseMakeSymbolicSource(); SourceResult ParseLazyInitializationContentSource(); @@ -483,8 +482,6 @@ SourceResult ParserImpl::ParseSource() { SourceResult source; if (type == "constant") { source = ParseConstantSource(); - } else if (type == "symbolicSizeConstant") { - source = ParseSymbolicSizeConstantSource(); } else if (type == "symbolicSizeConstantAddress") { source = ParseSymbolicSizeConstantAddressSource(); } else if (type == "makeSymbolic") { @@ -509,39 +506,51 @@ SourceResult ParserImpl::ParseSource() { } SourceResult ParserImpl::ParseConstantSource() { - std::vector> Values; + std::unordered_map> storage; + ref defaultValue = nullptr; + ConsumeLSquare(); + ConsumeLSquare(); while (Tok.kind != Token::RSquare) { if (Tok.kind == Token::EndOfFile) { Error("unexpected end of file."); assert(0); } - - ExprResult Res = ParseNumber(8); // Should be Range Type - if (Res.isValid()) - Values.push_back(cast(Res.get())); + ExprResult Index = ParseNumber(64).get(); + ConsumeExpectedToken(Token::Colon); + ExprResult Res = ParseNumber(8).get(); // Should be Range Type + storage.insert({cast(Index.get())->getZExtValue(), + cast(Res.get())}); + if (Tok.kind == Token::Comma) { + ConsumeExpectedToken(Token::Comma); + } } ConsumeRSquare(); - return SourceBuilder::constant(Values); -} + ConsumeExpectedToken(Token::KWDV); + ConsumeExpectedToken(Token::Colon); -SourceResult ParserImpl::ParseSymbolicSizeConstantSource() { - auto valueExpr = ParseNumber(64).get(); - if (auto ce = dyn_cast(valueExpr)) { - return SourceBuilder::symbolicSizeConstant(ce->getZExtValue()); + if (Tok.kind != Token::KWNull) { + ExprResult DV = ParseNumber(8).get(); // Should be Range Type + defaultValue = cast(DV.get()); } else { - assert(0); + ConsumeExpectedToken(Token::KWNull); } + + ConsumeRSquare(); + + SparseStorage> Values(storage, defaultValue); + return SourceBuilder::constant(Values); } SourceResult ParserImpl::ParseSymbolicSizeConstantAddressSource() { - auto valueExpr = ParseNumber(64).get(); - auto versionExpr = ParseNumber(64).get(); - auto value = dyn_cast(valueExpr); - auto version = dyn_cast(versionExpr); - assert(value && version); - return SourceBuilder::symbolicSizeConstantAddress(value->getZExtValue(), - version->getZExtValue()); + assert(0 && "unimplemented"); + // auto valueExpr = ParseNumber(64).get(); + // auto versionExpr = ParseNumber(64).get(); + // auto value = dyn_cast(valueExpr); + // auto version = dyn_cast(versionExpr); + // assert(value && version); + // return SourceBuilder::symbolicSizeConstantAddress(value->getZExtValue(), + // version->getZExtValue()); } SourceResult ParserImpl::ParseMakeSymbolicSource() { diff --git a/lib/Expr/SourceBuilder.cpp b/lib/Expr/SourceBuilder.cpp index a667a19ba26..75ffc2dc2d9 100644 --- a/lib/Expr/SourceBuilder.cpp +++ b/lib/Expr/SourceBuilder.cpp @@ -1,4 +1,5 @@ #include "klee/Expr/SourceBuilder.h" +#include "klee/ADT/SparseStorage.h" #include "klee/Expr/Expr.h" #include "klee/Expr/SymbolicSource.h" #include "klee/Module/KModule.h" @@ -6,23 +7,25 @@ using namespace klee; ref -SourceBuilder::constant(const std::vector> &constantValues) { +SourceBuilder::constant(SparseStorage> constantValues) { ref r(new ConstantSource(constantValues)); r->computeHash(); return r; } -ref SourceBuilder::symbolicSizeConstant(unsigned defaultValue) { - ref r(new SymbolicSizeConstantSource(defaultValue)); +ref +SourceBuilder::uninitialized(unsigned version, const KInstruction *allocSite) { + ref r(new UninitializedSource(version, allocSite)); r->computeHash(); return r; } ref -SourceBuilder::symbolicSizeConstantAddress(unsigned defaultValue, - unsigned version) { +SourceBuilder::symbolicSizeConstantAddress(unsigned version, + const KInstruction *allocSite, + ref size) { ref r( - new SymbolicSizeConstantAddressSource(defaultValue, version)); + new SymbolicSizeConstantAddressSource(version, allocSite, size)); r->computeHash(); return r; } @@ -81,9 +84,15 @@ ref SourceBuilder::value(const llvm::Value &_allocSite, assert(0 && "unreachable"); } +ref SourceBuilder::global(const llvm::GlobalVariable &gv) { + ref r(new GlobalSource(gv)); + r->computeHash(); + return r; +} + ref SourceBuilder::irreproducible(const std::string &name) { static unsigned id = 0; ref r(new IrreproducibleSource(name + llvm::utostr(++id))); r->computeHash(); return r; -} \ No newline at end of file +} diff --git a/lib/Expr/SymbolicSource.cpp b/lib/Expr/SymbolicSource.cpp index 9d8d3b6e582..ffbf94959c1 100644 --- a/lib/Expr/SymbolicSource.cpp +++ b/lib/Expr/SymbolicSource.cpp @@ -46,27 +46,34 @@ std::set LazyInitializationSource::getRelatedArrays() const { } unsigned ConstantSource::computeHash() { - unsigned res = 0; - for (unsigned i = 0, e = constantValues.size(); i != e; ++i) { - res = - (res * SymbolicSource::MAGIC_HASH_CONSTANT) + constantValues[i]->hash(); + auto defaultV = constantValues.defaultV(); + auto ordered = constantValues.calculateOrderedStorage(); + + unsigned res = (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + + (defaultV ? defaultV->hash() : 0); + + for (auto kv : ordered) { + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + kv.first; + res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + kv.second->hash(); } - res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + getKind(); + hashValue = res; return hashValue; } -unsigned SymbolicSizeConstantSource::computeHash() { - unsigned res = - (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + defaultValue; +unsigned UninitializedSource::computeHash() { + unsigned res = getKind(); + res = res * SymbolicSource::MAGIC_HASH_CONSTANT + version; + res = res * SymbolicSource::MAGIC_HASH_CONSTANT + allocSite->hash(); hashValue = res; return hashValue; } unsigned SymbolicSizeConstantAddressSource::computeHash() { - unsigned res = - (getKind() * SymbolicSource::MAGIC_HASH_CONSTANT) + defaultValue; - res = (res * SymbolicSource::MAGIC_HASH_CONSTANT) + version; + unsigned res = getKind(); + res = res * MAGIC_HASH_CONSTANT + version; + res = res * MAGIC_HASH_CONSTANT + allocSite->hash(); + res = res * MAGIC_HASH_CONSTANT + size->hash(); hashValue = res; return hashValue; } diff --git a/lib/Module/KInstruction.cpp b/lib/Module/KInstruction.cpp index b5c33fe41d8..4781c9d1f47 100644 --- a/lib/Module/KInstruction.cpp +++ b/lib/Module/KInstruction.cpp @@ -115,3 +115,11 @@ unsigned KInstruction::getDest() const { return parent->parent->getNumArgs() + getIndex() + (parent->instructions - parent->parent->instructions); } + +KInstruction::Index KInstruction::getID() const { + return {getGlobalIndex(), parent->getId(), parent->parent->id}; +} + +KArgument::Index KArgument::getID() const { + return {argNo, parent->id}; +} diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 946fd2f087a..3f5c83ea84a 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -482,7 +482,7 @@ void KModule::checkModule() { } } -KBlock *KModule::getKBlock(llvm::BasicBlock *bb) { +KBlock *KModule::getKBlock(const llvm::BasicBlock *bb) { return functionMap[bb->getParent()]->blockMap[bb]; } diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index d6c4bbacc05..f4c1b377aad 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -389,13 +389,9 @@ class CexRangeEvaluator : public ExprRangeEvaluator { if (array.isConstantArray() && index.isFixed()) { if (ref constantSource = dyn_cast(array.source)) { - if (index.min() < constantSource->constantValues.size()) { - return ValueRange( - constantSource->constantValues[index.min()]->getZExtValue(8)); + if (auto value = constantSource->constantValues.load(index.min())) { + return ValueRange(value->getZExtValue(8)); } - } else if (ref symbolicSizeConstantSource = - dyn_cast(array.source)) { - return ValueRange(symbolicSizeConstantSource->defaultValue); } } return ValueRange(0, 255); @@ -896,10 +892,11 @@ class CexData { if (ref constantSource = dyn_cast(array->source)) { // Verify the range. - propagateExactValues(constantSource->constantValues[index.min()], + if (!isa(array->size)) { + assert(0 && "Unimplemented"); + } + propagateExactValues(constantSource->constantValues.load(index.min()), range); - } else if (isa(array->source)) { - assert(0 && "not implemented"); } else { CexValueData cvd = cod.getExactValues(index.min()); if (range.min() > cvd.min()) { diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 3ee8fbe2b7b..95998f39859 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -435,7 +435,7 @@ ::VCExpr STPBuilder::getInitialArray(const Array *root) { std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); std::string unique_name = root->getName() + unique_id; - if (isa(root->source)) { + if (isa(root->source)) { llvm::report_fatal_error( "STP does not support constant arrays or quantifiers to instantiate " "constant array of symbolic size!"); @@ -451,14 +451,14 @@ ::VCExpr STPBuilder::getInitialArray(const Array *root) { // to work correctly in that case. // TODO: usage of `constantValues.size()` seems unconvinient. - for (unsigned i = 0, e = constantSource->constantValues.size(); i != e; - ++i) { - ::VCExpr prev = array_expr; - array_expr = vc_writeExpr( - vc, prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0), - construct(constantSource->constantValues[i], 0)); - vc_DeleteExpr(prev); - } + // for (unsigned i = 0, e = constantSource->constantValues.size(); i != e; + // ++i) { + // ::VCExpr prev = array_expr; + // array_expr = vc_writeExpr( + // vc, prev, construct(ConstantExpr::alloc(i, root->getDomain()), 0), + // construct(constantSource->constantValues[i], 0)); + // vc_DeleteExpr(prev); + // } } _arr_hash.hashArrayExpr(root, array_expr); diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index e80feae88c3..c9144cf2119 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -252,35 +252,47 @@ Z3ASTHandle Z3Builder::getInitialArray(const Array *root) { // using the size of the array hash as a counter. std::string unique_id = llvm::utostr(_arr_hash._array_hash.size()); std::string unique_name = root->getIdentifier() + unique_id; - if (ref symbolicSizeConstantSource = - dyn_cast(root->source)) { + + + auto source = dyn_cast(root->source); + auto value = (source ? source->constantValues.defaultV() : nullptr); + if (source) { + assert(value); + } + + if (source && !isa(root->size)) { array_expr = buildConstantArray(unique_name.c_str(), root->getDomain(), - root->getRange(), - symbolicSizeConstantSource->defaultValue); + root->getRange(), value->getZExtValue(8)); } else { - array_expr = - buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); + array_expr = buildArray(unique_name.c_str(), root->getDomain(), root->getRange()); } - if (root->isConstantArray() && constant_array_assertions.count(root) == 0) { - std::vector array_assertions; - if (ref constantSource = - dyn_cast(root->source)) { - for (unsigned i = 0, e = constantSource->constantValues.size(); i != e; - ++i) { + if (source) { + if (auto constSize = dyn_cast(root->size)) { + std::vector array_assertions; + for (size_t i = 0; i < constSize->getZExtValue(); i++) { + auto value = source->constantValues.load(i); // construct(= (select i root) root->value[i]) to be asserted in // Z3Solver.cpp int width_out; - Z3ASTHandle array_value = - construct(constantSource->constantValues[i], &width_out); + Z3ASTHandle array_value = construct(value, &width_out); assert(width_out == (int)root->getRange() && "Value doesn't match root range"); array_assertions.push_back( eqExpr(readExpr(array_expr, bvConst32(root->getDomain(), i)), array_value)); } + constant_array_assertions[root] = std::move(array_assertions); + } else { + for (auto [index, value] : source->constantValues.storage()) { + int width_out; + Z3ASTHandle array_value = construct(value, &width_out); + assert(width_out == (int)root->getRange() && + "Value doesn't match root range"); + array_expr = writeExpr( + array_expr, bvConst32(root->getDomain(), index), array_value); + } } - constant_array_assertions[root] = std::move(array_assertions); } _arr_hash.hashArrayExpr(root, array_expr); diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 643a9a61257..26b5ca699be 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -551,8 +551,8 @@ bool Z3SolverImpl::internalRunSolver( } for (auto constant_array : constant_arrays_in_query.results) { - assert(builder->constant_array_assertions.count(constant_array) == 1 && - "Constant array found in query, but not handled by Z3Builder"); + // assert(builder->constant_array_assertions.count(constant_array) == 1 && + // "Constant array found in query, but not handled by Z3Builder"); if (all_constant_arrays_in_query.count(constant_array)) continue; all_constant_arrays_in_query.insert(constant_array); @@ -852,7 +852,7 @@ class Z3NonIncSolverImpl final : public Z3SolverImpl { auto arrays = query.gatherArrays(); bool forceTactic = true; for (auto array : arrays) { - if (isa(array->source)) { + if (isa(array->source) && !isa(array->size)) { forceTactic = false; break; } diff --git a/test/Expr/Evaluate.kquery b/test/Expr/Evaluate.kquery index e6b0d1e1a44..03893c51e99 100644 --- a/test/Expr/Evaluate.kquery +++ b/test/Expr/Evaluate.kquery @@ -17,7 +17,7 @@ arr12 : (array (w64 8) (makeSymbolic arr1 0)) # RUN: grep "Query 2: VALID" %t.log # Query 2 -constant0 : (array (w64 4) (constant [ 1 2 3 5 ])) +constant0 : (array (w64 4) (constant [[0: 1, 1: 2, 2: 3, 3: 5] DV: 0])) (query [] (Eq (Add w8 (Read w8 0 constant0) (Read w8 3 constant0)) 6)) diff --git a/test/Expr/print-smt-let.kquery b/test/Expr/print-smt-let.kquery index 871e6e4f29c..54035a782bd 100644 --- a/test/Expr/print-smt-let.kquery +++ b/test/Expr/print-smt-let.kquery @@ -1069,7 +1069,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) [makeSymbolic0]) # Query 72 -- Type: InitialValues, Instructions: 30 -constant2 : (array (w64 4) (constant [121 101 115 0])) +constant2 : (array (w64 4) (constant [[0: 121, 1: 101, 2: 115, 3: 0] DV: 0])) makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) (query [(Eq false @@ -1105,7 +1105,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) # Query 74 -- Type: InitialValues, Instructions: 37 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 4) (constant [171 171 171 171])) +constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) @@ -1128,7 +1128,7 @@ constant2 : (array (w64 4) (constant [171 171 171 171])) # Query 75 -- Type: InitialValues, Instructions: 40 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) +constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0])) (query [(Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) 13)] @@ -1141,7 +1141,7 @@ constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) # Query 76 -- Type: InitialValues, Instructions: 50 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 4) (constant [171 171 171 171])) +constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) @@ -1160,7 +1160,7 @@ constant2 : (array (w64 4) (constant [171 171 171 171])) # Query 77 -- Type: InitialValues, Instructions: 51 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) +constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) diff --git a/test/Expr/print-smt-named.kquery b/test/Expr/print-smt-named.kquery index 5e0112b2b79..f5560bc9c46 100644 --- a/test/Expr/print-smt-named.kquery +++ b/test/Expr/print-smt-named.kquery @@ -1068,7 +1068,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) [makeSymbolic0]) # Query 72 -- Type: InitialValues, Instructions: 30 -constant2 : (array (w64 4) (constant [121 101 115 0])) +constant2 : (array (w64 4) (constant [[0: 121, 1: 101, 2: 115, 3: 0] DV: 0])) makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) (query [(Eq false @@ -1104,7 +1104,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) # Query 74 -- Type: InitialValues, Instructions: 37 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 4) (constant [171 171 171 171])) +constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) @@ -1127,7 +1127,7 @@ constant2 : (array (w64 4) (constant [171 171 171 171])) # Query 75 -- Type: InitialValues, Instructions: 40 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) +constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0])) (query [(Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) 13)] @@ -1140,7 +1140,7 @@ constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) # Query 76 -- Type: InitialValues, Instructions: 50 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 4) (constant [171 171 171 171])) +constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) @@ -1159,7 +1159,7 @@ constant2 : (array (w64 4) (constant [171 171 171 171])) # Query 77 -- Type: InitialValues, Instructions: 51 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) +constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) diff --git a/test/Expr/print-smt-none.kquery b/test/Expr/print-smt-none.kquery index 90c0bce0e72..1c3b12717f2 100644 --- a/test/Expr/print-smt-none.kquery +++ b/test/Expr/print-smt-none.kquery @@ -1068,7 +1068,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) [makeSymbolic0]) # Query 72 -- Type: InitialValues, Instructions: 30 -constant2 : (array (w64 4) (constant [121 101 115 0])) +constant2 : (array (w64 4) (constant [[0: 121, 1: 101, 2: 115, 3: 0] DV: 0])) makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) (query [(Eq false @@ -1104,7 +1104,7 @@ makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) # Query 74 -- Type: InitialValues, Instructions: 37 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 4) (constant [171 171 171 171])) +constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) @@ -1127,7 +1127,7 @@ constant2 : (array (w64 4) (constant [171 171 171 171])) # Query 75 -- Type: InitialValues, Instructions: 40 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) +constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0])) (query [(Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) 13)] @@ -1140,7 +1140,7 @@ constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) # Query 76 -- Type: InitialValues, Instructions: 50 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 4) (constant [171 171 171 171])) +constant2 : (array (w64 4) (constant [[0: 171, 1: 171, 2: 171, 3: 171] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) @@ -1159,7 +1159,7 @@ constant2 : (array (w64 4) (constant [171 171 171 171])) # Query 77 -- Type: InitialValues, Instructions: 51 makeSymbolic1 : (array (w64 4) (makeSymbolic unnamed 0)) makeSymbolic0 : (array (w64 4) (makeSymbolic unnamed_1 0)) -constant2 : (array (w64 16) (constant [12 0 0 0 13 0 0 0 14 0 0 0 15 0 0 0])) +constant2 : (array (w64 16) (constant [[0: 12, 4: 13, 8: 14, 12: 15] DV: 0])) (query [(Eq false (Ult N0:(Mul w64 4 (SExt w64 (ReadLSB w32 0 makeSymbolic0))) diff --git a/test/Feature/SymbolicSizes/UninitializedMemory.c b/test/Feature/SymbolicSizes/UninitializedMemory.c new file mode 100644 index 00000000000..43c2fa589bf --- /dev/null +++ b/test/Feature/SymbolicSizes/UninitializedMemory.c @@ -0,0 +1,25 @@ +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 --use-sym-size-alloc --skip-not-symbolic-objects --use-merged-pointer-dereference=true %t.bc 2>&1 | FileCheck %s +#include "klee/klee.h" + +#include +#include +#include + +int main() { + int n; + klee_make_symbolic(&n, sizeof(n), "n"); + + char *s = (char *)malloc(n); + s[2] = 10; + if (s[0] == 0) { + printf("1) 0\n"); + } else { + printf("1) not 0\n"); + } + + // CHECK-DAG: 1) 0 + // CHECK-DAG: 1) not 0 +} diff --git a/test/Feature/UninitializedConstantMemory.c b/test/Feature/UninitializedConstantMemory.c new file mode 100644 index 00000000000..5d795d9a1e2 --- /dev/null +++ b/test/Feature/UninitializedConstantMemory.c @@ -0,0 +1,30 @@ +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out --solver-backend=z3 %t.bc 2>&1 | FileCheck %s +#include "klee/klee.h" + +#include +#include +#include + +int main() { + char arr[3]; + + if (arr[0] == 0) { + printf("1) 0\n"); + } else { + printf("1) not 0\n"); + } + + char *zero_arr = (char *)calloc(3, sizeof(char)); + if (zero_arr[1] == 0) { + return 0; + } else { + // CHECK-NOT: ASSERTION FAIL + assert(0); + } + + // CHECK-DAG: 1) 0 + // CHECK-DAG: 1) not 0 +} diff --git a/test/regression/2023-08-28-invalid-pointer-dereference.c b/test/regression/2023-08-28-invalid-pointer-dereference.c new file mode 100644 index 00000000000..cdd8388e716 --- /dev/null +++ b/test/regression/2023-08-28-invalid-pointer-dereference.c @@ -0,0 +1,22 @@ +// RUN: %clang %s -g -emit-llvm %O0opt -c -o %t.bc +// RUN: rm -rf %t.klee-out +// RUN: %klee --use-sym-size-alloc --output-dir=%t.klee-out %t.bc 2>&1 | FileCheck %s + +#pragma clang attribute push(__attribute__((optnone)), apply_to = function) + +int main() { + int length1 = klee_int("len"); + int length2 = klee_int("len"); + if (length1 < 1) { + length1 = 1; + } + if (length2 < 1) { + length2 = 1; + } + char *nondetString1 = (char *)__builtin_alloca(length1 * sizeof(char)); + char *nondetString2 = (char *)__builtin_alloca(length2 * sizeof(char)); + nondetString1[length1 - 1] = '\0'; + // CHECK-NOT: memory error: out of bound pointer + nondetString2[length2 - 1] = '\0'; +} +#pragma clang attribute pop