Skip to content

Commit a82cdd1

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Implement JSON value unwrapping capability in verifier
PiperOrigin-RevId: 954872975
1 parent f502672 commit a82cdd1

4 files changed

Lines changed: 185 additions & 34 deletions

File tree

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -129,6 +129,7 @@ java_library(
129129
"//common/ast",
130130
"//common/ast:cel_block",
131131
"//common/types",
132+
"//common/types:cel_types",
132133
"//common/types:type_providers",
133134
"//verifier/axioms",
134135
"@maven//:com_google_errorprone_error_prone_annotations",

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

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
import com.google.common.collect.ImmutableList;
1818
import com.google.common.collect.ImmutableSet;
19+
import com.google.common.collect.Iterables;
1920
import com.microsoft.z3.ArithExpr;
2021
import com.microsoft.z3.ArrayExpr;
2122
import com.microsoft.z3.BoolExpr;
@@ -37,6 +38,7 @@
3738
import dev.cel.common.types.CelKind;
3839
import dev.cel.common.types.CelType;
3940
import dev.cel.common.types.CelTypeProvider;
41+
import dev.cel.common.types.CelTypes;
4042
import dev.cel.common.types.ListType;
4143
import dev.cel.common.types.MapType;
4244
import dev.cel.common.types.NullableType;
@@ -79,6 +81,7 @@ final class CelAstToZ3Translator {
7981
private static final String EMPTY_MSG_REF_PREFIX = "!empty_msg_ref_";
8082
private static final String EMPTY_LIST_PREFIX = "!empty_list";
8183
private static final String EMPTY_MAP_PREFIX = "!empty_map";
84+
private static final String NULL_VALUE_FIELD = "null_value";
8285
private final Context ctx;
8386
private final CelZ3TypeSystem typeSystem;
8487
private final CelZ3OperatorTranslator operatorTranslator;
@@ -370,6 +373,10 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
370373

371374
private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
372375
CelExpr.CelStruct createStruct = celExpr.struct();
376+
if (isJsonWkt(createStruct.messageName())) {
377+
return translateJsonWktStruct(celExpr, createStruct, ast);
378+
}
379+
373380
// Bypass SMT when the struct is empty (return the cached SMT default pointer)
374381
if (createStruct.entries().isEmpty()) {
375382
return TranslatedValue.create(
@@ -448,6 +455,56 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
448455
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
449456
}
450457

458+
private static boolean isJsonWkt(String messageName) {
459+
return messageName.equals(CelTypes.VALUE_MESSAGE)
460+
|| messageName.equals(CelTypes.LIST_VALUE_MESSAGE)
461+
|| messageName.equals(CelTypes.STRUCT_MESSAGE);
462+
}
463+
464+
// Concretize JSON WKT unwrapping directly into native Z3 primitives to avoid
465+
// sort incompatibilities (Message == String) and solver performance penalties (quantifiers).
466+
private TranslatedValue translateJsonWktStruct(
467+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
468+
Expr<?> fallback;
469+
if (createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)) {
470+
fallback = typeSystem.mkNull();
471+
} else if (createStruct.messageName().equals(CelTypes.LIST_VALUE_MESSAGE)) {
472+
fallback = getDefaultValueForType(ListType.create(SimpleType.DYN));
473+
} else {
474+
fallback = getDefaultValueForType(MapType.create(SimpleType.STRING, SimpleType.DYN));
475+
}
476+
477+
if (createStruct.entries().isEmpty()) {
478+
return TranslatedValue.create(fallback, celExpr, typeSystem, ctx.mkFalse());
479+
}
480+
481+
CelExpr.CelStruct.Entry entry = Iterables.getOnlyElement(createStruct.entries());
482+
483+
// Translate the value to properly capture approximations and Optionals
484+
TranslatedValue entryTv = translateExpr(entry.value(), ast);
485+
Expr<?> finalVal = entryTv.z3Expr();
486+
487+
boolean isNullValueField =
488+
createStruct.messageName().equals(CelTypes.VALUE_MESSAGE)
489+
&& entry.fieldKey().equals(NULL_VALUE_FIELD);
490+
491+
if (entry.optionalEntry()) {
492+
Expr<?> optRef = typeSystem.getOptionalRef(finalVal);
493+
BoolExpr hasValue = typeSystem.optHasValue(optRef);
494+
495+
Expr<?> unpackedVal = typeSystem.getOptionalValue(optRef);
496+
if (isNullValueField) {
497+
unpackedVal = typeSystem.mkNull();
498+
}
499+
finalVal = ctx.mkITE(hasValue, unpackedVal, fallback);
500+
} else if (isNullValueField) {
501+
finalVal = typeSystem.mkNull();
502+
}
503+
504+
return TranslatedValue.propagateStrict(
505+
ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
506+
}
507+
451508
private Expr<?> getDefaultValueForType(CelType type) {
452509
if (type instanceof NullableType) {
453510
return typeSystem.mkNull();

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

Lines changed: 66 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -805,38 +805,83 @@ private Expr<?> buildMapIndex(
805805

806806
private TranslatedValue translateIndex(
807807
List<TranslatedValue> args, CelAbstractSyntaxTree ast, boolean isOptional) {
808-
Expr<?> lhsTrans = args.get(0).z3Expr();
809-
Expr<?> rhsTrans = args.get(1).z3Expr();
810-
811808
TranslatedValue lhs = args.get(0);
812809
TranslatedValue rhs = args.get(1);
813810
CelType lhsType = extractAstTypeOrDefault(lhs, ast);
814811
CelType rhsType = extractAstTypeOrDefault(rhs, ast);
815812

816-
Expr<?> actualValue;
813+
Expr<?> lhsTrans = lhs.z3Expr();
814+
Expr<?> rhsTrans = rhs.z3Expr();
815+
816+
BoolExpr isLhsOpt = ctx.mkFalse();
817+
BoolExpr lhsHasValue = ctx.mkFalse();
818+
BoolExpr shouldEvaluate = ctx.mkTrue();
819+
820+
if (isOptional) {
821+
isLhsOpt = typeSystem.isOptional(lhsTrans);
822+
Expr<?> optRef = typeSystem.getOptionalRef(lhsTrans);
823+
lhsHasValue = typeSystem.optHasValue(optRef);
824+
825+
lhsTrans = ctx.mkITE(isLhsOpt, typeSystem.getOptionalValue(optRef), lhsTrans);
826+
shouldEvaluate = (BoolExpr) ctx.mkITE(isLhsOpt, lhsHasValue, ctx.mkTrue());
827+
828+
if (lhsType instanceof OptionalType) {
829+
lhsType = lhsType.parameters().get(0);
830+
}
831+
}
832+
833+
Expr<?> actualValue =
834+
buildAndConstrainIndex(lhsTrans, rhsTrans, lhsType, rhsType, shouldEvaluate, isOptional);
835+
836+
if (isOptional) {
837+
actualValue =
838+
ctx.mkITE(
839+
ctx.mkAnd(isLhsOpt, ctx.mkNot(lhsHasValue)),
840+
typeSystem.mkOptionalNone(),
841+
actualValue);
842+
}
843+
844+
return TranslatedValue.propagateStrict(ctx, typeSystem, actualValue, args);
845+
}
846+
847+
private Expr<?> buildAndConstrainIndex(
848+
Expr<?> lhsTrans,
849+
Expr<?> rhsTrans,
850+
CelType lhsType,
851+
CelType rhsType,
852+
BoolExpr shouldEvaluate,
853+
boolean isOptional) {
854+
CelType expectedElemType = null;
817855
if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) {
818-
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
819-
constraintSink.accept(
820-
ctx.mkImplies(
821-
ctx.mkNot(typeSystem.isError(actualValue)),
822-
typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType())));
856+
expectedElemType = ((ListType) lhsType).elemType();
823857
} else if (lhsType.kind() == CelKind.MAP) {
824-
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
858+
expectedElemType = ((MapType) lhsType).valueType();
859+
}
860+
861+
if (expectedElemType != null) {
862+
Expr<?> actualValue =
863+
lhsType.kind() == CelKind.LIST
864+
? buildListIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional)
865+
: buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional);
866+
867+
CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType;
868+
825869
constraintSink.accept(
826870
ctx.mkImplies(
827-
ctx.mkNot(typeSystem.isError(actualValue)),
828-
typeConstraintGenerator.apply(actualValue, ((MapType) lhsType).valueType())));
829-
} else {
830-
BoolExpr isListGuard = ctx.mkAnd(typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans));
831-
BoolExpr isMapGuard = typeSystem.isMap(lhsTrans);
832-
actualValue =
833-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
834-
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
835-
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
836-
.build(typeSystem.mkError());
871+
ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))),
872+
typeConstraintGenerator.apply(actualValue, finalType)));
873+
874+
return actualValue;
837875
}
838876

