mirror of
https://github.com/pgpainless/pgpainless.git
synced 2024-11-16 01:12:05 +01:00
Kotlin conversion: Syntax checking
This commit is contained in:
parent
25aff68765
commit
d27cd7f3f5
10 changed files with 157 additions and 254 deletions
|
@ -1,142 +0,0 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
|
||||||
//
|
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
|
||||||
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
|
||||||
|
|
||||||
import org.pgpainless.exception.MalformedOpenPgpMessageException;
|
|
||||||
|
|
||||||
import javax.annotation.Nonnull;
|
|
||||||
import javax.annotation.Nullable;
|
|
||||||
|
|
||||||
/**
|
|
||||||
* This class describes the syntax for OpenPGP messages as specified by rfc4880.
|
|
||||||
*
|
|
||||||
* @see <a href="https://www.rfc-editor.org/rfc/rfc4880#section-11.3">
|
|
||||||
* rfc4880 - §11.3. OpenPGP Messages</a>
|
|
||||||
* @see <a href="https://blog.jabberhead.tk/2022/09/14/using-pushdown-automata-to-verify-packet-sequences/">
|
|
||||||
* Blog post about theoretic background and translation of grammar to PDA syntax</a>
|
|
||||||
* @see <a href="https://blog.jabberhead.tk/2022/10/26/implementing-packet-sequence-validation-using-pushdown-automata/">
|
|
||||||
* Blog post about practically implementing the PDA for packet syntax validation</a>
|
|
||||||
*/
|
|
||||||
public class OpenPgpMessageSyntax implements Syntax {
|
|
||||||
|
|
||||||
@Override
|
|
||||||
public @Nonnull Transition transition(@Nonnull State from, @Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException {
|
|
||||||
switch (from) {
|
|
||||||
case OpenPgpMessage:
|
|
||||||
return fromOpenPgpMessage(input, stackItem);
|
|
||||||
case LiteralMessage:
|
|
||||||
return fromLiteralMessage(input, stackItem);
|
|
||||||
case CompressedMessage:
|
|
||||||
return fromCompressedMessage(input, stackItem);
|
|
||||||
case EncryptedMessage:
|
|
||||||
return fromEncryptedMessage(input, stackItem);
|
|
||||||
case Valid:
|
|
||||||
return fromValid(input, stackItem);
|
|
||||||
}
|
|
||||||
|
|
||||||
throw new MalformedOpenPgpMessageException(from, input, stackItem);
|
|
||||||
}
|
|
||||||
|
|
||||||
@Nonnull
|
|
||||||
Transition fromOpenPgpMessage(@Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException {
|
|
||||||
if (stackItem != StackSymbol.msg) {
|
|
||||||
throw new MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem);
|
|
||||||
}
|
|
||||||
|
|
||||||
switch (input) {
|
|
||||||
case LiteralData:
|
|
||||||
return new Transition(State.LiteralMessage);
|
|
||||||
|
|
||||||
case Signature:
|
|
||||||
return new Transition(State.OpenPgpMessage, StackSymbol.msg);
|
|
||||||
|
|
||||||
case OnePassSignature:
|
|
||||||
return new Transition(State.OpenPgpMessage, StackSymbol.ops, StackSymbol.msg);
|
|
||||||
|
|
||||||
case CompressedData:
|
|
||||||
return new Transition(State.CompressedMessage);
|
|
||||||
|
|
||||||
case EncryptedData:
|
|
||||||
return new Transition(State.EncryptedMessage);
|
|
||||||
|
|
||||||
case EndOfSequence:
|
|
||||||
default:
|
|
||||||
throw new MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
@Nonnull
|
|
||||||
Transition fromLiteralMessage(@Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException {
|
|
||||||
switch (input) {
|
|
||||||
case Signature:
|
|
||||||
if (stackItem == StackSymbol.ops) {
|
|
||||||
return new Transition(State.LiteralMessage);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
|
|
||||||
case EndOfSequence:
|
|
||||||
if (stackItem == StackSymbol.terminus) {
|
|
||||||
return new Transition(State.Valid);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
throw new MalformedOpenPgpMessageException(State.LiteralMessage, input, stackItem);
|
|
||||||
}
|
|
||||||
|
|
||||||
@Nonnull
|
|
||||||
Transition fromCompressedMessage(@Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException {
|
|
||||||
switch (input) {
|
|
||||||
case Signature:
|
|
||||||
if (stackItem == StackSymbol.ops) {
|
|
||||||
return new Transition(State.CompressedMessage);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
|
|
||||||
case EndOfSequence:
|
|
||||||
if (stackItem == StackSymbol.terminus) {
|
|
||||||
return new Transition(State.Valid);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
throw new MalformedOpenPgpMessageException(State.CompressedMessage, input, stackItem);
|
|
||||||
}
|
|
||||||
|
|
||||||
@Nonnull
|
|
||||||
Transition fromEncryptedMessage(@Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException {
|
|
||||||
switch (input) {
|
|
||||||
case Signature:
|
|
||||||
if (stackItem == StackSymbol.ops) {
|
|
||||||
return new Transition(State.EncryptedMessage);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
|
|
||||||
case EndOfSequence:
|
|
||||||
if (stackItem == StackSymbol.terminus) {
|
|
||||||
return new Transition(State.Valid);
|
|
||||||
}
|
|
||||||
break;
|
|
||||||
}
|
|
||||||
|
|
||||||
throw new MalformedOpenPgpMessageException(State.EncryptedMessage, input, stackItem);
|
|
||||||
}
|
|
||||||
|
|
||||||
@Nonnull
|
|
||||||
Transition fromValid(@Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException {
|
|
||||||
if (input == InputSymbol.EndOfSequence) {
|
|
||||||
// allow subsequent read() calls.
|
|
||||||
return new Transition(State.Valid);
|
|
||||||
}
|
|
||||||
// There is no applicable transition rule out of Valid
|
|
||||||
throw new MalformedOpenPgpMessageException(State.Valid, input, stackItem);
|
|
||||||
}
|
|
||||||
}
|
|
|
@ -1,33 +0,0 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
|
||||||
//
|
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
|
||||||
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
|
||||||
|
|
||||||
import org.pgpainless.exception.MalformedOpenPgpMessageException;
|
|
||||||
|
|
||||||
import javax.annotation.Nonnull;
|
|
||||||
import javax.annotation.Nullable;
|
|
||||||
|
|
||||||
/**
|
|
||||||
* This interface can be used to define a custom syntax for the {@link PDA}.
|
|
||||||
*/
|
|
||||||
public interface Syntax {
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Describe a transition rule from {@link State} <pre>from</pre> for {@link InputSymbol} <pre>input</pre>
|
|
||||||
* with {@link StackSymbol} <pre>stackItem</pre> from the top of the {@link PDA PDAs} stack.
|
|
||||||
* The resulting {@link Transition} contains the new {@link State}, as well as a list of
|
|
||||||
* {@link StackSymbol StackSymbols} that get pushed onto the stack by the transition rule.
|
|
||||||
* If there is no applicable rule, a {@link MalformedOpenPgpMessageException} is thrown, since in this case
|
|
||||||
* the {@link InputSymbol} must be considered illegal.
|
|
||||||
*
|
|
||||||
* @param from current state of the PDA
|
|
||||||
* @param input input symbol
|
|
||||||
* @param stackItem item that got popped from the top of the stack
|
|
||||||
* @return applicable transition rule containing the new state and pushed stack symbols
|
|
||||||
* @throws MalformedOpenPgpMessageException if there is no applicable transition rule (the input symbol is illegal)
|
|
||||||
*/
|
|
||||||
@Nonnull Transition transition(@Nonnull State from, @Nonnull InputSymbol input, @Nullable StackSymbol stackItem)
|
|
||||||
throws MalformedOpenPgpMessageException;
|
|
||||||
}
|
|
|
@ -1,48 +0,0 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
|
||||||
//
|
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
|
||||||
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
|
||||||
|
|
||||||
import javax.annotation.Nonnull;
|
|
||||||
import java.util.ArrayList;
|
|
||||||
import java.util.Arrays;
|
|
||||||
import java.util.List;
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Result of applying a transition rule.
|
|
||||||
* Transition rules can be described by implementing the {@link Syntax} interface.
|
|
||||||
*/
|
|
||||||
public class Transition {
|
|
||||||
|
|
||||||
private final List<StackSymbol> pushedItems = new ArrayList<>();
|
|
||||||
private final State newState;
|
|
||||||
|
|
||||||
public Transition(@Nonnull State newState, @Nonnull StackSymbol... pushedItems) {
|
|
||||||
this.newState = newState;
|
|
||||||
this.pushedItems.addAll(Arrays.asList(pushedItems));
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Return the new {@link State} that is reached by applying the transition.
|
|
||||||
*
|
|
||||||
* @return new state
|
|
||||||
*/
|
|
||||||
@Nonnull
|
|
||||||
public State getNewState() {
|
|
||||||
return newState;
|
|
||||||
}
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Return a list of {@link StackSymbol StackSymbols} that are pushed onto the stack
|
|
||||||
* by applying the transition.
|
|
||||||
* The list contains items in the order in which they are pushed onto the stack.
|
|
||||||
* The list may be empty.
|
|
||||||
*
|
|
||||||
* @return list of items to be pushed onto the stack
|
|
||||||
*/
|
|
||||||
@Nonnull
|
|
||||||
public List<StackSymbol> getPushedItems() {
|
|
||||||
return new ArrayList<>(pushedItems);
|
|
||||||
}
|
|
||||||
}
|
|
|
@ -1,8 +0,0 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
|
||||||
//
|
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
|
||||||
|
|
||||||
/**
|
|
||||||
* Pushdown Automaton to verify validity of packet sequences according to the OpenPGP Message format.
|
|
||||||
*/
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
|
|
@ -1,36 +1,30 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
|
||||||
//
|
//
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
// SPDX-License-Identifier: Apache-2.0
|
||||||
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
package org.pgpainless.decryption_verification.syntax_check
|
||||||
|
|
||||||
import org.bouncycastle.openpgp.PGPCompressedData;
|
enum class InputSymbol {
|
||||||
import org.bouncycastle.openpgp.PGPEncryptedDataList;
|
|
||||||
import org.bouncycastle.openpgp.PGPLiteralData;
|
|
||||||
import org.bouncycastle.openpgp.PGPOnePassSignatureList;
|
|
||||||
import org.bouncycastle.openpgp.PGPSignatureList;
|
|
||||||
|
|
||||||
public enum InputSymbol {
|
|
||||||
/**
|
/**
|
||||||
* A {@link PGPLiteralData} packet.
|
* A [PGPLiteralData] packet.
|
||||||
*/
|
*/
|
||||||
LiteralData,
|
LiteralData,
|
||||||
/**
|
/**
|
||||||
* A {@link PGPSignatureList} object.
|
* A [PGPSignatureList] object.
|
||||||
*/
|
*/
|
||||||
Signature,
|
Signature,
|
||||||
/**
|
/**
|
||||||
* A {@link PGPOnePassSignatureList} object.
|
* A [PGPOnePassSignatureList] object.
|
||||||
*/
|
*/
|
||||||
OnePassSignature,
|
OnePassSignature,
|
||||||
/**
|
/**
|
||||||
* A {@link PGPCompressedData} packet.
|
* A [PGPCompressedData] packet.
|
||||||
* The contents of this packet MUST form a valid OpenPGP message, so a nested PDA is opened to verify
|
* The contents of this packet MUST form a valid OpenPGP message, so a nested PDA is opened to verify
|
||||||
* its nested packet sequence.
|
* its nested packet sequence.
|
||||||
*/
|
*/
|
||||||
CompressedData,
|
CompressedData,
|
||||||
/**
|
/**
|
||||||
* A {@link PGPEncryptedDataList} object.
|
* A [PGPEncryptedDataList] object.
|
||||||
* This object combines multiple ESKs and the corresponding Symmetrically Encrypted
|
* This object combines multiple ESKs and the corresponding Symmetrically Encrypted
|
||||||
* (possibly Integrity Protected) Data packet.
|
* (possibly Integrity Protected) Data packet.
|
||||||
*/
|
*/
|
||||||
|
@ -42,4 +36,4 @@ public enum InputSymbol {
|
||||||
* (e.g. the end of a Compressed Data packet).
|
* (e.g. the end of a Compressed Data packet).
|
||||||
*/
|
*/
|
||||||
EndOfSequence
|
EndOfSequence
|
||||||
}
|
}
|
|
@ -0,0 +1,88 @@
|
||||||
|
// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
|
||||||
|
//
|
||||||
|
// SPDX-License-Identifier: Apache-2.0
|
||||||
|
|
||||||
|
package org.pgpainless.decryption_verification.syntax_check
|
||||||
|
|
||||||
|
import org.pgpainless.exception.MalformedOpenPgpMessageException
|
||||||
|
|
||||||
|
/**
|
||||||
|
* This class describes the syntax for OpenPGP messages as specified by rfc4880.
|
||||||
|
*
|
||||||
|
* See [rfc4880 - §11.3. OpenPGP Messages](https://www.rfc-editor.org/rfc/rfc4880#section-11.3)
|
||||||
|
* See [Blog post about theoretic background and translation of grammar to PDA syntax](https://blog.jabberhead.tk/2022/09/14/using-pushdown-automata-to-verify-packet-sequences/)
|
||||||
|
* See [Blog post about practically implementing the PDA for packet syntax validation](https://blog.jabberhead.tk/2022/10/26/implementing-packet-sequence-validation-using-pushdown-automata/)
|
||||||
|
*/
|
||||||
|
class OpenPgpMessageSyntax : Syntax {
|
||||||
|
|
||||||
|
override fun transition(from: State, input: InputSymbol, stackItem: StackSymbol?): Transition {
|
||||||
|
return when (from) {
|
||||||
|
State.OpenPgpMessage -> fromOpenPgpMessage(input, stackItem)
|
||||||
|
State.LiteralMessage -> fromLiteralMessage(input, stackItem)
|
||||||
|
State.CompressedMessage -> fromCompressedMessage(input, stackItem)
|
||||||
|
State.EncryptedMessage -> fromEncryptedMessage(input, stackItem)
|
||||||
|
State.Valid -> fromValid(input, stackItem)
|
||||||
|
else -> throw MalformedOpenPgpMessageException(from, input, stackItem)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
fun fromOpenPgpMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
|
||||||
|
if (stackItem !== StackSymbol.msg) {
|
||||||
|
throw MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem)
|
||||||
|
}
|
||||||
|
return when (input) {
|
||||||
|
InputSymbol.LiteralData -> Transition(State.LiteralMessage)
|
||||||
|
InputSymbol.Signature -> Transition(State.OpenPgpMessage, StackSymbol.msg)
|
||||||
|
InputSymbol.OnePassSignature -> Transition(State.OpenPgpMessage, StackSymbol.ops, StackSymbol.msg)
|
||||||
|
InputSymbol.CompressedData -> Transition(State.CompressedMessage)
|
||||||
|
InputSymbol.EncryptedData -> Transition(State.EncryptedMessage)
|
||||||
|
InputSymbol.EndOfSequence -> throw MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem)
|
||||||
|
else -> throw MalformedOpenPgpMessageException(State.OpenPgpMessage, input, stackItem)
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
@Throws(MalformedOpenPgpMessageException::class)
|
||||||
|
fun fromLiteralMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
|
||||||
|
if (input == InputSymbol.Signature && stackItem == StackSymbol.ops) {
|
||||||
|
return Transition(State.LiteralMessage)
|
||||||
|
}
|
||||||
|
if (input == InputSymbol.EndOfSequence && stackItem == StackSymbol.terminus) {
|
||||||
|
return Transition(State.Valid)
|
||||||
|
}
|
||||||
|
|
||||||
|
throw MalformedOpenPgpMessageException(State.LiteralMessage, input, stackItem)
|
||||||
|
}
|
||||||
|
|
||||||
|
@Throws(MalformedOpenPgpMessageException::class)
|
||||||
|
fun fromCompressedMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
|
||||||
|
if (input == InputSymbol.Signature && stackItem == StackSymbol.ops) {
|
||||||
|
return Transition(State.CompressedMessage)
|
||||||
|
}
|
||||||
|
if (input == InputSymbol.EndOfSequence && stackItem == StackSymbol.terminus) {
|
||||||
|
return Transition(State.Valid)
|
||||||
|
}
|
||||||
|
|
||||||
|
throw MalformedOpenPgpMessageException(State.CompressedMessage, input, stackItem)
|
||||||
|
}
|
||||||
|
|
||||||
|
@Throws(MalformedOpenPgpMessageException::class)
|
||||||
|
fun fromEncryptedMessage(input: InputSymbol, stackItem: StackSymbol?): Transition {
|
||||||
|
if (input == InputSymbol.Signature && stackItem == StackSymbol.ops) {
|
||||||
|
return Transition(State.EncryptedMessage)
|
||||||
|
}
|
||||||
|
if (input == InputSymbol.EndOfSequence && stackItem == StackSymbol.terminus) {
|
||||||
|
return Transition(State.Valid)
|
||||||
|
}
|
||||||
|
|
||||||
|
throw MalformedOpenPgpMessageException(State.EncryptedMessage, input, stackItem)
|
||||||
|
}
|
||||||
|
|
||||||
|
@Throws(MalformedOpenPgpMessageException::class)
|
||||||
|
fun fromValid(input: InputSymbol, stackItem: StackSymbol?): Transition {
|
||||||
|
if (input == InputSymbol.EndOfSequence) {
|
||||||
|
// allow subsequent read() calls.
|
||||||
|
return Transition(State.Valid)
|
||||||
|
}
|
||||||
|
throw MalformedOpenPgpMessageException(State.Valid, input, stackItem)
|
||||||
|
}
|
||||||
|
}
|
|
@ -1,10 +1,10 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
|
||||||
//
|
//
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
// SPDX-License-Identifier: Apache-2.0
|
||||||
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
package org.pgpainless.decryption_verification.syntax_check
|
||||||
|
|
||||||
public enum StackSymbol {
|
enum class StackSymbol {
|
||||||
/**
|
/**
|
||||||
* OpenPGP Message.
|
* OpenPGP Message.
|
||||||
*/
|
*/
|
||||||
|
@ -17,4 +17,4 @@ public enum StackSymbol {
|
||||||
* Special symbol representing the end of the message.
|
* Special symbol representing the end of the message.
|
||||||
*/
|
*/
|
||||||
terminus
|
terminus
|
||||||
}
|
}
|
|
@ -1,16 +1,16 @@
|
||||||
// SPDX-FileCopyrightText: 2022 Paul Schaub <vanitasvitae@fsfe.org>
|
// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
|
||||||
//
|
//
|
||||||
// SPDX-License-Identifier: Apache-2.0
|
// SPDX-License-Identifier: Apache-2.0
|
||||||
|
|
||||||
package org.pgpainless.decryption_verification.syntax_check;
|
package org.pgpainless.decryption_verification.syntax_check
|
||||||
|
|
||||||
/**
|
/**
|
||||||
* Set of states of the automaton.
|
* Set of states of the automaton.
|
||||||
*/
|
*/
|
||||||
public enum State {
|
enum class State {
|
||||||
OpenPgpMessage,
|
OpenPgpMessage,
|
||||||
LiteralMessage,
|
LiteralMessage,
|
||||||
CompressedMessage,
|
CompressedMessage,
|
||||||
EncryptedMessage,
|
EncryptedMessage,
|
||||||
Valid
|
Valid
|
||||||
}
|
}
|
|
@ -0,0 +1,30 @@
|
||||||
|
// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
|
||||||
|
//
|
||||||
|
// SPDX-License-Identifier: Apache-2.0
|
||||||
|
|
||||||
|
package org.pgpainless.decryption_verification.syntax_check
|
||||||
|
|
||||||
|
import org.pgpainless.exception.MalformedOpenPgpMessageException
|
||||||
|
|
||||||
|
/**
|
||||||
|
* This interface can be used to define a custom syntax for the [PDA].
|
||||||
|
*/
|
||||||
|
interface Syntax {
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Describe a transition rule from [State] <pre>from</pre> for [InputSymbol] <pre>input</pre>
|
||||||
|
* with [StackSymbol] <pre>stackItem</pre> from the top of the [PDAs][PDA] stack.
|
||||||
|
* The resulting [Transition] contains the new [State], as well as a list of
|
||||||
|
* [StackSymbols][StackSymbol] that get pushed onto the stack by the transition rule.
|
||||||
|
* If there is no applicable rule, a [MalformedOpenPgpMessageException] is thrown, since in this case
|
||||||
|
* the [InputSymbol] must be considered illegal.
|
||||||
|
*
|
||||||
|
* @param from current state of the PDA
|
||||||
|
* @param input input symbol
|
||||||
|
* @param stackItem item that got popped from the top of the stack
|
||||||
|
* @return applicable transition rule containing the new state and pushed stack symbols
|
||||||
|
* @throws MalformedOpenPgpMessageException if there is no applicable transition rule (the input symbol is illegal)
|
||||||
|
*/
|
||||||
|
@Throws(MalformedOpenPgpMessageException::class)
|
||||||
|
fun transition(from: State, input: InputSymbol, stackItem: StackSymbol?): Transition
|
||||||
|
}
|
|
@ -0,0 +1,22 @@
|
||||||
|
// SPDX-FileCopyrightText: 2023 Paul Schaub <vanitasvitae@fsfe.org>
|
||||||
|
//
|
||||||
|
// SPDX-License-Identifier: Apache-2.0
|
||||||
|
|
||||||
|
package org.pgpainless.decryption_verification.syntax_check
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Result of applying a transition rule.
|
||||||
|
* Transition rules can be described by implementing the [Syntax] interface.
|
||||||
|
*
|
||||||
|
* @param newState new [State] that is reached by applying the transition.
|
||||||
|
* @param pushedItems list of [StackSymbol] that are pushed onto the stack by applying the transition.
|
||||||
|
* The list contains items in the order in which they are pushed onto the stack.
|
||||||
|
* The list may be empty.
|
||||||
|
*/
|
||||||
|
class Transition private constructor(
|
||||||
|
val pushedItems: List<StackSymbol>,
|
||||||
|
val newState: State
|
||||||
|
) {
|
||||||
|
|
||||||
|
constructor(newState: State, vararg pushedItems: StackSymbol): this(pushedItems.toList(), newState)
|
||||||
|
}
|
Loading…
Reference in a new issue