diff --git a/backend/pom.xml b/backend/pom.xml index ca6665e3..d87abfce 100644 --- a/backend/pom.xml +++ b/backend/pom.xml @@ -127,7 +127,7 @@ org.key-project key.core - 2.12.2 + 3.0.0 org.projectlombok @@ -135,6 +135,11 @@ 1.18.38 provided + + com.bucket4j + bucket4j_jdk17-core + 8.14.0 + diff --git a/backend/src/main/java/edu/kit/cbc/common/corc/KeYInteraction.java b/backend/src/main/java/edu/kit/cbc/common/corc/KeYInteraction.java index 0becfe8c..1582701b 100644 --- a/backend/src/main/java/edu/kit/cbc/common/corc/KeYInteraction.java +++ b/backend/src/main/java/edu/kit/cbc/common/corc/KeYInteraction.java @@ -3,6 +3,7 @@ import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProblemLoaderException; +import de.uka.ilkd.key.proof.io.ProofSaver; import de.uka.ilkd.key.settings.ChoiceSettings; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.strategy.StrategyProperties; @@ -16,7 +17,7 @@ /** * Information: This class is taken from here. - * We know that it is ugly but there is no documentation of how to interact with KeY other than this. + * As far as we know, there is no documentation of how to interact with KeY other than this. * It is best if you leave this class unchanged. However, if you have to make changes here, make sure * to test them even more thoroughly than normal. */ @@ -32,7 +33,7 @@ public static Proof startKeyProof(File location, boolean inlining) { try { printFile(location.getPath()); if (!ProofSettings.isChoiceSettingInitialised()) { - KeYEnvironment env = KeYEnvironment.load(location); + KeYEnvironment env = KeYEnvironment.load(location.toPath()); env.dispose(); } @@ -44,7 +45,7 @@ public static Proof startKeyProof(File location, boolean inlining) { newSettings.put("runtimeExceptions", "runtimeExceptions:ban"); choiceSettings.setDefaultChoices(newSettings); - KeYEnvironment env = KeYEnvironment.load(location); + KeYEnvironment env = KeYEnvironment.load(location.toPath()); Proof proof = env.getLoadedProof(); /*Set STRATEGY options*/ @@ -68,10 +69,9 @@ public static Proof startKeyProof(File location, boolean inlining) { // Show proof result try { - Path parentDir = location.getParentFile().toPath(); Path proofLocation = parentDir.resolve(location.getName().split("\\.")[0] + ".proof"); - proof.saveToFile(proofLocation.toFile()); + ProofSaver.saveToFile(proofLocation, proof); } catch (IOException e) { e.printStackTrace(); } diff --git a/backend/src/main/java/edu/kit/cbc/common/corc/parsing/ParseException.java b/backend/src/main/java/edu/kit/cbc/common/corc/parsing/ParseException.java index 5a440eb4..4dc0ca0a 100644 --- a/backend/src/main/java/edu/kit/cbc/common/corc/parsing/ParseException.java +++ b/backend/src/main/java/edu/kit/cbc/common/corc/parsing/ParseException.java @@ -1,7 +1,33 @@ package edu.kit.cbc.common.corc.parsing; public class ParseException extends RuntimeException { + + private final int position; + private final String input; + private final String expected; + private final String found; + public ParseException(String message) { super(message); + this.position = -1; + this.input = null; + this.expected = null; + this.found = null; + } + + public int getPosition() { + return position; + } + + public String getInput() { + return input; + } + + public String getExpected() { + return expected; + } + + public String getFound() { + return found; } } diff --git a/backend/src/main/java/edu/kit/cbc/common/corc/parsing/SemanticException.java b/backend/src/main/java/edu/kit/cbc/common/corc/parsing/SemanticException.java index 24340334..7fd441f0 100644 --- a/backend/src/main/java/edu/kit/cbc/common/corc/parsing/SemanticException.java +++ b/backend/src/main/java/edu/kit/cbc/common/corc/parsing/SemanticException.java @@ -2,7 +2,14 @@ public class SemanticException extends Exception { + private final String variableName; + public SemanticException(String message) { super(message); + this.variableName = null; + } + + public String getVariableName() { + return variableName; } } diff --git a/backend/src/main/java/edu/kit/cbc/common/error/ParseExceptionHandler.java b/backend/src/main/java/edu/kit/cbc/common/error/ParseExceptionHandler.java new file mode 100644 index 00000000..3bcdf6be --- /dev/null +++ b/backend/src/main/java/edu/kit/cbc/common/error/ParseExceptionHandler.java @@ -0,0 +1,40 @@ +package edu.kit.cbc.common.error; + +import edu.kit.cbc.common.corc.parsing.ParseException; +import io.micronaut.context.annotation.Replaces; +import io.micronaut.core.convert.exceptions.ConversionErrorException; +import io.micronaut.http.HttpRequest; +import io.micronaut.http.HttpResponse; +import io.micronaut.http.MediaType; +import io.micronaut.http.annotation.Produces; +import io.micronaut.http.server.exceptions.ConversionErrorHandler; +import io.micronaut.http.server.exceptions.ExceptionHandler; +import jakarta.inject.Singleton; + +@Singleton +@Produces +@Replaces(ConversionErrorHandler.class) +public class ParseExceptionHandler implements ExceptionHandler> { + + @Override + public HttpResponse handle(HttpRequest request, ConversionErrorException exception) { + ParseException parseEx = findCause(exception, ParseException.class); + if (parseEx != null) { + PreExecutionError error = PreExecutionError.fromParseException(parseEx, request.getPath()); + return HttpResponse.badRequest(error).contentType(MediaType.of("application/problem+json")); + } + return HttpResponse.badRequest(); + } + + @SuppressWarnings("unchecked") + private static T findCause(Throwable ex, Class type) { + Throwable t = ex; + while (t != null) { + if (type.isInstance(t)) { + return (T) t; + } + t = t.getCause(); + } + return null; + } +} diff --git a/backend/src/main/java/edu/kit/cbc/common/error/PreExecutionError.java b/backend/src/main/java/edu/kit/cbc/common/error/PreExecutionError.java new file mode 100644 index 00000000..8b0c4e0b --- /dev/null +++ b/backend/src/main/java/edu/kit/cbc/common/error/PreExecutionError.java @@ -0,0 +1,73 @@ +package edu.kit.cbc.common.error; + +import com.fasterxml.jackson.annotation.JsonInclude; +import edu.kit.cbc.common.corc.parsing.ParseException; +import edu.kit.cbc.common.corc.parsing.SemanticException; +import io.micronaut.serde.annotation.Serdeable; +import java.util.List; + +@Serdeable +@JsonInclude(JsonInclude.Include.NON_NULL) +public record PreExecutionError( + String type, + String title, + int status, + String detail, + String instance, + List errors +) { + public enum ErrorType { SYNTACTIC, SEMANTIC } + + @Serdeable + @JsonInclude(JsonInclude.Include.NON_NULL) + public record ErrorDetail( + String message, + ErrorType errorType, + Integer position, + String input, + String expected, + String found, + String variableName + ) {} + + public static PreExecutionError fromParseException(ParseException ex, String instance) { + int pos = ex.getPosition(); + ErrorDetail detail = new ErrorDetail( + ex.getMessage(), + ErrorType.SYNTACTIC, + pos >= 0 ? pos : null, + ex.getInput(), + ex.getExpected(), + ex.getFound(), + null + ); + return new PreExecutionError( + "about:blank", + "Syntax Error", + 400, + ex.getMessage(), + instance, + List.of(detail) + ); + } + + public static PreExecutionError fromSemanticException(SemanticException ex, String instance) { + ErrorDetail detail = new ErrorDetail( + ex.getMessage(), + ErrorType.SEMANTIC, + null, + null, + null, + null, + ex.getVariableName() + ); + return new PreExecutionError( + "about:blank", + "Semantic Error", + 400, + ex.getMessage(), + instance, + List.of(detail) + ); + } +} diff --git a/backend/src/main/java/edu/kit/cbc/editor/llm/LLMQueryDto.java b/backend/src/main/java/edu/kit/cbc/editor/llm/LLMQueryDto.java index d4ae5d84..4170ed9e 100644 --- a/backend/src/main/java/edu/kit/cbc/editor/llm/LLMQueryDto.java +++ b/backend/src/main/java/edu/kit/cbc/editor/llm/LLMQueryDto.java @@ -5,11 +5,12 @@ import jakarta.validation.constraints.NotBlank; import jakarta.validation.constraints.NotNull; import jakarta.validation.constraints.Pattern; +import jakarta.validation.constraints.Size; import java.util.List; @Serdeable public record LLMQueryDto( - @NotNull @Valid List input, + @NotNull @Valid @Size(min = 1, max = 50) List input, @NotBlank String model, @NotNull LLMProvider provider ) { diff --git a/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitCleanupTask.java b/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitCleanupTask.java new file mode 100644 index 00000000..ec5e2161 --- /dev/null +++ b/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitCleanupTask.java @@ -0,0 +1,19 @@ +package edu.kit.cbc.editor.ratelimit; + +import io.micronaut.scheduling.annotation.Scheduled; +import jakarta.inject.Singleton; + +@Singleton +public class RateLimitCleanupTask { + + private final RateLimitFilter rateLimitFilter; + + public RateLimitCleanupTask(RateLimitFilter rateLimitFilter) { + this.rateLimitFilter = rateLimitFilter; + } + + @Scheduled(fixedDelay = "1h") + public void cleanupStaleBuckets() { + rateLimitFilter.removeStaleEntries(); + } +} diff --git a/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitConfiguration.java b/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitConfiguration.java new file mode 100644 index 00000000..22fd691c --- /dev/null +++ b/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitConfiguration.java @@ -0,0 +1,44 @@ +package edu.kit.cbc.editor.ratelimit; + +import io.micronaut.context.annotation.ConfigurationProperties; + +@ConfigurationProperties("rate-limit") +public class RateLimitConfiguration { + + private boolean enabled = true; + private int requestsPerMinute = 10; + private int requestsPerHour = 50; + private boolean trustForwardedHeaders = true; + + public boolean isEnabled() { + return enabled; + } + + public void setEnabled(boolean enabled) { + this.enabled = enabled; + } + + public int getRequestsPerMinute() { + return requestsPerMinute; + } + + public void setRequestsPerMinute(int requestsPerMinute) { + this.requestsPerMinute = requestsPerMinute; + } + + public int getRequestsPerHour() { + return requestsPerHour; + } + + public void setRequestsPerHour(int requestsPerHour) { + this.requestsPerHour = requestsPerHour; + } + + public boolean isTrustForwardedHeaders() { + return trustForwardedHeaders; + } + + public void setTrustForwardedHeaders(boolean trustForwardedHeaders) { + this.trustForwardedHeaders = trustForwardedHeaders; + } +} diff --git a/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitFilter.java b/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitFilter.java new file mode 100644 index 00000000..eb687443 --- /dev/null +++ b/backend/src/main/java/edu/kit/cbc/editor/ratelimit/RateLimitFilter.java @@ -0,0 +1,98 @@ +package edu.kit.cbc.editor.ratelimit; + +import io.github.bucket4j.Bandwidth; +import io.github.bucket4j.Bucket; +import io.github.bucket4j.ConsumptionProbe; +import io.micronaut.http.HttpRequest; +import io.micronaut.http.HttpResponse; +import io.micronaut.http.HttpStatus; +import io.micronaut.http.MediaType; +import io.micronaut.http.annotation.RequestFilter; +import io.micronaut.http.annotation.ServerFilter; +import java.time.Duration; +import java.util.Map; +import java.util.Optional; +import java.util.concurrent.ConcurrentHashMap; +import java.util.concurrent.TimeUnit; +import java.util.logging.Logger; + +@ServerFilter("/editor/askquestion") +public class RateLimitFilter { + + private static final Logger LOGGER = Logger.getGlobal(); + private final RateLimitConfiguration config; + private final ConcurrentHashMap buckets = new ConcurrentHashMap<>(); + private final ConcurrentHashMap lastAccess = new ConcurrentHashMap<>(); + + public RateLimitFilter(RateLimitConfiguration config) { + this.config = config; + } + + @RequestFilter + public Optional> filterRequest(HttpRequest request) { + if (!config.isEnabled()) { + return Optional.empty(); + } + + String clientIp = resolveClientIp(request); + lastAccess.put(clientIp, System.currentTimeMillis()); + Bucket bucket = buckets.computeIfAbsent(clientIp, ip -> createBucket()); + + ConsumptionProbe probe = bucket.tryConsumeAndReturnRemaining(1); + if (probe.isConsumed()) { + return Optional.empty(); + } + + long waitSeconds = TimeUnit.NANOSECONDS.toSeconds(probe.getNanosToWaitForRefill()) + 1; + LOGGER.warning(String.format("Rate limit exceeded for IP %s. Retry-After: %d seconds.", clientIp, waitSeconds)); + + return Optional.of( + HttpResponse.status(HttpStatus.TOO_MANY_REQUESTS) + .contentType(MediaType.APPLICATION_JSON) + .header("Retry-After", String.valueOf(waitSeconds)) + .body(Map.of( + "type", "about:blank", + "title", "Rate limit exceeded", + "status", 429, + "detail", "Too many requests. Please try again later.", + "instance", "about:blank" + )) + ); + } + + public void removeStaleEntries() { + long cutoff = System.currentTimeMillis() - Duration.ofHours(2).toMillis(); + lastAccess.entrySet().removeIf(entry -> { + if (entry.getValue() < cutoff) { + buckets.remove(entry.getKey()); + return true; + } + return false; + }); + } + + private String resolveClientIp(HttpRequest request) { + if (config.isTrustForwardedHeaders()) { + String forwarded = request.getHeaders().get("X-Forwarded-For"); + if (forwarded != null && !forwarded.isBlank()) { + return forwarded.split(",")[0].trim(); + } + } + return request.getRemoteAddress().getAddress().getHostAddress(); + } + + private Bucket createBucket() { + Bandwidth perMinute = Bandwidth.builder() + .capacity(config.getRequestsPerMinute()) + .refillIntervally(config.getRequestsPerMinute(), Duration.ofMinutes(1)) + .build(); + Bandwidth perHour = Bandwidth.builder() + .capacity(config.getRequestsPerHour()) + .refillIntervally(config.getRequestsPerHour(), Duration.ofHours(1)) + .build(); + return Bucket.builder() + .addLimit(perMinute) + .addLimit(perHour) + .build(); + } +} diff --git a/backend/src/main/resources/application.yml b/backend/src/main/resources/application.yml index 4b48ad50..e2314759 100644 --- a/backend/src/main/resources/application.yml +++ b/backend/src/main/resources/application.yml @@ -48,3 +48,9 @@ xai.accessToken: '${XAI_ACCESS_TOKEN:changeme}' google.accessToken: '${GOOGLE_ACCESS_TOKEN:changeme}' development: '${DEVELOPMENT:false}' + +rate-limit: + enabled: true + requests-per-minute: 10 + requests-per-hour: 50 + trust-forwarded-headers: true diff --git a/backend/src/test/resources/application-test.yml b/backend/src/test/resources/application-test.yml index 0545d60f..9af5b382 100644 --- a/backend/src/test/resources/application-test.yml +++ b/backend/src/test/resources/application-test.yml @@ -5,3 +5,6 @@ micronaut: test: resources: enabled: false + +rate-limit: + enabled: false diff --git a/frontend/src/app/components/ai-chat/ai-chat.component.css b/frontend/src/app/components/ai-chat/ai-chat.component.css index a834b4cd..cfb6523a 100644 --- a/frontend/src/app/components/ai-chat/ai-chat.component.css +++ b/frontend/src/app/components/ai-chat/ai-chat.component.css @@ -57,7 +57,6 @@ display: flex; flex-direction: column; height: 100%; - width: 400px; overflow: hidden; } diff --git a/frontend/src/app/components/ai-chat/ai-chat.component.html b/frontend/src/app/components/ai-chat/ai-chat.component.html index c7c5f0e0..a7db630b 100644 --- a/frontend/src/app/components/ai-chat/ai-chat.component.html +++ b/frontend/src/app/components/ai-chat/ai-chat.component.html @@ -27,7 +27,7 @@ -
+
@if (synthesisInProgress) {
Statements gets synthezied by AI.
@@ -54,27 +54,30 @@ }
- - - - - -
+ +
+
- + + +
+ + -
+
- + Actions @@ -36,16 +36,17 @@ - + -
+
diff --git a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.css b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.css index 4fc5ad73..182b44ee 100644 --- a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.css +++ b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.css @@ -1,35 +1,31 @@ .statements { - display: flex; - flex-direction: column; - width: 400px; overflow: visible; - .first-row { + .add-row { height: 3em; - display: grid; - place-items: center; color: #e0e0e0; } .statement-container { - height: 5em; display: flex; - flex-direction: row; - align-content: center; + height: 5em; + width: 100%; + gap: 10px; .guard { display: flex; - flex-grow: 3; - position: relative; height: 100%; + min-width: 0; + overflow: hidden; + column-wrap: nowrap; } .statement { align-content: center; - flex-grow: 1; - width: 100px; display: grid; place-items: center; + flex: 0; + overflow: hidden; } } -} \ No newline at end of file +} diff --git a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.html b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.html index ab77d447..93545d28 100644 --- a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.html +++ b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.html @@ -4,41 +4,35 @@ [refinement]="this" [hideSourceHandle]="true" > -
-
-
- - -
-
- +
@for (guard of _node.guards; track guard; let i = $index) {
-
- + + + +
+ @if (!_node.children[i]) { + + + } +
- @if (!_node.children[i]) { - - - }
} + +
diff --git a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.scss b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.scss deleted file mode 100644 index 4cc7d2cc..00000000 --- a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.scss +++ /dev/null @@ -1,36 +0,0 @@ -$refinementBoxAccentColor: rgb(87, 87, 87); -.statements { - display: flex; - flex-direction: column; - width: 400px; - overflow: visible; - - .first-row { - height: 3em; - display: grid; - place-items: center; - color: #e0e0e0; - } - - .statement-container { - height: 5em; - display: flex; - flex-direction: row; - align-content: center; - - .guard { - display: flex; - flex-grow: 3; - position: relative; - height: 100%; - } - - .statement { - align-content: center; - flex-grow: 1; - width: 100px; - display: grid; - place-items: center; - } - } -} \ No newline at end of file diff --git a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.ts b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.ts index e563e938..3fe1d4cb 100644 --- a/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.ts +++ b/frontend/src/app/components/editor/statements/selection-statement/selection-statement.component.ts @@ -19,6 +19,7 @@ import { import { Position } from "../../../../types/position"; import { SelectionStatementNode } from "../../../../types/statements/nodes/selection-statement-node"; import { HandleComponent } from "ngx-vflow"; +import {Button} from "primeng/button"; /** * Component in the graphical editor to represent the {@link SelectionStatement} @@ -37,6 +38,7 @@ import { HandleComponent } from "ngx-vflow"; MatButtonModule, ConditionEditorComponent, HandleComponent, + Button, ], templateUrl: "./selection-statement.component.html", styleUrl: "./selection-statement.component.css", @@ -74,12 +76,11 @@ export class SelectionStatementComponent extends Refinement implements OnInit { this._node.addSelection(); } - public removeSelection() { - const length = this._node.children.length; - if (this._node.children[length - 1]) { - this.treeService.deleteStatementNode(this._node.children[length - 1]!); + public removeSelection(index: number) { + if (this._node.children[index]) { + this.treeService.deleteStatementNode(this._node.children[index]!); } - this._node.removeSelection(); + this._node.removeSelectionAtIndex(index); } public override resetPosition(position: Position, offset: Position): void { diff --git a/frontend/src/app/services/tree/tree.service.ts b/frontend/src/app/services/tree/tree.service.ts index 0309cb23..3504972a 100644 --- a/frontend/src/app/services/tree/tree.service.ts +++ b/frontend/src/app/services/tree/tree.service.ts @@ -1,483 +1,503 @@ -import { Injectable, signal, Signal, WritableSignal } from "@angular/core"; -import { Subject } from "rxjs"; +import {Injectable, signal, Signal, WritableSignal} from "@angular/core"; +import {Subject} from "rxjs"; import { - AbstractStatement, - IAbstractStatement, - StatementType, + AbstractStatement, + IAbstractStatement, + StatementType, } from "../../types/statements/abstract-statement"; -import { JavaVariable, JavaVariableKind } from "../../types/JavaVariable"; -import { Renaming } from "../../types/Renaming"; -import { Condition } from "../../types/condition/condition"; -import { LocalCBCFormula } from "../../types/CBCFormula"; -import { ICompositionStatement } from "../../types/statements/composition-statement"; -import { IRepetitionStatement } from "../../types/statements/repetition-statement"; -import { ISelectionStatement } from "../../types/statements/selection-statement"; -import { AbstractStatementNode } from "../../types/statements/nodes/abstract-statement-node"; -import { statementNodeUtils } from "../../types/statements/nodes/statement-node-utils"; +import {JavaVariable, JavaVariableKind} from "../../types/JavaVariable"; +import {Renaming} from "../../types/Renaming"; +import {Condition} from "../../types/condition/condition"; +import {LocalCBCFormula} from "../../types/CBCFormula"; +import {ICompositionStatement} from "../../types/statements/composition-statement"; +import {IRepetitionStatement} from "../../types/statements/repetition-statement"; +import {ISelectionStatement} from "../../types/statements/selection-statement"; +import {AbstractStatementNode} from "../../types/statements/nodes/abstract-statement-node"; +import {statementNodeUtils} from "../../types/statements/nodes/statement-node-utils"; import { - IRootStatement, - RootStatement, + IRootStatement, + RootStatement, } from "../../types/statements/root-statement"; -import { RootStatementNode } from "../../types/statements/nodes/root-statement-node"; -import { RepetitionStatementNode } from "../../types/statements/nodes/repetition-statement-node"; +import {RootStatementNode} from "../../types/statements/nodes/root-statement-node"; +import {RepetitionStatementNode} from "../../types/statements/nodes/repetition-statement-node"; /** * Service for the context of the tree in the graphical editor. */ @Injectable({ - providedIn: "root", + providedIn: "root", }) export class TreeService { - private readonly _verifyNotifier: Subject; - private readonly _exportNotifier: Subject; - private readonly _resetVerifyNotifier: Subject; - private readonly _verificationResultNotifier: Subject; - private readonly _finalizeNotifier: Subject; - private _globalConditions: string[] = []; - private _renames: Renaming[] = []; - private _statementNodes: WritableSignal = signal([]); - private rootStatementNode: RootStatementNode | undefined; - private _urn = ""; - - public constructor() { - this._verificationResultNotifier = new Subject(); - this._verifyNotifier = new Subject(); - this._exportNotifier = new Subject(); - this._resetVerifyNotifier = new Subject(); - this._finalizeNotifier = new Subject(); - } - - setFormula(newFormula: LocalCBCFormula, urn: string) { - this._urn = urn; - this._rootFormula = newFormula; - this._variables = []; - this._renames = []; - this._globalConditions = []; - newFormula.javaVariables.forEach((variable) => { - this.addVariable(variable.name, variable.kind); - }); - if (newFormula.renamings) { - newFormula.renamings.forEach((renaming) => { - this.addRenaming(renaming.type, renaming.function, renaming.newName); - }); - } - newFormula.globalConditions.forEach((condition) => { - this.addGlobalCondition(condition.condition); - }); - - try { - this.generateStatementNodes(); - } catch (e) { - console.error( - "TreeService.setFormula: failed to initialize statement nodes", - e, - ); - } - } - - private _rootFormula: LocalCBCFormula | undefined; - - public get rootFormula() { - return this._rootFormula; - } - - private _variables: JavaVariable[] = []; - - public get variables(): string[] { - const variablesArray: string[] = []; - this._variables.forEach((javaVariable) => - variablesArray.push(javaVariable.toString()), - ); - return variablesArray; - } - - public get exportNotifier(): Subject { - return this._exportNotifier; - } - - public get urn() { - return this._urn; - } - - public get conditions(): Condition[] { - const conditionsArray: Condition[] = []; - this._globalConditions.forEach((condition) => - conditionsArray.push(new Condition(condition)), - ); - return conditionsArray; - } - - public get renaming(): Renaming[] { - const renames: Renaming[] = []; - this._renames.forEach((rename) => - renames.push(new Renaming(rename.type, rename.function, rename.newName)), - ); - return renames; - } - - public get verificationResultNotifier() { - return this._verificationResultNotifier; - } - - public get verifyNotifier() { - return this._verifyNotifier; - } - - public get resetVerifyNotifier() { - return this._resetVerifyNotifier; - } - - public get finalizeNotifier() { - return this._finalizeNotifier; - } - - public get rootStatement() { - return this.rootStatementNode; - } - - public export(): void { - this._exportNotifier.next(); - } - - public addVariable(name: string, kind: JavaVariableKind): boolean { - const sizeBeforeAdd = this._variables.length; - const newVariable = new JavaVariable(name, kind); - - let isDuplicate: boolean = false; - this._variables.forEach((val) => { - if (val.equalName(newVariable)) { - isDuplicate = true; - } - }); - - if (!isDuplicate) { - this._variables.push(newVariable); - } - - return this._variables.length != sizeBeforeAdd; - } - - public removeVariables(names: string[]): void { - const variablesToBeRemoved: string[] = []; - names.forEach((name) => { - const variableName = name.includes(" ") - ? name.split(" ").slice(1).join(" ") - : name; - variablesToBeRemoved.push(variableName); - }); - this._variables = this._variables.filter( - (val) => !variablesToBeRemoved.includes(val.name), - ); - } - - public removeAllVariables(): void { - this._variables = []; - } - - public addGlobalCondition(name: string): boolean { - const sizeBeforeAdd = this._globalConditions.length; - - let isDuplicate: boolean = false; - this._globalConditions.forEach((val) => { - if (val == name) { - isDuplicate = true; - } - }); - - if (!isDuplicate) { - this._globalConditions.push(name); - } - - return this._globalConditions.length != sizeBeforeAdd; - } - - public removeGlobalCondition(name: string): void { - this._globalConditions = this._globalConditions.filter( - (val) => val !== name, - ); - } - - public statements(): IAbstractStatement[] { - const statements: IAbstractStatement[] = []; - if (this.rootFormula && this.rootFormula.statement) { - this.collectStatements(this.rootFormula.statement, statements); - } - return statements; - } - - public getStatementsFromFormula( - formula: LocalCBCFormula, - ): IAbstractStatement[] { - const statements: IAbstractStatement[] = []; - if (formula && formula.statement) { - this.collectStatements(formula.statement, statements); - } - return statements; - } - - public refreshNodes(): void { - this._statementNodes.update((old) => [...old]); - } - - public addStatementNode(statementNode: AbstractStatementNode) { - if (this._statementNodes()) { - this._statementNodes.update((oldNodes) => [...oldNodes, statementNode]); - } else { - this._statementNodes.set([statementNode]); - } - } - - public createNodeForStatement( - parent: AbstractStatementNode, - statementType: StatementType, - index?: number, - ): AbstractStatementNode { - const child = parent.createChild(statementType, index); - this.addStatementNode(child); - return child; - } - - public deleteStatementNode(statementNode: AbstractStatementNode) { - if (statementNode.statement.type === "ROOT") { - return; - } - if (this._statementNodes().includes(statementNode)) { - if (statementNode.statement.type === "REPETITION") { - (statementNode as RepetitionStatementNode).destroy(); - } - statementNode.parent?.deleteChild(statementNode); - this._statementNodes.update((old) => - old.filter((node) => node != statementNode), - ); - } - } - - public generateStatementNodes(): Signal { - const rootStatementNode = this.rootFormula?.statement - ? new RootStatementNode( - this.rootFormula.statement as RootStatement, - undefined, - ) - : statementNodeUtils( - new RootStatement( - "", - new Condition(""), - new Condition(""), - undefined, - ), + private readonly _verifyNotifier: Subject; + private readonly _exportNotifier: Subject; + private readonly _resetVerifyNotifier: Subject; + private readonly _verificationResultNotifier: Subject; + private readonly _finalizeNotifier: Subject; + private _globalConditions: string[] = []; + private _renames: Renaming[] = []; + private _statementNodes: WritableSignal = signal([]); + private rootStatementNode: RootStatementNode | undefined; + private _urn = ""; + + public constructor() { + this._verificationResultNotifier = new Subject(); + this._verifyNotifier = new Subject(); + this._exportNotifier = new Subject(); + this._resetVerifyNotifier = new Subject(); + this._finalizeNotifier = new Subject(); + } + + setFormula(newFormula: LocalCBCFormula, urn: string) { + this._urn = urn; + this._rootFormula = newFormula; + this._variables = []; + this._renames = []; + this._globalConditions = []; + newFormula.javaVariables.forEach((variable) => { + this.addVariable(variable.name, variable.kind); + }); + if (newFormula.renamings) { + newFormula.renamings.forEach((renaming) => { + this.addRenaming(renaming.type, renaming.function, renaming.newName); + }); + } + newFormula.globalConditions.forEach((condition) => { + this.addGlobalCondition(condition.condition); + }); + + try { + this.generateStatementNodes(); + } catch (e) { + console.error( + "TreeService.setFormula: failed to initialize statement nodes", + e, + ); + } + } + + private _rootFormula: LocalCBCFormula | undefined; + + public get rootFormula() { + return this._rootFormula; + } + + private _variables: JavaVariable[] = []; + + public get variables(): string[] { + const variablesArray: string[] = []; + this._variables.forEach((javaVariable) => + variablesArray.push(javaVariable.toString()), + ); + return variablesArray; + } + + public get exportNotifier(): Subject { + return this._exportNotifier; + } + + public get urn() { + return this._urn; + } + + public get conditions(): Condition[] { + const conditionsArray: Condition[] = []; + this._globalConditions.forEach((condition) => + conditionsArray.push(new Condition(condition)), + ); + return conditionsArray; + } + + public get renaming(): Renaming[] { + const renames: Renaming[] = []; + this._renames.forEach((rename) => + renames.push(new Renaming(rename.type, rename.function, rename.newName)), + ); + return renames; + } + + public get verificationResultNotifier() { + return this._verificationResultNotifier; + } + + public get verifyNotifier() { + return this._verifyNotifier; + } + + public get resetVerifyNotifier() { + return this._resetVerifyNotifier; + } + + public get finalizeNotifier() { + return this._finalizeNotifier; + } + + public get rootStatement() { + return this.rootStatementNode; + } + + public export(): void { + this._exportNotifier.next(); + } + + public addVariable(name: string, kind: JavaVariableKind): boolean { + const sizeBeforeAdd = this._variables.length; + const newVariable = new JavaVariable(name, kind); + + let isDuplicate: boolean = false; + this._variables.forEach((val) => { + if (val.equalName(newVariable)) { + isDuplicate = true; + } + }); + + if (!isDuplicate) { + this._variables.push(newVariable); + } + + return this._variables.length != sizeBeforeAdd; + } + + public removeVariables(names: string[]): void { + const variablesToBeRemoved: string[] = []; + names.forEach((name) => { + const variableName = name.includes(" ") + ? name.split(" ").slice(1).join(" ") + : name; + variablesToBeRemoved.push(variableName); + }); + this._variables = this._variables.filter( + (val) => !variablesToBeRemoved.includes(val.name), ); - if (this._rootFormula) { - this._rootFormula.statement = - rootStatementNode.statement as IRootStatement; - } - this._statementNodes.set( - [rootStatementNode].concat( - this.collectStatementNodeChildren([rootStatementNode]), - ), - ); - this.rootStatementNode = rootStatementNode as RootStatementNode; - return this._statementNodes; - } - - public addRenaming(type: string, original: string, newName: string): void { - this._renames.push(new Renaming(type, original, newName)); - } - - public removeRenaming(type: string, original: string, newName: string): void { - this._renames = this._renames.filter( - (val) => !val.equal(new Renaming(type, original, newName)), - ); - } - - private collectStatementNodeChildren( - parentNodes: (AbstractStatementNode | undefined)[], - ): AbstractStatementNode[] { - let childNodes: AbstractStatementNode[] = []; - for (const parentNode of parentNodes) { - if (parentNode) { - childNodes = childNodes - .concat(parentNode.children.filter((child) => child != undefined) as AbstractStatementNode[]) - .concat(this.collectStatementNodeChildren(parentNode.children)); - } - } - return childNodes; - } - - private collectStatements( - statement: IAbstractStatement | undefined, - statements: IAbstractStatement[], - ) { - if (statement && statements) { - switch (statement.type) { - case "STATEMENT": - statements.push(statement); - return; - case "COMPOSITION": - statements.push(statement); - this.collectStatements( - (statement as ICompositionStatement).firstStatement, - statements, - ); - this.collectStatements( - (statement as ICompositionStatement).secondStatement, - statements, - ); - return; - case "REPETITION": - statements.push(statement); - this.collectStatements( - (statement as IRepetitionStatement).loopStatement, - statements, - ); - return; - case "RETURN": - statements.push(statement); - return; - case "SKIP": - statements.push(statement); - return; - case "SELECTION": - statements.push(statement); - (statement as ISelectionStatement).commands.forEach((command) => - this.collectStatements(command, statements), - ); - return; - case "ROOT": - statements.push(statement); - this.collectStatements( - (statement as IRootStatement).statement, - statements, - ); - } - } - } - - finalizeStatements() { - this.rootStatementNode?.finalize(); - if (this.rootFormula) { - this.rootFormula.javaVariables = this._variables; - this.rootFormula.renamings = this._renames; - this.rootFormula.globalConditions = this._globalConditions.map( - (condition) => new Condition(condition), - ); - } - this.finalizeNotifier.next() - } - - public findStatementNodeById(id: string): AbstractStatementNode | undefined { - const nodes = this._statementNodes(); - for (const node of nodes) { - if (node.statement.id === id) { - return node; - } - const found = this.findNodeInSubtree(node, id); - if (found) { - return found; - } - } - return undefined; - } - - private findNodeInSubtree( - node: AbstractStatementNode, - id: string, - ): AbstractStatementNode | undefined { - for (const child of node.children) { - if (child) { - if (child.statement.id === id) { - return child; + } + + public removeAllVariables(): void { + this._variables = []; + } + + public addGlobalCondition(name: string): boolean { + const sizeBeforeAdd = this._globalConditions.length; + + let isDuplicate: boolean = false; + this._globalConditions.forEach((val) => { + if (val == name) { + isDuplicate = true; + } + }); + + if (!isDuplicate) { + this._globalConditions.push(name); } - const found = this.findNodeInSubtree(child, id); - if (found) { - return found; + + return this._globalConditions.length != sizeBeforeAdd; + } + + public removeGlobalCondition(name: string): void { + this._globalConditions = this._globalConditions.filter( + (val) => val !== name, + ); + } + + public statements(): IAbstractStatement[] { + const statements: IAbstractStatement[] = []; + if (this.rootFormula && this.rootFormula.statement) { + this.collectStatements(this.rootFormula.statement, statements); } - } - } - return undefined; - } - - public collectSubtreeNodes( - node: AbstractStatementNode, - ): AbstractStatementNode[] { - const nodes: AbstractStatementNode[] = [node]; - for (const child of node.children) { - if (child) { - nodes.push(...this.collectSubtreeNodes(child)); - } - } - return nodes; - } - - public markSubtreeUnverified(node: AbstractStatementNode): void { - const subtreeNodes = this.collectSubtreeNodes(node); - subtreeNodes.forEach((subtreeNode) => { - subtreeNode.statement.isProven = false; - subtreeNode.statement.nodeState = 'unverified' - }); - if (this.rootFormula) { - this.rootFormula.isProven = false; - } - this.refreshNodes(); - } - - public markWholeTreeUnverified(): void { - if (!this.rootStatementNode) { - return; - } - this.markSubtreeUnverified(this.rootStatementNode); - } - - public createTempFormulaFromNode( - node: AbstractStatementNode, - ): LocalCBCFormula { - node.finalize(); - - let rootStatement: IRootStatement; - - if (node.statement.type === "ROOT") { - rootStatement = node.statement as IRootStatement; - } else { - rootStatement = new RootStatement( - node.statement.name || "temp", - node.statement.preCondition, - node.statement.postCondition, - node.statement, - ); - } - - const tempFormula = new LocalCBCFormula( - node.statement.name || "temp", - rootStatement, - this.rootFormula?.javaVariables || [], - this.rootFormula?.globalConditions || [], - this.rootFormula?.renamings || null, - false, - ); - - return tempFormula; - } - - public dump() { - return { - rootStatementNode: JSON.stringify( - this.rootStatementNode, - (key, value) => { - if (key == "parent") { - return undefined; - } - return value; - }, - ), - rootFormula: this.rootFormula, - statementNodes: JSON.stringify(this._statementNodes(), (key, value) => { - if (key == "parent") { - return undefined; + return statements; + } + + public getStatementsFromFormula( + formula: LocalCBCFormula, + ): IAbstractStatement[] { + const statements: IAbstractStatement[] = []; + if (formula && formula.statement) { + this.collectStatements(formula.statement, statements); } - return value; - }), - variables: this._variables, - globalConditions: this._globalConditions, - renames: this._renames, - }; - } + return statements; + } + + public refreshNodes(): void { + this._statementNodes.update((old) => [...old]); + } + + public addStatementNode(statementNode: AbstractStatementNode) { + if (this._statementNodes()) { + this._statementNodes.update((oldNodes) => [...oldNodes, statementNode]); + } else { + this._statementNodes.set([statementNode]); + } + } + + public createNodeForStatement( + parent: AbstractStatementNode, + statementType: StatementType, + index?: number, + ): AbstractStatementNode { + const child = parent.createChild(statementType, index); + this.addStatementNode(child); + return child; + } + + public deleteStatementNode(statementNode: AbstractStatementNode) { + if (statementNode.statement.type === "ROOT") { + return; + } + if (this._statementNodes().includes(statementNode)) { + if (statementNode.statement.type === "REPETITION") { + (statementNode as RepetitionStatementNode).destroy(); + } + statementNode.parent?.deleteChild(statementNode); + this._statementNodes.update((old) => + old.filter((node) => node != statementNode), + ); + } + } + + public generateStatementNodes(): Signal { + const rootStatementNode = this.rootFormula?.statement + ? new RootStatementNode( + this.rootFormula.statement as RootStatement, + undefined, + ) + : statementNodeUtils( + new RootStatement( + "", + new Condition(""), + new Condition(""), + undefined, + ), + ); + if (this._rootFormula) { + this._rootFormula.statement = + rootStatementNode.statement as IRootStatement; + } + this._statementNodes.set( + [rootStatementNode].concat( + this.collectStatementNodeChildren([rootStatementNode]), + ), + ); + this.rootStatementNode = rootStatementNode as RootStatementNode; + return this._statementNodes; + } + + public addRenaming(type: string, original: string, newName: string): void { + this._renames.push(new Renaming(type, original, newName)); + } + + public removeRenaming(type: string, original: string, newName: string): void { + this._renames = this._renames.filter( + (val) => !val.equal(new Renaming(type, original, newName)), + ); + } + + private collectStatementNodeChildren( + parentNodes: (AbstractStatementNode | undefined)[], + ): AbstractStatementNode[] { + let childNodes: AbstractStatementNode[] = []; + for (const parentNode of parentNodes) { + if (parentNode) { + childNodes = childNodes + .concat(parentNode.children.filter((child) => child != undefined) as AbstractStatementNode[]) + .concat(this.collectStatementNodeChildren(parentNode.children)); + } + } + return childNodes; + } + + private collectStatements( + statement: IAbstractStatement | undefined, + statements: IAbstractStatement[], + ) { + if (statement && statements) { + switch (statement.type) { + case "STATEMENT": + statements.push(statement); + return; + case "COMPOSITION": + statements.push(statement); + this.collectStatements( + (statement as ICompositionStatement).firstStatement, + statements, + ); + this.collectStatements( + (statement as ICompositionStatement).secondStatement, + statements, + ); + return; + case "REPETITION": + statements.push(statement); + this.collectStatements( + (statement as IRepetitionStatement).loopStatement, + statements, + ); + return; + case "RETURN": + statements.push(statement); + return; + case "SKIP": + statements.push(statement); + return; + case "SELECTION": + statements.push(statement); + (statement as ISelectionStatement).commands.forEach((command) => + this.collectStatements(command, statements), + ); + return; + case "ROOT": + statements.push(statement); + this.collectStatements( + (statement as IRootStatement).statement, + statements, + ); + } + } + } + + finalizeStatements() { + this.rootStatementNode?.finalize(); + if (this.rootFormula) { + this.rootFormula.javaVariables = this._variables; + this.rootFormula.renamings = this._renames; + this.rootFormula.globalConditions = this._globalConditions.map( + (condition) => new Condition(condition), + ); + } + this.finalizeNotifier.next() + } + + public findStatementNodeById(id: string): AbstractStatementNode | undefined { + const nodes = this._statementNodes(); + for (const node of nodes) { + if (node.statement.id === id) { + return node; + } + const found = this.findNodeInSubtree(node, id); + if (found) { + return found; + } + } + return undefined; + } + + private findNodeInSubtree( + node: AbstractStatementNode, + id: string, + ): AbstractStatementNode | undefined { + for (const child of node.children) { + if (child) { + if (child.statement.id === id) { + return child; + } + const found = this.findNodeInSubtree(child, id); + if (found) { + return found; + } + } + } + return undefined; + } + + public collectSubtreeNodes( + node: AbstractStatementNode, + ): AbstractStatementNode[] { + const nodes: AbstractStatementNode[] = []; + for (const child of node.children) { + if (child) { + nodes.push(...this.collectSubtreeNodes(child)); + } + } + return nodes; + } + + public collectAncestorNodes( + node: AbstractStatementNode, + ): AbstractStatementNode[] { + const ancestors: AbstractStatementNode[] = []; + let currentNode: AbstractStatementNode | undefined = node.parent; + while (currentNode) { + ancestors.push(currentNode); + currentNode = currentNode.parent; + } + return ancestors; + } + + public markSubtreeUnverified(node: AbstractStatementNode): void { + const subtreeNodes = this.collectSubtreeNodes(node); + const ancestorNodes = this.collectAncestorNodes(node); + subtreeNodes.forEach((subtreeNode) => { + subtreeNode.statement.isProven = false; + subtreeNode.statement.nodeState = 'unverified' + }); + ancestorNodes.forEach((ancestorNode) => { + ancestorNode.statement.isProven = false; + ancestorNode.statement.nodeState = 'unverified'; + }) + node.statement.isProven = false; + node.statement.nodeState = 'unverified'; + + if (this.rootFormula) { + this.rootFormula.isProven = false; + } + this.refreshNodes(); + } + + public markWholeTreeUnverified(): void { + if (!this.rootStatementNode) { + return; + } + this.markSubtreeUnverified(this.rootStatementNode); + } + + public createTempFormulaFromNode( + node: AbstractStatementNode, + ): LocalCBCFormula { + node.finalize(); + + let rootStatement: IRootStatement; + + if (node.statement.type === "ROOT") { + rootStatement = node.statement as IRootStatement; + } else { + rootStatement = new RootStatement( + node.statement.name || "temp", + node.statement.preCondition, + node.statement.postCondition, + node.statement, + ); + } + + const tempFormula = new LocalCBCFormula( + node.statement.name || "temp", + rootStatement, + this.rootFormula?.javaVariables || [], + this.rootFormula?.globalConditions || [], + this.rootFormula?.renamings || null, + false, + ); + + return tempFormula; + } + + public dump() { + return { + rootStatementNode: JSON.stringify( + this.rootStatementNode, + (key, value) => { + if (key == "parent") { + return undefined; + } + return value; + }, + ), + rootFormula: this.rootFormula, + statementNodes: JSON.stringify(this._statementNodes(), (key, value) => { + if (key == "parent") { + return undefined; + } + return value; + }), + variables: this._variables, + globalConditions: this._globalConditions, + renames: this._renames, + }; + } } diff --git a/frontend/src/app/types/statements/nodes/selection-statement-node.ts b/frontend/src/app/types/statements/nodes/selection-statement-node.ts index 1cc3bb8c..adbe7d89 100644 --- a/frontend/src/app/types/statements/nodes/selection-statement-node.ts +++ b/frontend/src/app/types/statements/nodes/selection-statement-node.ts @@ -188,16 +188,15 @@ export class SelectionStatementNode extends AbstractStatementNode { return statementNode; } - removeSelection() { - const index = this.guards.length - 1; + removeSelectionAtIndex(index: number) { if (this.childSubscriptions[index]) { this.childSubscriptions[index].unsubscribe(); - this.childSubscriptions.pop(); + this.childSubscriptions.splice(index, 1); } - this.guards.pop(); - this.children.pop(); - this.statement.guards.pop(); - this.statement.commands.pop(); + this.guards.splice(index, 1); + this.children.splice(index, 1); + this.statement.guards.splice(index, 1); + this.statement.commands.splice(index, 1); } override addChild(statement: AbstractStatementNode, index: number) {