Skip to content

No public description #1369

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
copybara-service wants to merge 1 commit into
base: main
Choose a base branch
from
+585 −51
Open

No public description #1369

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -178,6 +178,8 @@ java_library(
"//common:operator",
"//common/ast",
"//common/ast:cel_block",
"//common/internal:cel_descriptor_pools",
"//common/internal:well_known_proto",
"//common/types",
"//common/types:cel_types",
"//common/types:type_providers",
Expand All @@ -187,6 +189,7 @@ java_library(
"//verifier/axioms",
"@maven//:com_google_errorprone_error_prone_annotations",
"@maven//:com_google_guava_guava",
"@maven//:com_google_protobuf_protobuf_java",
"@maven//:org_jspecify_jspecify",
"@maven//:tools_aqua_z3_turnkey",
],
Expand Down
148 changes: 143 additions & 5 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.FPExpr;
import com.microsoft.z3.FuncDecl;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.Quantifier;
Expand Down Expand Up @@ -82,6 +83,9 @@ final class CelAstToZ3Translator {
private static final String EMPTY_LIST_PREFIX = "!empty_list";
private static final String EMPTY_MAP_PREFIX = "!empty_map";
private static final String NULL_VALUE_FIELD = "null_value";
private static final String SECONDS_FIELD = "seconds";
private static final long MAX_UINT32 = 0xFFFFFFFFL;
private static final int MIN_DURATION_NANOS = -999_999_999;
private final Context ctx;
private final CelZ3TypeSystem typeSystem;
private final CelZ3OperatorTranslator operatorTranslator;
Expand Down Expand Up @@ -401,6 +405,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
if (isJsonWkt(createStruct.messageName())) {
return translateJsonWktStruct(celExpr, createStruct, ast);
}
if (CelTypes.isWrapperType(createStruct.messageName())) {
return translateWrapperWktStruct(celExpr, createStruct, ast);
}
if (isTimeWkt(createStruct.messageName())) {
return translateTimeWktStruct(celExpr, createStruct, ast);
}

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

if (entry.optionalEntry()) {
Expr<?> optRef = typeSystem.getOptionalRef(finalVal);
Expr<?> checkedVal =
typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal)));
entryTv =
TranslatedValue.create(
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
BoolExpr hasValue = typeSystem.optHasValue(optRef);

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

private TranslatedValue translateWrapperWktStruct(
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
String typeName = createStruct.messageName();
CelType wrapperType =
CelTypes.getWellKnownCelType(typeName)
.orElseThrow(
() -> new IllegalArgumentException("Unexpected wrapper type: " + typeName));
CelType targetType = ((NullableType) wrapperType).targetType();
Expr<?> currentVal = getDefaultValueForType(targetType);

List<TranslatedValue> entryTvs = new ArrayList<>();
for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
TranslatedValue entryTv = translateExpr(entry.value(), ast);
Expr<?> val = entryTv.z3Expr();
if (entry.optionalEntry()) {
Expr<?> checkedVal =
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
entryTv =
TranslatedValue.create(
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
BoolExpr hasValue = typeSystem.optHasValue(optRef);
currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal);
} else {
currentVal = val;
}
entryTvs.add(entryTv);
}
BoolExpr validValue = createTypeConstraintForType(currentVal, targetType);
if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) {
IntExpr intVal = typeSystem.getInt(currentVal);
validValue =
ctx.mkAnd(
validValue,
ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)),
ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE)));
} else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) {
IntExpr uintVal = typeSystem.getUint(currentVal);
validValue =
ctx.mkAnd(
validValue,
ctx.mkGe(uintVal, ctx.mkInt(0)),
ctx.mkLe(uintVal, ctx.mkInt(MAX_UINT32)));
} else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) {
FPExpr doubleVal = typeSystem.getDouble(currentVal);
FPExpr narrowedFloat =
ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), doubleVal, ctx.mkFPSortSingle());
FPExpr widenedDouble =
ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), narrowedFloat, ctx.mkFPSortDouble());
currentVal = typeSystem.wrapDouble(widenedDouble);
}
currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue));
return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
}

private static boolean isTimeWkt(String messageName) {
return messageName.equals(CelTypes.TIMESTAMP_MESSAGE)
|| messageName.equals(CelTypes.DURATION_MESSAGE);
}

