Skip to content

Treat empty repeated and map fields as unset, and read unset fields of dyn messages as defaults #1454

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
copybara-service merged 1 commit into from
Nov 11, 2026
Merged

Treat empty repeated and map fields as unset, and read unset fields of dyn messages as defaults #1454

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
129 changes: 110 additions & 19 deletions verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
import com.microsoft.z3.Expr;
import com.microsoft.z3.FPExpr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.SeqExpr;
import dev.cel.common.CelAbstractSyntaxTree;
import dev.cel.common.ast.CelExpr;
import dev.cel.common.internal.ProtoTimeUtils;
Expand All @@ -39,8 +40,11 @@
import dev.cel.common.types.StructTypeReference;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import java.util.function.BiFunction;

/** Translates CEL message construction and field selection to Z3. */
Expand Down Expand Up @@ -91,13 +95,16 @@ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {

Expr<?> msgRef = typeSystem.mkMessageRefConst(MSG_REF_PREFIX);

// Initialize the values array with Unknown. Missing fields and explicit primitive defaults
// will both bypass the store and fall back to this Unknown base. However, their msgPresence
// will evaluate to false, allowing translateSelect to properly return the default value.
// Initialize the values array with Unknown. Missing fields, explicit primitive defaults and
// empty repeated or map fields all bypass the store and fall back to this Unknown base.
// However, their msgPresence will evaluate to false, allowing translateSelect to properly
// return the default value.
ArrayExpr msgValues = ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown());
ArrayExpr msgPresence = ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse());

List<TranslatedValue> elementsTv = new ArrayList<>();
List<BoolExpr> invalidFields = new ArrayList<>();
Set<String> fields = new HashSet<>();

for (CelExpr.CelStruct.Entry entryAst : createStruct.entries()) {
Expr<?> key = ctx.mkString(entryAst.fieldKey());
Expand All @@ -112,7 +119,6 @@ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
.flatMap(t -> t.findField(entryAst.fieldKey()))
.map(StructType.Field::type)
.orElseGet(() -> extractAstTypeOrDefault(ast, entryAst.value().id()));
Expr<?> defaultVal = getDefaultValueForType(fieldType);

Expr<?> finalValue = value;
BoolExpr optionalHasValue = ctx.mkTrue();
Expand All @@ -126,7 +132,6 @@ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
optionalHasValue = typeSystem.optHasValue(optRef);
finalValue = typeSystem.getOptionalValue(optRef);
}
elementsTv.add(valueTv);

// Canonicalization Trick:
//
Expand All @@ -136,25 +141,66 @@ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
// (`msg1 == msg2`) to work without using quantifiers (which avoids MBQI loops).
// Because proto3 singular primitives do not have field presence, we also skip setting
// `msgPresence`.
BoolExpr isDefaultPrimitive =
fieldType.kind().isPrimitive() ? ctx.mkEq(finalValue, defaultVal) : ctx.mkFalse();
BoolExpr isUnset = ctx.mkFalse();
if (fieldType.kind().isPrimitive()) {
isUnset = ctx.mkEq(finalValue, getDefaultValueForType(fieldType));
} else if (fieldType.kind() == CelKind.LIST || fieldType.kind() == CelKind.MAP) {
// Empty repeated and map fields are unset too. Other values can't initialize them.
boolean isList = fieldType.kind() == CelKind.LIST;
BoolExpr hasFieldKind =
isList ? typeSystem.isList(finalValue) : typeSystem.isMap(finalValue);
invalidFields.add(ctx.mkAnd(optionalHasValue, ctx.mkNot(hasFieldKind)));
SeqExpr<?> elements =
isList
? typeSystem.getSeq(typeSystem.getListRef(finalValue))
: typeSystem.getMapKeys(typeSystem.getMapRef(finalValue));
BoolExpr isEmpty = ctx.mkAnd(hasFieldKind, ctx.mkEq(ctx.mkLength(elements), ctx.mkInt(0)));
isUnset = isEmpty;
// A google.protobuf.ListValue or Struct field has the same type, but is set even if empty,
// so either may hold.
if (fieldType.equals(ListType.create(SimpleType.DYN))
|| fieldType.equals(MapType.create(SimpleType.STRING, SimpleType.DYN))) {
valueTv =
valueTv.withApproximation(
context.recordApproximation(
"whether empty `list(dyn)` and `map(string, dyn)` fields are set",
CelZ3Exprs.mkAndFlattened(ctx, optionalHasValue, isEmpty)));
isUnset =
ctx.mkAnd(
isEmpty,
ctx.mkBoolConst(
"!unset_" + createStruct.messageName() + "." + entryAst.fieldKey()));
}
}
elementsTv.add(valueTv);

