SymbolicExpression.h

#ifndef ROSE_BinaryAnalysis_SymbolicExpression_H
#define ROSE_BinaryAnalysis_SymbolicExpression_H
#include <featureTests.h>
#ifdef ROSE_ENABLE_BINARY_ANALYSIS
#include <Rose/BinaryAnalysis/BasicTypes.h>
#include <Rose/Exception.h>
 
#include "Map.h"
 
#include <boost/any.hpp>
#include <boost/lexical_cast.hpp>
#include <boost/logic/tribool.hpp>
#include <boost/serialization/access.hpp>
#include <boost/serialization/base_object.hpp>
#include <boost/serialization/export.hpp>
#include <boost/serialization/split_member.hpp>
#include <boost/serialization/string.hpp>
#include <boost/serialization/vector.hpp>
#include <boost/unordered_map.hpp>
#include <cassert>
#include <inttypes.h>
#include <Sawyer/Attribute.h>
#include <Sawyer/BitVector.h>
#include <Sawyer/Optional.h>
#include <Sawyer/Set.h>
#include <Sawyer/SharedPointer.h>
#include <Sawyer/SmallObject.h>
#include <set>
#include <string>
#include <vector>
 
namespace Rose {
namespace BinaryAnalysis {
 
namespace SymbolicExpression {
 
//                                      Basic Types and settings
 
extern bool serializeVariableIds;
 
namespace TypeStyle {
    enum Flag {
        FULL,                                           
        ABBREVIATED                                     
    };
}
 
 
class Exception: public Rose::Exception {
public:
    explicit Exception(const std::string &mesg): Rose::Exception(mesg) {}
};
 
enum Operator {
    OP_ADD,                 
    OP_AND,                 
    OP_ASR,                 
    OP_CONCAT,              
    OP_EQ,                  
    OP_EXTRACT,             
    OP_INVERT,              
    OP_ITE,                 
    OP_LET,                 
    OP_LSSB,                
    OP_MSSB,                
    OP_NE,                  
    OP_NEGATE,              
    OP_NOOP,                
    OP_OR,                  
    OP_READ,                
    OP_ROL,                 
    OP_ROR,                 
    OP_SDIV,                
    OP_SET,                 
    OP_SEXTEND,             
    OP_SGE,                 
    OP_SGT,                 
    OP_SHL0,                
    OP_SHL1,                
    OP_SHR0,                
    OP_SHR1,                
    OP_SLE,                 
    OP_SLT,                 
    OP_SMOD,                
    OP_SMUL,                
    OP_UDIV,                
    OP_UEXTEND,             
    OP_UGE,                 
    OP_UGT,                 
    OP_ULE,                 
    OP_ULT,                 
    OP_UMOD,                
    OP_UMUL,                
    OP_WRITE,               
    OP_XOR,                 
    OP_ZEROP,               
    OP_FP_ABS,              
    OP_FP_NEGATE,           
    OP_FP_ADD,              
    OP_FP_MUL,              
    OP_FP_DIV,              
    OP_FP_MULADD,           
    OP_FP_SQRT,             
    OP_FP_MOD,              
    OP_FP_ROUND,            
    OP_FP_MIN,              
    OP_FP_MAX,              
    OP_FP_LE,               
    OP_FP_LT,               
    OP_FP_GE,               
    OP_FP_GT,               
    OP_FP_EQ,               
    OP_FP_ISNORM,           
    OP_FP_ISSUBNORM,        
    OP_FP_ISZERO,           
    OP_FP_ISINFINITE,       
    OP_FP_ISNAN,            
    OP_FP_ISNEG,            
    OP_FP_ISPOS,            
    OP_CONVERT,             
    OP_REINTERPRET,         
    OP_NONE                 
};
 
std::string toStr(Operator);
 
using Nodes = std::vector<Ptr>;
using RenameMap = Map<uint64_t, uint64_t>;
 
using Hash = uint64_t;
 
class Formatter {
public:
    enum ShowComments {
        CMT_SILENT,                             
        CMT_AFTER,                              
        CMT_INSTEAD,                            
        CMT_BEFORE,                             
    };
    Formatter()
        : show_comments(CMT_INSTEAD), do_rename(false), add_renames(true), use_hexadecimal(true),
          max_depth(0), cur_depth(0), show_type(true), show_flags(true) {}
    ShowComments show_comments;                 
    bool do_rename;                             
    bool add_renames;                           
    bool use_hexadecimal;                       
    size_t max_depth;                           
    size_t cur_depth;                           
    RenameMap renames;                          
    bool show_type;                             
    bool show_flags;                            
};
 
enum VisitAction {
    CONTINUE,                               
    TRUNCATE,                               
    TERMINATE,                              
};
 
extern const uint64_t MAX_NNODES;       // defined in .C so we don't pollute user namespace with limit macros
 
class Visitor {
public:
    virtual ~Visitor() {}
 
