Skip to content

Commit

Permalink
Prepare examples to be sent to Mungo devs
Browse files Browse the repository at this point in the history
  • Loading branch information
jdmota committed May 12, 2020
1 parent f9f6250 commit 1831edb
Show file tree
Hide file tree
Showing 37 changed files with 473 additions and 0 deletions.
34 changes: 34 additions & 0 deletions examples/run_to_mungo_devs
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
#!/bin/bash

CD=`pwd`

if [[ "$CD" =~ ^\/cygdrive.* ]]; then
CD=`cygpath -w "$CD"`
fi

#originalMungo="$CD/mungo-73dd8ae.jar"
originalMungo="$CD/mungo-tools-4d05a7.jar"

testsFolder="$CD/to_mungo_devs"

tests=(
"flow-issue-1"
"flow-issue-2"
"crash-1"
"crash-2"
"crash-3"
"crash-1-adapted"
"crash-2-adapted"
"crash-3-adapted"
)

for testName in "${tests[@]}"
do
cd "$testsFolder/$testName"
echo "Running test: $testName"
output=`java -jar "$originalMungo" -classpath "$originalMungo" *.java 2>&1`

printf "## Current Mungo's output\n\n\`\`\`\n%s\`\`\`\n\n" "$output" > README.md

cd "$CD"
done
89 changes: 89 additions & 0 deletions examples/to_mungo_devs/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
# Examples

This folder contains some examples where Mungo does not detect present issues and code examples where the current version of Mungo crashes. Inside each folder there are `README.md` files with the corresponding outputs that Mungo gives.

