Merge branch 'main' into context-history

Author: rcosta358

.github/workflows/maven.yml

@@ -48,7 +48,7 @@ jobs:
 
       # Build the project (compiles and packages the code)
       - name: Build the project
-        run: mvn -B clean install --file pom.xml --batch-mode --fail-fast -Dgpg.skip=true -Dmaven.deploy.skip=true
+        run: mvn -B clean install -DskipTests --file pom.xml --batch-mode --fail-fast -Dgpg.skip=true -Dmaven.deploy.skip=true
 
       # Run tests
       - name: Run tests

liquidjava-example/src/main/java/testSuite/CorrectChars.java

@@ -0,0 +1,36 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class CorrectChars {
+
+    @Refinement("_ == 65")
+    int getA() {
+        return 'A';
+    }
+
+    void test() {
+        printLetter('A');
+        printLetter('Z');
+        printLetter('a');
+        printLetter('z');
+    }
+
+    void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) {
+        System.out.println(c);
+    }
+
+    void test2() {
+        @Refinement("_ == 97")
+        char c = 'a';
+        
+        @Refinement("_ == 98")
+        int res = inc(c);
+    }
+
+    @Refinement("_ == x + 1")
+    int inc(int x) {
+        return x + 1;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorChars.java

@@ -0,0 +1,15 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorChars {
+
+    void test() {
+        printLetter('$'); // error
+    }
+
+    void printLetter(@Refinement("_ >= 65 && _ <= 90 || _ >= 97 && _ <= 122") char c) {
+        System.out.println(c);
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinement.java

@@ -0,0 +1,13 @@
+// Invalid Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorInvalidRefinement {
+
+    void test() {
+        @Refinement("x")
+        int x = 0;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementParameter.java

@@ -0,0 +1,13 @@
+// Invalid Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorInvalidRefinementParameter {
+
+    void testInvalidRefinement(@Refinement("y + 1") int y) {}
+
+    int otherMethod() {
+        return -1;
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorInvalidRefinementReturn.java

@@ -0,0 +1,11 @@
+// Invalid Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorInvalidRefinementReturn {
+
+    @Refinement("_ * 2")
+    void test() {
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java

@@ -108,26 +108,34 @@ public String getSnippet() {
 
             for (int i = startLine; i <= endLine; i++) {
                 String lineNumStr = String.format("%" + padding + "d", i);
-                String line = lines.get(i - 1);
+                String rawLine = lines.get(i - 1);
+                String line = rawLine.replace("\t", "    ");
 
                 // add line
                 sb.append(Colors.GREY).append(lineNumStr).append(PIPE).append(line).append(Colors.RESET).append("\n");
 
                 // add error markers on the line(s) with the error
                 if (i >= position.lineStart() && i <= position.lineEnd()) {
                     int colStart = (i == position.lineStart()) ? position.colStart() : 1;
-                    int colEnd = (i == position.lineEnd()) ? position.colEnd() : line.length();
+                    int colEnd = (i == position.lineEnd()) ? position.colEnd() : rawLine.length();
 
                     if (colStart > 0 && colEnd > 0) {
+                        int tabsBeforeStart = (int) rawLine.substring(0, Math.max(0, colStart - 1)).chars()
+                                .filter(ch -> ch == '\t').count();
+                        int tabsBeforeEnd = (int) rawLine.substring(0, Math.max(0, colEnd)).chars()
+                                .filter(ch -> ch == '\t').count();
+                        int visualColStart = colStart + tabsBeforeStart * 3;
+                        int visualColEnd = colEnd + tabsBeforeEnd * 3;
+
                         // line number padding + pipe + column offset
                         String indent = " ".repeat(padding) + Colors.GREY + PIPE + Colors.RESET
-                                + " ".repeat(colStart - 1);
-                        String markers = accentColor + "^".repeat(Math.max(1, colEnd - colStart + 1));
+                            + " ".repeat(visualColStart - 1);
+                        String markers = accentColor + "^".repeat(Math.max(1, visualColEnd - visualColStart + 1));
                         sb.append(indent).append(markers);
 
                         // custom message
                         if (customMessage != null && !customMessage.isBlank()) {
-                            String offset = " ".repeat(padding + colEnd + PIPE.length() + 1);
+                            String offset = " ".repeat(padding + visualColEnd + PIPE.length() + 1);
                             sb.append(" " + customMessage.replace("\n", "\n" + offset));
                         }
                         sb.append(Colors.RESET).append("\n");

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/InvalidRefinementError.java

@@ -12,7 +12,7 @@ public class InvalidRefinementError extends LJError {
     private final String refinement;
 
     public InvalidRefinementError(SourcePosition position, String message, String refinement) {
-        super("Invalid Refinement", message, position, null);
+        super("Invalid Refinement Error", message, position, null);
         this.refinement = refinement;
     }
 

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -1,8 +1,8 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+import liquidjava.smt.Counterexample;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -14,13 +14,39 @@ public class RefinementError extends LJError {
 
     private final ValDerivationNode expected;
     private final ValDerivationNode found;
+    private final Counterexample counterexample;
 
     public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
-            TranslationTable translationTable, String customMessage) {
+            TranslationTable translationTable, Counterexample counterexample, String customMessage) {
         super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue(), expected.getValue()),
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
+        this.counterexample = counterexample;
+    }
+
+    @Override
+    public String getDetails() {
+        return getCounterexampleString();
+    }
+
+    private String getCounterexampleString() {
+        if (counterexample == null || counterexample.assignments().isEmpty())
+            return "";
+
+        // filter fresh variables and join assignements with &&
+        String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_"))
+                .reduce((a, b) -> a + " && " + b).orElse("");
+
+        // check if counterexample is trivial (same as the found value)
+        if (counterexampleExp.equals(found.getValue().toString()))
+            return "";
+
+        return "Counterexample: " + counterexampleExp;
+    }
+
+    public Counterexample getCounterexample() {
+        return counterexample;
     }
 
     public ValDerivationNode getExpected() {

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java

@@ -96,16 +96,24 @@ public <T> void visitCtInterface(CtInterface<T> intrface) {
     @Override
     public <T> void visitCtConstructor(CtConstructor<T> c) {
         context.enterContext();
-        getRefinementFromAnnotation(c);
-        mfc.getConstructorRefinements(c);
-        super.visitCtConstructor(c);
+        try {
+            getRefinementFromAnnotation(c);
+            mfc.getConstructorRefinements(c);
+            super.visitCtConstructor(c);
+        } catch (LJError e) {
+            diagnostics.add(e);
+        }
         context.exitContext();
     }
 
     public <R> void visitCtMethod(CtMethod<R> method) {
         context.enterContext();
-        mfc.getMethodRefinements(method);
-        super.visitCtMethod(method);
+        try {
+            mfc.getMethodRefinements(method);
+            super.visitCtMethod(method);
+        } catch (LJError e) {
+            diagnostics.add(e);
+        }
         context.exitContext();
     }
 }