Skip to content

Add type constraints to uninterpreted conversions #1154

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
Open

Add type constraints to uninterpreted conversions #1154

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
13 changes: 4 additions & 9 deletions common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,6 @@
import static com.google.common.math.LongMath.checkedMultiply;
import static com.google.common.math.LongMath.checkedSubtract;

import com.google.common.annotations.VisibleForTesting;
import com.google.common.base.Strings;
import com.google.errorprone.annotations.CanIgnoreReturnValue;
import com.google.protobuf.Duration;
Expand Down Expand Up @@ -50,15 +49,11 @@
public final class ProtoTimeUtils {

// Timestamp for "0001-01-01T00:00:00Z"
@VisibleForTesting
static final long TIMESTAMP_SECONDS_MIN = -62135596800L;
public static final long TIMESTAMP_SECONDS_MIN = -62135596800L;
// Timestamp for "9999-12-31T23:59:59Z"
@VisibleForTesting
static final long TIMESTAMP_SECONDS_MAX = 253402300799L;
@VisibleForTesting
static final long DURATION_SECONDS_MIN = -315576000000L;
@VisibleForTesting
static final long DURATION_SECONDS_MAX = 315576000000L;
public static final long TIMESTAMP_SECONDS_MAX = 253402300799L;
public static final long DURATION_SECONDS_MIN = -315576000000L;
public static final long DURATION_SECONDS_MAX = 315576000000L;

private static final int MILLIS_PER_SECOND = 1000;

Expand Down
2 changes: 1 addition & 1 deletion verifier/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -400,7 +400,7 @@ public class InvariantsExample {

### Timeouts

SMT solving is NP-complete and can theoretically stop responding or take an
SMT solving is NP-hard and can theoretically stop responding or take an
exponential amount of time for complex formulas.
The verifier uses a default timeout of 10 seconds. It is recommended to
configure this to a reasonable duration for your specific use case using
Expand Down
1 change: 1 addition & 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 @@ -98,6 +98,7 @@ java_library(
tags = [
],
deps = [
"//common/internal:proto_time_utils",
"@maven//:com_google_errorprone_error_prone_annotations",
"@maven//:com_google_guava_guava",
"@maven//:tools_aqua_z3_turnkey",
Expand Down
17 changes: 17 additions & 0 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 @@ -533,6 +533,12 @@ private Expr<?> getDefaultValueForType(CelType type) {
if (type.equals(SimpleType.UINT)) {
return typeSystem.mkUint(0);
}
if (type.equals(SimpleType.TIMESTAMP)) {
return typeSystem.wrapTimestamp(ctx.mkInt(0));
}
if (type.equals(SimpleType.DURATION)) {
return typeSystem.wrapDuration(ctx.mkInt(0));
}
if (type instanceof ListType) {
if (emptyListCache == null) {
emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX);
Expand Down Expand Up @@ -1269,6 +1275,17 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
if (type.equals(SimpleType.BYTES)) {
return (BoolExpr) ctx.mkApp(typeSystem.bytesCons().getTesterDecl(), val);
}
if (type.equals(SimpleType.TIMESTAMP)) {
IntExpr seconds = typeSystem.getTimestamp(val);
return ctx.mkAnd(
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
}
if (type.equals(SimpleType.DURATION)) {
IntExpr seconds = typeSystem.getDuration(val);
return ctx.mkAnd(
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
}

if (type instanceof ListType) {
// Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers
// here.
Expand Down
4 changes: 4 additions & 0 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 @@ -82,6 +82,10 @@ private static String formatExpr(
// Handle CelType constructors wrapper unwrapping
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]) + ")";
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
return "duration(" + formatExpr(ctx, typeSystem, model, 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
33 changes: 17 additions & 16 deletions verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -148,11 +148,11 @@ private BoolExpr mkTypeGuard(Expr<?> arg, CelType expectedType) {
// These match everything structurally type-wise, although we might refine this later.
return ctx.mkTrue();
case INT:
return typeSystem.isInt(arg);
case TIMESTAMP:
return typeSystem.isTimestamp(arg);
case DURATION:
// Safe to map int, timestamp, and duration to IntSort because CEL's static checker prevents
// invalid cross-type usage and their operator axioms translate to identical Z3 ASTs.
return typeSystem.isInt(arg);
return typeSystem.isDuration(arg);
case UINT:
return typeSystem.isUint(arg);
case DOUBLE:
Expand Down Expand Up @@ -386,7 +386,7 @@ private BoolExpr getNumericEqualityWithConstant(
? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal))
: ctx.mkFalse();
} else if (symType.kind() == CelKind.DOUBLE) {
return ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
return ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
}
}

Expand All @@ -396,8 +396,7 @@ private BoolExpr getNumericEqualityWithConstant(
(uintVal != null)
? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal))
: ctx.mkFalse();
BoolExpr doubleEq =
ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));

return (BoolExpr)
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
Expand Down Expand Up @@ -435,18 +434,17 @@ private BoolExpr getStaticallyKnownNumericEquality(
case UINT:
return ctx.mkEq(typeSystem.getUint(z3Expr0), typeSystem.getUint(z3Expr1));
case DOUBLE:
return ctx.mkFPEq(
(FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1));
return ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1));
default:
return ctx.mkFalse();
}
}

private BoolExpr mkIsFiniteDouble(Expr<?> z3Expr) {
Expr<?> fpVal = typeSystem.getDouble(z3Expr);
FPExpr fpVal = typeSystem.getDouble(z3Expr);
return ctx.mkAnd(
typeSystem.isDouble(z3Expr),
ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN((FPExpr) fpVal), ctx.mkFPIsInfinite((FPExpr) fpVal))));
ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN(fpVal), ctx.mkFPIsInfinite(fpVal))));
}