BoolExpr shouldBypass = ctx.mkOr(ctx.mkNot(optionalHasValue), isDefaultPrimitive);
BoolExpr shouldBypass = ctx.mkOr(ctx.mkNot(optionalHasValue), isUnset);
// The last entry for a field wins, so a later unset entry clears an earlier one.
boolean isRepeatedEntry = !fields.add(entryAst.fieldKey());

msgValues =
(ArrayExpr) ctx.mkITE(shouldBypass, msgValues, ctx.mkStore(msgValues, key, finalValue));
(ArrayExpr)
ctx.mkITE(
shouldBypass,
isRepeatedEntry ? ctx.mkStore(msgValues, key, typeSystem.mkUnknown()) : msgValues,
ctx.mkStore(msgValues, key, finalValue));

msgPresence =
(ArrayExpr)
ctx.mkITE(shouldBypass, msgPresence, ctx.mkStore(msgPresence, key, ctx.mkTrue()));
ctx.mkITE(
shouldBypass,
isRepeatedEntry ? ctx.mkStore(msgPresence, key, ctx.mkFalse()) : msgPresence,
ctx.mkStore(msgPresence, key, ctx.mkTrue()));
}

context.addConstraint(
ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString(createStruct.messageName())));
context.addConstraint(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues));
context.addConstraint(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence));

Expr<?> result = typeSystem.wrapMessage(msgRef);
Expr<?> result =
typeSystem.withRuntimeError(
typeSystem.wrapMessage(msgRef), CelZ3Exprs.mkOrFlattened(ctx, invalidFields));
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
}

Expand Down Expand Up @@ -368,14 +414,16 @@ private Expr<?> resolveStructFieldValue(
.orElse(defaultValue);
}

