InputVariables.h

#ifndef ROSE_BinaryAnalysis_Concolic_InputVariables_H
#define ROSE_BinaryAnalysis_Concolic_InputVariables_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_CONCOLIC_TESTING
#include <Rose/BinaryAnalysis/Concolic/BasicTypes.h>

#include <Rose/BinaryAnalysis/SymbolicExpr.h>

namespace Rose {
namespace BinaryAnalysis {
namespace Concolic {

class InputVariables: public Sawyer::SharedObject {
public:
    using Ptr = InputVariablesPtr;

private:
    using Variables = Sawyer::Container::Map<uint64_t, ExecutionEventPtr>; // map symbolic variable ID to program input
    Variables variables_;
    SymbolicExpr::ExprExprHashMap bindings_;      // used for substitutions

    // Constructors, etc.
protected:
    InputVariables();

public:
    static Ptr instance();

    ~InputVariables();

    // Properties and queries
public:

    const SymbolicExpr::ExprExprHashMap& bindings() const;

    ExecutionEventPtr event(const std::string &variableName) const;
    ExecutionEventPtr event(const SymbolicExprPtr &variable) const;
    // High-level functions.

    void activate(const ExecutionEventPtr&, InputType, size_t idx1 = INVALID_INDEX, size_t idx2 = INVALID_INDEX);

    void deactivate(const ExecutionEventPtr&);

    void playback(const ExecutionEventPtr&);

    void unplayback(const ExecutionEventPtr&);

    void addBindingsToSolver(const SmtSolverPtr&) const;

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

    // Mid-level functions

    void define(const ExecutionEventPtr&, InputType, size_t idx1 = INVALID_INDEX, size_t idx2 = INVALID_INDEX);

    void undefine(const ExecutionEventPtr&);

    void bind(const ExecutionEventPtr&);

    void unbind(const ExecutionEventPtr&);

    // Low-level functions.

    void bindVariableValue(const SymbolicExprPtr &variable, const SymbolicExprPtr &value);

    void unbindVariableValue(const SymbolicExprPtr &variable);
};

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

#endif
#endif