PartialSymbolicSemantics.h

#ifndef ROSE_BinaryAnalysis_InstructionSemantics2_PartialSymbolicSemantics_H
#define ROSE_BinaryAnalysis_InstructionSemantics2_PartialSymbolicSemantics_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS

#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
#endif
#include <inttypes.h>

#include <map>
#include <stdint.h>
#include <vector>

#include "rosePublicConfig.h"
#ifdef ROSE_HAVE_LIBGCRYPT
#include <gcrypt.h>
#endif

#include <Rose/BinaryAnalysis/InstructionSemantics2/BaseSemantics.h>
#include "integerOps.h"
#include <Rose/BinaryAnalysis/MemoryMap.h>
#include <Rose/FormatRestorer.h>

namespace Rose {
namespace BinaryAnalysis {              // documented elsewhere
namespace InstructionSemantics2 {       // documented elsewhere

namespace PartialSymbolicSemantics {

//                                      Print formatter

class Formatter: public BaseSemantics::Formatter {
protected:
    typedef std::map<uint64_t, uint64_t> Map;
    Map renames;
    size_t next_name;
public:
    Formatter(): next_name(1) {}
    uint64_t rename(uint64_t orig_name);
};


//                                      Semantic values

typedef Sawyer::SharedPointer<class SValue> SValuePtr;

class SValue: public BaseSemantics::SValue {
public:
    using Super = BaseSemantics::SValue;

    using Ptr = SValuePtr;

public:
    uint64_t name;              
    uint64_t offset;            
    bool negate;                
    // Real constructors
protected:
    explicit SValue(size_t nbits)
        : BaseSemantics::SValue(nbits), name(nextName()), offset(0), negate(false) {}

    SValue(size_t nbits, uint64_t number)
        : BaseSemantics::SValue(nbits), name(0), offset(number), negate(false) {
        if (nbits <= 64) {
            this->offset &= IntegerOps::genMask<uint64_t>(nbits);
        } else {
            name = nextName();
            offset = 0;
        }
    }

    SValue(size_t nbits, uint64_t name, uint64_t offset, bool negate)
        : BaseSemantics::SValue(nbits), name(name), offset(offset), negate(negate) {
        this->offset &= IntegerOps::genMask<uint64_t>(nbits);
        ASSERT_require(nbits <= 64 || name != 0);
    }

public:
    static uint64_t nextName();

    // Static allocating constructors
public:
    static SValuePtr instance() {
        return SValuePtr(new SValue(1));
    }

    static SValuePtr instance(size_t nbits) {
        return SValuePtr(new SValue(nbits));
    }

    static SValuePtr instance(size_t nbits, uint64_t value) {
        return SValuePtr(new SValue(nbits, value));
    }
    
    static SValuePtr instance(size_t nbits, uint64_t name, uint64_t offset, bool negate) {
        return SValuePtr(new SValue(nbits, name, offset, negate));
    }

    // Virtual constructors
public:
    virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override {
        return instance(nbits);
    }
    virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override {
        return instance(nbits);
    }
    virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override {
        return instance(nbits);
    }

    virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) const override {
        return instance(nbits, value);
    }

    virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const override {
        SValuePtr retval(new SValue(*this));
        if (new_width!=0 && new_width!=retval->nBits())
            retval->set_width(new_width);
        return retval;
    }

    virtual Sawyer::Optional<BaseSemantics::SValuePtr>
    createOptionalMerge(const BaseSemantics::SValuePtr &other,const BaseSemantics::MergerPtr&,
                        const SmtSolverPtr&) const override;
    
    virtual BaseSemantics::SValuePtr create(size_t nbits, uint64_t name, uint64_t offset, bool negate) const {
        return instance(nbits, name, offset, negate);
    }

    // Dynamic pointer casts
public:
    static SValuePtr promote(const BaseSemantics::SValuePtr &v) {
        SValuePtr retval = v.dynamicCast<SValue>();
        ASSERT_not_null(retval);
        return retval;
    }

    // Other stuff we inherited from the super class
public:
    virtual void hash(Combinatorics::Hasher&) const override;
    virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;

    virtual bool isBottom() const override {
        return false;
    }

    // Override legacy members. These have similar non-virtual camelCase names in the base class, and eventually we'll remoe
    // these snake_case names and change the camelCase names to be the virtual functions. Therefore, be sure to use "override"
    // in your own code so you know when we make this change.
public:
    // See nBits
    virtual void set_width(size_t nbits) override {
        if (nbits > 64 && name == 0) {
            *this = SValue(nbits);
        } else {
            ASSERT_require(nbits <= 64 || name != 0);
            BaseSemantics::SValue::set_width(nbits);
            offset &= IntegerOps::genMask<uint64_t>(nbits);
        }
    }

    // See mayEqual
    virtual bool may_equal(const BaseSemantics::SValuePtr &other,
                           const SmtSolverPtr &solver = SmtSolverPtr()) const override;

    // See mustEqual
    virtual bool must_equal(const BaseSemantics::SValuePtr &other,
                            const SmtSolverPtr &solver = SmtSolverPtr()) const override;

    // See isConcrete
    virtual bool is_number() const override {
        return 0==name;
    }

    // See toUnsigned and toSigned.
    virtual uint64_t get_number() const override {
        ASSERT_require(is_number());
        return offset;
    }
};


//                                      Register state

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


//                                      Memory state

// PartialSymbolicSemantics uses BaseSemantics::MemoryCellList (or subclass) as its memory state, and does not expect the
// MemoryCellList to be byte-restricted (i.e., the cells can store multi-byte values).

typedef BaseSemantics::MemoryCellList MemoryState;
typedef BaseSemantics::MemoryCellListPtr MemoryStatePtr;


//                                      Complete state

typedef boost::shared_ptr<class State> StatePtr;

class State: public BaseSemantics::State {
public:
    using Super = BaseSemantics::State;

