ModelChecker/Engine.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_Engine_H
#define ROSE_BinaryAnalysis_ModelChecker_Engine_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_MODEL_CHECKER

#include <Rose/BinaryAnalysis/ModelChecker/PathQueue.h>

#include <Rose/BinaryAnalysis/InstructionSemantics/BaseSemantics/BasicTypes.h>
#include <Rose/BinaryAnalysis/SmtSolver.h>
#include <Rose/BinaryAnalysis/Partitioner2/BasicTypes.h>
#include <Sawyer/Stopwatch.h>
#include <boost/filesystem.hpp>
#include <boost/thread/thread.hpp>
#include <thread>

namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {

class Engine final {
    // Types
public:
    using Ptr = EnginePtr;

    struct InProgress {
        InProgress();
        explicit InProgress(const PathPtr&);
        ~InProgress();

        PathPtr path;                                   
        Sawyer::Stopwatch elapsed;                      
        boost::thread::id threadId;                     
        int tid = 0;                                    
    };

    // Data members
private:
    PathQueue frontier_;                                // paths with work remaining
    PathQueue interesting_;                             // paths that are interesting, placed here by workers
    SemanticCallbacksPtr semantics_;                    // various configurable semantic operations

    mutable SAWYER_THREAD_TRAITS::Mutex mutex_;         // protects all following data members
    Sawyer::Container::Map<boost::thread::id, InProgress> inProgress_;// work that is in progress
    SAWYER_THREAD_TRAITS::ConditionVariable newWork_;   // signaled when work arrives or thread finishes
    SAWYER_THREAD_TRAITS::ConditionVariable newInteresting_; // signaled when interesting paths arrive or threads finish
    PathPredicatePtr frontierPredicate_;                // predicate for inserting paths into the "frontier" queue
    PathPredicatePtr interestingPredicate_;             // predicate for inserting paths into the "interesting" queue
    SettingsPtr settings_;                              // overall settings
    std::vector<std::thread> workers_;                  // managed worker threads
    size_t workCapacity_ = 0;                           // managed workers plus user threads
    size_t nWorking_ = 0;                               // number of threads currently doing work
    size_t nPathsExplored_ = 0;                         // number of path nodes executed, i.e., number of paths explored
    size_t nStepsExplored_ = 0;                         // number of steps executed
    bool stopping_ = false;                             // when true, workers stop even if there is still work remaining
    std::vector<std::pair<double, size_t>> fanout_;     // total fanout and number of nodes for each level of the forest
    size_t nFanoutRoots_ = 0;                           // number of execution trees for calculating total forest size
    Sawyer::Stopwatch elapsedTime_;                     // time since model checking started
    mutable Sawyer::Stopwatch timeSinceStats_;          // time since last statistics were reported
    mutable size_t nPathsStats_ = 0;                    // number of paths reported in last statistics output
    size_t nExpressionsTrimmed_ = 0;                    // number of symbolic expressions trimmed down to a new variable
    WorkerStatusPtr workerStatus_;                      // mostly for debugging

protected:
    Engine() = delete;
    explicit Engine(const SettingsPtr&);

public:
    static Ptr instance();

    static Ptr instance(const SettingsPtr&);

    ~Engine();

    // Configuration functions
public:
    SettingsPtr settings() const;
    void settings(const SettingsPtr&);
    SemanticCallbacksPtr semantics() const;
    void semantics(const SemanticCallbacksPtr&);
    PathPrioritizerPtr explorationPrioritizer() const;
    void explorationPrioritizer(const PathPrioritizerPtr&);
    PathPredicatePtr explorationPredicate() const;
    void explorationPredicate(const PathPredicatePtr&);
    PathPredicatePtr interestingPredicate() const;
    void interestingPredicate(const PathPredicatePtr&);
    // Initialization functions
public:
    void reset();

    void insertStartingPoint(const ExecutionUnitPtr&);
    void insertStartingPoint(const PathPtr&);
    // Model checker execution
public:
    void startWorkers(size_t n = 0);

    void run();

    void stop();

    bool step();

    bool workRemains() const;

    size_t workCapacity() const;

    size_t nWorking() const;

    size_t nPathsPending() const;

    // Model checker status
public:
    Sawyer::Stopwatch elapsedTime() const;

    size_t nPathsExplored() const;

    size_t nStepsExplored() const;

    const PathQueue& pendingPaths() const;

    std::vector<InProgress> inProgress() const;

    size_t nExpressionsTrimmed() const;

    void showStatistics(std::ostream&, const std::string &prefix = "") const;

    boost::filesystem::path workerStatusFile() const;
    void workerStatusFile(const boost::filesystem::path&);
    // Model checker results
public:
    const PathQueue& interesting() const;
    PathQueue& interesting();
    PathPtr takeNextInteresting();

    bool insertInteresting(const PathPtr&);

    double estimatedForestSize(size_t k) const;

    // Worker functions. It is useful to call these from user code.
public:
    bool insertWork(const PathPtr&);

    // Internal stuff.
private:
    // Update the fanout parameters used to estimate execution tree size.  The nChildren are the number of new paths created by
    // extending the current path, totalSteps is the number of steps in the whole path, and lastSteps is the number of steps in
    // the last node of the path.
    void updateFanout(size_t nChildren, size_t totalSteps, size_t lastSteps);

    // Called by each worker thread when they start. Users should not call this even though it's public. The ID is the index
    // of the managed worker in the workers_ vector.
    void worker(size_t id, const Progress::Ptr&);

    // Change state. The thread should hold its current state in a local variable. The state transition edges affect how
    // various counters are updated. All threads must start by initializing their current state to STARTING and then calling
    // changeState to also specify the new state is STARTING. Only certain transitions are allowed--read the source.
    void changeState(size_t workerId, WorkerState &currentState, WorkerState newState);

    // Non-synchronized version of changeState
    void changeStateNS(size_t workerId, WorkerState &currentState, WorkerState newState);

    // Do things that should be done when work is started.
    void startWorkingNS();

    // Called by changeState when a worker has finished.
    void finishWorkingNS();

    // Get the next path on which to work.  This function blocks until either more work is available, or no more work can
    // possibly be available. In the former case, it removes the highest priority path from the work queue, changes the work
    // state to WORKING, and returns the path. In the latter case, it returns a null pointer.
    //
    // Thread safety: This method is thread safe.
    PathPtr takeNextWorkItem(size_t workerId, WorkerState&);

    // Non-blocking version of takeNextWorkItem.
    PathPtr takeNextWorkItemNow(WorkerState&);

    // Execute a path. This goes back as far as necessary to get a known state, and then executes from there to the end
    // of the path.
    //
    // After a path is executed, it is conditionally added to the "interesting" queue according to the @ref
    // interestingPredicate.
    //
    // The solver argument is the solver used by model checker, which might be different than the optional solver already
    // attached to the RiscOperators object.
    //
    // Thread safety: The RISC operators must be thread-local, otherwise thread safe. All paths will have an identical
    // set of states for this path after this returns.
    void execute(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);

    // Produce more work, typically by looking at the instruction pointer register for the outgoing state of a previous
    // path (which is not currently in the work queue) and creating new paths.
    void extend(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);

    // Perform one step of model checking.
    void doOneStep(const PathPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&, const SmtSolver::Ptr&);

    // Indicates that a path has been finished.
    //
    // This should be called by a worker thread whenever its work on a path finishes, regardless of whether the work was
    // successful or not.  It removes the path from the @ref inProgress list.
    //
    // Thread safety: This method is thread safe.
    void finishPath(const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&);

    // Display diagnostics about where variables appear in path constraints.
    void displaySmtAssertions(const PathPtr&);
};


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

#endif
#endif