Skip to content

Commit db77be5

Browse files
TristonianJonescopybara-github
TristonianJones
authored and
copybara-github
committed
No public description
PiperOrigin-RevId: 1001131884
1 parent c29d49d commit db77be5

15 files changed

Lines changed: 585 additions & 51 deletions

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -178,6 +178,8 @@ java_library(
178178
"//common:operator",
179179
"//common/ast",
180180
"//common/ast:cel_block",
181+
"//common/internal:cel_descriptor_pools",
182+
"//common/internal:well_known_proto",
181183
"//common/types",
182184
"//common/types:cel_types",
183185
"//common/types:type_providers",
@@ -187,6 +189,7 @@ java_library(
187189
"//verifier/axioms",
188190
"@maven//:com_google_errorprone_error_prone_annotations",
189191
"@maven//:com_google_guava_guava",
192+
"@maven//:com_google_protobuf_protobuf_java",
190193
"@maven//:org_jspecify_jspecify",
191194
"@maven//:tools_aqua_z3_turnkey",
192195
],

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

Lines changed: 143 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@
2222
import com.microsoft.z3.BoolExpr;
2323
import com.microsoft.z3.Context;
2424
import com.microsoft.z3.Expr;
25+
import com.microsoft.z3.FPExpr;
2526
import com.microsoft.z3.FuncDecl;
2627
import com.microsoft.z3.IntExpr;
2728
import com.microsoft.z3.Quantifier;
@@ -82,6 +83,9 @@ final class CelAstToZ3Translator {
8283
private static final String EMPTY_LIST_PREFIX = "!empty_list";
8384
private static final String EMPTY_MAP_PREFIX = "!empty_map";
8485
private static final String NULL_VALUE_FIELD = "null_value";
86+
private static final String SECONDS_FIELD = "seconds";
87+
private static final long MAX_UINT32 = 0xFFFFFFFFL;
88+
private static final int MIN_DURATION_NANOS = -999_999_999;
8589
private final Context ctx;
8690
private final CelZ3TypeSystem typeSystem;
8791
private final CelZ3OperatorTranslator operatorTranslator;
@@ -401,6 +405,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
401405
if (isJsonWkt(createStruct.messageName())) {
402406
return translateJsonWktStruct(celExpr, createStruct, ast);
403407
}
408+
if (CelTypes.isWrapperType(createStruct.messageName())) {
409+
return translateWrapperWktStruct(celExpr, createStruct, ast);
410+
}
411+
if (isTimeWkt(createStruct.messageName())) {
412+
return translateTimeWktStruct(celExpr, createStruct, ast);
413+
}
404414

405415
// Bypass SMT when the struct is empty (return the cached SMT default pointer)
406416
if (createStruct.entries().isEmpty()) {
@@ -517,7 +527,12 @@ private TranslatedValue translateJsonWktStruct(
517527
&& entry.fieldKey().equals(NULL_VALUE_FIELD);
518528

519529
if (entry.optionalEntry()) {
520-
Expr<?> optRef = typeSystem.getOptionalRef(finalVal);
530+
Expr<?> checkedVal =
531+
typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal)));
532+
entryTv =
533+
TranslatedValue.create(
534+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
535+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
521536
BoolExpr hasValue = typeSystem.optHasValue(optRef);
522537

523538
Expr<?> unpackedVal = typeSystem.getOptionalValue(optRef);
@@ -533,6 +548,129 @@ private TranslatedValue translateJsonWktStruct(
533548
ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
534549
}
535550

551+
private TranslatedValue translateWrapperWktStruct(
552+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
553+
String typeName = createStruct.messageName();
554+
CelType wrapperType =
555+
CelTypes.getWellKnownCelType(typeName)
556+
.orElseThrow(
557+
() -> new IllegalArgumentException("Unexpected wrapper type: " + typeName));
558+
CelType targetType = ((NullableType) wrapperType).targetType();
559+
Expr<?> currentVal = getDefaultValueForType(targetType);
560+
561+
List<TranslatedValue> entryTvs = new ArrayList<>();
562+
for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
563+
TranslatedValue entryTv = translateExpr(entry.value(), ast);
564+
Expr<?> val = entryTv.z3Expr();
565+
if (entry.optionalEntry()) {
566+
Expr<?> checkedVal =
567+
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
568+
entryTv =
569+
TranslatedValue.create(
570+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
571+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
572+
BoolExpr hasValue = typeSystem.optHasValue(optRef);
573+
currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal);
574+
} else {
575+
currentVal = val;
576+
}
577+
entryTvs.add(entryTv);
578+
}
579+
BoolExpr validValue = createTypeConstraintForType(currentVal, targetType);
580+
if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) {
581+
IntExpr intVal = typeSystem.getInt(currentVal);
582+
validValue =
583+
ctx.mkAnd(
584+
validValue,
585+
ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)),
586+
ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE)));
587+
} else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) {
588+
IntExpr uintVal = typeSystem.getUint(currentVal);
589+
validValue =
590+
ctx.mkAnd(
591+
validValue,
592+
ctx.mkGe(uintVal, ctx.mkInt(0)),
593+
ctx.mkLe(uintVal, ctx.mkInt(MAX_UINT32)));
594+
} else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) {
595+
FPExpr doubleVal = typeSystem.getDouble(currentVal);
596+
FPExpr narrowedFloat =
597+
ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), doubleVal, ctx.mkFPSortSingle());
598+
FPExpr widenedDouble =
599+
ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), narrowedFloat, ctx.mkFPSortDouble());
600+
currentVal = typeSystem.wrapDouble(widenedDouble);
601+
}
602+
currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue));
603+
return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
604+
}
605+
606+
private static boolean isTimeWkt(String messageName) {
607+
return messageName.equals(CelTypes.TIMESTAMP_MESSAGE)
608+
|| messageName.equals(CelTypes.DURATION_MESSAGE);
609+
}
610+
611+
private TranslatedValue translateTimeWktStruct(
612+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
613+
boolean isTimestamp = createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE);
614+
Expr<?> secondsVal = typeSystem.mkInt(0);
615+
Expr<?> nanosVal = typeSystem.mkInt(0);
616+
List<TranslatedValue> entryTvs = new ArrayList<>();
617+
618+
for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
619+
TranslatedValue entryTv = translateExpr(entry.value(), ast);
620+
Expr<?> val = entryTv.z3Expr();
621+
Expr<?> unpackedVal = val;
622+
BoolExpr hasValue = ctx.mkTrue();
623+
if (entry.optionalEntry()) {
624+
Expr<?> checkedVal =
625+
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
626+
entryTv =
627+
TranslatedValue.create(
628+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
629+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
630+
hasValue = typeSystem.optHasValue(optRef);
631+
unpackedVal = typeSystem.getOptionalValue(optRef);
632+
}
633+
if (entry.fieldKey().equals(SECONDS_FIELD)) {
634+
secondsVal = ctx.mkITE(hasValue, unpackedVal, secondsVal);
635+
} else {
636+
nanosVal = ctx.mkITE(hasValue, unpackedVal, nanosVal);
637+
}
638+
entryTvs.add(entryTv);
639+
}
640+
641+
IntExpr seconds = typeSystem.getInt(secondsVal);
642+
IntExpr nanos = typeSystem.getInt(nanosVal);
643+
IntExpr totalNanos =
644+
(IntExpr)
645+
ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos);
646+
647+
BoolExpr typeError =
648+
ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal)));
649+
BoolExpr rangeError;
650+
if (isTimestamp) {
651+
BoolExpr nanosOutOfRange =
652+
ctx.mkOr(
653+
ctx.mkLt(nanos, ctx.mkInt(0)),
654+
ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
655+
rangeError = ctx.mkOr(nanosOutOfRange, typeSystem.checkTimestampOverflow(totalNanos));
656+
} else {
657+
BoolExpr nanosOutOfRange =
658+
ctx.mkOr(
659+
ctx.mkLt(nanos, ctx.mkInt(MIN_DURATION_NANOS)),
660+
ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
661+
BoolExpr signMismatch =
662+
ctx.mkOr(
663+
ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
664+
ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
665+
rangeError =
666+
ctx.mkOr(nanosOutOfRange, signMismatch, typeSystem.checkDurationOverflow(totalNanos));
667+
}
668+
Expr<?> wrapped =
669+
isTimestamp ? typeSystem.wrapTimestamp(totalNanos) : typeSystem.wrapDuration(totalNanos);
670+
Expr<?> result = typeSystem.withRuntimeError(wrapped, typeError, rangeError);
671+
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
672+
}
673+
536674
private Expr<?> getDefaultValueForType(CelType type) {
537675
if (type instanceof NullableType) {
538676
return typeSystem.mkNull();
@@ -1326,14 +1464,14 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
13261464
return typeSystem.isBytes(val);
13271465
}
13281466
if (type.equals(SimpleType.TIMESTAMP)) {
1329-
IntExpr seconds = typeSystem.getTimestamp(val);
1467+
IntExpr nanos = typeSystem.getTimestamp(val);
13301468
return ctx.mkAnd(
1331-
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
1469+
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
13321470
}
13331471
if (type.equals(SimpleType.DURATION)) {
1334-
IntExpr seconds = typeSystem.getDuration(val);
1472+
IntExpr nanos = typeSystem.getDuration(val);
13351473
return ctx.mkAnd(
1336-
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
1474+
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
13371475
}
13381476

13391477
if (type instanceof ListType) {

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

Lines changed: 27 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,13 +16,15 @@
1616

1717
import static com.google.common.base.Preconditions.checkArgument;
1818
import static com.google.common.base.Preconditions.checkNotNull;
19+
import static com.google.common.collect.ImmutableList.toImmutableList;
1920

2021
import com.google.common.annotations.VisibleForTesting;
2122
import com.google.common.collect.ImmutableList;
2223
import com.google.common.collect.ImmutableMap;
2324
import com.google.common.collect.ImmutableSet;
2425
import com.google.errorprone.annotations.CanIgnoreReturnValue;
2526
import com.google.errorprone.annotations.Immutable;
27+
import com.google.protobuf.Descriptors.Descriptor;
2628
import com.microsoft.z3.BoolExpr;
2729
import com.microsoft.z3.Context;
2830
import com.microsoft.z3.Model;
@@ -32,6 +34,8 @@
3234
import dev.cel.bundle.Cel;
3335
import dev.cel.bundle.CelFactory;
3436
import dev.cel.common.CelAbstractSyntaxTree;
37+
import dev.cel.common.internal.DefaultDescriptorPool;
38+
import dev.cel.common.internal.WellKnownProto;
3539
import dev.cel.common.types.CelType;
3640
import dev.cel.common.types.CelTypeProvider;
3741
import dev.cel.optimizer.CelOptimizationException;
@@ -64,6 +68,26 @@ public Optional<CelType> findType(String typeName) {
6468
}
6569
};
6670

71+
private static final ImmutableList<Descriptor> WELL_KNOWN_DESCRIPTORS =
72+
ImmutableList.of(
73+
WellKnownProto.DURATION,
74+
WellKnownProto.JSON_LIST_VALUE,
75+
WellKnownProto.JSON_STRUCT_VALUE,
76+
WellKnownProto.JSON_VALUE,
77+
WellKnownProto.TIMESTAMP,
78+
WellKnownProto.FLOAT_VALUE,
79+
WellKnownProto.INT32_VALUE,
80+
WellKnownProto.INT64_VALUE,
81+
WellKnownProto.STRING_VALUE,
82+
WellKnownProto.BOOL_VALUE,
83+
WellKnownProto.BYTES_VALUE,
84+
WellKnownProto.DOUBLE_VALUE,
85+
WellKnownProto.UINT32_VALUE,
86+
WellKnownProto.UINT64_VALUE)
87+
.stream()
88+
.map(DefaultDescriptorPool::getWellKnownProtoDescriptor)
89+
.collect(toImmutableList());
90+
6791
private final Duration timeout;
6892
private final int comprehensionUnrollLimit;
6993
private final ImmutableSet<String> unknownIdentifiers;
@@ -74,7 +98,8 @@ public Optional<CelType> findType(String typeName) {
7498
private final Cel cel;
7599

76100
static Builder newBuilder() {
77-
return new Builder(CelFactory.plannerCelBuilder().build());
101+
return new Builder(
102+
CelFactory.plannerCelBuilder().addMessageTypes(WELL_KNOWN_DESCRIPTORS).build());
78103
}
79104

80105
static Builder newBuilder(Cel cel) {
@@ -155,7 +180,7 @@ private Builder(Cel cel) {
155180
this.comprehensionUnrollLimit = 5;
156181
this.unknownIdentifiers = ImmutableSet.builder();
157182
this.functionAxioms = ImmutableList.builder();
158-
this.typeProvider = EMPTY_TYPE_PROVIDER;
183+
this.typeProvider = cel.getTypeProvider();
159184
this.cel = cel;
160185
}
161186
}

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

Lines changed: 29 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@
2323
import com.microsoft.z3.IntNum;
2424
import com.microsoft.z3.Model;
2525
import com.microsoft.z3.RatNum;
26+
import java.math.BigInteger;
2627
import java.util.ArrayList;
2728
import java.util.HashSet;
2829
import java.util.LinkedHashSet;
@@ -86,9 +87,9 @@ private static String formatExpr(
8687
if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
8788
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
8889
} else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
89-
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
90+
return formatTimestamp(expr.getArgs()[0]);
9091
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
91-
return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
92+
return formatDuration(expr.getArgs()[0]);
9293
} else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
9394
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
9495
} else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {
@@ -154,6 +155,32 @@ private static String formatExpr(
154155
return expr.toString();
155156
}
156157

158+
private static String formatTimestamp(Expr<?> nanosExpr) {
159+
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
160+
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
161+
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
162+
BigInteger seconds = divRem[0];
163+
BigInteger nanos = divRem[1];
164+
if (nanos.signum() < 0) {
165+
seconds = seconds.subtract(BigInteger.ONE);
166+
nanos = nanos.add(nanosPerSecond);
167+
}
168+
if (nanos.equals(BigInteger.ZERO)) {
169+
return "timestamp(" + seconds + ")";
170+
}
171+
return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}";
172+
}
173+
174+
private static String formatDuration(Expr<?> nanosExpr) {
175+
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
176+
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
177+
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
178+
if (divRem[1].equals(BigInteger.ZERO)) {
179+
return "duration('" + divRem[0] + "s')";
180+
}
181+
return "duration('" + totalNanos + "ns')";
182+
}
183+
157184
private static String reconstructList(
158185
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef) {
159186
Expr<?> lenExpr =

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

Lines changed: 28 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@
3535
import com.microsoft.z3.SeqSort;
3636
import com.microsoft.z3.Sort;
3737
import dev.cel.common.internal.ProtoTimeUtils;
38+
import java.math.BigInteger;
3839
import java.util.ArrayList;
3940
import java.util.Arrays;
4041
import java.util.HashMap;
@@ -56,6 +57,22 @@
5657
@SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types.
5758
public final class CelZ3TypeSystem {
5859

60+
/** Number of nanoseconds per second. */
61+
public static final long NANOS_PER_SECOND = 1_000_000_000L;
62+
63+
private static final long MAX_TIMESTAMP_NANOS_PART = 999_999_999L;
64+
65+
private static final String MIN_TIMESTAMP_NANOS =
66+
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)
67+
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
68+
.toString();
69+
70+
private static final String MAX_TIMESTAMP_NANOS =
71+
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)
72+
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
73+
.add(BigInteger.valueOf(MAX_TIMESTAMP_NANOS_PART))
74+
.toString();
75+
5976
private static final String TYPE_CEL_VALUE = "CelValue";
6077
private static final String CONS_BOOL = "Bool";
6178
private static final String IS_BOOL = "isBool";
@@ -777,18 +794,22 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
777794
ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64)));
778795
}
779796

780-
/** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
797+
/**
798+
* Checks if the given nanosecond arithmetic expression overflows CEL Timestamp bounds
799+
* ({@code [0001-01-01T00:00:00Z, 9999-12-31T23:59:59.999999999Z]}).
800+
*/
781801
public BoolExpr checkTimestampOverflow(ArithExpr result) {
782802
return ctx.mkOr(
783-
ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)),
784-
ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)));
803+
ctx.mkGt(result, ctx.mkInt(MAX_TIMESTAMP_NANOS)),
804+
ctx.mkLt(result, ctx.mkInt(MIN_TIMESTAMP_NANOS)));
785805
}
786806

787-
/** Checks if the given arithmetic expression overflows CEL Duration bounds. */
807+
/**
808+
* Checks if the given nanosecond arithmetic expression overflows CEL Duration bounds, which are
809+
* confined to a signed 64-bit integer of nanoseconds (matching Go's {@code time.Duration}).
810+
*/
788811
public BoolExpr checkDurationOverflow(ArithExpr result) {
789-
return ctx.mkOr(
790-
ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MAX)),
791-
ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MIN)));
812+
return checkIntOverflow(result);
792813
}
793814

794815
/** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */

0 commit comments

Comments
 (0)