private BoolExpr getDynamicNumericEquality(Expr<?> z3Expr0, Expr<?> z3Expr1) {
Expand Down Expand Up @@ -475,25 +473,28 @@ private BoolExpr getDynamicNumericEquality(Expr<?> z3Expr0, Expr<?> z3Expr1) {
BoolExpr isIntOrUintAndDouble = ctx.mkAnd(isIntOrUint0, typeSystem.isDouble(z3Expr1));
BoolExpr isDoubleAndIntOrUint = ctx.mkAnd(typeSystem.isDouble(z3Expr0), isIntOrUint1);

Expr<?> fpVal1 = typeSystem.getDouble(z3Expr1);
FPExpr fpVal1 = typeSystem.getDouble(z3Expr1);
ArithExpr<?> realVal0 = ctx.mkInt2Real(val0);
BoolExpr intDoubleEq =
ctx.mkAnd(
mkIsFiniteDouble(z3Expr1),
ctx.mkEq(ctx.mkInt2Real(val0), ctx.mkFPToReal((FPExpr) fpVal1)));
ctx.mkLe(realVal0, ctx.mkFPToReal(fpVal1)),
ctx.mkLe(ctx.mkFPToReal(fpVal1), realVal0));

Expr<?> fpVal0 = typeSystem.getDouble(z3Expr0);
FPExpr fpVal0 = typeSystem.getDouble(z3Expr0);
ArithExpr<?> realVal1 = ctx.mkInt2Real(val1);
BoolExpr doubleIntEq =
ctx.mkAnd(
mkIsFiniteDouble(z3Expr0),
ctx.mkEq(ctx.mkFPToReal((FPExpr) fpVal0), ctx.mkInt2Real(val1)));
ctx.mkLe(realVal1, ctx.mkFPToReal(fpVal0)),
ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1));

