diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index e3bb1bfaf..c1a8848e2 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -1247,9 +1247,10 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } Expr optRef = typeSystem.getOptionalRef(val); BoolExpr hasValue = typeSystem.optHasValue(optRef); - BoolExpr valConstraint = - createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType); - return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint)); + Expr optVal = typeSystem.getOptionalValue(optRef); + BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal)); + BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType); + return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); } if (type.equals(SimpleType.BOOL)) { return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val); @@ -1289,15 +1290,13 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } if (type instanceof ListType) { - // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers - // here. + // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather + // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops. + // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ + // typeConstraint(seq[i]) BoolExpr isList = typeSystem.isList(val); CelType elemType = ((ListType) type).elemType(); - if (elemType.equals(SimpleType.DYN)) { - return isList; - } - // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i]) Expr listRef = typeSystem.getListRef(val); SeqExpr seq = typeSystem.getSeq(listRef); Expr length = ctx.mkLength(seq); @@ -1307,20 +1306,58 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { for (int i = 0; i < comprehensionUnrollLimit; i++) { IntExpr idx = ctx.mkInt(i); Expr elem = ctx.mkNth(seq, idx); - BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); BoolExpr validIndex = ctx.mkLt(idx, length); + // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in + // list(dyn). For concrete types, this is already implied by createTypeConstraintForType. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem)))); + BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); - BoolExpr outOfBounds = ctx.mkGe(idx, length); - boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown()))); } return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type instanceof MapType) { - // Do NOT emit a for-all quantifier over map keys here. - // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is - // naturally constrained by the primitive key assertions in getStructuralEquality(). - return typeSystem.isMap(val); + // Do NOT emit a for-all quantifier over map keys or values here. + // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using + // bounded unrolling over the key sequence up to comprehensionUnrollLimit. + // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key) + // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val)) + BoolExpr isMap = typeSystem.isMap(val); + MapType mapType = (MapType) type; + CelType keyType = mapType.keyType(); + CelType valType = mapType.valueType(); + + Expr mapRef = typeSystem.getMapRef(val); + SeqExpr seq = typeSystem.getMapKeys(mapRef); + Expr length = ctx.mkLength(seq); + ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); + ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); + + List boundsAndTypes = new ArrayList<>(); + boundsAndTypes.add(isMap); + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + Expr key = ctx.mkNth(seq, idx); + BoolExpr validIndex = ctx.mkLt(idx, length); + + BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key); + BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key)); + // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in + // map(dyn, ...). For concrete map types, this is already implied by keyType constraints. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError))); + boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType))); + + BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key); + BoolExpr validEntry = ctx.mkAnd(validIndex, presence); + + Expr mapVal = ctx.mkSelect(mapValues, key); + BoolExpr valNotError = ctx.mkNot(typeSystem.isError(mapVal)); + boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); + boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); + } + + return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type.kind() == CelKind.STRUCT) { return ctx.mkAnd( diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 2355d36bf..f52886a42 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -127,6 +127,8 @@ private static String formatExpr( return "Error"; } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) { return "Unknown"; + } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) { + return "null"; } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) { Expr optRef = expr.getArgs()[0]; Expr hasValueExpr = diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index e9a1872c9..1c1435e3b 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -685,6 +685,11 @@ public Expr getBytes(Expr val) { return ctx.mkApp(bytesCons.getAccessorDecls()[0], val); } + /** Checks if the given CelValue is a valid primitive map key type. */ + public BoolExpr isPrimitiveKey(Expr val) { + return ctx.mkOr(isBool(val), isInt(val), isUint(val), isString(val), isBytes(val)); + } + /** Checks if the given CelValue is a struct (message). */ public BoolExpr isStruct(Expr val) { return isMessage(val); diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 1a41ef743..f230714b2 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -197,6 +197,80 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)"); } + @Test + public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("string_int_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_listNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_list.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_list = ["); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_dynMapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void counterexample_nullValueFormattedAsNull() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("unknown_var == 3u && request == null").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("request = null"); + } + + private enum CounterexampleNeverErrorTestCase { + DYN_LIST_REFLEXIVITY("dyn_list.size() == 1 ? dyn_list[0] == dyn_list[0] : true"), + 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'"), + ; + + final String expr; + + CounterexampleNeverErrorTestCase(String expr) { + this.expr = expr; + } + } + + @Test + public void isAlwaysTrue_counterexampleNeverContainsError( + @TestParameter CounterexampleNeverErrorTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).doesNotContain("Error"); + } + @Test public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exception { CelAbstractSyntaxTree ast = CEL.compile("1 + 1 == 2").getAst(); @@ -747,6 +821,9 @@ private enum IsAlwaysTrueTestCase { UINT64_BOUNDS_ALWAYS_TRUE("u <= 18446744073709551615u && u >= 0u"), MODULO_INT64_MIN_INT_BY_NEG_ONE_ALWAYS_ZERO( "x == -9223372036854775808 && y == -1 ? x % y == 0 : true"), + DYNAMIC_VAR_TYPE_IDENTITY("type(dyn_var) == type(dyn_var)"), + DYNAMIC_MAP_KEY_COMPREHENSION_TYPE_IDENTITY( + "size(dyn_map) > 0 && size(dyn_map) <= 5 ? dyn_map.all(k, type(k) == type(k)) : true"), ; final String expr;