Skip to content

Commit 0dabf79

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

7 files changed

Lines changed: 324 additions & 127 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+
// TODO: Remove default keyword by implementing this for all standard overloads
1589+
throw new UnsupportedOperationException("Unimplemented");
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: 130 additions & 77 deletions
Original file line numberDiff line numberDiff line change
@@ -97,95 +97,148 @@ public String getFunction() {
9797
}
9898
}
9999

100+
private static final class Types {
101+
private static final TypeParamType PARAM_TYPE_K = TypeParamType.create("K");
102+
private static final TypeParamType PARAM_TYPE_V = TypeParamType.create("V");
103+
private static final OptionalType OPTIONAL_TYPE_V = OptionalType.create(PARAM_TYPE_V);
104+
private static final ListType LIST_TYPE_V = ListType.create(PARAM_TYPE_V);
105+
private static final MapType MAP_TYPE_KV = MapType.create(PARAM_TYPE_K, PARAM_TYPE_V);
106+
}
107+
108+
/** Declarations for the optional extension library. */
109+
public enum OptionalDeclaration implements CelFunctionDecl.Declarer {
110+
OPTIONAL_OF(
111+
CelFunctionDecl.newFunctionDeclaration(
112+
Function.OPTIONAL_OF.getFunction(),
113+
CelOverloadDecl.newGlobalOverload(
114+
"optional_of", Types.OPTIONAL_TYPE_V, Types.PARAM_TYPE_V))),
115+
OPTIONAL_OF_NON_ZERO_VALUE(
116+
CelFunctionDecl.newFunctionDeclaration(
117+
Function.OPTIONAL_OF_NON_ZERO_VALUE.getFunction(),
118+
CelOverloadDecl.newGlobalOverload(
119+
"optional_ofNonZeroValue", Types.OPTIONAL_TYPE_V, Types.PARAM_TYPE_V))),
120+
OPTIONAL_NONE(
121+
CelFunctionDecl.newFunctionDeclaration(
122+
Function.OPTIONAL_NONE.getFunction(),
123+
CelOverloadDecl.newGlobalOverload("optional_none", Types.OPTIONAL_TYPE_V))),
124+
OPTIONAL_VALUE(
125+
CelFunctionDecl.newFunctionDeclaration(
126+
Function.VALUE.getFunction(),
127+
CelOverloadDecl.newMemberOverload(
128+
"optional_value", Types.PARAM_TYPE_V, Types.OPTIONAL_TYPE_V))),
129+
OPTIONAL_HAS_VALUE(
130+
CelFunctionDecl.newFunctionDeclaration(
131+
Function.HAS_VALUE.getFunction(),
132+
CelOverloadDecl.newMemberOverload(
133+
"optional_hasValue", SimpleType.BOOL, Types.OPTIONAL_TYPE_V))),
134+
OPTIONAL_UNWRAP(
135+
CelFunctionDecl.newFunctionDeclaration(
136+
Function.OPTIONAL_UNWRAP.getFunction(),
137+
CelOverloadDecl.newGlobalOverload(
138+
"optional_unwrap_list",
139+
Types.LIST_TYPE_V,
140+
ListType.create(Types.OPTIONAL_TYPE_V)))),
141+
OPTIONAL_OR(
142+
CelFunctionDecl.newFunctionDeclaration(
143+
"or",
144+
CelOverloadDecl.newMemberOverload(
145+
"optional_or_optional",
146+
Types.OPTIONAL_TYPE_V,
147+
Types.OPTIONAL_TYPE_V,
148+
Types.OPTIONAL_TYPE_V))),
149+
OPTIONAL_OR_VALUE(
150+
CelFunctionDecl.newFunctionDeclaration(
151+
"orValue",
152+
CelOverloadDecl.newMemberOverload(
153+
"optional_orValue_value",
154+
Types.PARAM_TYPE_V,
155+
Types.OPTIONAL_TYPE_V,
156+
Types.PARAM_TYPE_V))),
157+
OPTIONAL_SELECT(
158+
CelFunctionDecl.newFunctionDeclaration(
159+
Operator.OPTIONAL_SELECT.getFunction(),
160+
CelOverloadDecl.newGlobalOverload(
161+
"select_optional_field",
162+
Types.OPTIONAL_TYPE_V,
163+
SimpleType.DYN,
164+
SimpleType.STRING))),
165+
OPTIONAL_INDEX(
166+
CelFunctionDecl.newFunctionDeclaration(
167+
Operator.OPTIONAL_INDEX.getFunction(),
168+
CelOverloadDecl.newGlobalOverload(
169+
"list_optindex_optional_int",
170+
Types.OPTIONAL_TYPE_V,
171+
Types.LIST_TYPE_V,
172+
SimpleType.INT),
173+
CelOverloadDecl.newGlobalOverload(
174+
"optional_list_optindex_optional_int",
175+
Types.OPTIONAL_TYPE_V,
176+
OptionalType.create(Types.LIST_TYPE_V),
177+
SimpleType.INT),
178+
CelOverloadDecl.newGlobalOverload(
179+
"map_optindex_optional_value",
180+
Types.OPTIONAL_TYPE_V,
181+
Types.MAP_TYPE_KV,
182+
Types.PARAM_TYPE_K),
183+
CelOverloadDecl.newGlobalOverload(
184+
"optional_map_optindex_optional_value",
185+
Types.OPTIONAL_TYPE_V,
186+
OptionalType.create(Types.MAP_TYPE_KV),
187+
Types.PARAM_TYPE_K))),
188+
OPTIONAL_INDEX_OPERAND(
189+
CelFunctionDecl.newFunctionDeclaration(
190+
Operator.INDEX.getFunction(),
191+
CelOverloadDecl.newGlobalOverload(
192+
"optional_list_index_int",
193+
Types.OPTIONAL_TYPE_V,
194+
OptionalType.create(Types.LIST_TYPE_V),
195+
SimpleType.INT),
196+
CelOverloadDecl.newGlobalOverload(
197+
"optional_map_index_value",
198+
Types.OPTIONAL_TYPE_V,
199+
OptionalType.create(Types.MAP_TYPE_KV),
200+
Types.PARAM_TYPE_K)));
201+
202+
private final CelFunctionDecl celFunctionDecl;
203+
204+
OptionalDeclaration(CelFunctionDecl celFunctionDecl) {
205+
this.celFunctionDecl = celFunctionDecl;
206+
}
207+
208+
@Override
209+
public CelFunctionDecl functionDecl() {
210+
return celFunctionDecl;
211+
}
212+
}
213+
100214
private static final CelExtensionLibrary<CelOptionalLibrary> LIBRARY =
101215
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-
108216
private final CelOptionalLibrary version0 =
109217
new CelOptionalLibrary(
110218
0,
111219
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))),
220+
OptionalDeclaration.OPTIONAL_OF.functionDecl(),
221+
OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE.functionDecl(),
222+
OptionalDeclaration.OPTIONAL_NONE.functionDecl(),
223+
OptionalDeclaration.OPTIONAL_VALUE.functionDecl(),
224+
OptionalDeclaration.OPTIONAL_HAS_VALUE.functionDecl(),
225+
OptionalDeclaration.OPTIONAL_UNWRAP.functionDecl(),
135226
// Note: Implementation of "or" and "orValue" are special-cased inside the
136227
// 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)),
228+
OptionalDeclaration.OPTIONAL_OR.functionDecl(),
229+
OptionalDeclaration.OPTIONAL_OR_VALUE.functionDecl(),
145230
// Note: Function bindings for optional field selection and indexer is defined
146231
// 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)),
232+
OptionalDeclaration.OPTIONAL_SELECT.functionDecl(),
233+
OptionalDeclaration.OPTIONAL_INDEX.functionDecl(),
170234
// 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))),
235+
OptionalDeclaration.OPTIONAL_INDEX_OPERAND.functionDecl()),
183236
ImmutableSet.of(
184237
CelMacro.newReceiverMacro("optMap", 2, CelOptionalLibrary::expandOptMap)),
185238
ImmutableSet.of(
186239
// Type declaration for optional_type -> type(optional_type(V))
187240
CelVarDecl.newVarDeclaration(
188-
OptionalType.NAME, TypeType.create(optionalTypeV))));
241+
OptionalType.NAME, TypeType.create(Types.OPTIONAL_TYPE_V))));
189242

190243
private final CelOptionalLibrary version1 =
191244
new CelOptionalLibrary(
@@ -211,16 +264,16 @@ public String getFunction() {
211264
"optional_list_first",
212265
"Return the first value in a list if present, otherwise"
213266
+ " optional.none()",
214-
optionalTypeV,
215-
listTypeV)),
267+
Types.OPTIONAL_TYPE_V,
268+
Types.LIST_TYPE_V)),
216269
CelFunctionDecl.newFunctionDeclaration(
217270
LAST.functionName,
218271
CelOverloadDecl.newMemberOverload(
219272
"optional_list_last",
220273
"Return the last value in a list if present, otherwise"
221274
+ " optional.none()",
222-
optionalTypeV,
223-
listTypeV)))
275+
Types.OPTIONAL_TYPE_V,
276+
Types.LIST_TYPE_V)))
224277
.build(),
225278
version1.macros,
226279
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)