Semantics.h

#ifndef ROSE_BinaryAnalysis_Partitioner2_Semantics_H
#define ROSE_BinaryAnalysis_Partitioner2_Semantics_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS
 
#include <Rose/As.h>
#include <Rose/BinaryAnalysis/MemoryMap.h>
#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/MemoryCellMap.h>
#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
#include <Rose/BinaryAnalysis/SymbolicExpression.h>
 
#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
#include <boost/serialization/access.hpp>
#endif
 
namespace Rose {
namespace BinaryAnalysis {
namespace Partitioner2 {
 
namespace Semantics {
 
using SValue = InstructionSemantics::SymbolicSemantics::SValue;
 
using SValuePtr = InstructionSemantics::SymbolicSemantics::SValuePtr;
 
using RegisterState = InstructionSemantics::BaseSemantics::RegisterStateGeneric;
 
using RegisterStatePtr = InstructionSemantics::BaseSemantics::RegisterStateGenericPtr;
 
using State = InstructionSemantics::BaseSemantics::State;
 
using StatePtr = InstructionSemantics::BaseSemantics::StatePtr;
 
//                                      Memory State
 
template<class Super = InstructionSemantics::SymbolicSemantics::MemoryListState> // or MemoryMapState
class MemoryState: public Super {
public:
    using Ptr = boost::shared_ptr<MemoryState>;
 
private:
    MemoryMapPtr map_;
    std::vector<SValuePtr> addressesRead_;
    bool enabled_;
 
#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
private:
    friend class boost::serialization::access;
    template<class S> void serialize(S&, unsigned version);
#endif
 
protected:
    MemoryState()                                       // for serialization
        : enabled_(true) {}
 
    explicit MemoryState(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell)
        : Super(protocell), enabled_(true) {}
 
    MemoryState(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval,
                const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval)
        : Super(addrProtoval, valProtoval), enabled_(true) {}
 
public:
    static Ptr instance(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell) {
        return Ptr(new MemoryState(protocell));
    }
 
    static  Ptr instance(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval,
                         const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval) {
        return Ptr(new MemoryState(addrProtoval, valProtoval));
    }
 
    static Ptr instance(const Ptr &other) {
        return Ptr(new MemoryState(*other));
    }
 
public:
    virtual InstructionSemantics::BaseSemantics::MemoryStatePtr
    create(const InstructionSemantics::BaseSemantics::SValuePtr &addrProtoval,
           const InstructionSemantics::BaseSemantics::SValuePtr &valProtoval) const override {
        return instance(addrProtoval, valProtoval);
    }
 
    virtual InstructionSemantics::BaseSemantics::MemoryStatePtr
    create(const InstructionSemantics::BaseSemantics::MemoryCellPtr &protocell) const override {
        return instance(protocell);
    }
 
    virtual InstructionSemantics::BaseSemantics::AddressSpacePtr
    clone() const override {
        return Ptr(new MemoryState(*this));
    }
 
public:
    static Ptr
    promote(const InstructionSemantics::BaseSemantics::MemoryStatePtr &x) {
        Ptr retval = as<MemoryState>(x);
        assert(x!=NULL);
        return retval;
    }
 
public:
    bool enabled() const { return enabled_; }
    void enabled(bool b) { enabled_ = b; }
    MemoryMapPtr memoryMap() const { return map_; }
    void memoryMap(const MemoryMapPtr &map) { map_ = map; }
    const std::vector<SValuePtr>& addressesRead() const { return addressesRead_; }
    std::vector<SValuePtr>& addressesRead() { return addressesRead_; }
public:
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    readMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
               InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
               InstructionSemantics::BaseSemantics::RiscOperators *valOps) override;
 
    virtual void
    writeMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                const InstructionSemantics::BaseSemantics::SValuePtr &value,
                InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
                InstructionSemantics::BaseSemantics::RiscOperators *valOps) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    peekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
               InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
               InstructionSemantics::BaseSemantics::RiscOperators *valOps) override;
 
private:
    InstructionSemantics::BaseSemantics::SValuePtr
    readOrPeekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                     const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
                     InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
                     InstructionSemantics::BaseSemantics::RiscOperators *valOps,
                     bool withSideEffects);
 
public:
    void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&) const override;
};
 
