Changes:
authorbdemsky <bdemsky>
Wed, 21 Apr 2004 21:16:15 +0000 (21:16 +0000)
committerbdemsky <bdemsky>
Wed, 21 Apr 2004 21:16:15 +0000 (21:16 +0000)
1) Cleaned up CLI/Compiler classes that Dan provided.
2) Typecheck Constraints.
3) Repair dependence analysis (to order repair of constraints)
   A) checks for functions
4) Added class to compute exact sizes of sets (and constraints which
   establish these sizes)

19 files changed:
Repair/RepairCompiler/MCC/CLI.java
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/Conjunction.java
Repair/RepairCompiler/MCC/IR/Constraint.java
Repair/RepairCompiler/MCC/IR/ConstraintDependence.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/DotExpr.java
Repair/RepairCompiler/MCC/IR/ExactSize.java [new file with mode: 0755]
Repair/RepairCompiler/MCC/IR/Expr.java
Repair/RepairCompiler/MCC/IR/ExprPredicate.java
Repair/RepairCompiler/MCC/IR/InclusionPredicate.java
Repair/RepairCompiler/MCC/IR/LogicStatement.java
Repair/RepairCompiler/MCC/IR/OpExpr.java
Repair/RepairCompiler/MCC/IR/RelationExpr.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/IR/SemanticChecker.java
Repair/RepairCompiler/MCC/IR/Sources.java
Repair/RepairCompiler/MCC/IR/Termination.java
Repair/RepairCompiler/MCC/IR/VarDescriptor.java
Repair/RepairCompiler/MCC/IR/VarExpr.java