// TODO: proto2 fields with a custom default read as their type's zero value.
private Expr<?> getDefaultValueForType(CelType type) {
if (type instanceof NullableType) {
return typeSystem.mkNull();
}
if (type instanceof OptionalType) {
return typeSystem.mkOptionalNone();
}
if (type.equals(SimpleType.INT)) {
// Enums too.
if (type.kind() == CelKind.INT) {
return typeSystem.mkInt(0);
}
if (type.equals(SimpleType.BOOL)) {
Expand Down Expand Up @@ -498,6 +546,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {

Expr<?> presenceResult;
Expr<?> valueResult;
BoolExpr unmodeledMessage = ctx.mkFalse();
BoolExpr presenceError = ctx.mkFalse();

if (operandType instanceof MapType) {
FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue());
Expand All @@ -522,20 +572,60 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
.addCase(isMap, mapAcc.presence)
.build(ctx.mkFalse());

// TODO: Unsound: an unset field reads as an unknown, which can make a
// satisfiable
// expression look unsatisfiable. Its default depends on the message's runtime type.
Expr<?> msgRead = ctx.mkITE(msgAcc.presence, msgAcc.value, typeSystem.mkUnknown());
// A field reads as its value if set, else its default, in the message's runtime type, and is
// an error if that type doesn't declare it. Well-known types are never messages.
Expr<?> typeName = typeSystem.getMsgTypeName(typeSystem.getMessageRef(operand));
CelZ3Exprs.SwitchBuilder msgRead = CelZ3Exprs.SwitchBuilder.newBuilder(ctx);
List<BoolExpr> isModeledType = new ArrayList<>();
List<BoolExpr> isUndeclared = new ArrayList<>();
for (CelType type : typeProvider.types()) {
if (!(type instanceof StructType) || CelTypes.isWellKnownType(type.name())) {
continue;
}
BoolExpr isType = ctx.mkEq(typeName, ctx.mkString(type.name()));
isModeledType.add(isType);
Optional<StructType.Field> declared = ((StructType) type).findField(field);
if (!declared.isPresent()) {
isUndeclared.add(isType);
msgRead.addCase(isType, typeSystem.mkError());
continue;
}
if (select.testOnly()) {
continue;
}
CelType fieldType = declared.get().type();
context.addConstraint(
ctx.mkImplies(
ctx.mkAnd(isMessage, isType, msgAcc.presence),
typeConstraintGenerator.createTypeConstraintForType(msgAcc.value, fieldType)));
msgRead.addCase(
isType, ctx.mkITE(msgAcc.presence, msgAcc.value, getDefaultValueForType(fieldType)));
}
// Messages of other types aren't modeled.
unmodeledMessage =
context.recordApproximation(
"messages of types the type provider doesn't declare",
ctx.mkAnd(isMessage, ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType))));
Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
// Testing an undeclared field, or a field of something other than a map or message, errors.
presenceError =
ctx.mkOr(
ctx.mkAnd(isMessage, CelZ3Exprs.mkOrFlattened(ctx, isUndeclared)),
ctx.mkNot(ctx.mkOr(isMap, isMessage)));

valueResult =
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(isMessage, msgRead)
.addCase(
isMessage,
msgRead.build(ctx.mkITE(msgAcc.presence, msgAcc.value, typeSystem.mkUnknown())))
.addCase(isMap, mapRead)
.build(typeSystem.mkError());
}

Expr<?> fieldAccess = select.testOnly() ? typeSystem.wrapBool(presenceResult) : valueResult;
Expr<?> fieldAccess =
select.testOnly()
? typeSystem.withRuntimeError(typeSystem.wrapBool(presenceResult), presenceError)
: valueResult;

context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast));

Expand All @@ -545,7 +635,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
// Map presence is only linked to the keys up to the unroll limit.
return operandType.kind() == CelKind.STRUCT
? result
: result.withApproximation(context.isTruncatedMap(operand));
: result.withApproximation(
CelZ3Exprs.mkOrFlattened(ctx, context.isTruncatedMap(operand), unmodeledMessage));
}

