Skip to content

Commit dc9d2ca

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Implement optional field traversal semantics in verifier
PiperOrigin-RevId: 954809810
1 parent d4c8913 commit dc9d2ca

7 files changed

Lines changed: 272 additions & 93 deletions

File tree

‎checker/src/main/java/dev/cel/checker/CelStandardDeclarations.java‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,7 +55,7 @@ public final class CelStandardDeclarations {
5555
private final ImmutableSet<CelIdentDecl> celIdentDecls;
5656

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

1507+
@Override
15071508
public CelFunctionDecl functionDecl() {
15081509
return celFunctionDecl;
15091510
}
@@ -1579,8 +1580,14 @@ public CelIdentDecl identDecl() {
15791580

15801581
/** General interface for defining a standard function overload. */
15811582
@Immutable
1582-
public interface StandardOverload {
1583+
public interface StandardOverload extends CelFunctionDecl.Declarer {
15831584
CelOverloadDecl celOverloadDecl();
1585+
1586+
@Override
1587+
default CelFunctionDecl functionDecl() {
1588+
return CelFunctionDecl.newFunctionDeclaration(
1589+
celOverloadDecl().overloadId(), ImmutableSet.of(celOverloadDecl()));
1590+
}
15841591
}
15851592

15861593
/** Set of all standard function names. */

‎common/src/main/java/dev/cel/common/CelFunctionDecl.java‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,12 @@ public abstract class CelFunctionDecl {
3838
/** Required. List of function overloads. Must contain at least one overload. */
3939
public abstract ImmutableSet<CelOverloadDecl> overloads();
4040

41+
/** General interface for defining an extension function overload or standard declaration. */
42+
@Immutable
43+
public interface Declarer {
44+
CelFunctionDecl functionDecl();
45+
}
46+
4147
/** Builder for configuring the {@link CelFunctionDecl}. */
4248
@AutoValue.Builder
4349
public abstract static class Builder {

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,9 @@ package(
1313

1414
java_library(
1515
name = "extension_library",
16-
srcs = ["CelExtensionLibrary.java"],
16+
srcs = [
17+
"CelExtensionLibrary.java",
18+
],
1719
tags = [
1820
],
1921
deps = [

‎extensions/src/main/java/dev/cel/extensions/CelOptionalLibrary.java‎

Lines changed: 111 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -97,95 +97,129 @@ public String getFunction() {
9797
}
9898
}
9999

100+
private static final TypeParamType PARAM_TYPE_K = TypeParamType.create("K");
101+
private static final TypeParamType PARAM_TYPE_V = TypeParamType.create("V");
102+
private static final OptionalType OPTIONAL_TYPE_V = OptionalType.create(PARAM_TYPE_V);
103+
private static final ListType LIST_TYPE_V = ListType.create(PARAM_TYPE_V);
104+
private static final MapType MAP_TYPE_KV = MapType.create(PARAM_TYPE_K, PARAM_TYPE_V);
105+
106+
public static final CelFunctionDecl OPTIONAL_SELECT_DECL =
107+
CelFunctionDecl.newFunctionDeclaration(
108+
Operator.OPTIONAL_SELECT.getFunction(),
109+
CelOverloadDecl.newGlobalOverload(
110+
"select_optional_field", OPTIONAL_TYPE_V, SimpleType.DYN, SimpleType.STRING));
111+
112+
/** Declarations for the optional extension library. */
113+
public enum OptionalDeclaration implements CelFunctionDecl.Declarer {
114+
OPTIONAL_OF(
115+
CelFunctionDecl.newFunctionDeclaration(
116+
Function.OPTIONAL_OF.getFunction(),
117+
CelOverloadDecl.newGlobalOverload("optional_of", OPTIONAL_TYPE_V, PARAM_TYPE_V))),
118+
OPTIONAL_OF_NON_ZERO_VALUE(
119+
CelFunctionDecl.newFunctionDeclaration(
120+
Function.OPTIONAL_OF_NON_ZERO_VALUE.getFunction(),
121+
CelOverloadDecl.newGlobalOverload(
122+
"optional_ofNonZeroValue", OPTIONAL_TYPE_V, PARAM_TYPE_V))),
123+
OPTIONAL_NONE(
124+
CelFunctionDecl.newFunctionDeclaration(
125+
Function.OPTIONAL_NONE.getFunction(),
126+
CelOverloadDecl.newGlobalOverload("optional_none", OPTIONAL_TYPE_V))),
127+
OPTIONAL_VALUE(
128+
CelFunctionDecl.newFunctionDeclaration(
129+
Function.VALUE.getFunction(),
130+
CelOverloadDecl.newMemberOverload("optional_value", PARAM_TYPE_V, OPTIONAL_TYPE_V))),
131+
OPTIONAL_HAS_VALUE(
132+
CelFunctionDecl.newFunctionDeclaration(
133+
Function.HAS_VALUE.getFunction(),
134+
CelOverloadDecl.newMemberOverload(
135+
"optional_hasValue", SimpleType.BOOL, OPTIONAL_TYPE_V))),
136+
OPTIONAL_UNWRAP(
137+
CelFunctionDecl.newFunctionDeclaration(
138+
Function.OPTIONAL_UNWRAP.getFunction(),
139+
CelOverloadDecl.newGlobalOverload(
140+
"optional_unwrap_list", LIST_TYPE_V, ListType.create(OPTIONAL_TYPE_V)))),
141+
OPTIONAL_OR(
142+
CelFunctionDecl.newFunctionDeclaration(
143+
"or",
144+
CelOverloadDecl.newMemberOverload(
145+
"optional_or_optional", OPTIONAL_TYPE_V, OPTIONAL_TYPE_V, OPTIONAL_TYPE_V))),
146+
OPTIONAL_OR_VALUE(
147+
CelFunctionDecl.newFunctionDeclaration(
148+
"orValue",
149+
CelOverloadDecl.newMemberOverload(
150+
"optional_orValue_value", PARAM_TYPE_V, OPTIONAL_TYPE_V, PARAM_TYPE_V))),
151+
OPTIONAL_SELECT(OPTIONAL_SELECT_DECL),
152+
OPTIONAL_INDEX(
153+
CelFunctionDecl.newFunctionDeclaration(
154+
Operator.OPTIONAL_INDEX.getFunction(),
155+
CelOverloadDecl.newGlobalOverload(
156+
"list_optindex_optional_int", OPTIONAL_TYPE_V, LIST_TYPE_V, SimpleType.INT),
157+
CelOverloadDecl.newGlobalOverload(
158+
"optional_list_optindex_optional_int",
159+
OPTIONAL_TYPE_V,
160+
OptionalType.create(LIST_TYPE_V),
161+
SimpleType.INT),
162+
CelOverloadDecl.newGlobalOverload(
163+
"map_optindex_optional_value", OPTIONAL_TYPE_V, MAP_TYPE_KV, PARAM_TYPE_K),
164+
CelOverloadDecl.newGlobalOverload(
165+
"optional_map_optindex_optional_value",
166+
OPTIONAL_TYPE_V,
167+
OptionalType.create(MAP_TYPE_KV),
168+
PARAM_TYPE_K))),
169+
OPTIONAL_INDEX_OPERAND(
170+
CelFunctionDecl.newFunctionDeclaration(
171+
Operator.INDEX.getFunction(),
172+
CelOverloadDecl.newGlobalOverload(
173+
"optional_list_index_int",
174+
OPTIONAL_TYPE_V,
175+
OptionalType.create(LIST_TYPE_V),
176+
SimpleType.INT),
177+
CelOverloadDecl.newGlobalOverload(
178+
"optional_map_index_value",
179+
OPTIONAL_TYPE_V,
180+
OptionalType.create(MAP_TYPE_KV),
181+
PARAM_TYPE_K)));
182+
183+
private final CelFunctionDecl celFunctionDecl;
184+
185+
OptionalDeclaration(CelFunctionDecl celFunctionDecl) {
186+
this.celFunctionDecl = celFunctionDecl;
187+
}
188+
189+
@Override
190+
public CelFunctionDecl functionDecl() {
191+
return celFunctionDecl;
192+
}
193+
}
194+
100195
private static final CelExtensionLibrary<CelOptionalLibrary> LIBRARY =
101196
new CelExtensionLibrary<CelOptionalLibrary>() {
102-
final TypeParamType paramTypeK = TypeParamType.create("K");
103-
final TypeParamType paramTypeV = TypeParamType.create("V");
104-
final OptionalType optionalTypeV = OptionalType.create(paramTypeV);
105-
final ListType listTypeV = ListType.create(paramTypeV);
106-
final MapType mapTypeKv = MapType.create(paramTypeK, paramTypeV);
107-
108197
private final CelOptionalLibrary version0 =
109198
new CelOptionalLibrary(
110199
0,
111200
ImmutableSet.of(
112-
CelFunctionDecl.newFunctionDeclaration(
113-
OPTIONAL_OF.getFunction(),
114-
CelOverloadDecl.newGlobalOverload(
115-
"optional_of", optionalTypeV, paramTypeV)),
116-
CelFunctionDecl.newFunctionDeclaration(
117-
OPTIONAL_OF_NON_ZERO_VALUE.getFunction(),
118-
CelOverloadDecl.newGlobalOverload(
119-
"optional_ofNonZeroValue", optionalTypeV, paramTypeV)),
120-
CelFunctionDecl.newFunctionDeclaration(
121-
OPTIONAL_NONE.getFunction(),
122-
CelOverloadDecl.newGlobalOverload("optional_none", optionalTypeV)),
123-
CelFunctionDecl.newFunctionDeclaration(
124-
VALUE.getFunction(),
125-
CelOverloadDecl.newMemberOverload(
126-
"optional_value", paramTypeV, optionalTypeV)),
127-
CelFunctionDecl.newFunctionDeclaration(
128-
HAS_VALUE.getFunction(),
129-
CelOverloadDecl.newMemberOverload(
130-
"optional_hasValue", SimpleType.BOOL, optionalTypeV)),
131-
CelFunctionDecl.newFunctionDeclaration(
132-
OPTIONAL_UNWRAP.getFunction(),
133-
CelOverloadDecl.newGlobalOverload(
134-
"optional_unwrap_list", listTypeV, ListType.create(optionalTypeV))),
201+
OptionalDeclaration.OPTIONAL_OF.functionDecl(),
202+
OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE.functionDecl(),
203+
OptionalDeclaration.OPTIONAL_NONE.functionDecl(),
204+
OptionalDeclaration.OPTIONAL_VALUE.functionDecl(),
205+
OptionalDeclaration.OPTIONAL_HAS_VALUE.functionDecl(),
206+
OptionalDeclaration.OPTIONAL_UNWRAP.functionDecl(),
135207
// Note: Implementation of "or" and "orValue" are special-cased inside the
136208
// interpreter. Hence, their bindings are not provided here.
137-
CelFunctionDecl.newFunctionDeclaration(
138-
"or",
139-
CelOverloadDecl.newMemberOverload(
140-
"optional_or_optional", optionalTypeV, optionalTypeV, optionalTypeV)),
141-
CelFunctionDecl.newFunctionDeclaration(
142-
"orValue",
143-
CelOverloadDecl.newMemberOverload(
144-
"optional_orValue_value", paramTypeV, optionalTypeV, paramTypeV)),
209+
OptionalDeclaration.OPTIONAL_OR.functionDecl(),
210+
OptionalDeclaration.OPTIONAL_OR_VALUE.functionDecl(),
145211
// Note: Function bindings for optional field selection and indexer is defined
146212
// in {@code StandardFunctions}.
147-
CelFunctionDecl.newFunctionDeclaration(
148-
Operator.OPTIONAL_SELECT.getFunction(),
149-
CelOverloadDecl.newGlobalOverload(
150-
"select_optional_field",
151-
optionalTypeV,
152-
SimpleType.DYN,
153-
SimpleType.STRING)),
154-
CelFunctionDecl.newFunctionDeclaration(
155-
Operator.OPTIONAL_INDEX.getFunction(),
156-
CelOverloadDecl.newGlobalOverload(
157-
"list_optindex_optional_int", optionalTypeV, listTypeV, SimpleType.INT),
158-
CelOverloadDecl.newGlobalOverload(
159-
"optional_list_optindex_optional_int",
160-
optionalTypeV,
161-
OptionalType.create(listTypeV),
162-
SimpleType.INT),
163-
CelOverloadDecl.newGlobalOverload(
164-
"map_optindex_optional_value", optionalTypeV, mapTypeKv, paramTypeK),
165-
CelOverloadDecl.newGlobalOverload(
166-
"optional_map_optindex_optional_value",
167-
optionalTypeV,
168-
OptionalType.create(mapTypeKv),
169-
paramTypeK)),
213+
OptionalDeclaration.OPTIONAL_SELECT.functionDecl(),
214+
OptionalDeclaration.OPTIONAL_INDEX.functionDecl(),
170215
// Index overloads to accommodate using an optional value as the operand
171-
CelFunctionDecl.newFunctionDeclaration(
172-
Operator.INDEX.getFunction(),
173-
CelOverloadDecl.newGlobalOverload(
174-
"optional_list_index_int",
175-
optionalTypeV,
176-
OptionalType.create(listTypeV),
177-
SimpleType.INT),
178-
CelOverloadDecl.newGlobalOverload(
179-
"optional_map_index_value",
180-
optionalTypeV,
181-
OptionalType.create(mapTypeKv),
182-
paramTypeK))),
216+
OptionalDeclaration.OPTIONAL_INDEX_OPERAND.functionDecl()),
183217
ImmutableSet.of(
184218
CelMacro.newReceiverMacro("optMap", 2, CelOptionalLibrary::expandOptMap)),
185219
ImmutableSet.of(
186220
// Type declaration for optional_type -> type(optional_type(V))
187221
CelVarDecl.newVarDeclaration(
188-
OptionalType.NAME, TypeType.create(optionalTypeV))));
222+
OptionalType.NAME, TypeType.create(OPTIONAL_TYPE_V))));
189223

190224
private final CelOptionalLibrary version1 =
191225
new CelOptionalLibrary(
@@ -211,16 +245,16 @@ public String getFunction() {
211245
"optional_list_first",
212246
"Return the first value in a list if present, otherwise"
213247
+ " optional.none()",
214-
optionalTypeV,
215-
listTypeV)),
248+
OPTIONAL_TYPE_V,
249+
LIST_TYPE_V)),
216250
CelFunctionDecl.newFunctionDeclaration(
217251
LAST.functionName,
218252
CelOverloadDecl.newMemberOverload(
219253
"optional_list_last",
220254
"Return the last value in a list if present, otherwise"
221255
+ " optional.none()",
222-
optionalTypeV,
223-
listTypeV)))
256+
OPTIONAL_TYPE_V,
257+
LIST_TYPE_V)))
224258
.build(),
225259
version1.macros,
226260
version1.variables);

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

