Give each uninterpreted overload its own solver symbol

PiperOrigin-RevId: 1003517315

Author: l46kok

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<String> 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

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.