From 821cc7eaa8eb8f7449c41c2aef3bb07f954fd220 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Sat, 9 May 2026 18:31:42 +0100 Subject: [PATCH 1/3] Operator Assignment Support --- .../testSuite/CorrectOperatorAssignments.java | 47 +++++++++++++++ .../RefinementTypeChecker.java | 31 +++++++++- .../general_checkers/OperationsChecker.java | 58 +++++++++++++++++++ 3 files changed, 133 insertions(+), 3 deletions(-) create mode 100644 liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java diff --git a/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java b/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java new file mode 100644 index 00000000..fb466ee8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java @@ -0,0 +1,47 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectOperatorAssignments { + + @Refinement("_ > 0") + int plus(@Refinement("_ >= 0") int x) { + x += 1; // x is now > 0 + return x; + } + + @Refinement("_ > 0") + int plusInvocation(@Refinement("_ >= 0") int x) { + x += one(); // x is now > 0 + return x; + } + + @Refinement("_ == 1") + int one() { + return 1; + } + + @Refinement("_ < 0") + int minus(@Refinement("_ <= 0") int x) { + x -= 1; // x is now < 0 + return x; + } + + @Refinement("_ >= 0") + int multiply(int x) { + x *= x; // x is now >= 0 + return x; + } + + @Refinement("_ <= 1") + int divide(@Refinement("0 <= _ && _ <= 3") int x) { + x /= 2; // x is now <= 1 + return x; + } + + @Refinement("_ == 0 || _ == 1") + int remainder(@Refinement("_ >= 0") int x) { + x %= 2; // x is now == 0 || x is now == 1 + return x; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 09095f35..9fd9bd0f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -38,6 +38,7 @@ import spoon.reflect.code.CtLocalVariable; import spoon.reflect.code.CtNewArray; import spoon.reflect.code.CtNewClass; +import spoon.reflect.code.CtOperatorAssignment; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtStatement; import spoon.reflect.code.CtThisAccess; @@ -186,10 +187,23 @@ public void visitCtThisAccess(CtThisAccess thisAccess) { } } - @SuppressWarnings("unchecked") @Override public void visitCtAssignment(CtAssignment assignment) throws LJError { super.visitCtAssignment(assignment); + visitAssignment(assignment); + } + + @Override + public void visitCtOperatorAssignment(CtOperatorAssignment assignment) { + super.visitCtOperatorAssignment(assignment); + visitAssignment(assignment); + } + + /** + * Handles simple and operator assignments after Spoon has visited their children + */ + @SuppressWarnings("unchecked") + private void visitAssignment(CtAssignment assignment) throws LJError { CtExpression ex = assignment.getAssigned(); if (ex instanceof CtVariableWriteImpl) { @@ -379,7 +393,7 @@ public void visitCtIf(CtIf ifElement) { thenRefs = Predicate.createConjunction(expRefs, freshIsTrue); elseRefs = Predicate.createConjunction(expRefs, freshIsFalse); } - + freshRV = context.addInstanceToContext(pathVarName, factory.Type().BOOLEAN_PRIMITIVE, thenRefs, exp); } vcChecker.addPathVariable(freshRV); @@ -495,7 +509,7 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< CtElement parentElem, CtElement varDecl) throws LJError { getPutVariableMetadata(ex, name); - Predicate refinementFound = getRefinement(assignment); + Predicate refinementFound = getAssignmentRefinement(name, assignment, parentElem); if (refinementFound == null) { RefinedVariable rv = context.getVariableByName(name); if (rv instanceof Variable) { @@ -512,6 +526,17 @@ private void checkAssignment(String name, CtTypeReference type, CtExpression< checkVariableRefinements(refinementFound, name, type, parentElem, varDecl); } + /** + * Get the refinement for operator assignments (e.g. x += 1) + */ + private Predicate getAssignmentRefinement(String name, CtExpression assignment, CtElement parentElem) + throws LJError { + if (parentElem instanceof CtOperatorAssignment operatorAssignment) { + return otc.getOperatorAssignmentRefinement(name, operatorAssignment); + } + return getRefinement(assignment); + } + private Predicate getExpressionRefinements(CtExpression element) throws LJError { if (element instanceof CtVariableRead) { // CtVariableRead elemVar = (CtVariableRead) element; diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index de64ceb1..b8c86bfa 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -16,6 +16,9 @@ import liquidjava.utils.constants.Ops; import liquidjava.utils.constants.Types; import liquidjava.rj_language.Predicate; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.GroupExpression; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -26,6 +29,7 @@ import spoon.reflect.code.CtInvocation; import spoon.reflect.code.CtLiteral; import spoon.reflect.code.CtLocalVariable; +import spoon.reflect.code.CtOperatorAssignment; import spoon.reflect.code.CtReturn; import spoon.reflect.code.CtUnaryOperator; import spoon.reflect.code.CtVariableRead; @@ -94,6 +98,18 @@ public void getBinaryOpRefinements(CtBinaryOperator operator) throws LJEr // TODO ADD TYPES } + /** + * Builds the refinement for a operator assignment. Java operator assignments such as {@code x += y} are modeled as + * {@code x = x + y}; the returned predicate refines the assigned value as {@code _ == current(x) rhs}. + */ + public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperatorAssignment assignment) + throws LJError { + Predicate left = getCurrentVariableValue(assignedName); + Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment()); + Predicate operation = Predicate.createOperation(left, getOperatorFromKind(assignment.getKind()), right); + return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), operation); + } + /** * Finds and adds refinement metadata to the unary operation * @@ -280,6 +296,48 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation inv) thr return new Predicate(); } + /** + * Returns the latest symbolic value for a variable + */ + private Predicate getCurrentVariableValue(String name) { + Optional variableInstance = rtc.getContext().getLastVariableInstance(name); + return Predicate.createVar(variableInstance.map(VariableInstance::getName).orElse(name)); + } + + /** + * Converts a operator assignment into an arithmetic predicate operand + */ + private Predicate getOperatorAssignmentRefinement(CtExpression element) throws LJError { + if (element instanceof CtVariableRead variableRead) { + String name = variableRead.getVariable().getSimpleName(); + if (variableRead instanceof CtFieldRead) + name = String.format(Formats.THIS, name); + return getCurrentVariableValue(name); + } else if (element instanceof CtBinaryOperator binaryOperator) { + Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand()); + Predicate right = getOperatorAssignmentRefinement(binaryOperator.getRightHandOperand()); + return Predicate.createOperation(left, getOperatorFromKind(binaryOperator.getKind()), right); + } else if (element instanceof CtLiteral literal) { + if (literal.getValue() == null) + throw new CustomError("Null literals are not supported", literal.getPosition()); + return new Predicate(literal.getValue().toString(), element); + } + // unwrap wildcard equality: _ == expr -> expr + Predicate refinement = rtc.getRefinement(element); + Expression expression = unwrapGroupExpression(refinement.getExpression()); + if (expression instanceof BinaryExpression binaryExpression && Ops.EQ.equals(binaryExpression.getOperator()) + && Keys.WILDCARD.equals(binaryExpression.getFirstOperand().toString())) { + return new Predicate(binaryExpression.getSecondOperand()); + } + return refinement; + } + + private Expression unwrapGroupExpression(Expression expression) { + while (expression instanceof GroupExpression groupExpression) + expression = groupExpression.getExpression(); + return expression; + } + /** * Retrieves the refinements for the variable write inside unary operation * From bb5ac4f91b48fd5dc44ae705c017c79143645f39 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 11 May 2026 12:33:27 +0100 Subject: [PATCH 2/3] Cover Remaining RHS Expressions --- .../testSuite/CorrectOperatorAssignments.java | 41 +++++++++++++++ .../RefinementTypeChecker.java | 2 +- .../general_checkers/OperationsChecker.java | 52 +++++++++++++++++-- 3 files changed, 90 insertions(+), 5 deletions(-) diff --git a/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java b/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java index fb466ee8..6cd580aa 100644 --- a/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java +++ b/liquidjava-example/src/main/java/testSuite/CorrectOperatorAssignments.java @@ -44,4 +44,45 @@ int remainder(@Refinement("_ >= 0") int x) { x %= 2; // x is now == 0 || x is now == 1 return x; } + + int remainderInvocation(@Refinement("_ >= 0") int x) { + @Refinement("_ == 10 || _ == 11") + int y = 10; + y += remainder(x); // x is now >= 6 + return x; + } + + @Refinement("_ == 9") + int plusUnaryInvocation() { + int y = 10; + y += -one(); + return y; + } + + @Refinement("_ == 11") + int plusConditional(@Refinement("_ >= 0") int x) { + int y = 10; + y += x >= 0 ? one() : 2; + return y; + } + + @Refinement("_ == 13") + int plusBinaryExpression() { + int y = 10; + y += one() + 2; + return y; + } + + int plusArrayRead(int[] values) { + int y = 10; + y += values[0]; + return y; + } + + @Refinement("_ == 11") + int plusCast() { + int y = 10; + y += (int) one(); + return y; + } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 9fd9bd0f..5cc2a09d 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -194,7 +194,7 @@ public void visitCtAssignment(CtAssignment assignment) th } @Override - public void visitCtOperatorAssignment(CtOperatorAssignment assignment) { + public void visitCtOperatorAssignment(CtOperatorAssignment assignment) throws LJError { super.visitCtOperatorAssignment(assignment); visitAssignment(assignment); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index b8c86bfa..22b4c55b 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -22,6 +22,7 @@ import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; +import spoon.reflect.code.CtConditional; import spoon.reflect.code.CtBinaryOperator; import spoon.reflect.code.CtExpression; import spoon.reflect.code.CtFieldRead; @@ -317,19 +318,62 @@ private Predicate getOperatorAssignmentRefinement(CtExpression element) throw Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand()); Predicate right = getOperatorAssignmentRefinement(binaryOperator.getRightHandOperand()); return Predicate.createOperation(left, getOperatorFromKind(binaryOperator.getKind()), right); + } else if (element instanceof CtConditional conditional) { + Predicate condition = getConditionRefinement(conditional.getCondition()); + Predicate thenExpression = getOperatorAssignmentRefinement(conditional.getThenExpression()); + Predicate elseExpression = getOperatorAssignmentRefinement(conditional.getElseExpression()); + return Predicate.createITE(condition, thenExpression, elseExpression); } else if (element instanceof CtLiteral literal) { if (literal.getValue() == null) throw new CustomError("Null literals are not supported", literal.getPosition()); return new Predicate(literal.getValue().toString(), element); + } else if (element instanceof CtInvocation) { + VariableInstance invocationValue = (VariableInstance) element.getMetadata(Keys.TARGET); + if (invocationValue != null) + return Predicate.createVar(invocationValue.getName()); } - // unwrap wildcard equality: _ == expr -> expr - Predicate refinement = rtc.getRefinement(element); + return valueFromRefinement(element, rtc.getRefinement(element)); + } + + private Predicate getConditionRefinement(CtExpression condition) throws LJError { + Predicate refinement = rtc.getRefinement(condition); + Optional value = unwrapWildcardEquality(refinement); + if (value.isPresent()) + return value.get(); + return refinement; + } + + private Optional unwrapWildcardEquality(Predicate refinement) { Expression expression = unwrapGroupExpression(refinement.getExpression()); if (expression instanceof BinaryExpression binaryExpression && Ops.EQ.equals(binaryExpression.getOperator()) && Keys.WILDCARD.equals(binaryExpression.getFirstOperand().toString())) { - return new Predicate(binaryExpression.getSecondOperand()); + return Optional.of(new Predicate(binaryExpression.getSecondOperand())); } - return refinement; + return Optional.empty(); + } + + private Predicate valueFromRefinement(CtExpression element, Predicate refinement) { + if (refinement == null) + return createFreshValue(element, new Predicate()); + + Optional value = unwrapWildcardEquality(refinement); + if (value.isPresent()) + return value.get(); + + Expression expression = unwrapGroupExpression(refinement.getExpression()); + boolean hasWildcard = refinement.getVariableNames().contains(Keys.WILDCARD); + if (!hasWildcard && !expression.isBooleanExpression()) + return new Predicate(expression); + + Predicate constraint = hasWildcard ? refinement : new Predicate(); + return createFreshValue(element, constraint); + } + + private Predicate createFreshValue(CtExpression element, Predicate refinement) { + String newName = String.format(Formats.FRESH, rtc.getContext().getCounter()); + Predicate freshRefinement = refinement.substituteVariable(Keys.WILDCARD, newName); + rtc.getContext().addVarToContext(newName, element.getType(), freshRefinement, element); + return Predicate.createVar(newName); } private Expression unwrapGroupExpression(Expression expression) { From 968b2cd416ed94c5f7653cca1d8588861d5eb2a2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 11 May 2026 12:35:36 +0100 Subject: [PATCH 3/3] Add ErrorOperatorAssignments --- .../testSuite/ErrorOperatorAssignments.java | 60 +++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java diff --git a/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java b/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java new file mode 100644 index 00000000..1d55d76a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorOperatorAssignments.java @@ -0,0 +1,60 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +@SuppressWarnings("unused") +public class ErrorOperatorAssignments { + + @Refinement("_ == 1") + int one() { + return 1; + } + + @Refinement("_ == 0 || _ == 1") + int remainder(@Refinement("_ >= 0") int x) { + x %= 2; + return x; + } + + @Refinement("_ == 12") + int plusInvocation(@Refinement("_ >= 0") int x) { + int y = 10; + y += remainder(x); + return y; // Refinement Error + } + + @Refinement("_ == 10") + int plusUnaryInvocation() { + int y = 10; + y += -one(); + return y; // Refinement Error + } + + @Refinement("_ == 12") + int plusConditional(@Refinement("_ >= 0") int x) { + int y = 10; + y += x >= 0 ? one() : 2; + return y; // Refinement Error + } + + @Refinement("_ == 14") + int plusBinaryExpression() { + int y = 10; + y += one() + 2; + return y; // Refinement Error + } + + @Refinement("_ == 10") + int plusArrayRead(int[] values) { + int y = 10; + y += values[0]; + return y; // Refinement Error + } + + @Refinement("_ == 12") + int plusCast() { + int y = 10; + y += (int) one(); + return y; // Refinement Error + } +}