    virtual VisitAction preVisit(const Ptr&);
    virtual VisitAction postVisit(const Ptr&);
 
    virtual VisitAction preVisit(const Node*);
    virtual VisitAction postVisit(const Node*);
};
 
// Expression type information
 
class Type {
public:
    enum TypeClass {
        INTEGER,                                        
        FP,                                             
        MEMORY,                                         
        INVALID                                         
    };
 
private:
    // We use a 32-bit data member and pack into it the totalWidth (15 bits: 0 through 14), the secondaryWidth (15 bits: 15 through 29),
    // and the type class (2 bits: 30 and 31).
    uint32_t fields_;
 
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
private:
    friend class boost::serialization::access;
 
    template<class S>
    void serialize(S &s, const unsigned version) {
        if (version >= 1) {
            s & BOOST_SERIALIZATION_NVP(fields_);
        } else {
            TypeClass t = typeClass();
            size_t z1 = nBits();
            size_t z2 = secondaryWidth();
            s & boost::serialization::make_nvp("typeClass_", t);
            s & boost::serialization::make_nvp("totalWidth_", z1);
            s & boost::serialization::make_nvp("secondaryWidth_", z2);
            typeClass(t);
            nBits(z1);
            secondaryWidth(z2);
        }
    }
#endif
 
public:
    Type()
        : fields_(0) {
        typeClass(INVALID);
        nBits(0);
        secondaryWidth(0);
    }
 
private:
    Type(TypeClass tc, size_t w1, size_t w2)
        : fields_(0) {
        typeClass(tc);
        nBits(w1);
        secondaryWidth(w2);
    }
 
public:
    static Type none() {
        return Type();
    }
 
    static Type integer(size_t nBits) {
        return Type(INTEGER, nBits, 0);
    }
 
    static Type memory(size_t addressWidth, size_t valueWidth) {
        return Type(MEMORY, valueWidth, addressWidth);
    }
 
    static Type floatingPoint(size_t exponentWidth, size_t significandWidth) {
        return Type(FP, 1 /*sign bit*/ + exponentWidth + significandWidth - 1 /*implied bit*/, exponentWidth);
    }
 
    bool isValid() const {
        return typeClass() != INVALID;
    }
 
    TypeClass typeClass() const {
        return (TypeClass)((fields_ >> 30) & 0x3);
    }
 
    size_t nBits() const {
        return fields_ & 0x7fff;
    }
 
    size_t addressWidth() const {
        ASSERT_require(MEMORY == typeClass());
        return secondaryWidth();
    }
 
    size_t exponentWidth() const {
        ASSERT_require(FP == typeClass());
        return secondaryWidth();
    }
 
