Change to the spec...missed a consistency property. Adding timing option.
authorbdemsky <bdemsky>
Mon, 16 Aug 2004 20:54:16 +0000 (20:54 +0000)
committerbdemsky <bdemsky>
Mon, 16 Aug 2004 20:54:16 +0000 (20:54 +0000)
Repair/RepairCompiler/MCC/CLI.java
Repair/RepairCompiler/MCC/Compiler.java
Repair/RepairCompiler/MCC/IR/RepairGenerator.java
Repair/RepairCompiler/MCC/specs/abiword/abi.constraints
Repair/RepairCompiler/MCC/specs/abiword/abi.model
Repair/RepairCompiler/MCC/specs/abiword/abi.space

index 28ecc29..febfd74 100755 (executable)
@@ -11,7 +11,7 @@ import MCC.IR.DebugItem;
  * files.
  *
  * @author  le01, 6.035 Staff (<tt>6.035-staff@mit.edu</tt>)
- * @version <tt>$Id: CLI.java,v 1.11 2004/08/13 19:22:23 bdemsky Exp $</tt>
+ * @version <tt>$Id: CLI.java,v 1.12 2004/08/16 20:53:53 bdemsky Exp $</tt>
  */
 public class CLI {
     /**
@@ -106,6 +106,7 @@ public class CLI {
            System.out.println("-aggressivesearch");
            System.out.println("-prunequantifiernodes");
            System.out.println("-cplusplus");
+           System.out.println("-time");
            System.exit(-1);
        }
 
@@ -123,6 +124,8 @@ public class CLI {
                i+=3;
            } else if (args[i].equals("-debug")) {
                 Compiler.GENERATEDEBUGHOOKS=true;
+           } else if (args[i].equals("-time")) {
+                Compiler.TIME=true;
            } else if (args[i].equals("-instrument")) {
                 Compiler.GENERATEINSTRUMENT=true;
            } else if (args[i].equals("-aggressivesearch")) {
index 70e9749..04ad0ba 100755 (executable)
@@ -25,6 +25,7 @@ public class Compiler {
     public static boolean GENERATEDEBUGPRINT=false;
     public static boolean GENERATEINSTRUMENT=false;
     public static boolean ALLOCATECPLUSPLUS=false;
+    public static boolean TIME=false;
     
     public static Vector debuggraphs=new Vector();
 
index a6586bc..5d64040 100755 (executable)
@@ -497,6 +497,11 @@ public class RepairGenerator {
        crhead.outputline("void doanalysis();");
        craux.outputline("void "+name +"_state::doanalysis()");
        craux.startblock();
+       if (Compiler.TIME) {
+           craux.outputline("struct timeval _begin_time,_end_time;");
+           craux.outputline("gettimeofday(&_begin_time,NULL);");
+       }
+
        if (Compiler.GENERATEINSTRUMENT) {
            craux.outputline("updatecount=0;");
            craux.outputline("rebuildcount=0;");
@@ -521,6 +526,11 @@ public class RepairGenerator {
     private void generate_teardown() {
        CodeWriter cr = new StandardCodeWriter(outputaux);        
        cr.endblock();
+       if (Compiler.TIME) {
+           cr.outputline("gettimeofday(&_end_time,NULL);");
+           cr.outputline("printf(\"time=%ld uS\\n\",(_end_time.tv_sec-_begin_time.tv_sec)*1000000+_end_time.tv_usec-_begin_time.tv_usec)");
+       }
+
        if (Compiler.GENERATEINSTRUMENT) {
            cr.outputline("printf(\"updatecount=%d\\n\",updatecount);");
            cr.outputline("printf(\"rebuildcount=%d\\n\",rebuildcount);");
index 5ea646d..ea14482 100755 (executable)
@@ -5,3 +5,4 @@
 [forall f in Frags], (sizeof(f.~Next)<=1);
 [forall f in firstblock], sizeof(f.~Next)=0;
 [forall l in Last, forall f in Fragments], f.PLast=l and sizeof(f.PLast)=1;
+[forall f in Frags], f.Length>=1;
\ No newline at end of file
index 6e6a54e..1736391 100755 (executable)
@@ -6,5 +6,6 @@
 [forall f in Frags], !(f.m_next=null) => <f,f.m_next> in Next;
 [forall f in Frags], !(f.m_prev=null) => <f,f.m_prev> in Prev;
 [forall f in Frags], (f.m_next=null) => f in Last;
+[forall f in Frags], true => <f,f.m_length> in Length;
 [forall f in Fragments], !(f.m_pLast=null) => <f,f.m_pLast> in PLast;
-[forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;
\ No newline at end of file
+[forall f in Fragments], !(f.m_pLast=null) => f.m_pLast in LFrag;
index 1a71eb1..1914511 100755 (executable)
@@ -6,4 +6,5 @@ set secondblock(pf_Frag_Strux_Block);
 Next: Frags -> Frags;
 Prev: Frags -> Frags;
 set LFrag(pf_Frag);
-PLast: Fragments -> LFrag;
\ No newline at end of file
+PLast: Fragments -> LFrag;
+Length: Frags -> int;
\ No newline at end of file