Program Listing for File intArithLogical.h#
↰ Return to documentation for file (src/midend/programAnalysis/genericDataflow/lattice/intArithLogical.h)
#include <featureTests.h>
#ifdef ROSE_ENABLE_SOURCE_ANALYSIS
#ifndef INT_ARITH_LOGICAL
#define INT_ARITH_LOGICAL
#include "common.h"
#include "cfgUtils.h"
#include "lattice.h"
#include "logical.h"
#include "nodeState.h"
#include "variables.h"
#include "spearWrap.h"
#include "printAnalysisStates.h"
#include <list>
#include <string>
#include <fstream>
// Represents an expression that uses arithmetic and logical operators
// on a set of integral variables.
class IntArithLogical : public FiniteLattice, public LogicalCond
{
public:
// the information content of this expression/level in the lattice
typedef enum
{
// this object is uninitialized
uninitialized,
// no information is known about the value of the variable
bottom,
// we have a specific formula for this variable (may be True = no information, or False = full information)
known/*,
// this variable can be either positive or negative
top*/
} infContent;
infContent level;
// The possible comparison operations
typedef enum {eq=SpearOp::Equal, le=SpearOp::SgnLTE} cmpOps;
// The possible logical operations
typedef enum {andOp=SpearOp::AndOp, orOp=SpearOp::OrOp, notOp=SpearOp::NotOp} logOps;
class exprLeafOrNode: public virtual SpearExpr
{
public:
typedef enum {eLeaf, lNode} elt;
virtual elt elType()=0;
typedef enum {isTrue, exprKnown, isFalse} infContent;
virtual infContent getLevel()=0;
// Sets this expression to True, returning true if this causes
// the expression to be modified and false otherwise.
virtual bool setToTrue()=0;
// Sets this expression to False, returning true if this causes
// the expression to be modified and false otherwise.
virtual bool setToFalse()=0;
// Negate this logical expression.
// Returns true if this causes this logicNode to change, false otherwise.
virtual bool notUpd()=0;
virtual bool operator==(exprLeafOrNode& that)=0;
bool operator!=(exprLeafOrNode& that) { return !(*this == that); }
// Information order on affine relationships with the least information (True) being highest
// and most information (False) being lowest. Some expressions are not comparable since
// their sets of accepted points are not strictly related to each other.
virtual bool operator<=(exprLeafOrNode& that)=0;
bool operator<(exprLeafOrNode& that) { return (*this != that) && (*this <= that); }
bool operator>=(exprLeafOrNode& that) { return (*this == that) && !(*this <= that); }
bool operator>(exprLeafOrNode& that) { return (*this != that) && (*this >= that); }
// Returns a human-readable string representation of this expression.
// Every line of this string must be prefixed by indent.
// The last character of the returned string should not be '\n', even if it is a multi-line string.
virtual std::string str(std::string indent="")=0;
virtual ~exprLeafOrNode() {}
};
class logicNode;
// A leaf expression: a*x cmpOp b*y + c, where x and y are variables and a,b and c are integers
// These expressions are used conservatively: they must contain no more information than is actually
// known to be true. In other words, given a set R of points (x,y) that satisfy the real condition,
// and the set A of points that satisfy the approximation stored in exprLeaf. R must be a subset of A.
// Lattice: isTrue (all points x,y are accepted when some should not be: zero knowledge)
// exprKnown (exactly correct set of points x,y are accepted: partial knowledge)
// isFalse (no points x,y are accepted: perfect knowledge)
class exprLeaf: public virtual exprLeafOrNode
{
friend class logicNode;
protected:
SpearOp cmp;
int a, b, c;
varID x, y;
exprLeafOrNode::infContent level;
std::list<SpearAbstractVar*> vars;
SpearAbstractVar* outVar;
std::string logExpr;
bool varsExprInitialized;
exprLeaf(SpearOp cmp, int a, varID x, int b, varID y, int c);
public:
exprLeaf(cmpOps cmp, int a, varID x, int b, varID y, int c);
exprLeaf(const exprLeaf& that);
protected:
// divide out from a, b and c any common factors, reducing the triple to its normal form
// return true if this modifies this constraint and false otherwise
bool normalize();
// Sets this expression to True, returning true if this causes
// the expression to be modified and false otherwise.
bool setToTrue();
// Sets this expression to False, returning true if this causes
// the expression to be modified and false otherwise.
bool setToFalse();
infContent getLevel();
// computes vas and logExpr
void computeVarsExpr();
public:
// returns a list of the names of all the variables needed to represent the logical
// expression in this object
const std::list<SpearAbstractVar*>& getVars();
// returns the variable that represents the result of this expression
SpearAbstractVar* getOutVar();
// returns the SPEAR Format expression that represents the constraint in this object
const std::string& getExpr();
// Returns a human-readable string representation of this expression.
// Every line of this string must be prefixed by indent.
// The last character of the returned string should not be '\n', even if it is a multi-line string.
std::string str(std::string indent="");
std::string str(std::string indent="") const;
std::string genStr(std::string indent="") const;
elt elType(){ return exprLeafOrNode::eLeaf; }
SpearExpr* copy();
// Negate this logical expression.
// Returns true if this causes this logicNode to change, false otherwise.
bool notUpd();
// And-s this expression with the given expression, if possible
// Return true if the conjunction is possible and this now contains the conjunction expression and
// false if it is not possible.
// If the conjunction is possible, modified is set to true if the conjunction causes
// this to change and false otherwise.
bool andExprs(const exprLeaf& that, bool &modified);
// returns the same thing as orExprs but doesn't actually perform the conjunction
bool andExprsTest(const exprLeaf& that);
// Or-s this expression with the given expression, if possible
// Return true if the disjunction is possible and this now contains the disjunction expression and
// false if it is not possible.
// If the conjunction is possible, modified is set to true if the conjunction causes
// this to change and false otherwise.
bool orExprs(const exprLeaf& that, bool &modified);
// returns the same thing as andExprs but doesn't actually perform the disjunction
bool orExprsTest(const exprLeaf& that);
bool operator==(exprLeafOrNode& that);
// Information order on affine relationships with the least information (True) being highest
// and most information (False) being lowest. Some expressions are not comparable since
// their sets of accepted points are not strictly related to each other.
bool operator<=(exprLeafOrNode& that);
};
// An internal node that represents a logical connective between the affine relations
class logicNode: public virtual exprLeafOrNode
{
std::list<exprLeafOrNode*> children;
SpearOp logOp;
exprLeafOrNode::infContent level;
bool varsExprInitialized;
std::list<SpearAbstractVar*> vars;
SpearAbstractVar* outVar;
std::string logExpr;
public:
logicNode(logOps logOp);
// constructor for logOp==notOp, which has a single child
logicNode(logOps logOp, exprLeafOrNode* child);
// constructor for logOp==andOp, orOp and xorOp, which have 2+ children
logicNode(logOps logOp, exprLeafOrNode* childA, exprLeafOrNode* childB);
// constructor for logOp==andOp, orOp and xorOp, which have 2+ children
logicNode(logOps logOp, const std::list<exprLeafOrNode*>& children);
logicNode(const logicNode& that);
~logicNode();
// add a new child to this node
void addChild(exprLeafOrNode* child);
protected:
// propagates all the true and false sub-terms upwards through the tree, pruning the appropriate portions
// returns two if this causes the logicNode to change and false otherwise
bool normalize();
public:
// Sets this expression to True, returning true if this causes
// the expression to be modified and false otherwise.
bool setToTrue();
// Sets this expression to False, returning true if this causes
// the expression to be modified and false otherwise.
bool setToFalse();
infContent getLevel();
// returns a list of the names of all the variables needed to represent the logical
// expression in this object
const std::list<SpearAbstractVar*>& getVars();
// returns the variable that represents the result of this expression
SpearAbstractVar* getOutVar();
// returns the SPEAR Format expression that represents the constraint in this object
const std::string& getExpr();
// Returns a human-readable string representation of this expression.
// Every line of this string must be prefixed by indent.
// The last character of the returned string should not be '\n', even if it is a multi-line string.
std::string str(std::string indent="");
std::string str(std::string indent="") const;
std::string genStr(std::string indent="") const;
protected:
void computeVarsExpr();
public:
elt elType(){ return exprLeafOrNode::lNode; }
SpearExpr* copy();
// Negate this logical expression.
// Returns true if this causes this logicNode to change, false otherwise.
bool notUpd();
// given a 2-level expression tree, collects all the permutations of grandchildren
// from each child branch into conjunct logicNodes and saves them in newChildren.
// 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).
// The function works recursively, one child at a time.
// newChildren: The list where we'll save the new conjuncts
// newConjOrig: Accumulated stack of grandchildren that will be combined to form each conjunct
// Thus, for input (A^B)v(C^D)v(D^E)v(F^G)v(H^I), the contents of newConjOrig
// may be A,C,E,F, with H or I to be added when the function recurses again.
// curChild: Iterator that refers to the current child we're processing. The conjuncts
// are formed whenever curChild reaches the end of children.
void genChildrenConj(std::list<exprLeafOrNode*>& newChildren, std::list<exprLeafOrNode*> newConjOrig,
std::list<exprLeafOrNode*>::const_iterator curChild);
// ANDs this and that, storing the result in this.
// Returns true if this causes this logicNode to change, false otherwise.
bool andUpd(logicNode& that);
// OR this and that, storing the result in this.
// Returns true if this causes this logicNode to change, false otherwise.
bool orUpd(logicNode& that);
// Removes all instances of p*var with (q*var + r) and adjusts all relations that involve var
// accordingly.
// Returns true if this causes the logicNode object to change and false otherwise.
bool replaceVar(varID var, int p, int q, int r);
// Removes all facts that relate to the given variable, possibly replacing them
// with other facts that do not involve the variable but could be inferred through
// the removed facts. (i.e. if we have x<y ^ y<z and wish to remove y, the removed
// expressions may be replaced with x<z or just True)
// Returns true if this causes the logicNode object to change and false otherwise.
bool removeVar(varID var);
protected:
// generic function used by orUpd and andUpd to insert new term into a disjunction
// newChildren - The new list of children that will eventually replace children. We will be trying to
// insert newTerm into newChildren.
void insertNewChildOr(std::list<exprLeafOrNode*>& newChildren, exprLeafOrNode* newTerm);
// compares two different children lists, returning true if they're equal and false otherwise
bool eqChildren(std::list<exprLeafOrNode*>& one, std::list<exprLeafOrNode*>& two);
public:
bool operator==(exprLeafOrNode& that);
// Information order on affine relationships with the least information (True) being highest
// and most information (False) being lowest. Some expressions are not comparable since
// their sets of accepted points are not strictly related to each other.
bool operator<=(exprLeafOrNode& that);
};
/*class DNFOrNode : logicNode
{
// Negate this logical expression
void notUpd();
// given a 2-level expression tree, collects all the permutations of grandchildren
// from each child branch into conjunct logicNodes and saves them in newChildren.
// 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).
// The function works recursively, one child at a time.
// newChildren: The list where we'll save the new conjuncts
// newConjOrig: Accumulated stack of grandchildren that will be combined to form each conjunct
// Thus, for input (A^B)v(C^D)v(D^E)v(F^G)v(H^I), the contents of newConjOrig
// may be A,C,E,F, with H or I to be added when the function recurses again.
// curChild: Iterator that refers to the current child we're processing. The conjuncts
// are formed whenever curChild reaches the end of children.
void genChildrenConj(std::list<logicNode*>& newChildren, std::list<exprLeaf*> newConjOrig,
std::list<exprLeafOrNode*>::const_iterator curChild);
};
class DNFAndNode : logicNode
{
// Negate this logical expression
void notUpd();
};*/
// The expression tree itself
logicNode* expr;
public:
// Creates an uninitialized logical expression
IntArithLogical();
// Creates a logical expression that is either True or False, depending on the value argument
IntArithLogical(bool value);
// Create an IntArithLogical that corresponds to a single affine relationship
IntArithLogical(cmpOps cmp, int a, varID x, int b, varID y, int c);
IntArithLogical(const IntArithLogical& that);
// initializes this Lattice to its default bottom state
// if the given new level is higher than bottom, expr is also initialized to a new object
//void initialize(IntArithLogical::infContent newLevel=bottom);
void initialize();
// initializes this Lattice to its default state, with a specific value (true or false)
void initialize(bool value);
// returns a copy of this lattice
Lattice* copy() const;
// overwrites the state of this Lattice with that of that Lattice
void copy(Lattice* that);
// computes the meet of this and that and saves the result in this
// returns true if this causes this to change and false otherwise
bool meetUpdate(Lattice* that);
bool operator==(Lattice* that);
// The string that represents this object
// If indent!="", every line of this string must be prefixed by indent
// The last character of the returned string should not be '\n', even if it is a multi-line string.
std::string str(std::string indent="");
// the basic logical operations that must be supported by any implementation of
// a logical condition: NOT, AND and OR
// Return true if this causes the IntArithLogical object to change and false otherwise.
bool notUpd();
bool andUpd(LogicalCond& that);
bool orUpd(LogicalCond& that);
// Sets this expression to True, returning true if this causes
// the expression to be modified and false otherwise.
bool setToTrue(/*bool onlyIfNotInit=false*/);
// Sets this expression to False, returning true if this causes
// the expression to be modified and false otherwise.
bool setToFalse(/*bool onlyIfNotInit=false*/);
// Removes all facts that relate to the given variable, possibly replacing them
// with other facts that do not involve the variable but could be inferred through
// the removed facts. (i.e. if we have x<y ^ y<z and wish to remove y, the removed
// expressions may be replaced with x<z or just True)
// Returns true if this causes the IntArithLogical object to change and false otherwise.
bool removeVar(varID var);
// returns a copy of this LogicalCond object
LogicalCond* copy();
protected:
// Writes the full expression that corresponds to this object, including any required
// declarations and range constraints to os. Returns that variable that summarizes this expression.
// otherVars - list of variables that also need to be declared and ranged
// createProposition - if true, outputSpearExpr() creates a self-contained proposition. If false, no
// proposition is created; it is presumed that the caller will be using the expression as part
// of a larger proposition.
SpearVar outputSpearExpr(exprLeaf* otherExpr, std::ofstream &os, bool createProposition);
// Runs Spear on the given input file. Returns true if the file's conditions are satisfiable and false otherwise.
static bool runSpear(std::string inputFile);
public:
// Queries whether the given affine relation is implied by this arithmetic/logical constrains.
// Returns true if yes and false otherwise
bool isImplied(cmpOps cmp, int a, varID x, int b, varID y, int c);
// returns true if this logical condition must be true and false otherwise
bool mayTrue();
// Queries whether the arithmetic/logical constrains may be consistent with the given affine relation.
// Returns true if yes and false otherwise
bool mayConsistent(cmpOps cmp, int a, varID x, int b, varID y, int c);
// Updates the expression with the information that x*a has been assigned to y*b+c
// returns true if this causes the expression to change and false otherwise
bool assign(int a, varID x, int b, varID y, int c);
};
/****************************
*** affineInequalityFact ***
****************************/
class IntArithLogicalFact : public NodeFact
{
public:
IntArithLogical expr;
IntArithLogicalFact()
{}
IntArithLogicalFact(const IntArithLogical& expr): expr(expr)
{ }
IntArithLogicalFact(const IntArithLogicalFact& that)
{
this->expr = that.expr;
}
NodeFact* copy() const;
std::string str(std::string indent="");
};
/*****************************
*** IntArithLogicalPlacer ***
*****************************/
class IntArithLogicalPlacer : public UnstructuredPassIntraAnalysis
{
public:
void visit(const Function& func, const DataflowNode& n, NodeState& state);
protected:
// points trueIneqFact and falseIneqFact to freshly allocated objects that represent the true and false
// branches of the control flow guarded by the given expression. They are set to NULL if our representation
// cannot represent one of the expressions.
// doFalseBranch - if =true, falseIneqFact is set to the correct false-branch condition and to NULL otherwise
static void setTrueFalseBranches(SgExpression* expr,
IntArithLogicalFact **trueIneqFact, IntArithLogicalFact **falseIneqFact,
bool doFalseBranch);
};
// prints the inequality facts set by the given affineInequalityPlacer
void printIntArithLogicals(IntArithLogicalPlacer* aip, std::string indent="");
// Runs the Affine Inequality Placer analysis
void runIntArithLogicalPlacer(bool printStates);
// returns the set of IntArithLogical expressions known to be true at the given DataflowNode
const IntArithLogical& getIntArithLogical(const DataflowNode& n);
#endif
#endif