Lines changed: 29 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,9 @@ private TranslatedValue translateOperatorCall(
243243
// by our axioms
244244
return TranslatedValue.propagateStrict(ctx, typeSystem, typeSystem.mkError(), args);
245245
case INDEX:
246-
return translateIndex(args, ast);
246+
return translateIndex(args, ast, false);
247+
case OPTIONAL_INDEX:
248+
return translateIndex(args, ast, true);
247249
case CONDITIONAL:
248250
return translateConditional(args, ast);
249251
case NOT_STRICTLY_FALSE:
@@ -600,7 +602,8 @@ private TranslatedValue translateEquality(
600602
.withApproximation(ctx.mkFalse());
601603
}
602604

603-
private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard) {
605+
private Expr<?> buildListIndex(
606+
Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
604607
Expr<?> listRef = typeSystem.getListRef(lhsTrans);
605608
SeqExpr<?> seq = typeSystem.getSeq(listRef);
606609
Expr<?> index = typeSystem.getInt(rhsTrans);
@@ -617,6 +620,14 @@ private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr type
617620
constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotUnknown));
618621
}
619622

623+
if (isOptional) {
624+
Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val);
625+
constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val));
626+
constraintSink.accept(typeSystem.optHasValue(resultOptRef));
627+
return ctx.mkITE(
628+
inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
629+
}
630+
620631
return ctx.mkITE(inBounds, val, typeSystem.mkError());
621632
}
622633

