Skip to content

Commit b6ddfc0

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Fix overflow handlings for Uint, add more test cases around IntSort overflows
PiperOrigin-RevId: 952879660
1 parent 46e1933 commit b6ddfc0

5 files changed

Lines changed: 290 additions & 66 deletions

File tree

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

Lines changed: 41 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@
4040
import dev.cel.common.types.ListType;
4141
import dev.cel.common.types.MapType;
4242
import dev.cel.common.types.NullableType;
43+
import dev.cel.common.types.OptionalType;
4344
import dev.cel.common.types.SimpleType;
4445
import dev.cel.common.types.StructType;
4546
import dev.cel.common.types.StructTypeReference;
@@ -287,9 +288,13 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
287288
for (int i = 0; i < elements.size(); i++) {
288289
CelExpr element = elements.get(i);
289290
TranslatedValue elem = translateExpr(element, ast);
290-
elementsTv.add(elem);
291291

292292
if (optionalIndices.contains(i)) {
293+
Expr<?> checkedValue =
294+
typeSystem.withRuntimeError(
295+
elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr())));
296+
elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());
297+
293298
Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
294299
seq =
295300
(SeqExpr)
@@ -300,6 +305,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
300305
} else {
301306
seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
302307
}
308+
elementsTv.add(elem);
303309
}
304310
listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX);
305311
typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq));
@@ -327,15 +333,20 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
327333
elementsTv.add(keyTv);
328334
TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
329335
Expr<?> value = valueTv.z3Expr();
330-
elementsTv.add(valueTv);
331336

332337
Expr<?> finalValue = value;
333338
BoolExpr finalPresence = ctx.mkTrue();
334339
if (entryAst.optionalEntry()) {
335-
Expr<?> optRef = typeSystem.getOptionalRef(value);
340+
Expr<?> checkedValue =
341+
typeSystem.withRuntimeError(value, ctx.mkNot(typeSystem.isOptional(value)));
342+
valueTv =
343+
TranslatedValue.create(
344+
checkedValue, entryAst.value(), typeSystem, valueTv.isApproximate());
345+
Expr<?> optRef = typeSystem.getOptionalRef(checkedValue);
336346
finalPresence = typeSystem.optHasValue(optRef);
337347
finalValue = typeSystem.getOptionalValue(optRef);
338348
}
349+
elementsTv.add(valueTv);
339350

340351
BoolExpr keyAlreadyPresent = (BoolExpr) ctx.mkSelect(mapPresence, key);
341352
BoolExpr shouldInsertKey = ctx.mkAnd(ctx.mkNot(keyAlreadyPresent), finalPresence);
@@ -382,7 +393,6 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
382393
Expr<?> key = ctx.mkString(entryAst.fieldKey());
383394
TranslatedValue valueTv = translateExpr(entryAst.value(), ast);
384395
Expr<?> value = valueTv.z3Expr();
385-
elementsTv.add(valueTv);
386396

387397
CelType fieldType =
388398
typeProvider
@@ -397,10 +407,16 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
397407
Expr<?> finalValue = value;
398408
BoolExpr optionalHasValue = ctx.mkTrue();
399409
if (entryAst.optionalEntry()) {
400-
Expr<?> optRef = typeSystem.getOptionalRef(value);
410+
Expr<?> checkedValue =
411+
typeSystem.withRuntimeError(value, ctx.mkNot(typeSystem.isOptional(value)));
412+
valueTv =
413+
TranslatedValue.create(
414+
checkedValue, entryAst.value(), typeSystem, valueTv.isApproximate());
415+
Expr<?> optRef = typeSystem.getOptionalRef(checkedValue);
401416
optionalHasValue = typeSystem.optHasValue(optRef);
402417
finalValue = typeSystem.getOptionalValue(optRef);
403418
}
419+
elementsTv.add(valueTv);
404420

