Program Listing for File affineInequality.h

↰ Return to documentation for file (src/midend/programAnalysis/genericDataflow/lattice/affineInequality.h)

#include <featureTests.h>
#ifdef ROSE_ENABLE_SOURCE_ANALYSIS

#ifndef AFFINE_INEQUALITY_H
#define AFFINE_INEQUALITY_H

#include "genericDataflowCommon.h"
#include "VirtualCFGIterator.h"
#include "cfgUtils.h"
#include "CallGraphTraverse.h"
#include "analysis.h"
#include "divAnalysis.h"
#include "printAnalysisStates.h"
#include "LogicalCond.h"

#include <sstream>
#include <iostream>
#include <string>
#include <functional>
#include <queue>
#include <list>
#include <set>

// represents the constraint on variables x and y: x*a <= y*b + c
class affineInequality: public printable // : public LogicalCond
{
        friend class varAffineInequality;

        public:
        // The different signs that a variable may have
        typedef enum{
                // This variable's state is unknown
                unknownSgn,
                // This variable is =zero
                eqZero,
                // This variable is positive or =zero
                posZero,
                // This variable is negative or =zero
                negZero} signs;

        protected:
        //varID y;
        int a;
        int b;
        int c;

        // flags that indicate whether the x or y variables are = zeroVar
        bool xZero;
        bool yZero;

        // indicate the sign of x and y
        signs xSign;
        signs ySign;

        public:
        // Possible levels of this constraint. Above bottom the levels are ordered according to their
        //    information content. False has the most content (admits fewest points), then a specific
        //    affine inequality and finally, top, which represents a state where the true inequality is
        //    too complex to be represented as an affine inequality, meaning that the only affine inequality
        //    that can do the job is x <= y + infinity.
        // no constraint known since current constraints are not representable using a single affine
        // inequality (i.e. x <= y + infinity)
        static const short top=3;
        // some affine inequality constraint is known
        static const short constrKnown=2;
        // it is known that the affine constraints are inconsistent: x<=y-infinity
        //static const short falseConstr=1;
        // the values of the variables are not constrained relative to each other (effectively, bottom == uninitialized)
        // (this object would not even be created in this case)
        static const short bottom=0;

        protected:
        // the current level in this constraint's lattice
        short level;

        public:

        affineInequality();

        affineInequality(const affineInequality& that);

        affineInequality(int a, int b, int c, bool xZero, bool yZero, signs xSign, signs ySign);

        // given a constraint on x, z and a constraint on z, y, infers the corresponding constraint on x, y
        // and sets this constraint to it
        affineInequality(const affineInequality& xz, const affineInequality& zy/*, bool xZero, bool yZero, DivLattice* divX, DivLattice* divY, varID z*/);

        void operator=(const affineInequality& that);

        bool operator==(const affineInequality& that) const;

        bool operator!=(const affineInequality& that) const;

        // lexicographic ordering (total order)
        bool operator<(const affineInequality& that) const;

        // Semantic affineInequality ordering (partial order)
        // Returns true if this affineInequality represents less or more information (less information is
        // top, more information is bottom) than that for all values of x and y and false otherwise
        //bool operator<<(const affineInequality& that) const;
        // !!! NOTE: WE MAY WANT A SEMANTIC LESS-THAN-OR-EQ SINCE THAT CAN BE COMPUTED MORE PRECISELY BASED IN <= INFORMATION
        bool semLessThan(const affineInequality& that, bool xEqZero, bool yEqZero) const;
        bool semLessThan(const affineInequality& that,
                    const affineInequality* xZero, const affineInequality* zeroX,
                    const affineInequality* yZero, const affineInequality* zeroY, std::string indent="") const;
        bool semLessThanEq(const affineInequality& that,
                    bool xIsZeroVar,
                    const affineInequality* xZero, const affineInequality* zeroX,
                    bool yIsZeroVar,
                    const affineInequality* yZero, const affineInequality* zeroY, std::string indent="") const;

        // Semantic affineInequality ordering (partial order), focused on negated inequalities
        // Returns true if the negation of this affineInequality represents more information (less information is
        // top, more information is bottom) than the nagation of that for all values of x and y and false otherwise
        //bool affineInequality::semLessThanNeg(const affineInequality& that) const
        bool semLessThanNeg(const affineInequality& that, bool xEqZero, bool yEqZero) const;

        bool set(const affineInequality& that);

        bool set(int a, int b, int c);
        bool set(int a, int b, int c, bool xZero, bool yZero, signs xSign, signs ySign);

        bool setA(int a);

        bool setB(int b);

        bool setC(int c);

        // sets this constraint object to bottom
        bool setToBottom();

        // sets this constraint object to false
        //bool setToFalse();

        // sets this constraint object to top
        bool setToTop();

        // returns y, a, b or c

        int getA() const;

        int getB() const;

        int getC() const;

        short getLevel() const;

        bool isXZero() const;
        bool isYZero() const;

        signs getXSign() const;
        signs getYSign() const;

        protected:
        // divide out from a, b and c any common factors, reducing the triple to its normal form
        // return true if this modifies this constraint and false otherwise
        bool normalize();

        public:
        // INTERSECT this with that, saving the result in this
        // Intersection = the affine inequality that contains the constraint information of both
        //         this AND that (i.e. the line that is lower than both lines)
        // (moves this/that upward in the lattice)
        void operator*=(const affineInequality& that);

        // Just like *=, except intersectUpd() returns true if the operation causes this
        // affineInequality to change and false otherwise.
        bool intersectUpd(const affineInequality& that);

