PartitionerModel.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
#define ROSE_BinaryAnalysis_ModelChecker_PartitionerModel_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER
 
#include <Rose/BinaryAnalysis/InstructionSemantics/SymbolicSemantics.h>
#include <Rose/BinaryAnalysis/ModelChecker/SemanticCallbacks.h>
#include <Rose/BinaryAnalysis/ModelChecker/Variables.h>
#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
#include <Rose/BinaryAnalysis/Variables.h>
 
#include <Sawyer/CommandLine.h>
#include <Sawyer/Stack.h>
 
namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {
 
namespace PartitionerModel {
 
// 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 InstructionSemantics::SymbolicSemantics::SValue {
public:
    using Super = InstructionSemantics::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 SymbolicExpression::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 SymbolicExpression::Ptr &value);
 
public:
    virtual InstructionSemantics::BaseSemantics::SValuePtr bottom_(size_t nBits) const override;
    virtual InstructionSemantics::BaseSemantics::SValuePtr undefined_(size_t nBits) const override;
    virtual InstructionSemantics::BaseSemantics::SValuePtr unspecified_(size_t nBits) const override;
    virtual InstructionSemantics::BaseSemantics::SValuePtr number_(size_t nBits, uint64_t value) const override;
    virtual InstructionSemantics::BaseSemantics::SValuePtr boolean_(bool value) const override;
    virtual InstructionSemantics::BaseSemantics::SValuePtr copy(size_t newNBits = 0) const override;
 
    virtual Sawyer::Optional<InstructionSemantics::BaseSemantics::SValuePtr>
    createOptionalMerge(const InstructionSemantics::BaseSemantics::SValuePtr &other,
                        const InstructionSemantics::BaseSemantics::MergerPtr&,
                        const SmtSolverPtr&) const override;
 
public:
    static Ptr promote(const InstructionSemantics::BaseSemantics::SValuePtr&);
 
public:
    AddressInterval region() const;
    void region(const AddressInterval&);
public:
    virtual void print(std::ostream&, InstructionSemantics::BaseSemantics::Formatter&) const override;
    virtual void hash(Combinatorics::Hasher&) const override;
};
 
// Instruction semantics state
 
using StatePtr = boost::shared_ptr<class State>;
 
class State: public InstructionSemantics::SymbolicSemantics::State {
public:
    using Super = InstructionSemantics::SymbolicSemantics::State;
 
    using Ptr = StatePtr;
 
private:
    FunctionCallStack callStack_;
 
protected:
    State();
    State(const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
          const InstructionSemantics::BaseSemantics::MemoryStatePtr&);
 
    // Deep copy
    State(const State&);
 
public:
    static Ptr instance(const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
                        const InstructionSemantics::BaseSemantics::MemoryStatePtr&);
 
    static Ptr instance(const StatePtr&);
 
    virtual InstructionSemantics::BaseSemantics::StatePtr
    create(const InstructionSemantics::BaseSemantics::RegisterStatePtr&,
           const InstructionSemantics::BaseSemantics::MemoryStatePtr&) const override;
 
    virtual InstructionSemantics::BaseSemantics::StatePtr clone() const override;
 
    static Ptr promote(const InstructionSemantics::BaseSemantics::StatePtr&);
 
public:
    const FunctionCallStack& callStack() const;
    FunctionCallStack& callStack();
};
 
// Instruction semantics domain
 
class RiscOperators: public InstructionSemantics::SymbolicSemantics::RiscOperators {
public:
    using Super = InstructionSemantics::SymbolicSemantics::RiscOperators;
 
    using Ptr = RiscOperatorsPtr;
 
private:
    const Settings settings_;
    Partitioner2::PartitionerConstPtr partitioner_;     // not null
    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.
    const Variables::GlobalVariables &gvars_;
 
    mutable SAWYER_THREAD_TRAITS::Mutex variableFinderMutex_; // protects the following data members
    Variables::VariableFinderPtr variableFinder_unsync;       // shared by all RiscOperator objects
 
protected:
    RiscOperators(const Settings&, const Partitioner2::PartitionerConstPtr&, ModelChecker::SemanticCallbacks*,
                  const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&,
                  const Variables::VariableFinderPtr&, const Variables::GlobalVariables&);
 
public: // Standard public construction-like functions
    ~RiscOperators();
 
    static Ptr instance(const Settings&, const Partitioner2::PartitionerConstPtr&, ModelChecker::SemanticCallbacks*,
                        const InstructionSemantics::BaseSemantics::SValuePtr &protoval, const SmtSolverPtr&,
                        const Variables::VariableFinderPtr&, const Variables::GlobalVariables&);
 
    virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics::BaseSemantics::SValuePtr&, const SmtSolverPtr&) const override;
 
    virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr
    create(const InstructionSemantics::BaseSemantics::StatePtr&, const SmtSolverPtr&) const override;
 
    static Ptr promote(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &x);
 
