ROSE  0.11.109.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
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.