Semantics.h

#ifndef ROSE_BinaryAnalysis_Partitioner_Semantics_H
#define ROSE_BinaryAnalysis_Partitioner_Semantics_H

#include <Partitioner2/BasicTypes.h>
#include "SymbolicSemantics2.h"

#include <boost/serialization/access.hpp>
#include <boost/serialization/base_object.hpp>
#include <boost/serialization/export.hpp>
#include <boost/serialization/vector.hpp>

namespace Rose {
namespace BinaryAnalysis {
namespace Partitioner2 {
namespace Semantics {

typedef InstructionSemantics2::SymbolicSemantics::SValue SValue;
typedef InstructionSemantics2::SymbolicSemantics::SValuePtr SValuePtr;

typedef InstructionSemantics2::BaseSemantics::RegisterStateGeneric RegisterState;
typedef InstructionSemantics2::BaseSemantics::RegisterStateGenericPtr RegisterStatePtr;

typedef InstructionSemantics2::BaseSemantics::State State;
typedef InstructionSemantics2::BaseSemantics::StatePtr StatePtr;

//                                      Memory State

template<class Super = InstructionSemantics2::SymbolicSemantics::MemoryListState> // or MemoryMapState
class MemoryState: public Super {
public:
    typedef boost::shared_ptr<MemoryState> Ptr;

private:
    MemoryMap::Ptr map_;
    std::vector<SValuePtr> addressesRead_;
    bool enabled_;

#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
private:
    friend class boost::serialization::access;

    template<class S>
    void serialize(S &s, const unsigned version) {
        s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
        s & BOOST_SERIALIZATION_NVP(map_);
        s & BOOST_SERIALIZATION_NVP(addressesRead_);
        s & BOOST_SERIALIZATION_NVP(enabled_);
    }
#endif

protected:
    MemoryState()                                       // for serialization
        : enabled_(true) {}

    explicit MemoryState(const InstructionSemantics2::BaseSemantics::MemoryCellPtr &protocell)
        : Super(protocell), enabled_(true) {}

    MemoryState(const InstructionSemantics2::BaseSemantics::SValuePtr &addrProtoval,
                const InstructionSemantics2::BaseSemantics::SValuePtr &valProtoval)
        : Super(addrProtoval, valProtoval), enabled_(true) {}

public:
    static Ptr instance(const InstructionSemantics2::BaseSemantics::MemoryCellPtr &protocell) {
        return Ptr(new MemoryState(protocell));
    }

    static  Ptr instance(const InstructionSemantics2::BaseSemantics::SValuePtr &addrProtoval,
                         const InstructionSemantics2::BaseSemantics::SValuePtr &valProtoval) {
        return Ptr(new MemoryState(addrProtoval, valProtoval));
    }

    static Ptr instance(const Ptr &other) {
        return Ptr(new MemoryState(*other));
    }

public:
    virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr
    create(const InstructionSemantics2::BaseSemantics::SValuePtr &addrProtoval,
           const InstructionSemantics2::BaseSemantics::SValuePtr &valProtoval) const ROSE_OVERRIDE {
        return instance(addrProtoval, valProtoval);
    }

    virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr
    create(const InstructionSemantics2::BaseSemantics::MemoryCellPtr &protocell) const ROSE_OVERRIDE {
        return instance(protocell);
    }

    virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr
    clone() const ROSE_OVERRIDE {
        return Ptr(new MemoryState(*this));
    }

public:
    static Ptr
    promote(const InstructionSemantics2::BaseSemantics::MemoryStatePtr &x) {
        Ptr retval = boost::dynamic_pointer_cast<MemoryState>(x);
        assert(x!=NULL);
        return retval;
    }

public:
    bool enabled() const { return enabled_; }
    void enabled(bool b) { enabled_ = b; }
    MemoryMap::Ptr memoryMap() const { return map_; }
    void memoryMap(const MemoryMap::Ptr &map) { map_ = map; }
    const std::vector<SValuePtr>& addressesRead() const { return addressesRead_; }
    std::vector<SValuePtr>& addressesRead() { return addressesRead_; }
public:
    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    readMemory(const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics2::BaseSemantics::SValuePtr &dflt,
               InstructionSemantics2::BaseSemantics::RiscOperators *addrOps,
               InstructionSemantics2::BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;

    virtual void
    writeMemory(const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
                const InstructionSemantics2::BaseSemantics::SValuePtr &value,
                InstructionSemantics2::BaseSemantics::RiscOperators *addrOps,
                InstructionSemantics2::BaseSemantics::RiscOperators *valOps) ROSE_OVERRIDE;
};

typedef MemoryState<InstructionSemantics2::SymbolicSemantics::MemoryListState> MemoryListState;
typedef MemoryState<InstructionSemantics2::SymbolicSemantics::MemoryMapState> MemoryMapState;

typedef boost::shared_ptr<MemoryListState> MemoryListStatePtr;

typedef boost::shared_ptr<MemoryMapState> MemoryMapStatePtr;

//                                      RISC Operators

typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;

class RiscOperators: public InstructionSemantics2::SymbolicSemantics::RiscOperators {
public:
    typedef InstructionSemantics2::SymbolicSemantics::RiscOperators Super;

private:
    static const size_t TRIM_THRESHOLD_DFLT = 100;

