constraint.h

Go to the documentation of this file.
00001 /*
00002  * Copyright (C) 2003, Mike Van Emmerik
00003  *
00004  * See the file "LICENSE.TERMS" for information on usage and
00005  * redistribution of this file, and for a DISCLAIMER OF ALL
00006  * WARRANTIES.
00007  *
00008  */
00009 
00010 /*==============================================================================
00011  * FILE:       constraint.h
00012  * OVERVIEW:   Definition of objects related to type constraints
00013  *============================================================================*/
00014 
00015 /*
00016  * $Revision: 1.10 $
00017  *
00018  * 22 Aug 03 - Mike: Created
00019  */
00020 
00021 #include "statement.h"
00022 #include "exp.h"
00023 #include <sstream>
00024 
00025 // This class represents fixed constraints (e.g. Ta = <int>, Tb = <alpha2*>),
00026 // but also "tentative" constraints resulting from disjunctions of constraints
00027 class ConstraintMap {
00028     std::map<Exp*, Exp*, lessExpStar> cmap;
00029 public:
00030 typedef std::map<Exp*, Exp*, lessExpStar>::iterator iterator;
00031 
00032     // Return true if the given expression is in the map
00033     bool isFound(Exp* e)  {return cmap.find(e) != cmap.end();}
00034     // Return an iterator to the given left hand side Exp
00035     iterator find(Exp* e) {return cmap.find(e);}
00036     // Lookup a given left hand side Exp (e.g. given Tlocal1, return <char*>)
00037     Exp*& operator[](Exp* e) {return cmap[e];}
00038     // Return the number of constraints in the map
00039     int   size() {return cmap.size();}
00040     // Empty the map
00041     void  clear() {cmap.clear();}
00042     // Return iterators for the begin() and end() of the map
00043     iterator begin() {return cmap.begin();}
00044     iterator end()   {return cmap.end();}
00045     // Insert a constraint given two locations (i.e. Tloc1 = Tloc2)
00046     void constrain(Exp* loc1, Exp* loc2) {
00047         cmap[new Unary(opTypeOf, loc1)] = new Unary(opTypeOf, loc2);}
00048     // Insert a constraint given an equality expression
00049     // e.g. Tlocal1 = <char*>
00050     void insert(Exp* term);
00051     // Insert a constraint given left and right hand sides (as type Exps)
00052     void insert(Exp* lhs, Exp* rhs) {cmap[lhs] = rhs;}
00053     // Insert a constraint given a location and a Type
00054     void constrain(Exp* loc, Type* t) {
00055         cmap[new Unary(opTypeOf, loc)] = new TypeVal(t);}
00056     // Insert a constraint given two Types (at least one variable)
00057     void constrain(Type* t1, Type* t2) { // Example: alpha1 = alpha2
00058         cmap[new TypeVal(t1)] = new TypeVal(t2);}
00059     // Union with another constraint map
00060     void makeUnion(ConstraintMap& o);
00061     // Print to the given stream
00062     void print(std::ostream& os);
00063     // Print to the debug buffer, and return that buffer
00064     char* prints();
00065     // Substitute the given constraints into this map
00066     void    substitute(ConstraintMap& other);
00067     // For this solution, we need to find disjunctions of the form
00068     // <alphaN> = <type>      or
00069     // <type>   = <alphaN>
00070     // and substitute these into each part of the solution
00071     void    substAlpha();
00072 };  // class ConstraintMap
00073 
00074 // A class used for fast location of a constraint
00075 // An equation like Ta = Tb is inserted into this class twice (i.e. as
00076 // Ta = Tb and also as Tb = Ta. So to find out if Ta is involved in an
00077 // equate, only have to look up Ta in the map (on the LHS, which is fast)
00078 class EquateMap {
00079     std::map<Exp*, LocationSet, lessExpStar> emap;
00080 public:
00081 typedef std::map<Exp*, LocationSet, lessExpStar>::iterator iterator;
00082     iterator begin() {return emap.begin();}
00083     iterator end()   {return emap.end();}
00084     void erase(iterator it) {emap.erase(it);}
00085     int  size() {return emap.size();}
00086     // Add an equate (both ways)
00087     void addEquate(Exp* a, Exp* b) {
00088         emap[a].insert(b); emap[b].insert(a);}
00089     iterator find(Exp* e) {return emap.find(e);}
00090     void print(std::ostream& os);
00091     char* prints();
00092 };  // class EquateMap
00093 
00094 class Constraints {
00095     LocationSet     conSet;
00096     std::list<Exp*> disjunctions;
00097     // Map from location to a fixed type (could be a pointer to a variable
00098     // type, i.e. an alpha).
00099     ConstraintMap fixed;
00100     // EquateMap of locations that are equal
00101     EquateMap equates;
00102 
00103 public:
00104     Constraints() {}
00105     ~Constraints();
00106 
00107     void    print(std::ostream& os);
00108     char*   prints();
00109 
00110     LocationSet& getConstraints() {return conSet;}
00111     void    addConstraints(LocationSet& con) {conSet.makeUnion(con);}
00112     // Substitute the given constraintMap into the disjuncts
00113     void    substIntoDisjuncts(ConstraintMap& in);
00114     // Substitute the given constraintMap into the equates
00115     void    substIntoEquates(ConstraintMap& in);
00116     // Perform "alpha substitution". Example:
00117     //   <fixedtype*> = alphaX* and T[Y] = alphaX*  ->
00118     //   T[Y] = <fixedtype*>
00119     void    alphaSubst();
00120 
00121     // Solve the constraints. If they can be solved, return true and put
00122     // a copy of the solution (in the form of a set of T<location> = <type>)
00123     // into solns
00124     bool    solve(std::list<ConstraintMap>& solns);
00125 private:
00126     bool    doSolve(std::list<Exp*>::iterator it, ConstraintMap& extra,
00127               std::list<ConstraintMap>& solns);
00128     // Test for compatibility of these types. Sometimes, they are compatible
00129     // with an extra constraint (e.g. alpha3* is compatible with alpha4* with
00130     // the extra constraint that alpha3 == alpha4)
00131     bool    unify(Exp* x, Exp* y, ConstraintMap& extra);
00132 };  // class Constraints

Generated on Tue Sep 19 21:18:15 2006 for Boomerang by  doxygen 1.4.6