SymbolicMemory2.h

// Symbolic memory -- a memory state where memory is represented by an SMT function whose domain is the address space and whose
// range are the bytes stored at those addresses.
#ifndef Rose_SymbolicMemory_H
#define Rose_SymbolicMemory_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS

#include <BaseSemantics2.h>

namespace Rose {
namespace BinaryAnalysis {
namespace InstructionSemantics2 {
namespace BaseSemantics {

typedef boost::shared_ptr<class SymbolicMemory> SymbolicMemoryPtr;

class SymbolicMemory: public MemoryState {
    SymbolicExpr::Ptr mem_;
protected:
    // All memory states should be heap allocated; use instance(), create(), or clone() instead.
    explicit SymbolicMemory(const SValuePtr &addrProtoval, const SValuePtr &valProtoval)
        : MemoryState(addrProtoval, valProtoval) {
        // Initially assume that addresses are 32 bits wide and values are 8 bits wide. We can change this on the first access.
        mem_ = SymbolicExpr::makeMemoryVariable(32, 8);
    }

public:
    static SymbolicMemoryPtr instance(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) {
        return SymbolicMemoryPtr(new SymbolicMemory(addrProtoval, valProtoval));
    }

public:
    // documented in base class
    virtual MemoryStatePtr create(const SValuePtr &addrProtoval, const SValuePtr &valProtoval) const ROSE_OVERRIDE {
        return instance(addrProtoval, valProtoval);
    }

    // documented in base class
    virtual MemoryStatePtr clone() const ROSE_OVERRIDE {
        return SymbolicMemoryPtr(new SymbolicMemory(*this));
    }

    static SymbolicMemoryPtr promote(const MemoryStatePtr &x) {
        SymbolicMemoryPtr retval = boost::dynamic_pointer_cast<SymbolicMemory>(x);
        ASSERT_not_null(retval);
        return retval;
    }

public:
    SymbolicExpr::Ptr expression() const { return mem_; }
    void expression(const SymbolicExpr::Ptr &mem);
public:
    virtual bool merge(const MemoryStatePtr &other, RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;

    virtual void clear() ROSE_OVERRIDE;

    virtual SValuePtr readMemory(const SValuePtr &address, const SValuePtr &dflt,
                                 RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;

    virtual void writeMemory(const SValuePtr &address, const SValuePtr &value,
                             RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;

    virtual SValuePtr peekMemory(const SValuePtr &address, const SValuePtr &dflt,
                                 RiscOperators *addrOps, RiscOperators *valOps) ROSE_OVERRIDE;

public:
    virtual void hash(Combinatorics::Hasher&, RiscOperators *addrOps, RiscOperators *valOps) const override;

    virtual void print(std::ostream&, Formatter&) const ROSE_OVERRIDE;
};
    
} // namespace
} // namespace
} // namespace
} // namespace

#endif
#endif