Skip to content

Commit 9606982

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 54ecf52 commit 9606982

17 files changed

Lines changed: 441 additions & 123 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: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1228,7 +1228,7 @@ private BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSynta
12281228
.orElseThrow(
12291229
() -> new IllegalArgumentException("Type not found for expr ID: " + exprId));
12301230
BoolExpr typeConstraint = createTypeConstraintForType(val, type);
1231-
return ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val), typeConstraint);
1231+
return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint);
12321232
}
12331233

12341234
private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
@@ -1257,15 +1257,15 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
12571257
Expr<?> unwrapped = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], val);
12581258
return ctx.mkAnd(
12591259
ctx.mkApp(typeSystem.intCons().getTesterDecl(), val),
1260-
ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MIN_INT64)),
1261-
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)));
12621262
}
12631263
if (type.equals(SimpleType.UINT)) {
12641264
Expr<?> unwrapped = ctx.mkApp(typeSystem.uintCons().getAccessorDecls()[0], val);
12651265
return ctx.mkAnd(
12661266
ctx.mkApp(typeSystem.uintCons().getTesterDecl(), val),
12671267
ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(0)),
1268-
ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_UINT64)));
1268+
ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_UINT64)));
12691269
}
12701270
if (type.equals(SimpleType.DOUBLE)) {
12711271
return (BoolExpr) ctx.mkApp(typeSystem.doubleCons().getTesterDecl(), val);
@@ -1351,7 +1351,10 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
13511351
BoolExpr validEntry = ctx.mkAnd(validIndex, presence);
13521352

13531353
Expr mapVal = ctx.mkSelect(mapValues, key);
1354-
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));
13551358
boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
13561359
boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
13571360
}
@@ -1409,6 +1412,12 @@ private Optional<Object> toCacheKey(CelExpr expr) {
14091412
case CONSTANT:
14101413
return Optional.of(expr.constant());
14111414
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+
}
14121421
ImmutableList.Builder<Object> builder = ImmutableList.builder();
14131422
for (CelExpr elem : expr.list().elements()) {
14141423
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/CelZ3CounterexampleGenerator.java‎

Lines changed: 28 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -24,14 +24,17 @@
2424
import com.microsoft.z3.Model;
2525
import com.microsoft.z3.RatNum;
2626
import java.util.ArrayList;
27+
import java.util.HashSet;
28+
import java.util.LinkedHashSet;
2729
import java.util.List;
30+
import java.util.Set;
2831
import org.jspecify.annotations.Nullable;
2932

3033
/** Generates human-readable counterexample strings from Z3 models. */
3134
@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
3235
final class CelZ3CounterexampleGenerator {
3336

34-
private static final int MAX_LIST_ELEMENTS_TO_PRINT = 15;
37+
private static final int MAX_ELEMENTS_TO_PRINT = 15;
3538

3639
private CelZ3CounterexampleGenerator() {}
3740

@@ -158,8 +161,10 @@ private static String reconstructList(
158161
model,
159162
ctx.mkLength(typeSystem.getSeq(listRef)),
160163
String.format("Z3 failed to evaluate length for list %s", listRef));
161-
int length = ((IntNum) lenExpr).getInt();
162-
int printLimit = Math.min(length, MAX_LIST_ELEMENTS_TO_PRINT);
164+
Preconditions.checkState(
165+
lenExpr instanceof IntNum, "Expected IntNum length for list %s, got %s", listRef, lenExpr);
166+
long length = ((IntNum) lenExpr).getInt64();
167+
int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT);
163168
List<String> elements = new ArrayList<>();
164169
for (int i = 0; i < printLimit; i++) {
165170
Expr<?> elem =
@@ -179,36 +184,33 @@ private static String reconstructList(
179184

180185
private static String reconstructMap(
181186
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
182-
List<Expr<?>> keys = new ArrayList<>();
183187
Expr<?> lenExpr =
184188
evaluateStrict(
185189
model,
186190
ctx.mkLength(typeSystem.getMapKeys(mapRef)),
187191
String.format("Z3 failed to evaluate length for map %s", mapRef));
188-
if (lenExpr instanceof IntNum) {
189-
int length = ((IntNum) lenExpr).getInt();
190-
int printLimit = Math.min(length, 100);
191-
for (int i = 0; i < printLimit; i++) {
192-
Expr<?> elem =
193-
evaluateStrict(
194-
model,
195-
ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)),
196-
String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef));
197-
if (!keys.contains(elem)) {
198-
keys.add(elem);
199-
}
200-
}
201-
}
192+
Preconditions.checkState(
193+
lenExpr instanceof IntNum, "Expected IntNum length for map %s, got %s", mapRef, lenExpr);
202194

195+
long length = ((IntNum) lenExpr).getInt64();
196+
int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT);
203197
List<String> entries = new ArrayList<>();
204-
for (Expr<?> key : keys) {
198+
Set<Expr<?>> seenKeys = new HashSet<>();
199+
for (int i = 0; i < printLimit; i++) {
200+
Expr<?> key =
201+
evaluateStrict(
202+
model,
203+
ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)),
204+
String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef));
205+
if (!seenKeys.add(key)) {
206+
continue;
207+
}
205208
Expr<?> presence =
206209
evaluateStrict(
207210
model,
208211
ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key),
209212
String.format(
210213
"Z3 failed to evaluate map presence for key %s in map %s", key, mapRef));
211-
212214
if (presence.isTrue()) {
213215
Expr<?> value =
214216
evaluateStrict(
@@ -221,6 +223,9 @@ private static String reconstructMap(
221223
+ formatExpr(ctx, typeSystem, model, value));
222224
}
223225
}
226+
if (length > printLimit) {
227+
entries.add("... (" + (length - printLimit) + " more entries)");
228+
}
224229

225230
return "{" + String.join(", ", entries) + "}";
226231
}
@@ -241,7 +246,7 @@ private static String reconstructMessage(
241246

242247
String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");
243248

244-
List<Expr<?>> keys = new ArrayList<>();
249+
Set<Expr<?>> keys = new LinkedHashSet<>();
245250
extractKeys(presenceArray, keys);
246251

247252
List<String> entries = new ArrayList<>();
@@ -268,7 +273,7 @@ private static String reconstructMessage(
268273
return typeName + "{" + String.join(", ", entries) + "}";
269274
}
270275

271-
private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
276+
private static void extractKeys(Expr<?> arrayExpr, Set<Expr<?>> keys) {
272277
int iterations = 0;
273278
while (true) {
274279
if (++iterations > 100_000) {
@@ -284,9 +289,7 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
284289
Expr<?>[] args = arrayExpr.getArgs();
285290
Preconditions.checkState(
286291
args.length == 3, "Z3 store array operation must have exactly 3 arguments");
287-
if (!keys.contains(args[1])) {
288-
keys.add(args[1]);
289-
}
292+
keys.add(args[1]);
290293
arrayExpr = args[0];
291294
continue;
292295
}

0 commit comments

Comments
 (0)