Skip to content

Commit ad083df

Browse files
CatarinaGamboaclaude
CatarinaGamboa
and
claude
authored
Fold constant bitwise and shift operations, treat others as unknown (#351)
Fixes #350. ## Problem A bitwise or shift operator in a refined argument crashed the verifier: `getOperatorFromKind` had no case for `|`, `&`, `^`, `<<`, `>>` or `>>>`, so the null operator reached a string switch (`Cannot invoke "String.hashCode()"`). Bit flags combined with `|` are the standard way to pass JDK mode constants, so correct code such as `new ZipFile(f, ZipFile.OPEN_READ | ZipFile.OPEN_DELETE)` could not be verified. ## Example ```java static void open(@refinement("_ == 1 || _ == 5") int mode) {} open(ZipFile.OPEN_READ | ZipFile.OPEN_DELETE); // was: crash; now: verifies (1 | 4 == 5) open(READ | WRITE); // static final 1 | 2 == 3: Refinement Error open(1 | extra); // unknown operand: Refinement Error (cannot prove) ``` ## Change - `StaticConstants.foldIntegral` evaluates integral compile-time constant expressions (literals, `static final` constants from source or by reflection, and arithmetic, bitwise and shift operators over them) with Java's semantics for the expression's type (`int` vs `long` overflow and shift masking). - `OperationsChecker`: where a binary operator has no counterpart in the logic, a constant expression is folded to a literal; anything else is a fresh, unconstrained value of its type, as null comparisons already are. A compound assignment such as `x |= y` leaves `x` unknown. The non-short-circuit `&`, `|` and `^` on booleans map to and, or and not-equal. - Unchanged for every operator that was already supported. ## Tests - `CorrectBitwiseConstantArgument`: literals, `static final` constants, JDK constants by reflection, nested, shifts and xor, `|=`, boolean `&`/`|`/`^`. - `ErrorBitwiseConstantArgument`: a folded constant that violates the refinement. - `ErrorBitwiseUnknownOperand`: a non-constant operand is reported as not provable instead of crashing. `mvn test`: all tests pass (369). Found while building verification exercises from real Java bugs (a passport decoder passed `OPEN_DELETE` without `OPEN_READ`; the corrected program hit this crash). 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
1 parent f4f65d7 commit ad083df

5 files changed

Lines changed: 177 additions & 4 deletions

File tree

‎liquidjava-example/src/main/java/testSuite/CorrectBitwiseConstantArgument.java‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
package testSuite;
2+
3+
import java.util.zip.ZipFile;
4+
5+
import liquidjava.specification.Refinement;
6+
7+
@SuppressWarnings("unused")
8+
public class CorrectBitwiseConstantArgument {
9+
static final int READ = 1;
10+
static final int DELETE = 4;
11+
12+
static void open(@Refinement("_ == 1 || _ == 5") int mode) {
13+
}
14+
15+
static void flags(@Refinement("_ >= 0") int f) {
16+
}
17+
18+
public static void main(String[] args) {
19+
open(1 | 4); // literals fold to 5
20+
open(READ | DELETE); // static final constants
21+
open(ZipFile.OPEN_READ | ZipFile.OPEN_DELETE); // JDK constants, by reflection
22+
open((READ | DELETE) & 5); // nested
23+
open(20 >> 2 ^ 1 << 2); // shifts and xor: 5 ^ 4 = 1
24+
int mask = 3 << 1;
25+
mask |= 1; // operator assignment: the new value is unknown, nothing is claimed about it
26+
boolean a = true, b = false;
27+
boolean both = a & b; // non-short-circuit boolean operators are and/or/not-equal
28+
boolean either = a | b;
29+
boolean differ = a ^ b;
30+
}
31+
}

‎liquidjava-example/src/main/java/testSuite/ErrorBitwiseConstantArgument.java‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorBitwiseConstantArgument {
7+
static final int READ = 1;
8+
static final int WRITE = 2;
9+
10+
static void open(@Refinement("_ == 1 || _ == 5") int mode) {
11+
}
12+
13+
public static void main(String[] args) {
14+
open(READ | WRITE); // Expect: Refinement Error
15+
}
16+
}

‎liquidjava-example/src/main/java/testSuite/ErrorBitwiseUnknownOperand.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
package testSuite;
2+
3+
import liquidjava.specification.Refinement;
4+
5+
@SuppressWarnings("unused")
6+
public class ErrorBitwiseUnknownOperand {
7+
static void open(@Refinement("_ == 1 || _ == 5") int mode) {
8+
}
9+
10+
static void m(int extra) {
11+
open(1 | extra); // Expect: Refinement Error
12+
}
13+
}

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java‎

Lines changed: 41 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@
1010
import liquidjava.processor.context.Variable;
1111
import liquidjava.processor.context.VariableInstance;
1212
import liquidjava.processor.refinement_checker.TypeChecker;
13+
import liquidjava.utils.StaticConstants;
1314
import liquidjava.utils.Utils;
1415
import liquidjava.utils.constants.Formats;
1516
import liquidjava.utils.constants.Keys;
@@ -83,10 +84,12 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
8384

8485
} else if (hasNullOperand(operator)) {
8586
oper = createFreshValue(operator, new Predicate()); // null comparisons are not supported yet: unknown value
87+
} else if (operatorFor(operator) == null) {
88+
oper = untranslatableOperation(operator);
8689
} else {
8790
Predicate varLeft = getOperationRefinements(operator, left);
8891
Predicate varRight = getOperationRefinements(operator, right);
89-
oper = Predicate.createOperation(varLeft, getOperatorFromKind(operator.getKind()), varRight);
92+
oper = Predicate.createOperation(varLeft, operatorFor(operator), varRight);
9093
}
9194
List<String> types = Arrays.asList(Types.IMPLEMENTED);
9295
if (type.contentEquals("boolean")) {
@@ -108,9 +111,12 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
108111
*/
109112
public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperatorAssignment<?, ?> assignment)
110113
throws LJError {
114+
String op = getOperatorFromKind(assignment.getKind());
115+
if (op == null) // x |= y, x <<= n, ...: no counterpart in the integer logic, so the new value is unknown
116+
return new Predicate();
111117
Predicate left = getCurrentVariableValue(assignedName);
112118
Predicate right = getOperatorAssignmentRefinement(assignment.getAssignment());
113-
Predicate operation = Predicate.createOperation(left, getOperatorFromKind(assignment.getKind()), right);
119+
Predicate operation = Predicate.createOperation(left, op, right);
114120
return Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), operation);
115121
}
116122