using MemoryListState = MemoryState<InstructionSemantics::SymbolicSemantics::MemoryListState>;
 
using MemoryMapState = MemoryState<InstructionSemantics::SymbolicSemantics::MemoryMapState>;
 
using MemoryListStatePtr = boost::shared_ptr<MemoryListState>;
 
using MemoryMapStatePtr = boost::shared_ptr<MemoryMapState>;
 
//                                      RISC Operators
 
using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;
 
class RiscOperators: public InstructionSemantics::SymbolicSemantics::RiscOperators {
public:
    using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
    using Ptr = RiscOperatorsPtr;
 
private:
    static const size_t TRIM_THRESHOLD_DFLT = 100;
 
    // Serialization
#ifdef ROSE_ENABLE_BOOST_SERIALIZATION
private:
    friend class boost::serialization::access;
    template<class S> void serialize(S&, unsigned version);
#endif
 
    // Real constructors
protected:
    RiscOperators();                                    // for serialization
 
    RiscOperators(const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver);
 
    RiscOperators(const InstructionSemantics::BaseSemantics::StatePtr &state, const SmtSolverPtr &solver);
 
public:
    ~RiscOperators();
 
    // Static allocating constructors
public:
    static RiscOperatorsPtr instance(const RegisterDictionaryPtr&);
    static RiscOperatorsPtr instance(const RegisterDictionaryPtr&, const SmtSolverPtr&,
                                     SemanticMemoryParadigm memoryParadigm = LIST_BASED_MEMORY);
    static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::SValuePtr &protoval);
    static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&);
    static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::StatePtr&);
    static RiscOperatorsPtr instance(const InstructionSemantics::BaseSemantics::StatePtr&, const SmtSolverPtr&);
    // Virtual constructors
public:
    virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics::BaseSemantics::SValuePtr &protoval,
           const SmtSolverPtr &solver = SmtSolverPtr()) const override;
 
    virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics::BaseSemantics::StatePtr &state,
           const SmtSolverPtr &solver = SmtSolverPtr()) const override;
 
    // Dynamic pointer casts
public:
    static RiscOperatorsPtr promote(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
 
    // Override methods from base class.
public:
    virtual void startInstruction(SgAsmInstruction*) override;
};
 
//                                      Memory State
 
template<class Super>
InstructionSemantics::BaseSemantics::SValuePtr
MemoryState<Super>::readMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                               const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
                               InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
                               InstructionSemantics::BaseSemantics::RiscOperators *valOps) {
    return readOrPeekMemory(addr, dflt, addrOps, valOps, true/*with side effects*/);
}
 
template<class Super>
InstructionSemantics::BaseSemantics::SValuePtr
MemoryState<Super>::peekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                               const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
                               InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
                               InstructionSemantics::BaseSemantics::RiscOperators *valOps) {
    return readOrPeekMemory(addr, dflt, addrOps, valOps, false/*no side effects*/);
}
 
