P2Model.h

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

#include <Rose/BinaryAnalysis/ModelChecker/SemanticCallbacks.h>
#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
#include <Sawyer/CommandLine.h>
#include <Sawyer/Stack.h>
#include <Rose/BinaryAnalysis/InstructionSemantics2/SymbolicSemantics.h>

namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {

namespace P2Model {

// Settings for this model checker

struct Settings {
    enum class MemoryType {
        LIST,                                           
        MAP                                             
    };

    TestMode nullRead = TestMode::MUST;                 
    TestMode nullWrite = TestMode::MUST;                
    TestMode oobRead = TestMode::OFF;                   
    TestMode oobWrite = TestMode::OFF;                  
    TestMode uninitVar = TestMode::OFF;                 
    rose_addr_t maxNullAddress = 4095;                  
    bool debugNull = false;                             
    Sawyer::Optional<rose_addr_t> initialStackVa;       
    MemoryType memoryType = MemoryType::MAP;            
    bool solverMemoization = false;                     
    bool traceSemantics = false;                        
};

class SemanticCallbacks;

void commandLineDebugSwitches(Sawyer::CommandLine::SwitchGroup&, Settings&);

Sawyer::CommandLine::SwitchGroup commandLineModelSwitches(Settings&);

Sawyer::CommandLine::SwitchGroup commandLineSwitches(Settings&);

// Function call stack

class FunctionCall {
    Partitioner2::FunctionPtr function_;
    rose_addr_t initialStackPointer_ = 0;
    rose_addr_t framePointerDelta_ = (rose_addr_t)(-4); // Normal frame pointer w.r.t. initial stack pointer
    Sawyer::Optional<rose_addr_t> returnAddress_;
    Variables::StackVariables stackVariables_;

public:
    ~FunctionCall();
    FunctionCall(const Partitioner2::FunctionPtr&, rose_addr_t initialSp, Sawyer::Optional<rose_addr_t> returnAddress,
                 const Variables::StackVariables&);

    Partitioner2::FunctionPtr function() const;

    rose_addr_t initialStackPointer() const;

    const Variables::StackVariables& stackVariables() const;

    rose_addr_t framePointerDelta() const;
    void framePointerDelta(rose_addr_t);
    rose_addr_t framePointer(size_t nBits) const;

    Sawyer::Optional<rose_addr_t> returnAddress() const;
    void returnAddress(Sawyer::Optional<rose_addr_t>);
    std::string printableName(size_t nBits) const;
};

using FunctionCallStack = Sawyer::Container::Stack<FunctionCall>;

// Instruction semantics value

class SValue: public InstructionSemantics2::SymbolicSemantics::SValue {
public:
    using Super = InstructionSemantics2::SymbolicSemantics::SValue;

    using Ptr = SValuePtr;

private:
    AddressInterval region_;

#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);
        s & BOOST_SERIALIZATION_NVP(region_);
    }
#endif

public:
    ~SValue();

protected:
    SValue();

    SValue(size_t nBits, uint64_t number);

    explicit SValue(const SymbolicExpr::Ptr&);

public:
    static Ptr instance();

    static Ptr instanceBottom(size_t nBits);

    static Ptr instanceUndefined(size_t nBits);

    static Ptr instanceUnspecified(size_t nBits);

    static Ptr instanceInteger(size_t nBits, uint64_t value);

    static Ptr instanceSymbolic(const SymbolicExpr::Ptr &value);

public:
    virtual InstructionSemantics2::BaseSemantics::SValuePtr bottom_(size_t nBits) const override {
        return instanceBottom(nBits);
    }

    virtual InstructionSemantics2::BaseSemantics::SValuePtr undefined_(size_t nBits) const override {
        return instanceUndefined(nBits);
    }

    virtual InstructionSemantics2::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override {
        return instanceUnspecified(nBits);
    }

    virtual InstructionSemantics2::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override {
        return instanceInteger(nBits, value);
    }

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

    virtual InstructionSemantics2::BaseSemantics::SValuePtr copy(size_t newNBits = 0) const override;

    virtual Sawyer::Optional<InstructionSemantics2::BaseSemantics::SValuePtr>
    createOptionalMerge(const InstructionSemantics2::BaseSemantics::SValuePtr &other,
                        const InstructionSemantics2::BaseSemantics::MergerPtr&,
                        const SmtSolverPtr&) const override;

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

public:
    AddressInterval region() const;
    void region(const AddressInterval&);
public:
    virtual void print(std::ostream&, InstructionSemantics2::BaseSemantics::Formatter&) const override;
    virtual void hash(Combinatorics::Hasher&) const override;
};

// Instruction semantics state

using StatePtr = boost::shared_ptr<class State>;

class State: public InstructionSemantics2::SymbolicSemantics::State {
public:
    using Super = InstructionSemantics2::SymbolicSemantics::State;

    using Ptr = StatePtr;

private:
    FunctionCallStack callStack_;

protected:
    State();
    State(const InstructionSemantics2::BaseSemantics::RegisterStatePtr&,
          const InstructionSemantics2::BaseSemantics::MemoryStatePtr&);

    // Deep copy
    State(const State&);

public:
    static Ptr instance(const InstructionSemantics2::BaseSemantics::RegisterStatePtr&,
                        const InstructionSemantics2::BaseSemantics::MemoryStatePtr&);

    static Ptr instance(const StatePtr&);

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

    virtual InstructionSemantics2::BaseSemantics::StatePtr clone() const override;

    static Ptr promote(const InstructionSemantics2::BaseSemantics::StatePtr&);

public:
    const FunctionCallStack& callStack() const;
    FunctionCallStack& callStack();
};

// Instruction semantics domain

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

    using Ptr = RiscOperatorsPtr;

private:
    const Settings settings_;
    const Partitioner2::Partitioner &partitioner_;
    SmtSolver::Ptr modelCheckerSolver_;                 // solver used for model checking, different than RISC operators
    size_t nInstructions_ = 0;
    SemanticCallbacks *semantics_ = nullptr;
    AddressInterval stackLimits_;                       // where the stack can exist in memory
    bool computeMemoryRegions_ = false;                 // compute memory regions. This is needed for OOB analysis.

    mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_; // protects the following data m
    Variables::VariableFinderPtr variableFinder_unsync;       // shared by all RiscOperator objects

protected:
    RiscOperators(const Settings&, const Partitioner2::Partitioner&, ModelChecker::SemanticCallbacks*,
                  const InstructionSemantics2::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&,
                  const Variables::VariableFinderPtr&);

public: // Standard public construction-like functions
    ~RiscOperators();

    static Ptr instance(const Settings&, const Partitioner2::Partitioner&, ModelChecker::SemanticCallbacks*,
                        const InstructionSemantics2::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&,
                        const Variables::VariableFinderPtr&);

    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics2::BaseSemantics::SValuePtr&, const SmtSolverPtr&) const override;

    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics2::BaseSemantics::StatePtr&, const SmtSolverPtr&) const override;

    static Ptr promote(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &x);

