From 409cd495662fbf12b4f5c63b2e964bc340732b5f Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 21 Oct 2026 15:58:09 -0700 Subject: [PATCH] Give each uninterpreted overload its own solver symbol PiperOrigin-RevId: 1004298455 --- .../cel/verifier/CelAstToZ3Translator.java | 18 ++++++- .../cel/verifier/CelVerifierZ3ImplTest.java | 51 +++++++++++++++++++ 2 files changed, 68 insertions(+), 1 deletion(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index cf0c2cab9..913582ee4 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -16,6 +16,7 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; +import com.google.common.collect.ImmutableSortedSet; import com.google.common.collect.Iterables; import com.google.common.collect.Streams; import com.microsoft.z3.ArithExpr; @@ -83,6 +84,7 @@ final class CelAstToZ3Translator { private static final String EMPTY_MSG_REF_PREFIX = "!empty_msg_ref_"; private static final String EMPTY_LIST_PREFIX = "!empty_list"; private static final String EMPTY_MAP_PREFIX = "!empty_map"; + private static final String FUNCTION_PREFIX = "!fn_"; private static final String NULL_VALUE_FIELD = "null_value"; private static final String SECONDS_FIELD = "seconds"; private static final String NANOS_FIELD = "nanos"; @@ -927,7 +929,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { Sort[] argSorts = new Sort[args.size()]; Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort()); FuncDecl funcDecl = - typeSystem.internFuncDecl(functionName, argSorts, typeSystem.celValueSort()); + typeSystem.internFuncDecl( + uninterpretedFunctionSymbol(exprId, ast), + argSorts, + typeSystem.celValueSort()); Expr[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new); Expr callRes = ctx.mkApp(funcDecl, exprArgs); @@ -947,6 +952,17 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { }); } + /** + * Returns the Z3 symbol for an uninterpreted call. Each set of candidate overloads gets its own + * symbol, since distinct overloads may have different implementations even on equal values (e.g. + * empty lists of different element types). The prefix keeps it apart from variables and internal + * symbols. + */ + private static String uninterpretedFunctionSymbol(long exprId, CelAbstractSyntaxTree ast) { + ImmutableList overloadIds = ast.getReferenceOrThrow(exprId).overloadIds(); + return FUNCTION_PREFIX + String.join("|", ImmutableSortedSet.copyOf(overloadIds)); + } + /** * Whether a call may construct a container that embeds its args (e.g. list concatenation, map * insertion or optional.of). Indexing and conditionals return existing values instead, so diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index e9af39bed..e207d0d06 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -2802,6 +2802,57 @@ public void isAlwaysTrue_boolFunction_verified() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } + // Each pair of calls looks alike but may have different implementations, so equating them would + // be a false VERIFIED. Any counterexample depends on the values the functions return. + @Test + public void isAlwaysTrue_distinctFunctionSymbols_inconclusive( + @TestParameter({ + // Member and global overloads of the same name. + "fx(role, country) == role.fx(country)", + // Overloads whose argument values coincide (empty lists of different element types). + "size(int_list) == 0 && size(string_list) == 0 ? f(int_list) == f(string_list) : true" + }) + String expression) + throws Exception { + CelCompiler celCompiler = + CEL.toCompilerBuilder() + .addVar("string_list", ListType.create(SimpleType.STRING)) + .addFunctionDeclarations( + CelFunctionDecl.newFunctionDeclaration( + "fx", + CelOverloadDecl.newGlobalOverload( + "fx_global", SimpleType.BOOL, SimpleType.STRING, SimpleType.STRING), + CelOverloadDecl.newMemberOverload( + "fx_member", SimpleType.BOOL, SimpleType.STRING, SimpleType.STRING)), + CelFunctionDecl.newFunctionDeclaration( + "f", + CelOverloadDecl.newGlobalOverload( + "f_list_int", SimpleType.INT, ListType.create(SimpleType.INT)), + CelOverloadDecl.newGlobalOverload( + "f_list_string", SimpleType.INT, ListType.create(SimpleType.STRING)))) + .build(); + CelAbstractSyntaxTree ast = celCompiler.compile(expression).getAst(); + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + + @Test + public void isAlwaysTrue_zeroArityFunctionAndSameNamedVariable_inconclusive() throws Exception { + CelCompiler celCompiler = + CEL.toCompilerBuilder() + .addVar("g", SimpleType.INT) + .addFunctionDeclarations( + CelFunctionDecl.newFunctionDeclaration( + "g", CelOverloadDecl.newGlobalOverload("g_zero", SimpleType.INT))) + .build(); + CelAbstractSyntaxTree ast = celCompiler.compile("g() == g").getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + @Test public void verifyEquivalence_identicalFunctionCalls_equivalent() throws Exception { // Identical calls to an uninterpreted function always produce identical results.