Check If Refinement Predicates Are Boolean Expressions (#85)

Author: rcosta358

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java

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

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

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

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

@@ -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;
@@ -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;
+        }
+        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
      *