public: // Supporting functions
    const Partitioner2::Partitioner& partitioner() const;

    SmtSolver::Ptr modelCheckerSolver() const;
    void modelCheckerSolver(const SmtSolver::Ptr&);
    bool computeMemoryRegions() const;
    void computeMemoryRegions(bool);
    void checkNullAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode);

    void checkOobAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes);

    void checkUninitVar(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode, size_t nBytes);

    size_t nInstructions() const;
    void nInstructions(size_t);
    void maybeInitCallStack(rose_addr_t insnVa);

    void pushCallStack(const Partitioner2::FunctionPtr &callee, rose_addr_t initialSp, Sawyer::Optional<rose_addr_t> returnVa);

    void popCallStack();

    size_t pruneCallStack();

    void printCallStack(std::ostream&, const std::string &prefix);

    InstructionSemantics2::BaseSemantics::SValuePtr
    assignRegion(const InstructionSemantics2::BaseSemantics::SValuePtr &result);

    InstructionSemantics2::BaseSemantics::SValuePtr
    assignRegion(const InstructionSemantics2::BaseSemantics::SValuePtr &result,
                 const InstructionSemantics2::BaseSemantics::SValuePtr &a);

    InstructionSemantics2::BaseSemantics::SValuePtr
    assignRegion(const InstructionSemantics2::BaseSemantics::SValuePtr &result,
                 const InstructionSemantics2::BaseSemantics::SValuePtr &a,
                 const InstructionSemantics2::BaseSemantics::SValuePtr &b);
