Skip to content

Commit 7a8de62

Browse files
rcosta358rcosta358
committed
Add Null & Boxed Types Support
1 parent 1b290cb commit 7a8de62

15 files changed

Lines changed: 179 additions & 24 deletions

File tree

‎liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,8 @@ literal:
5858
BOOL
5959
| STRING
6060
| INT
61-
| REAL;
61+
| REAL
62+
| NULL;
6263

6364
//----------------------- Declarations -----------------------
6465

@@ -89,6 +90,7 @@ BOOLOP : '=='|'!='|'>='|'>'|'<='|'<';
8990
ARITHOP : '+'|'*'|'/'|'%';//|'-';
9091

9192
BOOL : 'true' | 'false';
93+
NULL : 'null';
9294
ID_UPPER: ([A-Z][a-zA-Z0-9]*);
9395
OBJECT_TYPE:
9496
(([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);

‎liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java‎

Lines changed: 13 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,8 +13,11 @@
1313
import liquidjava.processor.refinement_checker.object_checkers.AuxStateHandler;
1414
import liquidjava.rj_language.BuiltinFunctionPredicate;
1515
import liquidjava.rj_language.Predicate;
16+
import liquidjava.rj_language.ast.LiteralNull;
17+
import liquidjava.utils.Utils;
1618
import liquidjava.utils.constants.Formats;
1719
import liquidjava.utils.constants.Keys;
20+
import liquidjava.utils.constants.Ops;
1821
import liquidjava.utils.constants.Types;
1922

2023
import org.apache.commons.lang3.NotImplementedException;
@@ -136,6 +139,9 @@ public <T> void visitCtLocalVariable(CtLocalVariable<T> localVariable) {
136139
if (refinementFound == null) {
137140
refinementFound = new Predicate();
138141
}
142+
if (Utils.isBoxedType(localVariable.getType()) && !Utils.isNullLiteral(e)) {
143+
refinementFound = Predicate.createConjunction(refinementFound, Predicate.createNonNullEq());
144+
}
139145
context.addVarToContext(varName, localVariable.getType(), new Predicate(), e);
140146
checkVariableRefinements(refinementFound, varName, localVariable.getType(), localVariable, localVariable);
141147
AuxStateHandler.addStateRefinements(this, varName, e);
@@ -219,9 +225,9 @@ public <T> void visitCtLiteral(CtLiteral<T> lit) {
219225
Predicate.createLit(lit.getValue().toString(), type)));
220226

221227
} else if (lit.getType().getQualifiedName().equals("java.lang.String")) {
222-
// Only taking care of strings inside refinements
228+
lit.putMetadata(Keys.REFINEMENT, Predicate.createNonNullEq());
223229
} else if (type.equals(Types.NULL)) {
224-
// Skip null literals
230+
lit.putMetadata(Keys.REFINEMENT, Predicate.createNullEq());
225231
} else {
226232
throw new NotImplementedException(
227233
String.format("Literal of type %s not implemented:", lit.getType().getQualifiedName()));
@@ -373,12 +379,14 @@ public <T> void visitCtConditional(CtConditional<T> conditional) {
373379
@Override
374380
public <T> void visitCtConstructorCall(CtConstructorCall<T> ctConstructorCall) {
375381
super.visitCtConstructorCall(ctConstructorCall);
382+
ctConstructorCall.putMetadata(Keys.REFINEMENT, Predicate.createNonNullEq());
376383
mfc.getConstructorInvocationRefinements(ctConstructorCall);
377384
}
378385

379386
@Override
380387
public <T> void visitCtNewClass(CtNewClass<T> newClass) {
381388
super.visitCtNewClass(newClass);
389+
newClass.putMetadata(Keys.REFINEMENT, Predicate.createNonNullEq());
382390
}
383391

384392
// ############################### Inner Visitors
@@ -396,6 +404,9 @@ private void checkAssignment(String name, CtTypeReference<?> type, CtExpression<
396404
refinementFound = new Predicate();
397405
}
398406
}
407+
if (Utils.isBoxedType(type) && !Utils.isNullLiteral(assignment)) {
408+
refinementFound = Predicate.createConjunction(refinementFound, Predicate.createNonNullEq());
409+
}
399410
Optional<VariableInstance> r = context.getLastVariableInstance(name);
400411
// AQUI!!
401412
r.ifPresent(variableInstance -> vcChecker.removePathVariableThatIncludes(variableInstance.getName()));

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -221,7 +221,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
221221
return new Predicate();
222222
}
223223
if (l.getValue() == null)
224-
throw new CustomError("Null literals are not supported");
224+
return new Predicate("null", element);
225225

226226
return new Predicate(l.getValue().toString(), element);
227227

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,7 @@
66
import java.util.Map;
77
import java.util.stream.Collectors;
88

9-
import liquidjava.diagnostics.errors.ArgumentMismatchError;
109
import liquidjava.diagnostics.errors.LJError;
11-
import liquidjava.diagnostics.errors.SyntaxError;
1210
import liquidjava.processor.context.AliasWrapper;
1311
import liquidjava.processor.context.Context;
1412
import liquidjava.processor.context.GhostFunction;
@@ -22,6 +20,7 @@
2220
import liquidjava.rj_language.ast.LiteralBoolean;
2321
import liquidjava.rj_language.ast.LiteralInt;
2422
import liquidjava.rj_language.ast.LiteralLong;
23+
import liquidjava.rj_language.ast.LiteralNull;
2524
import liquidjava.rj_language.ast.LiteralReal;
2625
import liquidjava.rj_language.ast.UnaryExpression;
2726
import liquidjava.rj_language.ast.Var;
@@ -255,4 +254,12 @@ public static Predicate createInvocation(String name, Predicate... Predicates) {
255254
le.add(c.getExpression());
256255
return new Predicate(new FunctionInvocation(name, le));
257256
}
257+
258+
public static Predicate createNonNullEq() {
259+
return Predicate.createOperation(Predicate.createVar(Keys.WILDCARD), Ops.NEQ, new Predicate(new LiteralNull()));
260+
}
261+
262+
public static Predicate createNullEq() {
263+
return Predicate.createOperation(Predicate.createVar(Keys.WILDCARD), Ops.EQ, new Predicate(new LiteralNull()));
264+
}
258265
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@ public void setChild(int index, Expression element) {
6767

6868
public boolean isLiteral() {
6969
return this instanceof LiteralInt || this instanceof LiteralLong || this instanceof LiteralReal
70-
|| this instanceof LiteralBoolean;
70+
|| this instanceof LiteralBoolean || this instanceof LiteralNull;
7171
}
7272

7373
/**

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralNull.java‎

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
package liquidjava.rj_language.ast;
2+
3+
import java.util.List;
4+
5+
import liquidjava.diagnostics.errors.LJError;
6+
import liquidjava.rj_language.visitors.ExpressionVisitor;
7+
8+
public class LiteralNull extends Expression {
9+
10+
@Override
11+
public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
12+
return visitor.visitLiteralNull(this);
13+
}
14+
15+
@Override
16+
public String toString() {
17+
return "null";
18+
}
19+
20+
@Override
21+
public void getVariableNames(List<String> toAdd) {
22+
// end leaf
23+
}
24+
25+
@Override
26+
public void getStateInvocations(List<String> toAdd, List<String> all) {
27+
// end leaf
28+
}
29+
30+
@Override
31+
public Expression clone() {
32+
return new LiteralNull();
33+
}
34+
35+
@Override
36+
public boolean isBooleanTrue() {
37+
return false;
38+
}
39+
40+
@Override
41+
public int hashCode() {
42+
return 31;
43+
}
44+
45+
@Override
46+
public boolean equals(Object obj) {
47+
return obj != null && getClass() == obj.getClass();
48+
}
49+
}

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import liquidjava.rj_language.ast.LiteralBoolean;
1313
import liquidjava.rj_language.ast.LiteralInt;
1414
import liquidjava.rj_language.ast.LiteralLong;
15+
import liquidjava.rj_language.ast.LiteralNull;
1516
import liquidjava.rj_language.ast.LiteralReal;
1617
import liquidjava.rj_language.ast.LiteralString;
1718
import liquidjava.rj_language.ast.UnaryExpression;
@@ -24,6 +25,8 @@
2425
public class TypeInfer {
2526

2627
public static boolean checkCompatibleType(String type, Expression e, Context ctx, Factory factory) {
28+
if (e instanceof LiteralNull)
29+
return !Utils.isPrimitiveType(type);
2730
Optional<CtTypeReference<?>> t1 = getType(ctx, factory, e);
2831
CtTypeReference<?> t2 = Utils.getType(type, factory);
2932
return t1.isPresent() && t1.get().equals(t2);
@@ -40,6 +43,8 @@ else if (e instanceof LiteralReal)
4043
return Optional.of(Utils.getType("double", factory));
4144
else if (e instanceof LiteralBoolean)
4245
return boolType(factory);
46+
else if (e instanceof LiteralNull)
47+
return Optional.of(Utils.getType("java.lang.Object", factory));
4348
else if (e instanceof Var)
4449
return varType(ctx, (Var) e);
4550
else if (e instanceof UnaryExpression)

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/ExpressionSimplifier.java‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
import liquidjava.rj_language.ast.BinaryExpression;
44
import liquidjava.rj_language.ast.Expression;
55
import liquidjava.rj_language.ast.LiteralBoolean;
6+
import liquidjava.rj_language.ast.LiteralNull;
67
import liquidjava.rj_language.opt.derivation_node.BinaryDerivationNode;
78
import liquidjava.rj_language.opt.derivation_node.DerivationNode;
89
import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
@@ -58,6 +59,12 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod
5859
rightSimplified = simplifyValDerivationNode(new ValDerivationNode(binExp.getSecondOperand(), null));
5960
}
6061

62+
// remove null check when equality already implies non-null
63+
if (isNullCheckImpliedBy(rightSimplified.getValue(), leftSimplified.getValue()))
64+
return leftSimplified;
65+
if (isNullCheckImpliedBy(leftSimplified.getValue(), rightSimplified.getValue()))
66+
return rightSimplified;
67+
6168
// check if either side is redundant
6269
if (isRedundant(leftSimplified.getValue()))
6370
return rightSimplified;
@@ -83,6 +90,9 @@ private static ValDerivationNode simplifyValDerivationNode(ValDerivationNode nod
8390
return node;
8491
}
8592

93+
/**
94+
* Checks if a binary expression is of the form x == y && y == x, which can be simplified to x == y
95+
*/
8696
private static boolean isSymmetricEquality(Expression left, Expression right) {
8797
if (left instanceof BinaryExpression b1 && "==".equals(b1.getOperator()) && right instanceof BinaryExpression b2
8898
&& "==".equals(b2.getOperator())) {
@@ -96,6 +106,36 @@ private static boolean isSymmetricEquality(Expression left, Expression right) {
96106
return false;
97107
}
98108

109+
/**
110+
* Checks if a null check (x != null) is implied by an equality check (x == y) where y is not null
111+
*/
112+
private static boolean isNullCheckImpliedBy(Expression nullCheck, Expression context) {
113+
114+
// check if in form of x != null
115+
if (!(nullCheck instanceof BinaryExpression nb) || !"!=".equals(nb.getOperator()))
116+
return false;
117+
118+
// identify the variable being checked for null
119+
Expression checkedVar;
120+
if (nb.getFirstOperand() instanceof LiteralNull && !(nb.getSecondOperand() instanceof LiteralNull)) {
121+
checkedVar = nb.getSecondOperand();
122+
} else if (nb.getSecondOperand() instanceof LiteralNull && !(nb.getFirstOperand() instanceof LiteralNull)) {
123+
checkedVar = nb.getFirstOperand();
124+
} else {
125+
return false;
126+
}
127+
128+
// check if context contains an equality check of the form x == y where y is not null
129+
if (!(context instanceof BinaryExpression cb) || !"==".equals(cb.getOperator()))
130+
return false;
131+
132+
// check if either side of the equality is the checked variable and the other side is not null
133+
Expression left = cb.getFirstOperand();
134+
Expression right = cb.getSecondOperand();
135+
return (left.equals(checkedVar) && !(right instanceof LiteralNull))
136+
|| (right.equals(checkedVar) && !(left instanceof LiteralNull));
137+
}
138+
99139
/**
100140
* Checks if an expression is redundant (e.g. true or x == x)
101141
*/

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/derivation_node/ValDerivationNode.java‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
import liquidjava.rj_language.ast.LiteralBoolean;
1414
import liquidjava.rj_language.ast.LiteralInt;
1515
import liquidjava.rj_language.ast.LiteralLong;
16+
import liquidjava.rj_language.ast.LiteralNull;
1617
import liquidjava.rj_language.ast.LiteralReal;
1718
import liquidjava.rj_language.ast.Var;
1819

@@ -49,6 +50,8 @@ public JsonElement serialize(Expression exp, Type typeOfSrc, JsonSerializationCo
4950
return new JsonPrimitive(((LiteralReal) exp).getValue());
5051
if (exp instanceof LiteralBoolean)
5152
return new JsonPrimitive(exp.isBooleanTrue());
53+
if (exp instanceof LiteralNull)
54+
return JsonNull.INSTANCE;
5255
if (exp instanceof Var)
5356
return new JsonPrimitive(((Var) exp).getName());
5457
return new JsonPrimitive(exp.toString());

‎liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java‎

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,6 @@
44
import java.util.List;
55

66
import liquidjava.diagnostics.errors.LJError;
7-
import liquidjava.diagnostics.errors.SyntaxError;
87
import liquidjava.rj_language.ast.AliasInvocation;
98
import liquidjava.rj_language.ast.BinaryExpression;
109
import liquidjava.rj_language.ast.Expression;
@@ -16,6 +15,7 @@
1615
import liquidjava.rj_language.ast.LiteralLong;
1716
import liquidjava.rj_language.ast.LiteralReal;
1817
import liquidjava.rj_language.ast.LiteralString;
18+
import liquidjava.rj_language.ast.LiteralNull;
1919
import liquidjava.rj_language.ast.UnaryExpression;
2020
import liquidjava.rj_language.ast.Var;
2121
import liquidjava.utils.Utils;
@@ -53,7 +53,6 @@
5353
import rj.grammar.RJParser.StartPredContext;
5454
import rj.grammar.RJParser.TargetInvocationContext;
5555
import rj.grammar.RJParser.VarContext;
56-
import spoon.reflect.cu.SourcePosition;
5756
import liquidjava.diagnostics.errors.ArgumentMismatchError;
5857

5958
/**
@@ -200,13 +199,12 @@ else if (literalContext.STRING() != null)
200199
else if (literalContext.INT() != null) {
201200
String text = literalContext.INT().getText();
202201
long value = Long.parseLong(text);
203-
if (value <= Integer.MAX_VALUE && value >= Integer.MIN_VALUE) {
204-
return new LiteralInt((int) value);
205-
} else {
206-
return new LiteralLong(value);
207-
}
202+
return value <= Integer.MAX_VALUE && value >= Integer.MIN_VALUE ? new LiteralInt((int) value)
203+
: new LiteralLong(value);
208204
} else if (literalContext.REAL() != null)
209205
return new LiteralReal(literalContext.REAL().getText());
206+
else if (literalContext.NULL() != null)
207+
return new LiteralNull();
210208
throw new NotImplementedException("Literal type not implemented");
211209
}
212210
}

0 commit comments

Comments
 (0)