TaintSemantics.h

#ifndef ROSE_BinaryAnalysis_InstructionSemantics_TaintSemantics_H
#define ROSE_BinaryAnalysis_InstructionSemantics_TaintSemantics_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS
#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>

#include <Rose/BinaryAnalysis/BasicTypes.h>
#include <Rose/BinaryAnalysis/SymbolicExpression.h>

namespace Rose {
namespace BinaryAnalysis {              // documented elsewhere
namespace InstructionSemantics {        // documented elsewhere

namespace TaintSemantics {

enum class Taintedness {
    BOTTOM,                                             
    UNTAINTED,                                          
    TAINTED,                                            
    TOP                                                 
};

using ExprPtr = SymbolicSemantics::ExprPtr;
using ExprNode = SymbolicSemantics::ExprNode;

//                                      Merging values

using Merger = SymbolicSemantics::Merger;

using MergerPtr = Sawyer::SharedPointer<Merger>;


//                                      Semantic values

using SValuePtr = Sawyer::SharedPointer<class SValue>;

using Formatter = SymbolicSemantics::Formatter;

class SValue: public SymbolicSemantics::SValue {
    Taintedness taintedness_ = Taintedness::BOTTOM;

public:
    using Super = SymbolicSemantics::SValue;

    using Ptr = SValuePtr;

protected:
    // 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:
    SValue() {}                                         // needed for serialization

    explicit SValue(size_t nbits): Super(nbits) {}

    SValue(size_t nbits, uint64_t number): Super(nbits, number) {}

    SValue(ExprPtr expr): Super(expr) {}

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

    static SValuePtr instance_bottom(size_t nbits) {
        return SValuePtr(new SValue(SymbolicExpression::makeIntegerVariable(nbits, "", ExprNode::BOTTOM)));
    }

    static SValuePtr instance_undefined(size_t nbits) {
        return SValuePtr(new SValue(SymbolicExpression::makeIntegerVariable(nbits)));
    }

    static SValuePtr instance_unspecified(size_t nbits) {
        return SValuePtr(new SValue(SymbolicExpression::makeIntegerVariable(nbits, "", ExprNode::UNSPECIFIED)));
    }

    static SValuePtr instance_integer(size_t nbits, uint64_t value) {
        return SValuePtr(new SValue(SymbolicExpression::makeIntegerConstant(nbits, value)));
    }

    static SValuePtr instance_symbolic(const SymbolicExpression::Ptr &value) {
        ASSERT_not_null(value);
        return SValuePtr(new SValue(value));
    }

    // Virtual allocating constructors
public:
    virtual BaseSemantics::SValuePtr bottom_(size_t nbits) const override {
        return instance_bottom(nbits);
    }

    /*  Instantiate a new data-flow bottom value of specified width.
     *
     *  The symbolic value is what is set to bottom in this case. The taintedness is always set to bottom by all the static
     *  allocating constructors. If you need a different taintedness then you need to change it with the @ref taintedness
     *  property. */
    virtual BaseSemantics::SValuePtr undefined_(size_t nbits) const override {
        return instance_undefined(nbits);
    }

    virtual BaseSemantics::SValuePtr unspecified_(size_t nbits) const override {
        return instance_unspecified(nbits);
    }

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

    virtual BaseSemantics::SValuePtr boolean_(bool value) const override {
        return instance_integer(1, value?1:0);
    }

    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;

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

    // Override virtual methods...
public:
    virtual void print(std::ostream&, BaseSemantics::Formatter&) const override;

    virtual void hash(Combinatorics::Hasher&) const override;

protected: // when implementing use these names; but when calling, use the camelCase names
    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;


    // Additional methods first declared in this class...
public:
    Taintedness taintedness() const;
    void taintedness(Taintedness);
public:
    // Merge two taintedness values
    static Taintedness mergeTaintedness(Taintedness, Taintedness);
};


//                                      Register state

using RegisterState = SymbolicSemantics::RegisterState;
using RegisterStatePtr = SymbolicSemantics::RegisterStatePtr;


//                                      Memory state

using MemoryListState = SymbolicSemantics::MemoryListState;
using MemoryListStatePtr = SymbolicSemantics::MemoryListStatePtr;

using MemoryMapState = SymbolicSemantics::MemoryMapState;
using MemoryMapStatePtr = SymbolicSemantics::MemoryMapStatePtr;

using MemoryState = MemoryListState;
using MemoryStatePtr = MemoryListStatePtr;


//                                      Complete state

using State = SymbolicSemantics::State;
using StatePtr = SymbolicSemantics::StatePtr;


//                                      RISC operators

using RiscOperatorsPtr = boost::shared_ptr<class RiscOperators>;

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

    using Ptr = RiscOperatorsPtr;

    // 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 BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&);

    explicit RiscOperators(const BaseSemantics::StatePtr&, const SmtSolverPtr&);

    // Static allocating constructors
public:
    ~RiscOperators();

    static RiscOperatorsPtr instanceFromRegisters(const RegisterDictionaryPtr&, const SmtSolverPtr &solver = SmtSolverPtr());

    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&);

    // Override methods from base class.  These are the RISC operators that are invoked by a Dispatcher.
public:
    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 iteWithStatus(const BaseSemantics::SValuePtr &sel_,
                                                   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/*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 fpConvert(const BaseSemantics::SValuePtr &a, SgAsmFloatType *aType,
                                               SgAsmFloatType *retType) override;
    virtual BaseSemantics::SValuePtr reinterpret(const BaseSemantics::SValuePtr&, SgAsmType*) override;

private:
    static Taintedness mergeTaintedness(const BaseSemantics::SValuePtr&, const BaseSemantics::SValue::Ptr&);
};

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

#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::SValue);
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::InstructionSemantics::TaintSemantics::RiscOperators);
#endif

#endif
#endif