405421
// Canonicalization Trick:
406422
//
@@ -436,6 +452,9 @@ private Expr<?> getDefaultValueForType(CelType type) {
436452
if (type instanceof NullableType) {
437453
return typeSystem.mkNull();
438454
}
455+
if (type instanceof OptionalType) {
456+
return typeSystem.mkOptionalNone();
457+
}
439458
if (type.equals(SimpleType.INT)) {
440459
return typeSystem.mkInt(0);
441460
}
@@ -1147,6 +1166,23 @@ private BoolExpr createTypeConstraint(Expr<?> val, long exprId, CelAbstractSynta
11471166
}
11481167

11491168
private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
1169+
if (type instanceof NullableType) {
1170+
NullableType nullableType = (NullableType) type;
1171+
return ctx.mkOr(
1172+
typeSystem.isNull(val), createTypeConstraintForType(val, nullableType.targetType()));
1173+
}
1174+
if (type instanceof OptionalType) {
1175+
BoolExpr isOpt = typeSystem.isOptional(val);
1176+
CelType paramType = type.parameters().get(0);
1177+
if (paramType.kind().isDyn() || paramType.kind().isTypeParam()) {
1178+
return isOpt;
1179+
}
1180+
Expr<?> optRef = typeSystem.getOptionalRef(val);
1181+
BoolExpr hasValue = typeSystem.optHasValue(optRef);
1182+
BoolExpr valConstraint =
1183+
createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType);
1184+
return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint));
1185+
}
11501186
if (type.equals(SimpleType.BOOL)) {
11511187
return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val);
11521188
}

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

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -123,6 +123,23 @@ private static String formatExpr(
123123
return "Error";
124124
} else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) {
125125
return "Unknown";
126+
} else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) {
127+
Expr<?> optRef = expr.getArgs()[0];
128+
Expr<?> hasValueExpr =
129+
evaluateStrict(
130+
model,
131+
typeSystem.optHasValue(optRef),
132+
String.format("Z3 failed to evaluate optHasValue natively for %s", optRef));
133+
if (hasValueExpr.isTrue()) {
134+
Expr<?> valueExpr =
135+
evaluateStrict(
136+
model,
137+
typeSystem.getOptionalValue(optRef),
138+
String.format("Z3 failed to evaluate optValue natively for %s", optRef));
139+
return "optional(" + formatExpr(ctx, typeSystem, model, valueExpr) + ")";
140+
} else if (hasValueExpr.isFalse()) {
141+
return "optional.none()";
142+
}
126143
}
127144

128145
return expr.toString();

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

Lines changed: 13 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
import com.google.common.collect.Lists;
1818
import com.google.common.collect.ObjectArrays;
19+
import com.google.common.primitives.UnsignedLong;
1920
import com.google.errorprone.annotations.CanIgnoreReturnValue;
2021
import com.microsoft.z3.ArithExpr;
2122
import com.microsoft.z3.ArrayExpr;
@@ -256,6 +257,10 @@ Constructor bytesCons() {
256257
return bytesCons;
257258
}
258259

260+
Constructor optionalCons() {
261+
return optionalCons;
262+
}
263+
259264
/** Creates a CelValue containing a boolean. */
260265
public Expr<?> mkBool(boolean val) {
261266
return ctx.mkApp(boolCons.ConstructorDecl(), ctx.mkBool(val));
@@ -296,9 +301,14 @@ public Expr<?> mkInt(long val) {
296301
return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val));
297302
}
298303

304+
/** Creates a CelValue containing an unsigned integer from a string representation. */
305+
public Expr<?> mkUint(String val) {
306+
return ctx.mkApp(uintCons.ConstructorDecl(), ctx.mkInt(val));
307+
}
308+
299309
/** Creates a CelValue containing an unsigned integer. */
300310
public Expr<?> mkUint(long val) {
301-
return ctx.mkApp(uintCons.ConstructorDecl(), ctx.mkInt(val));
311+
return mkUint(UnsignedLong.fromLongBits(val).toString());
302312
}
303313

304314
/** Creates a CelValue containing a double. */
@@ -855,10 +865,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
855865
this.boolCons =
856866
ctx.mkConstructor(
857867
CONS_BOOL, IS_BOOL, new String[] {GET_BOOL}, new Sort[] {ctx.getBoolSort()}, null);
858-
// Note: Z3's IntSort models unbounded mathematical integers. We do not currently use
859-
// BitVecSort(64), which means CEL integer overflow semantics are not natively modeled,
860-
// and bitwise operations are unsupported. We enforce 64-bit value bounds explicitly
861-
// during variable constraint generation instead.
868+
// We use Z3's IntSort instead of BitVecSort(64) for faster arithmetic solving without
869+
// bit-blasting, explicitly enforcing 64-bit range bounds and overflow errors.
862870
this.intCons =
863871
ctx.mkConstructor(
864872
CONS_INT, IS_INT, new String[] {GET_INT}, new Sort[] {ctx.getIntSort()}, null);

