Implement JSON value unwrapping capability in verifier

PiperOrigin-RevId: 954872975

Author: l46kok

verifier/src/main/java/dev/cel/verifier/BUILD.bazel

@@ -129,6 +129,7 @@ java_library(
         "//common/ast",
         "//common/ast:cel_block",
         "//common/types",
+        "//common/types:cel_types",
         "//common/types:type_providers",
         "//verifier/axioms",
         "@maven//:com_google_errorprone_error_prone_annotations",

verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

@@ -37,6 +37,7 @@
 import dev.cel.common.types.CelKind;
 import dev.cel.common.types.CelType;
 import dev.cel.common.types.CelTypeProvider;
+import dev.cel.common.types.CelTypes;
 import dev.cel.common.types.ListType;
 import dev.cel.common.types.MapType;
 import dev.cel.common.types.NullableType;
@@ -79,6 +80,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 NULL_VALUE_FIELD = "null_value";
   private final Context ctx;
   private final CelZ3TypeSystem typeSystem;
   private final CelZ3OperatorTranslator operatorTranslator;
@@ -370,6 +372,10 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
 
   private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
     CelExpr.CelStruct createStruct = celExpr.struct();
+    if (isJsonWkt(createStruct.messageName())) {
+      return translateJsonWktStruct(celExpr, createStruct, ast);
+    }
+
     // Bypass SMT when the struct is empty (return the cached SMT default pointer)
     if (createStruct.entries().isEmpty()) {
       return TranslatedValue.create(
@@ -448,6 +454,56 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
     return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
   }
 
+  private static boolean isJsonWkt(String messageName) {
+    return messageName.equals(CelTypes.VALUE_MESSAGE)
+        || messageName.equals(CelTypes.LIST_VALUE_MESSAGE)
+        || messageName.equals(CelTypes.STRUCT_MESSAGE);
+  }
+
+  // Concretize JSON WKT unwrapping directly into native Z3 primitives to avoid
+  // sort incompatibilities (Message == String) and solver performance penalties (quantifiers).
+  private TranslatedValue translateJsonWktStruct(
+      CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
+    Expr<?> fallback;
+    if (createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)) {
+      fallback = typeSystem.mkNull();
+    } else if (createStruct.messageName().equals(CelTypes.LIST_VALUE_MESSAGE)) {
+      fallback = getDefaultValueForType(ListType.create(SimpleType.DYN));
+    } else {
+      fallback = getDefaultValueForType(MapType.create(SimpleType.STRING, SimpleType.DYN));
+    }
+
+    if (createStruct.entries().isEmpty()) {
+      return TranslatedValue.create(fallback, celExpr, typeSystem, ctx.mkFalse());
+    }
+
+    CelExpr.CelStruct.Entry entry = createStruct.entries().get(0);
+
+    // Translate the value to properly capture approximations and Optionals
+    TranslatedValue entryTv = translateExpr(entry.value(), ast);
+    Expr<?> finalVal = entryTv.z3Expr();
+
+    boolean isNullValueField =
+        createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)
+            && entry.fieldKey().equals(NULL_VALUE_FIELD);
+
+    if (entry.optionalEntry()) {
+      Expr<?> optRef = typeSystem.getOptionalRef(finalVal);
+      BoolExpr hasValue = typeSystem.optHasValue(optRef);
+
+      Expr<?> unpackedVal = typeSystem.getOptionalValue(optRef);
+      if (isNullValueField) {
+        unpackedVal = typeSystem.mkNull();
+      }
+      finalVal = ctx.mkITE(hasValue, unpackedVal, fallback);
+    } else if (isNullValueField) {
+      finalVal = typeSystem.mkNull();
+    }
+
+    return TranslatedValue.propagateStrict(
+        ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
+  }
+
   private Expr<?> getDefaultValueForType(CelType type) {
     if (type instanceof NullableType) {
       return typeSystem.mkNull();

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

@@ -805,38 +805,83 @@ private Expr<?> buildMapIndex(
 
   private TranslatedValue translateIndex(
       List<TranslatedValue> args, CelAbstractSyntaxTree ast, boolean isOptional) {
-    Expr<?> lhsTrans = args.get(0).z3Expr();
-    Expr<?> rhsTrans = args.get(1).z3Expr();
-
     TranslatedValue lhs = args.get(0);
     TranslatedValue rhs = args.get(1);
     CelType lhsType = extractAstTypeOrDefault(lhs, ast);
     CelType rhsType = extractAstTypeOrDefault(rhs, ast);
 
-    Expr<?> actualValue;
+    Expr<?> lhsTrans = lhs.z3Expr();
+    Expr<?> rhsTrans = rhs.z3Expr();
+
+    BoolExpr isLhsOpt = ctx.mkFalse();
+    BoolExpr lhsHasValue = ctx.mkFalse();
+    BoolExpr shouldEvaluate = ctx.mkTrue();
+
+    if (isOptional) {
+      isLhsOpt = typeSystem.isOptional(lhsTrans);
+      Expr<?> optRef = typeSystem.getOptionalRef(lhsTrans);
+      lhsHasValue = typeSystem.optHasValue(optRef);
+
+      lhsTrans = ctx.mkITE(isLhsOpt, typeSystem.getOptionalValue(optRef), lhsTrans);
+      shouldEvaluate = (BoolExpr) ctx.mkITE(isLhsOpt, lhsHasValue, ctx.mkTrue());
+
+      if (lhsType instanceof OptionalType) {
+        lhsType = ((OptionalType) lhsType).parameters().get(0);
+      }
+    }
+
+    Expr<?> actualValue =
+        buildAndConstrainIndex(lhsTrans, rhsTrans, lhsType, rhsType, shouldEvaluate, isOptional);
+
+    if (isOptional) {
+      actualValue =
+          ctx.mkITE(
+              ctx.mkAnd(isLhsOpt, ctx.mkNot(lhsHasValue)),
+              typeSystem.mkOptionalNone(),
+              actualValue);
+    }
+
+    return TranslatedValue.propagateStrict(ctx, typeSystem, actualValue, args);
+  }
+
+  private Expr<?> buildAndConstrainIndex(
+      Expr<?> lhsTrans,
+      Expr<?> rhsTrans,
+      CelType lhsType,
+      CelType rhsType,
+      BoolExpr shouldEvaluate,
+      boolean isOptional) {
+    CelType expectedElemType = null;
     if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) {
-      actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
-      constraintSink.accept(
-          ctx.mkImplies(
-              ctx.mkNot(typeSystem.isError(actualValue)),
-              typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType())));
+      expectedElemType = ((ListType) lhsType).elemType();
     } else if (lhsType.kind() == CelKind.MAP) {
-      actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
+      expectedElemType = ((MapType) lhsType).valueType();
+    }
+
+    if (expectedElemType != null) {
+      Expr<?> actualValue =
+          lhsType.kind() == CelKind.LIST
+              ? buildListIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional)
+              : buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional);
+
+      CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType;
+
       constraintSink.accept(
           ctx.mkImplies(
-              ctx.mkNot(typeSystem.isError(actualValue)),
-              typeConstraintGenerator.apply(actualValue, ((MapType) lhsType).valueType())));
-    } else {
-      BoolExpr isListGuard = ctx.mkAnd(typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans));
-      BoolExpr isMapGuard = typeSystem.isMap(lhsTrans);
-      actualValue =
-          CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
-              .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
-              .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
-              .build(typeSystem.mkError());
+              ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))),
+              typeConstraintGenerator.apply(actualValue, finalType)));
+
+      return actualValue;
     }
 
