Skip to content

Commit

Permalink
Improve parser general error message
Browse files Browse the repository at this point in the history
  • Loading branch information
bobismijnnaam committed Nov 20, 2024
1 parent 2994a57 commit 6ea3d61
Show file tree
Hide file tree
Showing 4 changed files with 19 additions and 18 deletions.
2 changes: 1 addition & 1 deletion src/parsers/vct/parsers/AntlrParser.scala
Original file line number Diff line number Diff line change
Expand Up @@ -152,7 +152,7 @@ abstract class AntlrParser extends Parser {
convert(newConverter(baseOrigin, expectedErrors, tokenStream), main),
expectedErrors.map(_._3),
)
} catch { case m: MatchError => throw ParseMatchError(m.getMessage()) }
} catch { case m: MatchError => throw ParseMatchError(m) }
}

def parseReaderOrThrow[Ctx, G, Out](
Expand Down
5 changes: 3 additions & 2 deletions src/parsers/vct/parsers/err/ParseMatchError.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,8 @@ package vct.parsers.err

import vct.result.VerificationError.SystemError

case class ParseMatchError(objectDescription: String) extends SystemError {
case class ParseMatchError(error: Throwable) extends SystemError {
initCause(error)
override def text: String =
s"A MatchError occurred while parsing. This likely indicates a missing case in a parser: $objectDescription"
s"A MatchError occurred while parsing. This likely indicates a missing case in a parser (see below): ${error.getMessage}"
}
1 change: 1 addition & 0 deletions src/parsers/vct/parsers/transform/PVLToCol.scala
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,7 @@ case class PVLToCol[G](
) =>
new PVLEndpoint(
convert(name),
None,
new UnresolvedRef[G, Class[G]](convert(endpointType)),
typeArgs.map(convert(_)).getOrElse(Seq()),
args.map(convert(_)).getOrElse(Nil),
Expand Down
29 changes: 14 additions & 15 deletions src/rewrite/vct/rewrite/lang/LangVeyMontToCol.scala
Original file line number Diff line number Diff line change
Expand Up @@ -83,11 +83,10 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
val currentStatement: ScopedStack[Statement[Pre]] = ScopedStack()
val currentExpr: ScopedStack[Expr[Pre]] = ScopedStack()

lazy val warnedAboutAssign: Boolean = {
lazy val warnedAboutAssign: Unit = {
logger.warn(
"Plain assignment detected in choreography. This is allowed, but technically unsound. Use `:=` instead to also check endpoint ownership."
)
true
}

def rewriteCommunicateStatement(
Expand Down Expand Up @@ -169,11 +168,11 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])

def rewriteStatement(stmt: Statement[Pre]): Statement[Post] =
stmt match {
case stmt @ PVLEndpointStatement(endpointName, inner) =>
EndpointStatement[Post](
endpointName.map(rewriteEndpointName),
inner.rewriteDefault(),
)(stmt.blame)(stmt.o)
case stmt @ PVLEndpointStatement(endpointName, inner) => ???
// EndpointStatement[Post](
// endpointName.map(rewriteEndpointName),
// inner.rewriteDefault(),
// )(stmt.blame)(stmt.o)
case eval: Eval[Pre] =>
EndpointStatement[Post](None, eval.rewriteDefault())(PanicBlame(
"Inner statement cannot fail"
Expand All @@ -191,7 +190,7 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])
case comm: PVLCommunicateStatement[Pre] =>
rewriteCommunicateStatement(comm)
case assign: Assign[Pre] =>
val dummyToTriggerPrint = warnedAboutAssign
warnedAboutAssign
assign.rewriteDefault()
// Any statement not listed here, we put in ChorStatement. ChorStatementImpl defines which leftover statement we tolerate in choreographies
case stmt =>
Expand All @@ -204,19 +203,19 @@ case class LangVeyMontToCol[Pre <: Generation](rw: LangSpecificToCol[Pre])

def rewriteExpr(expr: Expr[Pre]): Expr[Post] =
expr match {
case PVLChorPerm(endpoint, loc, perm) =>
EndpointExpr(
rewriteEndpointName(endpoint),
Perm(rw.dispatch(loc), rw.dispatch(perm))(expr.o),
)(expr.o)
case PVLChorPerm(endpoint, loc, perm) => ???
// EndpointExpr(
// rewriteEndpointName(endpoint),
// Perm(rw.dispatch(loc), rw.dispatch(perm))(expr.o),
// )(expr.o)
case expr @ PVLSender() =>
Sender[Post](commSucc.ref(expr.ref.get.comm))(expr.o)
case expr @ PVLReceiver() =>
Receiver[Post](commSucc.ref(expr.ref.get.comm))(expr.o)
case expr @ PVLMessage() =>
Message[Post](commSucc.ref(expr.ref.get.comm))(expr.o)
case PVLEndpointExpr(endpoint, expr) =>
EndpointExpr(rewriteEndpointName(endpoint), rw.dispatch(expr))(expr.o)
case PVLEndpointExpr(endpoint, expr) => ???
// EndpointExpr(rewriteEndpointName(endpoint), rw.dispatch(expr))(expr.o)
case expr => currentExpr.having(expr) { rw.dispatch(expr) }
}
}

0 comments on commit 6ea3d61

Please sign in to comment.