        // UNION this with that, saving the result in this
        // Union = the affine inequality that contains no more information than either
        //         this OR that (i.e. the line that is higher than both lines)
        // (moves this/that downward in the lattice)
        void operator+=(const affineInequality& that);

        // Just like +=, except unionUpd() returns true if the operation causes this
        // affineInequality to change and false otherwise.
        bool unionUpd(const affineInequality& that);

        // WIDEN this with that, saving the result in this
        //void operator^=(const affineInequality& that);

        // returns true if the x-y constraint constrXY is consistent with the y-x constraint constrYX for
        // some values of x and y and false otherwise. Since affineInequalities are conservative in the
        // sense that they don't contain any more information than is definitely true, it may be
        // that the true constraints are in fact inconsistent but we do not have enough information to
        // prove this.
        static bool mayConsistent(const affineInequality& constrXY, const affineInequality& constrYX);

        static std::string signToString(signs sign);

        std::string str(std::string indent="");
        std::string str(std::string indent="") const;

        std::string str(varID x, varID y, std::string indent="") const;
        // Prints out the negation of the constraint ax <= by+c
        std::string strNeg(varID x, varID y, std::string indent) const;

        public:
        // the basic logical operations that must be supported by any implementation of
        // a logical condition: NOT, AND and OR
        /*void notUpd();
        void andUpd(LogicalCond& that);
        void orUpd(LogicalCond& that);*/
};

// represents a full affine inequality, including the variables involved in the inequality
class varAffineInequality : public printable //: public LogicalCond
{
        protected:
        varID x;
        varID y;
        affineInequality ineq;

        public:
        varAffineInequality(const varAffineInequality& that);

        varAffineInequality(const varID& x, const varID& y, const affineInequality& ineq);

        varAffineInequality(const varID& x, const varID& y, int a, int b, int c, bool xZero, bool yZero);

        // get methods
        /*varID& getX() const;

        varID& getY() const;

        affineInequality& getIneq() const;*/

        const varID& getX() const;

        const varID& getY() const;

        int getA() const;

        int getB() const;

        int getC() const;


        const affineInequality& getIneq() const;

        // set methods, return true if this object changes
        const bool setX(const varID& x);

        const bool setY(const varID& y);

        const bool setA(int a);

        const bool setB(int b);

        const bool setC(int c);

        const bool setIneq(affineInequality& ineq);

        // comparison methods
        bool operator==(const varAffineInequality& that) const;

        bool operator<(const varAffineInequality& that) const;

        std::string str(std::string indent="");

        std::string str(std::string indent="") const;

        // Parses expr and returns the corresponding varAffineInequality if expr can be represented
        // as such and NULL otherwise.
        //static varAffineInequality* parseIneq(SgExpression* expr);

        public:
        // the basic logical operations that must be supported by any implementation of
        // a logical condition: NOT, AND and OR
        /*void notUpd();
        void andUpd(LogicalCond& that);
        void orUpd(LogicalCond& that);

        // returns a copy of this LogicalCond object
        LogicalCond* copy();*/
};

/****************************
 *** affineInequalityFact ***
 ****************************/

class affineInequalityFact : public NodeFact
{
        public:
        std::set<varAffineInequality> ineqs;

        affineInequalityFact()
        {}

        affineInequalityFact(const affineInequalityFact& that)
        {
                this->ineqs = that.ineqs;
        }

        NodeFact* copy() const;

        std::string str(std::string indent="");
        std::string str(std::string indent="") const;
};


/********************************
 *** affineInequalitiesPlacer ***
 ********************************/
// points trueIneqFact and falseIneqFact to freshly allocated objects that represent the true and false
// branches of the control flow guarded by the given expression. They are set to NULL if our representation
// cannot represent one of the expressions.
// doFalseBranch - if =true, falseIneqFact is set to the correct false-branch condition and to NULL otherwise
void setTrueFalseIneq(SgExpression* expr,
                      affineInequalityFact **trueIneqFact, affineInequalityFact **falseIneqFact,
                      bool doFalseBranch);

class affineInequalitiesPlacer : public UnstructuredPassIntraAnalysis
{
        public:
        void visit(const Function& func, const DataflowNode& n, NodeState& state);
};

/*// Looks over all the conditional statements in the application and associates appropriate
//    affine inequalities with the SgNodes that depend on these statements. Each inequality
//    is a must: it must be true of the node that it is associated with.
void initAffineIneqs(SgProject* project);

// return the set of varAffineInequalities associated with this node or NULL if none are available
std::set<varAffineInequality>* getAffineIneq(SgNode* n);*/

/*class printAffineInequalities : public UnstructuredPassIntraAnalysis
{
        affineInequalitiesPlacer* placer;

        public:
        printAffineInequalities(affineInequalitiesPlacer *placer);

        void visit(const Function& func, const DataflowNode& n, NodeState& state);
};*/

// prints the inequality facts set by the given affineInequalityPlacer
void printAffineInequalities(affineInequalitiesPlacer* aip, std::string indent="");

// Runs the Affine Inequality Placer analysis
void runAffineIneqPlacer(bool printStates=false);

// returns the set of inequalities known to be true at the given DataflowNode
const std::set<varAffineInequality>& getAffineIneq(const DataflowNode& n);

// Returns the set of inequalities known to be true at the given DataflowNode's descendants
std::list<std::set<varAffineInequality> > getAffineIneqDesc(const DataflowNode& n);

#endif
#endif