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,64 @@ 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);
+  }
+
+  private BoolExpr createJsonWktTypeConstraint(String messageName, Expr<?> val) {
+    if (messageName.equals(CelTypes.VALUE_MESSAGE)) {
+      return ctx.mkTrue();
+    }
+    if (messageName.equals(CelTypes.LIST_VALUE_MESSAGE)) {
+      return typeSystem.isList(val);
+    }
+    return typeSystem.isMap(val);
+  }
+
+  // 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);
+    TranslatedValue entryTv;
+
+    // null_value is a proto enum represented as integer 0 in the AST.
+    // We must explicitly force it to CelNull to match runtime semantics.
+    if (createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)
+        && entry.fieldKey().equals(NULL_VALUE_FIELD)) {
+      entryTv =
+          TranslatedValue.create(typeSystem.mkNull(), entry.value(), typeSystem, ctx.mkFalse());
+    } else {
+      entryTv = translateExpr(entry.value(), ast);
+    }
+
+    Expr<?> finalVal = entryTv.z3Expr();
+
+    if (entry.optionalEntry()) {
+      Expr<?> optRef = typeSystem.getOptionalRef(finalVal);
+      BoolExpr hasValue = typeSystem.optHasValue(optRef);
+      finalVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), fallback);
+    }
+
+    return TranslatedValue.propagateStrict(
+        ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
+  }
+
   private Expr<?> getDefaultValueForType(CelType type) {
     if (type instanceof NullableType) {
       return typeSystem.mkNull();
@@ -1244,6 +1308,9 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
       return typeSystem.isMap(val);
     }
     if (type.kind() == CelKind.STRUCT) {
+      if (isJsonWkt(type.name())) {
+        return createJsonWktTypeConstraint(type.name(), val);
+      }
       return ctx.mkAnd(
           typeSystem.isMessage(val),
           ctx.mkEq(

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

@@ -1590,7 +1590,25 @@ 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");
 
     private final String exprA;
     private final String exprB;