template<class Super>
InstructionSemantics::BaseSemantics::SValuePtr
MemoryState<Super>::readOrPeekMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                                     const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
                                     InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
                                     InstructionSemantics::BaseSemantics::RiscOperators *valOps,
                                     bool withSideEffects) {
    using namespace InstructionSemantics;
    ASSERT_require2(8==dflt->nBits(), "multi-byte reads should have been handled above this call");
 
    if (!enabled_)
        return dflt->copy();
 
    addressesRead_.push_back(SValue::promote(addr));
 
    // Symbolic memory takes precedence over concrete memory when the address is concrete. I.e., reading from concrete address
    // 0x1234 the first time will return the value stored in concrete memory, say 0 and not make any modifications to the symbolic
    // state. If the value 1 is then written to 0x1234 it will be written to the symbolic state, not the concrete state (because
    // changing the concrete state is probably a global side effect unless the entire memory map has been copied). Subsequent reads
    // from 0x1234 should return the 1 that we wrote, not the 0 that's stored in the concrete memory.
    BaseSemantics::SValuePtr symbolicDefault = dflt;
    if (map_ && addr->toUnsigned()) {
        Address va = *addr->toUnsigned();
        bool isModifiable = map_->at(va).require(MemoryMap::WRITABLE).exists();
        bool isInitialized = map_->at(va).require(MemoryMap::INITIALIZED).exists();
 
        // Read the byte from concrete memory if possible.
        SymbolicExpression::Ptr valueRead;
        if (!isModifiable || isInitialized) {
            uint8_t byte;
            if (1 == map_->at(va).limit(1).read(&byte).size())
                valueRead = SymbolicExpression::makeIntegerConstant(8, byte);
        }
 
        // If concrete memory is mutable, then we don't really know the value for sure.
        if (isModifiable) {
            const auto indeterminate = SymbolicExpression::makeIntegerVariable(8);
            if (valueRead) {
                valueRead = SymbolicExpression::makeSet(valueRead, indeterminate, valOps->solver());
            } else {
                valueRead = indeterminate;
            }
        }
 
        // Make the value that we read from concrete memory the default for reading from symbolic memory.
        if (valueRead) {
            auto val = SymbolicSemantics::SValue::promote(valOps->undefined_(8));
            val->set_expression(valueRead);
            symbolicDefault = val;
        }
 
        // Does symbolic memory define this address?
        const bool isPresentSymbolically = [this, &addr]() {
            struct CellFinder: BaseSemantics::MemoryCell::Visitor {
                BaseSemantics::SValue::Ptr needle;
                bool found = false;
 
                explicit CellFinder(const BaseSemantics::SValue::Ptr &addr)
                    : needle(addr) {
                    ASSERT_not_null(addr);
                }
 
                void operator()(BaseSemantics::MemoryCell::Ptr &haystack) override {
                    ASSERT_not_null(haystack);
                    if (haystack->address()->mustEqual(needle))
                        found = true;
                }
            } cellFinder(addr);
            this->traverse(cellFinder);
            return cellFinder.found;
        }();
 
        // Perhaps there is no need to update the symbolic memory.
        if (!isPresentSymbolically && isInitialized && !isModifiable)
            return symbolicDefault;
 
        // But if we do have to update the symbolic memory, do so in a way that makes it look like the value was always there.
        if (!isPresentSymbolically && withSideEffects) {
            SgAsmInstruction *addrInsn = addrOps->currentInstruction(); // order is important because addrOps and valOps
            SgAsmInstruction *valInsn = valOps->currentInstruction();   // might be the same object. Read both of them
            addrOps->currentInstruction(nullptr);                       // before clearing either of them.
            valOps->currentInstruction(nullptr);
            Super::writeMemory(addr, symbolicDefault, addrOps, valOps);
            addrOps->currentInstruction(addrInsn);
            valOps->currentInstruction(valInsn);
        }
    }
 
    // Read from symbolic memory
    if (withSideEffects) {
        return Super::readMemory(addr, symbolicDefault, addrOps, valOps);
    } else {
        return Super::peekMemory(addr, symbolicDefault, addrOps, valOps);
    }
}
 
template<class Super>
void
MemoryState<Super>::writeMemory(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                                const InstructionSemantics::BaseSemantics::SValuePtr &value,
                                InstructionSemantics::BaseSemantics::RiscOperators *addrOps,
                                InstructionSemantics::BaseSemantics::RiscOperators *valOps) {
    if (!enabled_)
        return;
    Super::writeMemory(addr, value, addrOps, valOps);
}
 
template<class Super>
void
MemoryState<Super>::print(std::ostream &out, InstructionSemantics::BaseSemantics::Formatter &fmt) const {
    namespace BS = InstructionSemantics::BaseSemantics;
 
    out <<fmt.get_line_prefix() <<"concrete memory:\n";
    if (map_) {
        map_->dump(out, fmt.get_line_prefix() + "  ");
    } else {
        out <<fmt.get_line_prefix() <<"no memory map\n";
    }
 
    const bool isEmpty = as<const BS::MemoryCellState>(this) ?
                         as<const BS::MemoryCellState>(this)->allCells().empty() :
                         false;
 
    if (as<const BS::MemoryCellMap>(this)) {
        out <<fmt.get_line_prefix() <<"symbolic memory (map-based):\n";
    } else {
        out <<fmt.get_line_prefix() <<"symbolic memory (list-based):\n";
    }
    BS::Indent indent(fmt);
    if (isEmpty) {
        out <<fmt.get_line_prefix() <<"empty\n";
    } else {
        Super::print(out, fmt);
    }
}
 
} // namespace
} // namespace
} // namespace
} // namespace
 
#endif
#endif