PathNode.h

#ifndef ROSE_BinaryAnalysis_ModelChecker_PathNode_H
#define ROSE_BinaryAnalysis_ModelChecker_PathNode_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/BinaryAnalysis/SymbolicExpression.h>
 
namespace Rose {
namespace BinaryAnalysis {
namespace ModelChecker {
 
class PathNode {
public:
    using Ptr = PathNodePtr;
 
private:
    const Ptr parent_;                                             // Previous node in execution path. Null for root node.
    const ExecutionUnitPtr executionUnit_;                         // The thing to execute, non-null
 
    mutable SAWYER_THREAD_TRAITS::Mutex mutex_;                    // protects all following data members
 
    // Path states are used as follows:
    //
    //    When a path is executed, its incomingState_ is copied, modified by the thread's semantics operators, and the
    //    resulting state is stored as outgoingState_. The incomingState_ (which is shared among paths, see next bullet) is
    //    then set to null.
    //
    //    When a path is extended by creating new paths each with an additional node, the new nodes' incomingState_ points to
    //    the original path's outgoingState_, then the original path's outgoingState_ is set to null. Thus the new paths all
    //    point to a shared incoming state.
    InstructionSemantics::BaseSemantics::StatePtr incomingState_;  // shared state before execution, then null afterward
    InstructionSemantics::BaseSemantics::StatePtr outgoingState_;  // state after execution, or null if error during execution
 
    bool executionFailed_ = false;                                 // true iff execution failed (and outgoingState_ therefore null)
    std::vector<SymbolicExpression::Ptr> assertions_;              // assertions for the model checker for this node of the path
    SmtSolver::Evidence evidence_;                                 // SMT evidence that path to and including this node is feasible
    std::vector<TagPtr> tags_;                                     // tags associated with this node of the path
    uint32_t id_ = 0;                                              // a random path ID number
    double processingTime_ = NAN;                                  // time required to execute and extend this node
    double sortKey_ = NAN;                                         // field for user-defined sorting
 
protected:
    PathNode() = delete;
 
    PathNode(const ExecutionUnitPtr&);
 
    PathNode(const Ptr &parent, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
             const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);
 
public:
    ~PathNode();
 
public:
    static Ptr instance(const ExecutionUnitPtr&);
 
    static Ptr instance(const Ptr &parent, const ExecutionUnitPtr&, const SymbolicExpression::Ptr &assertion,
                        const SmtSolver::Evidence&, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState);
 
    uint32_t id() const;
 
    double sortKey() const;
    void sortKey(double);
    Ptr parent() const;
 
    ExecutionUnitPtr executionUnit() const;
 
    size_t nSteps() const;
 
    void assertion(const SymbolicExpression::Ptr&);
 
    std::vector<SymbolicExpression::Ptr> assertions() const;
 
    SmtSolver::Evidence evidence() const;
 
    void execute(const SettingsPtr&, const SemanticCallbacksPtr&, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr&,
                 const SmtSolver::Ptr&);
 
    bool executionFailed() const;
 
    InstructionSemantics::BaseSemantics::StatePtr copyOutgoingState() const;
 
    class BorrowedOutgoingState {
        friend class PathNode;
    private:
        PathNode* const node;
    public:
        const InstructionSemantics::BaseSemantics::StatePtr state;
    private:
        BorrowedOutgoingState() = delete;
        BorrowedOutgoingState& operator=(const BorrowedOutgoingState&) = delete;
        BorrowedOutgoingState(PathNode*, const InstructionSemantics::BaseSemantics::StatePtr&);
    public:
        ~BorrowedOutgoingState();
    };
 
    BorrowedOutgoingState borrowOutgoingState();
 
    void releaseOutgoingState();
 
    void appendTag(const TagPtr&);
    void appendTags(const std::vector<TagPtr>&);
    size_t nTags() const;
 
    std::vector<TagPtr> tags() const;
 
    double processingTime() const;
 
    void incrementProcessingTime(double seconds);
 
    Sawyer::Optional<rose_addr_t> address() const;
 
    std::string printableName() const;
 
    void toYamlHeader(const SettingsPtr&, std::ostream&, const std::string &prefix) const;
 
    void toYamlSteps(const SettingsPtr&, std::ostream&, const std::string &prefix,
                     size_t stepOrigin, size_t maxSteps) const;
 
    std::vector<Sarif::LocationPtr> toSarif(size_t maxSteps) const;
 
private:
    void restoreOutgoingState(const InstructionSemantics::BaseSemantics::StatePtr&);
};
 
} // namespace
} // namespace
} // namespace
 
#endif
#endif