index 609455a..f03831e 100755 (executable)
@@ -11,47 +11,9 @@ import java.util.StringTokenizer;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.2 2004/04/15 05:41:46 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.3 2004/04/21 21:15:48 bdemsky Exp $</tt>
  */
 public class CLI {
-    /**
-     * Target value indicating that the compiler should produce its
-     * default output.
-     */
-    public static final int DEFAULT = 0;
-
-    /**
-     * Target value indicating that the compiler should scan the input
-     * and stop.
-     */
-    public static final int SCAN = 1;
-
-    /**
-     * Target value indicating that the compiler should scan and parse
-     * its input, and stop.
-     */
-    public static final int PARSE = 2;
-
-    /**
-     * Target value indicating that the compiler should produce a
-     * high-level intermediate representation from its input, and stop.
-     * This is not one of the segment targets for Fall 2000, but you
-     * may wish to use it for your own purposes.
-     */
-    public static final int INTER = 3;
-
-    /**
-     * Target value indicating that the compiler should produce a
-     * low-level intermediate representation from its input, and stop.
-     */
-    public static final int LOWIR = 4;
-
-    /**
-     * Target value indicating that the compiler should produce
-     * assembly from its input.
-     */
-    public static final int ASSEMBLY = 5;
-
     /**
      * Array indicating which optimizations should be performed.  If
      * a particular element is true, it indicates that the optimization
@@ -84,42 +46,12 @@ public class CLI {
      */
     public String infile;
 
-    /**
-     * The target stage.  This should be one of the integer constants
-     * defined elsewhere in this package.
-     */
-    public int target;
-
     /**
      * The debug flag.  This is true if <tt>-debug</tt> was passed on
      * the command line, requesting debugging output.
      */
     public boolean debug;
 
-    /**
-     * Native MIPS architecture is specified by "-native".  The default
-     * is SPIM.
-     */
-    public boolean fNative;
-
-    /**
-     * Runs IRVis on final node tree.
-     */
-    public boolean fVis;
-    public String visClass;
-    public String visMethod;
-
-    /**
-     * Dumps the before and after Node structure to two files that can be diffed.
-     */
-    public boolean fDiff;
-    public String diffFile;
-
-    /**
-     * Maximum optimization iterations.
-     */
-    public int numIterations = 5;
-
     /**
      * Verbose output
      */
@@ -134,16 +66,9 @@ public class CLI {
     public CLI() {
         outfile = null;
         infile = null;
-        target = DEFAULT;
         extras = new Vector();
         extraopts = new Vector();
-        fNative = false;
-        fVis = false;
         verbose = 0;
-        visClass = "";
-        visMethod = "";
-        fDiff = false;
-        diffFile = "";
     }
 
     /**
@@ -177,19 +102,8 @@ public class CLI {
             if (args[i].equals("-debug")) {
                 context = 0;
                 debug = true;
-           } else if (args[i].equals("-native")) {
-                context = 0;
-                fNative = true;
            } else if (args[i].equals("-checkonly")) {
                 Compiler.REPAIR=false;
-            } else if (args[i].equals("-vis")) {
-                context = 4;
-                fVis = true;
-            } else if (args[i].equals("-diff")) {
-                context = 5;
-                fDiff = true;
-            } else if (args[i].equals("-i")) {
-                context = 6;
             } else if (args[i].equals("-verbose") || args[i].equals("-v")) {
                 context = 0;
                 verbose++;
@@ -197,8 +111,6 @@ public class CLI {
                 context = 1;
             else if (args[i].equals("-o"))
                 context = 2;
-            else if (args[i].equals("-target"))
-                context = 3;
             else if (context == 1) {
                 boolean hit = false;
                 for (int j = 0; j < optnames.length; j++) {
@@ -214,41 +126,9 @@ public class CLI {
                }
                 if (!hit)
                     extraopts.addElement(args[i]);
-           }
-            else if (context == 2) {
+           } else if (context == 2) {
                 outfile = args[i];
                 context = 0;
-           }
-            else if (context == 3) {
-                // Process case insensitive.
-                String argSansCase = args[i].toLowerCase();
-                // accept "scan" and "scanner" due to handout mistake
-                if (argSansCase.equals("scan") || 
-                    argSansCase.equals("scanner"))
-                    target = SCAN;
-                else if (argSansCase.equals("parse"))
-                    target = PARSE;
-                else if (argSansCase.equals("inter"))
-                    target = INTER;
-                else if (argSansCase.equals("lowir"))
-                    target = LOWIR;
-                else if (argSansCase.equals("assembly") ||
-                         argSansCase.equals("codegen"))
-                    target = ASSEMBLY;
-                else
-                    target = DEFAULT; // Anything else is just default
-                context = 0;
-           } else if (context == 4) { // -vis
-                StringTokenizer st = new StringTokenizer(args[i], ".");
-                visClass = st.nextToken();
-                visMethod = st.nextToken();
-                context = 0;
-           } else if (context == 5) { // -diff
-                diffFile = args[i]; // argument following is filename
-                context = 0;
-           } else if (context == 6) { // -i <iterations>
-                numIterations = Integer.parseInt(args[i]);
-                context = 0;
             } else {
                boolean hit = false;
                for (int j = 0; j < optnames.length; j++) {
@@ -275,40 +155,5 @@ public class CLI {
            }
             i++;
        }
-
-        // create outfile name
-        switch (target) {
-        case SCAN:
-            ext = ".scan";
-            break;
-        case PARSE:
-            ext = ".parse";
-            break;
-        case INTER:
-            ext = ".ir";
-            break;
-        case LOWIR:
-            ext = ".lowir";
-            break;
-        case ASSEMBLY:
-            ext = ".s";
-            break;
-        case DEFAULT:
-        default:
-            ext = ".out";
-            break;
-        }
-
-        if (outfile == null && infile != null) {
-            int dot = infile.lastIndexOf('.');
-            int slash = infile.lastIndexOf('/');
-            // Last dot comes after last slash means that the file
-            // has an extention.  Note that the base case where dot
-            // or slash are -1 also work.
-            if (dot <= slash)
-                outfile = infile + ext;
-            else
-                outfile = infile.substring(0, dot) + ext;
-       }
     }
 }
index 949ae87..c0dca65 100755 (executable)
@@ -46,111 +46,71 @@ public class Compiler {
            System.exit(-1);
        }
         
-       if (cli.target == CLI.ASSEMBLY || cli.target == CLI.DEFAULT) {
-           if (state.debug) {
-               System.out.println("Compiling " + cli.infile + ".");
-           }
-
-           success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
-           success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
-           success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
-
-
-           Termination termination=null;
-           /* Check partition constraints */
-           (new ImplicitSchema(state)).update();
-           termination=new Termination(state);
-
-            state.printall();
-            (new DependencyBuilder(state)).calculate();
-            
-            try {
-                Vector nodes = new Vector(state.constraintnodes.values());
-                nodes.addAll(state.rulenodes.values());
-
-                FileOutputStream dotfile;
-                dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot");
-                GraphNode.useEdgeLabels = true;
-                GraphNode.DOTVisitor.visit(dotfile, nodes);
-                dotfile.close();
-
-                dotfile = new FileOutputStream(cli.infile + ".dependencies.dot");
-                GraphNode.useEdgeLabels = false;
-                GraphNode.DOTVisitor.visit(dotfile, nodes);                
-                dotfile.close();
-            } catch (Exception e) {
-                e.printStackTrace();
-                System.exit(-1);
-            }
-            
-            try {
-                FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
-
-
-                // do model optimizations
-                //(new Optimizer(state)).optimize();
-
-
-
-               FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
-               FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
-               RepairGenerator wg = new RepairGenerator(state,termination);
-               wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
-               gcode2.close();
-               gcode3.close();
-               /*              } else {
-                   WorklistGenerator ng = new WorklistGenerator(state);
+       if (state.debug) {
+           System.out.println("Compiling " + cli.infile + ".");
+       }
+       
+       success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
+       success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
+       success = semantics(state) || error(state, "Semantic analysis failed, not attempting variable initialization.");
+       
+       
+       Termination termination=null;
+       /* Check partition constraints */
+       (new ImplicitSchema(state)).update();
+       termination=new Termination(state);
+       
+       state.printall();
+       (new DependencyBuilder(state)).calculate();
+       
+       try {
+           Vector nodes = new Vector(state.constraintnodes.values());
+           nodes.addAll(state.rulenodes.values());
+           
+           FileOutputStream dotfile;
+           dotfile = new FileOutputStream(cli.infile + ".dependencies.edgelabels.dot");
+           GraphNode.useEdgeLabels = true;
+           GraphNode.DOTVisitor.visit(dotfile, nodes);
+           dotfile.close();
+           
+           dotfile = new FileOutputStream(cli.infile + ".dependencies.dot");
+           GraphNode.useEdgeLabels = false;
+           GraphNode.DOTVisitor.visit(dotfile, nodes);                
+           dotfile.close();
+       } catch (Exception e) {
+           e.printStackTrace();
+           System.exit(-1);
+       }
+       
+       try {
+           FileOutputStream gcode = new FileOutputStream(cli.infile + ".cc");
+           
+           
+           // do model optimizations
+           //(new Optimizer(state)).optimize();
+           
+           FileOutputStream gcode2 = new FileOutputStream(cli.infile + "_aux.cc");
+           FileOutputStream gcode3 = new FileOutputStream(cli.infile + "_aux.h");
+           RepairGenerator wg = new RepairGenerator(state,termination);
+           wg.generate(gcode,gcode2,gcode3, cli.infile + "_aux.h");
+           gcode2.close();
+           gcode3.close();
+           /*          } else {
+                       WorklistGenerator ng = new WorklistGenerator(state);
                    SetInclusion.worklist=true;
                    RelationInclusion.worklist=true;
                    ng.generate(gcode);
                    }*/
-                gcode.close();
-            } catch (Exception e) {
-                e.printStackTrace();
-                System.exit(-1);
-            }
-            
-           if (state.debug) {
-               System.out.println("Compilation of " + state.infile + " successful.");
-               System.out.println("#SUCCESS#");
-           }
-       } else if (cli.target == CLI.INTER) {
-           if (state.debug) {
-               System.out.println("Semantic analysis for " + cli.infile + ".");
-           }
-
-           success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
-           success = parse(state) || error(state, "Parsing failed, not attempting semantic analysis.");
-           success = semantics(state) || error(state, "Semantic analysis failed.");
-
-           if (state.debug) {
-               System.out.println("Semantic analysis of " + state.infile + " successful.");
-               System.out.println("#SUCCESS#");
-           }
-       } else if (cli.target == CLI.PARSE) {
-           if (state.debug) {
-               System.out.println("Parsing " + cli.infile + ".");
-           }
-
-           success = scan(state) || error(state, "Scanning failed, not attempting to parse.");
-           success = parse(state) || error(state, "Parsing failed.");
-
-           if (state.debug) {
-               System.out.println("Parsing of " + state.infile + " successful.");
-               System.out.println("#SUCCESS#");
-           }
-        } else if (cli.target == CLI.SCAN) {
-           if (state.debug) {
-               System.out.println("Scanning " + cli.infile + ".");
-           }
-
-           success = scan(state) || error(state, "Scanning failed.");
-
-           if (state.debug) {
-               System.out.println("Scanning of " + state.infile + " successful.");
-               System.out.println("#SUCCESS#");
-           }
-        }
+           gcode.close();
+       } catch (Exception e) {
+           e.printStackTrace();
+           System.exit(-1);
+       }
+       
+       if (state.debug) {
+           System.out.println("Compilation of " + state.infile + " successful.");
+           System.out.println("#SUCCESS#");
+       }
     }
 
     private static void printArgInfo(CLI cli) {
@@ -158,31 +118,6 @@ public class Compiler {
             System.out.println("Printing debugging information...");
             System.out.println("Input filename: " + cli.infile);
             System.out.println("Output filename: " + cli.outfile);
-            System.out.print("Target: ");
-
-            switch(cli.target) {
-            case CLI.ASSEMBLY:
-                System.out.println("ASSEMBLY");
-                break;
-            case CLI.DEFAULT:
-                System.out.println("DEFAULT");
-                break;
-            case CLI.INTER:
-                System.out.println("INTER");
-                break;
-            case CLI.LOWIR:
-                System.out.println("LOWIR");
-                break;
-            case CLI.PARSE:
-                System.out.println("PARSE");
-                break;
-            case CLI.SCAN:
-                System.out.println("SCAN");
-                break;
-            default:
-                System.out.println("not recognized");
-                break;
-            }
 
             for (int i = 0; i < cli.opts.length; i++) {
                 if (cli.opts[i]) {
index 90e1f09..445e018 100755 (executable)
@@ -9,7 +9,7 @@ public class Conjunction {
        predicates.add(pred);
     }
     Conjunction(Vector preds){
-       predicates=preds       ;
+       predicates=preds;
     }
     String name() {
        String name="";
index f3fdcec..a506b03 100755 (executable)
@@ -96,6 +96,5 @@ public class Constraint implements Quantifiers {
         set.addAll(getRequiredDescriptorsFromLogicStatement());
         return set;
     }
-   
 }
 
diff --git a/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java b/Repair/RepairCompiler/MCC/IR/ConstraintDependence.java
new file mode 100755 (executable)
index 0000000..49d4cb9
--- /dev/null
@@ -0,0 +1,216 @@
+package MCC.IR;
+import MCC.State;
+import java.util.*;
+
+public class ConstraintDependence {
+    State state;
+    HashSet constnodes;
+    HashSet nodes;
+    Hashtable constonode;
+    Hashtable nodetonode;
+    Termination termination;
+
+    ConstraintDependence(State state, Termination t) {
+       this.state=state;
+       this.termination=t;
+       constnodes=new HashSet();
+       nodes=new HashSet();
+       constonode=new Hashtable();
+       nodetonode=new Hashtable();
+       constructnodes();
+       constructconjunctionnodes();
+       constructconjunctionedges();
+    }
+    
+    public void addNode(GraphNode gn) {
+       GraphNode gn2=new GraphNode(gn.getLabel(),gn.getTextLabel(),gn);
+       nodes.add(gn2);
+       nodetonode.put(gn,gn2);
+    }
+
+    public void associateWithConstraint(GraphNode gn, Constraint c) {
+       GraphNode ggn=(GraphNode)nodetonode.get(gn);
+       GraphNode gc=(GraphNode)constonode.get(c);
+       GraphNode.Edge e=new GraphNode.Edge("associated",ggn);
+       gc.addEdge(e);
+    }
+
+    public void requiresConstraint(GraphNode gn, Constraint c) {
+       GraphNode ggn=(GraphNode)nodetonode.get(gn);
+       GraphNode gc=(GraphNode)constonode.get(c);
+       GraphNode.Edge e=new GraphNode.Edge("requires",gc);
+       ggn.addEdge(e);
+    }
+
+    /** Constructs a node for each Constraint */
+    private void constructnodes() {
+       for(int i=0;i<state.vConstraints.size();i++) {
+           Constraint c=(Constraint)state.vConstraints.get(i);
+           GraphNode gn=new GraphNode(c.toString(),c);
+           constonode.put(c,gn);
+           constnodes.add(gn);
+       }
+    }
+    
+    private void constructconjunctionnodes() {
+       for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+           GraphNode conjnode=(GraphNode)it.next();
+           TermNode tn=(TermNode)conjnode.getOwner();
+           Conjunction conj=tn.getConjunction();
+           addNode(conjnode);
+       }
+       for(int i=0;i<state.vConstraints.size();i++) {
+           Constraint c=(Constraint)state.vConstraints.get(i);
+           Set conjset=(Set)termination.conjunctionmap.get(c);
+           for(Iterator it=conjset.iterator();it.hasNext();) {
+               GraphNode gn=(GraphNode)it.next();
+               associateWithConstraint(gn,c);
+           }
+       }
+    }
+
+    private void constructconjunctionedges() {
+       for(Iterator it=termination.conjunctions.iterator();it.hasNext();) {
+           GraphNode conjnode=(GraphNode)it.next();
+           TermNode tn=(TermNode)conjnode.getOwner();
+           Conjunction conj=tn.getConjunction();
+           for(int i=0;i<conj.size();i++) {
+               DNFPredicate dpred=conj.get(i);
+               Predicate pred=dpred.getPredicate();
+               Expr expr=null;
+               if (pred instanceof InclusionPredicate) {
+                   InclusionPredicate ip=(InclusionPredicate)pred;
+                   expr=ip.expr;
+               } else if (pred instanceof ExprPredicate) {
+                   ExprPredicate ep=(ExprPredicate)pred;
+                   expr=ep.expr;
+               } else throw new Error("Unrecognized Predicate");
+               Set functions=expr.getfunctions();
+               if (functions==null)
+                   continue;
+               for(Iterator fit=functions.iterator();fit.hasNext();) {
+                   Function f=(Function)fit.next();
+                   if (rulesensurefunction(f))
+                       continue; //no constraint needed to ensure
+
+                   Set s=providesfunction(f);
+                   if (s.size()==0) {
+                       System.out.println("Error: No constraint ensures that [forall v in "+f.getSet()+"], size(v."+(f.isInverse()?"~":"")+f.getRelation()+")=1");
+                       System.exit(-1);
+                   }
+                   Constraint c=(Constraint)s.iterator().next(); //Take the first one
+                   requiresConstraint(conjnode,c);
+               }
+           }
+       }
+    }
+
+    private boolean rulesensurefunction(Function f) {
+       boolean foundrule=false;
+       for(int i=0;i<state.vRules.size();i++) {
+           Rule r=(Rule)state.vRules.get(i);
+           if (r.getInclusion().getTargetDescriptors().contains(f.getRelation())) {
+               RelationInclusion ri=(RelationInclusion)r.getInclusion();
+               Expr e=f.isInverse()?ri.getRightExpr():ri.getLeftExpr();
+               SetDescriptor sd=e.getSet();
+               if (!(sd.isSubset(f.getSet())||f.getSet().isSubset(sd)))
+                   continue; /* This rule doesn't effect the function */
+               if (foundrule) /* two different rules are a problem */
+                   return false;
+               if (!((e instanceof VarExpr)&&(r.numQuantifiers()==1)))
+                   return false;
+               VarExpr ve=(VarExpr)e;
+               Quantifier q=r.getQuantifier(0);
+               if (!(q instanceof SetQuantifier))
+                   return false;
+               SetQuantifier sq=(SetQuantifier)q;
+               if (ve.getVar()!=sq.getVar())
+                   return false;
+               if (!sq.getSet().isSubset(f.getSet()))
+                   return false;
+               if (!((r.getGuardExpr() instanceof BooleanLiteralExpr)&&
+                     ((BooleanLiteralExpr)r.getGuardExpr()).getValue()==true))
+                   return false;
+               Expr e2=f.isInverse()?ri.getLeftExpr():ri.getRightExpr();
+               if (e2.isSafe())
+                   foundrule=true;
+               else
+                   return false;
+           }
+       }
+       return foundrule;
+    }
+    private Set providesfunction(Function f) {
+       HashSet set=new HashSet();
+       for(int i=0;i<state.vConstraints.size();i++) {
+           Constraint c=(Constraint)state.vConstraints.get(i);
+           boolean goodconstraint=true;
+           DNFConstraint dnfconst=c.dnfconstraint;
+           for(int j=0;j<dnfconst.size();j++) {
+               Conjunction conj=dnfconst.get(j);
+               boolean conjprovides=false;
+               for(int k=0;k<conj.size();k++) {
+                   DNFPredicate dpred=conj.get(k);
+                   if (!dpred.isNegated()&&
+                       (dpred.getPredicate() instanceof ExprPredicate)&&
+                       ((ExprPredicate)dpred.getPredicate()).getType()==ExprPredicate.SIZE) {
+                       ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
+                       if (ep.isRightInt()&&
+                           ep.rightSize()==1&&
+                           ep.getOp()==Opcode.EQ&&
+                           ep.inverted()==f.isInverse()&&
+                           ep.getDescriptor()==f.getRelation()) {
+                           ImageSetExpr se=(ImageSetExpr) ((SizeofExpr) ((OpExpr)ep.expr).left).getSetExpr();
+                           VarDescriptor vd=se.getVar();
+                           if (c.numQuantifiers()==1) {
+                               for(int l=0;l<c.numQuantifiers();l++) {
+                                   Quantifier q=c.getQuantifier(l);
+                                   if (q instanceof SetQuantifier&&
+                                       ((SetQuantifier)q).getVar()==vd) {
+                                       SetDescriptor sd=((SetQuantifier)q).getSet();
+                                       if (sd.isSubset(f.getSet()))
+                                           conjprovides=true;
+                                   }
+                               }
+                           } else
+                               break;
+                       }
+                   }
+               }
+               if (!conjprovides) {
+                   goodconstraint=false;
+                   break;
+               }
+           }
+           if (goodconstraint)
+               set.add(c);
+       }
+       return set;
+    }
+
+    public static class Function {
+       private RelationDescriptor rd;
+       private SetDescriptor sd;
+       private boolean inverse;
+
+       public Function(RelationDescriptor r, SetDescriptor sd, boolean inverse) {
+           this.inverse=inverse;
+           this.sd=sd;
+           this.rd=r;
+       }
+
+       public SetDescriptor getSet() {
+           return sd;
+       }
+
+       public RelationDescriptor getRelation() {
+           return rd;
+       }
+
+       public boolean isInverse() {
+           return inverse;
+       }
+    }
+
+}
index fbd217d..bc0bc17 100755 (executable)
@@ -12,6 +12,17 @@ public class DotExpr extends Expr {
     static boolean DOTYPECHECKS=false;
     static boolean DONULL=false;
 
+    public boolean isSafe() {
+       if (!left.isSafe())
+           return false;
+       FieldDescriptor tmpfd=fd;
+       if (tmpfd instanceof ArrayDescriptor)
+           return false; // Arrays could be out of bounds
+       if (tmpfd.getPtr()) // Pointers cound be invalid
+           return false;
+       return true;
+    }
+
     public void findmatch(Descriptor d, Set s) {
        if (d==fd)
            s.add(this);
diff --git a/Repair/RepairCompiler/MCC/IR/ExactSize.java b/Repair/RepairCompiler/MCC/IR/ExactSize.java
new file mode 100755 (executable)
index 0000000..7be110b
--- /dev/null
@@ -0,0 +1,73 @@
+package MCC.IR;
+import java.util.*;
+import MCC.State;
+
+
+class ExactSize {
+    State state;
+    private Hashtable sizemap;
+    private Hashtable constraintmap;
+
+    public ExactSize(State state) {
+       this.state=state;
+       this.sizemap=new Hashtable();
+       this.constraintmap=new Hashtable();
+       computesizes();
+    }
+    
+    public int getsize(SetDescriptor sd) {
+       if (sizemap.contains(sd))
+           return ((Integer)sizemap.get(sd)).intValue();
+       else
+           return -1;
+    }
+    public Constraint getConstraint(SetDescriptor sd) {
+       return (Constraint)constraintmap.get(sd);
+    }
+
+    private void computesizes() {
+       for(Iterator it=state.stSets.descriptors();it.hasNext();) {
+           SetDescriptor sd=(SetDescriptor)it.next();
+           for(int i=0;i<state.vConstraints.size();i++) {
+               Constraint c=(Constraint)state.vConstraints.get(i);
+               DNFConstraint dconst=c.dnfconstraint;
+               int oldsize=-1;
+               boolean matches=true;
+               for(int j=0;j<dconst.size();j++) {
+                   Conjunction conj=dconst.get(j);
+                   boolean goodmatch=false;
+                   for(int k=0;k<conj.size();k++) {
+                       DNFPredicate dpred=conj.get(k);
+                       if (!dpred.isNegated()) {
+                           Predicate p=dpred.getPredicate();
+                           if (p instanceof ExprPredicate) {
+                               ExprPredicate ep=(ExprPredicate)p;
+                               if (ep.getType()==ExprPredicate.SIZE&&
+                                   ep.getOp()==Opcode.EQ&&
+                                   ep.getDescriptor()==sd&&
+                                   ep.isRightInt()) {
+                                   if (k==0) {
+                                       oldsize=ep.rightSize();
+                                   } else {
+                                       if (oldsize==ep.rightSize()) {
+                                           goodmatch=true;
+                                           break;
+                                       }
+                                   }
+                               }
+                           }
+                       }
+                   }
+                   if (!goodmatch) {
+                       matches=false;
+                       break; //this constraint won't work
+                   }
+               }
+               if (matches) {
+                   sizemap.put(sd,new Integer(oldsize));
+                   constraintmap.put(sd,c);
+               }
+           }
+       }
+    }
+}
index e98abc5..771b9f8 100755 (executable)
@@ -69,4 +69,16 @@ public abstract class Expr {
 
     public void findmatch(Descriptor d, Set s) {
     }
+
+    public Set getfunctions() {
+       return null;
+    }
+
+    public SetDescriptor getSet() {
+       throw new Error("No Set for this Expr");
+    }
+
+    public boolean isSafe() {
+       return true;
+    }
 }
index 7626732..a282045 100755 (executable)
@@ -10,6 +10,11 @@ public class ExprPredicate extends Predicate {
     public static final int SIZE=1;
     public static final int COMPARISON=2;
 
+    public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+       TypeDescriptor t=expr.typecheck(sa);
+       return t;
+    }
+
     public String name() {
        return expr.name();
     }
@@ -27,6 +32,7 @@ public class ExprPredicate extends Predicate {
     }
 
     public int rightSize() {
+       assert isRightInt();
        return OpExpr.getInt(((OpExpr)expr).right);
     }
 
index 8c4e6d1..4fda86c 100755 (executable)
@@ -7,6 +7,15 @@ public class InclusionPredicate extends Predicate {
     Expr expr;
     SetExpr setexpr;
 
+    public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+       TypeDescriptor t=expr.typecheck(sa);
+       TypeDescriptor ts=setexpr.typecheck(sa);
+       if (t!=ts)
+           return null;
+       
+       return ReservedTypeDescriptor.INT;
+    }
+
     public boolean inverted() {
        return setexpr.inverted();
     }
index ab23ec3..f31c815 100755 (executable)
@@ -29,6 +29,19 @@ public class LogicStatement {
         return set;
     }
     
+    public TypeDescriptor typecheck(SemanticAnalyzer sa) {
+       TypeDescriptor lt=left.typecheck(sa);
+       if (lt!=ReservedTypeDescriptor.INT)
+           return null;
+       TypeDescriptor rt;
+       if (op!=NOT) {
+           rt=right.typecheck(sa);
+           if (rt!=ReservedTypeDescriptor.INT)
+               return null;
+       }
+       return ReservedTypeDescriptor.INT;
+    }
+
     public DNFConstraint constructDNF() {
        if (op==AND) {
            DNFConstraint leftd=left.constructDNF();
index 4714735..09895eb 100755 (executable)
@@ -8,6 +8,26 @@ public class OpExpr extends Expr {
     Expr right;
     Opcode opcode;
 
+    public boolean isSafe() {
+       if (right==null)
+           return left.isSafe();
+       return left.isSafe()&&right.isSafe();
+    }
+
+    public Set getfunctions() {
+       Set leftfunctions=left.getfunctions();
+       Set rightfunctions=right.getfunctions();
+       if (leftfunctions!=null&&rightfunctions!=null) {
+           HashSet functions=new HashSet();
+           functions.addAll(leftfunctions);
+           functions.addAll(rightfunctions);
+           return functions;
+       }
+       if (leftfunctions!=null)
+           return leftfunctions;
+       return rightfunctions;
+    }
+
     public void findmatch(Descriptor d, Set  s) {
        left.findmatch(d,s);
        if (right!=null)
index 1b7336a..355f461 100755 (executable)
@@ -8,6 +8,23 @@ public class RelationExpr extends Expr {
     RelationDescriptor relation;
     boolean inverse;
 
+    public Set getfunctions() {
+       HashSet functions=new HashSet();
+       Set exprfunctions=expr.getfunctions();
+       if (exprfunctions!=null)
+           functions.addAll(exprfunctions);
+       functions.add(new ConstraintDependence.Function(relation,expr.getSet(),inverse));
+       
+       return functions;
+    }
+
+    public SetDescriptor getSet() {
+       if (inverse)
+           return relation.domain;
+       else
+           return relation.range;
+    }
+
     public RelationExpr(Expr expr, RelationDescriptor relation, boolean inverse) {
         this.expr = expr;
         this.relation = relation;
index 9d236e8..8bff959 100755 (executable)
@@ -637,9 +637,9 @@ public class RepairGenerator {
            
             {
                final SymbolTable st = constraint.getSymbolTable();
-               CodeWriter cr = new StandardCodeWriter(outputaux) {
-                        public SymbolTable getSymbolTable() { return st; }
-                    };
+               CodeWriter cr = new StandardCodeWriter(outputaux);
+               cr.pushSymbolTable(constraint.getSymbolTable());
+
                cr.outputline("// checking " + escape(constraint.toString()));
                 cr.startblock();
 
@@ -938,25 +938,8 @@ public class RepairGenerator {
        ExprPredicate ep=(ExprPredicate)dpred.getPredicate();
        OpExpr expr=(OpExpr)ep.expr;
        Opcode opcode=expr.getOpcode();
-       {
-           boolean negated=dpred.isNegated();
-           if (negated)
-               if (opcode==Opcode.GT) {
-                   opcode=Opcode.LE;
-               } else if (opcode==Opcode.GE) {
-                   opcode=Opcode.LT;
-               } else if (opcode==Opcode.LT) {
-                   opcode=Opcode.GE;
-               } else if (opcode==Opcode.LE) {
-                   opcode=Opcode.GT;
-               } else if (opcode==Opcode.EQ) {
-                   opcode=Opcode.NE;
-               } else if (opcode==Opcode.NE) {
-                   opcode=Opcode.EQ;
-               } else {
-                   throw new Error("Unrecognized Opcode");
-               }       
-       }
+       opcode=Opcode.translateOpcode(dpred.isNegated(),opcode);
+
        MultUpdateNode munremove;
 
        MultUpdateNode munadd;
@@ -1004,6 +987,12 @@ public class RepairGenerator {
        } else {
            throw new Error("Unrecognized Opcode");
        }
+
+// In some cases the analysis has determined that generating removes
+// is unnecessary
+       if (generateremove&&munremove==null) 
+           generateremove=false;
+
        Descriptor d=ep.getDescriptor();
        if (generateremove) {
            cr.outputline("for(;"+change.getSafeSymbol()+"<0;"+change.getSafeSymbol()+"++)");
index 0b9598d..61dc275 100755 (executable)
@@ -379,7 +379,7 @@ public class SemanticChecker {
 
         boolean ok = true;
         ParseNodeVector constraints = pn.getChildren();
-        
+
         for (int i = 0; i < constraints.size(); i++) {
             ParseNode constraint = constraints.elementAt(i);
             assert constraint.getLabel().equals("constraint");
@@ -390,6 +390,27 @@ public class SemanticChecker {
 
         /* do any post checks... (type constraints, etc?) */
 
+        Iterator consiterator = state.vConstraints.iterator();
+
+        while (consiterator.hasNext()) {
+            Constraint cons = (Constraint) consiterator.next();
+
+            final SymbolTable consst = cons.getSymbolTable();
+            SemanticAnalyzer sa = new SemanticAnalyzer() {
+                    public IRErrorReporter getErrorReporter() { return er; }
+                    public SymbolTable getSymbolTable() { return consst; }
+                };
+
+            TypeDescriptor constype = cons.getLogicStatement().typecheck(sa);
+
+            if (constype == null) {
+                ok = false;
+            } else if (constype != ReservedTypeDescriptor.INT) {
+                er.report(null, "Type of guard must be 'int' not '" + constype.getSymbol() + "'");
+                ok = false;
+            }
+       }
+
        return ok;
     }
 
@@ -424,7 +445,7 @@ public class SemanticChecker {
                 }
             }
         }
-                                                      
+
         /* get body */
         LogicStatement logicexpr = parse_body(pn.getChild("body"));
 
@@ -442,7 +463,7 @@ public class SemanticChecker {
         assert sts.empty();
 
         /* add to vConstraints */
-        vConstraints.addElement(constraint);           
+        vConstraints.addElement(constraint);
 
         return ok;
     }
@@ -468,6 +489,7 @@ public class SemanticChecker {
             SetDescriptor set = parse_set(pn.getChild("set"));
             assert set != null;
             sq.setSet(set);
+           vd.setSet(set);
 
             vd.setType(set.getType());
 
@@ -498,7 +520,9 @@ public class SemanticChecker {
             
             rq.setRelation(rd);
             vd1.setType(rd.getDomain().getType());
+           vd1.setSet(rd.getDomain());
             vd2.setType(rd.getRange().getType());
+           vd2.setSet(rd.getRange());
             return rq;
         } else if (pn.getChild("for") != null) { /* for j = x to y */
             ForQuantifier fq = new ForQuantifier();
@@ -510,6 +534,7 @@ public class SemanticChecker {
                 return null;
             }
 
+           vd.setSet(lookupSet("int", false));
             vd.setType(ReservedTypeDescriptor.INT);
             fq.setVar(vd);
 
@@ -984,11 +1009,9 @@ public class SemanticChecker {
                         }
                     }
                 }
-                
-            } else {
+           } else {
                 throw new IRException("shouldn't be any other typedescriptor classes");
             }
-
         }
 
         // #TBD#: need to make sure that no cycles exist in any of the declarations or subtypes
@@ -1436,7 +1459,14 @@ public class SemanticChecker {
         /* do semantic check and if valid, add it to symbol table
            and add it to the quantifier as well */
         if (sts.peek().contains(varname)) {
-            return new VarDescriptor(varname);
+           VarDescriptor vdold=(VarDescriptor)sts.peek().get(varname);
+           return vdold;
+           /*     Dan was creating a new VarDescriptor...This seems
+                  like the wrong thing to do.  We'll just lookup the
+                  other one.
+                  --------------------------------------------------
+                  VarDescriptor vd=new VarDescriptor(varname);
+                  vd.setSet(vdold.getSet()); return vd;*/
         } else {
             /* Semantic Error: undefined variable */
             er.report(pn, "Undefined variable '" + varname + "'");
index b37fa11..04203ba 100755 (executable)
@@ -22,7 +22,9 @@ public class Sources {
        TypeDescriptor td=sd.getType();
        Expr e=td.getSizeExpr();
        VarDescriptor size=VarDescriptor.makeNew("size");
+       cr.pushSymbolTable(state.stGlobals);
        e.generate(cr, size);
+       cr.popSymbolTable();
        cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");");
     }
 
@@ -44,7 +46,9 @@ public class Sources {
        TypeDescriptor td=sd.getType();
        Expr e=td.getSizeExpr();
        VarDescriptor size=VarDescriptor.makeNew("size");
+       cr.pushSymbolTable(state.stGlobals);
        e.generate(cr, size);
+       cr.popSymbolTable();
        cr.outputline(td.getGenerateType().getSafeSymbol()+" "+vd.getSafeSymbol()+"=("+td.getGenerateType().getSafeSymbol()+") malloc("+size.getSafeSymbol()+");");
     }
 
index d6a792f..14d1549 100755 (executable)
@@ -26,7 +26,8 @@ public class Termination {
     ComputeMaxSize maxsize;
     State state;
     AbstractInterferes abstractinterferes;
-
+    ConstraintDependence constraintdependence;
+    ExactSize exactsize;
 
     public Termination(State state) {
        this.state=state;
@@ -47,14 +48,14 @@ public class Termination {
        if (!Compiler.REPAIR)
            return;
 
-       
+
        for(int i=0;i<state.vRules.size();i++)
            System.out.println(state.vRules.get(i));
        for(int i=0;i<state.vConstraints.size();i++)
            System.out.println(state.vConstraints.get(i));
 
-
        maxsize=new ComputeMaxSize(state);
+       exactsize=new ExactSize(state);
 
        abstractinterferes=new AbstractInterferes(this);
        generateconjunctionnodes();
@@ -66,15 +67,12 @@ public class Termination {
        generateabstractedges();
        generatescopeedges();
        generateupdateedges();
+       constraintdependence=new ConstraintDependence(state,this);
 
        HashSet superset=new HashSet();
        superset.addAll(conjunctions);
        HashSet closureset=new HashSet();
-       //      closureset.addAll(updatenodes);
-       //superset.addAll(abstractrepair);
-       //superset.addAll(updatenodes);
-       //superset.addAll(scopenodes);
-       //superset.addAll(consequencenodes);
+
        GraphNode.computeclosure(superset,closureset);
        try {
            GraphNode.DOTVisitor.visit(new FileOutputStream("graph.dot"),superset);
@@ -134,6 +132,8 @@ public class Termination {
                    conjunctionmap.put(c,new HashSet());
                ((Set)conjunctionmap.get(c)).add(gn);
                conjtonodemap.put(dnf.get(j),gn);
+
+
            }
            // Construct quantifier "conjunction" nodes
            for(int j=0;j<c.numQuantifiers();j++) {
@@ -153,6 +153,7 @@ public class Termination {
                        conjunctionmap.put(c,new HashSet());
                    ((Set)conjunctionmap.get(c)).add(gn);
                    conjtonodemap.put(dconst.get(0),gn);
+
                } else if (q instanceof RelationQuantifier) {
                    RelationQuantifier rq=(RelationQuantifier)q;
                    VarExpr ve=new VarExpr(rq.y);
@@ -168,6 +169,7 @@ public class Termination {
                        conjunctionmap.put(c,new HashSet());
                    ((Set)conjunctionmap.get(c)).add(gn);
                    conjtonodemap.put(dconst.get(0),gn);
+
                }
            }
        }
@@ -701,10 +703,11 @@ public class Termination {
                        goodupdate=true;
                    } else {
                        /* Create new element to bind to */
-                       Binding binding=new Binding(vd,set,createorsearch(set));
+                       // search if the set 'set' has a size
+                       Binding binding=new Binding(vd,set,exactsize.getsize(set)!=-1);
                        bindings.add(binding);
                        goodupdate=true;
-                       //FIXME
+
                    }
            } else if (q instanceof RelationQuantifier) {
                RelationQuantifier rq=(RelationQuantifier)q;
@@ -754,22 +757,16 @@ public class Termination {
        return goodupdate;
     }
 
-    /** Returns true if we search for an element from sd
-     *  false if we create an element for sd */
-    private boolean createorsearch(SetDescriptor sd) {
-       return false;
-    }
-
     static int addtocount=0;
     void generateaddtosetrelation(GraphNode gn, AbstractRepair ar) {
        for(int i=0;i<state.vRules.size();i++) {
            Rule r=(Rule) state.vRules.get(i);
            /* See if this is a good rule*/
            if ((r.getInclusion() instanceof SetInclusion&&
-               ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
+                ar.getDescriptor()==((SetInclusion)r.getInclusion()).getSet())||
                (r.getInclusion() instanceof RelationInclusion&&
                 ar.getDescriptor()==((RelationInclusion)r.getInclusion()).getRelation())) {
-
+               
                /* First solve for quantifiers */
                Vector bindings=new Vector();
                /* Construct bindings */
@@ -841,7 +838,8 @@ public class Termination {
                        GraphNode.Edge e=new GraphNode.Edge("abstract"+addtocount,gn2);
                        addtocount++;
                        gn.addEdge(e);
-                       updatenodes.add(gn2);}
+                       updatenodes.add(gn2);
+                   }
                }
            }
        }
@@ -872,6 +870,9 @@ public class Termination {
                
            } else if (q instanceof SetQuantifier) {
                SetQuantifier sq=(SetQuantifier)q;
+               if (un.getBinding(sq.var).getType()==Binding.SEARCH)
+                   continue; /* Don't need to ensure addition for search */
+
                ElementOfExpr eoe=new ElementOfExpr(new VarExpr(sq.var),sq.set);
                eoe.td=ReservedTypeDescriptor.INT;
                Updates u=new Updates(eoe,false);
index f7f8722..ef31f2b 100755 (executable)
@@ -7,6 +7,16 @@ public class VarDescriptor extends Descriptor {
 
     TypeDescriptor td = null;
 
+    SetDescriptor sd=null;
+
+    public SetDescriptor getSet() {
+       return sd;
+    }
+
+    public void setSet(SetDescriptor sd) {
+       this.sd=sd;
+    }
+
     public VarDescriptor(String name) {
         super(name);
     }
index 76ab416..e2f8198 100755 (executable)
@@ -17,8 +17,12 @@ public class VarExpr extends Expr {
        return hs;
     }
 
+    public SetDescriptor getSet() {
+       return vd.getSet();
+    }
+
     public VarExpr(String varname) {
-        this.varname = varname; 
+        this.varname = varname;
     }
 
     public VarExpr(VarDescriptor vd) {
@@ -74,13 +78,11 @@ public class VarExpr extends Expr {
     }
 
     public void generate(CodeWriter writer, VarDescriptor dest) {        
-
         // #TBD#: bit of a hack, really should have been type checked properly 
-
-        vd = (VarDescriptor) writer.getSymbolTable().get(varname);        
+        vd = (VarDescriptor) writer.getSymbolTable().get(varname);
         assert vd != null;
         assert vd.getType() != null;
-        this.td = vd.getType();
+       this.td = vd.getType();
 
 
         writer.outputline(vd.getType().getGenerateType().getSafeSymbol() + " " + dest.getSafeSymbol() +