Each example was run with the command `java -jar "mungo.jar" -classpath "mungo.jar" *.java`, where `mungo.jar` is the file available at [https://bitbucket.org/abcd-glasgow/mungo-tools/src/4d05a797a0ee22a3680890cbdbd88158056af224/](https://bitbucket.org/abcd-glasgow/mungo-tools/src/4d05a797a0ee22a3680890cbdbd88158056af224/).

## `flow-issue-1`

An example where an error was expected but none is reported.

```java
import java.util.*;

public class Main {
public static void main(String[] args) {
JavaIterator it = new JavaIterator(Arrays.asList(args).iterator());

loop: do {
switch(it.hasNext()) {
case True:
System.out.println(it.next());
continue loop;
case False:
break loop;
}
} while(false); // This is false, iterator might not finish
}
}
```

The current version seems to wrongly assume that a `continue` statement jumps to the beginning of a loop, when in actuality, a `continue` statement jumps to the condition expression. If the condition were to be always `true`, that would make no difference, but if the condition is `false`, bugs may go unnoticed. Like in the example, where the iterator might not reach the `end` state.

## `flow-issue-2`

An example where an error was expected but none is reported.

```java
public class Main {
public static void main(String args[]) {
File f = new File();

switch (f.open()) {
case OK:
switch (f.read()) {
case "CLOSE":
f.close();
break;
}
// File might not close
break;
case ERROR:
break;
}
}
}
```

The current implementation of Mungo does not seem to detect that it is possible that no case in the `switch` statement matches. In the example, this allows the code to exit without the file being closed.

This is a simplified example of an issue not detected in the `CMain.java` file in the `http` example at [https://bitbucket.org/abcd-glasgow/mungo-tools/src/master/demos/http/](https://bitbucket.org/abcd-glasgow/mungo-tools/src/master/demos/http/). If `sread1` does not match `"REQUEST"`, the code jumps to line 102, where there is a `currentC.receive_httpvStrFromS()` call, which is not allowed in the initial state of `CRole`, as specified by the `CProtocol`. An error reporting that was expected, but none was shown.

## `crash-1`

An example that crashes with `NullPointerException`.

Removing the following code from inside the lambda in the `Main.java` avoids the crash, like one can see in the `crash-1-adapted` example.

```java
File f = new File();
f.read();
f.close();
```

## `crash-2`

An example that crashes with `NullPointerException`.

Removing the `@Typestate` annotation from the `File` class, avoids the crash, like one can see in the `crash-2-adapted` example.

## `crash-3`

An example that crashes with `NullPointerException`.

Removing the following line of code from the `Main.java` file avoids the crash, like one can see in the `crash-3-adapted` example.

```java
File f1 = list.get(0);
```

13 changes: 13 additions & 0 deletions examples/to_mungo_devs/crash-1-adapted/File.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import mungo.lib.Typestate;

@Typestate("FileProtocol")
class File {

public String read() {
return "";
}

public void close() {
}

}
6 changes: 6 additions & 0 deletions examples/to_mungo_devs/crash-1-adapted/FileProtocol.protocol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
typestate FileProtocol {
Read = {
String read(): Read,
void close(): end
}
}
9 changes: 9 additions & 0 deletions examples/to_mungo_devs/crash-1-adapted/Main.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
import java.util.function.Supplier;

public class Main {
public static void main() {
Supplier<String> fn = () -> {
return "";
};
}
}
5 changes: 5 additions & 0 deletions examples/to_mungo_devs/crash-1-adapted/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
## Current Mungo's output

```
```

13 changes: 13 additions & 0 deletions examples/to_mungo_devs/crash-1/File.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import mungo.lib.Typestate;

@Typestate("FileProtocol")
class File {

public String read() {
return "";
}

public void close() {
}

}
6 changes: 6 additions & 0 deletions examples/to_mungo_devs/crash-1/FileProtocol.protocol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
typestate FileProtocol {
Read = {
String read(): Read,
void close(): end
}
}
12 changes: 12 additions & 0 deletions examples/to_mungo_devs/crash-1/Main.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
import java.util.function.Supplier;

public class Main {
public static void main() {
Supplier<String> fn = () -> {
File f = new File();
f.read();
f.close();
return "";
};
}
}
29 changes: 29 additions & 0 deletions examples/to_mungo_devs/crash-1/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
## Current Mungo's output

```
Exception in thread "main" java.lang.NullPointerException
at org.extendj.ast.Declarator.typestateCheck(Declarator.java:157)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:610)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.Program.collect(Program.java:582)
at org.extendj.ast.Program.compile(Program.java:604)
at org.extendj.TypestateChecker.run(TypestateChecker.java:32)
at org.extendj.TypestateChecker.main(TypestateChecker.java:18)```
Expand Down
10 changes: 10 additions & 0 deletions examples/to_mungo_devs/crash-2-adapted/File.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
class File {

public String read() {
return "";
}

public void close() {
}

}
6 changes: 6 additions & 0 deletions examples/to_mungo_devs/crash-2-adapted/FileProtocol.protocol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
typestate FileProtocol {
Read = {
String read(): Read,
void close(): end
}
}
3 changes: 3 additions & 0 deletions examples/to_mungo_devs/crash-2-adapted/FileWrapper.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
class FileWrapper {
public File file = new File();
}
5 changes: 5 additions & 0 deletions examples/to_mungo_devs/crash-2-adapted/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
## Current Mungo's output

```
```

13 changes: 13 additions & 0 deletions examples/to_mungo_devs/crash-2/File.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import mungo.lib.Typestate;

@Typestate("FileProtocol")
class File {

public String read() {
return "";
}

public void close() {
}

}
6 changes: 6 additions & 0 deletions examples/to_mungo_devs/crash-2/FileProtocol.protocol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
typestate FileProtocol {
Read = {
String read(): Read,
void close(): end
}
}
3 changes: 3 additions & 0 deletions examples/to_mungo_devs/crash-2/FileWrapper.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
class FileWrapper {
public File file = new File();
}
17 changes: 17 additions & 0 deletions examples/to_mungo_devs/crash-2/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
## Current Mungo's output

```
Exception in thread "main" java.lang.NullPointerException
at org.extendj.ast.Declarator.typestateCheck(Declarator.java:157)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:610)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.Program.collect(Program.java:582)
at org.extendj.ast.Program.compile(Program.java:604)
at org.extendj.TypestateChecker.run(TypestateChecker.java:32)
at org.extendj.TypestateChecker.main(TypestateChecker.java:18)```
Expand Down
13 changes: 13 additions & 0 deletions examples/to_mungo_devs/crash-3-adapted/File.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import mungo.lib.Typestate;

@Typestate("FileProtocol")
class File {

public String read() {
return "";
}

public void close() {
}

}
6 changes: 6 additions & 0 deletions examples/to_mungo_devs/crash-3-adapted/FileProtocol.protocol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
typestate FileProtocol {
Read = {
String read(): Read,
void close(): end
}
}
8 changes: 8 additions & 0 deletions examples/to_mungo_devs/crash-3-adapted/Main.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
import java.util.*;

public class Main {
public static void main() {
List<File> list = new LinkedList<>();
list.add(new File());
}
}
5 changes: 5 additions & 0 deletions examples/to_mungo_devs/crash-3-adapted/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
## Current Mungo's output

```
```

13 changes: 13 additions & 0 deletions examples/to_mungo_devs/crash-3/File.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
import mungo.lib.Typestate;

@Typestate("FileProtocol")
class File {

public String read() {
return "";
}

public void close() {
}

}
6 changes: 6 additions & 0 deletions examples/to_mungo_devs/crash-3/FileProtocol.protocol
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
typestate FileProtocol {
Read = {
String read(): Read,
void close(): end
}
}
9 changes: 9 additions & 0 deletions examples/to_mungo_devs/crash-3/Main.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
import java.util.*;

public class Main {
public static void main() {
List<File> list = new LinkedList<>();
list.add(new File());
File f1 = list.get(0);
}
}
21 changes: 21 additions & 0 deletions examples/to_mungo_devs/crash-3/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
## Current Mungo's output

```
Exception in thread "main" java.lang.NullPointerException
at org.extendj.ast.MethodAccess.getTypestateVar(MethodAccess.java:1909)
at org.extendj.ast.Dot.getTypestateVar(Dot.java:855)
at org.extendj.ast.Declarator.getGraph(Declarator.java:855)
at org.extendj.ast.VarDeclStmt.getGraph(VarDeclStmt.java:567)
at org.extendj.ast.Block.getGraph(Block.java:723)
at org.extendj.ast.MethodDecl.getGraph(MethodDecl.java:2202)
at org.extendj.ast.ClassDecl.getGraph_compute(ClassDecl.java:2586)
at org.extendj.ast.ClassDecl.getGraph(ClassDecl.java:2550)
at org.extendj.ast.ClassDecl.typestateCheck(ClassDecl.java:220)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:610)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.ASTNode.collectTypestate(ASTNode.java:612)
at org.extendj.ast.Program.collect(Program.java:582)
at org.extendj.ast.Program.compile(Program.java:604)
at org.extendj.TypestateChecker.run(TypestateChecker.java:32)
at org.extendj.TypestateChecker.main(TypestateChecker.java:18)```
Expand Down
3 changes: 3 additions & 0 deletions examples/to_mungo_devs/flow-issue-1/Boolean.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
enum Boolean {
True, False;
}
Loading

0 comments on commit 1831edb

Please sign in to comment.