Check If Refinements Are Boolean Expressions

Author: rcosta358

liquidjava-verifier/pom.xml

@@ -95,6 +95,17 @@
 					</execution>
 				</executions>
 			</plugin>
+			<plugin>
+				<groupId>org.apache.maven.plugins</groupId>
+				<artifactId>maven-compiler-plugin</artifactId>
+				<version>3.11.0</version>
+				<configuration>
+					<release>24</release>
+					<compilerArgs>
+						<arg>--enable-preview</arg>
+					</compilerArgs>
+				</configuration>
+			</plugin>
 		</plugins>
 	</build>
 

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;

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,20 @@ 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() {
+        return switch (this) {
+            case LiteralBoolean _, Ite _, AliasInvocation _, FunctionInvocation _ -> true;
+            case GroupExpression ge -> ge.getExpression().isBooleanExpression();
+            case BinaryExpression be -> be.isBooleanOperation() || be.isLogicOperation();
+            case UnaryExpression ue -> ue.getOp().equals("!");
+            default -> false;
+        };
+    }
+
     /**
      * Substitutes the expression first given expression by the second
      *