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