private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) {
Expand Down
58 changes: 56 additions & 2 deletions verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -169,6 +169,8 @@ private enum IsSatisfiableTestCase {
DYNAMIC_MAP_COMPREHENSION_EXISTS("string_int_map.exists(k, k == 'test')", "string_int_map = "),
NULL_SATISFIABLE("unknown_var == null", "unknown_var = null"),
DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0", "dyn_var = 1"),
DYNAMIC_VAR_UNSET_MESSAGE_FIELD(
"dyn_var == TestAllTypes{} && dyn_var.single_string == ''", "dyn_var = "),
ANY_NUMERIC_EQUALITY(
"test_all_types.single_any == 1 && 1.0 == test_all_types.single_any", "test_all_types = "),
DYNAMIC_VAR_NOT_IN_LIST(
Expand Down Expand Up @@ -547,6 +549,13 @@ public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exc

private enum ApproximationSourceTestCase {
PARTIALLY_MODELED_FUNCTION("int(string_var) == 5", "calls to `int`"),
EMPTY_LIST_DYN_FIELD(
"has(TestAllTypes{list_value: []}.list_value)",
"whether empty `list(dyn)` and `map(string, dyn)` fields are set"),
// An absent optional entry's value is never read.
ABSENT_OPTIONAL_LIST_DYN_FIELD(
"TestAllTypes{?list_value: optional.none()} == TestAllTypes{} && int(string_var) == 5",
"calls to `int`"),
// `type` is exact; only its argument is approximate.
APPROXIMATE_ARGUMENT("type(int(string_var)) == int", "calls to `int`"),
APPROXIMATE_ARGUMENT_OF_UNCONDITIONAL_SOURCE(
Expand Down Expand Up @@ -664,6 +673,8 @@ public void isSatisfiable_approximate_returnsPotentialSatisfyingInput() throws E
}

private enum IsSatisfiableInconclusiveTestCase {
// Well-known types are never messages, and other message types may have the field.
DYN_MESSAGE_FIELD_OF_UNKNOWN_TYPE("type(dyn_var) != map && dyn_var.type_url == ''"),
MASKED_BY_BMC("int_list == [1, 2, 3, 4, 5, 6] ? int_list.exists(x, x == 42) : false"),
MASKED_BY_BMC_ALL("int_list == [1, 2, 3, 4, 5, 6] ? int_list.all(x, x > 0) : false"),
MASKED_BY_BMC_FILTER(
Expand Down Expand Up @@ -781,6 +792,9 @@ public void isSatisfiable_comprehensionZeroUnrollLimit_inconclusive() throws Exc
}

private enum IsUnsatisfiableTestCase {
DYN_MESSAGE_PRESENT_UNDECLARED_FIELD("dyn(test_all_types).unknown_field == 42"),
REPEATED_FIELD_FROM_NON_LIST(
"dyn_var == 42 && TestAllTypes{repeated_int64: dyn_var} == TestAllTypes{}"),
UNSATISFIABLE("x > 5 && x < 3"),
DYN_RANGE_COMPREHENSION_MASKED_BY_FALSE("dyn_var.exists(e, e == 1) && false"),
CONTRADICTORY_TYPES_FOR_DYNAMIC_VARIABLE("unknown_var + 1 == 2 && unknown_var[0] == 1"),
Expand Down Expand Up @@ -1083,6 +1097,29 @@ private enum IsAlwaysTrueTestCase {
DIVIDE_TRUNCATED("-5 / 3 == -1"),
MODULO_TRUNCATED("-5 % 3 == -2"),
EXPLICIT_DEFAULT_READ("TestAllTypes{single_int32: 0}.single_int32 == 0"),
// Repeated and map fields are unset exactly when empty.
STRUCT_REPEATED_EQ_UNSET_IFF_EMPTY(
"(TestAllTypes{repeated_int64: int_list} == TestAllTypes{}) == (int_list == [])"),
STRUCT_MAP_EQ_UNSET_IFF_EMPTY(
"(TestAllTypes{map_string_int64: string_int_map} == TestAllTypes{})"
+ " == (size(string_int_map) == 0)"),
STRUCT_EMPTY_REPEATED_NOT_PRESENT("!has(TestAllTypes{repeated_int64: []}.repeated_int64)"),
// The last entry for a field wins.
STRUCT_REPEATED_FIELD_ENTRY_RESET_TO_EMPTY(
"TestAllTypes{repeated_int64: [1], repeated_int64: []} == TestAllTypes{}"),
STRUCT_REPEATED_FIELD_ENTRY_RESET_TO_DEFAULT(
"TestAllTypes{single_int64: 1, single_int64: 0} == TestAllTypes{}"),
// Unset fields read through dyn are their default in the message's runtime type.
DYN_MESSAGE_EMPTY_REPEATED_FIELD("dyn(TestAllTypes{repeated_int64: []}).repeated_int64 == []"),
DYN_MESSAGE_DEFAULT_SCALAR_FIELD("dyn(TestAllTypes{single_int64: 0}).single_int64 == 0"),
DYN_MESSAGE_UNSET_NESTED_FIELD("dyn(TestAllTypes.NestedMessage{}).bb == 0"),
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{}"),
// Whether an empty list(dyn) field is set is the same in every literal.
STRUCT_EMPTY_LIST_DYN_FIELD_PRESENCE_CONSISTENT(
"has(TestAllTypes{list_value: []}.list_value)"
+ " == has(TestAllTypes{list_value: []}.list_value)"),
STRUCT_EMPTY_MESSAGE_FIELD_INEQUALITY(
"TestAllTypes{standalone_message: TestAllTypes.NestedMessage{}} != TestAllTypes{}"),
IEEE_754_NAN_NEQ_ITSELF("(0.0 / 0.0) != (0.0 / 0.0)"),
Expand Down Expand Up @@ -1682,6 +1719,13 @@ public void isSatisfiable_mapWithUnusedApproximateIteration_verified() throws Ex
}

private enum UnconditionalErrorTestCase {
HAS_UNDECLARED_FIELD_OF_DYN_MESSAGE(
"has(dyn(TestAllTypes.NestedMessage{}).single_int64)"
+ " || !has(dyn(TestAllTypes.NestedMessage{}).single_int64)"),
HAS_FIELD_OF_DYN_SCALAR("has(dyn(42).f) || !has(dyn(42).f)"),
DYN_MESSAGE_UNDECLARED_FIELD(
"dyn(TestAllTypes.NestedMessage{}).single_int64 == 0"
+ " || dyn(TestAllTypes.NestedMessage{}).single_int64 != 0"),
MAP_MISSING_KEY("{'a': 1}['b'] == 0 || !({'a': 1}['b'] == 0)"),
COLLECTION_ERROR("{'a': 1 / 0} == {'a': 1 / 0}"),
LIST_ERROR("[1 / 0] == [1 / 0]"),
Expand Down Expand Up @@ -1810,6 +1854,10 @@ public void verifyEquivalence_infinityConstants_notEquivalent() throws Exception
}

private enum IsAlwaysTrueViolationTestCase {
// 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{}",
"Condition is not always true\\."),
NOT_ALWAYS_TRUE(
"x > 5", "Condition is not always true\\.", "Counterexample input:", "x = -?\\d+"),
UNINTERPRETED_CONVERSION_CAN_ERROR_INT(
Expand Down Expand Up @@ -2198,6 +2246,11 @@ private enum IsInconclusiveTestCase {
// The approximate operand may really be false, which absorbs the error.
LOGICAL_AND_APPROXIMATE_OPERAND_WITH_ERROR(
"size(int_list) < 6 || !(dyn(int_list)[5] == 'x' && 1 / 0 == 1)"),
// An empty list(dyn) or map(string, dyn) field is set if it's a ListValue or Struct, and unset
// if it's repeated or a map.
EMPTY_REPEATED_VALUE_FIELD("TestAllTypes{repeated_value: []} != TestAllTypes{}"),
EMPTY_MAP_VALUE_FIELD("TestAllTypes{map_string_value: {}} != TestAllTypes{}"),
EMPTY_LIST_VALUE_FIELD("!has(TestAllTypes{list_value: []}.list_value)"),
;

private final String expr;
Expand Down Expand Up @@ -2461,8 +2514,9 @@ private enum EquivalenceTestCase {
+ " [nested_list[1]] : true",
"true"),
NESTED_DYNAMIC_MAP_LOOKUP_EXTENSIONALITY(
"has(dyn_map.a) && has(dyn_map.a.b) && has(dyn_map.c) && has(dyn_map.c.d) && dyn_map.a.b =="
+ " dyn_map.c.d ? [dyn_map.a.b] == [dyn_map.c.d] : true",
"has(dyn_map.a) && type(dyn_map.a) == map && has(dyn_map.a.b) && has(dyn_map.c)"
+ " && type(dyn_map.c) == map && has(dyn_map.c.d) && dyn_map.a.b == dyn_map.c.d"
+ " ? [dyn_map.a.b] == [dyn_map.c.d] : true",
"true"),
MULTIPLY("x * y", "y * x"),
DIVIDE("x / y == 5", "5 == x / y"),
Expand Down
Loading