    using Ptr = StatePtr;

    // Real constructors
protected:
    State(const BaseSemantics::RegisterStatePtr &registers,
          const BaseSemantics::MemoryStatePtr &memory)
        : BaseSemantics::State(registers, memory) {
        // This state should use PartialSymbolicSemantics values (or subclasses thereof)
        ASSERT_not_null(registers);
        (void) SValue::promote(registers->protoval());
        ASSERT_not_null(memory);
        (void) SValue::promote(memory->get_addr_protoval());
        (void) SValue::promote(memory->get_val_protoval());

        // This state should use a memory that is not byte restricted.
        MemoryStatePtr mcl = MemoryState::promote(memory);
        ASSERT_require(!mcl->byteRestricted());
    }

    State(const State &other): BaseSemantics::State(other) {}

    // Static allocating constructors
public:
    static StatePtr instance(const BaseSemantics::RegisterStatePtr &registers,
                             const BaseSemantics::MemoryStatePtr &memory) {
        return StatePtr(new State(registers, memory));
    }

    static StatePtr instance(const StatePtr &other) {
        return StatePtr(new State(*other));
    }

    // Virtual constructors
public:
    virtual BaseSemantics::StatePtr create(const BaseSemantics::RegisterStatePtr &registers,
                                           const BaseSemantics::MemoryStatePtr &memory) const override {
        return instance(registers, memory);
    }

    virtual BaseSemantics::StatePtr clone() const override {
        StatePtr self = promote(boost::const_pointer_cast<BaseSemantics::State>(shared_from_this()));
        return instance(self);
    }

    // Dynamic pointer casts
public:
    static StatePtr promote(const BaseSemantics::StatePtr &x) {
        StatePtr retval = boost::dynamic_pointer_cast<State>(x);
        ASSERT_not_null(x);
        return retval;
    }

    // Methods first declared at this level of the class hierarchy
public:
    virtual void print_diff_registers(std::ostream&, const StatePtr &other_state, Formatter&) const;

    virtual bool equal_registers(const StatePtr &other) const;

    virtual void discard_popped_memory();
};


//                                      RISC operators

typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;

class RiscOperators: public BaseSemantics::RiscOperators {
public:
    using Super = BaseSemantics::RiscOperators;

    using Ptr = RiscOperatorsPtr;

protected:
    MemoryMap::Ptr map;

    // Real constructors
protected:
    explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr())
        : BaseSemantics::RiscOperators(protoval, solver) {
        name("PartialSymbolic");
    }
    explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
        : BaseSemantics::RiscOperators(state, solver) {
        name("PartialSymbolic");
    }

    // Static allocating constructors
public:
    static RiscOperatorsPtr instance(const RegisterDictionary *regdict);

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

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

    // Virtual constructors
public:
    virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
                                                   const SmtSolverPtr &solver = SmtSolverPtr()) const override {
        return instance(protoval, solver);
    }

    virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr &state,
                                                   const SmtSolverPtr &solver = SmtSolverPtr()) const override {
        return instance(state, solver);
    }

    // Dynamic pointer casts
public:
    static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &x) {
        RiscOperatorsPtr retval = boost::dynamic_pointer_cast<RiscOperators>(x);
        ASSERT_not_null(retval);
        return retval;
    }

    // Methods first declared at this level of the class hierarchy
public:
    const MemoryMap::Ptr get_memory_map() const { return map; }
    void set_memory_map(const MemoryMap::Ptr &m) { map = m; }
    // Risc operators inherited
public:
    virtual void interrupt(int majr, int minr) override;
    virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a_,
                                          const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a_,
                                         const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a_,
                                          const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a_) override;
    virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a_,
                                             size_t begin_bit, size_t end_bit) override;
    virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a_,
                                            const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a_) override;
    virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a_) override;
    virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a_,
                                                const BaseSemantics::SValuePtr &sa_) override;
    virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a_,
                                                 const BaseSemantics::SValuePtr &sa_) override;
    virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a_,
                                               const BaseSemantics::SValuePtr &sa_) override;
    virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a_,
                                                const BaseSemantics::SValuePtr &sa_) override;
    virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a_,
                                                          const BaseSemantics::SValuePtr &sa_) override;
    virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a_) override;
    virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &sel_,
                                         const BaseSemantics::SValuePtr &a_,
                                         const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a_, size_t new_width) override;
    virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a_,
                                         const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a_,
                                                    const BaseSemantics::SValuePtr &b_,
                                                    const BaseSemantics::SValuePtr &c_,
                                                    BaseSemantics::SValuePtr &carry_out/*out*/) override;
    virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a_) override;
    virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a_,
                                                  const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a_,
                                                  const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a_,
                                                    const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a_,
                                                    const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a_,
                                                    const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a_,
                                                      const BaseSemantics::SValuePtr &b_) override;
    virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg,
                                                const BaseSemantics::SValuePtr &addr,
                                                const BaseSemantics::SValuePtr &dflt,
                                                const BaseSemantics::SValuePtr &cond) override;
    virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg,
                                                const BaseSemantics::SValuePtr &addr,
                                                const BaseSemantics::SValuePtr &dflt) override;
    virtual void writeMemory(RegisterDescriptor segreg,
                             const BaseSemantics::SValuePtr &addr,
                             const BaseSemantics::SValuePtr &data,
                             const BaseSemantics::SValuePtr &cond) override;

protected:
    BaseSemantics::SValuePtr readOrPeekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &address,
                                              const BaseSemantics::SValuePtr &dflt_, bool allowSideEffects);
};

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

#endif
#endif