Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Remove usages of K error handling infrastructure #1001

Merged
merged 12 commits into from
Mar 1, 2024
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
package org.kframework.backend.llvm.matching;

import org.kframework.attributes.Location;
import org.kframework.attributes.Source;

import java.util.Optional;

public final class MatchingException extends Throwable {
public enum Type {
USELESS_RULE,
NON_EXHAUSTIVE_MATCH,
INTERNAL_ERROR,
COMPILER_ERROR,
}

Type type;
String message;
Optional<Source> source;
Optional<Location> location;

public MatchingException(Type type, String message, Optional<Source> source, Optional<Location> location) {
this.type = type;
this.message = message;
this.source = source;
this.location = location;
}

public MatchingException(Type type, String message, Source source, Location location) {
this(type, message, Optional.of(source), Optional.of(location));
}

public MatchingException(Type type, String message) {
this(type, message, Optional.empty(), Optional.empty());
}

public Type getType() {
return type;
}

@Override
public String getMessage() {
return message;
}

public Optional<Source> getSource() {
return source;
}

public Optional<Location> getLocation() {
return location;
}
}
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@ import org.kframework.backend.llvm.matching.pattern.SymbolP
import org.kframework.backend.llvm.matching.pattern.VariableP
import org.kframework.backend.llvm.matching.pattern.WildcardP
import org.kframework.parser.kore._
import org.kframework.utils.errorsystem.KException

object Generator {

Expand Down Expand Up @@ -210,7 +209,7 @@ object Generator {
axioms: IndexedSeq[AxiomInfo],
sorts: Seq[Sort],
name: SymbolOrAlias,
kem: KException => scala.Unit
kem: MatchingException => scala.Unit
): DecisionTree = {
val matrix = genClauseMatrix(symlib, mod, axioms, sorts)
matrix.checkUsefulness(kem)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ import java.util.Optional
import org.kframework.backend.llvm.matching.dt._
import org.kframework.parser.kore._
import org.kframework.parser.kore.parser.TextToKore
import org.kframework.utils.errorsystem.KException

object Matching {
def writeDecisionTreeToFile(
Expand All @@ -17,7 +16,7 @@ object Matching {
genSingleRuleTrees: Boolean,
warn: Boolean,
genSearch: Boolean,
kem: KException => Unit
kem: MatchingException => Unit
) {
val defn = new TextToKore().parse(filename)
outputFolder.mkdirs()
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,6 @@ import org.kframework.parser.kore.Sort
import org.kframework.parser.kore.SymbolOrAlias
import org.kframework.parser.kore.Variable
import org.kframework.unparser.ToKast
import org.kframework.utils.errorsystem.KEMException
import org.kframework.utils.errorsystem.KException

trait AbstractColumn {
def column: Column
Expand Down Expand Up @@ -744,11 +742,12 @@ class Matrix private (
try
row.clause.action.rhsVars.map(v => v -> (grouped(v).head._2, grouped(v).head._1.hookAtt))
catch {
case e: NoSuchElementException =>
throw KEMException.internalError(
case _: NoSuchElementException =>
throw new MatchingException(
MatchingException.Type.INTERNAL_ERROR,
"Could not find binding for variable while compiling pattern matching.",
e,
row.clause.action
row.clause.action.source,
row.clause.action.location
)
}
(lhs ++ rhs).sortBy(v => v._1).map(v => v._2)
Expand Down Expand Up @@ -1052,23 +1051,22 @@ class Matrix private (
}
}

def checkUsefulness(kem: KException => Unit): Unit =
def checkUsefulness(kem: MatchingException => Unit): Unit =
for (rowIx <- rows.indices)
if (rowUseless(rowIx)) {
if (clauses(rowIx).action.source.isPresent && clauses(rowIx).action.location.isPresent) {
kem(
new KException(
KException.ExceptionType.USELESS_RULE,
KException.KExceptionGroup.COMPILER,
new MatchingException(
MatchingException.Type.USELESS_RULE,
"Potentially useless rule detected.",
clauses(rowIx).action.source.get,
clauses(rowIx).action.location.get
clauses(rowIx).action.source,
clauses(rowIx).action.location
)
)
}
}

def checkExhaustiveness(name: SymbolOrAlias, kem: KException => Unit): Unit = {
def checkExhaustiveness(name: SymbolOrAlias, kem: MatchingException => Unit): Unit = {
Matrix.id = 0
val id = Matrix.id
if (Matching.logging) {
Expand All @@ -1093,9 +1091,8 @@ class Matrix private (
val source = Parser.source(attributes).orElse(null)

kem(
new KException(
KException.ExceptionType.NON_EXHAUSTIVE_MATCH,
KException.KExceptionGroup.COMPILER,
new MatchingException(
MatchingException.Type.NON_EXHAUSTIVE_MATCH,
"Non exhaustive match detected: " ++ ToKast(func),
source,
location
Expand Down
Original file line number Diff line number Diff line change
@@ -1,13 +1,15 @@
package org.kframework.backend.llvm.matching.pattern

import java.util.regex.{ Pattern => Regex }
import java.util.Optional
import org.kframework.attributes.Location
import org.kframework.attributes.Source
import org.kframework.backend.llvm.matching._
import org.kframework.backend.llvm.matching.dt._
import org.kframework.backend.llvm.matching.MatchingException
import org.kframework.mpfr._
import org.kframework.parser.kore.CompoundSort
import org.kframework.parser.kore.Sort
import org.kframework.parser.kore.SymbolOrAlias
import org.kframework.utils.errorsystem.KEMException

sealed trait SortCategory {
def hookAtt: String
Expand Down Expand Up @@ -46,7 +48,8 @@ object SortCategory {
case Some("BUFFER.StringBuffer") => BufferS()
case Some("MINT.MInt") => MIntS(getBitwidth(s.asInstanceOf[CompoundSort].params(0), symlib))
case Some("BAG.Bag") =>
throw KEMException.compilerError(
throw new MatchingException(
MatchingException.Type.COMPILER_ERROR,
"LLVM Backend does not support multisets. If you are seeing this error due to a configuration cell tagged with multiplicity=\"*\", please add either type=\"Map\" or type=\"Set\". If you still need the collection to not contain duplicates, it is recommended you also add a unique identifier each time a cell is created. You can do this with !X:Int."
);
}
Expand Down
Loading