From 54ecf526783109a0ef6a2e54ae3fede1e5010e58 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 5 Aug 2026 14:24:55 -0700 Subject: [PATCH] Prevent spurious counterexamples on maps by tightening its domain PiperOrigin-RevId: 959869777 --- .../cel/verifier/CelAstToZ3Translator.java | 15 +++--- .../dev/cel/verifier/CelVerifierZ3Impl.java | 6 ++- .../CelZ3CounterexampleGenerator.java | 51 ++++++++++++------- .../dev/cel/verifier/axioms/GreaterAxiom.java | 13 ++--- .../verifier/axioms/GreaterEqualsAxiom.java | 13 ++--- .../dev/cel/verifier/axioms/LessAxiom.java | 13 ++--- .../cel/verifier/axioms/LessEqualsAxiom.java | 13 ++--- .../verifier/axioms/TypeConversionAxioms.java | 4 +- .../test/java/dev/cel/verifier/BUILD.bazel | 2 +- .../cel/verifier/CelVerifierZ3ImplTest.java | 47 +++++++++++++++-- 10 files changed, 108 insertions(+), 69 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index c1a8848e2..e253b27ad 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -741,7 +741,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); - boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true); + boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN); BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); @@ -877,10 +877,6 @@ private TranslatedValue translateDynamicComprehension( ArrayExpr mapPresence = isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null; - if (isMap) { - applyBoundedMapBijection(mapPresence, seq, lengthExpr); - } - BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)); truncationConditions.add(isTruncated); @@ -893,14 +889,15 @@ private TranslatedValue translateDynamicComprehension( } } - private void applyBoundedMapBijection( + private BoolExpr getBoundedMapBijection( ArrayExpr mapPresence, SeqExpr seq, ArithExpr lengthExpr) { + List constraints = new ArrayList<>(); for (int i = 0; i < comprehensionUnrollLimit; i++) { for (int j = i + 1; j < comprehensionUnrollLimit; j++) { BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr); BoolExpr notEqual = ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j)))); - typeConstraints.add(ctx.mkImplies(validPair, notEqual)); + constraints.add(ctx.mkImplies(validPair, notEqual)); } } @@ -915,7 +912,8 @@ private void applyBoundedMapBijection( ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()), seqMap); } - typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + return CelZ3TypeSystem.mkAndFlattened(ctx, constraints); } private TranslatedValue[] evaluateLoopCondAndStep( @@ -1335,6 +1333,7 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { List boundsAndTypes = new ArrayList<>(); boundsAndTypes.add(isMap); + boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length)); for (int i = 0; i < comprehensionUnrollLimit; i++) { IntExpr idx = ctx.mkInt(i); diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 510d88ec0..90d7238c2 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -303,8 +303,10 @@ CelVerificationResult verifyImplication( /* isCounterexample= */ true)); case TRUNCATED: return CelVerificationResult.inconclusive( - String.format("Inconclusive: %s holds within the current loop unroll limit, but" - + " may be violated for larger collections.", subjectName.toLowerCase(Locale.US))); + String.format( + "Inconclusive: %s holds within the current loop unroll limit, but" + + " may be violated for larger collections.", + subjectName.toLowerCase(Locale.US))); case NO_MATCH: return CelVerificationResult.verified(); case SOLVER_UNKNOWN: diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index f52886a42..104e224a6 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -179,14 +179,26 @@ private static String reconstructList( private static String reconstructMap( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr mapRef) { - Expr presenceArray = + List> keys = new ArrayList<>(); + Expr lenExpr = evaluateStrict( model, - typeSystem.getMapPresence(mapRef), - String.format("Z3 failed to evaluate presence array natively for map %s", mapRef)); - - List> keys = new ArrayList<>(); - extractKeys(presenceArray, keys); + ctx.mkLength(typeSystem.getMapKeys(mapRef)), + String.format("Z3 failed to evaluate length for map %s", mapRef)); + if (lenExpr instanceof IntNum) { + int length = ((IntNum) lenExpr).getInt(); + int printLimit = Math.min(length, 100); + for (int i = 0; i < printLimit; i++) { + Expr elem = + evaluateStrict( + model, + ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)), + String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef)); + if (!keys.contains(elem)) { + keys.add(elem); + } + } + } List entries = new ArrayList<>(); for (Expr key : keys) { @@ -215,11 +227,11 @@ private static String reconstructMap( private static String reconstructMessage( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr msgRef) { - Expr valuesArray = + Expr presenceArray = evaluateStrict( model, - typeSystem.getMsgValues(msgRef), - String.format("Z3 failed to evaluate values array natively for msg %s", msgRef)); + typeSystem.getMsgPresence(msgRef), + String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef)); Expr typeNameExpr = evaluateStrict( @@ -230,7 +242,7 @@ private static String reconstructMessage( String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); List> keys = new ArrayList<>(); - extractKeys(valuesArray, keys); + extractKeys(presenceArray, keys); List entries = new ArrayList<>(); for (Expr key : keys) { @@ -268,16 +280,17 @@ private static void extractKeys(Expr arrayExpr, List> keys) { FuncDecl decl = arrayExpr.getFuncDecl(); String declName = decl.getName().toString(); - if (!declName.equals("store")) { - break; + if (declName.equals("store")) { + Expr[] args = arrayExpr.getArgs(); + Preconditions.checkState( + args.length == 3, "Z3 store array operation must have exactly 3 arguments"); + if (!keys.contains(args[1])) { + keys.add(args[1]); + } + arrayExpr = args[0]; + continue; } - - Expr[] args = arrayExpr.getArgs(); - Preconditions.checkState( - args.length == 3, "Z3 store array operation must have exactly 3 arguments"); - keys.add(args[1]); - - arrayExpr = args[0]; + break; } } diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java index 292b86135..2ccb1543a 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class GreaterAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPGt( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPGt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -82,7 +79,7 @@ final class GreaterAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_UINT64_DOUBLE.celOverloadDecl(), @@ -91,7 +88,7 @@ final class GreaterAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_INT64.celOverloadDecl(), @@ -101,7 +98,7 @@ final class GreaterAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getInt(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -110,7 +107,7 @@ final class GreaterAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getUint(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java index 4be0c23e2..d71f0f248 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class GreaterEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPGEq( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPGEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -82,7 +79,7 @@ final class GreaterEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_UINT64_DOUBLE.celOverloadDecl(), @@ -91,7 +88,7 @@ final class GreaterEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_INT64.celOverloadDecl(), @@ -101,7 +98,7 @@ final class GreaterEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getInt(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -110,7 +107,7 @@ final class GreaterEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getUint(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java index e09484f28..31b1d3a21 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class LessAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPLt( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPLt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -83,7 +80,7 @@ final class LessAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -92,7 +89,7 @@ final class LessAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -100,7 +97,7 @@ final class LessAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_UINT64.celOverloadDecl(), @@ -109,7 +106,7 @@ final class LessAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java index e27b47631..c2466cf1b 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class LessEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPLEq( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPLEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -83,7 +80,7 @@ final class LessEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -92,7 +89,7 @@ final class LessEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -100,7 +97,7 @@ final class LessEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_UINT64.celOverloadDecl(), @@ -109,7 +106,7 @@ final class LessEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index 8cd844214..f4dba5afc 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -19,7 +19,6 @@ import com.google.common.collect.ImmutableList; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Sort; @@ -233,8 +232,7 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res))); sink.accept( ctx.mkImplies( - typeSystem.isDouble(res), - ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res))))); + typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res))))); break; case STRING: sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res))); diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index de788ca5c..6bf44cafd 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -61,7 +61,7 @@ java_library( junit4_test_suites( name = "test_suites", - shard_count = 4, + shard_count = 8, sizes = [ "small", "medium", diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index f230714b2..696a21387 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -157,12 +157,22 @@ private enum IsSatisfiableTestCase { CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"), MACRO_LIMIT("dyn_list.all(x, x == 1)"), STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"), - NULLABLE_INT_SATISFIABLE("nullable_int == 123"); + NULLABLE_INT_SATISFIABLE("nullable_int == 123"), + MAP_INDEX_SATISFIABLE("string_int_map['alice'] > 0", "\"alice\": [1-9]\\d*"), + MAP_SIZE_GREATER_THAN_ONE_WITH_KEY( + "string_int_map.size() > 1 && string_int_map['foo'] == 42", + "string_int_map = \\{[^}]*,[^}]*\\}"), + MAP_SIZE_GREATER_THAN_ONE_WITH_LIST_ELEMENT( + "string_int_map.size() > 1 && string_int_map['a'] == int_list[0] && int_list.size() == 1", + "string_int_map = \\{[^}]*,[^}]*\\}"), + ; final String expr; + final ImmutableList expectedFragments; - IsSatisfiableTestCase(String expr) { + IsSatisfiableTestCase(String expr, String... expectedFragments) { this.expr = expr; + this.expectedFragments = ImmutableList.copyOf(expectedFragments); } } @@ -183,6 +193,9 @@ public void isSatisfiable_success(@TestParameter IsSatisfiableTestCase testCase) CelVerificationResult result = VERIFIER.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + for (String fragment : testCase.expectedFragments) { + assertThat(result.message()).containsMatch(fragment); + } } @Test @@ -251,6 +264,7 @@ private enum CounterexampleNeverErrorTestCase { DYN_MAP_REFLEXIVITY("dyn_map.size() == 1 ? dyn_map[1] == dyn_map[1] : true"), DYN_LIST_ELEMENT("size(dyn_list) == 1 && dyn_list[0] == 'impossible_value'"), DYN_MAP_VALUE("size(dyn_map) == 1 && dyn_map['a'] == 'impossible_value'"), + STRUCT_FIELD_VALUE("test_all_types.single_int64 == 12345 && false"), ; final String expr; @@ -365,7 +379,28 @@ private enum IsUnsatisfiableTestCase { TIMESTAMP_INEQUALITY_CONTRADICTION( "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"), TYPE_TIMESTAMP_NOT_INT("type(timestamp('1970-01-01T00:00:00Z')) == int"), - DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"); + DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"), + DYNAMIC_MAP_DUPLICATE_KEYS_CONTRADICTION( + "size(string_int_map) == 2 && string_int_map.all(k, k == 'a')"), + EMPTY_MAP_WITH_KEY_IN("string_int_map.size() == 0 && 'foo' in string_int_map"), + KEY_IN_EMPTY_MAP("('x' in string_int_map) && string_int_map.size() == 0"), + EMPTY_MAP_AND_LIST_WITH_KEY_IN( + "int_list.size() == string_int_map.size() && int_list.size() == 0 && 'a' in" + + " string_int_map"), + MAP_SIZE_ONE_TWO_KEYS( + "string_int_map.size() == 1 && string_int_map['a'] == 1 && string_int_map['b'] == 2"), + MAP_SIZE_LESS_THAN_TWO_TWO_KEYS( + "string_int_map['foo'] == 10 && string_int_map['bar'] == 20 && string_int_map.size() < 2"), + MAP_SIZE_ONE_SUM_TWO_KEYS( + "string_int_map['a'] + string_int_map['b'] == 10 && string_int_map.size() == 1"), + MAP_SIZE_ONE_TWO_EQUAL_KEYS( + "string_int_map.size() == 1 && string_int_map['foo'] == 10 && string_int_map['bar'] == 10"), + MAP_SIZE_TWO_THREE_KEYS( + "string_int_map['k1'] == 1 && string_int_map['k2'] == 2 && string_int_map['k3'] == 3 &&" + + " string_int_map.size() == 2"), + EMPTY_MAP_KEY_LOOKUP("string_int_map['a'] > 100 && string_int_map.size() == 0"), + EMPTY_MAP_DYNAMIC_KEY_LOOKUP("string_int_map[string_var] == 100 && string_int_map.size() == 0"), + ; final String expr; @@ -1343,7 +1378,7 @@ private enum IsAlwaysTrueViolationTestCase { + "? dyn_map[1 + 1] == [] : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_map = \\{\\}"), + "dyn_map = \\{.*\\}"), DYNAMIC_MAP_COMPREHENSION_NESTED_EQUALITY_VIOLATION( "cel.bind(r, request, r.l == [[1], [2], [3], [4], [5]] && r.m == {1: [1], 2: [2]," + " 3: [3]} ? r.l.all(x, r.m.exists(k, r.m[k] == x)) : true)", @@ -1601,6 +1636,9 @@ private enum EquivalenceTestCase { MACRO_EXISTS_ONE_EQUIVALENT( "[1, 2, 3].exists_one(x, x == 2)", "(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"), + TIMESTAMP_CONVERSION_OVERFLOW_EQUIVALENCE( + "timestamp(string_var) <= timestamp(253402300799)", + "timestamp(string_var) == timestamp(string_var)"), TIMESTAMP_MATH_SUBTRACT_TS( "timestamp(900000) - timestamp(100)", "timestamp(899900) - timestamp(0)"), TIMESTAMP_MATH_COMMUTATIVITY( @@ -2937,3 +2975,4 @@ public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() t assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } } +