MultiSemantics2.h

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

#include "BaseSemantics2.h"

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

namespace MultiSemantics {

class Formatter: public BaseSemantics::Formatter {
public:
    std::vector<std::string> subdomain_names;
};

//                                      Semantic values

typedef Sawyer::SharedPointer<class SValue> SValuePtr;

class SValue: public BaseSemantics::SValue {
protected:
    typedef std::vector<BaseSemantics::SValuePtr> Subvalues;
    Subvalues subvalues;

protected:
    // Protected constructors
    explicit SValue(size_t nbits)
        : BaseSemantics::SValue(nbits) {}

    SValue(const SValue &other)
        : BaseSemantics::SValue(other.nBits()) {
        init(other);
    }

    void init(const SValue &other);

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

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

    // Virtual allocating constructors
public:

    virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const ROSE_OVERRIDE;

    virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const ROSE_OVERRIDE;

    virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const ROSE_OVERRIDE;

    virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t number) const ROSE_OVERRIDE;

    virtual SValuePtr create_empty(size_t nbits) const {
        return SValuePtr(new SValue(nbits));
    }
    
    virtual BaseSemantics::SValuePtr copy(size_t new_width=0) const ROSE_OVERRIDE {
        return BaseSemantics::SValuePtr(new SValue(*this));
    }
    
    virtual Sawyer::Optional<BaseSemantics::SValuePtr>
    createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&,
                        const SmtSolverPtr&) const ROSE_OVERRIDE;

    // Override virtual methods
