diff --git a/.gitignore b/.gitignore
index e496871..1771e41 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,3 +18,5 @@ drivers/
# Error screenshots generated by TestBench for failed integration tests
error-screenshots/
webpack.generated.js
+
+/fuzz-results
diff --git a/README.md b/README.md
index a485ba3..b2e6578 100644
--- a/README.md
+++ b/README.md
@@ -1,11 +1,11 @@
# Typicalc
-The project is a standard Maven project, so you can import it to your IDE of choice. [Read more how to set up a development environment](https://vaadin.com/docs/v14/flow/installing/installing-overview.html) for Vaadin projects (Windows, Linux, macOS).
+The project is a standard Maven project, so you can import it to your IDE of choice.
+[Read more how to set up a development environment](https://vaadin.com/docs/v18/flow/installing/installing-overview.html) for Vaadin projects (Windows, Linux, macOS).
[To Vaadin documentation](https://vaadin.com/docs-beta/latest/flow/overview/)
-
-## Running and debugging the applcation
+## Running and debugging the application
### Running the application from the command line.
To run from the command line, use `mvn` and open http://localhost:8080 in your browser.
@@ -15,7 +15,7 @@ To run from the command line, use `mvn` and open http://localhost:8080 in your b
- Right click on the Application class
- Select "Debug 'Application.main()'" from the list
-After the application has started, you can view your it at http://localhost:8080/ in your browser.
+After the application has started, you can view it at http://localhost:8080/ in your browser.
You can now also attach break points in code for debugging purposes, by clicking next to a line number in any source file.
### Running and debugging the application in Eclipse
@@ -27,13 +27,29 @@ Do not worry if the debugger breaks at a `SilentExitException`. This is a Spring
After the application has started, you can view your it at http://localhost:8080/ in your browser.
You can now also attach break points in code for debugging purposes, by clicking next to a line number in any source file.
-## What next?
+## Fuzzing with [JQF](https://github.com/rohanpadhye/JQF)
-[vaadin.com](https://vaadin.com) has lots of material to help you get you started:
+### [Zest](https://github.com/rohanpadhye/JQF/wiki/Fuzzing-with-Zest)
-- Follow the tutorials in [vaadin.com/tutorials](https://vaadin.com/tutorials). Especially [vaadin.com/tutorials/getting-started-with-flow](https://vaadin.com/tutorials/getting-started-with-flow) is good for getting a grasp of the basic Vaadin concepts.
-- Read the documentation in [vaadin.com/docs](https://vaadin.com/docs).
-- For a bigger Vaadin application example, check out the Full Stack App starter from [vaadin.com/start](https://vaadin.com/start).
+Run:
+```
+mvn test-compile jqf:fuzz -Dclass=edu.kit.typicalc.model.parser.LambdaParserFuzzTest -Dmethod=testInference
+```
+
+This will use the `LambdaTermGenerator` to create random lambda terms that are then passed to the `ModelImpl`.
+
+### [AFL](https://lcamtuf.coredump.cx/afl/)
+
+First install the necessary JQF tools: https://github.com/rohanpadhye/jqf/wiki/Fuzzing-with-AFL
+
+Remove the `@Ignore` annotation in `LambdaParserFuzzTest` and run:
+```
+mvn test-compile
+jqf-afl-fuzz -c target/test-classes:target/classes -i src/test/resources/terms/ edu.kit.typicalc.model.parser.LambdaParserFuzzTest testLambdaParserAFL
+```
+
+Generated inputs are stored in `fuzz-results/queue/`.
+More samples can be added to `src/test/resources/terms/` to speed up the process.
## Deploying using Docker
@@ -48,3 +64,14 @@ Once the Docker image is correctly built, you can test it locally using
```
docker run -p 8080:8080 myapp:latest
```
+
+## Deploying using a JAR
+
+First build the project:
+```
+mvn package -Pproduction
+```
+Then run the server:
+```
+java -jar target/typicalc-1.0-SNAPSHOT.jar
+```
diff --git a/pom.xml b/pom.xml
index 0371b6c..3cdb986 100644
--- a/pom.xml
+++ b/pom.xml
@@ -92,6 +92,12 @@
spring-boot-devtools
true
+
+ edu.berkeley.cs.jqf
+ jqf-fuzz
+ 1.6
+ test
+
com.vaadin
vaadin-testbench
@@ -159,6 +165,11 @@
spring-boot:run
+
+ edu.berkeley.cs.jqf
+ jqf-maven-plugin
+ 1.6
+
org.springframework.boot
spring-boot-maven-plugin
diff --git a/src/main/resources/application.properties b/src/main/resources/application.properties
index 4f880ca..74a734d 100644
--- a/src/main/resources/application.properties
+++ b/src/main/resources/application.properties
@@ -1,6 +1,5 @@
server.port=${PORT:8080}
+server.servlet.session.persistent=false
logging.level.org.atmosphere = warn
spring.mustache.check-template-location = false
spring.devtools.add-properties = false
-
-# vaadin.whitelisted-packages= org/vaadin/example
diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java
new file mode 100644
index 0000000..20c7a27
--- /dev/null
+++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java
@@ -0,0 +1,65 @@
+package edu.kit.typicalc.model.parser;
+
+import edu.berkeley.cs.jqf.fuzz.Fuzz;
+import edu.berkeley.cs.jqf.fuzz.JQF;
+import edu.kit.typicalc.model.Model;
+import edu.kit.typicalc.model.ModelImpl;
+import edu.kit.typicalc.model.TypeInfererInterface;
+import edu.kit.typicalc.model.step.InferenceStep;
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.util.Result;
+import org.junit.Ignore;
+import org.junit.runner.RunWith;
+
+import java.io.IOException;
+import java.io.InputStream;
+import java.util.HashMap;
+
+import com.pholser.junit.quickcheck.*;
+
+@RunWith(JQF.class)
+public class LambdaParserFuzzTest {
+ /**
+ * Runs the type inference algorithm and gets the first inference step.
+ * Only validates that the algorithm produced something.
+ *
+ * @param term lambda term
+ */
+ @Fuzz
+ public void testInference(@From(LambdaTermGenerator.class) String term) {
+ Model model = new ModelImpl();
+ Result typer = model.getTypeInferer(term, new HashMap<>());
+ InferenceStep first = typer.unwrap().getFirstInferenceStep();
+ }
+
+ // this is how to rerun a specific fuzz result
+ /*
+ @Fuzz(repro="target/fuzz-results/edu.kit.typicalc.model.parser.LambdaParserFuzzTest/testInference/corpus/id_000066")
+ public void testWithGenerator(@From(LambdaTermGenerator.class) String code) {
+ System.out.println(code);
+ }
+ */
+
+ @Fuzz
+ @Ignore // remove if you intend to use AFL
+ public void testLambdaParserAFL(InputStream input) {
+ String term;
+ try {
+ term = new String(input.readAllBytes());
+ } catch (Throwable t) {
+ return;
+ }
+ LambdaParser parser = new LambdaParser(term);
+ Result result = parser.parse();
+ if (result.isOk()) {
+ LambdaTerm term1 = result.unwrap();
+ String sameTerm = term1.toString();
+ LambdaParser parser2 = new LambdaParser(sameTerm);
+ Result result2 = parser2.parse();
+ LambdaTerm term2 = result2.unwrap();
+ if (!term2.equals(term1)) {
+ throw new IllegalStateException("results differ, when parsing: " + term);
+ }
+ }
+ }
+}
diff --git a/src/test/java/edu/kit/typicalc/model/parser/LambdaTermGenerator.java b/src/test/java/edu/kit/typicalc/model/parser/LambdaTermGenerator.java
new file mode 100644
index 0000000..d1747be
--- /dev/null
+++ b/src/test/java/edu/kit/typicalc/model/parser/LambdaTermGenerator.java
@@ -0,0 +1,53 @@
+package edu.kit.typicalc.model.parser;
+
+import com.pholser.junit.quickcheck.generator.GenerationStatus;
+import com.pholser.junit.quickcheck.generator.Generator;
+import com.pholser.junit.quickcheck.random.SourceOfRandomness;
+import edu.kit.typicalc.model.term.AbsTerm;
+import edu.kit.typicalc.model.term.AppTerm;
+import edu.kit.typicalc.model.term.IntegerTerm;
+import edu.kit.typicalc.model.term.LambdaTerm;
+import edu.kit.typicalc.model.term.LetTerm;
+import edu.kit.typicalc.model.term.VarTerm;
+
+public class LambdaTermGenerator extends Generator {
+
+ public LambdaTermGenerator() {
+ super(String.class); // Register the type of objects that we can create
+ }
+
+ public static final String[] VARIABLES = new String[]{"x", "y", "z"};
+
+ /**
+ * Generate a random lambda term.
+ *
+ * @param random source of randomness
+ * @param status not used
+ * @return a random lambda term
+ */
+ @Override
+ public String generate(SourceOfRandomness random, GenerationStatus status) {
+ return generateReal(random).toString();
+ }
+
+ private LambdaTerm generateReal(SourceOfRandomness random) {
+ if (random.nextInt(1, 7) < 3) {
+ LambdaTerm one = generateReal(random);
+ LambdaTerm two = generateReal(random);
+ if (random.nextInt(1, 10) < 8) {
+ return new AppTerm(one, two);
+ } else {
+ return new LetTerm(new VarTerm(random.choose(VARIABLES)), one, two);
+ }
+ } else {
+ if (random.nextBoolean()) {
+ LambdaTerm one = generateReal(random);
+ return new AbsTerm(new VarTerm(random.choose(VARIABLES)), one);
+ } else if (random.nextBoolean()) {
+ return new VarTerm(random.choose(VARIABLES));
+ } else {
+ return new IntegerTerm(5);
+ }
+ }
+ }
+}
diff --git a/src/test/resources/terms/abs b/src/test/resources/terms/abs
new file mode 100644
index 0000000..db2cce6
--- /dev/null
+++ b/src/test/resources/terms/abs
@@ -0,0 +1 @@
+λx. x
diff --git a/src/test/resources/terms/app b/src/test/resources/terms/app
new file mode 100644
index 0000000..74b863c
--- /dev/null
+++ b/src/test/resources/terms/app
@@ -0,0 +1 @@
+x y
diff --git a/src/test/resources/terms/complex b/src/test/resources/terms/complex
new file mode 100644
index 0000000..cc4d4bc
--- /dev/null
+++ b/src/test/resources/terms/complex
@@ -0,0 +1 @@
+(λy. y 5)(λx.x)
diff --git a/src/test/resources/terms/const b/src/test/resources/terms/const
new file mode 100644
index 0000000..27ba77d
--- /dev/null
+++ b/src/test/resources/terms/const
@@ -0,0 +1 @@
+true
diff --git a/src/test/resources/terms/let b/src/test/resources/terms/let
new file mode 100644
index 0000000..8115c39
--- /dev/null
+++ b/src/test/resources/terms/let
@@ -0,0 +1 @@
+let f = λx.x in f 5