Skip to content

Check If Refinement Predicates Are Boolean Expressions #85

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rcosta358 merged 5 commits into from
Nov 8, 2025
Merged

Check If Refinement Predicates Are Boolean Expressions #85

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
b1d6701
Check If Refinements Are Boolean Expressions
rcosta358 Nov 5, 2025
425a5b8
Check If Refinement Aliases Return Boolean Expressions
rcosta358 Nov 5, 2025
051e676
Check If State Refinement Transitions Are Boolean Expressions
rcosta358 Nov 5, 2025
89c626a
Minor Change
rcosta358 Nov 5, 2025
1700e3c
Remove Pattern Matching
rcosta358 Nov 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,8 +88,15 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
}
if (ref.isPresent()) {
Predicate p = new Predicate(ref.get(), element, errorEmitter);

// check if refinement is valid
if (!p.getExpression().isBooleanExpression()) {
ErrorHandler.printCustomError(element, "Refinement predicate must be a boolean expression",
errorEmitter);
}
if (errorEmitter.foundError())
return Optional.empty();

constr = Optional.of(p);
}
return constr;
Expand Down Expand Up @@ -245,6 +252,12 @@ protected void handleAlias(String value, CtElement element) {
}
if (klass != null && path != null) {
a.parse(path);
// refinement alias must return a boolean expression
if (a.getExpression() != null && !a.getExpression().isBooleanExpression()) {
ErrorHandler.printCustomError(element, "Refinement alias must return a boolean expression",
errorEmitter);
return;
}
AliasWrapper aw = new AliasWrapper(a, factory, WILD_VAR, context, klass, path);
context.addAlias(aw);
}
Expand Down
16 changes: 14 additions & 2 deletions ...rc/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,8 +65,15 @@ private static void setConstructorStates(RefinedFunction f, List<CtAnnotation<?
Map<String, CtExpression> m = an.getAllValues();
String to = TypeCheckingUtils.getStringFromAnnotation(m.get("to"));
ObjectState state = new ObjectState();
if (to != null)
state.setTo(new Predicate(to, element, tc.getErrorEmitter()));
if (to != null) {
Predicate p = new Predicate(to, element, tc.getErrorEmitter());
if (!p.getExpression().isBooleanExpression()) {
ErrorHandler.printCustomError(element, "State refinement transition must be a boolean expression",
tc.getErrorEmitter());
return;
}
state.setTo(p);
}
l.add(state);
}
f.setAllStates(l);
Expand Down Expand Up @@ -176,6 +183,11 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> ctAnnota
private static Predicate createStatePredicate(String value, /* RefinedFunction f */ String targetClass,
TypeChecker tc, CtElement e, boolean isTo, String prefix) throws ParsingException {
Predicate p = new Predicate(value, e, tc.getErrorEmitter(), prefix);
if (!p.getExpression().isBooleanExpression()) {
ErrorHandler.printCustomError(e, "State refinement transition must be a boolean expression",
tc.getErrorEmitter());
return new Predicate();
}
String t = targetClass; // f.getTargetClass();
CtTypeReference<?> r = tc.getFactory().Type().createReference(t);

Expand Down
24 changes: 22 additions & 2 deletions liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,6 @@
import java.util.List;
import java.util.Map;

import com.microsoft.z3.Expr;

import liquidjava.processor.context.Context;
import liquidjava.processor.facade.AliasDTO;
import liquidjava.rj_language.ast.typing.TypeInfer;
Expand Down Expand Up @@ -53,6 +51,28 @@ public boolean isLiteral() {
return this instanceof LiteralInt || this instanceof LiteralReal || this instanceof LiteralBoolean;
}

/**
* Checks if this expression produces a boolean type based on its structure
*
* @return true if it is a boolean expression, false otherwise
*/
public boolean isBooleanExpression() {
if (this instanceof LiteralBoolean || this instanceof Ite || this instanceof AliasInvocation
|| this instanceof FunctionInvocation) {
return true;
Copy link
Collaborator Author

@rcosta358 rcosta358 Nov 6, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We assume ghost and alias invocations always return boolean expressions.

Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa Nov 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

but ghosts can be ints right? like size is that an issue?

Copy link
Collaborator Author

@rcosta358 rcosta358 Nov 8, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah in that case we can't catch it there since would need the context to check if it actually returns a boolean.

}
if (this instanceof GroupExpression ge) {
return ge.getExpression().isBooleanExpression();
}
if (this instanceof BinaryExpression be) {
return be.isBooleanOperation() || be.isLogicOperation();
}
if (this instanceof UnaryExpression ue) {
return ue.getOp().equals("!");
}
return false;
}

/**
* Substitutes the expression first given expression by the second
*
Expand Down