SemanticCallbacks.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
#define ROSE_BinaryAnalysis_ModelChecker_SemanticCallbacks_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER
 
#include <Rose/BinaryAnalysis/ModelChecker/BasicTypes.h>
 
#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
#include <Rose/BinaryAnalysis/SmtSolver.h>
#include <Rose/Yaml.h>
 
#ifdef ROSE_HAVE_YAMLCPP
#include <yaml-cpp/yaml.h>
#endif
 
namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {
 
class SemanticCallbacks {
public:
    using Ptr = SemanticCallbacksPtr;
 
private:
    const SettingsPtr mcSettings_;                      // model checker settings
 
protected:
    SemanticCallbacks() = delete;
    explicit SemanticCallbacks(const SettingsPtr&);
public:
    virtual ~SemanticCallbacks();
 
public:
    // Functions for creating the semantics framework
 
    virtual void reset() {}
 
    SettingsPtr mcSettings() const;
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr protoval();
 
    virtual InstructionSemantics::BaseSemantics::RegisterStatePtr createInitialRegisters() = 0;
 
    virtual InstructionSemantics::BaseSemantics::MemoryStatePtr createInitialMemory() = 0;
 
    virtual InstructionSemantics::BaseSemantics::StatePtr createInitialState();
 
    virtual InstructionSemantics::BaseSemantics::RiscOperatorsPtr createRiscOperators() = 0;
 
    virtual SmtSolverPtr createSolver() = 0;
 
    virtual void attachModelCheckerSolver(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
                                          const SmtSolverPtr&) {}
 
    virtual void initializeState(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
 
    virtual InstructionSemantics::BaseSemantics::DispatcherPtr
    createDispatcher(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) = 0;
 
    // State query functions
 
    virtual InstructionSemantics::BaseSemantics::SValuePtr
    instructionPointer(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&) = 0;
 
    struct CodeAddresses {
        InstructionSemantics::BaseSemantics::SValuePtr ip; 
        std::set<rose_addr_t> addresses;                    
        bool isComplete = true;                             
    };
 
    virtual CodeAddresses nextCodeAddresses(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
 
    // Execution tree functions
 
    virtual std::vector<TagPtr>
    preExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
 
    virtual std::vector<TagPtr>
    postExecute(const ExecutionUnitPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);
 
    struct NextUnit {
        ExecutionUnitPtr unit;                          
        SymbolicExpression::Ptr assertion;              
        SmtSolver::Evidence evidence;                   
    };
 
    virtual std::vector<NextUnit>
    nextUnits(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolverPtr&) = 0;
 
    // Path creation functions.
 
#ifdef ROSE_HAVE_YAMLCPP
    virtual std::list<ExecutionUnitPtr>
    parsePath(const YAML::Node&, const std::string &sourceName) = 0;
#endif
    virtual std::list<ExecutionUnitPtr>
    parsePath(const Yaml::Node&, const std::string &sourceName) = 0;
};
 
} // namespace
} // namespace
} // namespace
 
#endif
#endif