@@ -677,7 +688,8 @@ private ProbeResult createProbeResult(
677688
return new ProbeResult(altInMap, altVal);
678689
}
679690

680-
private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard) {
691+
private Expr<?> buildMapIndex(
692+
Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
681693
Expr<?> mapRef = typeSystem.getMapRef(lhsTrans);
682694
ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
683695
ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
@@ -780,10 +792,19 @@ private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeG
780792
constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotUnknown));
781793
}
782794

795+
if (isOptional) {
796+
Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal);
797+
constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
798+
constraintSink.accept(typeSystem.optHasValue(resultOptRef));
799+
return ctx.mkITE(
800+
finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
801+
}
802+
783803
return ctx.mkITE(finalInMap, finalVal, typeSystem.mkError());
784804
}
785805

786-
private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSyntaxTree ast) {
806+
private TranslatedValue translateIndex(
807+
List<TranslatedValue> args, CelAbstractSyntaxTree ast, boolean isOptional) {
787808
Expr<?> lhsTrans = args.get(0).z3Expr();
788809
Expr<?> rhsTrans = args.get(1).z3Expr();
789810

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

795816
Expr<?> actualValue;
796817
if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) {
797-
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue());
818+
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
798819
constraintSink.accept(
799820
ctx.mkImplies(
800821
ctx.mkNot(typeSystem.isError(actualValue)),
801822
typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType())));
802823
} else if (lhsType.kind() == CelKind.MAP) {
803-
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue());
824+
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
804825
constraintSink.accept(
805826
ctx.mkImplies(
806827
ctx.mkNot(typeSystem.isError(actualValue)),
@@ -810,8 +831,8 @@ private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSy
810831
BoolExpr isMapGuard = typeSystem.isMap(lhsTrans);
811832
actualValue =
812833
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
813-
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard))
814-
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard))
834+
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
835+
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
815836
.build(typeSystem.mkError());
816837
}
817838

0 commit comments

Comments
 (0)