Fix/verify behaviour

backend/pom.xml

@@ -127,14 +127,19 @@
         <dependency>
             <groupId>org.key-project</groupId>
             <artifactId>key.core</artifactId>
-            <version>2.12.2</version>
+            <version>3.0.0</version>
         </dependency>
         <dependency>
             <groupId>org.projectlombok</groupId>
             <artifactId>lombok</artifactId>
             <version>1.18.38</version>
             <scope>provided</scope>
         </dependency>
+        <dependency>
+            <groupId>com.bucket4j</groupId>
+            <artifactId>bucket4j_jdk17-core</artifactId>
+            <version>8.14.0</version>
+        </dependency>
     </dependencies>
     <build>
         <pluginManagement>

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 <a href="https://github.com/KeYProject/key-java-example">here</a>.
- * 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();
             }

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;
     }
 }

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;
     }
 }

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<ConversionErrorException, HttpResponse<?>> {
+
+    @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 extends Throwable> T findCause(Throwable ex, Class<T> type) {
+        Throwable t = ex;
+        while (t != null) {
+            if (type.isInstance(t)) {
+                return (T) t;
+            }
+            t = t.getCause();
+        }
+        return null;
+    }
+}

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<ErrorDetail> 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)
+        );
+    }
+}

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<LLMQueryInput> input,
+        @NotNull @Valid @Size(min = 1, max = 50) List<LLMQueryInput> input,
         @NotBlank String model,
         @NotNull LLMProvider provider
 ) {

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();
+    }
+}

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;
+    }
+}