MultiSemantics.h

#ifndef ROSE_BinaryAnalysis_InstructionSemantics_MultiSemantics_H
#define ROSE_BinaryAnalysis_InstructionSemantics_MultiSemantics_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS
 
#include <Rose/BinaryAnalysis/BasicTypes.h>
#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics.h>
 
namespace Rose {                                // documented elsewhere
namespace BinaryAnalysis {                      // documented elsewhere
namespace InstructionSemantics {                // 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 {
public:
    using Super = BaseSemantics::SValue;
 
    using Ptr = SValuePtr;
 
protected:
    typedef std::vector<BaseSemantics::SValuePtr> Subvalues;
    Subvalues subvalues;
 
protected:
    // Protected constructors
    explicit SValue(size_t nbits);
    SValue(const SValue &other);
 
    void init(const SValue &other);
 
    // Static allocating constructors
public:
    static SValuePtr instance();
 
    static SValuePtr promote(const BaseSemantics::SValuePtr&);
 
    // Virtual allocating constructors
public:
 
    virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override;
 
    virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override;
 
    virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override;
 
    virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t number) const override;
 
    virtual SValuePtr create_empty(size_t nbits) const;
 
    virtual BaseSemantics::SValuePtr copy(size_t /*new_width*/=0) const override;
 
    virtual Sawyer::Optional<BaseSemantics::SValuePtr>
    createOptionalMerge(const BaseSemantics::SValuePtr &other, const BaseSemantics::MergerPtr&,
                        const SmtSolverPtr&) const override;
 
    // Override virtual methods
public:
    virtual bool isBottom() const override;
    virtual void print(std::ostream&, BaseSemantics::Formatter&) const 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 override;
 
    virtual bool must_equal(const BaseSemantics::SValuePtr &other,
                            const SmtSolverPtr &solver = SmtSolverPtr()) const override;
 
    virtual void set_width(size_t nbits) override;
 
    virtual bool is_number() const override;
 
    virtual uint64_t get_number() const override;
 
 
    // Additional methods first declared at this level of the class hierarchy
public:
    virtual bool is_valid(size_t idx) const;
 
    virtual void invalidate(size_t idx);
 
    virtual BaseSemantics::SValuePtr get_subvalue(size_t idx) const;
 
    virtual void set_subvalue(size_t idx, const BaseSemantics::SValuePtr &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 {
public:
    using Super = BaseSemantics::RiscOperators;
 
    using Ptr = RiscOperatorsPtr;
 
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&);
 
    explicit RiscOperators(const BaseSemantics::StatePtr&, const SmtSolverPtr&);
 
    // Static allocating constructors
public:
    ~RiscOperators();
 
    static RiscOperatorsPtr instanceFromRegisters(const RegisterDictionaryPtr&);
 
    static RiscOperatorsPtr instanceFromProtoval(const BaseSemantics::SValuePtr &protoval,
                                                 const SmtSolverPtr &solver = SmtSolverPtr());
 
    static RiscOperatorsPtr instanceFromState(const BaseSemantics::StatePtr&, const SmtSolverPtr &solver = SmtSolverPtr());
 
    // Virtual constructors
public:
    virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::SValuePtr &protoval,
                                                   const SmtSolverPtr &solver = SmtSolverPtr()) const override;
 
    virtual BaseSemantics::RiscOperatorsPtr create(const BaseSemantics::StatePtr&,
                                                   const SmtSolverPtr &solver = SmtSolverPtr()) const override;
 
    // 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;
 
    virtual BaseSemantics::RiscOperatorsPtr get_subdomain(size_t idx) const;
 
    virtual bool is_active(size_t idx) const;
 
    virtual void clear_active(size_t idx);
 
    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());
        Cursor(RiscOperators *ops, const Inputs &inputs);
 
        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 override;
    virtual void startInstruction(SgAsmInstruction *insn) override;
    virtual void finishInstruction(SgAsmInstruction *insn) override;
    virtual BaseSemantics::SValuePtr undefined_(size_t nbits) override;
    virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) override;
    virtual BaseSemantics::SValuePtr number_(size_t nbits, uint64_t value) override;
    virtual BaseSemantics::SValuePtr boolean_(bool) override;
    virtual BaseSemantics::SValuePtr bottom_(size_t nbits) override;
    virtual BaseSemantics::SValuePtr filterCallTarget(const BaseSemantics::SValuePtr&) override;
    virtual BaseSemantics::SValuePtr filterReturnTarget(const BaseSemantics::SValuePtr&) override;
    virtual BaseSemantics::SValuePtr filterIndirectJumpTarget(const BaseSemantics::SValuePtr&) 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 &nbits) override;
    virtual BaseSemantics::SValuePtr rotateRight(const BaseSemantics::SValuePtr &a,
                                                 const BaseSemantics::SValuePtr &nbits) override;
    virtual BaseSemantics::SValuePtr shiftLeft(const BaseSemantics::SValuePtr &a,
                                               const BaseSemantics::SValuePtr &nbits) override;
    virtual BaseSemantics::SValuePtr shiftRight(const BaseSemantics::SValuePtr &a,
                                                const BaseSemantics::SValuePtr &nbits) override;
    virtual BaseSemantics::SValuePtr shiftRightArithmetic(const BaseSemantics::SValuePtr &a,
                                                          const BaseSemantics::SValuePtr &nbits) override;
    virtual BaseSemantics::SValuePtr equalToZero(const BaseSemantics::SValuePtr &a) override;
    virtual BaseSemantics::SValuePtr iteWithStatus(const BaseSemantics::SValuePtr &cond, const BaseSemantics::SValuePtr &a,
                                                   const BaseSemantics::SValuePtr &b, IteStatus&) override;
    virtual BaseSemantics::SValuePtr unsignedExtend(const BaseSemantics::SValuePtr &a, size_t new_width) 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/*output*/) 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 fpFromInteger(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpToInteger(const BaseSemantics::SValuePtr&, SgAsmFloatType*,
                                                 const BaseSemantics::SValuePtr&) override;
    virtual BaseSemantics::SValuePtr fpConvert(const BaseSemantics::SValuePtr&, SgAsmFloatType*, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpIsNan(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpIsDenormalized(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpIsZero(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpIsInfinity(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpSign(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpEffectiveExponent(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpAdd(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                           SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpSubtract(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                                SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpMultiply(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                                SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpDivide(const BaseSemantics::SValuePtr&, const BaseSemantics::SValuePtr&,
                                              SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpSquareRoot(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr fpRoundTowardZero(const BaseSemantics::SValuePtr&, SgAsmFloatType*) override;
    virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr&, SgAsmType*) override;
    virtual BaseSemantics::SValuePtr readRegister(RegisterDescriptor reg,
                                                  const BaseSemantics::SValuePtr &dflt) override;
    virtual BaseSemantics::SValuePtr peekRegister(RegisterDescriptor reg,
                                                  const BaseSemantics::SValuePtr &dflt) override;
    virtual void writeRegister(RegisterDescriptor reg, const BaseSemantics::SValuePtr &a) 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;
};
 
} // namespace
} // namespace
} // namespace
} // namespace
 
#endif
#endif