private TranslatedValue translateTimeWktStruct(
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
boolean isTimestamp = createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE);
Expr<?> secondsVal = typeSystem.mkInt(0);
Expr<?> nanosVal = typeSystem.mkInt(0);
List<TranslatedValue> entryTvs = new ArrayList<>();

for (CelExpr.CelStruct.Entry entry : createStruct.entries()) {
TranslatedValue entryTv = translateExpr(entry.value(), ast);
Expr<?> val = entryTv.z3Expr();
Expr<?> unpackedVal = val;
BoolExpr hasValue = ctx.mkTrue();
if (entry.optionalEntry()) {
Expr<?> checkedVal =
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
entryTv =
TranslatedValue.create(
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
hasValue = typeSystem.optHasValue(optRef);
unpackedVal = typeSystem.getOptionalValue(optRef);
}
if (entry.fieldKey().equals(SECONDS_FIELD)) {
secondsVal = ctx.mkITE(hasValue, unpackedVal, secondsVal);
} else {
nanosVal = ctx.mkITE(hasValue, unpackedVal, nanosVal);
}
entryTvs.add(entryTv);
}

IntExpr seconds = typeSystem.getInt(secondsVal);
IntExpr nanos = typeSystem.getInt(nanosVal);
IntExpr totalNanos =
(IntExpr)
ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos);