    size_t significandWidth() const {
        ASSERT_require(FP == typeClass());
        ASSERT_require(nBits() > 1  /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
        return nBits() - (1 /*sign bit*/ + exponentWidth() - 1 /*implied bit*/);
    }
 
    bool operator==(const Type &other) const {
        return fields_ == other.fields_;
    }
    bool operator!=(const Type &other) const {
        return !(*this == other);
    }
    bool operator<(const Type &other) const;
 
    void print(std::ostream&, TypeStyle::Flag style = TypeStyle::FULL) const;
 
    std::string toString(TypeStyle::Flag style = TypeStyle::FULL) const;
 
private:
    // mutators are all private
    void typeClass(TypeClass tc) {
        unsigned n = tc;
        ASSERT_require(n <= 3);
        fields_ = (fields_ & 0x3fffffff) | (n << 30);
    }
 
    // mutators are all private
    void nBits(size_t n) {
        if (n > 0x7fff)
            throw Exception("type width is out of range");
        fields_ = (fields_ & 0xffff8000) | n;
    }
 
    // mutators are all private
    void secondaryWidth(size_t n) {
        if (n > 0x7fff)
            throw Exception("second width is out of range");
        fields_ = (fields_ & 0xc0007fff) | (n << 15);
    }
 
    size_t secondaryWidth() const {
        return (fields_ >> 15) & 0x7fff;
    }
};
 
//                                      Base Node Type
 
class Node
    : public Sawyer::SharedObject,
      public Sawyer::SharedFromThis<Node>,
      public Sawyer::SmallObject,
      public Sawyer::Attribute::Storage<> { // Attributes are not significant for hashing or arithmetic
protected:
    Type type_;
    unsigned flags_;                  
    std::string comment_;             
    mutable Hash hashval_;            
    boost::any userData_;             
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
private:
    friend class boost::serialization::access;
 
    template<class S>
    void serialize(S &s, const unsigned version) {
        if (version < 1)
            ASSERT_not_reachable("SymbolicExpression version " + boost::lexical_cast<std::string>(version) + " is no longer supported");
        s & BOOST_SERIALIZATION_NVP(type_);
        s & BOOST_SERIALIZATION_NVP(flags_);
        s & BOOST_SERIALIZATION_NVP(comment_);
        s & BOOST_SERIALIZATION_NVP(hashval_);
        // s & userData_;
    }
#endif
 
public:
    // Bit flags
 
    static const unsigned RESERVED_FLAGS = 0x0000ffff;
 
    static const unsigned INDETERMINATE  = 0x00000001;
 
    static const unsigned UNSPECIFIED    = 0x00000002;
 
    static const unsigned BOTTOM         = 0x00000004;
 
public:
    virtual ~Node() {}
 
protected:
    Node()
        : type_(Type::integer(0)), flags_(0), hashval_(0) {}
    explicit Node(const std::string &comment, unsigned flags=0)
        : type_(Type::integer(0)), flags_(flags), comment_(comment), hashval_(0) {}
 
public:
    Type type() const {
        return type_;
    }
 
    static boost::logic::tribool (*mayEqualCallback)(const Ptr &a, const Ptr &b, const SmtSolverPtr&);
 
    virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
 
    virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
 
    virtual bool isEquivalentTo(const Ptr &other) = 0;
 
    virtual int compareStructure(const Ptr &other) = 0;
 
    virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) = 0;
 
    Ptr substituteMultiple(const ExprExprHashMap &substitutions, const SmtSolverPtr &solver = SmtSolverPtr());
 
    Ptr renameVariables(ExprExprHashMap &index /*in,out*/, size_t &nextVariableId /*in,out*/,
                        const SmtSolverPtr &solver = SmtSolverPtr());
 
    virtual Operator getOperator() const = 0;
 
    virtual size_t nChildren() const = 0;
 
    virtual const Ptr& child(size_t idx) const = 0;
    virtual const Node* childRaw(size_t idx) const = 0;
    virtual const Nodes& children() const = 0;
 
    virtual Sawyer::Optional<uint64_t> toUnsigned() const = 0;
 
    virtual Sawyer::Optional<int64_t> toSigned() const = 0;
 
    bool isIntegerExpr() const {
        return type_.typeClass() == Type::INTEGER;
    }
 
    bool isFloatingPointExpr() const {
        return type_.typeClass() == Type::FP;
    }
 
    bool isMemoryExpr() const {
        return type_.typeClass() == Type::MEMORY;
    }
 
    bool isScalarExpr() const {
        return isIntegerExpr() || isFloatingPointExpr();
    }
 
    virtual bool isConstant() const = 0;
 
    bool isIntegerConstant() const {
        return isIntegerExpr() && isConstant();
    }
 
    bool isFloatingPointConstant() const {
        return isFloatingPointExpr() && isConstant();
    }
 
    bool isScalarConstant() const {
        return isIntegerConstant() || isFloatingPointConstant();
    }
 
    bool isFloatingPointNan() const;
 
    virtual bool isVariable2() const = 0;
 
    Sawyer::Optional<uint64_t> variableId() const;
 
    bool isIntegerVariable() const {
        return isIntegerExpr() && isVariable2();
    }
 
    bool isFloatingPointVariable() const {
        return isFloatingPointExpr() && isVariable2();
    }
 
    bool isMemoryVariable() const {
        return isMemoryExpr() && isVariable2();
    }
 
