Merge pull request #307 from phiash/master

Stability abstract domain implementation

lisa/lisa-analyses/imp-testcases/numeric/numeric.imp

@@ -1,13 +1,25 @@
 class tutorial {
 
+	constants(d) {
+		def c = 0;
+		def b = 1;
+		if (d > 10)
+	        c = -2;
+	    else
+		    c = 2;
+        b = b + c;
+        return b;
+    }
+
+/*
 	constants() {
 		def c = 1;
 		def b = 0;
    		while (b < 10) 
         	b = b + c;
    		return b;
     }
-    
+
 	sign_parity_example() {
 		def i = 2;
 		def max = 10;
@@ -109,4 +121,6 @@ class tutorial {
 		}
 		return x;
 	}
+	*/
+
 }

lisa/lisa-analyses/imp-testcases/stability/rectangleScale.imp

@@ -0,0 +1,36 @@
+class Rectangle{
+    width;
+    height;
+    botLeftX;
+    botLeftY;
+
+    ~Rectangle(){
+        this.width = 8;
+        this.height = 8;
+        this.botLeftX = 1;
+        this.botLeftY = 1;
+    }
+}
+
+class scaleBis{
+
+    scale(){
+        def r = new Rectangle();
+        def scaleX = 2;
+        def scaleY = -1;
+
+        def botRightX = r.botLeftX + r.width;
+        def topLeftY = r.botLeftY + r.height;
+
+        r.botLeftX = r.botLeftX * scaleX;
+        r.botLeftY = r.botLeftY * scaleY;
+
+        botRightX = botRightX * scaleX;
+        topLeftY = topLeftY * scaleY;
+
+        r.width = botRightX - r.botLeftX;
+        r.height = topLeftY - r.botLeftY;
+
+    }
+
+}

lisa/lisa-analyses/imp-testcases/stability/saneScale.imp

@@ -0,0 +1,26 @@
+class scaleBis{
+
+    scale(){
+        def width = 8;
+        def height = 8;
+        def botLeftX = 1;
+        def botLeftY = 9;
+
+        def scaleX = 2;
+        def scaleY = 1;
+
+        def botRightX = botLeftX + width;
+        def topLeftY = botLeftY + height;
+
+        botLeftX = botLeftX * scaleX;
+        botLeftY = botLeftY * scaleY;
+
+        botRightX = botRightX * scaleX;
+        topLeftY = topLeftY * scaleY;
+
+        width = botRightX - botLeftX;
+        height = topLeftY - botLeftY;
+
+    }
+
+}

lisa/lisa-analyses/imp-testcases/stability/scale.imp

@@ -0,0 +1,69 @@
+
+// assume only positive values (negative values are for reflection)
+class scale{
+
+     main(b) {
+        def x = 10;
+        def y = 30;
+        def width = 3;
+        def height = 7;
+
+        while(b) {
+            x = x + 1;
+            y = y + 1;
+            width = width + 1;
+            height = height + 1;
+        }
+        while(b) {
+            x = x - 1;
+            y = y - 1;
+            width = width - 1;
+            height = height - 1;
+        }
+
+        this.scale(x, y, width, height);
+    }
+
+    //x, upperRightPointX and width should be covariant
+    //y, lowerLeftPointY and height should be covariant
+    //the two groups should be contravariant
+    scale(x, y, width, height){
+        if (x >= 0)
+         if (y >= 0)
+          if(width >= 0)
+           if (height >= 0){
+        //if (x >= 0 && y >= 0 && width > 0 && height > 0){
+            def scale1 = 2;
+            def scale2 = 3;
+
+            def upperRightPointX = x + width;
+
+            def lowerLeftPointY = y - height;
+
+            x = x * scale1;
+            y = y * scale2;
+            upperRightPointX = upperRightPointX * scale1;
+            lowerLeftPointY = lowerLeftPointY * scale2;
+
+            width = x - upperRightPointX;
+            height = y - lowerLeftPointY;
+        }
+    }
+/*
+    // all variables should be covariant
+    uniformScale(x, y, width, height, scale){
+            def upperRightPointX = x + width;
+
+            def lowerLeftPointY = y - height;
+
+            x = x * scale;
+            y = y * scale;
+            upperRightPointX = upperRightPointX * scale;
+            lowerLeftPointY = lowerLeftPointY * scale;
+
+            width = x - upperRightPointX;
+            height = y - lowerLeftPointY;
+    }
+    */
+
+}