Support ++, --, compound assignment, and unary + operators

verifier/src/main/java/org/strata/jverify/verifier/compiler/generator/laurel/JavaToLaurelCompiler.java

@@ -312,6 +312,7 @@ private StmtExpr convertExpression(JCTree.JCExpression expr, Map<String, String>
                 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<String, String> 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<String, String> 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<String, String> renames) {

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);

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);
+    }
+}

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++;