public: // Override RISC operations
    virtual void finishInstruction(SgAsmInstruction*) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    number_(size_t nBits, uint64_t value) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    extract(const InstructionSemantics2::BaseSemantics::SValuePtr&, size_t begin, size_t end) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    concat(const InstructionSemantics2::BaseSemantics::SValuePtr &lowBits,
           const InstructionSemantics2::BaseSemantics::SValuePtr &highBits) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    shiftLeft(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
              const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    shiftRight(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
               const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    shiftRightArithmetic(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
                         const InstructionSemantics2::BaseSemantics::SValuePtr &nBits) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    unsignedExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    signExtend(const InstructionSemantics2::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    add(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
        const InstructionSemantics2::BaseSemantics::SValuePtr &b) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    addCarry(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
             const InstructionSemantics2::BaseSemantics::SValuePtr &b,
             InstructionSemantics2::BaseSemantics::SValuePtr &carryOut /*out*/,
             InstructionSemantics2::BaseSemantics::SValuePtr &overflowed /*out*/) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    subtract(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
             const InstructionSemantics2::BaseSemantics::SValuePtr &b) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    subtractCarry(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
                  const InstructionSemantics2::BaseSemantics::SValuePtr &b,
                  InstructionSemantics2::BaseSemantics::SValuePtr &carryOut /*out*/,
                  InstructionSemantics2::BaseSemantics::SValuePtr &overflowed /*out*/) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    addWithCarries(const InstructionSemantics2::BaseSemantics::SValuePtr &a,
                   const InstructionSemantics2::BaseSemantics::SValuePtr &b,
                   const InstructionSemantics2::BaseSemantics::SValuePtr &c,
                   InstructionSemantics2::BaseSemantics::SValuePtr &carryOut /*out*/) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    readRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr&) override;

    virtual void
    writeRegister(RegisterDescriptor, const InstructionSemantics2::BaseSemantics::SValuePtr&) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    readMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics2::BaseSemantics::SValuePtr &dflt,
               const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override;

    virtual void
    writeMemory(RegisterDescriptor segreg, const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
                const InstructionSemantics2::BaseSemantics::SValuePtr &value,
                const InstructionSemantics2::BaseSemantics::SValuePtr &cond) override;
};

// High-level semantic operations

class SemanticCallbacks: public Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks {
public:
    using Ptr = SemanticCallbacksPtr;
    using UnitCounts = Sawyer::Container::Map<rose_addr_t, size_t>;

private:
    Settings settings_;                                 // settings are set by the constructor and not modified thereafter
    const Partitioner2::Partitioner &partitioner_;      // generally shouldn't be changed once model checking starts
    SmtSolver::Memoizer::Ptr smtMemoizer_;              // memoizer shared among all solvers

    mutable SAWYER_THREAD_TRAITS::Mutex unitsMutex_;    // protects only the units_ data member
    Sawyer::Container::Map<rose_addr_t, ExecutionUnitPtr> units_; // cached execution units

    mutable SAWYER_THREAD_TRAITS::Mutex mutex_;         // protects the following data members
    std::set<uint64_t> seenStates_;                     // states we've seen, by hash
    size_t nDuplicateStates_ = 0;                       // number of times a previous state is seen again
    size_t nSolverFailures_ = 0;                        // number of times the SMT solver failed
    UnitCounts unitsReached_;                           // number of times basic blocks were reached
    Variables::VariableFinderPtr variableFinder_;       // also shared by all RiscOperator objects

    // This model is able to follow a single path specified by the user. In order to do that, the user should call
    // followOnePath to provide the ordered list of execution units. The nextCodeAddresses function is overridden to
    // return only the address of the next execution unit in this list, or none when the list is empty. The findUnit
    // function is enhanced to return the next execution unit and remove it from the list.
    //
    // These are also protected by mutex_
    bool followingOnePath_ = false;
    std::list<ExecutionUnitPtr> onePath_;               // execution units yet to be consumed by findUnit

protected:
    SemanticCallbacks(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::Partitioner&);
public:
    ~SemanticCallbacks();

public:
    static Ptr instance(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::Partitioner&);

public:
    const Partitioner2::Partitioner& partitioner() const;

public:
    void followOnePath(const std::list<ExecutionUnitPtr>&);

    bool followingOnePath() const;
    void followingOnePath(bool);
    SmtSolver::Memoizer::Ptr smtMemoizer() const;
    void smtMemoizer(const SmtSolver::Memoizer::Ptr&);
    size_t nDuplicateStates() const;

    size_t nSolverFailures() const;

    size_t nUnitsReached() const;

    UnitCounts unitsReached() const;

    virtual bool filterNullDeref(const InstructionSemantics2::BaseSemantics::SValuePtr &addr, SgAsmInstruction*,
                                 TestMode testMode, IoMode ioMode);

    virtual bool filterOobAccess(const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
                                 const AddressInterval &referencedRegion, const AddressInterval &accessedRegion,
                                 SgAsmInstruction *insn, TestMode testMode, IoMode ioMode,
                                 const Variables::StackVariable &intendedVariable, const AddressInterval &intendedVariableLocation,
                                 const Variables::StackVariable &accessedVariable, const AddressInterval &accessedVariableLocation);

    virtual bool filterUninitVar(const InstructionSemantics2::BaseSemantics::SValuePtr &addr,
                                 const AddressInterval &referencedREgion, const AddressInterval &accessedRegion,
                                 SgAsmInstruction *insn, TestMode testMode, const Variables::StackVariable &variable,
                                 const AddressInterval &variableLocation);

public:
    virtual void reset() override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr protoval() override;

    virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr createInitialRegisters() override;

    virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr createInitialMemory() override;

    virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState() override;

    virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr createRiscOperators() override;

    virtual void
    initializeState(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;

    virtual InstructionSemantics2::BaseSemantics::DispatcherPtr
    createDispatcher(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;

    virtual SmtSolver::Ptr createSolver() override;

    virtual void attachModelCheckerSolver(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&,
                                          const SmtSolver::Ptr&) override;

    virtual CodeAddresses
    nextCodeAddresses(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;

    virtual std::vector<TagPtr>
    preExecute(const ExecutionUnitPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;

    virtual std::vector<TagPtr>
    postExecute(const ExecutionUnitPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;

    virtual InstructionSemantics2::BaseSemantics::SValuePtr
    instructionPointer(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&) override;

    virtual std::vector<NextUnit>
    nextUnits(const PathPtr&, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&) override;

#ifdef ROSE_HAVE_YAMLCPP
    virtual std::list<ExecutionUnitPtr>
    parsePath(const YAML::Node&, const std::string &sourceName) override;
#endif

    virtual std::list<ExecutionUnitPtr>
    parsePath(const Yaml::Node&, const std::string &sourceName) override;

private:
    // Records the state hash and returns true if we've seen it before.
    bool seenState(const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr&);

    // Find and cache the execution unit at the specified address.
    ExecutionUnitPtr findUnit(rose_addr_t va, const Progress::Ptr&);
};

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

#endif
#endif