Skip to content

Commit 3faeb8d

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

11 files changed

Lines changed: 424 additions & 34 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: 156 additions & 1 deletion
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,11 @@ 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 String SUBSECOND_FUNC_SUFFIX = "_subsecond";
88+
private static final long MAX_UINT32 = 0xFFFFFFFFL;
89+
private static final int NANOS_PER_SECOND = 1_000_000_000;
90+
private static final int MIN_DURATION_NANOS = -999_999_999;
8591
private final Context ctx;
8692
private final CelZ3TypeSystem typeSystem;
8793
private final CelZ3OperatorTranslator operatorTranslator;
@@ -401,6 +407,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
401407
if (isJsonWkt(createStruct.messageName())) {
402408
return translateJsonWktStruct(celExpr, createStruct, ast);
403409
}
410+
if (CelTypes.isWrapperType(createStruct.messageName())) {
411+
return translateWrapperWktStruct(celExpr, createStruct, ast);
412+
}
413+
if (isTimeWkt(createStruct.messageName())) {
414+
return translateTimeWktStruct(celExpr, createStruct, ast);
415+
}
404416

405417
// Bypass SMT when the struct is empty (return the cached SMT default pointer)
406418
if (createStruct.entries().isEmpty()) {
@@ -517,7 +529,12 @@ private TranslatedValue translateJsonWktStruct(
517529
&& entry.fieldKey().equals(NULL_VALUE_FIELD);
518530

519531
if (entry.optionalEntry()) {
520-
Expr<?> optRef = typeSystem.getOptionalRef(finalVal);
532+
Expr<?> checkedVal =
533+
typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal)));
534+
entryTv =
535+
TranslatedValue.create(
536+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
537+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
521538
BoolExpr hasValue = typeSystem.optHasValue(optRef);
522539

523540
Expr<?> unpackedVal = typeSystem.getOptionalValue(optRef);
@@ -533,6 +550,144 @@ private TranslatedValue translateJsonWktStruct(
533550
ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv));
534551
}
535552

