SymbolicExpression.h

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

#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
#endif

#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 <Rose/Exception.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