@@ -241,9 +247,11 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
241247
} else if (element instanceof CtBinaryOperator<?> binop) {
242248
if (hasNullOperand(binop)) // null comparisons are not supported yet: unknown boolean value
243249
return createFreshValue(binop, new Predicate());
250+
if (operatorFor(binop) == null)
251+
return untranslatableOperation(binop);
244252
Predicate right = getOperationRefinements(operator, parentVar, binop.getRightHandOperand());
245253
Predicate left = getOperationRefinements(operator, parentVar, binop.getLeftHandOperand());
246-
return Predicate.createOperation(left, getOperatorFromKind(binop.getKind()), right);
254+
return Predicate.createOperation(left, operatorFor(binop), right);
247255
} else if (element instanceof CtUnaryOperator<?>) {
248256
Predicate a = (Predicate) element.getMetadata(Keys.REFINEMENT);
249257
a = a.substituteVariable(Keys.WILDCARD, "");
@@ -354,9 +362,11 @@ private Predicate getOperatorAssignmentRefinement(CtExpression<?> element) throw
354362
name = Utils.qualifyFieldName(fieldRead.getVariable());
355363
return getCurrentVariableValue(name);
356364
} else if (element instanceof CtBinaryOperator<?> binaryOperator) {
365+
if (operatorFor(binaryOperator) == null)
366+
return untranslatableOperation(binaryOperator);
357367
Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand());
358368
Predicate right = getOperatorAssignmentRefinement(binaryOperator.getRightHandOperand());
359-
return Predicate.createOperation(left, getOperatorFromKind(binaryOperator.getKind()), right);
369+
return Predicate.createOperation(left, operatorFor(binaryOperator), right);
360370
} else if (element instanceof CtConditional<?> conditional) {
361371
Predicate condition = getConditionRefinement(conditional.getCondition());
362372
Predicate thenExpression = getOperatorAssignmentRefinement(conditional.getThenExpression());
@@ -443,6 +453,33 @@ private <T> Predicate getRefinementUnaryVariableWrite(CtExpression<T> ex, CtUnar
443453
// ############################### Operations Auxiliaries
444454
// ##########################################
445455

456+
/**
457+
* The logic's operator for a binary operation, or {@code null} when it has none. On booleans the non-short-circuit
458+
* {@code &}, {@code |} and {@code ^} are exactly and, or and not-equal; on integers the bitwise and shift operators
459+
* have no counterpart in the linear integer logic.
460+
*/
461+
private String operatorFor(CtBinaryOperator<?> op) {
462+
String o = getOperatorFromKind(op.getKind());
463+
if (o != null || op.getType() == null || !"boolean".equals(op.getType().unbox().getSimpleName()))
464+
return o;
465+
return switch (op.getKind()) {
466+
case BITAND -> Ops.AND;
467+
case BITOR -> Ops.OR;
468+
case BITXOR -> Ops.NEQ;
469+
default -> null;
470+
};
471+
}
472+
473+
/**
474+
* A bitwise or shift operation on integers: a compile-time constant expression (e.g.
475+
* {@code ZipFile.OPEN_READ | ZipFile.OPEN_DELETE}) is folded to its value; anything else is an unconstrained value
476+
* of its type, so a refinement that depends on it is reported as not provable instead of crashing (#350).
477+
*/
478+
private Predicate untranslatableOperation(CtBinaryOperator<?> op) {
479+
Predicate literal = StaticConstants.asLiteralPredicate(StaticConstants.foldIntegral(op));
480+
return literal != null ? literal : createFreshValue(op, new Predicate());
481+
}
482+
446483
/**
447484
* Get the String value of the operator from the enum
448485
*

‎liquidjava-verifier/src/main/java/liquidjava/utils/StaticConstants.java‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,11 @@
77
import liquidjava.rj_language.ast.LiteralChar;
88
import liquidjava.rj_language.ast.LiteralString;
99
import liquidjava.utils.constants.Types;
10+
import spoon.reflect.code.CtBinaryOperator;
11+
import spoon.reflect.code.CtExpression;
12+
import spoon.reflect.code.CtFieldRead;
1013
import spoon.reflect.code.CtLiteral;
14+
import spoon.reflect.code.CtUnaryOperator;
1115
import spoon.reflect.declaration.CtCompilationUnit;
1216
import spoon.reflect.declaration.CtElement;
1317
import spoon.reflect.declaration.CtField;
@@ -159,6 +163,78 @@ private static String packageName(CtType<?> type) {
159163
return type.getPackage().getQualifiedName();
160164
}
161165

166+
/**
167+
* Evaluate an integral compile-time constant expression: integer literals, {@code static final} constants (see
168+
* {@link #resolve(CtFieldReference)}) and the arithmetic, bitwise and shift operators over them, e.g.
169+
* {@code ZipFile.OPEN_READ | ZipFile.OPEN_DELETE}. The result has Java's own semantics for the expression's type
170+
* ({@code int} wraps and masks shift distances to 5 bits, {@code long} to 6). Returns {@code null} when any part is
171+
* not a constant, or on division by zero.
172+
*/
173+
public static Number foldIntegral(CtExpression<?> e) {
174+
if (e instanceof CtLiteral<?> lit)
175+
return integral(lit.getValue());
176+
if (e instanceof CtFieldRead<?> fr)
177+
return integral(resolve(fr.getVariable()));
178+
boolean isLong = e.getType() != null && "long".equals(e.getType().unbox().getSimpleName());
179+
if (e instanceof CtUnaryOperator<?> un) {
180+
Number v = foldIntegral(un.getOperand());
181+
if (v == null)
182+
return null;
183+
return switch (un.getKind()) {
184+
case NEG -> isLong ? (Number) (-v.longValue()) : (Number) (-v.intValue());
185+
case COMPL -> isLong ? (Number) (~v.longValue()) : (Number) (~v.intValue());
186+
case POS -> v;
187+
default -> null;
188+
};
189+
}
190+
if (e instanceof CtBinaryOperator<?> bin) {
191+
Number l = foldIntegral(bin.getLeftHandOperand()), r = foldIntegral(bin.getRightHandOperand());
192+
if (l == null || r == null)
193+
return null;
194+
if (isLong) {
195+
long a = l.longValue(), b = r.longValue();
196+
return switch (bin.getKind()) {
197+
case BITOR -> a | b;
198+
case BITAND -> a & b;
199+
case BITXOR -> a ^ b;
200+
case SL -> a << b;
201+
case SR -> a >> b;
202+
case USR -> a >>> b;
203+
case PLUS -> a + b;
204+
case MINUS -> a - b;
205+
case MUL -> a * b;
206+
case DIV -> b == 0 ? null : a / b;
207+
case MOD -> b == 0 ? null : a % b;
208+
default -> null;
209+
};
210+
}
211+
int a = l.intValue(), b = r.intValue();
212+
return switch (bin.getKind()) {
213+
case BITOR -> a | b;
214+
case BITAND -> a & b;
215+
case BITXOR -> a ^ b;
216+
case SL -> a << b;
217+
case SR -> a >> b;
218+
case USR -> a >>> b;
219+
case PLUS -> a + b;
220+
case MINUS -> a - b;
221+
case MUL -> a * b;
222+
case DIV -> b == 0 ? null : a / b;
223+
case MOD -> b == 0 ? null : a % b;
224+
default -> null;
225+
};
226+
}
227+
return null;
228+
}
229+
230+
private static Number integral(Object v) {
231+
if (v instanceof Integer || v instanceof Long || v instanceof Short || v instanceof Byte)
232+
return (Number) v;
233+
if (v instanceof Character c)
234+
return (int) c;
235+
return null;
236+
}
237+
162238
/** Wrap a resolved value as an RJ literal predicate, or {@code null} if its type is not modeled. */
163239
public static Predicate asLiteralPredicate(Object value) {
164240
if (value instanceof Boolean)

0 commit comments

Comments
 (0)