553+
private TranslatedValue translateWrapperWktStruct(
554+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
555+
String typeName = createStruct.messageName();
556+
CelType wrapperType =
557+
CelTypes.getWellKnownCelType(typeName)
558+
.orElseThrow(
559+
() -> new IllegalArgumentException("Unexpected wrapper type: " + typeName));
560+
CelType targetType = ((NullableType) wrapperType).targetType();
561+
Expr<?> currentVal = getDefaultValueForType(targetType);
562+
563+
List<TranslatedValue> entryTvs = new ArrayList<>();
564+
for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
565+
TranslatedValue entryTv = translateExpr(entry.value(), ast);
566+
Expr<?> val = entryTv.z3Expr();
567+
if (entry.optionalEntry()) {
568+
Expr<?> checkedVal =
569+
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
570+
entryTv =
571+
TranslatedValue.create(
572+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
573+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
574+
BoolExpr hasValue = typeSystem.optHasValue(optRef);
575+
currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal);
576+
} else {
577+
currentVal = val;
578+
}
579+
entryTvs.add(entryTv);
580+
}
581+
BoolExpr validValue = createTypeConstraintForType(currentVal, targetType);
582+
if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) {
583+
IntExpr intVal = typeSystem.getInt(currentVal);
584+
validValue =
585+
ctx.mkAnd(
586+
validValue,
587+
ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)),
588+
ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE)));
589+
} else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) {
590+
IntExpr uintVal = typeSystem.getUint(currentVal);
591+
validValue =
592+
ctx.mkAnd(
593+
validValue,
594+
ctx.mkGe(uintVal, ctx.mkInt(0)),
595+
ctx.mkLe(uintVal, ctx.mkInt(MAX_UINT32)));
596+
} else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) {
597+
FPExpr floatVal = typeSystem.getDouble(currentVal);
598+
validValue =
599+
ctx.mkAnd(
600+
validValue,
601+
ctx.mkFPGEq(floatVal, typeSystem.mkFpDouble(-Float.MAX_VALUE)),
602+
ctx.mkFPLEq(floatVal, typeSystem.mkFpDouble(Float.MAX_VALUE)));
603+
}
604+
currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue));
605+
return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
606+
}
607+
608+
private static boolean isTimeWkt(String messageName) {
609+
return messageName.equals(CelTypes.TIMESTAMP_MESSAGE)
610+
|| messageName.equals(CelTypes.DURATION_MESSAGE);
611+
}
612+
613+
private TranslatedValue translateTimeWktStruct(
614+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
615+
boolean isTimestamp = createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE);
616+
Expr<?> secondsVal = typeSystem.mkInt(0);
617+
Expr<?> nanosVal = typeSystem.mkInt(0);
618+
List<TranslatedValue> entryTvs = new ArrayList<>();
619+
620+
for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
621+
TranslatedValue entryTv = translateExpr(entry.value(), ast);
622+
Expr<?> val = entryTv.z3Expr();
623+
Expr<?> unpackedVal = val;
624+
BoolExpr hasValue = ctx.mkTrue();
625+
if (entry.optionalEntry()) {
626+
Expr<?> checkedVal =
627+
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
628+
entryTv =
629+
TranslatedValue.create(
630+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
631+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
632+
hasValue = typeSystem.optHasValue(optRef);
633+
unpackedVal = typeSystem.getOptionalValue(optRef);
634+
}
635+
if (entry.fieldKey().equals(SECONDS_FIELD)) {
636+
secondsVal = ctx.mkITE(hasValue, unpackedVal, secondsVal);
637+
} else {
638+
nanosVal = ctx.mkITE(hasValue, unpackedVal, nanosVal);
639+
}
640+
entryTvs.add(entryTv);
641+
}
642+
643+
IntExpr seconds = typeSystem.getInt(secondsVal);
644+
BoolExpr secondsError =
645+
ctx.mkOr(
646+
ctx.mkNot(typeSystem.isInt(secondsVal)),
647+
isTimestamp
648+
? typeSystem.checkTimestampOverflow(seconds)
649+
: typeSystem.checkDurationOverflow(seconds));
650+
651+
IntExpr nanos = typeSystem.getInt(nanosVal);
652+
BoolExpr nanosError;
653+
if (isTimestamp) {
654+
nanosError =
655+
ctx.mkOr(
656+
ctx.mkNot(typeSystem.isInt(nanosVal)),
657+
ctx.mkLt(nanos, ctx.mkInt(0)),
658+
ctx.mkGe(nanos, ctx.mkInt(NANOS_PER_SECOND)));
659+
} else {
660+
BoolExpr nanosOutOfRange =
661+
ctx.mkOr(
662+
ctx.mkLt(nanos, ctx.mkInt(MIN_DURATION_NANOS)),
663+
ctx.mkGe(nanos, ctx.mkInt(NANOS_PER_SECOND)));
664+
BoolExpr signMismatch =
665+
ctx.mkOr(
666+
ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
667+
ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
668+
nanosError = ctx.mkOr(ctx.mkNot(typeSystem.isInt(nanosVal)), nanosOutOfRange, signMismatch);
669+
}
670+
BoolExpr nanosNonZero = ctx.mkNot(ctx.mkEq(nanos, ctx.mkInt(0)));
671+
BoolExpr subSecondApprox = ctx.mkAnd(ctx.mkNot(nanosError), nanosNonZero);
672+
FuncDecl<?> subSecondOffset =
673+
typeSystem.internFuncDecl(
674+
createStruct.messageName() + SUBSECOND_FUNC_SUFFIX,
675+
new Sort[] {ctx.getIntSort(), ctx.getIntSort()},
676+
ctx.getIntSort());
677+
IntExpr subSecondTime = (IntExpr) ctx.mkApp(subSecondOffset, seconds, nanos);
678+
IntExpr encodedTime = (IntExpr) ctx.mkITE(subSecondApprox, subSecondTime, seconds);
679+
Expr<?> wrapped =
680+
isTimestamp ? typeSystem.wrapTimestamp(encodedTime) : typeSystem.wrapDuration(encodedTime);
681+
Expr<?> result = typeSystem.withRuntimeError(wrapped, secondsError, nanosError);
682+
TranslatedValue strictResult =
683+
TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
684+
return TranslatedValue.create(
685+
strictResult.z3Expr(),
686+
celExpr,
687+
typeSystem,
688+
CelZ3TypeSystem.mkOrFlattened(ctx, strictResult.isApproximate(), subSecondApprox));
689+
}
690+
536691
private Expr<?> getDefaultValueForType(CelType type) {
537692
if (type instanceof NullableType) {
538693
return typeSystem.mkNull();

‎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/tools/BUILD.bazel‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,10 +45,11 @@ java_library(
4545
"//common:cel_ast",
4646
"//common:compiler_common",
4747
"//common:options",
48+
"//common/internal:cel_descriptor_pools",
49+
"//common/internal:well_known_proto",
4850
"//common/types",
4951
"//common/types:cel_types",
5052
"//common/types:type_providers",
51-
"//compiler",
5253
"//compiler:compiler_builder",
5354
"//extensions",
5455
"//parser:macro",
@@ -64,6 +65,7 @@ java_library(
6465
"//verifier:verifier_factory",
6566
"@maven//:com_google_errorprone_error_prone_annotations",
6667
"@maven//:com_google_guava_guava",
68+
"@maven//:com_google_protobuf_protobuf_java",
6769
"@maven//:info_picocli_picocli",
6870
],
6971
)

‎verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -315,7 +315,7 @@ private static void printHelp(String topic, PrintStream out) {
315315
out.println();
316316
out.println("Supported Types:");
317317
out.println(" - Primitive types: int, uint, string, bool, double, bytes, dyn");
318-
out.println(" - Well-known types: timestamp, duration");
318+
out.println(" - Well-known types: timestamp, duration, google.protobuf.*");
319319
out.println(" - List types: list<T> (e.g., list<int>, list<string>)");
320320
out.println(" - Map types: map<K,V> (e.g., map<string,int>, map<string,string>)");
321321
out.println(" - Optional types: optional<T> (e.g., optional<string>, optional<int>)");

0 commit comments

Comments
 (0)