From 6b019ecb8aea6b1d5c1912ad878c14623776671b Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Tue, 28 Jul 2026 15:17:37 -0700 Subject: [PATCH] Implement JSON value unwrapping capability in verifier PiperOrigin-RevId: 955499463 --- .../main/java/dev/cel/verifier/BUILD.bazel | 1 + .../cel/verifier/CelAstToZ3Translator.java | 60 +++++++++++++ .../cel/verifier/CelZ3OperatorTranslator.java | 87 +++++++++++++----- .../cel/verifier/CelVerifierZ3ImplTest.java | 88 ++++++++++++++++--- 4 files changed, 202 insertions(+), 34 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 792ac5d2d..b9ac88687 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/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", diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index bc9ad676a..8c0239efd 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.Iterables; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; @@ -37,6 +38,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 +81,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 +373,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 +455,59 @@ 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()); + } + + // JSON WKT messages (gp.Struct, gp.Value, gp.ListValue) can only have a single top-level + // field entry in non-empty creation literals (e.g., 'fields' for Struct, 'values' for + // ListValue, or a single 'oneof' field for Value). + CelExpr.CelStruct.Entry entry = Iterables.getOnlyElement(createStruct.entries()); + + // 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(); diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 955c3d530..effa91c2b 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -805,38 +805,83 @@ private Expr buildMapIndex( private TranslatedValue translateIndex( List 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 = 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( diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 8a975f37a..2b41408d7 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -115,18 +115,21 @@ 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 = - CelVerifierFactory.newVerifier() - .setTypeProvider( - ProtoMessageTypeProvider.newBuilder() - .addDescriptors( - ImmutableList.of( - TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor())) - .build()) + private static final ProtoMessageTypeProvider TYPE_PROVIDER = + ProtoMessageTypeProvider.newBuilder() + .addDescriptors( + ImmutableList.of( + TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor())) .build(); + private static final CelVerifier VERIFIER = + CelVerifierFactory.newVerifier().setTypeProvider(TYPE_PROVIDER).build(); + @Before public void setUp() { System.setProperty("z3.skipLibraryLoad", "true"); @@ -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,24 @@ 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(); + + CelVerifier customVerifier = + CelVerifierFactory.newVerifier() + .setComprehensionUnrollLimit(3) + .setTypeProvider(TYPE_PROVIDER) + .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"; @@ -1581,6 +1599,9 @@ private enum EquivalenceTestCase { "TestAllTypes{}.?single_int64_wrapper", "optional.none()"), OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_EXPLICIT_NULL( "TestAllTypes{single_int64_wrapper: null}.?single_int64_wrapper", "optional.none()"), + OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_OPTIONAL_NONE( + "TestAllTypes{?single_int64_wrapper: optional.none()}.?single_int64_wrapper", + "optional.none()"), OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_PRESENT( "TestAllTypes{single_int64_wrapper: 42}.?single_int64_wrapper", "optional.of(42)"), OPTIONAL_FIELD_SELECTION_DYNAMIC_MISS( @@ -1590,7 +1611,43 @@ 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_STRUCT_MULTIPLE_FIELDS( + "google.protobuf.Struct{fields: {'a': 1, 'b': 'hello'}}", "{'a': 1, 'b': 'hello'}"), + JSON_STRUCT_EXPLICIT_VALUES( + "google.protobuf.Struct{fields: {'a': google.protobuf.Value{number_value: 1.0}, 'b':" + + " google.protobuf.Value{string_value: 'hello'}}}", + "{'a': 1.0, 'b': 'hello'}"), + JSON_STRUCT_OPTIONAL_ENTRIES( + "google.protobuf.Struct{fields: {'a': 1, ?'b': optional.of(2), ?'c': optional.none()}}", + "{'a': 1, 'b': 2}"), + 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 +1701,12 @@ 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_PROTO3_WRAPPER_ZERO_VS_NONE( + "TestAllTypes{single_int64_wrapper: 0}.?single_int64_wrapper", "optional.none()"), + 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;