From 2289f46e39abe86d4c6621961c665b3f09ff9133 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 21 Oct 2026 15:46:00 -0700 Subject: [PATCH] Treat all uninterpreted function results as approximate PiperOrigin-RevId: 1004290245 --- verifier/README.md | 14 ++++----- .../cel/verifier/CelAstToZ3Translator.java | 11 +++++-- .../cel/verifier/CelVerifierZ3ImplTest.java | 31 ++++++++++++++----- 3 files changed, 38 insertions(+), 18 deletions(-) diff --git a/verifier/README.md b/verifier/README.md index bd9979390..d0c054485 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -370,14 +370,12 @@ public class InvariantsExample { ### Limitations -* **Unsupported Standard Functions (Uninterpreted Functions):** Not all - CEL standard library functions have SMT axioms defined yet. Unsupported - functions are treated as *uninterpreted functions* by Z3 (the solver - only guarantees that identical inputs yield identical outputs, but does - not understand the function's internal logic or return types). - Consequently, verifications that rely on the specific semantics of - these functions may return `VerificationStatus.INCONCLUSIVE`. Support for - more standard library functions will be added incrementally. +* **Uninterpreted Functions:** Custom functions, and standard library + functions that don't have SMT axioms yet, are treated as uninterpreted: + the solver only knows that identical inputs yield identical outputs. + Results that depend on their return values are `INCONCLUSIVE`, and a + `VERIFIED` result assumes they return a value of their declared type + rather than an error. ### Best Practices & Performance diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 64cf80a99..cf0c2cab9 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -935,10 +935,15 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); - boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN); - BoolExpr isApprox = ctx.mkBool(!isDynamic); + // The solver picks the result freely, so a model depending on it is never exact. return TranslatedValue.propagateStrict( - ctx, typeSystem, functionName, callRes, Optional.of(expr), isApprox, args); + ctx, + typeSystem, + functionName, + callRes, + Optional.of(expr), + /* baseTaint= */ ctx.mkTrue(), + args); }); } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index c5bd7410a..e9af39bed 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -2750,9 +2750,9 @@ public void isAlwaysTrue_operationError_counterexampleFormat() throws Exception } @Test - public void isAlwaysTrue_dynamicFunction_nan_violated() throws Exception { - // request() == request() is a tautology only if request() does not evaluate to NaN. - // Since request() returns DYN, Z3 can assign NaN to its return value, and NaN == NaN is false. + public void isAlwaysTrue_dynamicFunction_inconclusive() throws Exception { + // request() == request() fails only if request() returns NaN. The solver may pick NaN for an + // uninterpreted function, but the actual function may never return it. CelCompiler celCompiler = CEL.toCompilerBuilder() .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) @@ -2764,8 +2764,26 @@ public void isAlwaysTrue_dynamicFunction_nan_violated() throws Exception { CelAbstractSyntaxTree ast = celCompiler.compile("request() == request()").getAst(); CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.message()).contains("depends on approximations"); + } + + @Test + public void isAlwaysTrue_dynamicFunctionShortCircuited_violated() throws Exception { + // x == 0 falsifies the condition regardless of request()'s value. + CelCompiler celCompiler = + CEL.toCompilerBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .addFunctionDeclarations( + CelFunctionDecl.newFunctionDeclaration( + "request", + CelOverloadDecl.newGlobalOverload("request_overload", SimpleType.DYN))) + .build(); + CelAbstractSyntaxTree ast = celCompiler.compile("x != 0 && request() == 1").getAst(); + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); - assertThat(result.message()).contains("request = NaN"); + assertThat(result.message()).contains("x = 0"); } @Test @@ -2785,9 +2803,8 @@ public void isAlwaysTrue_boolFunction_verified() throws Exception { } @Test - public void verifyEquivalence_functionError_equivalent() throws Exception { - // request() and request() are equivalent, even if request() throws an Error, - // because Error == Error structurally in Z3 equivalence. + public void verifyEquivalence_identicalFunctionCalls_equivalent() throws Exception { + // Identical calls to an uninterpreted function always produce identical results. CelCompiler celCompiler = CEL.toCompilerBuilder() .setContainer(CelContainer.ofName("cel.expr.conformance.proto3"))