diff --git a/.vscode/settings.json b/.vscode/settings.json index 082b194..058a00f 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,3 +1,4 @@ { + "prettier.enable": false, "makefile.configureOnOpen": false } \ No newline at end of file diff --git a/docs/devel/HowToTaclet.md b/docs/devel/HowToTaclet.md index 04c1a8e..de77650 100644 --- a/docs/devel/HowToTaclet.md +++ b/docs/devel/HowToTaclet.md @@ -1,3 +1,6 @@ +---- +approved: DD 2026-08-11 +---- # How to write new taclets New prover rules in KeY can be added in form of built-in rules[^1] written in plain @@ -72,7 +75,14 @@ The `\rules` block contains the taclet definitions, each of which begins with th ("cut_direct"), creating a new block defined by curly brackets and a semicolon at the end. Since the `\find(...)` part of the taclet definition does not contain a `==>`, the `cut_direct` taclet finds (matches) a sub-term anywhere in a sequent formula. -The `\sameUpdateLevel` essentially ensures it doesn't match under an update application. +The application restriction flag `\sameUpdateLevel` ensures that the `\find(...)` and `\add(...)` parts are +under the same update application (or none). + +!!! info + + Since KeY 3.0, `\sameUpdateLevel` is the default for all (relevant) taclets + and does not need to be added manually. Use `\ignoreUpdateLevel` to switch + it off. The taclet creates two new branches, which are defined directly afterwards. The first branch is labeled "CUT: #cutFormula TRUE". @@ -88,6 +98,62 @@ In this branch, the found sub-term is replaced with false (`\replacewith(false)` Finally, the taclet is added to the `cut_direct` heuristics group. +## Automatically Generating Additional Taclets + +KeY 3.1 allows for automatic generation of "derived" taclets. This is +especially helpful for "EQ" taclets, which are commonly used to achieve more +performant automation. Assume a taclet like `elementOfUnion`: + +```key +elementOfUnion { + \schemaVar \term Object o; + \schemaVar \term Field f; + \schemaVar \term LocSet s, s2; + + \find(elementOf(o, f, union(s, s2))) + + \replacewith(elementOf(o, f, s) | elementOf(o, f, s2)) + + \heuristics(simplify_enlarging) + \generate(\EQ(union(s, s2))) +}; +``` + +This taclet can only be applied when `union(s, s2)` is directly in the +`elementOf` function. But a common situation is a sequent such as +``` +s1 = union(s, s2), +==> +elementOf(o, f, s1) +``` +where `union(s, s2)` has been "pulled out" into `s1`. + +We can use _taclet generators_ to deal with this case easily. The +`\generate(\EQ(...))` generates the following taclet automatically: + +```key +elementOfUnionEQ { + \schemaVar \term Object o; + \schemaVar \term Field f; + \schemaVar \term LocSet s, s2; + \schemaVar \term LocSet EQ; + + \assumes(union(s, s2) = EQ ==>) + \find(elementOf(o, f, EQ)) + + \replacewith(elementOf(o, f, s) | elementOf(o, f, s2)) + + \heuristics(simplify_enlarging) +}; +``` + +Note that an `\assumes(...)` part with an equation is added and how the term +given to `\EQ(...)` is replaced in `\find(...)`. The `\find` parts of any rules +in `\addrules` are also altered the same way. Rule sets are copied from the +original taclet but can be altered by `\EQ(union(s, s2) : concrete)`. + +At the moment, `\EQ` is the only supported generator. + ## How to extend the taclet language !!! danger @@ -108,16 +174,16 @@ depend on additional input such as specifications, one can define (automatic or interactive) completions for the taclet. We'll discuss all those points in the following. -It might be helpful to (additionally?) learn about the process by examples. To +It might be helpful to learn about the process by examples. To get started, an example for a new program statement used for matching is -"merge_point", the keyword for a merge point statement. A simpler one is -"ForLoop", a schema variable matching for loops. If you search for those -identifiers in all files in the "key.core" project, you'll find the entry points +`merge_point`, the keyword for a merge point statement. A simpler one is +`ForLoop`, a schema variable matching for loops. If you search for those +identifiers in all files in the project, you'll find the entry points needed for extensions. Note that merge points are also used in JML specifications, which is a different topic (therefore, you might want to ignore -the corresponding parser files "KeYJMLPre{Lexer, Parser}.g, basically everything -in the `(...)/speclang/jml` directory.). An example for a transformer is the -"#for-to-while" construct which accepts a for loop as input and transforms it to +the corresponding parser files `KeYJMLPre{Lexer, Parser}.g`, basically everything +in the `(...)/speclang/jml` directory). An example for a transformer is the +`#for-to-while` construct which accepts a for loop as input and transforms it to a while loop. Your friends here are the eclipse functionalities `Search -> File` (use `*.*` as a pattern here, and only search in the key.core project), `Ctrl+T` for finding types, and `Ctrl+R` for finding resources. @@ -125,22 +191,21 @@ for finding types, and `Ctrl+R` for finding resources. ### Parsing There are several relevant parsers you might need to know. The "main KeY -parser", `src/de/uka/ilkd/key/parser/KeY{Lexer, Parser}.g` is an ANTLR3 parser +parser," `src/main/antlr4/JavaKeY{Lexer, Parser}.g4` is an ANTLR4 parser which covers KeY's language for sorts, terms, formulas etc., taclets, and proof -files. For most extensions, this file does not need to be touched. +files. For most extensions, this file does not need to be touched. It extends +the more general, largely Java-independent parser in `key.ncore/main/antlr/`. -The parsers for Java extensions in taclets and proof files are -`src/de/uka/ilkd/key/parser/schemajava/SchemaJavaParser.jj` and -`src/de/uka/ilkd/key/parser/schemajava/ProofJavaParser.jj`, which are JavaCC -parsers. In the former, you also find definitions for `#for-to-while` and -`merge_point`; in the latter, only `merge_point` occurs since it is an extension -of Java and not a transformer like `#for-to-while` which is only needed in -taclets, but will never occur in a Java program. +We use an [extension of the JavaParser project](https://github.com/jmltoolkit/jmltk) +to parse Java and the KeY's +extentions for Java, such as schema variables or KeY specific constructs. +In its JavaCC file, you find definitions for `#for-to-while` and +`merge_point`. So, if for your taclet the basic taclet language has to be changed, adapt -`KeYParser.g` accordingly; for creating new transformers, `SchemaJavaParser.jj` -is the relevant parser, and for additions to the Java language accepted by KeY, -`SchemaJavaParser.jj` and `ProofJavaParser.jj` will have to be changed. The best +`(Java)KeYParser.g4` accordingly and for creating new transformers or language +extensions, the JavaParser +is the relevant parser. The best advice here is to have a look at the existing definitions to see how to add a new one. Note that at the same time when extending the parser by new transformers or statement types, you will also have to add new Java classes and @@ -148,43 +213,37 @@ extend factories. We cover this in the next section. ### New Program Statement / Expression Types -There are two categories of extensions: (1) New program schema variable sorts, which match existing programming language fragments, and (2) extensions to the language, e.g. by artificial constructs needed for a proof / symbolic execution technique. +There are two categories of extensions: (1) New program schema variable sorts, +which match existing programming language fragments, and (2) extensions to the +language, e.g. by artificial constructs needed for a proof / symbolic +execution technique. A new "matcher sort" for taclets is added quite easily. As an example, take the "loop init" clause of a for loop. A corresponding schema variable for the use in taclets can be declared as `\program LoopInit #loopInit;`. After that, `#loopInit` can be used in a taclet to match a loop init clause. It suffices to -(1) declare a new "program schema variable sort" in +declare a new "program schema variable sort" in `de.uka.ilkd.key.logic.sort.ProgramSVSort` (for instance `LoopInitSort` in the example) which calls the constructor of `ProgramSVSort` with the identifier by -which it later should be referred to in taclet definitions, and (2) to use that -sort in `SchemaJavaParser.jj`. Have a look how `ForInit` is used there to get -a feeling. +which it later should be referred to in taclet definitions. A language extension like the merge points has to be added to several parts in the system: -1. A parser model extension is added in `src/de/uka/ilkd/key/java/recoderext/` +1. A parser model extension is added in [JML ToolKit](https://github.com/jmltoolkit/jmltk) (see `MergePointStatement.java` for an example). -2. The factories `de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java` -and `(...)/ProofJavaProgramFactory.java` are extended by corresponding factory -methods. -3. A mirror of the parser extension for the logic side of KeY is added to +2. A mirror of the parser extension for the logic side of KeY is added to `de/uka/ilkd/key/java/statement/` (also here, there's a `MergePointStatement.java`). -5. A converter for the parser model extension to the logic representation in -`de/uka/ilkd/key/java/Recoder2KeYConverter.java`. Look what's done for the -`MergePointStatement`. The methods there are called by reflection, so the name -of the new method has to be `convert`, and it has to accept the parser model -extension as only argument. -6. Extension of Java visitor classes: Classes `Visitor.java`, +3. A converter for the parser model extension to the logic representation in +`de/uka/ilkd/key/java/loader/JP2KeYConverter.java`. Look what's done for the +`MergePointStatement`. +4. Extension of Java visitor classes: Classes `Visitor.java`, `JavaASTVisitor.java`, `CreatingASTVisitor.java`, and `ProgVarReplaceVisitor.java` -in directory `de/uka/ilkd/key/java/visitor/`. Note that now all of these might +in directory `de/uka/ilkd/key/java/visitor/`. Note that not all of these might apply to you, e.g. if your new statement does not contain program variables that might have to be substituted in a proof. -7. Extension of the pretty printer to nicely render your extension in sequents: +5. Extension of the pretty printer to nicely render your extension in sequents: `de/uka/ilkd/key/java/PrettyPrinter.java`. -The factory methods and parser model classes can then be used in -`{Schema, Proof}JavaParser.jj`. ### New Meta Constructs / Transformers @@ -200,19 +259,18 @@ for the bad style of delegating everything to a transformer). For adding transformers this to the system, follow these steps: 1. Add a model class to the directory `src/de/uka/ilkd/key/rule/metaconstruct/` -(see e.g. `ForToWhile.java). The class should extend `ProgramTransformer` and -pass the keyword to be used to the super class, here "#for-to-while". -2. Extend the class `src/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter` -to return the new class when appropriate. Look for `convert(RKeYMetaConstruct)` -to see what's done for `#for-to-while`. -3. Add the construct to the parser (`SchemaJavaParser.jj`). +(see e.g. `ForToWhile.java`). The class should extend `ProgramTransformer` and +pass the keyword to be used to the super class, here `#for-to-while`. +2. Extend the `visit(MetaConstruct, Void)` method in `src/de/uka/ilkd/key/java/JP2KeYConverter` +to return the new class when appropriate. See what's done for `#for-to-while`. +3. Add the construct to [the parser](https://github.com/jmltoolkit/jmltk). ### Completions Sometimes the input to a taclet depends on other information than that available from a current proof situation (i.e., a sequent). In that case, the rule has to be completed before it is applied. A good example is the rule "cut" -(`resources/de/uka/ilkd/key/proof/rules/propRule.key`) defined as follows: +(`resources/de/uka/ilkd/key/proof/rules/classicalLogic/propRule.key`) defined as follows: ```key \schemaVariables {