Skip to content

Commit 95fb796

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Tighten the counterexample domain for double/int and parameterized unknown
PiperOrigin-RevId: 957339001
1 parent 75e0900 commit 95fb796

22 files changed

Lines changed: 530 additions & 173 deletions

‎verifier/BUILD.bazel‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,13 @@ java_library(
4141
exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"],
4242
)
4343

44+
java_library(
45+
name = "numeric_bounds",
46+
compatible_with = [],
47+
visibility = [":verifier_internal"],
48+
exports = ["//verifier/src/main/java/dev/cel/verifier:numeric_bounds"],
49+
)
50+
4451
java_library(
4552
name = "type_system",
4653
compatible_with = [],

‎verifier/src/main/java/dev/cel/verifier/BUILD.bazel‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,13 +91,27 @@ java_library(
9191
],
9292
)
9393

94+
java_library(
95+
name = "numeric_bounds",
96+
srcs = ["CelNumericBounds.java"],
97+
compatible_with = [],
98+
tags = [
99+
],
100+
deps = [
101+
"//:auto_value",
102+
"//common/annotations",
103+
"@maven//:com_google_guava_guava",
104+
],
105+
)
106+
94107
java_library(
95108
name = "type_system",
96109
srcs = ["CelZ3TypeSystem.java"],
97110
compatible_with = [],
98111
tags = [
99112
],
100113
deps = [
114+
":numeric_bounds",
101115
"//common/internal:proto_time_utils",
102116
"@maven//:com_google_errorprone_error_prone_annotations",
103117
"@maven//:com_google_guava_guava",
@@ -121,6 +135,7 @@ java_library(
121135
tags = [
122136
],
123137
deps = [
138+
":numeric_bounds",
124139
":type_system",
125140
":verifier",
126141
"//:auto_value",

‎verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java‎

Lines changed: 6 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,9 @@
2424
import dev.cel.common.ast.CelConstant;
2525
import dev.cel.common.ast.CelExpr;
2626
import java.util.ArrayList;
27+
import java.util.HashMap;
2728
import java.util.List;
29+
import java.util.Map;
2830
import org.jspecify.annotations.Nullable;
2931

3032
/**
@@ -83,29 +85,22 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c
8385
context.hasher.putByte((byte) 0); // 0 = bound
8486
context.hasher.putInt(bIdx);
8587
} else {
86-
int fIdx = -1;
87-
for (int i = 0; i < context.freeVars.size(); i++) {
88-
if (context.freeVars.get(i).ident().name().equals(name)) {
89-
fIdx = i;
90-
break;
91-
}
92-
}
93-
if (fIdx == -1) {
88+
Integer fIdx = context.freeVarIndices.get(name);
89+
if (fIdx == null) {
9490
context.freeVars.add(expr);
9591
fIdx = context.freeVars.size() - 1;
92+
context.freeVarIndices.put(name, fIdx);
9693
}
9794
context.hasher.putByte((byte) 1); // 1 = free
9895
context.hasher.putInt(fIdx);
9996
}
10097
break;
10198
case SELECT:
10299
hashAst(expr.select().operand(), scope, context);
103-
context.hasher.putInt(expr.select().field().length());
104100
context.hasher.putString(expr.select().field(), UTF_8);
105101
context.hasher.putBoolean(expr.select().testOnly());
106102
break;
107103
case CALL:
108-
context.hasher.putInt(expr.call().function().length());
109104
context.hasher.putString(expr.call().function(), UTF_8);
110105
context.hasher.putBoolean(expr.call().target().isPresent());
111106
if (expr.call().target().isPresent()) {
@@ -210,6 +205,7 @@ private static void hashConstant(CelConstant constant, HasherContext context) {
210205

211206
private static final class HasherContext {
212207
final Hasher hasher;
208+
final Map<String, Integer> freeVarIndices = new HashMap<>();
213209
final List<CelExpr> freeVars = new ArrayList<>();
214210

215211
HasherContext(HashFunction hashFunction) {

‎verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java‎

Lines changed: 21 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -741,7 +741,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
741741
typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
742742
typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
743743

744-
boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true);
744+
boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
745745
BoolExpr isApprox = ctx.mkBool(!isDynamic);
746746
return TranslatedValue.propagateStrict(
747747
ctx, typeSystem, callRes, Optional.of(expr), isApprox, args);
@@ -877,10 +877,6 @@ private TranslatedValue translateDynamicComprehension(
877877
ArrayExpr mapPresence =
878878
isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null;
879879

880-
if (isMap) {
881-
applyBoundedMapBijection(mapPresence, seq, lengthExpr);
882-
}
883-
884880
BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
885881
truncationConditions.add(isTruncated);
886882

@@ -893,14 +889,15 @@ private TranslatedValue translateDynamicComprehension(
893889
}
894890
}
895891

896-
private void applyBoundedMapBijection(
892+
private BoolExpr getBoundedMapBijection(
897893
ArrayExpr mapPresence, SeqExpr<?> seq, ArithExpr lengthExpr) {
894+
List<BoolExpr> constraints = new ArrayList<>();
898895
for (int i = 0; i < comprehensionUnrollLimit; i++) {
899896
for (int j = i + 1; j < comprehensionUnrollLimit; j++) {
900897
BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr);
901898
BoolExpr notEqual =
902899
ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j))));
903-
typeConstraints.add(ctx.mkImplies(validPair, notEqual));
900+
constraints.add(ctx.mkImplies(validPair, notEqual));
904901
}
905902
}
906903

@@ -915,7 +912,8 @@ private void applyBoundedMapBijection(
915912
ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
916913
seqMap);
917914
}
918-
typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
915+
constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
916+
return CelZ3TypeSystem.mkAndFlattened(ctx, constraints);
919917
}
920918

921919
private TranslatedValue[] evaluateLoopCondAndStep(
@@ -1230,7 +1228,7 @@ private BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSynta
12301228
.orElseThrow(
12311229
() -> new IllegalArgumentException("Type not found for expr ID: " + exprId));
12321230
BoolExpr typeConstraint = createTypeConstraintForType(val, type);
1233-
return ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val), typeConstraint);
1231+
return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint);
12341232
}
12351233

12361234
private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
@@ -1259,15 +1257,15 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
12591257
Expr<?> unwrapped = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], val);
12601258
return ctx.mkAnd(
12611259
ctx.mkApp(typeSystem.intCons().getTesterDecl(), val),
1262-
ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MIN_INT64)),
1263-
ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_INT64)));
1260+
ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MIN_INT64)),
1261+
ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_INT64)));
12641262
}
12651263
if (type.equals(SimpleType.UINT)) {
12661264
Expr<?> unwrapped = ctx.mkApp(typeSystem.uintCons().getAccessorDecls()[0], val);
12671265
return ctx.mkAnd(
12681266
ctx.mkApp(typeSystem.uintCons().getTesterDecl(), val),
12691267
ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(0)),
1270-
ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_UINT64)));
1268+
ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_UINT64)));
12711269
}
12721270
if (type.equals(SimpleType.DOUBLE)) {
12731271
return (BoolExpr) ctx.mkApp(typeSystem.doubleCons().getTesterDecl(), val);
@@ -1335,6 +1333,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
13351333

13361334
List<BoolExpr> boundsAndTypes = new ArrayList<>();
13371335
boundsAndTypes.add(isMap);
1336+
boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
13381337

13391338
for (int i = 0; i < comprehensionUnrollLimit; i++) {
13401339
IntExpr idx = ctx.mkInt(i);
@@ -1352,7 +1351,10 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
13521351
BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
13531352

13541353
Expr mapVal = ctx.mkSelect(mapValues, key);
1355-
BoolExpr valNotError = ctx.mkNot(typeSystem.isError(mapVal));
1354+
BoolExpr valNotError =
1355+
unknownIdentifiers.isEmpty()
1356+
? ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal))
1357+
: ctx.mkNot(typeSystem.isError(mapVal));
13561358
boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
13571359
boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
13581360
}
@@ -1410,6 +1412,12 @@ private Optional<Object> toCacheKey(CelExpr expr) {
14101412
case CONSTANT:
14111413
return Optional.of(expr.constant());
14121414
case LIST:
1415+
if (!expr.list().optionalIndices().isEmpty()) {
1416+
// Do not cache lists with optional elements. Optional elements conditionally alter
1417+
// sequence length and presence via ITE branches at runtime; caching would collide
1418+
// [1, 2] with [?1, 2] and freeze conditional evaluations to a static reference.
1419+
return Optional.empty();
1420+
}
14131421
ImmutableList.Builder<Object> builder = ImmutableList.builder();
14141422
for (CelExpr elem : expr.list().elements()) {
14151423
Optional<Object> elemKey = toCacheKey(elem);

‎verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
// Copyright 2026 Google LLC
2+
//
3+
// Licensed under the Apache License, Version 2.0 (the "License");
4+
// you may not use this file except in compliance with the License.
5+
// You may obtain a copy of the License at
6+
//
7+
// https://www.apache.org/licenses/LICENSE-2.0
8+
//
9+
// Unless required by applicable law or agreed to in writing, software
10+
// distributed under the License is distributed on an "AS IS" BASIS,
11+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
// See the License for the specific language governing permissions and
13+
// limitations under the License.
14+
15+
package dev.cel.verifier;
16+
17+
import com.google.auto.value.AutoValue;
18+
import com.google.common.primitives.UnsignedLong;
19+
import dev.cel.common.annotations.Internal;
20+
import java.util.Optional;
21+
22+
/**
23+
* Utility for computing matching integer and unsigned integer ranges for IEEE-754 double-precision
24+
* floating-point constants in Z3 verification.
25+
*/
26+
@Internal
27+
public final class CelNumericBounds {
28+
29+
/** Minimum representable signed 64-bit integer string. */
30+
public static final String MIN_INT64 = "-9223372036854775808";
31+
32+
/** Maximum representable signed 64-bit integer string. */
33+
public static final String MAX_INT64 = "9223372036854775807";
34+
35+
/** Maximum representable unsigned 64-bit integer string. */
36+
public static final String MAX_UINT64 = "18446744073709551615";
37+
38+
private static final double TWO_TO_63 = Math.scalb(1.0, 63);
39+
private static final double TWO_TO_64 = Math.scalb(1.0, 64);
40+
41+
@AutoValue
42+
abstract static class IntRange {
43+
abstract long min();
44+
45+
abstract long max();
46+
47+
static IntRange of(long min, long max) {
48+
return new AutoValue_CelNumericBounds_IntRange(min, max);
49+
}
50+
}
51+
52+
@AutoValue
53+
abstract static class UintRange {
54+
abstract String min();
55+
56+
abstract String max();
57+
58+
static UintRange of(String min, String max) {
59+
return new AutoValue_CelNumericBounds_UintRange(min, max);
60+
}
61+
}
62+
63+
private static boolean isMathematicalInteger(double vDouble) {
64+
return Double.isFinite(vDouble) && vDouble == Math.rint(vDouble);
65+
}
66+
67+
static Optional<IntRange> getMatchingIntRange(double vDouble) {
68+
if (!isMathematicalInteger(vDouble) || vDouble < -TWO_TO_63 || vDouble > TWO_TO_63) {
69+
return Optional.empty();
70+
}
71+
long minL = (long) vDouble;
72+
while (minL > Long.MIN_VALUE && (double) (minL - 1) == vDouble) {
73+
minL--;
74+
}
75+
long maxL = (long) vDouble;
76+
while (maxL < Long.MAX_VALUE && (double) (maxL + 1) == vDouble) {
77+
maxL++;
78+
}
79+
return Optional.of(IntRange.of(minL, maxL));
80+
}
81+
82+
static Optional<UintRange> getMatchingUintRange(double vDouble) {
83+
if (!isMathematicalInteger(vDouble) || vDouble < 0 || vDouble > TWO_TO_64) {
84+
return Optional.empty();
85+
}
86+
// XOR with Long.MIN_VALUE (0x8000000000000000L) flips bit 63 to 1, encoding unsigned values
87+
// >= 2^63 into Java's two's-complement signed long representation.
88+
long uBits =
89+
vDouble < TWO_TO_63 ? (long) vDouble : (long) (vDouble - TWO_TO_63) ^ Long.MIN_VALUE;
90+
UnsignedLong uVal = UnsignedLong.fromLongBits(uBits);
91+
UnsignedLong minU = uVal;
92+
while (!minU.equals(UnsignedLong.ZERO)
93+
&& minU.minus(UnsignedLong.ONE).doubleValue() == vDouble) {
94+
minU = minU.minus(UnsignedLong.ONE);
95+
}
96+
UnsignedLong maxU = uVal;
97+
while (!maxU.equals(UnsignedLong.MAX_VALUE)
98+
&& maxU.plus(UnsignedLong.ONE).doubleValue() == vDouble) {
99+
maxU = maxU.plus(UnsignedLong.ONE);
100+
}
101+
return Optional.of(UintRange.of(minU.toString(), maxU.toString()));
102+
}
103+
104+
private CelNumericBounds() {}
105+
}

‎verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,8 +303,10 @@ CelVerificationResult verifyImplication(
303303
/* isCounterexample= */ true));
304304
case TRUNCATED:
305305
return CelVerificationResult.inconclusive(
306-
String.format("Inconclusive: %s holds within the current loop unroll limit, but"
307-
+ " may be violated for larger collections.", subjectName.toLowerCase(Locale.US)));
306+
String.format(
307+
"Inconclusive: %s holds within the current loop unroll limit, but"
308+
+ " may be violated for larger collections.",
309+
subjectName.toLowerCase(Locale.US)));
308310
case NO_MATCH:
309311
return CelVerificationResult.verified();
310312
case SOLVER_UNKNOWN:

0 commit comments

Comments
 (0)