diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java index d31fc958b..11cc36191 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java @@ -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; @@ -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. */ @@ -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 elementsTv = new ArrayList<>(); + List invalidFields = new ArrayList<>(); + Set fields = new HashSet<>(); for (CelExpr.CelStruct.Entry entryAst : createStruct.entries()) { Expr key = ctx.mkString(entryAst.fieldKey()); @@ -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(); @@ -126,7 +132,6 @@ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) { optionalHasValue = typeSystem.optHasValue(optRef); finalValue = typeSystem.getOptionalValue(optRef); } - elementsTv.add(valueTv); // Canonicalization Trick: // @@ -136,17 +141,56 @@ 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( @@ -154,7 +198,9 @@ TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) { 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); } @@ -368,6 +414,7 @@ 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(); @@ -375,7 +422,8 @@ private Expr getDefaultValueForType(CelType type) { 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)) { @@ -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()); @@ -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 isModeledType = new ArrayList<>(); + List 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 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)); @@ -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) { diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index c40cba230..383bb8ba0 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -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( @@ -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( @@ -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( @@ -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"), @@ -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)"), @@ -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]"), @@ -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( @@ -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; @@ -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"),