public: // Supporting functions
    Partitioner2::PartitionerConstPtr partitioner() const;
 
    SmtSolver::Ptr modelCheckerSolver() const;
    void modelCheckerSolver(const SmtSolver::Ptr&);
    bool computeMemoryRegions() const;
    void computeMemoryRegions(bool);
    void checkNullAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode);
 
    void checkOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr, TestMode, IoMode, size_t nBytes);
 
    void checkUninitVar(const InstructionSemantics::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);
 
    InstructionSemantics::BaseSemantics::SValuePtr
    assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result);
 
    InstructionSemantics::BaseSemantics::SValuePtr
    assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result,
                 const InstructionSemantics::BaseSemantics::SValuePtr &a);
 
    InstructionSemantics::BaseSemantics::SValuePtr
    assignRegion(const InstructionSemantics::BaseSemantics::SValuePtr &result,
                 const InstructionSemantics::BaseSemantics::SValuePtr &a,
                 const InstructionSemantics::BaseSemantics::SValuePtr &b);
public: // Override RISC operations
    virtual void finishInstruction(SgAsmInstruction*) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    number_(size_t nBits, uint64_t value) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    extract(const InstructionSemantics::BaseSemantics::SValuePtr&, size_t begin, size_t end) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    concat(const InstructionSemantics::BaseSemantics::SValuePtr &lowBits,
           const InstructionSemantics::BaseSemantics::SValuePtr &highBits) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    shiftLeft(const InstructionSemantics::BaseSemantics::SValuePtr &a,
              const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    shiftRight(const InstructionSemantics::BaseSemantics::SValuePtr &a,
               const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    shiftRightArithmetic(const InstructionSemantics::BaseSemantics::SValuePtr &a,
                         const InstructionSemantics::BaseSemantics::SValuePtr &nBits) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    unsignedExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    signExtend(const InstructionSemantics::BaseSemantics::SValue::Ptr &a, size_t newWidth) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    add(const InstructionSemantics::BaseSemantics::SValuePtr &a,
        const InstructionSemantics::BaseSemantics::SValuePtr &b) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    addCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a,
             const InstructionSemantics::BaseSemantics::SValuePtr &b,
             InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/,
             InstructionSemantics::BaseSemantics::SValuePtr &overflowed /*out*/) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    subtract(const InstructionSemantics::BaseSemantics::SValuePtr &a,
             const InstructionSemantics::BaseSemantics::SValuePtr &b) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    subtractCarry(const InstructionSemantics::BaseSemantics::SValuePtr &a,
                  const InstructionSemantics::BaseSemantics::SValuePtr &b,
                  InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/,
                  InstructionSemantics::BaseSemantics::SValuePtr &overflowed /*out*/) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    addWithCarries(const InstructionSemantics::BaseSemantics::SValuePtr &a,
                   const InstructionSemantics::BaseSemantics::SValuePtr &b,
                   const InstructionSemantics::BaseSemantics::SValuePtr &c,
                   InstructionSemantics::BaseSemantics::SValuePtr &carryOut /*out*/) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    readRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
 
    virtual void
    writeRegister(RegisterDescriptor, const InstructionSemantics::BaseSemantics::SValuePtr&) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    readMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
               const InstructionSemantics::BaseSemantics::SValuePtr &dflt,
               const InstructionSemantics::BaseSemantics::SValuePtr &cond) override;
 
    virtual void
    writeMemory(RegisterDescriptor segreg, const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                const InstructionSemantics::BaseSemantics::SValuePtr &value,
                const InstructionSemantics::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
    Partitioner2::PartitionerConstPtr partitioner_;     // generally shouldn't be changed once model checking starts, non-null
    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
    Variables::GlobalVariables gvars_;                  // all global variables identified by variableFinder_
 
    // 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::PartitionerConstPtr&);
public:
    ~SemanticCallbacks();
 
public:
    static Ptr instance(const ModelChecker::SettingsPtr&, const Settings&, const Partitioner2::PartitionerConstPtr&);
 
public:
    Partitioner2::PartitionerConstPtr 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 InstructionSemantics::BaseSemantics::SValuePtr &addr, SgAsmInstruction*,
                                 TestMode testMode, IoMode ioMode);
 
    virtual bool filterOobAccess(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                                 const AddressInterval &referencedRegion, const AddressInterval &accessedRegion,
                                 SgAsmInstruction *insn, TestMode testMode, IoMode ioMode,
                                 const FoundVariable &intendedVariable, const FoundVariable &accessedVariable);
 
    virtual bool filterUninitVar(const InstructionSemantics::BaseSemantics::SValuePtr &addr,
                                 const AddressInterval &referencedREgion, const AddressInterval &accessedRegion,
                                 SgAsmInstruction *insn, TestMode testMode, const FoundVariable &accessedVariable);
 
public:
    virtual void reset() override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr protoval() override;
 
    virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters() override;
 
    virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory() override;
 
    virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState() override;
 
    virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators() override;
 
    virtual void
    initializeState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
 
    virtual InstructionSemantics::BaseSemantics::DispatcherPtr
    createDispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
 
    virtual SmtSolver::Ptr createSolver() override;
 
    virtual void attachModelCheckerSolver(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
                                          const SmtSolver::Ptr&) override;
 
    virtual CodeAddresses
    nextCodeAddresses(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
 
    virtual std::vector<TagPtr>
    preExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
 
    virtual std::vector<TagPtr>
    postExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    instructionPointer(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) override;
 
    virtual std::vector<NextUnit>
    nextUnits(const PathPtr&, const InstructionSemantics::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 InstructionSemantics::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