diff --git a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java index 57668124da..d08110dbfb 100644 --- a/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java +++ b/subprojects/cfa/src/main/java/hu/bme/mit/theta/cfa/dsl/CfaExpression.java @@ -25,6 +25,7 @@ import hu.bme.mit.theta.core.decl.Decl; import hu.bme.mit.theta.core.decl.ParamDecl; import hu.bme.mit.theta.core.dsl.DeclSymbol; +import hu.bme.mit.theta.core.dsl.ParseException; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; import hu.bme.mit.theta.core.type.abstracttype.*; @@ -266,7 +267,7 @@ public Expr visitEqualityExpr(final EqualityExprContext ctx) { case NEQ: return Neq(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -290,7 +291,7 @@ public Expr visitRelationExpr(final RelationExprContext ctx) { case GEQ: return Geq(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -310,7 +311,7 @@ public Expr visitBitwiseOrExpr(final BitwiseOrExprContext ctx) { case BITWISE_OR: return BvExprs.Or(List.of(leftOp, rightOp)); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -328,7 +329,7 @@ public Expr visitBitwiseXorExpr(final BitwiseXorExprContext ctx) { case BITWISE_XOR: return BvExprs.Xor(List.of(leftOp, rightOp)); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -346,7 +347,7 @@ public Expr visitBitwiseAndExpr(final BitwiseAndExprContext ctx) { case BITWISE_AND: return BvExprs.And(List.of(leftOp, rightOp)); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -372,7 +373,7 @@ public Expr visitBitwiseShiftExpr(final BitwiseShiftExprContext ctx) { case BITWISE_ROTATE_RIGHT: return BvExprs.RotateRight(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -391,14 +392,14 @@ public Expr visitAdditiveExpr(final AdditiveExprContext ctx) { final Expr opsHead = ops.get(0); final List> opsTail = ops.subList(1, ops.size()); - return createAdditiveExpr(opsHead, opsTail, ctx.opers); + return createAdditiveExpr(opsHead, opsTail, ctx.opers, ctx); } else { return visitChildren(ctx); } } private Expr createAdditiveExpr(final Expr opsHead, final List> opsTail, - final List opers) { + final List opers, final AdditiveExprContext ctx) { checkArgument(opsTail.size() == opers.size()); if (opsTail.isEmpty()) { @@ -410,13 +411,14 @@ private Expr createAdditiveExpr(final Expr opsHead, final List opersTail = opers.subList(1, opers.size()); - final Expr subExpr = createAdditiveSubExpr(opsHead, newOpsHead, operHead); + final Expr subExpr = createAdditiveSubExpr(opsHead, newOpsHead, operHead, ctx); - return createAdditiveExpr(subExpr, newOpsTail, opersTail); + return createAdditiveExpr(subExpr, newOpsTail, opersTail, ctx); } } - private Expr createAdditiveSubExpr(final Expr leftOp, final Expr rightOp, final Token oper) { + private Expr createAdditiveSubExpr(final Expr leftOp, final Expr rightOp, final Token oper, + final AdditiveExprContext ctx) { switch (oper.getType()) { case PLUS: @@ -426,7 +428,7 @@ private Expr createAdditiveSubExpr(final Expr leftOp, final Expr rightO return createSubExpr(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator '" + oper.getText() + "'"); } } @@ -456,7 +458,7 @@ public Expr visitMultiplicativeExpr(final MultiplicativeExprContext ctx) { final Expr opsHead = ops.get(0); final List> opsTail = ops.subList(1, ops.size()); - return createMutliplicativeExpr(opsHead, opsTail, ctx.opers); + return createMutliplicativeExpr(opsHead, opsTail, ctx.opers, ctx); } else { return visitChildren(ctx); } @@ -464,7 +466,7 @@ public Expr visitMultiplicativeExpr(final MultiplicativeExprContext ctx) { } private Expr createMutliplicativeExpr(final Expr opsHead, final List> opsTail, - final List opers) { + final List opers, final MultiplicativeExprContext ctx) { checkArgument(opsTail.size() == opers.size()); if (opsTail.isEmpty()) { @@ -476,13 +478,14 @@ private Expr createMutliplicativeExpr(final Expr opsHead, final List opersTail = opers.subList(1, opers.size()); - final Expr subExpr = createMultiplicativeSubExpr(opsHead, newOpsHead, operHead); + final Expr subExpr = createMultiplicativeSubExpr(opsHead, newOpsHead, operHead, ctx); - return createMutliplicativeExpr(subExpr, newOpsTail, opersTail); + return createMutliplicativeExpr(subExpr, newOpsTail, opersTail, ctx); } } - private Expr createMultiplicativeSubExpr(final Expr leftOp, final Expr rightOp, final Token oper) { + private Expr createMultiplicativeSubExpr(final Expr leftOp, final Expr rightOp, final Token oper, + final MultiplicativeExprContext ctx) { switch (oper.getType()) { case MUL: @@ -498,7 +501,7 @@ private Expr createMultiplicativeSubExpr(final Expr leftOp, final Expr return createRemExpr(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator '" + oper.getText() + "'"); } } @@ -539,7 +542,7 @@ public Expr visitUnaryExpr(final UnaryExprContext ctx) { return Neg(op); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { return visitChildren(ctx); @@ -588,7 +591,7 @@ private Expr createAccessSubExpr(final Expr op, final AccessContext access } else if (access.prime != null) { return createPrimeExpr(op); } else { - throw new AssertionError(); + throw new ParseException(access, "Unknown expression"); } } @@ -723,7 +726,7 @@ else if(sizeAndContent[1].startsWith("x")) { isSigned = false; } else { - throw new IllegalArgumentException("Invalid bitvector literal"); + throw new ParseException(ctx, "Invalid bitvector literal"); } checkArgument(value.length <= size, "The value of the literal cannot be represented on the given amount of bits"); @@ -801,8 +804,7 @@ private boolean[] decodeHexadecimalBvContent(String lit) { public RefExpr visitIdExpr(final IdExprContext ctx) { Optional optSymbol = currentScope.resolve(ctx.id.getText()); if (optSymbol.isEmpty()) { - throw new NoSuchElementException("Identifier '" + ctx.id.getText() + "' at line " + - ctx.start.getLine() + " cannot be resolved"); + throw new ParseException(ctx, "Identifier '" + ctx.id.getText() + "' cannot be resolved"); } final Symbol symbol = optSymbol.get(); final Decl decl = (Decl) env.eval(symbol); diff --git a/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/ParseException.java b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/ParseException.java new file mode 100644 index 0000000000..cfb141feec --- /dev/null +++ b/subprojects/core/src/main/java/hu/bme/mit/theta/core/dsl/ParseException.java @@ -0,0 +1,29 @@ +/* + * Copyright 2017 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ +package hu.bme.mit.theta.core.dsl; + +import org.antlr.v4.runtime.ParserRuleContext; + +public class ParseException extends RuntimeException { + public ParseException(ParserRuleContext ctx, String message){ + this(ctx, message, null); + } + + public ParseException(ParserRuleContext ctx, String message, Throwable cause) { + super("Line " + ctx.getStart().getLine() + " col " + ctx.getStart().getCharPositionInLine() + ": " + message, cause); + } + +} diff --git a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java index 3d59cddd25..e346abcf70 100644 --- a/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java +++ b/subprojects/sts/src/main/java/hu/bme/mit/theta/sts/dsl/StsExprCreatorVisitor.java @@ -48,6 +48,7 @@ import java.util.Optional; import java.util.stream.Stream; +import hu.bme.mit.theta.core.dsl.ParseException; import org.antlr.v4.runtime.Token; import com.google.common.collect.ImmutableList; @@ -268,7 +269,7 @@ public Expr visitEqualityExpr(final EqualityExprContext ctx) { case StsDslParser.NEQ: return Neq(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -292,7 +293,7 @@ public Expr visitRelationExpr(final RelationExprContext ctx) { case StsDslParser.GEQ: return Geq(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator"); } } else { @@ -311,14 +312,14 @@ public Expr visitAdditiveExpr(final AdditiveExprContext ctx) { final Expr opsHead = ops.get(0); final List> opsTail = ops.subList(1, ops.size()); - return createAdditiveExpr(opsHead, opsTail, ctx.opers); + return createAdditiveExpr(opsHead, opsTail, ctx.opers, ctx); } else { return visitChildren(ctx); } } private Expr createAdditiveExpr(final Expr opsHead, final List> opsTail, - final List opers) { + final List opers, final AdditiveExprContext ctx) { checkArgument(opsTail.size() == opers.size()); if (opsTail.isEmpty()) { @@ -330,13 +331,14 @@ private Expr createAdditiveExpr(final Expr opsHead, final List opersTail = opers.subList(1, opers.size()); - final Expr subExpr = createAdditiveSubExpr(opsHead, newOpsHead, operHead); + final Expr subExpr = createAdditiveSubExpr(opsHead, newOpsHead, operHead, ctx); - return createAdditiveExpr(subExpr, newOpsTail, opersTail); + return createAdditiveExpr(subExpr, newOpsTail, opersTail, ctx); } } - private Expr createAdditiveSubExpr(final Expr leftOp, final Expr rightOp, final Token oper) { + private Expr createAdditiveSubExpr(final Expr leftOp, final Expr rightOp, final Token oper, + final AdditiveExprContext ctx) { switch (oper.getType()) { case StsDslParser.PLUS: @@ -346,7 +348,7 @@ private Expr createAdditiveSubExpr(final Expr leftOp, final Expr rightO return createSubExpr(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator '" + oper.getText() + "'"); } } @@ -375,7 +377,7 @@ public Expr visitMultiplicativeExpr(final MultiplicativeExprContext ctx) { final Expr opsHead = ops.get(0); final List> opsTail = ops.subList(1, ops.size()); - return createMutliplicativeExpr(opsHead, opsTail, ctx.opers); + return createMutliplicativeExpr(opsHead, opsTail, ctx.opers, ctx); } else { return visitChildren(ctx); } @@ -383,7 +385,7 @@ public Expr visitMultiplicativeExpr(final MultiplicativeExprContext ctx) { } private Expr createMutliplicativeExpr(final Expr opsHead, final List> opsTail, - final List opers) { + final List opers, final MultiplicativeExprContext ctx) { checkArgument(opsTail.size() == opers.size()); if (opsTail.isEmpty()) { @@ -395,13 +397,14 @@ private Expr createMutliplicativeExpr(final Expr opsHead, final List opersTail = opers.subList(1, opers.size()); - final Expr subExpr = createMultiplicativeSubExpr(opsHead, newOpsHead, operHead); + final Expr subExpr = createMultiplicativeSubExpr(opsHead, newOpsHead, operHead, ctx); - return createMutliplicativeExpr(subExpr, newOpsTail, opersTail); + return createMutliplicativeExpr(subExpr, newOpsTail, opersTail, ctx); } } - private Expr createMultiplicativeSubExpr(final Expr leftOp, final Expr rightOp, final Token oper) { + private Expr createMultiplicativeSubExpr(final Expr leftOp, final Expr rightOp, final Token oper, + final MultiplicativeExprContext ctx) { switch (oper.getType()) { case StsDslParser.MUL: @@ -417,7 +420,7 @@ private Expr createMultiplicativeSubExpr(final Expr leftOp, final Expr return createRemExpr(leftOp, rightOp); default: - throw new AssertionError(); + throw new ParseException(ctx, "Unknown operator '" + oper.getText() + "'"); } } @@ -489,18 +492,16 @@ private Expr createAccessSubExpr(final Expr op, final AccessContext access } else if (access.prime != null) { return createPrimeExpr(op); } else { - throw new AssertionError(); + throw new ParseException(access, "Unknown expression"); } } private Expr createFuncAppExpr(final Expr op, final FuncAccessContext ctx) { - // TODO Auto-generated method stub - throw new UnsupportedOperationException("TODO: auto-generated method stub"); + throw new ParseException(ctx, "Unsupported expression"); } private Expr createArrayReadExpr(final Expr op, final ArrayAccessContext ctx) { - // TODO Auto-generated method stub - throw new UnsupportedOperationException("TODO: auto-generated method stub"); + throw new ParseException(ctx, "Unsupported expression"); } private Expr createPrimeExpr(final Expr op) { @@ -536,7 +537,9 @@ public RatLitExpr visitRatLitExpr(final RatLitExprContext ctx) { public Expr visitIdExpr(final IdExprContext ctx) { final Optional optSymbol = currentScope.resolve(ctx.id.getText()); - if (optSymbol.isEmpty()) throw new NoSuchElementException("Identifier '" + ctx.id.getText() + "' not found"); + if (optSymbol.isEmpty()) { + throw new ParseException(ctx, "Identifier '" + ctx.id.getText() + "' cannot be resolved"); + } final Symbol symbol = optSymbol.get(); checkArgument(symbol instanceof DeclSymbol); diff --git a/subprojects/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XSTSVisitor.java b/subprojects/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XSTSVisitor.java index 5c8d11fac6..f20314e270 100644 --- a/subprojects/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XSTSVisitor.java +++ b/subprojects/xsts/src/main/java/hu/bme/mit/theta/xsts/dsl/XSTSVisitor.java @@ -2,6 +2,7 @@ import hu.bme.mit.theta.core.decl.Decls; import hu.bme.mit.theta.core.decl.VarDecl; +import hu.bme.mit.theta.core.dsl.ParseException; import hu.bme.mit.theta.core.stmt.*; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.booltype.BoolType; @@ -66,12 +67,14 @@ private void checkIfTempVar(String name){ @Override public Expr visitTypeDeclaration(XstsDslParser.TypeDeclarationContext ctx) { checkIfTempVar(ctx.name.getText()); - if(nameToTypeMap.containsKey(ctx.name.getText()) || ctx.name.getText().equals("integer") || ctx.name.getText().equals("boolean")) throw new RuntimeException("Type "+ctx.name.getText()+" already exists!"+" On line "+ctx.start.getLine()); + if(nameToTypeMap.containsKey(ctx.name.getText()) || ctx.name.getText().equals("integer") || ctx.name.getText().equals("boolean")) { + throw new ParseException(ctx, "Type '" + ctx.name.getText() + "' already exists!"); + } List literals=new ArrayList<>(); List intValues=new ArrayList<>(); for(XstsDslParser.TypeLiteralContext literal:ctx.literals){ checkIfTempVar(literal.name.getText()); - if(literals.contains(literal.name.getText())) throw new RuntimeException("Duplicate literal "+literal.name.getText()+" in type "+ctx.name.getText()); + if(literals.contains(literal.name.getText())) throw new ParseException(ctx, "Duplicate literal '" + literal.name.getText() + "' in type '" + ctx.name.getText() + "'"); if(literalToIntMap.containsKey(literal.name.getText())) { intValues.add(literalToIntMap.get(literal.name.getText())); } else { @@ -90,9 +93,9 @@ public Expr visitTypeDeclaration(XstsDslParser.TypeDeclarationContext ctx) { public Expr visitVariableDeclaration(XstsDslParser.VariableDeclarationContext ctx) { checkIfTempVar(ctx.name.getText()); if(nameToDeclMap.containsKey(ctx.name.getText())){ - throw new RuntimeException("Variable ["+ctx.name.getText()+"] already exists."); + throw new ParseException(ctx, "Variable '" + ctx.name.getText() + "' already exists."); } else if(literalToIntMap.containsKey(ctx.name.getText())){ - throw new RuntimeException("["+ctx.name.getText()+"] is a type literal, cannot declare variable with this name."); + throw new ParseException(ctx, "'" + ctx.name.getText() + "' is a type literal, cannot declare variable with this name."); } VarDecl decl; @@ -106,7 +109,7 @@ else if(nameToTypeMap.containsKey(ctx.type.customType().name.getText())){ decl=Decls.Var(ctx.name.getText(),IntType.getInstance()); varToTypeMap.put(decl,nameToTypeMap.get(ctx.type.customType().name.getText())); } else { - throw new RuntimeException("Unknown type "+ctx.type.customType().name.getText()+" on line "+ctx.start.getLine()); + throw new ParseException(ctx, "Unknown type '" + ctx.type.customType().name.getText() + "'."); } if(ctx.CTRL()!=null) ctrlVars.add(decl); @@ -119,17 +122,17 @@ else if(nameToTypeMap.containsKey(ctx.type.customType().name.getText())){ @Override public Expr visitExpr(XstsDslParser.ExprContext ctx) { - if(ctx.iteExpression()==null) throw new RuntimeException("Invalid expression on line "+ctx.start.getLine()); + if (ctx.iteExpression() == null) throw new ParseException(ctx, "Invalid expression."); return visitIteExpression(ctx.iteExpression()); } @Override public Expr visitIteExpression(XstsDslParser.IteExpressionContext ctx) { - if(ctx.cond != null){ - if(ctx.then == null || ctx.elze == null) throw new RuntimeException("Invalid if-then-else expression on line "+ctx.start.getLine()); - return Ite(visitExpr(ctx.cond),visitExpr(ctx.then),visitExpr(ctx.elze)); + if (ctx.cond != null){ + if (ctx.then == null || ctx.elze == null) throw new ParseException(ctx, "Invalid if-then-else expression."); + return Ite(visitExpr(ctx.cond), visitExpr(ctx.then), visitExpr(ctx.elze)); } else { - if(ctx.implyExpression()==null) throw new RuntimeException("Invalid expression on line "+ctx.start.getLine()); + if (ctx.implyExpression() == null) throw new ParseException(ctx, "Invalid expression."); return visitImplyExpression(ctx.implyExpression()); } } @@ -191,7 +194,7 @@ public Expr visitRelationExpr(XstsDslParser.RelationExprContext ctx) { return Lt(visitAdditiveExpr(ctx.ops.get(0)),visitAdditiveExpr(ctx.ops.get(1))); }else if(ctx.oper.GT()!=null){ return Gt(visitAdditiveExpr(ctx.ops.get(0)),visitAdditiveExpr(ctx.ops.get(1))); - } else throw new UnsupportedOperationException("Unsupported operation "+ctx.oper.getText()+" on line "+ctx.start.getLine()); + } else throw new ParseException(ctx, "Unsupported operation '" + ctx.oper.getText() + "'"); }else return visitAdditiveExpr(ctx.ops.get(0)); } @@ -230,7 +233,7 @@ public Expr visitMultiplicativeExpr(XstsDslParser.MultiplicativeExprContext ctx) }else if(ctx.opers.get(i-1).MUL()!=null){ res=Mul(res,visitNegExpr(ctx.ops.get(i))); } else{ - throw new UnsupportedOperationException("Unsupported operation "+ctx.opers.get(i-1).getText()+" on line "+ctx.start.getLine()); + throw new ParseException(ctx, "Unsupported operation '" + ctx.opers.get(i-1).getText() + "'"); } } return res; @@ -272,7 +275,7 @@ public Expr visitLiteral(XstsDslParser.LiteralContext ctx) { if(ctx.BOOLLIT().getText().equals("true")) return True(); else return False(); }else if(ctx.INTLIT()!=null){ return Int(ctx.INTLIT().getText()); - }else throw new RuntimeException("Literal "+ctx.getText()+" could not be resolved to integer or boolean type."+" On line "+ctx.start.getLine()); + }else throw new ParseException(ctx, "Literal '" + ctx.getText() + "' could not be resolved to integer or boolean type."); } @Override @@ -280,15 +283,14 @@ public Expr visitReference(XstsDslParser.ReferenceContext ctx) { checkIfTempVar(ctx.name.getText()); if(literalToIntMap.containsKey(ctx.name.getText())) return Int(literalToIntMap.get(ctx.name.getText())); else if(nameToDeclMap.containsKey(ctx.name.getText())) return nameToDeclMap.get(ctx.name.getText()).getRef(); - else throw new RuntimeException("Literal or reference "+ctx.name.getText()+" could not be resolved."+" On line "+ctx.start.getLine()); + else throw new ParseException(ctx, "Literal or reference '" + ctx.name.getText() + "' could not be resolved."); } @Override public Expr visitPrime(XstsDslParser.PrimeContext ctx) { if(ctx.reference()!=null) return visitReference(ctx.reference()); - else throw new UnsupportedOperationException("Prime expressions are not supported."+" On line "+ctx.start.getLine()); -// return Prime(visitPrime(ctx.prime())); + else throw new ParseException(ctx, "Prime expressions are not supported."); } public Stmt processAction(XstsDslParser.ActionContext ctx) { @@ -329,12 +331,16 @@ public AssumeStmt processAssumeAction(XstsDslParser.AssumeActionContext ctx) { } public AssignStmt processAssignAction(XstsDslParser.AssignActionContext ctx) { - if(!nameToDeclMap.containsKey(ctx.lhs.getText())) throw new RuntimeException("Could not resolve variable "+ctx.lhs.getText()+" on line "+ctx.start.getLine()); + if(!nameToDeclMap.containsKey(ctx.lhs.getText())) { + throw new ParseException(ctx, "Could not resolve variable '" + ctx.lhs.getText() + "'"); + } return Stmts.Assign(nameToDeclMap.get(ctx.lhs.getText()),visitExpr(ctx.rhs)); } public HavocStmt processHavocAction(XstsDslParser.HavocActionContext ctx){ - if(!nameToDeclMap.containsKey(ctx.name.getText())) throw new RuntimeException("Could not resolve variable "+ctx.name.getText()+" on line "+ctx.start.getLine()); + if(!nameToDeclMap.containsKey(ctx.name.getText())) { + throw new ParseException(ctx, "Could not resolve variable '" + ctx.name.getText() + "'"); + } return Stmts.Havoc(nameToDeclMap.get(ctx.name.getText())); } }