From e2b8089943473cc951534e0f2aabc2008db9a6fc Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 11 Nov 2026 15:56:19 -0800 Subject: [PATCH] Reject map literal keys that the runtime rejects PiperOrigin-RevId: 1019572347 --- .../cel/verifier/CelAstToZ3Translator.java | 28 ++++++++++++++++++- .../dev/cel/verifier/CelZ3TypeSystem.java | 4 +-- .../cel/verifier/CelVerifierZ3ImplTest.java | 16 +++++++++-- 3 files changed, 42 insertions(+), 6 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 00b04b199..e3211e0f0 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -41,6 +41,7 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; +import java.util.LinkedHashMap; import java.util.LinkedHashSet; import java.util.List; import java.util.Map; @@ -342,11 +343,33 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) List elementsTv = new ArrayList<>(); List> values = new ArrayList<>(); + // Keys must be strings, ints, uints or bools, and can't equal an earlier key in the map. + List invalidKeys = new ArrayList<>(); + Map, BoolExpr> keysSoFar = new LinkedHashMap<>(); for (CelExpr.CelMap.Entry entryAst : createMap.entries()) { TranslatedValue keyTv = translateExpr(entryAst.key(), ast); Expr key = keyTv.z3Expr(); elementsTv.add(keyTv); + invalidKeys.add( + ctx.mkNot( + ctx.mkOr( + typeSystem.isString(key), + typeSystem.isInt(key), + typeSystem.isUint(key), + typeSystem.isBool(key)))); + for (CelZ3TypeSystem.EqualKey equalKey : typeSystem.equalKeys(key)) { + keysSoFar.forEach( + (earlierKey, isPresent) -> { + BoolExpr repeats = + ctx.mkAnd( + isPresent, equalKey.condition(), ctx.mkEq(earlierKey, equalKey.key())); + // Performance only: skips what distinct constant keys rule out. + if (!repeats.simplify().isFalse()) { + invalidKeys.add(repeats); + } + }); + } TranslatedValue valueTv = translateExpr(entryAst.value(), ast); Expr value = valueTv.z3Expr(); @@ -364,6 +387,7 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) } elementsTv.add(valueTv); values.add(finalValue); + keysSoFar.merge(key, finalPresence, ctx::mkOr); BoolExpr keyAlreadyPresent = (BoolExpr) ctx.mkSelect(mapPresence, key); BoolExpr shouldInsertKey = ctx.mkAnd(ctx.mkNot(keyAlreadyPresent), finalPresence); @@ -381,7 +405,9 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) context.addConstraint(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence)); context.addConstraint(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); - Expr result = typeSystem.wrapMap(mapRef); + Expr result = + typeSystem.withRuntimeError( + typeSystem.wrapMap(mapRef), CelZ3Exprs.mkOrFlattened(ctx, invalidKeys)); propagateTruncatedTypeConstraint(result, values); return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index b3ba7d4fe..1a9d262d0 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -951,8 +951,8 @@ public BoolExpr doubleLeInt(FPExpr d, IntExpr n) { return ctx.mkAnd(ctx.mkNot(ctx.mkFPIsNaN(d)), ctx.mkNot(intLtDouble(n, d))); } - // Returns the double that holds the constant n exactly, if any. Comparing with it needs no - // truncation (performance only), and it's the double key equal to n. + // Performance only: a constant that a double holds exactly compares as that double, without the + // uninterpreted truncation. private Optional asExactDouble(IntExpr n) { Expr simplified = n.simplify(); if (!(simplified instanceof IntNum)) { diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 9853fb8d1..8ab5fa1cf 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -349,7 +349,7 @@ private enum InexactWitnessTestCase { LIST_PAST_UNROLL_LIMIT("size(int_list) == 6", "int_list"), MAP_PAST_UNROLL_LIMIT("size(string_int_map) == 6", "string_int_map"), LIST_WITH_INEXACT_ELEMENT("dyn_list == [b'\\xc3\\xa9']", "dyn_list"), - MAP_WITH_INEXACT_KEY("dyn_int_map == {b'\\xc3\\xa9': 1}", "dyn_int_map"), + MAP_WITH_INEXACT_KEY("b'\\xc3\\xa9' in dyn_int_map", "dyn_int_map"), MAP_WITH_INEXACT_VALUE("string_dyn_map == {'a': b'\\xc3\\xa9'}", "string_dyn_map"), OPTIONAL_WITH_INEXACT_VALUE("opt_dyn_var == optional.of(b'\\xc3\\xa9')", "opt_dyn_var"); @@ -991,14 +991,12 @@ private enum IsAlwaysTrueTestCase { MAP_SIZE("size({'a': 1, 'b': 2}) == 2"), EMPTY_LIST_SIZE("size([]) == 0"), EMPTY_MAP_SIZE("size({}) == 0"), - MAP_LITERAL_DUPLICATE_KEYS("size({'a': 1, 'a': 2}) == 1"), LIST_CONCATENATION_SIZE("size(int_list + [1]) == size(int_list) + 1"), STRING_CONCATENATION_SIZE("size(role + 'a') == size(role) + 1"), BYTES_CONCATENATION_SIZE("size(by + b'a') == size(by) + 1"), LIST_SIZE_NON_NEGATIVE("size(int_list) >= 0"), STRING_SIZE_NON_NEGATIVE("size(role) >= 0"), MAP_SIZE_NON_NEGATIVE("size(string_int_map) >= 0"), - DYNAMIC_MAP_DUPLICATE_KEYS("!(x == y) || size({x: 1, y: 2}) == 1"), MEMBER_LIST_SIZE("[1, 2].size() == 2"), MEMBER_STRING_SIZE("'abc'.size() == 3"), MEMBER_BYTES_SIZE("b'abc'.size() == 3"), @@ -1123,6 +1121,8 @@ private enum IsAlwaysTrueTestCase { DYN_MESSAGE_UNSET_ENUM_FIELD("dyn(TestAllTypes{}).standalone_enum == 0"), DYN_MESSAGE_SET_FIELD_TYPE("type(dyn(test_all_types).single_string) == string"), STRUCT_DEFAULT_ENUM_EQ_UNSET("TestAllTypes{standalone_enum: 0} == TestAllTypes{}"), + // An absent optional entry's key may repeat. + MAP_LITERAL_ABSENT_OPTIONAL_KEY_REPEATED("{?1: optional.none(), 1: 'b'}[1] == 'b'"), // Map keys and values compare by CEL equality: numerically across int, uint and double. MAP_LITERAL_EQ_ACROSS_NUMERIC_KEYS("dyn({1: 'a'}) == {1u: 'a'}"), MAP_LITERAL_EQ_ACROSS_NUMERIC_VALUES("dyn({'a': 1}) == {'a': 1.0}"), @@ -1881,6 +1881,16 @@ public void verifyEquivalence_infinityConstants_notEquivalent() throws Exception } private enum IsAlwaysTrueViolationTestCase { + // Map literal keys must be strings, ints, uints or bools, and can't repeat. + MAP_LITERAL_DOUBLE_KEY("{1.0: 'a'}[dyn(1)] == 'a'", "Condition is not always true\\."), + MAP_LITERAL_BYTES_KEY("size({b'a': 1}) == 1", "Condition is not always true\\."), + MAP_LITERAL_REPEATED_KEY("size({1: 'a', 1: 'b'}) == 1", "Condition is not always true\\."), + MAP_LITERAL_NUMERICALLY_REPEATED_KEY( + "size({1: 'a', 1u: 'b'}) == 2", "Condition is not always true\\."), + MAP_LITERAL_PRESENT_OPTIONAL_KEY_REPEATED( + "size({?1: optional.of('a'), 1: 'b'}) == 1", "Condition is not always true\\."), + MAP_LITERAL_VARIABLE_KEY_REPEATED( + "x == 1 ? size({x: 'a', 1u: 'b'}) == 2 : true", "Condition is not always true\\."), // The exact error wins over whether the empty list(dyn) field is set. STRUCT_EMPTY_LIST_DYN_FIELD_WITH_ERROR( "TestAllTypes{repeated_value: [], single_int64: 1 / 0} == TestAllTypes{}",