BoolExpr typeError =
ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal)));
BoolExpr rangeError;
if (isTimestamp) {
BoolExpr nanosOutOfRange =
ctx.mkOr(
ctx.mkLt(nanos, ctx.mkInt(0)),
ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
rangeError = ctx.mkOr(nanosOutOfRange, typeSystem.checkTimestampOverflow(totalNanos));
} else {
BoolExpr nanosOutOfRange =
ctx.mkOr(
ctx.mkLt(nanos, ctx.mkInt(MIN_DURATION_NANOS)),
ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
BoolExpr signMismatch =
ctx.mkOr(
ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
rangeError =
ctx.mkOr(nanosOutOfRange, signMismatch, typeSystem.checkDurationOverflow(totalNanos));
}
Expr<?> wrapped =
isTimestamp ? typeSystem.wrapTimestamp(totalNanos) : typeSystem.wrapDuration(totalNanos);
Expr<?> result = typeSystem.withRuntimeError(wrapped, typeError, rangeError);
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
}

private Expr<?> getDefaultValueForType(CelType type) {
if (type instanceof NullableType) {
return typeSystem.mkNull();
Expand Down Expand Up @@ -1326,14 +1464,14 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
return typeSystem.isBytes(val);
}
if (type.equals(SimpleType.TIMESTAMP)) {
IntExpr seconds = typeSystem.getTimestamp(val);
IntExpr nanos = typeSystem.getTimestamp(val);
return ctx.mkAnd(
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
}
if (type.equals(SimpleType.DURATION)) {
IntExpr seconds = typeSystem.getDuration(val);
IntExpr nanos = typeSystem.getDuration(val);
return ctx.mkAnd(
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
}

if (type instanceof ListType) {
Expand Down
29 changes: 27 additions & 2 deletions verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,13 +16,15 @@

import static com.google.common.base.Preconditions.checkArgument;
import static com.google.common.base.Preconditions.checkNotNull;
import static com.google.common.collect.ImmutableList.toImmutableList;

import com.google.common.annotations.VisibleForTesting;
import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableMap;
import com.google.common.collect.ImmutableSet;
import com.google.errorprone.annotations.CanIgnoreReturnValue;
import com.google.errorprone.annotations.Immutable;
import com.google.protobuf.Descriptors.Descriptor;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Model;
Expand All @@ -32,6 +34,8 @@
import dev.cel.bundle.Cel;
import dev.cel.bundle.CelFactory;
import dev.cel.common.CelAbstractSyntaxTree;
import dev.cel.common.internal.DefaultDescriptorPool;
import dev.cel.common.internal.WellKnownProto;
import dev.cel.common.types.CelType;
import dev.cel.common.types.CelTypeProvider;
import dev.cel.optimizer.CelOptimizationException;
Expand Down Expand Up @@ -64,6 +68,26 @@ public Optional<CelType> findType(String typeName) {
}
};

private static final ImmutableList<Descriptor> WELL_KNOWN_DESCRIPTORS =
ImmutableList.of(
WellKnownProto.DURATION,
WellKnownProto.JSON_LIST_VALUE,
WellKnownProto.JSON_STRUCT_VALUE,
WellKnownProto.JSON_VALUE,
WellKnownProto.TIMESTAMP,
WellKnownProto.FLOAT_VALUE,
WellKnownProto.INT32_VALUE,
WellKnownProto.INT64_VALUE,
WellKnownProto.STRING_VALUE,
WellKnownProto.BOOL_VALUE,
WellKnownProto.BYTES_VALUE,
WellKnownProto.DOUBLE_VALUE,
WellKnownProto.UINT32_VALUE,
WellKnownProto.UINT64_VALUE)
.stream()
.map(DefaultDescriptorPool::getWellKnownProtoDescriptor)
.collect(toImmutableList());

private final Duration timeout;
private final int comprehensionUnrollLimit;
private final ImmutableSet<String> unknownIdentifiers;
Expand All @@ -74,7 +98,8 @@ public Optional<CelType> findType(String typeName) {
private final Cel cel;

static Builder newBuilder() {
return new Builder(CelFactory.plannerCelBuilder().build());
return new Builder(
CelFactory.plannerCelBuilder().addMessageTypes(WELL_KNOWN_DESCRIPTORS).build());
}

static Builder newBuilder(Cel cel) {
Expand Down Expand Up @@ -155,7 +180,7 @@ private Builder(Cel cel) {
this.comprehensionUnrollLimit = 5;
this.unknownIdentifiers = ImmutableSet.builder();
this.functionAxioms = ImmutableList.builder();
this.typeProvider = EMPTY_TYPE_PROVIDER;
this.typeProvider = cel.getTypeProvider();
this.cel = cel;
}
}
Expand Down
31 changes: 29 additions & 2 deletions verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@
import com.microsoft.z3.IntNum;
import com.microsoft.z3.Model;
import com.microsoft.z3.RatNum;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.LinkedHashSet;
Expand Down Expand Up @@ -86,9 +87,9 @@ private static String formatExpr(
if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
} else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
return formatTimestamp(expr.getArgs()[0]);
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
return formatDuration(expr.getArgs()[0]);
} else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
} else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {
Expand Down Expand Up @@ -154,6 +155,32 @@ private static String formatExpr(
return expr.toString();
}

private static String formatTimestamp(Expr<?> nanosExpr) {
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
BigInteger seconds = divRem[0];
BigInteger nanos = divRem[1];
if (nanos.signum() < 0) {
seconds = seconds.subtract(BigInteger.ONE);
nanos = nanos.add(nanosPerSecond);
}
if (nanos.equals(BigInteger.ZERO)) {
return "timestamp(" + seconds + ")";
}
return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}";
}

private static String formatDuration(Expr<?> nanosExpr) {
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
if (divRem[1].equals(BigInteger.ZERO)) {
return "duration('" + divRem[0] + "s')";
}
return "duration('" + totalNanos + "ns')";
}

private static String reconstructList(
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef) {
Expr<?> lenExpr =
Expand Down
35 changes: 28 additions & 7 deletions verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
import com.microsoft.z3.SeqSort;
import com.microsoft.z3.Sort;
import dev.cel.common.internal.ProtoTimeUtils;
import java.math.BigInteger;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
Expand All @@ -56,6 +57,22 @@
@SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types.
public final class CelZ3TypeSystem {

/** Number of nanoseconds per second. */
public static final long NANOS_PER_SECOND = 1_000_000_000L;

private static final long MAX_TIMESTAMP_NANOS_PART = 999_999_999L;

private static final String MIN_TIMESTAMP_NANOS =
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
.toString();

private static final String MAX_TIMESTAMP_NANOS =
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
.add(BigInteger.valueOf(MAX_TIMESTAMP_NANOS_PART))
.toString();

private static final String TYPE_CEL_VALUE = "CelValue";
private static final String CONS_BOOL = "Bool";
private static final String IS_BOOL = "isBool";
Expand Down Expand Up @@ -777,18 +794,22 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64)));
}

/** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
/**
* Checks if the given nanosecond arithmetic expression overflows CEL Timestamp bounds
* ({@code [0001-01-01T00:00:00Z, 9999-12-31T23:59:59.999999999Z]}).
*/
public BoolExpr checkTimestampOverflow(ArithExpr result) {
return ctx.mkOr(
ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)),
ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)));
ctx.mkGt(result, ctx.mkInt(MAX_TIMESTAMP_NANOS)),
ctx.mkLt(result, ctx.mkInt(MIN_TIMESTAMP_NANOS)));
}

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

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