public:
    virtual bool isBottom() const ROSE_OVERRIDE;
    virtual void print(std::ostream&, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
    virtual void hash(Combinatorics::Hasher&) const override;

    // Override legacy methods. Override these for now, but always call the camelCase names from the base class. Eventually
    // these snake_case names will go away and the camelCase will become the virtual functions, so be sure to specify
    // "override" in your own code so you get notified when that change occurs.
public:
    virtual bool may_equal(const BaseSemantics::SValuePtr &other,
                           const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;

    virtual bool must_equal(const BaseSemantics::SValuePtr &other,
                            const SmtSolverPtr &solver = SmtSolverPtr()) const ROSE_OVERRIDE;

    virtual void set_width(size_t nbits) ROSE_OVERRIDE;

    virtual bool is_number() const ROSE_OVERRIDE;

    virtual uint64_t get_number() const ROSE_OVERRIDE;


    // Additional methods first declared at this level of the class hierarchy
public:
    virtual bool is_valid(size_t idx) const { // hot
        return idx<subvalues.size() && subvalues[idx]!=NULL;
    }

    virtual void invalidate(size_t idx);

    virtual BaseSemantics::SValuePtr get_subvalue(size_t idx) const { // hot
        ASSERT_require(idx<subvalues.size() && subvalues[idx]!=NULL); // you should have called is_valid() first
        return subvalues[idx];
    }

    virtual void set_subvalue(size_t idx, const BaseSemantics::SValuePtr &value) { // hot
        ASSERT_require(value==NULL || value->nBits()==nBits());
        if (idx>=subvalues.size())
            subvalues.resize(idx+1);
        subvalues[idx] = value;
    }
};


//                                      Register states

typedef void RegisterState;

typedef boost::shared_ptr<void> RegisterStatePtr;

//                                      Memory states

typedef void MemoryState;

typedef boost::shared_ptr<void> MemoryStatePtr;

//                                      Complete state

typedef void State;

typedef boost::shared_ptr<void> StatePtr;

//                                      RISC operators

typedef boost::shared_ptr<class RiscOperators> RiscOperatorsPtr;

class RiscOperators: public BaseSemantics::RiscOperators {
protected:
    typedef std::vector<BaseSemantics::RiscOperatorsPtr> Subdomains;
    Subdomains subdomains;
    std::vector<bool> active;
    Formatter formatter;                // contains names for the subdomains

    // Real constructors
protected:
    explicit RiscOperators(const BaseSemantics::SValuePtr &protoval, const SmtSolverPtr &solver = SmtSolverPtr())
        : BaseSemantics::RiscOperators(protoval, solver) {
        name("Multi");
        (void) SValue::promote(protoval); // check that its dynamic type is a MultiSemantics::SValue
    }

    explicit RiscOperators(const BaseSemantics::StatePtr &state, const SmtSolverPtr &solver = SmtSolverPtr())
        : BaseSemantics::RiscOperators(state, solver) {
        name("Multi");
        (void) SValue::promote(state->protoval());      // dynamic type must be a MultiSemantics::SValue
    }

    // Static allocating constructors
public:
    static RiscOperatorsPtr instance(const RegisterDictionary *regdict) {
        BaseSemantics::SValuePtr protoval = SValue::instance();
        return RiscOperatorsPtr(new RiscOperators(protoval));
    }

    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 ROSE_OVERRIDE {
        return instance(protoval, solver);
    }

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

    // Dynamic pointer casts
public:
    static RiscOperatorsPtr promote(const BaseSemantics::RiscOperatorsPtr &ops);
    
    // Methods first defined at this level of the class hiearchy
public:
    virtual size_t add_subdomain(const BaseSemantics::RiscOperatorsPtr &subdomain, const std::string &name, bool activate=true);

    virtual Formatter& get_formatter() {
        return formatter;
    }
    
    virtual size_t nsubdomains() const {
        return subdomains.size();
    }

    virtual BaseSemantics::RiscOperatorsPtr get_subdomain(size_t idx) const;

    virtual bool is_active(size_t idx) const {
        return idx<subdomains.size() && subdomains[idx]!=NULL && active[idx];
    }

    virtual void clear_active(size_t idx) {
        set_active(idx, false);
    }

    virtual void set_active(size_t idx, bool status);

    virtual void before(size_t idx) {}

    virtual void after(size_t idx) {}

    virtual SValuePtr svalue_empty(size_t nbits) {
        return SValue::promote(protoval())->create_empty(nbits);
    }
    
    class Cursor {
    public:
        typedef std::vector<SValuePtr> Inputs;
    protected:
        RiscOperators *ops_;
        Inputs inputs_;
        size_t idx_;
    public:
        Cursor(RiscOperators *ops, const SValuePtr &arg1=SValuePtr(), const SValuePtr &arg2=SValuePtr(),
               const SValuePtr &arg3=SValuePtr())
            : ops_(ops), idx_(0) {
            init(arg1, arg2, arg3);
        }
        Cursor(RiscOperators *ops, const Inputs &inputs)
            : ops_(ops), inputs_(inputs), idx_(0) {
            init();
        }

        static Inputs inputs(const BaseSemantics::SValuePtr &arg1=BaseSemantics::SValuePtr(),
                             const BaseSemantics::SValuePtr &arg2=BaseSemantics::SValuePtr(),
                             const BaseSemantics::SValuePtr &arg3=BaseSemantics::SValuePtr());
                             
        bool at_end() const;                    
        void next();                            
        size_t idx() const;                     
        BaseSemantics::RiscOperatorsPtr operator->() const;   
        BaseSemantics::RiscOperatorsPtr operator*() const;    
        BaseSemantics::SValuePtr operator()(const BaseSemantics::SValuePtr&) const;

    protected:
        void init(const SValuePtr &arg1, const SValuePtr &arg2, const SValuePtr &arg3);
        void init();
        void skip_invalid();
        bool inputs_are_valid() const;
    };
        
    // RISC operations and other overrides
public:
    virtual void print(std::ostream &o, BaseSemantics::Formatter&) const ROSE_OVERRIDE;
    virtual void startInstruction(SgAsmInstruction *insn) ROSE_OVERRIDE;
    virtual void finishInstruction(SgAsmInstruction *insn) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr undefined_(size_t nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr boolean_(bool) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr bottom_(size_t nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr filterCallTarget(const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr filterReturnTarget(const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr filterIndirectJumpTarget(const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr and_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr or_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr xor_(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr invert(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr extract(const BaseSemantics::SValuePtr &a, size_t begin_bit, size_t end_bit) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr concat(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr leastSignificantSetBit(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr mostSignificantSetBit(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr rotateLeft(const BaseSemantics::SValuePtr &a,
                                                const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a,
                                                 const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a,
                                               const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a,
                                                const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a,
                                                          const BaseSemantics::SValuePtr &nbits) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr ite(const BaseSemantics::SValuePtr &cond, const BaseSemantics::SValuePtr &a,
                                         const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a, size_t new_width) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr signExtend(const BaseSemantics::SValuePtr &a, size_t new_width) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr add(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr addWithCarries(const BaseSemantics::SValuePtr &a, const BaseSemantics::SValuePtr &b,
                                                    const BaseSemantics::SValuePtr &c,
                                                    BaseSemantics::SValuePtr &carry_out/*output*/) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr negate(const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr signedDivide(const BaseSemantics::SValuePtr &a,
                                                  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr signedModulo(const BaseSemantics::SValuePtr &a,
                                                  const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr signedMultiply(const BaseSemantics::SValuePtr &a,
                                                    const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr unsignedDivide(const BaseSemantics::SValuePtr &a,
                                                    const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr unsignedModulo(const BaseSemantics::SValuePtr &a,
                                                    const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr unsignedMultiply(const BaseSemantics::SValuePtr &a,
                                                      const BaseSemantics::SValuePtr &b) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpFromInteger(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpToInteger(const BaseSemantics::SValuePtr&, SgAsmFloatType*,
                                                 const BaseSemantics::SValuePtr&) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr&, SgAsmFloatType*, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpIsNan(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpIsDenormalized(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpIsZero(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpIsInfinity(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpSign(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpEffectiveExponent(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpAdd(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                           SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpSubtract(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                                SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpMultiply(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                                SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpDivide(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                              SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpSquareRoot(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr fpRoundTowardZero(const BaseSemantics::SValuePtr&, SgAsmFloatType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr&, SgAsmType*) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
                                                  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg,
                                                  const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
    virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr readMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr,
                                                const BaseSemantics::SValuePtr &dflt,
                                                const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
    virtual BaseSemantics::SValuePtr peekMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr,
                                                const BaseSemantics::SValuePtr &dflt) ROSE_OVERRIDE;
    virtual void writeMemory(RegisterDescriptor segreg, const BaseSemantics::SValuePtr &addr,
                             const BaseSemantics::SValuePtr &data, const BaseSemantics::SValuePtr &cond) ROSE_OVERRIDE;
};

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

#endif
#endif