    bool isScalarVariable() const {
        return isIntegerVariable() || isFloatingPointVariable();
    }
 
    const std::string& comment() const {
        return comment_;
    }
    void comment(const std::string &s) {
        comment_ = s;
    }
    void userData(boost::any &data) {
        userData_ = data;
    }
    const boost::any& userData() const {
        return userData_;
    }
    size_t nBits() const {
        return type_.nBits();
    }
 
    unsigned flags() const {
        return flags_;
    }
 
    Ptr newFlags(unsigned flags) const;
 
    size_t domainWidth() const {
        return type_.addressWidth();
    }
 
    bool isScalar() const {
        return type_.typeClass() != Type::MEMORY;
    }
 
    virtual VisitAction depthFirstTraversal(Visitor&) const = 0;
 
    virtual uint64_t nNodes() const = 0;
 
    uint64_t nNodesUnique() const;
 
    std::set<LeafPtr> getVariables() const;
 
    InteriorPtr isInteriorNode() const;
    Interior* isInteriorNodeRaw() const;
    LeafPtr isLeafNode() const;
    Leaf* isLeafNodeRaw() const;
    bool isHashed() const {
        return hashval_ != 0;
    }
 
    Hash hash() const;
 
    // used internally to set the hash value
    void hash(Hash) const;
 
    class WithFormatter {
    private:
        Ptr node;
        Formatter &formatter;
    public:
        WithFormatter(const Ptr &node, Formatter &formatter): node(node), formatter(formatter) {}
        void print(std::ostream &stream) const { node->print(stream, formatter); }
    };
 
    WithFormatter withFormat(Formatter &fmt) { return WithFormatter(sharedFromThis(), fmt); }
    WithFormatter operator+(Formatter &fmt) { return withFormat(fmt); }
    virtual void print(std::ostream&, Formatter&) const = 0;
    void print(std::ostream &o) const { Formatter fmt; print(o, fmt); }
    std::string toString() const;
 
    void assertAcyclic() const;
 
    std::vector<Ptr> findCommonSubexpressions() const;
 
    bool matchAddVariableConstant(LeafPtr &variable/*out*/, LeafPtr &constant/*out*/) const;
 
    InteriorPtr isOperator(Operator) const;
 
protected:
    void printFlags(std::ostream &o, unsigned flags, char &bracket) const;
 
public: // only used internally
    using EquivPairs = std::map<Node*, std::vector<std::pair<Node*, bool>>>;
    virtual bool isEquivalentHelper(Node*, EquivPairs&) = 0;
};
 
class Simplifier {
public:
    virtual ~Simplifier() {}
 
