explicit, BinaryOp and UnaryOp evaluation: Use overflow-aware math for integer evaluation

For the evaluation of integer math operations, use the ...Exact methods from
java.lang.Math to catch integer under-/overflows and throw PrismLangExceptions.

(adapted by Joachim Klein from https://github.com/prismmodelchecker/prism/pull/91)

Tag: performance

prism/src/parser/ast/ExpressionBinaryOp.java

@@ -192,19 +192,31 @@ public class ExpressionBinaryOp extends Expression
 			}
 		case PLUS:
 			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
-				return operand1.evaluateInt(ec) + operand2.evaluateInt(ec);
+				try {
+					return Math.addExact(operand1.evaluateInt(ec), operand2.evaluateInt(ec));
+				} catch (ArithmeticException e) {
+					throw new PrismLangException(e.getMessage(), this);
+				}
 			} else {
 				return operand1.evaluateDouble(ec) + operand2.evaluateDouble(ec);
 			}
 		case MINUS:
 			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
-				return operand1.evaluateInt(ec) - operand2.evaluateInt(ec);
+				try {
+					return Math.subtractExact(operand1.evaluateInt(ec), operand2.evaluateInt(ec));
+				} catch (ArithmeticException e) {
+					throw new PrismLangException(e.getMessage(), this);
+				}
 			} else {
 				return operand1.evaluateDouble(ec) - operand2.evaluateDouble(ec);
 			}
 		case TIMES:
 			if (operand1.getType() == TypeInt.getInstance() && operand2.getType() == TypeInt.getInstance()) {
-				return operand1.evaluateInt(ec) * operand2.evaluateInt(ec);
+				try {
+					return Math.multiplyExact(operand1.evaluateInt(ec), operand2.evaluateInt(ec));
+				} catch (ArithmeticException e) {
+					throw new PrismLangException(e.getMessage(), this);
+				}
 			} else {
 				return operand1.evaluateDouble(ec) * operand2.evaluateDouble(ec);
 			}

prism/src/parser/ast/ExpressionUnaryOp.java

@@ -123,7 +123,11 @@ public class ExpressionUnaryOp extends Expression
 			return !operand.evaluateBoolean(ec);
 		case MINUS:
 			if (type instanceof TypeInt) {
-				return -operand.evaluateInt(ec);
+				try {
+					return Math.negateExact(operand.evaluateInt(ec));
+				} catch (ArithmeticException e) {
+					throw new PrismLangException(e.getMessage(), this);
+				}
 			} else {
 				return -operand.evaluateDouble(ec);
 			}