    // Serialization
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
private:
    friend class boost::serialization::access;

    template<class S>
    void serialize(S &s, const unsigned version) {
        s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Super);
    }
#endif

    // Real constructors
protected:
    RiscOperators() {}                                  // for serialization

    explicit RiscOperators(const InstructionSemantics2::BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL)
        : InstructionSemantics2::SymbolicSemantics::RiscOperators(protoval, solver) {
        name("PartitionerSemantics");
        (void)SValue::promote(protoval);                // make sure its dynamic type is appropriate
        trimThreshold(TRIM_THRESHOLD_DFLT);
    }

    explicit RiscOperators(const InstructionSemantics2::BaseSemantics::StatePtr &state, SMTSolver *solver=NULL)
        : InstructionSemantics2::SymbolicSemantics::RiscOperators(state, solver) {
        name("PartitionerSemantics");
        (void)SValue::promote(state->protoval());
        trimThreshold(TRIM_THRESHOLD_DFLT);
    }

    // Static allocating constructors
public:
    static RiscOperatorsPtr instance(const RegisterDictionary *regdict, SMTSolver *solver=NULL,
                                     SemanticMemoryParadigm memoryParadigm = LIST_BASED_MEMORY) {
        InstructionSemantics2::BaseSemantics::SValuePtr protoval = SValue::instance();
        InstructionSemantics2::BaseSemantics::RegisterStatePtr registers = RegisterState::instance(protoval, regdict);
        InstructionSemantics2::BaseSemantics::MemoryStatePtr memory;
        switch (memoryParadigm) {
            case LIST_BASED_MEMORY:
                memory = MemoryListState::instance(protoval, protoval);
                break;
            case MAP_BASED_MEMORY:
                memory = MemoryMapState::instance(protoval, protoval);
                break;
        }
        InstructionSemantics2::BaseSemantics::StatePtr state = State::instance(registers, memory);
        return RiscOperatorsPtr(new RiscOperators(state, solver));
    }

    static RiscOperatorsPtr
    instance(const InstructionSemantics2::BaseSemantics::SValuePtr &protoval, SMTSolver *solver=NULL) {
        return RiscOperatorsPtr(new RiscOperators(protoval, solver));
    }

    static RiscOperatorsPtr
    instance(const InstructionSemantics2::BaseSemantics::StatePtr &state, SMTSolver *solver=NULL) {
        return RiscOperatorsPtr(new RiscOperators(state, solver));
    }

    // Virtual constructors
public:
    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics2::BaseSemantics::SValuePtr &protoval,
           SMTSolver *solver=NULL) const ROSE_OVERRIDE {
        return instance(protoval, solver);
    }

    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics2::BaseSemantics::StatePtr &state,
           SMTSolver *solver=NULL) const ROSE_OVERRIDE {
        return instance(state, solver);
    }

    // Dynamic pointer casts
public:
    static RiscOperatorsPtr
    promote(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &x) {
        RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
        assert(retval!=NULL);
        return retval;
    }
    
    // Override methods from base class.
public:
    virtual void startInstruction(SgAsmInstruction*) ROSE_OVERRIDE;
};

//                                      Memory State

template<class Super>
InstructionSemantics2::BaseSemantics::SValuePtr
MemoryState<Super>::readMemory(const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
                               const InstructionSemantics2::BaseSemantics::SValuePtr &dflt,
                               InstructionSemantics2::BaseSemantics::RiscOperators *addrOps,
                               InstructionSemantics2::BaseSemantics::RiscOperators *valOps) {
    using namespace InstructionSemantics2;

    if (!enabled_)
        return dflt->copy();

    addressesRead_.push_back(SValue::promote(addr));
    if (map_ && addr->is_number()) {
        ASSERT_require2(8==dflt->get_width(), "multi-byte reads should have been handled above this call");
        rose_addr_t va = addr->get_number();
        bool isModifiable = map_->at(va).require(MemoryMap::WRITABLE).exists();
        bool isInitialized = map_->at(va).require(MemoryMap::INITIALIZED).exists();
        if (!isModifiable || isInitialized) {
            uint8_t byte;
            if (1 == map_->at(va).limit(1).read(&byte).size()) {
                SymbolicExpr::Ptr expr = SymbolicExpr::makeInteger(8, byte);
                if (isModifiable) {
                    SymbolicExpr::Ptr indet = SymbolicExpr::makeVariable(8);
                    expr = SymbolicExpr::makeSet(expr, indet);
                }
                SymbolicSemantics::SValuePtr val = SymbolicSemantics::SValue::promote(valOps->undefined_(8));
                val->set_expression(expr);
                return val;
            }
        }
    }
    return Super::readMemory(addr, dflt, addrOps, valOps);
}

template<class Super>
void
MemoryState<Super>::writeMemory(const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
                                const InstructionSemantics2::BaseSemantics::SValuePtr &value,
                                InstructionSemantics2::BaseSemantics::RiscOperators *addrOps,
                                InstructionSemantics2::BaseSemantics::RiscOperators *valOps) {
    if (!enabled_)
        return;
    Super::writeMemory(addr, value, addrOps, valOps);
}

} // namespace
} // namespace
} // namespace
} // namespace

#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryListState);
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Partitioner2::Semantics::MemoryMapState);
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::Partitioner2::Semantics::RiscOperators);
#endif

#endif