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