SmtlibSolver.h

#ifndef ROSE_BinaryAnalysis_SmtlibSolver_H
#define ROSE_BinaryAnalysis_SmtlibSolver_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS

#include <Rose/BinaryAnalysis/SmtSolver.h>
#include <boost/filesystem.hpp>
#include <boost/unordered_map.hpp>

namespace Rose {
namespace BinaryAnalysis {

class SmtlibSolver: public SmtSolver {
private:
    boost::filesystem::path executable_;                // solver program
    std::string shellArgs_;                             // extra arguments for command (passed through shell)
    ExprExprMap varsForSets_;                           // variables to use for sets

protected:
    Sawyer::Optional<boost::chrono::duration<double> > timeout_; // max time for solving a single set of equations in seconds

protected:
    // Reference counted. Use instance() or create() instead.
    explicit SmtlibSolver(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
                          unsigned linkages = LM_EXECUTABLE)
        : SmtSolver(name, linkages), executable_(executable), shellArgs_(shellArgs) {}

public:
    static Ptr instance(const std::string &name, const boost::filesystem::path &executable, const std::string &shellArgs = "",
                        unsigned linkages = LM_EXECUTABLE) {
        return Ptr(new SmtlibSolver(name, executable, shellArgs, linkages));
    }

    virtual Ptr create() const override;

public:
    virtual void reset() override;
    virtual void generateFile(std::ostream&, const std::vector<SymbolicExpression::Ptr> &exprs, Definitions*) override;
    virtual std::string getCommand(const std::string &configName) override;
    virtual std::string getErrorMessage(int exitStatus) override;
    virtual void findVariables(const SymbolicExpression::Ptr&, VariableSet&) override;
    virtual void timeout(boost::chrono::duration<double>) override;

protected:
    void varForSet(const SymbolicExpression::InteriorPtr &set, const SymbolicExpression::LeafPtr &var);
    SymbolicExpression::LeafPtr varForSet(const SymbolicExpression::InteriorPtr &set);
    virtual void parseEvidence() override;

    virtual void outputBvxorFunctions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);

    virtual void outputComparisonFunctions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);

protected:
    // Return the most common type (arbitrarily if tied). Returns NO_TYPE when there are no inputs.
    virtual Type mostType(const std::vector<SExprTypePair>&);

    // Cast an SMT expression(s) to some other type.
    virtual SExprTypePair outputCast(const SExprTypePair&, Type to);
    virtual std::vector<SExprTypePair> outputCast(const std::vector<SExprTypePair>&, Type to);

    virtual std::string typeName(const SymbolicExpression::Ptr&);

    // Convert a ROSE symbolic expression to an SMT solver expression. The return value is a pair consisting of an SExpr::Ptr
    // (ROSE internal representation of an SMT solver expression) and a type indicating whether the SMT solver expression is a
    // bit vector, a Boolean, or a memory state. Although ROSE uses a bit to represent Booleans, SMT solvers often distinguish
    // betwen a single bit and a Boolean.
    virtual SExprTypePair outputExpression(const SymbolicExpression::Ptr&);
    virtual std::vector<SmtSolver::SExprTypePair> outputExpressions(const std::vector<SymbolicExpression::Ptr>&);

    // Create an SMT expression from a ROSE symbolic leaf node (constant, variable, or memory state).
    virtual SExprTypePair outputLeaf(const SymbolicExpression::LeafPtr&);

    // Create an expression composed of only 2-argument calls to the specified function.  The arguments are all first converted
    // to the most common argument type (which is usually a no-op since arguments are normally all the same type). If rettype
    // is NO_TYPE then the returned type is assumed to be the same as the arguments, otherwise it is set as specified.
    virtual SExprTypePair outputLeftAssoc(const std::string &func, const SymbolicExpression::InteriorPtr&, Type rettype = NO_TYPE);
    virtual SExprTypePair outputLeftAssoc(const std::string &func, const std::vector<SExprTypePair>&, Type rettype = NO_TYPE);

    // Create an expression that does a shift operation.
    virtual SExprTypePair outputArithmeticShiftRight(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputLogicalShiftRight0(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputLogicalShiftRight1(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputShiftLeft0(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputShiftLeft1(const SymbolicExpression::InteriorPtr&);

    // Create a rotate expression. */
    virtual SExprTypePair outputRotateLeft(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputRotateRight(const SymbolicExpression::InteriorPtr&);

    // Create an expression that does either a bit-wise or boolean XOR. All arguments must be the same type, either bit vectors
    // or Booleans, and the return value is the same as the argument type.
    virtual SExprTypePair outputXor(const SymbolicExpression::InteriorPtr&);

    // Create a binary expression. This is a special case of outputLeftAssoc.
    virtual SExprTypePair outputBinary(const std::string &func, const SymbolicExpression::InteriorPtr&, Type rettype = NO_TYPE);

    // Create a unary expression.  The return type is the same as the argument type.
    virtual SExprTypePair outputUnary(const std::string &funcName, const SExprTypePair &arg);

    // Create a bit extraction expression, i.e., a bit vector result which is a sub-array of the input bit vector.
    virtual SExprTypePair outputExtract(const SymbolicExpression::InteriorPtr&);

    // Create a widening expression that returns a bit vector type. */
    virtual SExprTypePair outputSignExtend(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputUnsignedExtend(const SymbolicExpression::InteriorPtr&);

    // Create an if-then-else expression. The arguments should be the same type (one is cast if not) and the return type is the
    // same as the argument types.
    virtual SExprTypePair outputIte(const SymbolicExpression::InteriorPtr&);

    // Create a not-equal expression. The operands can be any type and are cast to a common type before comparing. The return
    // type is Boolean.
    virtual SExprTypePair outputNotEqual(const SymbolicExpression::InteriorPtr&);

    // Create a comparison expression for bit vectors. Return type is Boolean. */
    virtual SExprTypePair outputSignedCompare(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputUnsignedCompare(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputZerop(const SymbolicExpression::InteriorPtr&);

    // Create multiplicative expression. */
    virtual SExprTypePair outputMultiply(const SymbolicExpression::InteriorPtr&);
    virtual SExprTypePair outputDivide(const SymbolicExpression::InteriorPtr&, const std::string &operation);
    virtual SExprTypePair outputModulo(const SymbolicExpression::InteriorPtr&, const std::string &operation);

    // Create a memory read expression. The return type is a bit vector. */
    virtual SExprTypePair outputRead(const SymbolicExpression::InteriorPtr&);

    // Create a memory write operation. The return value is a memory state. */
    virtual SExprTypePair outputWrite(const SymbolicExpression::InteriorPtr&);

    // Create a set expression that represents a set of bit vectors all the same size. */
    virtual SExprTypePair outputSet(const SymbolicExpression::InteriorPtr&);

    // Functions that generate SMT-LIB output to a stream when given a Rose::BinaryAnalysis::SymbolicExpression
    virtual void outputVariableDeclarations(std::ostream&, const VariableSet&);
    virtual void outputComments(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);
    virtual void outputCommonSubexpressions(std::ostream&, const std::vector<SymbolicExpression::Ptr>&);
    virtual void outputAssertion(std::ostream&, const SymbolicExpression::Ptr&);
};

} // namespace
} // namespace

#endif
#endif