-    return TranslatedValue.propagateStrict(ctx, typeSystem, actualValue, args);
+    BoolExpr isListGuard =
+        ctx.mkAnd(shouldEvaluate, typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans));
+    BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans));
+
+    return CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
+        .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
+        .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
+        .build(typeSystem.mkError());
   }
 
   private TranslatedValue translateConditional(

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

@@ -115,6 +115,9 @@ public final class CelVerifierZ3ImplTest {
           .addVar(
               "test_all_types",
               StructTypeReference.create("cel.expr.conformance.proto3.TestAllTypes"))
+          .addVar("json_val", StructTypeReference.create("google.protobuf.Value"))
+          .addVar("json_list", StructTypeReference.create("google.protobuf.ListValue"))
+          .addVar("json_struct", StructTypeReference.create("google.protobuf.Struct"))
           .build();
 
   private static final CelVerifier VERIFIER =
@@ -226,9 +229,6 @@ private enum IsSatisfiableInconclusiveTestCase {
     MASKED_BY_BMC_MAP(
         "string_int_map == {'a':1, 'b':2, 'c':3, 'd':4, 'e':5, 'f':6} ? string_int_map.exists(k,"
             + " k == 'g') : false"),
-    MASKED_BY_BMC_NESTED(
-        "nested_list == [[1, 2, 3, 4, 5, 6]] ? nested_list.exists(row, row.exists(x, x == 42)) :"
-            + " false"),
     APPROXIMATED_STRING_TO_INT("int('123') == 123"),
     APPROXIMATED_DOUBLE_TO_INT("int(1.5) == 1"),
     APPROXIMATED_INT_TO_STRING("string(123) == '123'"),
@@ -252,6 +252,26 @@ public void isSatisfiable_inconclusive(@TestParameter IsSatisfiableInconclusiveT
     assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
   }
 
+  @Test
+  public void isSatisfiable_maskedByBmcNested_inconclusive() throws Exception {
+    String expr =
+        "nested_list == [[1, 2, 3, 4, 5, 6]] ? nested_list.exists(row, row.exists(x, x == 42)) :"
+            + " false";
+    CelAbstractSyntaxTree ast = CEL.compile(expr).getAst();
+
+    // Reduce the comprehension unroll limit specifically for this heavy nested query
+    // to prevent Z3 from timing out during the macro expansion.
+    CelVerifier customVerifier =
+        CelVerifierFactory.newVerifier()
+            .setComprehensionUnrollLimit(3)
+            .setTypeProvider(VERIFIER.getTypeProvider())
+            .build();
+
+    CelVerificationResult result = customVerifier.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+  }
+
   @Test
   public void isSatisfiable_comprehensionZeroUnrollLimit_inconclusive() throws Exception {
     String expr = "int_list == [1] ? int_list.exists(x, x == 1) : false";
@@ -1590,7 +1610,34 @@ private enum EquivalenceTestCase {
         "true"),
     OPTIONAL_FIELD_SELECTION_MAP_COMPREHENSION(
         "{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v).?b", "optional.of(2)"),
-    OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)");
+    OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)"),
+    JSON_VALUE_BOOL("google.protobuf.Value{bool_value: true}", "true"),
+    JSON_VALUE_NUMBER("google.protobuf.Value{number_value: 1.0}", "1.0"),
+    JSON_VALUE_NULL("google.protobuf.Value{null_value: 0}", "null"),
+    JSON_VALUE_EMPTY("google.protobuf.Value{}", "null"),
+    JSON_LIST_VALUE_EMPTY("google.protobuf.ListValue{}", "[]"),
+    JSON_STRUCT_EMPTY("google.protobuf.Struct{}", "{}"),
+    JSON_LIST_VALUE("google.protobuf.ListValue{values: [1, 2]}", "[1, 2]"),
+    JSON_STRUCT("google.protobuf.Struct{fields: {'a': 1}}", "{'a': 1}"),
+    JSON_DEEP_NESTING(
+        "google.protobuf.ListValue{values: [google.protobuf.Struct{fields: {'a':"
+            + " google.protobuf.Value{number_value: 1.0}}}]}",
+        "[{'a': 1.0}]"),
+    JSON_NUMBER_HETEROGENEOUS_EQUALITY("google.protobuf.Value{number_value: 1.0} == 1", "true"),
+    JSON_VALUE_OPTIONAL_NONE("google.protobuf.Value{?string_value: optional.none()}", "null"),
+    JSON_LIST_VALUE_OPTIONAL_NONE("google.protobuf.ListValue{?values: optional.none()}", "[]"),
+    JSON_STRUCT_OPTIONAL_NONE("google.protobuf.Struct{?fields: optional.none()}", "{}"),
+    JSON_VALUE_TYPE_REFLECTION("type(google.protobuf.Value{string_value: 'hi'}) == string", "true"),
+    JSON_STRUCT_TYPE_REFLECTION("type(google.protobuf.Struct{fields: {'a': 1}}) == map", "true"),
+    JSON_VAR_VALUE_EQUALITY("json_val == 'hi' || json_val != 'hi'", "true"),
+    JSON_VAR_LIST_EQUALITY("json_list == [1, 2] || json_list != [1, 2]", "true"),
+    JSON_VAR_MAP_EQUALITY("json_struct == {'a': 1} || json_struct != {'a': 1}", "true"),
+    JSON_VALUE_OPTIONAL_NULL_VALUE_NONE(
+        "google.protobuf.Value{?null_value: optional.none()}", "null"),
+    JSON_VALUE_OPTIONAL_NULL_VALUE_OF("google.protobuf.Value{?null_value: optional.of(0)}", "null"),
+    OPTIONAL_INDEX_LIST_UNWRAPPING("optional.of([1, 2, 3])[?0]", "optional.of(1)"),
+    OPTIONAL_INDEX_MAP_UNWRAPPING("optional.of({'a': 1})[?'a']", "optional.of(1)"),
+    OPTIONAL_INDEX_UNWRAPPING_NONE("optional.none()[?0]", "optional.none()");
 
     private final String exprA;
     private final String exprB;
@@ -1644,7 +1691,10 @@ private enum EquivalenceViolationTestCase {
         "TestAllTypes{single_int32: 0}.?single_int32", "optional.of(0)"),
     OPTIONAL_PROTO3_WRAPPER_ZERO_VS_UNSET(
         "TestAllTypes{single_int64_wrapper: 0}.?single_int64_wrapper",
-        "TestAllTypes{}.?single_int64_wrapper");
+        "TestAllTypes{}.?single_int64_wrapper"),
+    OPTIONAL_DYNAMIC_TARGET_TYPE_MISMATCH("dyn_var.?a == optional.none()", "false"),
+    OPTIONAL_NESTED_NONE_VS_MISSING(
+        "{'a': optional.none()}.?a.orValue(optional.of(1))", "optional.of(1)");
 
     final String exprA;
     final String exprB;