Merge pull request #78 from OpenVADL/feature/typechecker-improved-branching

typechecker: Implement new semantics for constant branches

Author: flofriday

vadl-cli/main/vadl/cli/BaseCommand.java

@@ -49,6 +49,7 @@
 import vadl.pass.PassManager;
 import vadl.pass.PassOrder;
 import vadl.pass.exception.DuplicatedPassKeyException;
+import vadl.utils.EditorUtils;
 import vadl.utils.SourceLocation;
 import vadl.viam.Specification;
 
@@ -211,6 +212,37 @@ private Specification parseToVIAM() {
     return spec;
   }
 
+  protected void printDumps(String message) {
+    if (ArtifactTracker.getDumpPaths().isEmpty()) {
+      return;
+    }
+
+    System.out.println(message);
+    for (var path : ArtifactTracker.getDumpPaths()) {
+      if (EditorUtils.isIntelliJIDE()) {
+        var uri = path.toAbsolutePath().toUri();
+        System.out.printf("\t- %s\n", uri);
+      } else {
+        System.out.printf("\t- %s\n", path);
+      }
+    }
+  }
+
+  protected void printArtifacts(String message) {
+    if (ArtifactTracker.getArtifactPathsPaths().isEmpty()) {
+      return;
+    }
+    System.out.println(message);
+    for (var path : ArtifactTracker.getArtifactPathsPaths()) {
+      if (EditorUtils.isIntelliJIDE()) {
+        var uri = path.toAbsolutePath().toUri();
+        System.out.printf("\t- %s\n", uri);
+      } else {
+        System.out.printf("\t- %s\n", path);
+      }
+    }
+  }
+
   // lazy evaluated config, do NOT use this directly.
   // use getConfig() instead.
   @Nullable
