ROSE  0.11.51.0
intArithLogical.h
1 #include <featureTests.h>
2 #ifdef ROSE_ENABLE_SOURCE_ANALYSIS
3 
4 #ifndef INT_ARITH_LOGICAL
5 #define INT_ARITH_LOGICAL
6 
7 #include "common.h"
8 #include "cfgUtils.h"
9 #include "lattice.h"
10 #include "logical.h"
11 #include "nodeState.h"
12 #include "variables.h"
13 #include "spearWrap.h"
14 #include "printAnalysisStates.h"
15 
16 #include <list>
17 #include <string>
18 #include <fstream>
19 
20 // Represents an expression that uses arithmetic and logical operators
21 // on a set of integral variables.
23 {
24 public:
25  // the information content of this expression/level in the lattice
26  typedef enum
27  {
28  // this object is uninitialized
29  uninitialized,
30  // no information is known about the value of the variable
31  bottom,
32  // we have a specific formula for this variable (may be True = no information, or False = full information)
33  known/*,
34  // this variable can be either positive or negative
35  top*/
36  } infContent;
37 
38  infContent level;
39 
40 
41  // The possible comparison operations
42  typedef enum {eq=SpearOp::Equal, le=SpearOp::SgnLTE} cmpOps;
43 
44  // The possible logical operations
45  typedef enum {andOp=SpearOp::AndOp, orOp=SpearOp::OrOp, notOp=SpearOp::NotOp} logOps;
46 
47  class exprLeafOrNode: public virtual SpearExpr
48  {
49  public:
50  typedef enum {eLeaf, lNode} elt;
51  virtual elt elType()=0;
52 
53  typedef enum {isTrue, exprKnown, isFalse} infContent;
54  virtual infContent getLevel()=0;
55 
56  // Sets this expression to True, returning true if this causes
57  // the expression to be modified and false otherwise.
58  virtual bool setToTrue()=0;
59 
60  // Sets this expression to False, returning true if this causes
61  // the expression to be modified and false otherwise.
62  virtual bool setToFalse()=0;
63 
64  // Negate this logical expression.
65  // Returns true if this causes this logicNode to change, false otherwise.
66  virtual bool notUpd()=0;
67 
68  virtual bool operator==(exprLeafOrNode& that)=0;
69  bool operator!=(exprLeafOrNode& that) { return !(*this == that); }
70 
71  // Information order on affine relationships with the least information (True) being highest
72  // and most information (False) being lowest. Some expressions are not comparable since
73  // their sets of accepted points are not strictly related to each other.
74  virtual bool operator<=(exprLeafOrNode& that)=0;
75  bool operator<(exprLeafOrNode& that) { return (*this != that) && (*this <= that); }
76  bool operator>=(exprLeafOrNode& that) { return (*this == that) && !(*this <= that); }
77  bool operator>(exprLeafOrNode& that) { return (*this != that) && (*this >= that); }
78 
79  // Returns a human-readable string representation of this expression.
80  // Every line of this string must be prefixed by indent.
81  // The last character of the returned string should not be '\n', even if it is a multi-line string.
82  virtual std::string str(std::string indent="")=0;
83 
84  virtual ~exprLeafOrNode() {}
85  };
86 
87  class logicNode;
88 
89  // A leaf expression: a*x cmpOp b*y + c, where x and y are variables and a,b and c are integers
90  // These expressions are used conservatively: they must contain no more information than is actually
91  // known to be true. In other words, given a set R of points (x,y) that satisfy the real condition,
92  // and the set A of points that satisfy the approximation stored in exprLeaf. R must be a subset of A.
93  // Lattice: isTrue (all points x,y are accepted when some should not be: zero knowledge)
94  // exprKnown (exactly correct set of points x,y are accepted: partial knowledge)
95  // isFalse (no points x,y are accepted: perfect knowledge)
96  class exprLeaf: public virtual exprLeafOrNode
97  {
98  friend class logicNode;
99 
100  protected:
101  SpearOp cmp;
102  int a, b, c;
103  varID x, y;
104 
105  exprLeafOrNode::infContent level;
106 
107  std::list<SpearAbstractVar*> vars;
108  SpearAbstractVar* outVar;
109  std::string logExpr;
110  bool varsExprInitialized;
111 
112  exprLeaf(SpearOp cmp, int a, varID x, int b, varID y, int c);
113 
114  public:
115  exprLeaf(cmpOps cmp, int a, varID x, int b, varID y, int c);
116 
117  exprLeaf(const exprLeaf& that);
118 
119  protected:
120  // divide out from a, b and c any common factors, reducing the triple to its normal form
121  // return true if this modifies this constraint and false otherwise
122  bool normalize();
123 
124  // Sets this expression to True, returning true if this causes
125  // the expression to be modified and false otherwise.
126  bool setToTrue();
127 
128  // Sets this expression to False, returning true if this causes
129  // the expression to be modified and false otherwise.
130  bool setToFalse();
131 
132  infContent getLevel();
133 
134  // computes vas and logExpr
135  void computeVarsExpr();
136 
137  public:
138 
139  // returns a list of the names of all the variables needed to represent the logical
140  // expression in this object
141  const std::list<SpearAbstractVar*>& getVars();
142 
143  // returns the variable that represents the result of this expression
144  SpearAbstractVar* getOutVar();
145 
146  // returns the SPEAR Format expression that represents the constraint in this object
147  const std::string& getExpr();
148 
149  // Returns a human-readable string representation of this expression.
150  // Every line of this string must be prefixed by indent.
151  // The last character of the returned string should not be '\n', even if it is a multi-line string.
152  std::string str(std::string indent="");
153  std::string str(std::string indent="") const;
154  std::string genStr(std::string indent="") const;
155 
156  elt elType(){ return exprLeafOrNode::eLeaf; }
157 
158  SpearExpr* copy();
159 
160  // Negate this logical expression.
161  // Returns true if this causes this logicNode to change, false otherwise.
162  bool notUpd();
163 
164  // And-s this expression with the given expression, if possible
165  // Return true if the conjunction is possible and this now contains the conjunction expression and
166  // false if it is not possible.
167  // If the conjunction is possible, modified is set to true if the conjunction causes
168  // this to change and false otherwise.
169  bool andExprs(const exprLeaf& that, bool &modified);
170  // returns the same thing as orExprs but doesn't actually perform the conjunction
171  bool andExprsTest(const exprLeaf& that);
172 
173  // Or-s this expression with the given expression, if possible
174  // Return true if the disjunction is possible and this now contains the disjunction expression and
175  // false if it is not possible.
176  // If the conjunction is possible, modified is set to true if the conjunction causes
177  // this to change and false otherwise.
178  bool orExprs(const exprLeaf& that, bool &modified);
179  // returns the same thing as andExprs but doesn't actually perform the disjunction
180  bool orExprsTest(const exprLeaf& that);
181 
182  bool operator==(exprLeafOrNode& that);
183 
184  // Information order on affine relationships with the least information (True) being highest
185  // and most information (False) being lowest. Some expressions are not comparable since
186  // their sets of accepted points are not strictly related to each other.
187  bool operator<=(exprLeafOrNode& that);
188  };
189 
190  // An internal node that represents a logical connective between the affine relations
191  class logicNode: public virtual exprLeafOrNode
192  {
193  std::list<exprLeafOrNode*> children;
194  SpearOp logOp;
195  exprLeafOrNode::infContent level;
196 
197  bool varsExprInitialized;
198  std::list<SpearAbstractVar*> vars;
199  SpearAbstractVar* outVar;
200  std::string logExpr;
201 
202  public:
203  logicNode(logOps logOp);
204 
205  // constructor for logOp==notOp, which has a single child
206  logicNode(logOps logOp, exprLeafOrNode* child);
207 
208  // constructor for logOp==andOp, orOp and xorOp, which have 2+ children
209  logicNode(logOps logOp, exprLeafOrNode* childA, exprLeafOrNode* childB);
210 
211  // constructor for logOp==andOp, orOp and xorOp, which have 2+ children
212  logicNode(logOps logOp, const std::list<exprLeafOrNode*>& children);
213 
214  logicNode(const logicNode& that);
215 
216  ~logicNode();
217 
218  // add a new child to this node
219  void addChild(exprLeafOrNode* child);
220 
221  protected:
222  // propagates all the true and false sub-terms upwards through the tree, pruning the appropriate portions
223  // returns two if this causes the logicNode to change and false otherwise
224  bool normalize();
225 
226  public:
227  // Sets this expression to True, returning true if this causes
228  // the expression to be modified and false otherwise.
229  bool setToTrue();
230 
231  // Sets this expression to False, returning true if this causes
232  // the expression to be modified and false otherwise.
233  bool setToFalse();
234 
235  infContent getLevel();
236 
237  // returns a list of the names of all the variables needed to represent the logical
238  // expression in this object
239  const std::list<SpearAbstractVar*>& getVars();
240 
241  // returns the variable that represents the result of this expression
242  SpearAbstractVar* getOutVar();
243 
244  // returns the SPEAR Format expression that represents the constraint in this object
245  const std::string& getExpr();
246 
247  // Returns a human-readable string representation of this expression.
248  // Every line of this string must be prefixed by indent.
249  // The last character of the returned string should not be '\n', even if it is a multi-line string.
250  std::string str(std::string indent="");
251  std::string str(std::string indent="") const;
252  std::string genStr(std::string indent="") const;
253 
254  protected:
255  void computeVarsExpr();
256 
257  public:
258  elt elType(){ return exprLeafOrNode::lNode; }
259 
260  SpearExpr* copy();
261 
262  // Negate this logical expression.
263  // Returns true if this causes this logicNode to change, false otherwise.
264  bool notUpd();
265 
266  // given a 2-level expression tree, collects all the permutations of grandchildren
267  // from each child branch into conjunct logicNodes and saves them in newChildren.
268  // Thus, (A^B^C)v(D^E^F) would become the list (A^D),(A^E),(A^F),(B^D),(B^E),(B^F),(C^D),(C^E),(C^F).
269  // The function works recursively, one child at a time.
270  // newChildren: The list where we'll save the new conjuncts
271  // newConjOrig: Accumulated stack of grandchildren that will be combined to form each conjunct
272  // Thus, for input (A^B)v(C^D)v(D^E)v(F^G)v(H^I), the contents of newConjOrig
273  // may be A,C,E,F, with H or I to be added when the function recurses again.
274  // curChild: Iterator that refers to the current child we're processing. The conjuncts
275  // are formed whenever curChild reaches the end of children.
276  void genChildrenConj(std::list<exprLeafOrNode*>& newChildren, std::list<exprLeafOrNode*> newConjOrig,
277  std::list<exprLeafOrNode*>::const_iterator curChild);
278 
279  // ANDs this and that, storing the result in this.
280  // Returns true if this causes this logicNode to change, false otherwise.
281  bool andUpd(logicNode& that);
282 
283  // OR this and that, storing the result in this.
284  // Returns true if this causes this logicNode to change, false otherwise.
285  bool orUpd(logicNode& that);
286 
287  // Removes all instances of p*var with (q*var + r) and adjusts all relations that involve var
288  // accordingly.
289  // Returns true if this causes the logicNode object to change and false otherwise.
290  bool replaceVar(varID var, int p, int q, int r);
291 
292  // Removes all facts that relate to the given variable, possibly replacing them
293  // with other facts that do not involve the variable but could be inferred through
294  // the removed facts. (i.e. if we have x<y ^ y<z and wish to remove y, the removed
295  // expressions may be replaced with x<z or just True)
296  // Returns true if this causes the logicNode object to change and false otherwise.
297  bool removeVar(varID var);
298 
299  protected:
300  // generic function used by orUpd and andUpd to insert new term into a disjunction
301  // newChildren - The new list of children that will eventually replace children. We will be trying to
302  // insert newTerm into newChildren.
303  void insertNewChildOr(std::list<exprLeafOrNode*>& newChildren, exprLeafOrNode* newTerm);
304 
305  // compares two different children lists, returning true if they're equal and false otherwise
306  bool eqChildren(std::list<exprLeafOrNode*>& one, std::list<exprLeafOrNode*>& two);
307 
308  public:
309  bool operator==(exprLeafOrNode& that);
310 
311  // Information order on affine relationships with the least information (True) being highest
312  // and most information (False) being lowest. Some expressions are not comparable since
313  // their sets of accepted points are not strictly related to each other.
314  bool operator<=(exprLeafOrNode& that);
315  };
316 
317  /*class DNFOrNode : logicNode
318  {
319  // Negate this logical expression
320  void notUpd();
321 
322  // given a 2-level expression tree, collects all the permutations of grandchildren
323  // from each child branch into conjunct logicNodes and saves them in newChildren.
324  // Thus, (A^B^C)v(D^E^F) would become the list (A^D),(A^E),(A^F),(B^D),(B^E),(B^F),(C^D),(C^E),(C^F).
325  // The function works recursively, one child at a time.
326  // newChildren: The list where we'll save the new conjuncts
327  // newConjOrig: Accumulated stack of grandchildren that will be combined to form each conjunct
328  // Thus, for input (A^B)v(C^D)v(D^E)v(F^G)v(H^I), the contents of newConjOrig
329  // may be A,C,E,F, with H or I to be added when the function recurses again.
330  // curChild: Iterator that refers to the current child we're processing. The conjuncts
331  // are formed whenever curChild reaches the end of children.
332  void genChildrenConj(std::list<logicNode*>& newChildren, std::list<exprLeaf*> newConjOrig,
333  std::list<exprLeafOrNode*>::const_iterator curChild);
334  };
335 
336  class DNFAndNode : logicNode
337  {
338  // Negate this logical expression
339  void notUpd();
340  };*/
341 
342  // The expression tree itself
343  logicNode* expr;
344 
345  public:
346  // Creates an uninitialized logical expression
347  IntArithLogical();
348 
349  // Creates a logical expression that is either True or False, depending on the value argument
350  IntArithLogical(bool value);
351 
352  // Create an IntArithLogical that corresponds to a single affine relationship
353  IntArithLogical(cmpOps cmp, int a, varID x, int b, varID y, int c);
354 
355  IntArithLogical(const IntArithLogical& that);
356 
357  // initializes this Lattice to its default bottom state
358  // if the given new level is higher than bottom, expr is also initialized to a new object
359  //void initialize(IntArithLogical::infContent newLevel=bottom);
360  void initialize();
361 
362  // initializes this Lattice to its default state, with a specific value (true or false)
363  void initialize(bool value);
364 
365  // returns a copy of this lattice
366  Lattice* copy() const;
367  // overwrites the state of this Lattice with that of that Lattice
368  void copy(Lattice* that);
369 
370  // computes the meet of this and that and saves the result in this
371  // returns true if this causes this to change and false otherwise
372  bool meetUpdate(Lattice* that);
373 
374  bool operator==(Lattice* that);
375 
376  // The string that represents this object
377  // If indent!="", every line of this string must be prefixed by indent
378  // The last character of the returned string should not be '\n', even if it is a multi-line string.
379  std::string str(std::string indent="");
380 
381  // the basic logical operations that must be supported by any implementation of
382  // a logical condition: NOT, AND and OR
383  // Return true if this causes the IntArithLogical object to change and false otherwise.
384  bool notUpd();
385  bool andUpd(LogicalCond& that);
386  bool orUpd(LogicalCond& that);
387 
388  // Sets this expression to True, returning true if this causes
389  // the expression to be modified and false otherwise.
391  bool setToTrue(/*bool onlyIfNotInit=false*/);
392 
393  // Sets this expression to False, returning true if this causes
394  // the expression to be modified and false otherwise.
396  bool setToFalse(/*bool onlyIfNotInit=false*/);
397 
398  // Removes all facts that relate to the given variable, possibly replacing them
399  // with other facts that do not involve the variable but could be inferred through
400  // the removed facts. (i.e. if we have x<y ^ y<z and wish to remove y, the removed
401  // expressions may be replaced with x<z or just True)
402  // Returns true if this causes the IntArithLogical object to change and false otherwise.
403  bool removeVar(varID var);
404 
405  // returns a copy of this LogicalCond object
406  LogicalCond* copy();
407 
408  protected:
409  // Writes the full expression that corresponds to this object, including any required
410  // declarations and range constraints to os. Returns that variable that summarizes this expression.
411  // otherVars - list of variables that also need to be declared and ranged
412  // createProposition - if true, outputSpearExpr() creates a self-contained proposition. If false, no
413  // proposition is created; it is presumed that the caller will be using the expression as part
414  // of a larger proposition.
415  SpearVar outputSpearExpr(exprLeaf* otherExpr, std::ofstream &os, bool createProposition);
416 
417  // Runs Spear on the given input file. Returns true if the file's conditions are satisfiable and false otherwise.
418  static bool runSpear(std::string inputFile);
419 
420  public:
421  // Queries whether the given affine relation is implied by this arithmetic/logical constrains.
422  // Returns true if yes and false otherwise
423  bool isImplied(cmpOps cmp, int a, varID x, int b, varID y, int c);
424 
425  // returns true if this logical condition must be true and false otherwise
426  bool mayTrue();
427 
428  // Queries whether the arithmetic/logical constrains may be consistent with the given affine relation.
429  // Returns true if yes and false otherwise
430  bool mayConsistent(cmpOps cmp, int a, varID x, int b, varID y, int c);
431 
432  // Updates the expression with the information that x*a has been assigned to y*b+c
433  // returns true if this causes the expression to change and false otherwise
434  bool assign(int a, varID x, int b, varID y, int c);
435 };
436 
437 /****************************
438  *** affineInequalityFact ***
439  ****************************/
440 
442 {
443  public:
444  IntArithLogical expr;
445 
447  {}
448 
449  IntArithLogicalFact(const IntArithLogical& expr): expr(expr)
450  { }
451 
453  {
454  this->expr = that.expr;
455  }
456 
457  NodeFact* copy() const;
458 
459  std::string str(std::string indent="");
460 };
461 
462 /*****************************
463  *** IntArithLogicalPlacer ***
464  *****************************/
465 
467 {
468  public:
469  void visit(const Function& func, const DataflowNode& n, NodeState& state);
470 
471  protected:
472  // points trueIneqFact and falseIneqFact to freshly allocated objects that represent the true and false
473  // branches of the control flow guarded by the given expression. They are set to NULL if our representation
474  // cannot represent one of the expressions.
475  // doFalseBranch - if =true, falseIneqFact is set to the correct false-branch condition and to NULL otherwise
476  static void setTrueFalseBranches(SgExpression* expr,
477  IntArithLogicalFact **trueIneqFact, IntArithLogicalFact **falseIneqFact,
478  bool doFalseBranch);
479 };
480 
481 // prints the inequality facts set by the given affineInequalityPlacer
482 void printIntArithLogicals(IntArithLogicalPlacer* aip, std::string indent="");
483 
484 // Runs the Affine Inequality Placer analysis
485 void runIntArithLogicalPlacer(bool printStates);
486 
487 // returns the set of IntArithLogical expressions known to be true at the given DataflowNode
488 const IntArithLogical& getIntArithLogical(const DataflowNode& n);
489 
490 #endif
491 #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.