‎verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,19 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.google.common.collect.ImmutableList;
18+
import com.microsoft.z3.BoolExpr;
19+
import com.microsoft.z3.Context;
1820
import com.microsoft.z3.Expr;
21+
import com.microsoft.z3.FPExpr;
22+
import com.microsoft.z3.SeqExpr;
1923
import dev.cel.common.CelFunctionDecl;
2024
import dev.cel.extensions.CelOptionalLibrary;
2125
import dev.cel.extensions.CelOptionalLibrary.Function;
26+
import dev.cel.verifier.CelZ3TypeSystem;
2227
import java.util.Optional;
2328

2429
/** Axiomatization for CEL's optional library functions. */
30+
@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
2531
final class OptionalAxioms {
2632

2733
static final ImmutableList<CelZ3FunctionAxiom> ALL_AXIOMS =
@@ -40,6 +46,17 @@ final class OptionalAxioms {
4046
sink.accept(ts.optHasValue(optRef));
4147
return Optional.of(ts.mkOptionalOf(optRef));
4248
}),
49+
createUnaryAxiom(
50+
Function.OPTIONAL_OF_NON_ZERO_VALUE,
51+
"optional_ofNonZeroValue",
52+
(ctx, ts, sink, value) -> {
53+
Expr<?> optRef = ctx.mkApp(ts.optionalOfRefFunc(), value);
54+
BoolExpr isZero = isZeroValue(ctx, ts, value);
55+
sink.accept(
56+
ctx.mkImplies(ctx.mkNot(isZero), ctx.mkEq(ts.getOptionalValue(optRef), value)));
57+
sink.accept(ctx.mkImplies(ctx.mkNot(isZero), ts.optHasValue(optRef)));
58+
return Optional.of(ctx.mkITE(isZero, ts.mkOptionalNone(), ts.mkOptionalOf(optRef)));
59+
}),
4360
createUnaryAxiom(
4461
Function.HAS_VALUE,
4562
"optional_hasValue",
@@ -69,6 +86,27 @@ final class OptionalAxioms {
6986
return Optional.of(ctx.mkITE(ts.optHasValue(optRef), val, other));
7087
}));
7188

89+
private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr<?> val) {
90+
return ctx.mkOr(
91+
ts.isNull(val),
92+
ctx.mkAnd(ts.isBool(val), ctx.mkEq(ts.unwrapBool(val), ctx.mkFalse())),
93+
ctx.mkAnd(ts.isInt(val), ctx.mkEq(ts.getInt(val), ctx.mkInt(0))),
94+
ctx.mkAnd(ts.isUint(val), ctx.mkEq(ts.getUint(val), ctx.mkInt(0))),
95+
ctx.mkAnd(ts.isDouble(val), ctx.mkFPIsZero((FPExpr) ts.getDouble(val))),
96+
ctx.mkAnd(ts.isString(val), ctx.mkEq(ts.getString(val), ctx.mkString(""))),
97+
ctx.mkAnd(
98+
ts.isBytes(val), ctx.mkEq(ctx.mkLength((SeqExpr) ts.getBytes(val)), ctx.mkInt(0))),
99+
ctx.mkAnd(
100+
ts.isList(val), ctx.mkEq(ctx.mkLength(ts.getSeq(ts.getListRef(val))), ctx.mkInt(0))),
101+
ctx.mkAnd(
102+
ts.isMap(val), ctx.mkEq(ctx.mkLength(ts.getMapKeys(ts.getMapRef(val))), ctx.mkInt(0))),
103+
ctx.mkAnd(
104+
ts.isMessage(val),
105+
ctx.mkEq(
106+
ts.getMsgPresence(ts.getMessageRef(val)),
107+
ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse()))));
108+
}
109+
72110
private static CelFunctionDecl getDecl(Function funcEnum) {
73111
return CelOptionalLibrary.INSTANCE.functions().stream()
74112
.filter(d -> d.name().equals(funcEnum.getFunction()))

0 commit comments

Comments
 (0)