diff --git a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java index e8ee3a6ca..74cd00c7f 100644 --- a/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java +++ b/verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java @@ -312,6 +312,7 @@ private StmtExpr convertExpression(JCTree.JCExpression expr, Map case JCTree.JCUnary unary -> convertUnary(unary, renames); case JCTree.JCAssign asgn -> assign(toSourceRange(asgn), convertExpression(asgn.lhs, renames), convertExpression(asgn.rhs, renames)); + case JCTree.JCAssignOp assignOp -> convertCompoundAssign(assignOp, renames); case JCTree.JCConditional cond -> ifThenElse(toSourceRange(cond), convertExpression(cond.cond, renames), convertExpression(cond.truepart, renames), @@ -374,10 +375,28 @@ private StmtExpr convertUnary(JCTree.JCUnary unary, Map renames) return switch (unary.getTag()) { case NOT -> not(sr, inner); case NEG -> neg(sr, inner); + case POS -> inner; + case PREINC, POSTINC -> assign(sr, inner, add(sr, convertExpression(unary.arg, renames), longLiteral(sr, 1))); + case PREDEC, POSTDEC -> assign(sr, inner, sub(sr, convertExpression(unary.arg, renames), longLiteral(sr, 1))); default -> throw new JavaViolationException("Unsupported unary op: " + unary.getTag()); }; } + private StmtExpr convertCompoundAssign(JCTree.JCAssignOp assignOp, Map renames) { + StmtExpr lhs = convertExpression(assignOp.lhs, renames); + StmtExpr rhs = convertExpression(assignOp.rhs, renames); + SourceRange sr = toSourceRange(assignOp); + StmtExpr value = switch (assignOp.getTag()) { + case PLUS_ASG -> add(sr, lhs, rhs); + case MINUS_ASG -> sub(sr, lhs, rhs); + case MUL_ASG -> mul(sr, lhs, rhs); + case DIV_ASG -> divT(sr, lhs, rhs); + case MOD_ASG -> modT(sr, lhs, rhs); + default -> throw new JavaViolationException("Unsupported compound assignment op: " + assignOp.getTag()); + }; + return assign(sr, convertExpression(assignOp.lhs, renames), value); + } + private StmtExpr convertJVerifyCall(JCTree.JCMethodInvocation invocation, Symbol.MethodSymbol jverifyMethod, Map renames) { diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/ImpureNumericOperatorsVerification.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/ImpureNumericOperatorsVerification.java index e6891568c..25509bf22 100644 --- a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/ImpureNumericOperatorsVerification.java +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/ImpureNumericOperatorsVerification.java @@ -16,10 +16,10 @@ public int foo() { var r = 3; var incrementPostfix = l++; check(incrementPostfix == 4); - check(l == 4L); + check(l == 4); var decrementPostfix = l--; check(decrementPostfix == 3); - check(l == 3L); + check(l == 3); var incrementPrefix = ++l; check(incrementPrefix == 4); check(l == 4); diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/IncrementDecrementVerification.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/IncrementDecrementVerification.java new file mode 100644 index 000000000..80d3794b6 --- /dev/null +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/IncrementDecrementVerification.java @@ -0,0 +1,45 @@ +package org.strata.jverify.verifier.tests.javasupport.expressions; + +import org.strata.jverify.testengine.JVerifyTest; + +import static org.strata.jverify.JVerify.check; + +/** + * Tests for prefix and postfix increment/decrement operators. + * + * Note: both prefix and postfix are currently lowered identically to x = x ± 1, + * so the expression value is always the new value. Correct postfix semantics + * (returning the old value) requires Laurel IR support for block expressions. + */ +@SuppressWarnings("ConstantValue") +@JVerifyTest(methodsVerified = 5, errorCount = 0) +class IncrementDecrementVerification { + + /** Postfix ++ increments the variable. */ + static void postfixIncrement() { + var x = 5; + x++; + check(x == 6); + } + + /** Prefix ++ increments the variable. */ + static void prefixIncrement() { + var x = 5; + ++x; + check(x == 6); + } + + /** Postfix -- decrements the variable. */ + static void postfixDecrement() { + var x = 10; + x--; + check(x == 9); + } + + /** Prefix -- decrements the variable. */ + static void prefixDecrement() { + var x = 10; + --x; + check(x == 9); + } +} diff --git a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/VerifyNumericOperators.java b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/VerifyNumericOperators.java index 8b951f11f..5caa6e7c7 100644 --- a/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/VerifyNumericOperators.java +++ b/verifier/src/test/java/org/strata/jverify/verifier/tests/javasupport/expressions/VerifyNumericOperators.java @@ -9,9 +9,9 @@ * byte, short, int, long, float, double, char */ @SuppressWarnings("ConstantValue") -@JVerifyTest(skip = "Strata: not yet supported", exitCode = 4, methodsVerified = 1, errorCount = 1) +@JVerifyTest(exitCode = 4, methodsVerified = 1, errorCount = 1) class VerifyNumericOperators { - public void foo() { + static void foo() { var l = 3L; var r = 3L; l++;