839-
return TranslatedValue.propagateStrict(ctx, typeSystem, actualValue, args);
877+
BoolExpr isListGuard =
878+
ctx.mkAnd(shouldEvaluate, typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans));
879+
BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans));
880+
881+
return CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
882+
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
883+
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
884+
.build(typeSystem.mkError());
840885
}
841886

842887
private TranslatedValue translateConditional(

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

Lines changed: 61 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -115,18 +115,21 @@ public final class CelVerifierZ3ImplTest {
115115
.addVar(
116116
"test_all_types",
117117
StructTypeReference.create("cel.expr.conformance.proto3.TestAllTypes"))
118+
.addVar("json_val", StructTypeReference.create("google.protobuf.Value"))
119+
.addVar("json_list", StructTypeReference.create("google.protobuf.ListValue"))
120+
.addVar("json_struct", StructTypeReference.create("google.protobuf.Struct"))
118121
.build();
119122

120-
private static final CelVerifier VERIFIER =
121-
CelVerifierFactory.newVerifier()
122-
.setTypeProvider(
123-
ProtoMessageTypeProvider.newBuilder()
124-
.addDescriptors(
125-
ImmutableList.of(
126-
TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor()))
127-
.build())
123+
private static final ProtoMessageTypeProvider TYPE_PROVIDER =
124+
ProtoMessageTypeProvider.newBuilder()
125+
.addDescriptors(
126+
ImmutableList.of(
127+
TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor()))
128128
.build();
129129

130+
private static final CelVerifier VERIFIER =
131+
CelVerifierFactory.newVerifier().setTypeProvider(TYPE_PROVIDER).build();
132+
130133
@Before
131134
public void setUp() {
132135
System.setProperty("z3.skipLibraryLoad", "true");
@@ -226,9 +229,6 @@ private enum IsSatisfiableInconclusiveTestCase {
226229
MASKED_BY_BMC_MAP(
227230
"string_int_map == {'a':1, 'b':2, 'c':3, 'd':4, 'e':5, 'f':6} ? string_int_map.exists(k,"
228231
+ " k == 'g') : false"),
229-
MASKED_BY_BMC_NESTED(
230-
"nested_list == [[1, 2, 3, 4, 5, 6]] ? nested_list.exists(row, row.exists(x, x == 42)) :"
231-
+ " false"),
232232
APPROXIMATED_STRING_TO_INT("int('123') == 123"),
233233
APPROXIMATED_DOUBLE_TO_INT("int(1.5) == 1"),
234234
APPROXIMATED_INT_TO_STRING("string(123) == '123'"),
@@ -252,6 +252,24 @@ public void isSatisfiable_inconclusive(@TestParameter IsSatisfiableInconclusiveT
252252
assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
253253
}
254254

255+
@Test
256+
public void isSatisfiable_maskedByBmcNested_inconclusive() throws Exception {
257+
String expr =
258+
"nested_list == [[1, 2, 3, 4, 5, 6]] ? nested_list.exists(row, row.exists(x, x == 42)) :"
259+
+ " false";
260+
CelAbstractSyntaxTree ast = CEL.compile(expr).getAst();
261+
262+
CelVerifier customVerifier =
263+
CelVerifierFactory.newVerifier()
264+
.setComprehensionUnrollLimit(3)
265+
.setTypeProvider(TYPE_PROVIDER)
266+
.build();
267+
268+
CelVerificationResult result = customVerifier.isSatisfiable(ast);
269+
270+
assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
271+
}
272+
255273
@Test
256274
public void isSatisfiable_comprehensionZeroUnrollLimit_inconclusive() throws Exception {
257275
String expr = "int_list == [1] ? int_list.exists(x, x == 1) : false";
@@ -1590,7 +1608,34 @@ private enum EquivalenceTestCase {
15901608
"true"),
15911609
OPTIONAL_FIELD_SELECTION_MAP_COMPREHENSION(
15921610
"{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v).?b", "optional.of(2)"),
1593-
OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)");
1611+
OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)"),
1612+
JSON_VALUE_BOOL("google.protobuf.Value{bool_value: true}", "true"),
1613+
JSON_VALUE_NUMBER("google.protobuf.Value{number_value: 1.0}", "1.0"),
1614+
JSON_VALUE_NULL("google.protobuf.Value{null_value: 0}", "null"),
1615+
JSON_VALUE_EMPTY("google.protobuf.Value{}", "null"),
1616+
JSON_LIST_VALUE_EMPTY("google.protobuf.ListValue{}", "[]"),
1617+
JSON_STRUCT_EMPTY("google.protobuf.Struct{}", "{}"),
1618+
JSON_LIST_VALUE("google.protobuf.ListValue{values: [1, 2]}", "[1, 2]"),
1619+
JSON_STRUCT("google.protobuf.Struct{fields: {'a': 1}}", "{'a': 1}"),
1620+
JSON_DEEP_NESTING(
1621+
"google.protobuf.ListValue{values: [google.protobuf.Struct{fields: {'a':"
1622+
+ " google.protobuf.Value{number_value: 1.0}}}]}",
1623+
"[{'a': 1.0}]"),
1624+
JSON_NUMBER_HETEROGENEOUS_EQUALITY("google.protobuf.Value{number_value: 1.0} == 1", "true"),
1625+
JSON_VALUE_OPTIONAL_NONE("google.protobuf.Value{?string_value: optional.none()}", "null"),
1626+
JSON_LIST_VALUE_OPTIONAL_NONE("google.protobuf.ListValue{?values: optional.none()}", "[]"),
1627+
JSON_STRUCT_OPTIONAL_NONE("google.protobuf.Struct{?fields: optional.none()}", "{}"),
1628+
JSON_VALUE_TYPE_REFLECTION("type(google.protobuf.Value{string_value: 'hi'}) == string", "true"),
1629+
JSON_STRUCT_TYPE_REFLECTION("type(google.protobuf.Struct{fields: {'a': 1}}) == map", "true"),
1630+
JSON_VAR_VALUE_EQUALITY("json_val == 'hi' || json_val != 'hi'", "true"),
1631+
JSON_VAR_LIST_EQUALITY("json_list == [1, 2] || json_list != [1, 2]", "true"),
1632+
JSON_VAR_MAP_EQUALITY("json_struct == {'a': 1} || json_struct != {'a': 1}", "true"),
1633+
JSON_VALUE_OPTIONAL_NULL_VALUE_NONE(
1634+
"google.protobuf.Value{?null_value: optional.none()}", "null"),
1635+
JSON_VALUE_OPTIONAL_NULL_VALUE_OF("google.protobuf.Value{?null_value: optional.of(0)}", "null"),
1636+
OPTIONAL_INDEX_LIST_UNWRAPPING("optional.of([1, 2, 3])[?0]", "optional.of(1)"),
1637+
OPTIONAL_INDEX_MAP_UNWRAPPING("optional.of({'a': 1})[?'a']", "optional.of(1)"),
1638+
OPTIONAL_INDEX_UNWRAPPING_NONE("optional.none()[?0]", "optional.none()");
15941639

15951640
private final String exprA;
15961641
private final String exprB;
@@ -1644,7 +1689,10 @@ private enum EquivalenceViolationTestCase {
16441689
"TestAllTypes{single_int32: 0}.?single_int32", "optional.of(0)"),
16451690
OPTIONAL_PROTO3_WRAPPER_ZERO_VS_UNSET(
16461691
"TestAllTypes{single_int64_wrapper: 0}.?single_int64_wrapper",
1647-
"TestAllTypes{}.?single_int64_wrapper");
1692+
"TestAllTypes{}.?single_int64_wrapper"),
1693+
OPTIONAL_DYNAMIC_TARGET_TYPE_MISMATCH("dyn_var.?a == optional.none()", "false"),
1694+
OPTIONAL_NESTED_NONE_VS_MISSING(
1695+
"{'a': optional.none()}.?a.orValue(optional.of(1))", "optional.of(1)");
16481696

16491697
final String exprA;
16501698
final String exprB;

0 commit comments

Comments
 (0)