ROSE  0.9.9.109
affineInequality.h
1 #ifndef AFFINE_INEQUALITY_H
2 #define AFFINE_INEQUALITY_H
3 
4 #include "genericDataflowCommon.h"
5 #include "VirtualCFGIterator.h"
6 #include "cfgUtils.h"
7 #include "CallGraphTraverse.h"
8 #include "analysis.h"
9 #include "divAnalysis.h"
10 #include "printAnalysisStates.h"
11 #include "LogicalCond.h"
12 
13 #include <sstream>
14 #include <iostream>
15 #include <string>
16 #include <functional>
17 #include <queue>
18 #include <list>
19 #include <set>
20 
21 // represents the constraint on variables x and y: x*a <= y*b + c
22 class affineInequality: public printable // : public LogicalCond
23 {
24  friend class varAffineInequality;
25 
26  public:
27  // The different signs that a variable may have
28  typedef enum{
29  // This variable's state is unknown
30  unknownSgn,
31  // This variable is =zero
32  eqZero,
33  // This variable is positive or =zero
34  posZero,
35  // This variable is negative or =zero
36  negZero} signs;
37 
38  protected:
39  //varID y;
40  int a;
41  int b;
42  int c;
43 
44  // flags that indicate whether the x or y variables are = zeroVar
45  bool xZero;
46  bool yZero;
47 
48  // indicate the sign of x and y
49  signs xSign;
50  signs ySign;
51 
52  public:
53  // Possible levels of this constraint. Above bottom the levels are ordered according to their
54  // information content. False has the most content (admits fewest points), then a specific
55  // affine inequality and finally, top, which represents a state where the true inequality is
56  // too complex to be represented as an affine inequality, meaning that the only affine inequality
57  // that can do the job is x <= y + infinity.
58  // no constraint known since current constraints are not representable using a single affine
59  // inequality (i.e. x <= y + infinity)
60  static const short top=3;
61  // some affine inequality constraint is known
62  static const short constrKnown=2;
63  // it is known that the affine constraints are inconsistent: x<=y-infinity
64  //static const short falseConstr=1;
65  // the values of the variables are not constrained relative to each other (effectively, bottom == uninitialized)
66  // (this object would not even be created in this case)
67  static const short bottom=0;
68 
69  protected:
70  // the current level in this constraint's lattice
71  short level;
72 
73  public:
74 
76 
78 
79  affineInequality(int a, int b, int c, bool xZero, bool yZero, signs xSign, signs ySign);
80 
81  // given a constraint on x, z and a constraint on z, y, infers the corresponding constraint on x, y
82  // and sets this constraint to it
83  affineInequality(const affineInequality& xz, const affineInequality& zy/*, bool xZero, bool yZero, DivLattice* divX, DivLattice* divY, varID z*/);
84 
85  void operator=(const affineInequality& that);
86 
87  bool operator==(const affineInequality& that) const;
88 
89  bool operator!=(const affineInequality& that) const;
90 
91  // lexicographic ordering (total order)
92  bool operator<(const affineInequality& that) const;
93 
94  // Semantic affineInequality ordering (partial order)
95  // Returns true if this affineInequality represents less or more information (less information is
96  // top, more information is bottom) than that for all values of x and y and false otherwise
97  //bool operator<<(const affineInequality& that) const;
98  // !!! NOTE: WE MAY WANT A SEMANTIC LESS-THAN-OR-EQ SINCE THAT CAN BE COMPUTED MORE PRECISELY BASED IN <= INFORMATION
99  bool semLessThan(const affineInequality& that, bool xEqZero, bool yEqZero) const;
100  bool semLessThan(const affineInequality& that,
101  const affineInequality* xZero, const affineInequality* zeroX,
102  const affineInequality* yZero, const affineInequality* zeroY, std::string indent="") const;
103  bool semLessThanEq(const affineInequality& that,
104  bool xIsZeroVar,
105  const affineInequality* xZero, const affineInequality* zeroX,
106  bool yIsZeroVar,
107  const affineInequality* yZero, const affineInequality* zeroY, std::string indent="") const;
108 
109  // Semantic affineInequality ordering (partial order), focused on negated inequalities
110  // Returns true if the negation of this affineInequality represents more information (less information is
111  // top, more information is bottom) than the nagation of that for all values of x and y and false otherwise
112  //bool affineInequality::semLessThanNeg(const affineInequality& that) const
113  bool semLessThanNeg(const affineInequality& that, bool xEqZero, bool yEqZero) const;
114 
115  bool set(const affineInequality& that);
116 
117  bool set(int a, int b, int c);
118  bool set(int a, int b, int c, bool xZero, bool yZero, signs xSign, signs ySign);
119 
120  bool setA(int a);
121 
122  bool setB(int b);
123 
124  bool setC(int c);
125 
126  // sets this constraint object to bottom
127  bool setToBottom();
128 
129  // sets this constraint object to false
130  //bool setToFalse();
131 
132  // sets this constraint object to top
133  bool setToTop();
134 
135  // returns y, a, b or c
136 
137  int getA() const;
138 
139  int getB() const;
140 
141  int getC() const;
142 
143  short getLevel() const;
144 
145  bool isXZero() const;
146  bool isYZero() const;
147 
148  signs getXSign() const;
149  signs getYSign() const;
150 
151  protected:
152  // divide out from a, b and c any common factors, reducing the triple to its normal form
153  // return true if this modifies this constraint and false otherwise
154  bool normalize();
155 
156  public:
157  // INTERSECT this with that, saving the result in this
158  // Intersection = the affine inequality that contains the constraint information of both
159  // this AND that (i.e. the line that is lower than both lines)
160  // (moves this/that upward in the lattice)
161  void operator*=(const affineInequality& that);
162 
163  // Just like *=, except intersectUpd() returns true if the operation causes this
164  // affineInequality to change and false otherwise.
165  bool intersectUpd(const affineInequality& that);
166 
167  // UNION this with that, saving the result in this
168  // Union = the affine inequality that contains no more information than either
169  // this OR that (i.e. the line that is higher than both lines)
170  // (moves this/that downward in the lattice)
171  void operator+=(const affineInequality& that);
172 
173  // Just like +=, except unionUpd() returns true if the operation causes this
174  // affineInequality to change and false otherwise.
175  bool unionUpd(const affineInequality& that);
176 
177  // WIDEN this with that, saving the result in this
178  //void operator^=(const affineInequality& that);
179 
180  // returns true if the x-y constraint constrXY is consistent with the y-x constraint constrYX for
181  // some values of x and y and false otherwise. Since affineInequalities are conservative in the
182  // sense that they don't contain any more information than is definitely true, it may be
183  // that the true constraints are in fact inconsistent but we do not have enough information to
184  // prove this.
185  static bool mayConsistent(const affineInequality& constrXY, const affineInequality& constrYX);
186 
187  static std::string signToString(signs sign);
188 
189  std::string str(std::string indent="");
190  std::string str(std::string indent="") const;
191 
192  std::string str(varID x, varID y, std::string indent="") const;
193  // Prints out the negation of the constraint ax <= by+c
194  std::string strNeg(varID x, varID y, std::string indent) const;
195 
196  public:
197  // the basic logical operations that must be supported by any implementation of
198  // a logical condition: NOT, AND and OR
199  /*void notUpd();
200  void andUpd(LogicalCond& that);
201  void orUpd(LogicalCond& that);*/
202 };
203 
204 // represents a full affine inequality, including the variables involved in the inequality
205 class varAffineInequality : public printable //: public LogicalCond
206 {
207  protected:
208  varID x;
209  varID y;
210  affineInequality ineq;
211 
212  public:
214 
215  varAffineInequality(const varID& x, const varID& y, const affineInequality& ineq);
216 
217  varAffineInequality(const varID& x, const varID& y, int a, int b, int c, bool xZero, bool yZero);
218 
219  // get methods
220  /*varID& getX() const;
221 
222  varID& getY() const;
223 
224  affineInequality& getIneq() const;*/
225 
226  const varID& getX() const;
227 
228  const varID& getY() const;
229 
230  int getA() const;
231 
232  int getB() const;
233 
234  int getC() const;
235 
236 
237  const affineInequality& getIneq() const;
238 
239  // set methods, return true if this object changes
240  const bool setX(const varID& x);
241 
242  const bool setY(const varID& y);
243 
244  const bool setA(int a);
245 
246  const bool setB(int b);
247 
248  const bool setC(int c);
249 
250  const bool setIneq(affineInequality& ineq);
251 
252  // comparison methods
253  bool operator==(const varAffineInequality& that) const;
254 
255  bool operator<(const varAffineInequality& that) const;
256 
257  std::string str(std::string indent="");
258 
259  std::string str(std::string indent="") const;
260 
261  // Parses expr and returns the corresponding varAffineInequality if expr can be represented
262  // as such and NULL otherwise.
263  //static varAffineInequality* parseIneq(SgExpression* expr);
264 
265  public:
266  // the basic logical operations that must be supported by any implementation of
267  // a logical condition: NOT, AND and OR
268  /*void notUpd();
269  void andUpd(LogicalCond& that);
270  void orUpd(LogicalCond& that);
271 
272  // returns a copy of this LogicalCond object
273  LogicalCond* copy();*/
274 };
275 
276 /****************************
277  *** affineInequalityFact ***
278  ****************************/
279 
281 {
282  public:
283  std::set<varAffineInequality> ineqs;
284 
286  {}
287 
289  {
290  this->ineqs = that.ineqs;
291  }
292 
293  NodeFact* copy() const;
294 
295  std::string str(std::string indent="");
296  std::string str(std::string indent="") const;
297 };
298 
299 
300 /********************************
301  *** affineInequalitiesPlacer ***
302  ********************************/
303 // points trueIneqFact and falseIneqFact to freshly allocated objects that represent the true and false
304 // branches of the control flow guarded by the given expression. They are set to NULL if our representation
305 // cannot represent one of the expressions.
306 // doFalseBranch - if =true, falseIneqFact is set to the correct false-branch condition and to NULL otherwise
307 void setTrueFalseIneq(SgExpression* expr,
308  affineInequalityFact **trueIneqFact, affineInequalityFact **falseIneqFact,
309  bool doFalseBranch);
310 
312 {
313  public:
314  void visit(const Function& func, const DataflowNode& n, NodeState& state);
315 };
316 
317 /*// Looks over all the conditional statements in the application and associates appropriate
318 // affine inequalities with the SgNodes that depend on these statements. Each inequality
319 // is a must: it must be true of the node that it is associated with.
320 void initAffineIneqs(SgProject* project);
321 
322 // return the set of varAffineInequalities associated with this node or NULL if none are available
323 std::set<varAffineInequality>* getAffineIneq(SgNode* n);*/
324 
325 /*class printAffineInequalities : public UnstructuredPassIntraAnalysis
326 {
327  affineInequalitiesPlacer* placer;
328 
329  public:
330  printAffineInequalities(affineInequalitiesPlacer *placer);
331 
332  void visit(const Function& func, const DataflowNode& n, NodeState& state);
333 };*/
334 
335 // prints the inequality facts set by the given affineInequalityPlacer
336 void printAffineInequalities(affineInequalitiesPlacer* aip, std::string indent="");
337 
338 // Runs the Affine Inequality Placer analysis
339 void runAffineIneqPlacer(bool printStates=false);
340 
341 // returns the set of inequalities known to be true at the given DataflowNode
342 const std::set<varAffineInequality>& getAffineIneq(const DataflowNode& n);
343 
344 // Returns the set of inequalities known to be true at the given DataflowNode's descendants
345 std::list<std::set<varAffineInequality> > getAffineIneqDesc(const DataflowNode& n);
346 
347 #endif
This class represents the notion of an expression. Expressions are derived from SgLocatedNodes, since similar to statement, expressions have a concrete location within the user's source code.