return (BoolExpr)
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
.addCase(bothIntOrUint, ctx.mkEq(val0, val1))
.addCase(
bothDouble,
ctx.mkFPEq(
(FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1)))
ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1)))
.addCase(isIntOrUintAndDouble, intDoubleEq)
.addCase(isDoubleAndIntOrUint, doubleIntEq)
.build(ctx.mkFalse());
Expand Down
105 changes: 94 additions & 11 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 @@ -31,6 +31,7 @@
import com.microsoft.z3.SeqExpr;
import com.microsoft.z3.SeqSort;
import com.microsoft.z3.Sort;
import dev.cel.common.internal.ProtoTimeUtils;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
Expand Down Expand Up @@ -82,6 +83,14 @@ public final class CelZ3TypeSystem {
private static final String IS_BYTES = "isBytes";
private static final String GET_BYTES = "getBytes";

private static final String CONS_TIMESTAMP = "Timestamp";
private static final String IS_TIMESTAMP = "isTimestamp";
private static final String GET_TIMESTAMP = "getTimestamp";

private static final String CONS_DURATION = "Duration";
private static final String IS_DURATION = "isDuration";
private static final String GET_DURATION = "getDuration";

private static final String CONS_ERROR = "CelError";
private static final String IS_ERROR = "isError";

Expand Down Expand Up @@ -170,6 +179,8 @@ public int hashCode() {
private final Constructor doubleCons;
private final Constructor stringCons;
private final Constructor bytesCons;
private final Constructor timestampCons;
private final Constructor durationCons;
private final Constructor errorCons;
private final Constructor unknownCons;
private final Constructor nullCons;
Expand Down Expand Up @@ -233,30 +244,38 @@ public Sort listRefSort() {
return listRefSort;
}

Constructor boolCons() {
public Constructor boolCons() {
return boolCons;
}

Constructor intCons() {
public Constructor intCons() {
return intCons;
}

Constructor uintCons() {
public Constructor uintCons() {
return uintCons;
}

Constructor doubleCons() {
public Constructor doubleCons() {
return doubleCons;
}

Constructor stringCons() {
public Constructor stringCons() {
return stringCons;
}

Constructor bytesCons() {
public Constructor bytesCons() {
return bytesCons;
}

public Constructor timestampCons() {
return timestampCons;
}

public Constructor durationCons() {
return durationCons;
}

Constructor optionalCons() {
return optionalCons;
}
Expand Down Expand Up @@ -296,6 +315,16 @@ public Expr<?> wrapBytes(Expr<?> expr) {
return ctx.mkApp(bytesCons.ConstructorDecl(), expr);
}

/** Wraps a Z3 integer expression into a timestamp CelValue. */
public Expr<?> wrapTimestamp(IntExpr expr) {
return ctx.mkApp(timestampCons.ConstructorDecl(), expr);
}

/** Wraps a Z3 integer expression into a duration CelValue. */
public Expr<?> wrapDuration(IntExpr expr) {
return ctx.mkApp(durationCons.ConstructorDecl(), expr);
}

/** Creates a CelValue containing an integer. */
public Expr<?> mkInt(long val) {
return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val));
Expand Down Expand Up @@ -326,8 +355,8 @@ public BoolExpr isDouble(Expr<?> val) {
}

/** Extracts the double reference from a double CelValue. */
public Expr<?> getDouble(Expr<?> val) {
return ctx.mkApp(doubleCons.getAccessorDecls()[0], val);
public FPExpr getDouble(Expr<?> val) {
return (FPExpr) ctx.mkApp(doubleCons.getAccessorDecls()[0], val);
}

/**
Expand Down Expand Up @@ -372,7 +401,7 @@ public BoolExpr getStructuralEquality(Expr<?> arg0, Expr<?> arg1) {
// Doubles must be compared using native floating-point equality to follow IEEE-754.
// Z3's structural mkEq evaluates NaN == NaN as true and 0.0 == -0.0 as false.
BoolExpr isDoubleEq = ctx.mkAnd(isDouble(arg0), isDouble(arg1));
BoolExpr doubleEq = ctx.mkFPEq((FPExpr) getDouble(arg0), (FPExpr) getDouble(arg1));
BoolExpr doubleEq = ctx.mkFPEq(getDouble(arg0), getDouble(arg1));

// For primitives, generic equality matches the direct Z3 datatype wrapper.
BoolExpr genericEq = ctx.mkEq(arg0, arg1);
Expand Down Expand Up @@ -409,10 +438,14 @@ public Expr<?> mkNull() {
return ctx.mkConst(nullCons.ConstructorDecl());
}

Constructor errorCons() {
public Constructor errorCons() {
return errorCons;
}

public Constructor nullCons() {
return nullCons;
}

/** Creates a CelValue representing an unknown value. */
public Expr<?> mkUnknown() {
return mkUnknown(ctx.mkConst(GENERIC_UNKNOWN_ID, unknownIdSort));
Expand Down Expand Up @@ -498,7 +531,7 @@ public Expr<?> withRuntimeError(
return ctx.mkITE(condition, mkError(), result);
}

Constructor unknownCons() {
public Constructor unknownCons() {
return unknownCons;
}

Expand Down Expand Up @@ -582,6 +615,26 @@ public IntExpr getUint(Expr<?> val) {
return (IntExpr) ctx.mkApp(uintCons.getAccessorDecls()[0], val);
}

/** Checks if the given CelValue is a timestamp. */
public BoolExpr isTimestamp(Expr<?> val) {
return (BoolExpr) ctx.mkApp(timestampCons.getTesterDecl(), val);
}

/** Extracts the integer expression from a timestamp CelValue. */
public IntExpr getTimestamp(Expr<?> val) {
return (IntExpr) ctx.mkApp(timestampCons.getAccessorDecls()[0], val);
}

/** Checks if the given CelValue is a duration. */
public BoolExpr isDuration(Expr<?> val) {
return (BoolExpr) ctx.mkApp(durationCons.getTesterDecl(), val);
}

/** Extracts the integer expression from a duration CelValue. */
public IntExpr getDuration(Expr<?> val) {
return (IntExpr) ctx.mkApp(durationCons.getAccessorDecls()[0], val);
}

/** Checks if the given CelValue is a string. */
public BoolExpr isString(Expr<?> val) {
return (BoolExpr) ctx.mkApp(stringCons.getTesterDecl(), val);
Expand Down Expand Up @@ -719,6 +772,20 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64)));
}

/** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
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)));
}

/** Checks if the given arithmetic expression overflows CEL Duration bounds. */
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)));
}

/** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */
public BoolExpr checkUintOverflow(ArithExpr result) {
return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0)));
Expand Down Expand Up @@ -890,6 +957,20 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
this.bytesCons =
ctx.mkConstructor(
CONS_BYTES, IS_BYTES, new String[] {GET_BYTES}, new Sort[] {ctx.getStringSort()}, null);
this.timestampCons =
ctx.mkConstructor(
CONS_TIMESTAMP,
IS_TIMESTAMP,
new String[] {GET_TIMESTAMP},
new Sort[] {ctx.getIntSort()},
null);
this.durationCons =
ctx.mkConstructor(
CONS_DURATION,
IS_DURATION,
new String[] {GET_DURATION},
new Sort[] {ctx.getIntSort()},
null);
this.errorCons = ctx.mkConstructor(CONS_ERROR, IS_ERROR, null, null, null);

this.unknownIdSort = ctx.mkUninterpretedSort("UnknownId");
Expand Down Expand Up @@ -936,6 +1017,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
this.doubleCons,
this.stringCons,
this.bytesCons,
this.timestampCons,
this.durationCons,
this.errorCons,
this.unknownCons,
this.optionalCons,
Expand Down
Loading
Loading