Skip to content

Commit efeafc5

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Add axioms for comparison operators for booleans
PiperOrigin-RevId: 1004349459
1 parent 6ef4a7b commit efeafc5

6 files changed

Lines changed: 69 additions & 0 deletions

File tree

‎verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,14 @@ Optional<TranslatedValue> translateFunctionCall(
8585
return opOpt.isPresent() ? Optional.of(resultChain) : Optional.empty();
8686
}
8787

88+
// A candidate overload without an axiom (e.g. a custom overload of a standard operator) is
89+
// treated as an uninterpreted call, rather than falling through to the type-mismatch error.
90+
if (reference != null
91+
&& reference.overloadIds().stream()
92+
.anyMatch(id -> !functionRegistry.getTranslator(id).isPresent())) {
93+
return Optional.empty();
94+
}
95+
8896
boolean matchedAny = false;
8997
Expr<?> currentZ3Result = resultChain.z3Expr();
9098
BoolExpr currentApprox = resultChain.isApproximate();

‎verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class GreaterAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.GREATER_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkAnd(
36+
(BoolExpr) typeSystem.unwrapBool(lhs),
37+
ctx.mkNot((BoolExpr) typeSystem.unwrapBool(rhs))))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.GREATER_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

‎verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class GreaterEqualsAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER_EQUALS.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.GREATER_EQUALS_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkImplies(
36+
(BoolExpr) typeSystem.unwrapBool(rhs),
37+
(BoolExpr) typeSystem.unwrapBool(lhs)))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.GREATER_EQUALS_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

‎verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class LessAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.LESS.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.LESS_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkAnd(
36+
ctx.mkNot((BoolExpr) typeSystem.unwrapBool(lhs)),
37+
(BoolExpr) typeSystem.unwrapBool(rhs)))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.LESS_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

‎verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class LessEqualsAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.LESS_EQUALS.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.LESS_EQUALS_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkImplies(
36+
(BoolExpr) typeSystem.unwrapBool(lhs),
37+
(BoolExpr) typeSystem.unwrapBool(rhs)))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.LESS_EQUALS_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

‎verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -554,6 +554,10 @@ public void isSatisfiable_timeout_throwsException() throws Exception {
554554

555555
private enum IsAlwaysTrueTestCase {
556556
LOGICAL_OR_CONSTANTS("true || false"),
557+
BOOL_ORDERING(
558+
"false < true && !(true < false) && false <= true && !(true <= false) && true > false"
559+
+ " && !(false > true) && true >= false && !(false >= true)"),
560+
BOOL_ORDERING_REFLEXIVE("a <= a && a >= a && !(a < a) && !(a > a)"),
557561
TIMESTAMP_GREATER_EQUALS("timestamp(200) >= timestamp(100)"),
558562
DURATION_GREATER_EQUALS(
559563
"(timestamp(200) - timestamp(100)) >= (timestamp(150) - timestamp(100))"),
@@ -2853,6 +2857,27 @@ public void verifyEquivalence_identicalFunctionCalls_equivalent() throws Excepti
28532857
assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
28542858
}
28552859

2860+
@Test
2861+
public void isSatisfiable_customOperatorOverload_inconclusive() throws Exception {
2862+
// The custom overload has no axiom, so it must not fall through to the type-mismatch error.
2863+
CelCompiler celCompiler =
2864+
CEL.toCompilerBuilder()
2865+
.addFunctionDeclarations(
2866+
CelFunctionDecl.newFunctionDeclaration(
2867+
Operator.LESS.getFunction(),
2868+
CelOverloadDecl.newGlobalOverload(
2869+
"less_list_int",
2870+
SimpleType.BOOL,
2871+
ListType.create(SimpleType.INT),
2872+
ListType.create(SimpleType.INT))))
2873+
.build();
2874+
CelAbstractSyntaxTree ast = celCompiler.compile("!(int_list < int_list_2)").getAst();
2875+
2876+
CelVerificationResult result = VERIFIER.isSatisfiable(ast);
2877+
2878+
assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
2879+
}
2880+
28562881
@Test
28572882
@SuppressWarnings("GoodTime-ApiWithNumericTimeUnit") // Test only
28582883
public void setTimeout_invalidDuration_throws(@TestParameter({"0", "-1"}) long timeoutSeconds) {

0 commit comments

Comments
 (0)