@@ -263,17 +295,10 @@ public Integer call() {
                                    🔥 The vadl compiler crashed 🔥  \s
           
           This shouldn't have happened, please open an issue with the stacktrace below at:
-          https://ea.complang.tuwien.ac.at/vadl/open-vadl/issues/new
+          https://github.com/OpenVADL/open-vadl/issues/new
           """);
 
-      if (!ArtifactTracker.getDumpPaths().isEmpty()) {
-        var dumpMessage = "\nBefore the crash, the following dumps were generated:";
-        System.out.println(dumpMessage);
-        for (var path : ArtifactTracker.getDumpPaths()) {
-          System.out.printf("\t- %s\n", path);
-        }
-        System.out.println("");
-      }
+      printDumps("\nBefore the crash, the following dumps were generated:");
 
       // Dirty hack to avoid stdout and stderr getting mixed in IntelliJ (flushing wasn't enough).
       try {
@@ -296,25 +321,13 @@ public Integer call() {
       }
     }
 
-    if (!ArtifactTracker.getArtifactPathsPaths().isEmpty()) {
-      var artifactMessage = returnVal == 0
-          ? "\nThe following artifacts were generated:"
-          : "\nEven though some errors occurred, the following artifacts were generated:";
-      System.out.println(artifactMessage);
-      for (var path : ArtifactTracker.getArtifactPathsPaths()) {
-        System.out.printf("\t- %s\n", path);
-      }
-    }
+    printArtifacts(returnVal == 0
+        ? "\nThe following artifacts were generated:"
+        : "\nEven though some errors occurred, the following artifacts were generated:");
 
-    if (!ArtifactTracker.getDumpPaths().isEmpty()) {
-      var dumpMessage = returnVal == 0
-          ? "\nThe following dumps were generated:"
-          : "\nEven though some errors occurred, the following dumps were generated:";
-      System.out.println(dumpMessage);
-      for (var path : ArtifactTracker.getDumpPaths()) {
-        System.out.printf("\t- %s\n", path);
-      }
-    }
+    printDumps(returnVal == 0
+        ? "\nThe following dumps were generated:"
+        : "\nEven though some errors occurred, the following dumps were generated:");
 
     return returnVal;
   }

vadl/main/vadl/ast/ConstantType.java

@@ -35,6 +35,10 @@ public ConstantType(BigInteger value) {
     this.value = value;
   }
 
+  public ConstantType(long value) {
+    this.value = BigInteger.valueOf(value);
+  }
+
   BigInteger getValue() {
     return value;
   }

vadl/main/vadl/ast/TypeChecker.java

@@ -30,6 +30,7 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+import java.util.function.Supplier;
 import javax.annotation.Nullable;
 import vadl.error.Diagnostic;
 import vadl.types.BitsType;
@@ -58,9 +59,24 @@
 public class TypeChecker
     implements DefinitionVisitor<Void>, StatementVisitor<Void>, ExprVisitor<Void> {
 
+  private BranchStrategy branchStrategy = BranchStrategy.ALL;
+
+  /**
+   * Describes whether all branches are checked and the result of all branches must be equal, or
+   * if we must evaluate the condition and propergate the type from the chosen branch.
+   */
+  enum BranchStrategy {
+    ALL,
+    ONE,
+  }
+
   //private final List<Diagnostic> errors = new ArrayList<>();
   private final ConstantEvaluator constantEvaluator;
 
+  /**
+   * There is no point in checking a statement or definition twice, so these sets record which
+   * nodes we already visited. For expressions, we can simply check if the type is set.
+   */
   private final Set<Statement> checkedStatements =
       Collections.newSetFromMap(new IdentityHashMap<>());
   private final Set<Definition> checkedDefinitions =
@@ -149,6 +165,23 @@ private void throwInvalidAsmCast(AsmType from, AsmType to, WithSourceLocation lo
         .build();
   }
 
+  /**
+   * Execute the operation with the specified strategy set, and reset it afterwards again.
+   *
+   * @param strategy  to be active during the execution of the operation
+   * @param operation to be executed
+   * @return the result of the operation
+   */
+  private <T> T withBranchingStrategy(BranchStrategy strategy, Supplier<T> operation) {
+    var oldStrategy = branchStrategy;
+    try {
+      branchStrategy = strategy;
+      return operation.get();
+    } finally {
+      branchStrategy = oldStrategy;
+    }
+  }
+
   /**
    * Tests whether a type can implicitly be cast to another.
    *
@@ -252,7 +285,7 @@ private static Expr wrapImplicitCast(Expr inner, Type to) {
     }
 
     if (!canImplicitCast(innerType, to)) {
-      if (!(innerType instanceof ConstantType innerConstTyp)) {
+      if (!(innerType instanceof ConstantType innerConstTyp) || to instanceof ConstantType) {
         return inner;
       }
 
@@ -311,7 +344,7 @@ private static BuiltInTable.BuiltIn getBuiltIn(String name, List<Type> argTypes)
 
   @Override
   public Void visit(ConstantDefinition definition) {
-    Type valType = check(definition.value);
+    Type valType = withBranchingStrategy(BranchStrategy.ONE, () -> check(definition.value));
 
     if (definition.typeLiteral == null) {
       // Do nothing on purpose
@@ -644,10 +677,10 @@ public Void visit(EnumerationDefinition definition) {
           .build();
     }
 
-
     int nextVal = 0;
     for (var entry : definition.entries) {
       if (entry.value != null) {
+        check(entry.value);
         nextVal = constantEvaluator.eval(entry.value).value().intValueExact() + 1;
         continue;
       }
@@ -2526,6 +2559,25 @@ public Void visit(IfExpr expr) {
     var thenType = check(expr.thenExpr);
     var elseType = check(expr.elseExpr);
 
+    // If only one branch should be checked, directly propergate the type, and don't check whether
+    // the branches are compatible.
+    // This is intended: https://github.com/OpenVADL/open-vadl/issues/47#issuecomment-2725475475
+    if (branchStrategy.equals(BranchStrategy.ONE)) {
+      var condVal = constantEvaluator.eval(expr.condition).value().intValueExact();
+      expr.type = condVal == 1 ? thenType : elseType;
+      return null;
+    }
+
+    // FIXME: Fix this with bidirectional checking in the future
+    if (thenType instanceof ConstantType && elseType instanceof ConstantType
+        && !thenType.equals(elseType)) {
+      throw Diagnostic.error("Type Mismatch", expr)
+          .description("Both branches return different constant types.")
+          .help("Add an explicit cast on one of the branches.")
+          .note("In the future this will work without a cast.")
+          .build();
+    }
+
     // Apply general implicit casting rules after specialised once.
     expr.thenExpr = wrapImplicitCast(expr.thenExpr, elseType);
     thenType = expr.thenExpr.type();
@@ -2579,8 +2631,9 @@ public Void visit(MacroMatchExpr expr) {
 
   @Override
   public Void visit(MatchExpr expr) {
+
+    // Check all entities
     var candidateType = check(expr.candidate);
-    var firstResultType = check(expr.cases.get(0).result);
     for (var kase : expr.cases) {
       kase.patterns.forEach(this::check);
       kase.patterns.replaceAll(p -> wrapImplicitCast(p, candidateType));
@@ -2593,28 +2646,49 @@ public Void visit(MatchExpr expr) {
               .note("The type of the candidate and the pattern must be the same.")
               .build();
         }
+        check(kase.result);
       }
+    }
+    check(expr.defaultResult);
 
-      // Check that all branches have the same type
-      check(kase.result);
+    // If only one branch should be checked, directly propergate the type, and don't check whether
+    // the branches are compatible.
+    // This is intended: https://github.com/OpenVADL/open-vadl/issues/47#issuecomment-2725475475
+    if (branchStrategy.equals(BranchStrategy.ONE)) {
+      var candidateConstant = constantEvaluator.eval(expr.candidate);
+      for (var kase : expr.cases) {
+        if (kase.patterns.stream()
+            .map(constantEvaluator::eval)
+            .allMatch(candidateConstant::equals)) {
+          expr.type = kase.result.type();
+          return null;
+        }
+      }
+
+      expr.type = expr.defaultResult.type();
+      return null;
+    }
+
+    // Check that all branches have the same type
+    var firstResultType = check(expr.cases.get(0).result);
+    for (var kase : expr.cases) {
       kase.result = wrapImplicitCast(kase.result, firstResultType);
-      var resultType = check(kase.result);
+      var resultType = kase.result.type();
       if (!resultType.equals(firstResultType)) {
         throw Diagnostic.error("Type Mismatch", kase.result)
-            .locationNote(kase.result, "All results before were of type `%s`, but this is `%s`",
+            .locationNote(kase.result, "All previous branches were of type `%s`, but this is `%s`",
                 firstResultType, resultType)
             .description("All branches of a match must have the same type")
             .build();
       }
     }
 
-    check(expr.defaultResult);
     expr.defaultResult = wrapImplicitCast(expr.defaultResult, firstResultType);
     var defaultResultType = expr.defaultResult.type();
     if (!defaultResultType.equals(firstResultType)) {
       throw Diagnostic.error("Type Mismatch", expr.defaultResult)
           .locationNote(expr.defaultResult,
-              "All results before were of type `%s`, but this is `%s`",
+              "All previous branches were of type `%s`, but this is `%s`",
               firstResultType, defaultResultType)
           .description("All branches of a match must have the same type")
           .build();

vadl/main/vadl/utils/EditorUtils.java

@@ -0,0 +1,44 @@
+// SPDX-FileCopyrightText : © 2025 TU Wien <vadl@tuwien.ac.at>
+// SPDX-License-Identifier: GPL-3.0-or-later
+//
+// This program is free software: you can redistribute it and/or modify
+// it under the terms of the GNU General Public License as published by
+// the Free Software Foundation, either version 3 of the License, or
+// (at your option) any later version.
+//
+// This program is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+// GNU General Public License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <https://www.gnu.org/licenses/>.
+
+package vadl.utils;
+
+import java.util.Objects;
+import javax.annotation.Nullable;
+
+/**
+ * A file to work around the "quirks" of some editors and IDE's.
+ */
+public class EditorUtils {
+
+  @Nullable
+  private static Boolean isIntelliJ = null;
+
+  /**
+   * Detect whether the program is currently executing inside IntelliJ.
+   */
+  public static boolean isIntelliJIDE() {
+    if (isIntelliJ == null) {
+      isIntelliJ = Objects.requireNonNullElse(System.getenv("TERMINAL_EMULATOR"), "")
+          .equals("JetBrains-JediTerm")
+          || Objects.requireNonNullElse(System.getenv("XPC_SERVICE_NAME"), "")
+          .startsWith("application.com.jetbrains")
+      ;
+    }
+
+    return isIntelliJ;
+  }
+}

vadl/main/vadl/utils/SourceLocation.java

@@ -16,6 +16,8 @@
 
 package vadl.utils;
 
+import static vadl.utils.EditorUtils.isIntelliJIDE;
+
 import java.io.IOException;
 import java.net.URI;
 import java.nio.file.Files;
@@ -173,8 +175,7 @@ public String toIDEString() {
 
     String printablePath;
 
-    if (Objects.requireNonNullElse(System.getenv("TERMINAL_EMULATOR"), "")
-        .equals("JetBrains-JediTerm") || this.uri.getScheme().equals("memory")) {
+    if (isIntelliJIDE() || this.uri.getScheme().equals("memory")) {
       // IntelliJ integrated terminal needs special treatment
       printablePath = this.uri.toString();
     } else {