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/Types.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