changed API for data annotations

Janala.iml

@@ -1,5 +1,10 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <module type="JAVA_MODULE" version="4">
+  <component name="FacetManager">
+    <facet type="Python" name="Python">
+      <configuration sdkName="" />
+    </facet>
+  </component>
   <component name="NewModuleRootManager" inherit-compiler-output="true">
     <exclude-output />
     <content url="file://$MODULE_DIR$">
@@ -19,5 +24,4 @@
       </library>
     </orderEntry>
   </component>
-</module>
-
+</module>

src/catg/CATG.java

@@ -43,46 +43,74 @@
  * Time: 12:09 PM
  */
 public class CATG {
-    public static int abstractInt(int x) {
-        int y = readInt(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static int abstractInt(String test, int x) {
+        if (Config.instance.testChecker.check(test)) {
+            int y = readInt(x);
+            Main.AbstractEqualsConcrete(Main.compare(y, x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
-    public static boolean abstractBool(boolean x) {
-        boolean y = readBool(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static boolean abstractBool(String test, boolean x) {
+        if (Config.instance.testChecker.check(test)) {
+            boolean y = readBool(x);
+            Main.AbstractEqualsConcrete(Main.compare(y,x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
-    public static long abstractLong(long x) {
-        long y = readLong(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static long abstractLong(String test, long x) {
+        if (Config.instance.testChecker.check(test)) {
+            long y = readLong(x);
+            Main.AbstractEqualsConcrete(Main.compare(y,x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
-    public static char abstractChar(char x) {
-        char y = readChar(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static char abstractChar(String test, char x) {
+        if (Config.instance.testChecker.check(test)) {
+            char y = readChar(x);
+            Main.AbstractEqualsConcrete(Main.compare(y,x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
-    public static byte abstractByte(byte x) {
-        byte y = readByte(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static byte abstractByte(String test, byte x) {
+        if (Config.instance.testChecker.check(test)) {
+            byte y = readByte(x);
+            Main.AbstractEqualsConcrete(Main.compare(y,x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
-    public static short abstractShort(short x) {
-        short y = readShort(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static short abstractShort(String test, short x) {
+        if (Config.instance.testChecker.check(test)) {
+            short y = readShort(x);
+            Main.AbstractEqualsConcrete(Main.compare(y,x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
-    public static String abstractString(String x) {
-        String y = readString(x);
-        Main.AbstractEqualsConcrete(Main.compare(y,x));
-        return y;
+    public static String abstractString(String test, String x) {
+        if (Config.instance.testChecker.check(test)) {
+            String y = readString(x);
+            Main.AbstractEqualsConcrete(Main.compare(y,x));
+            return y;
+        } else {
+            return x;
+        }
     }
 
     public static int[] readIntArray(int length, int x) {
@@ -161,12 +189,16 @@ public static boolean assertIfPossible(int pathId, boolean predicate) {
         return predicate;
     }
 
-    public static void BeginScope() {
-        Main.BeginScope();
+    public static void BeginScope(String test) {
+        if (Config.instance.testChecker.check(test)) {
+            Main.BeginScope();
+        }
     }
 
-    public static void EndScope() {
-        Main.EndScope();
+    public static void EndScope(String test) {
+        if (Config.instance.testChecker.check(test)) {
+            Main.EndScope();
+        }
     }
 
     public static void event(String test, String eventName) {

src/janala/instrument/Coverage.java

@@ -181,6 +181,7 @@ public void printCoverage() {
         //System.out.println("Total branches ="+covered.size());
         System.out.println("Branch coverage with respect to covered classes = "+(100.0*nCovered/nBranches)+"%");
         System.out.println("Branch coverage with respect to covered methods = "+(100.0*nCovered/mtotals)+"%");
+        System.out.println("Total branches in covered methods = "+mtotals);
         //System.out.println("Methods covered = "+nM);
         //System.out.println("Total methods = "+counters.size());
     }

src/tests/AbstractionTest1.java

@@ -59,15 +59,15 @@ public static void main(String[] args){
         System.out.println(x2);
         System.out.println(y2);
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         boolean b1 = testme(x1, y1);
-        CATG.EndScope();
-        b1 = CATG.abstractBool(b1);
+        CATG.EndScope("test");
+        b1 = CATG.abstractBool("test", b1);
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         boolean b2 = testme(x2, y2);
-        CATG.EndScope();
-        b2 = CATG.abstractBool(b2);
+        CATG.EndScope("test");
+        b2 = CATG.abstractBool("test", b2);
 
         System.out.println(b1);
         System.out.println(b2);

src/tests/AbstractionTest2.java

@@ -65,7 +65,7 @@
 
 public class AbstractionTest2 {
     public static boolean foo(){
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         boolean ret;
         int x = CATG.readInt(0);
         int y = CATG.readInt(0);
@@ -78,8 +78,8 @@ public static boolean foo(){
         } else {
             ret = false;
         }
-        CATG.EndScope();
-        ret = CATG.abstractBool(ret);
+        CATG.EndScope("test");
+        ret = CATG.abstractBool("test", ret);
         System.out.print("ret = ");
         System.out.println(ret);
         return ret;
@@ -88,13 +88,13 @@ public static boolean foo(){
     public static void main(String[] args){
         int sum = 0;
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         if (foo()) sum++;
         if (foo()) sum++;
         if (foo()) sum++;
         if (foo()) sum++;
-        CATG.EndScope();
-        sum = CATG.abstractInt(sum);
+        CATG.EndScope("test");
+        sum = CATG.abstractInt("test", sum);
 
         System.out.print("sum = ");
         System.out.println(sum);

src/tests/Annot1.java

@@ -43,15 +43,15 @@ public static int count(int[] array, int element) {
     public static void main(String[] args) {
         int[] input = CATG.readIntArray(10,0);
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         int count1 = count(input, 3);
-        CATG.EndScope();
-        count1 = CATG.abstractInt(count1);
+        CATG.EndScope("test");
+        count1 = CATG.abstractInt("test", count1);
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         int count2 = count(input, 7);
-        CATG.EndScope();
-        count2 = CATG.abstractInt(count2);
+        CATG.EndScope("test");
+        count2 = CATG.abstractInt("test", count2);
 
         if (count1+count2 == 0) {
             System.out.println("do something");

src/tests/AnnotationExample.java

@@ -0,0 +1,65 @@
+/*
+ * Copyright (c) 2012, NTT Multimedia Communications Laboratories, Inc. and Koushik Sen
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * 1. Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * 2. Redistributions in binary form must reproduce the above copyright
+ * notice, this list of conditions and the following disclaimer in the
+ * documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+package tests;
+
+import catg.CATG;
+
+/**
+ * Author: Koushik Sen (ksen@cs.berkeley.edu)
+ */
+public class AnnotationExample {
+    public static int count(int[] array,int element){
+        int ret = 0;
+        for (int i=0; i<array.length; i++)
+            if (array[i]==element) {
+                CATG.event("test1", "a");
+                ret++;
+            }
+        return ret;
+    }
+    public static void main(String[] args) {
+        CATG.pathRegex("test1", "a?ba?");
+        int[] input = CATG.readIntArray(6, 0);
+        int count1 = count(input, 3);
+        System.out.print("count1 = ");
+        System.out.println(count1);
+        CATG.equivalent("test2", "loc1", count1>0);
+        CATG.event("test1", "b");
+        int count2 = count(input, 7);
+        System.out.print("count2 = ");
+        System.out.println(count2);
+//        CATG.equivalent("test2", "loc2", count2>0);
+        if (count1 == 0 && count2 == 0) {
+            System.out.println("do something ");
+        } else {
+            System.out.println("do something else");
+        }
+    }
+}

src/tests/DataAnnotation6.java

@@ -13,15 +13,15 @@ public static void main(String[] args) {
 		System.out.println("z = " + z);
 
 		boolean flag, flagRuntime;
-		CATG.BeginScope();
+		CATG.BeginScope("test");
 		{
 			flag = someComplexLogic(x, y, z);
 
 			flagRuntime = flag;
 			System.out.println("flagRuntime = " + flagRuntime);
 		}
-		CATG.EndScope();
-		flag = CATG.abstractBool(flag);
+		CATG.EndScope("test");
+		flag = CATG.abstractBool("test", flag);
 
         System.out.println("flag = " + flag);
 		if(flag) {

src/tests/DataAnnotation7.java

@@ -8,14 +8,14 @@ public static void main(String[] args) {
        System.out.println("x = " + x);
 
 		boolean a, b;
-		CATG.BeginScope();
+		CATG.BeginScope("test");
         System.out.println("1");
         a = !x;
 		b = a;
         System.out.println("2");
 
-		CATG.EndScope();
-		a = CATG.abstractBool(a);
+		CATG.EndScope("test");
+		a = CATG.abstractBool("test", a);
 
        System.out.println("a = " + a);
        System.out.println("b = " + b);

src/tests/ManyColumnsRecords2.java

@@ -23,7 +23,7 @@ public class ManyColumnsRecords2 {
     public  static void testme(Table customers, int c1){
         int result;
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
 
         l_c1 = c1;
 
@@ -41,7 +41,7 @@ public Operations[] select() {
                 new Where() {
                     @Override
                     public boolean where(Row[] rows) {
-                        CATG.BeginScope();
+                        CATG.BeginScope("test");
                         boolean ret = true;
 
                         for(int i = 1;i < COLUMN_COUNT; i++){
@@ -51,8 +51,8 @@ public boolean where(Row[] rows) {
                                 break;
                             }
                         }
-                        CATG.EndScope();
-                        ret = CATG.abstractBool(ret);
+                        CATG.EndScope("test");
+                        ret = CATG.abstractBool("test", ret);
                         return ret;
                     }
 
@@ -64,8 +64,8 @@ public boolean where(Row[] rows) {
 
         result = t.size();
 
-        CATG.EndScope();
-        result = CATG.abstractInt(result);
+        CATG.EndScope("test");
+        result = CATG.abstractInt("test", result);
 
         System.out.println(result + " record(s) are selected.");
 

src/tests/ScopeTest1.java

@@ -59,9 +59,9 @@ public static void main(String[] args){
             System.out.println("20");
         }
 
-        CATG.BeginScope();
+        CATG.BeginScope("test");
         testme();
-        CATG.EndScope();
+        CATG.EndScope("test");
 
         int y2 = CATG.readInt(0);
         if (y2 == 30) {