Check If Refinement Predicates Are Boolean Expressions

[rcosta358]

Previously, we weren't checking if refinement predicates were actually boolean expressions, and this was only caught by the SMT solver.

Examples

Refinements

public class InvalidRefinement {
    void example() {
        @Refinement("_ + 1") // not a boolean expression
        int x = 5;
    }
}

Before

Found Error: class com.microsoft.z3.IntExpr cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.IntExpr and com.microsoft.z3.BoolExpr are in unnamed module of loader org.codehaus.mojo.exec.URLClassLoaderBuilder$ExecJavaClassLoader @7a729f84)

After

Found Error: Refinement predicate must be a boolean expression

Refinement Aliases

@RefinementAlias("Test(int v) { v }") // does not return a boolean expression
public class InvalidRefinementAlias {

    void example() {
        @Refinement("Test(_)")
        int x = 1;
    }
}

Before

Found Error: class com.microsoft.z3.IntExpr cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.IntExpr and com.microsoft.z3.BoolExpr are in unnamed module of loader org.codehaus.mojo.exec.URLClassLoaderBuilder$ExecJavaClassLoader @78d6447a)

After

Found Error: Refinement alias must return a boolean expression

State Refinements

public class InvalidStateRefinementFrom {

    @StateRefinement(from="123") // not a boolean expression
    void example() {}
}

Before:

class com.microsoft.z3.IntNum cannot be cast to class com.microsoft.z3.BoolExpr (com.microsoft.z3.IntNum and com.microsoft.z3.BoolExpr are in unnamed module of loader org.codehaus.mojo.exec.URLClassLoaderBuilder$ExecJavaClassLoader @38bb9d7a)

After

Found Error: State refinement transition must be a boolean expression

The same happens with state refinements in constructors and with to transitions.

[rcosta358]

We assume ghost and alias invocations always return boolean expressions.

[CatarinaGamboa]

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

[rcosta358]

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

[CatarinaGamboa]

LGTM. We should also have tests that check if the right error message is sent and not just if the verifier fails or not, I'll add a issue with that and we can discuss it later