Skip to content

Prevent spurious counterexamples on maps by tightening its domain #1161

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
Aug 5, 2026
Merged

Prevent spurious counterexamples on maps by tightening its domain #1161

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
15 changes: 7 additions & 8 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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);

Expand All @@ -893,14 +889,15 @@ private TranslatedValue translateDynamicComprehension(
}
}

private void applyBoundedMapBijection(
private BoolExpr getBoundedMapBijection(
ArrayExpr mapPresence, SeqExpr<?> seq, ArithExpr lengthExpr) {
List<BoolExpr> 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));
}
}

Expand All @@ -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(
Expand Down Expand Up @@ -1335,6 +1333,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {

List<BoolExpr> 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);
Expand Down
6 changes: 4 additions & 2 deletions verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
51 changes: 32 additions & 19 deletions verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -179,14 +179,26 @@ private static String reconstructList(

private static String reconstructMap(
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
Expr<?> presenceArray =
List<Expr<?>> keys = new ArrayList<>();
Expr<?> lenExpr =
evaluateStrict(
model,
typeSystem.getMapPresence(mapRef),
String.format("Z3 failed to evaluate presence array natively for map %s", mapRef));

List<Expr<?>> 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<String> entries = new ArrayList<>();
for (Expr<?> key : keys) {
Expand Down Expand Up @@ -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(
Expand All @@ -230,7 +242,7 @@ private static String reconstructMessage(
String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");

List<Expr<?>> keys = new ArrayList<>();
extractKeys(valuesArray, keys);
extractKeys(presenceArray, keys);

List<String> entries = new ArrayList<>();
for (Expr<?> key : keys) {
Expand Down Expand Up @@ -268,16 +280,17 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> 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;
}
}

Expand Down
13 changes: 5 additions & 8 deletions verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) ->
Expand All @@ -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(),
Expand All @@ -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(),
Expand All @@ -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) ->
Expand All @@ -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) ->
Expand Down
13 changes: 5 additions & 8 deletions verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) ->
Expand All @@ -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(),
Expand All @@ -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(),
Expand All @@ -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) ->
Expand All @@ -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) ->
Expand Down
13 changes: 5 additions & 8 deletions verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) ->
Expand All @@ -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) ->
Expand All @@ -92,15 +89,15 @@ 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) ->
Optional.of(
typeSystem.wrapBool(
AxiomHelpers.mkFpLtReal(
ctx,
(FPExpr) typeSystem.getDouble(lhs),
typeSystem.getDouble(lhs),
ctx.mkInt2Real(typeSystem.getInt(rhs))))))
.addBinaryOverloadTranslator(
Comparison.LESS_DOUBLE_UINT64.celOverloadDecl(),
Expand All @@ -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(),
Expand Down
13 changes: 5 additions & 8 deletions verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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) ->
Expand All @@ -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) ->
Expand All @@ -92,15 +89,15 @@ 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) ->
Optional.of(
typeSystem.wrapBool(
AxiomHelpers.mkFpLeReal(
ctx,
(FPExpr) typeSystem.getDouble(lhs),
typeSystem.getDouble(lhs),
ctx.mkInt2Real(typeSystem.getInt(rhs))))))
.addBinaryOverloadTranslator(
Comparison.LESS_EQUALS_DOUBLE_UINT64.celOverloadDecl(),
Expand All @@ -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(),
Expand Down
4 changes: 1 addition & 3 deletions verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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)));
Expand Down
2 changes: 1 addition & 1 deletion verifier/src/test/java/dev/cel/verifier/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ java_library(

junit4_test_suites(
name = "test_suites",
shard_count = 4,
shard_count = 8,
sizes = [
"small",
"medium",
Expand Down
Loading
Loading