    virtual Ptr fold(Nodes::const_iterator /*begin*/, Nodes::const_iterator /*end*/) const {
        return Ptr();
    }
 
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const {
        return Ptr();
    }
};
 
struct ExprExprHashMapHasher {
     size_t operator()(const Ptr &expr) const {
        return expr->hash();
    }
};
 
struct ExprExprHashMapCompare {
    bool operator()(const Ptr &a, const Ptr &b) const {
        return a->isEquivalentTo(b);
    }
};
 
class ExpressionLessp {
public:
    bool operator()(const Ptr &a, const Ptr &b) const;
};
 
class ExprExprHashMap: public boost::unordered_map<SymbolicExpression::Ptr, SymbolicExpression::Ptr,
                                                   ExprExprHashMapHasher, ExprExprHashMapCompare> {
public:
    ExprExprHashMap invert() const;
};
 
typedef Sawyer::Container::Set<Ptr, ExpressionLessp> ExpressionSet;
 
 
//                                      Simplification
 
struct AddSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct AndSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct ConvertSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct OrSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct XorSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SmulSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
};
struct UmulSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
};
struct ConcatSimplifier: Simplifier {
    virtual Ptr fold(Nodes::const_iterator, Nodes::const_iterator) const override;
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct ExtractSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct AsrSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct InvertSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct NegateSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct IteSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct NoopSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct ReinterpretSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct RolSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct RorSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UextendSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SextendSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct EqSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SgeSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SgtSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SleSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SltSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UgeSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UgtSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UleSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UltSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct ZeropSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SdivSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SmodSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UdivSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct UmodSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct ShiftSimplifier: Simplifier {
    bool newbits;
    ShiftSimplifier(bool newbits): newbits(newbits) {}
    Ptr combine_strengths(Ptr strength1, Ptr strength2, size_t value_width, const SmtSolverPtr &solver) const;
};
struct ShlSimplifier: ShiftSimplifier {
    ShlSimplifier(bool newbits): ShiftSimplifier(newbits) {}
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct ShrSimplifier: ShiftSimplifier {
    ShrSimplifier(bool newbits): ShiftSimplifier(newbits) {}
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct LssbSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct MssbSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
struct SetSimplifier: Simplifier {
    virtual Ptr rewrite(Interior*, const SmtSolverPtr&) const override;
};
 
 
 
//                                      Interior Nodes
 
class Interior: public Node {
private:
    Operator op_;
    Nodes children_;
    uint64_t nnodes_;                                   // total number of nodes; self + children's nnodes
 
    //--------------------------------------------------------
    // Serialization
    //--------------------------------------------------------
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
private:
    friend class boost::serialization::access;
 
    template<class S>
    void serialize(S &s, const unsigned /*version*/) {
        s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
        s & BOOST_SERIALIZATION_NVP(op_);
        s & BOOST_SERIALIZATION_NVP(children_);
        s & BOOST_SERIALIZATION_NVP(nnodes_);
    }
#endif
 
    //--------------------------------------------------------
    // Real constructors
    //--------------------------------------------------------
private:
    Interior();                                         // needed for serialization
    // Only constructs, does not simplify.
    Interior(const Type&, Operator, const Nodes &arguments, const std::string &comment, unsigned flags);
 
    //--------------------------------------------------------
    // Allocating constructors
    //--------------------------------------------------------
public:
    static Ptr instance(Operator op, const Ptr &a,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(const Type &type, Operator op, const Ptr &a,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(Operator op, const Ptr &a, const Ptr &b,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(const Type &type, Operator op, const Ptr &a, const Ptr &b, const Ptr &c,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(Operator op, const Nodes &arguments,
                      const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    static Ptr instance(const Type &type, Operator op, const Nodes &arguments,
                        const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
    //--------------------------------------------------------
    // Overrides
    //--------------------------------------------------------
public:
    virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
    virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
    virtual bool isEquivalentTo(const Ptr &other) override;
    virtual bool isEquivalentHelper(Node*, EquivPairs&) override;
    virtual int compareStructure(const Ptr& other) override;
    virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) override;
    virtual VisitAction depthFirstTraversal(Visitor&) const override;
    virtual uint64_t nNodes() const override { return nnodes_; }
    virtual const Nodes& children() const override { return children_; }
    virtual Operator getOperator() const override { return op_; }
    virtual size_t nChildren() const override { return children_.size(); }
    virtual const Ptr& child(size_t idx) const override;
    virtual Node* childRaw(size_t idx) const override;
    virtual Sawyer::Optional<uint64_t> toUnsigned() const override { return Sawyer::Nothing(); }
    virtual Sawyer::Optional<int64_t> toSigned() const override { return Sawyer::Nothing(); }
    virtual bool isConstant() const override { return false; }
    virtual bool isVariable2() const override { return false; }
 
    //--------------------------------------------------------
    // Simplification
    //--------------------------------------------------------
public:
    Ptr simplifyTop(const SmtSolverPtr &solver = SmtSolverPtr());
 
    Ptr foldConstants(const Simplifier&);
 
    InteriorPtr associative();
 
    InteriorPtr commutative();
 
    InteriorPtr idempotent(const SmtSolverPtr &solver = SmtSolverPtr());
 
    Ptr involutary();
 
    Ptr additiveNesting(const SmtSolverPtr &solver = SmtSolverPtr());
 
    Ptr identity(uint64_t ident, const SmtSolverPtr &solver = SmtSolverPtr());
 
    Ptr poisonNan(const SmtSolverPtr &solver = SmtSolverPtr());
 
    Ptr unaryNoOp();
 
    Ptr rewrite(const Simplifier &simplifier, const SmtSolverPtr &solver = SmtSolverPtr());
 
    //--------------------------------------------------------
    // Functions specific to internal nodes
    //--------------------------------------------------------
public:
    virtual void print(std::ostream&, Formatter&) const override;
 
protected:
    void addChild(const Ptr &child);
 
    void adjustWidth(const Type&);
 
    void adjustBitFlags(unsigned extraFlags);
};
 
 
//                                      Leaf Nodes
 
class Leaf: public Node {
private:
    Sawyer::Container::BitVector bits_; // Value for constants if size > 0
    uint64_t name_;                     // Variable ID for variables when bits_.size() == 0
 
    //--------------------------------------------------------
    // Serialization
    //--------------------------------------------------------
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
private:
    friend class boost::serialization::access;
 
    template<class S>
    void save(S &s, const unsigned /*version*/) const {
        s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
        s & BOOST_SERIALIZATION_NVP(bits_);
        s & BOOST_SERIALIZATION_NVP(name_);
    }
 
    template<class S>
    void load(S &s, const unsigned /*version*/) {
        s & BOOST_SERIALIZATION_BASE_OBJECT_NVP(Node);
        s & BOOST_SERIALIZATION_NVP(bits_);
        s & BOOST_SERIALIZATION_NVP(name_);
        nextNameCounter(name_);
    }
 
    BOOST_SERIALIZATION_SPLIT_MEMBER();
#endif
 
    //--------------------------------------------------------
    // Private constructors. Use create methods instead.
    //--------------------------------------------------------
private:
    Leaf()
        : name_(0) {}
    explicit Leaf(const std::string &comment, unsigned flags=0)
        : Node(comment, flags), name_(0) {}
 
    // Allocating constructors.
public:
    static LeafPtr createVariable(const Type&,
                                  const std::string &comment = "", unsigned flags = 0);
 
    static LeafPtr createVariable(const Type&, const uint64_t id,
                                  const std::string &comment = "", unsigned flags = 0);
 
    static LeafPtr createConstant(const Type&, const Sawyer::Container::BitVector&,
                                  const std::string &comment = "", unsigned flags = 0);
 
    //--------------------------------------------------------
    // Override base class implementations
    //--------------------------------------------------------
public:
    virtual size_t nChildren() const override { return 0; }
    virtual const Ptr& child(size_t idx) const override;
    virtual const Node* childRaw(size_t) const override { return nullptr; }
    virtual const Nodes& children() const override;
    virtual Operator getOperator() const override { return OP_NONE; }
    virtual bool mustEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
    virtual bool mayEqual(const Ptr &other, const SmtSolverPtr &solver = SmtSolverPtr()) override;
    virtual bool isEquivalentTo(const Ptr &other) override;
    virtual bool isEquivalentHelper(Node*, EquivPairs&) override;
    virtual int compareStructure(const Ptr& other) override;
    virtual Ptr substitute(const Ptr &from, const Ptr &to, const SmtSolverPtr &solver = SmtSolverPtr()) override;
    virtual VisitAction depthFirstTraversal(Visitor&) const override;
    virtual uint64_t nNodes() const override { return 1; }
    virtual Sawyer::Optional<uint64_t> toUnsigned() const override;
    virtual Sawyer::Optional<int64_t> toSigned() const override;
    virtual bool isConstant() const override { return !bits_.isEmpty(); }
    virtual bool isVariable2() const override { return !isConstant(); }
    virtual void print(std::ostream&, Formatter&) const override;
 
    //--------------------------------------------------------
    // Leaf-specific methods
    //--------------------------------------------------------
public:
    const Sawyer::Container::BitVector& bits() const;
 
    bool isIntegerVariable() const {
        return type().typeClass() == Type::INTEGER && !isConstant();
    }
 
    bool isFloatingPointVariable() const {
        return type().typeClass() == Type::FP && !isConstant();
    }
 
    bool isFloatingPointNan() const;
 
    bool isMemoryVariable() const {
        return type().typeClass() == Type::MEMORY && !isConstant();
    }
 
    uint64_t nameId() const;
 
    std::string toString() const;
 
    void printAsSigned(std::ostream&, Formatter&, bool asSigned = true) const;
 
    void printAsUnsigned(std::ostream &o, Formatter &f) const {
        printAsSigned(o, f, false);
    }
 
private:
    // Obtain or register a name ID
    static uint64_t nextNameCounter(uint64_t useThis = (uint64_t)(-1));
};
 
//                                      Factories
 
LeafPtr makeVariable(const Type&, const std::string &comment="", unsigned flags=0);
LeafPtr makeVariable(const Type&, uint64_t id, const std::string &comment="", unsigned flags=0);
LeafPtr makeConstant(const Type&, const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
LeafPtr makeIntegerVariable(size_t nBits, const std::string &comment="", unsigned flags=0);
LeafPtr makeIntegerVariable(size_t nBits, uint64_t id, const std::string &comment="", unsigned flags=0);
LeafPtr makeIntegerConstant(size_t nBits, uint64_t value, const std::string &comment="", unsigned flags=0);
LeafPtr makeIntegerConstant(const Sawyer::Container::BitVector&, const std::string &comment="", unsigned flags=0);
LeafPtr makeBooleanConstant(bool, const std::string &comment="", unsigned flags=0);
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, const std::string &comment="", unsigned flags=0);
LeafPtr makeMemoryVariable(size_t addressWidth, size_t valueWidth, uint64_t id, const std::string &comment="", unsigned flags=0);
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
LeafPtr makeFloatingPointVariable(size_t eb, size_t sb, uint64_t id, const std::string &comment="", unsigned flags=0);
LeafPtr makeFloatingPointConstant(float, const std::string &comment="", unsigned flags=0);
LeafPtr makeFloatingPointConstant(double, const std::string &comment="", unsigned flags=0);
LeafPtr makeFloatingPointNan(size_t eb, size_t sb, const std::string &comment="", unsigned flags=0);
Ptr makeAdd(const Ptr&a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeAsr(const Ptr &sa, const Ptr &a,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeAnd(const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeOr(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeXor(const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeConcat(const Ptr &hi, const Ptr &lo,
               const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeConvert(const Ptr &a, const Type &b,
                const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeEq(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeExtract(const Ptr &begin, const Ptr &end, const Ptr &a,
                const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeInvert(const Ptr &a,
               const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsInfinite(const Ptr &a,
                   const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsNan(const Ptr &a,
              const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsNeg(const Ptr &a,
              const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsNorm(const Ptr &a,
               const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsPos(const Ptr &a,
              const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsSubnorm(const Ptr &a,
                  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIte(const Ptr &cond, const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeLet(const Ptr &a, const Ptr &b, const Ptr &c,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeLssb(const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeMax(const Ptr &a, const Ptr &b,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeMin(const Ptr &a, const Ptr &b,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeMssb(const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeMultiplyAdd(const Ptr &a, const Ptr &b, const Ptr &c,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeNe(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeNegate(const Ptr &a,
               const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeRead(const Ptr &mem, const Ptr &addr,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeReinterpret(const Ptr &a, const Type &b,
                    const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeRol(const Ptr &sa, const Ptr &a,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeRor(const Ptr &sa, const Ptr &a,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeRound(const Ptr &a,
              const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSet(const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSet(const Ptr &a, const Ptr &b, const Ptr &c,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedDiv(const Ptr &a, const Ptr &b,
                  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignExtend(const Ptr &newSize, const Ptr &a,
                   const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedGe(const Ptr &a, const Ptr &b,
                 const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedGt(const Ptr &a, const Ptr &b,
                 const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeShl0(const Ptr &sa, const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeShl1(const Ptr &sa, const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeShr0(const Ptr &sa, const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeShr1(const Ptr &sa, const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeIsSignedPos(const Ptr &a,
                    const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedLe(const Ptr &a, const Ptr &b,
                 const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedLt(const Ptr &a, const Ptr &b,
                 const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedMax(const Ptr &a, const Ptr &b,
                  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedMin(const Ptr &a, const Ptr &b,
                  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedMod(const Ptr &a, const Ptr &b,
                  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSignedMul(const Ptr &a, const Ptr &b,
                  const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeSqrt(const Ptr &a,
             const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeDiv(const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeExtend(const Ptr &newSize, const Ptr &a,
               const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeGe(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeGt(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeLe(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeLt(const Ptr &a, const Ptr &b,
           const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeMod(const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeMul(const Ptr &a, const Ptr &b,
            const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeWrite(const Ptr &mem, const Ptr &addr, const Ptr &a,
              const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
Ptr makeZerop(const Ptr &a,
              const SmtSolverPtr &solver = SmtSolverPtr(), const std::string &comment="", unsigned flags=0);
//                                      Miscellaneous functions
 
 
std::ostream& operator<<(std::ostream &o, const Node&);
std::ostream& operator<<(std::ostream &o, const Node::WithFormatter&);
 
Ptr setToIte(const Ptr&, const SmtSolverPtr &solver = SmtSolverPtr(), const LeafPtr &var = LeafPtr());
 
Hash hash(const std::vector<Ptr>&);
 
template<typename InputIterator>
uint64_t
nNodes(InputIterator begin, InputIterator end) {
    uint64_t total = 0;
    for (InputIterator ii=begin; ii!=end; ++ii) {
        uint64_t n = (*ii)->nnodes();
        if (MAX_NNODES==n)
            return MAX_NNODES;
        if (total + n < total)
            return MAX_NNODES;
        total += n;
    }
    return total;
}
 
template<typename InputIterator>
uint64_t
nNodesUnique(InputIterator begin, InputIterator end)
{
    struct T1: Visitor {
        typedef std::set<const Node*> SeenNodes;
 
        SeenNodes seen;                                 // nodes that we've already seen, and the subtree size
        uint64_t nUnique;                               // number of unique nodes
 
        T1(): nUnique(0) {}
 
        VisitAction preVisit(const Node *node) override {
            ASSERT_not_null(node);
            if (seen.insert(node).second) {
                ++nUnique;
                return CONTINUE;                        // this node has not been seen before; traverse into children
            } else {
                return TRUNCATE;                        // this node has been seen already; skip over the children
            }
        }
 
        VisitAction postVisit(const Node*) override {
            return CONTINUE;
        }
    } visitor;
 
    VisitAction status = CONTINUE;
    for (InputIterator ii=begin; ii!=end && TERMINATE!=status; ++ii)
        status = (*ii)->depthFirstTraversal(visitor);
    return visitor.nUnique;
}
 
std::vector<Ptr> findCommonSubexpressions(const std::vector<Ptr>&);
 
template<typename InputIterator>
std::vector<Ptr>
findCommonSubexpressions(InputIterator begin, InputIterator end) {
    typedef Sawyer::Container::Map<const Node*, size_t> NodeCounts;
    struct T1: Visitor {
        NodeCounts nodeCounts;
        std::vector<Ptr> result;
 
        VisitAction preVisit(const Node *node) override {
            ASSERT_not_null(node);
            size_t &nSeen = nodeCounts.insertMaybe(node, 0);
            if (2 == ++nSeen)
                result.push_back(Ptr(const_cast<Node*>(node)));
            return nSeen>1 ? TRUNCATE : CONTINUE;
        }
 
        VisitAction postVisit(const Node*) override {
            return CONTINUE;
        }
    } visitor;
 
    for (InputIterator ii=begin; ii!=end; ++ii)
        (*ii)->depthFirstTraversal(visitor);
    return visitor.result;
}
template<class Substitution>
Ptr substitute(const Ptr &src, Substitution &subber, const SmtSolverPtr &solver = SmtSolverPtr()) {
    if (!src)
        return Ptr();                                   // no input implies no output
 
    // Try substituting the whole expression, returning the result.
    Ptr dst = subber(src, solver);
    ASSERT_not_null(dst);
    if (dst != src)
        return dst;
 
    // Try substituting all the subexpressions.
    const Interior *inode = src->isInteriorNodeRaw();
    if (!inode)
        return src;
    bool anyChildChanged = false;
    Nodes newChildren;
    newChildren.reserve(inode->nChildren());
    for (const Ptr &child: inode->children()) {
        Ptr newChild = substitute(child, subber, solver);
        if (newChild != child)
            anyChildChanged = true;
        newChildren.push_back(newChild);
    }
    if (!anyChildChanged)
        return src;
 
    // Some subexpression changed, so build a new expression
    return Interior::instance(inode->getOperator(), newChildren, solver, inode->comment(), inode->flags());
}
 
} // namespace
 
using SymbolicExpressionPtr = SymbolicExpression::Ptr;
 
} // namespace
} // namespace
 
#ifdef ROSE_HAVE_BOOST_SERIALIZATION_LIB
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpression::Interior);
BOOST_CLASS_EXPORT_KEY(Rose::BinaryAnalysis::SymbolicExpression::Leaf);
BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpression::Type, 1);
BOOST_CLASS_VERSION(Rose::BinaryAnalysis::SymbolicExpression::Node, 1);
#endif
 
#endif
#endif