Refactoring (v1.1)

README.md

@@ -1,8 +1,10 @@
-# Mungo plugin for Checker Framework
+# Java Typestate Checker plugin for Checker Framework
+
+*Work in progress...*
 
 ## How it works
 
-This version of Mungo is implemented as a plugin for the Checker Framework. Adding a `@mungo.lib.Typestate("ProtocolFile")` annotation to the top of a class enforces that instances of that class follow the protocol defined by the protocol file. Every time a method call on a object is encountered, we make sure that object is in a state that allows that invocation. The type of the object then changes to conform to the new state reached after that method call. We also make sure protocols are completed and that objects are used in a linear way.
+Adding a `@mungo.lib.Typestate("ProtocolFile")` annotation to the top of a class enforces that instances of that class follow the protocol defined by the protocol file. Every time a method call on a object is encountered, we make sure that object is in a state that allows that invocation. The type of the object then changes to conform to the new state reached after that method call. We also make sure protocols are completed.
 
 ### Type system
 
@@ -30,18 +32,14 @@ The type of files that are in the `Open` state and the type of files that are in
 
 ![Type system example](./type_system_example.svg)
 
-#### Notes
-
-1. `null` should NOT have the bottom type, otherwise its type would be the subtype of all types, allowing `null` assignments going unchecked. Which is what Java already (wrongly) does.
-1. `Ended` and `Null` could be joined in an `Unusable` type. The reason to split both is to provide more information to error messages as to why an operation is not allowed.
-
 ### Checking
 
 - The type checker tracks all the possible states that an object might be in.
 - When initializing, an object is only in its initial state.
 - If a variable declaration is encountered, for example in a method argument, it is assumed that the object might be in any of its states. That can be refined with the use of `@MungoState({"Open"})`.
 - When a method invocation is encountered, considering all possible states, the type checker creates a set with all the possible destination states via that method invocation. If that method invocation happened on the condition of a `if/while` statement or in the expression of a `switch` statement, the possible states are properly refined: if the transition leads to a decision state, only the destination state associated with the relevant label is added to the set of possible states.
 
+<!--
 ### Architecture
 
 Plugins for the Checker Framework usually extend the `BaseTypeChecker` and then override some aspects of it if necessary. To understand how plugins work it is important to understand how information is stored:
@@ -64,6 +62,7 @@ Our plugin is composed by:
 Since annotations are only able to store some types of values, not arbitrary objects, we store a `long` id value in each annotation that is then mapped to an object which stores the concrete type information.
 
 More details: [Manual - How to create a Checker plugin](https://checkerframework.org/manual/#creating-a-checker)
+-->
 
 ## Run version 1
 

build.gradle

@@ -1,6 +1,6 @@
 plugins {
     id "java"
-    id "org.jetbrains.kotlin.jvm" version "1.3.70"
+    id "org.jetbrains.kotlin.jvm" version "1.4.0"
     id "antlr"
     id "maven-publish"
     id "idea"
@@ -22,13 +22,12 @@ configurations {
 }
 
 sourceCompatibility = 1.8
-def checkerframework_local = false
 
 ext {
     versions = [
-        kotlin: "1.3.72",
+        kotlin: "1.4.0",
         antlr4: "4.8",
-        checkerFramework: "3.3.0",
+        checkerFramework: "3.6.1",
         errorproneJavacVersion: "9+181-r4173-1",
         junit: "4.13",
     ]
@@ -51,6 +50,9 @@ sourceSets {
         kotlin {
             srcDirs = ["src/main/java", "src/main/kotlin"]
         }
+        resources {
+            srcDirs = ["src/main/resources"]
+        }
     }
 }
 
@@ -64,14 +66,7 @@ dependencies {
     antlr "org.antlr:antlr4:${versions.antlr4}"
     compile "org.antlr:antlr4-runtime:${versions.antlr4}"
 
-    if (checkerframework_local) {
-        implementation files("checker-framework-${versions.checkerFramework}/checker/dist/checker-qual.jar")
-        implementation files("checker-framework-${versions.checkerFramework}/checker/dist/checker.jar")
-        implementation files("checker-framework-${versions.checkerFramework}/checker/dist/jdk8.jar")
-    }
-    else {
-        implementation "org.checkerframework:checker:${versions.checkerFramework}"
-    }
+    implementation "org.checkerframework:checker:${versions.checkerFramework}"
 
     compileOnly "com.google.errorprone:javac:${versions.errorproneJavacVersion}"
 

examples/comparison/_latex/auction.tex

@@ -121,11 +121,22 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-Auction.java:13: error: [Cannot override because object has not ended its protocol] (Cannot override because object has not ended its protocol)
+Auction.java:13: error: [Cannot override because object has not ended its protocol. Type: ClientProtocol{Running} | Ended | Moved] (Cannot override because object has not ended its protocol. Type: ClientProtocol{Running} | Ended | Moved)
       clients[i] = new Client(i);
              ^
+Auction.java:18: error: [Cannot call getBid on ended protocol, on moved value] (Cannot call getBid on ended protocol, on moved value)
+           (hBidder != clientId && val > clients[hBidder].getBid())) ?
+                                                                ^
+Auction.java:23: error: [Cannot call bid on ended protocol, on moved value] (Cannot call bid on ended protocol, on moved value)
+    clients[clientId].bid(val);
+                         ^
 Auction.java:29: error: [Object did not complete its protocol. Type: ClientProtocol{Running}] (Object did not complete its protocol. Type: ClientProtocol{Running})
     for (Client client : clients) {
                 ^
-2 errors\end{code}
+Auction.java:29: error: [enhancedfor.type.incompatible] incompatible types in enhanced for loop.
+    for (Client client : clients) {
+                         ^
+  found   : NoProtocol Client
+  required: ClientProtocol{Running} Client
+5 errors\end{code}
 

examples/comparison/_latex/class-analysis-2.tex

@@ -62,11 +62,14 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-NotOkFileWrapper4.java:8: error: [Cannot override because object has not ended its protocol] (Cannot override because object has not ended its protocol)
+NotOkFileWrapper4.java:5: error: [Object did not complete its protocol. Type: FileProtocol{Read} | Null] (Object did not complete its protocol. Type: FileProtocol{Read} | Null)
+  private @MungoNullable File file = null;
+                              ^
+NotOkFileWrapper4.java:8: error: [Cannot override because object has not ended its protocol. Type: FileProtocol{Read} | Null] (Cannot override because object has not ended its protocol. Type: FileProtocol{Read} | Null)
     this.file = file;
         ^
-NotOkFileWrapper4.java:12: error: [Cannot call read on null, on ended protocol, on moved value] (Cannot call read on null, on ended protocol, on moved value)
+NotOkFileWrapper4.java:12: error: [Cannot call read on null] (Cannot call read on null)
     return file.read();
                     ^
-2 errors\end{code}
+3 errors\end{code}
 

examples/comparison/_latex/class-analysis.tex

@@ -150,14 +150,14 @@
 NotOkFileWrapper2.java:7: error: [Object did not complete its protocol. Type: FileProtocol{Read}] (Object did not complete its protocol. Type: FileProtocol{Read})
   private @MungoNullable File file = null;
                               ^
+NotOkFileWrapper3.java:7: error: [Object did not complete its protocol. Type: FileProtocol{Read}] (Object did not complete its protocol. Type: FileProtocol{Read})
+  private @MungoNullable File file = null;
+                              ^
 NotOkFileWrapper3.java:14: error: [Cannot call close on ended protocol] (Cannot call close on ended protocol)
     file.close();
               ^
 NotOkFileWrapper3.java:19: error: [Cannot call read on ended protocol] (Cannot call read on ended protocol)
     file.read();
              ^
-NotOkFileWrapper3.java:7: error: [Object did not complete its protocol. Type: FileProtocol{Read}] (Object did not complete its protocol. Type: FileProtocol{Read})
-  private @MungoNullable File file = null;
-                              ^
 7 errors\end{code}
 

examples/comparison/_latex/iterator-attempt1.tex

@@ -16,6 +16,10 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-None
-\end{code}
+Main.java:6: error: [argument.type.incompatible] incompatible types in argument.
+    System.out.println(it.next());
+                              ^
+  found   : NoProtocol | Null /*INFERENCE FAILED for:*/ ? extends String
+  required: NoProtocol String
+1 error\end{code}
 

examples/comparison/_latex/linearity-checking-corner-cases.tex

@@ -62,6 +62,24 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-None
-\end{code}
+NotOk.java:6: error: [Passing an object with protocol to a method that cannot be analyzed] (Passing an object with protocol to a method that cannot be analyzed)
+    list.add(new File());
+             ^
+NotOk.java:7: error: [assignment.type.incompatible] incompatible types in assignment.
+    File f1 = list.get(0);
+                      ^
+  found   : FileProtocol{Read} | Ended | Moved File
+  required: FileProtocol{Read} File
+NotOk.java:8: error: [assignment.type.incompatible] incompatible types in assignment.
+    File f2 = list.get(0);
+                      ^
+  found   : FileProtocol{Read} | Ended | Moved File
+  required: FileProtocol{Read} File
+NotOk.java:9: error: [Cannot call read on ended protocol, on moved value] (Cannot call read on ended protocol, on moved value)
+    f1.read();
+           ^
+NotOk.java:11: error: [Cannot call read on ended protocol, on moved value] (Cannot call read on ended protocol, on moved value)
+    f2.read();
+           ^
+5 errors\end{code}
 

examples/comparison/_latex/nullness-checking.tex

@@ -45,11 +45,12 @@
 
 \lstset{language=Java,caption=\textit{NotOk.java}}
 \begin{code}
-import org.checkerframework.checker.mungo.lib.MungoState;
+import org.checkerframework.checker.mungo.lib.MungoNullable;
+import org.checkerframework.checker.mungo.lib.MungoRequires;
 
 public class NotOk {
   public static void main1(String args[]) {
-    File f = new File();
+    @MungoNullable File f = new File();
 
     switch (f.open()) {
       case OK:
@@ -66,7 +67,7 @@
     use(null);
   }
 
-  public static void use(@MungoState("Init") File f) {
+  public static void use(@MungoRequires("Init") File f) {
     switch (f.open()) {
       case OK:
         System.out.println(f.read());
@@ -81,7 +82,7 @@
 \lstset{language=Java,caption=\textit{Ok.java}}
 \begin{code}
 import org.checkerframework.checker.mungo.lib.MungoNullable;
-import org.checkerframework.checker.mungo.lib.MungoState;
+import org.checkerframework.checker.mungo.lib.MungoRequires;
 
 public class Ok {
   public static void main(String args[]) {
@@ -91,8 +92,8 @@
       use(f);
     }
   }
-  
-  public static void use(@MungoState("Init") File f) {
+
+  public static void use(@MungoRequires("Init") File f) {
     switch (f.open()) {
       case OK:
         System.out.println(f.read());
@@ -107,24 +108,24 @@
 \lstset{language=,caption=Original Mungo output}
 \begin{code}
 
-NotOk.java: 10-13: Semantic Error
+NotOk.java: 11-13: Semantic Error
 		Object reference is used uninitialised.
 
 NotOk.java: 0-0: Semantic Error
-		Object created at NotOk.java: 5. Typestate mismatch. Found: end. Expected: void close().
+		Object created at NotOk.java: 6. Typestate mismatch. Found: end. Expected: void close().
 
 Ok.java: 6-25: Semantic Error
 		Object reference is used uninitialised.\end{code}
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-NotOk.java:10: error: [Cannot override because object has not ended its protocol] (Cannot override because object has not ended its protocol)
+NotOk.java:11: error: [Cannot override because object has not ended its protocol. Type: FileProtocol{Close}] (Cannot override because object has not ended its protocol. Type: FileProtocol{Close})
         f = null;
         ^
-NotOk.java:11: error: [Cannot call close on null] (Cannot call close on null)
+NotOk.java:12: error: [Cannot call close on null] (Cannot call close on null)
         f.close();
                ^
-NotOk.java:19: error: [argument.type.incompatible] incompatible types in argument.
+NotOk.java:20: error: [argument.type.incompatible] incompatible types in argument.
     use(null);
         ^
   found   : Null null

examples/comparison/_latex/original-mungo-crash-2.tex

@@ -47,6 +47,8 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-None
-\end{code}
+FileWrapper.java:2: error: [Object did not complete its protocol. Type: FileProtocol{Read} | Ended | Moved] (Object did not complete its protocol. Type: FileProtocol{Read} | Ended | Moved)
+  public File file = new File();
+              ^
+1 error\end{code}
 

examples/comparison/_latex/original-mungo-crash-3-adapted.tex

@@ -41,6 +41,8 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-None
-\end{code}
+Main.java:6: error: [Passing an object with protocol to a method that cannot be analyzed] (Passing an object with protocol to a method that cannot be analyzed)
+    list.add(new File());
+             ^
+1 error\end{code}
 

examples/comparison/_latex/original-mungo-crash-3.tex

@@ -57,8 +57,16 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-Main.java:7: error: [Object did not complete its protocol. Type: FileProtocol{Read}] (Object did not complete its protocol. Type: FileProtocol{Read})
+Main.java:7: error: [Object did not complete its protocol. Type: FileProtocol{Read} | Ended | Moved] (Object did not complete its protocol. Type: FileProtocol{Read} | Ended | Moved)
     File f1 = list.get(0);
          ^
-1 error\end{code}
+Main.java:6: error: [Passing an object with protocol to a method that cannot be analyzed] (Passing an object with protocol to a method that cannot be analyzed)
+    list.add(new File());
+             ^
+Main.java:7: error: [assignment.type.incompatible] incompatible types in assignment.
+    File f1 = list.get(0);
+                      ^
+  found   : FileProtocol{Read} | Ended | Moved File
+  required: FileProtocol{Read} File
+3 errors\end{code}
 

examples/comparison/_latex/protocol-completion-corner-cases.tex

@@ -63,6 +63,11 @@
 
 \lstset{language=,caption=New Mungo output}
 \begin{code}
-None
-\end{code}
+NotOk.java:6: error: [Passing an object with protocol to a method that cannot be analyzed] (Passing an object with protocol to a method that cannot be analyzed)
+    list.add(new File());
+             ^
+NotOk.java:10: error: [Object did not complete its protocol. Type: FileProtocol{Read} | Ended | Moved] (Object did not complete its protocol. Type: FileProtocol{Read} | Ended | Moved)
+    public File file = new File();
+                ^
+2 errors\end{code}
 

examples/comparison/_latex/state-refinement.tex

@@ -44,7 +44,7 @@
 
 \lstset{language=Java,caption=\textit{NotOk.java}}
 \begin{code}
-import org.checkerframework.checker.mungo.lib.MungoState;
+import org.checkerframework.checker.mungo.lib.MungoRequires;
 
 public class NotOk {
 
@@ -60,7 +60,7 @@
     }
   }
 
-  public static void use(@MungoState("Close") File f) {
+  public static void use(@MungoRequires("Close") File f) {
     f.read();
     f.close();
   }
@@ -69,7 +69,7 @@
 
 \lstset{language=Java,caption=\textit{Ok.java}}
 \begin{code}
-import org.checkerframework.checker.mungo.lib.MungoState;
+import org.checkerframework.checker.mungo.lib.MungoRequires;
 
 public class Ok {
 
@@ -85,7 +85,7 @@
     }
   }
 
-  public static void use(@MungoState("Read") File f) {
+  public static void use(@MungoRequires("Read") File f) {
     f.read();
     f.close();
   }

examples/comparison/auction/README.md

@@ -14,10 +14,21 @@ Auction.java: 29-17: Semantic Error
 ## Mungo Checker's output
 
 ```
-Auction.java:13: error: [Cannot override because object has not ended its protocol] (Cannot override because object has not ended its protocol)
+Auction.java:13: error: [Cannot override because object has not ended its protocol. Type: ClientProtocol{Running} | Ended | Moved] (Cannot override because object has not ended its protocol. Type: ClientProtocol{Running} | Ended | Moved)
       clients[i] = new Client(i);
              ^
+Auction.java:18: error: [Cannot call getBid on ended protocol, on moved value] (Cannot call getBid on ended protocol, on moved value)
+           (hBidder != clientId && val > clients[hBidder].getBid())) ?
+                                                                ^
+Auction.java:23: error: [Cannot call bid on ended protocol, on moved value] (Cannot call bid on ended protocol, on moved value)
+    clients[clientId].bid(val);
+                         ^
 Auction.java:29: error: [Object did not complete its protocol. Type: ClientProtocol{Running}] (Object did not complete its protocol. Type: ClientProtocol{Running})
     for (Client client : clients) {
                 ^
-2 errors```
+Auction.java:29: error: [enhancedfor.type.incompatible] incompatible types in enhanced for loop.
+    for (Client client : clients) {
+                         ^
+  found   : NoProtocol Client
+  required: ClientProtocol{Running} Client
+5 errors```

examples/comparison/class-analysis-2/README.md

@@ -17,10 +17,13 @@ Exception in thread "main" java.lang.NullPointerException
 ## Mungo Checker's output
 
 ```
-NotOkFileWrapper4.java:8: error: [Cannot override because object has not ended its protocol] (Cannot override because object has not ended its protocol)
+NotOkFileWrapper4.java:5: error: [Object did not complete its protocol. Type: FileProtocol{Read} | Null] (Object did not complete its protocol. Type: FileProtocol{Read} | Null)
+  private @MungoNullable File file = null;
+                              ^
+NotOkFileWrapper4.java:8: error: [Cannot override because object has not ended its protocol. Type: FileProtocol{Read} | Null] (Cannot override because object has not ended its protocol. Type: FileProtocol{Read} | Null)
     this.file = file;
         ^
-NotOkFileWrapper4.java:12: error: [Cannot call read on null, on ended protocol, on moved value] (Cannot call read on null, on ended protocol, on moved value)
+NotOkFileWrapper4.java:12: error: [Cannot call read on null] (Cannot call read on null)
     return file.read();
                     ^
-2 errors```
+3 errors```