Skip to content

Implement optional field traversal semantics in verifier #1146

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

Merged
copybara-service merged 1 commit into from
Jul 27, 2026
Merged

Implement optional field traversal semantics in verifier #1146

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
11 changes: 9 additions & 2 deletions checker/src/main/java/dev/cel/checker/CelStandardDeclarations.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ public final class CelStandardDeclarations {
private final ImmutableSet<CelIdentDecl> celIdentDecls;

/** Enumeration of Standard Functions. */
public enum StandardFunction {
public enum StandardFunction implements CelFunctionDecl.Declarer {
// Deprecated - use {@link #IN}
OLD_IN(
true,
Expand Down Expand Up @@ -1504,6 +1504,7 @@ private CelFunctionDecl withOverloads(Iterable<StandardOverload> overloads) {
return newCelFunctionDecl(functionName, ImmutableSet.copyOf(overloads));
}

@Override
public CelFunctionDecl functionDecl() {
return celFunctionDecl;
}
Expand Down Expand Up @@ -1579,8 +1580,14 @@ public CelIdentDecl identDecl() {

/** General interface for defining a standard function overload. */
@Immutable
public interface StandardOverload {
public interface StandardOverload extends CelFunctionDecl.Declarer {
CelOverloadDecl celOverloadDecl();

@Override
default CelFunctionDecl functionDecl() {
// TODO: Remove default keyword by implementing this for all standard overloads
throw new UnsupportedOperationException("Unimplemented");
}
}

/** Set of all standard function names. */
Expand Down
6 changes: 6 additions & 0 deletions common/src/main/java/dev/cel/common/CelFunctionDecl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,12 @@ public abstract class CelFunctionDecl {
/** Required. List of function overloads. Must contain at least one overload. */
public abstract ImmutableSet<CelOverloadDecl> overloads();

/** General interface for defining an extension function overload or standard declaration. */
@Immutable
public interface Declarer {
CelFunctionDecl functionDecl();
}

/** Builder for configuring the {@link CelFunctionDecl}. */
@AutoValue.Builder
public abstract static class Builder {
Expand Down
4 changes: 3 additions & 1 deletion extensions/src/main/java/dev/cel/extensions/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,9 @@ package(

java_library(
name = "extension_library",
srcs = ["CelExtensionLibrary.java"],
srcs = [
"CelExtensionLibrary.java",
],
tags = [
],
deps = [
Expand Down
207 changes: 130 additions & 77 deletions extensions/src/main/java/dev/cel/extensions/CelOptionalLibrary.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -97,95 +97,148 @@ public String getFunction() {
}
}

private static final class Types {
private static final TypeParamType PARAM_TYPE_K = TypeParamType.create("K");
private static final TypeParamType PARAM_TYPE_V = TypeParamType.create("V");
private static final OptionalType OPTIONAL_TYPE_V = OptionalType.create(PARAM_TYPE_V);
private static final ListType LIST_TYPE_V = ListType.create(PARAM_TYPE_V);
private static final MapType MAP_TYPE_KV = MapType.create(PARAM_TYPE_K, PARAM_TYPE_V);
}

/** Declarations for the optional extension library. */
public enum OptionalDeclaration implements CelFunctionDecl.Declarer {
OPTIONAL_OF(
CelFunctionDecl.newFunctionDeclaration(
Function.OPTIONAL_OF.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_of", Types.OPTIONAL_TYPE_V, Types.PARAM_TYPE_V))),
OPTIONAL_OF_NON_ZERO_VALUE(
CelFunctionDecl.newFunctionDeclaration(
Function.OPTIONAL_OF_NON_ZERO_VALUE.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_ofNonZeroValue", Types.OPTIONAL_TYPE_V, Types.PARAM_TYPE_V))),
OPTIONAL_NONE(
CelFunctionDecl.newFunctionDeclaration(
Function.OPTIONAL_NONE.getFunction(),
CelOverloadDecl.newGlobalOverload("optional_none", Types.OPTIONAL_TYPE_V))),
OPTIONAL_VALUE(
CelFunctionDecl.newFunctionDeclaration(
Function.VALUE.getFunction(),
CelOverloadDecl.newMemberOverload(
"optional_value", Types.PARAM_TYPE_V, Types.OPTIONAL_TYPE_V))),
OPTIONAL_HAS_VALUE(
CelFunctionDecl.newFunctionDeclaration(
Function.HAS_VALUE.getFunction(),
CelOverloadDecl.newMemberOverload(
"optional_hasValue", SimpleType.BOOL, Types.OPTIONAL_TYPE_V))),
OPTIONAL_UNWRAP(
CelFunctionDecl.newFunctionDeclaration(
Function.OPTIONAL_UNWRAP.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_unwrap_list",
Types.LIST_TYPE_V,
ListType.create(Types.OPTIONAL_TYPE_V)))),
OPTIONAL_OR(
CelFunctionDecl.newFunctionDeclaration(
"or",
CelOverloadDecl.newMemberOverload(
"optional_or_optional",
Types.OPTIONAL_TYPE_V,
Types.OPTIONAL_TYPE_V,
Types.OPTIONAL_TYPE_V))),
OPTIONAL_OR_VALUE(
CelFunctionDecl.newFunctionDeclaration(
"orValue",
CelOverloadDecl.newMemberOverload(
"optional_orValue_value",
Types.PARAM_TYPE_V,
Types.OPTIONAL_TYPE_V,
Types.PARAM_TYPE_V))),
OPTIONAL_SELECT(
CelFunctionDecl.newFunctionDeclaration(
Operator.OPTIONAL_SELECT.getFunction(),
CelOverloadDecl.newGlobalOverload(
"select_optional_field",
Types.OPTIONAL_TYPE_V,
SimpleType.DYN,
SimpleType.STRING))),
OPTIONAL_INDEX(
CelFunctionDecl.newFunctionDeclaration(
Operator.OPTIONAL_INDEX.getFunction(),
CelOverloadDecl.newGlobalOverload(
"list_optindex_optional_int",
Types.OPTIONAL_TYPE_V,
Types.LIST_TYPE_V,
SimpleType.INT),
CelOverloadDecl.newGlobalOverload(
"optional_list_optindex_optional_int",
Types.OPTIONAL_TYPE_V,
OptionalType.create(Types.LIST_TYPE_V),
SimpleType.INT),
CelOverloadDecl.newGlobalOverload(
"map_optindex_optional_value",
Types.OPTIONAL_TYPE_V,
Types.MAP_TYPE_KV,
Types.PARAM_TYPE_K),
CelOverloadDecl.newGlobalOverload(
"optional_map_optindex_optional_value",
Types.OPTIONAL_TYPE_V,
OptionalType.create(Types.MAP_TYPE_KV),
Types.PARAM_TYPE_K))),
OPTIONAL_INDEX_OPERAND(
CelFunctionDecl.newFunctionDeclaration(
Operator.INDEX.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_list_index_int",
Types.OPTIONAL_TYPE_V,
OptionalType.create(Types.LIST_TYPE_V),
SimpleType.INT),
CelOverloadDecl.newGlobalOverload(
"optional_map_index_value",
Types.OPTIONAL_TYPE_V,
OptionalType.create(Types.MAP_TYPE_KV),
Types.PARAM_TYPE_K)));

private final CelFunctionDecl celFunctionDecl;

OptionalDeclaration(CelFunctionDecl celFunctionDecl) {
this.celFunctionDecl = celFunctionDecl;
}

@Override
public CelFunctionDecl functionDecl() {
return celFunctionDecl;
}
}

private static final CelExtensionLibrary<CelOptionalLibrary> LIBRARY =
new CelExtensionLibrary<CelOptionalLibrary>() {
final TypeParamType paramTypeK = TypeParamType.create("K");
final TypeParamType paramTypeV = TypeParamType.create("V");
final OptionalType optionalTypeV = OptionalType.create(paramTypeV);
final ListType listTypeV = ListType.create(paramTypeV);
final MapType mapTypeKv = MapType.create(paramTypeK, paramTypeV);

private final CelOptionalLibrary version0 =
new CelOptionalLibrary(
0,
ImmutableSet.of(
CelFunctionDecl.newFunctionDeclaration(
OPTIONAL_OF.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_of", optionalTypeV, paramTypeV)),
CelFunctionDecl.newFunctionDeclaration(
OPTIONAL_OF_NON_ZERO_VALUE.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_ofNonZeroValue", optionalTypeV, paramTypeV)),
CelFunctionDecl.newFunctionDeclaration(
OPTIONAL_NONE.getFunction(),
CelOverloadDecl.newGlobalOverload("optional_none", optionalTypeV)),
CelFunctionDecl.newFunctionDeclaration(
VALUE.getFunction(),
CelOverloadDecl.newMemberOverload(
"optional_value", paramTypeV, optionalTypeV)),
CelFunctionDecl.newFunctionDeclaration(
HAS_VALUE.getFunction(),
CelOverloadDecl.newMemberOverload(
"optional_hasValue", SimpleType.BOOL, optionalTypeV)),
CelFunctionDecl.newFunctionDeclaration(
OPTIONAL_UNWRAP.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_unwrap_list", listTypeV, ListType.create(optionalTypeV))),
OptionalDeclaration.OPTIONAL_OF.functionDecl(),
OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE.functionDecl(),
OptionalDeclaration.OPTIONAL_NONE.functionDecl(),
OptionalDeclaration.OPTIONAL_VALUE.functionDecl(),
OptionalDeclaration.OPTIONAL_HAS_VALUE.functionDecl(),
OptionalDeclaration.OPTIONAL_UNWRAP.functionDecl(),
// Note: Implementation of "or" and "orValue" are special-cased inside the
// interpreter. Hence, their bindings are not provided here.
CelFunctionDecl.newFunctionDeclaration(
"or",
CelOverloadDecl.newMemberOverload(
"optional_or_optional", optionalTypeV, optionalTypeV, optionalTypeV)),
CelFunctionDecl.newFunctionDeclaration(
"orValue",
CelOverloadDecl.newMemberOverload(
"optional_orValue_value", paramTypeV, optionalTypeV, paramTypeV)),
OptionalDeclaration.OPTIONAL_OR.functionDecl(),
OptionalDeclaration.OPTIONAL_OR_VALUE.functionDecl(),
// Note: Function bindings for optional field selection and indexer is defined
// in {@code StandardFunctions}.
CelFunctionDecl.newFunctionDeclaration(
Operator.OPTIONAL_SELECT.getFunction(),
CelOverloadDecl.newGlobalOverload(
"select_optional_field",
optionalTypeV,
SimpleType.DYN,
SimpleType.STRING)),
CelFunctionDecl.newFunctionDeclaration(
Operator.OPTIONAL_INDEX.getFunction(),
CelOverloadDecl.newGlobalOverload(
"list_optindex_optional_int", optionalTypeV, listTypeV, SimpleType.INT),
CelOverloadDecl.newGlobalOverload(
"optional_list_optindex_optional_int",
optionalTypeV,
OptionalType.create(listTypeV),
SimpleType.INT),
CelOverloadDecl.newGlobalOverload(
"map_optindex_optional_value", optionalTypeV, mapTypeKv, paramTypeK),
CelOverloadDecl.newGlobalOverload(
"optional_map_optindex_optional_value",
optionalTypeV,
OptionalType.create(mapTypeKv),
paramTypeK)),
OptionalDeclaration.OPTIONAL_SELECT.functionDecl(),
OptionalDeclaration.OPTIONAL_INDEX.functionDecl(),
// Index overloads to accommodate using an optional value as the operand
CelFunctionDecl.newFunctionDeclaration(
Operator.INDEX.getFunction(),
CelOverloadDecl.newGlobalOverload(
"optional_list_index_int",
optionalTypeV,
OptionalType.create(listTypeV),
SimpleType.INT),
CelOverloadDecl.newGlobalOverload(
"optional_map_index_value",
optionalTypeV,
OptionalType.create(mapTypeKv),
paramTypeK))),
OptionalDeclaration.OPTIONAL_INDEX_OPERAND.functionDecl()),
ImmutableSet.of(
CelMacro.newReceiverMacro("optMap", 2, CelOptionalLibrary::expandOptMap)),
ImmutableSet.of(
// Type declaration for optional_type -> type(optional_type(V))
CelVarDecl.newVarDeclaration(
OptionalType.NAME, TypeType.create(optionalTypeV))));
OptionalType.NAME, TypeType.create(Types.OPTIONAL_TYPE_V))));

private final CelOptionalLibrary version1 =
new CelOptionalLibrary(
Expand All @@ -211,16 +264,16 @@ public String getFunction() {
"optional_list_first",
"Return the first value in a list if present, otherwise"
+ " optional.none()",
optionalTypeV,
listTypeV)),
Types.OPTIONAL_TYPE_V,
Types.LIST_TYPE_V)),
CelFunctionDecl.newFunctionDeclaration(
LAST.functionName,
CelOverloadDecl.newMemberOverload(
"optional_list_last",
"Return the last value in a list if present, otherwise"
+ " optional.none()",
optionalTypeV,
listTypeV)))
Types.OPTIONAL_TYPE_V,
Types.LIST_TYPE_V)))
.build(),
version1.macros,
version1.variables);
Expand Down
37 changes: 29 additions & 8 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 @@ -243,7 +243,9 @@ private TranslatedValue translateOperatorCall(
// by our axioms
return TranslatedValue.propagateStrict(ctx, typeSystem, typeSystem.mkError(), args);
case INDEX:
return translateIndex(args, ast);
return translateIndex(args, ast, false);
case OPTIONAL_INDEX:
return translateIndex(args, ast, true);
case CONDITIONAL:
return translateConditional(args, ast);
case NOT_STRICTLY_FALSE:
Expand Down Expand Up @@ -600,7 +602,8 @@ private TranslatedValue translateEquality(
.withApproximation(ctx.mkFalse());
}

private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard) {
private Expr<?> buildListIndex(
Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
Expr<?> listRef = typeSystem.getListRef(lhsTrans);
SeqExpr<?> seq = typeSystem.getSeq(listRef);
Expr<?> index = typeSystem.getInt(rhsTrans);
Expand All @@ -617,6 +620,14 @@ private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr type
constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotUnknown));
}

if (isOptional) {
Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val);
constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
constraintSink.accept(typeSystem.optHasValue(resultOptRef));
return ctx.mkITE(
inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
}

return ctx.mkITE(inBounds, val, typeSystem.mkError());
}

Expand Down Expand Up @@ -677,7 +688,8 @@ private ProbeResult createProbeResult(
return new ProbeResult(altInMap, altVal);
}

private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard) {
private Expr<?> buildMapIndex(
Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
Expr<?> mapRef = typeSystem.getMapRef(lhsTrans);
ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
Expand Down Expand Up @@ -780,10 +792,19 @@ private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeG
constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotUnknown));
}

if (isOptional) {
Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal);
constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
constraintSink.accept(typeSystem.optHasValue(resultOptRef));
return ctx.mkITE(
finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
}

return ctx.mkITE(finalInMap, finalVal, typeSystem.mkError());
}

private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSyntaxTree ast) {
private TranslatedValue translateIndex(
List<TranslatedValue> args, CelAbstractSyntaxTree ast, boolean isOptional) {
Expr<?> lhsTrans = args.get(0).z3Expr();
Expr<?> rhsTrans = args.get(1).z3Expr();

Expand All @@ -794,13 +815,13 @@ private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSy

Expr<?> actualValue;
if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) {
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue());
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
constraintSink.accept(
ctx.mkImplies(
ctx.mkNot(typeSystem.isError(actualValue)),
typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType())));
} else if (lhsType.kind() == CelKind.MAP) {
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue());
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
constraintSink.accept(
ctx.mkImplies(
ctx.mkNot(typeSystem.isError(actualValue)),
Expand All @@ -810,8 +831,8 @@ private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSy
BoolExpr isMapGuard = typeSystem.isMap(lhsTrans);
actualValue =
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard))
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard))
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
.build(typeSystem.mkError());
}

Expand Down
Loading
Loading