arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-09 10:50:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

Add new fuzzing target for latex creator

Browse Source 
FWIW this didn't find anything, we might need type assumptions..
This commit is contained in:
Arne Keller 2021-08-31 11:34:25 +02:00
parent c7bb826b73
commit c2ae5ca10e
1 changed files with 24 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
src/test/java/edu/kit/typicalc/model/parser/LambdaParserFuzzTest.java
View File

@ -8,15 +8,17 @@ import edu.kit.typicalc.model.TypeInfererInterface;
import edu.kit.typicalc.model.step.InferenceStep; import edu.kit.typicalc.model.step.InferenceStep;
import edu.kit.typicalc.model.term.LambdaTerm; import edu.kit.typicalc.model.term.LambdaTerm;
import edu.kit.typicalc.util.Result; import edu.kit.typicalc.util.Result;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreator;
import edu.kit.typicalc.view.content.typeinferencecontent.latexcreator.LatexCreatorMode;
import org.junit.Ignore; import org.junit.Ignore;
import org.junit.runner.RunWith; import org.junit.runner.RunWith;
import java.io.IOException;
import java.io.InputStream; import java.io.InputStream;
import java.util.HashMap;
import com.pholser.junit.quickcheck.*; import com.pholser.junit.quickcheck.*;
import static org.junit.jupiter.api.Assertions.assertTrue;
@RunWith(JQF.class) @RunWith(JQF.class)
public class LambdaParserFuzzTest { public class LambdaParserFuzzTest {
/** /**
@ -32,6 +34,26 @@ public class LambdaParserFuzzTest {
InferenceStep first = typer.unwrap().getFirstInferenceStep(); InferenceStep first = typer.unwrap().getFirstInferenceStep();
} }
/**
* Runs the type inference algorithm and exports the proof tree as latex.
* Validates that it ends with `\end{prooftree}`.
*
* @param term lambda term
*/
@Fuzz
public void testInferenceLatex(@From(LambdaTermGenerator.class) String term) {
Model model = new ModelImpl();
Result<TypeInfererInterface, ParseError> typer = model.getTypeInferer(term, "");
if (typer.isError()) {
return; // don't care
}
var lc = new LatexCreator(typer.unwrap(),
error -> "root." + error.toString(),
LatexCreatorMode.NORMAL);
var latexCode = lc.getTree();
assertTrue(latexCode.endsWith("\\end{prooftree}"));
}
// this is how to rerun a specific fuzz result // this is how to rerun a specific fuzz result
/* /*
@Fuzz(repro="target/fuzz-results/edu.kit.typicalc.model.parser.LambdaParserFuzzTest/testInference/corpus/id_000066") @Fuzz(repro="target/fuzz-results/edu.kit.typicalc.model.parser.LambdaParserFuzzTest/testInference/corpus/id_000066")