Skip to content

Commit 51ab112

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

4 files changed

Lines changed: 131 additions & 12 deletions

File tree

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

Lines changed: 24 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,7 @@ private TranslatedValue translateEquality(
600602
.withApproximation(ctx.mkFalse());
601603
}
602604

603-
private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard) {
605+
private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
604606
Expr<?> listRef = typeSystem.getListRef(lhsTrans);
605607
SeqExpr<?> seq = typeSystem.getSeq(listRef);
606608
Expr<?> index = typeSystem.getInt(rhsTrans);
@@ -617,6 +619,13 @@ private Expr<?> buildListIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr type
617619
constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotUnknown));
618620
}
619621

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

@@ -677,7 +686,7 @@ private ProbeResult createProbeResult(
677686
return new ProbeResult(altInMap, altVal);
678687
}
679688

680-
private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard) {
689+
private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeGuard, boolean isOptional) {
681690
Expr<?> mapRef = typeSystem.getMapRef(lhsTrans);
682691
ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef);
683692
ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef);
@@ -780,10 +789,17 @@ private Expr<?> buildMapIndex(Expr<?> lhsTrans, Expr<?> rhsTrans, BoolExpr typeG
780789
constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotUnknown));
781790
}
782791

792+
if (isOptional) {
793+
Expr<?> resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal);
794+
constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal));
795+
constraintSink.accept(typeSystem.optHasValue(resultOptRef));
796+
return ctx.mkITE(finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone());
797+
}
798+
783799
return ctx.mkITE(finalInMap, finalVal, typeSystem.mkError());
784800
}
785801

786-
private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSyntaxTree ast) {
802+
private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSyntaxTree ast, boolean isOptional) {
787803
Expr<?> lhsTrans = args.get(0).z3Expr();
788804
Expr<?> rhsTrans = args.get(1).z3Expr();
789805

@@ -794,13 +810,13 @@ private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSy
794810

795811
Expr<?> actualValue;
796812
if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) {
797-
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue());
813+
actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
798814
constraintSink.accept(
799815
ctx.mkImplies(
800816
ctx.mkNot(typeSystem.isError(actualValue)),
801817
typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType())));
802818
} else if (lhsType.kind() == CelKind.MAP) {
803-
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue());
819+
actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional);
804820
constraintSink.accept(
805821
ctx.mkImplies(
806822
ctx.mkNot(typeSystem.isError(actualValue)),
@@ -810,8 +826,8 @@ private TranslatedValue translateIndex(List<TranslatedValue> args, CelAbstractSy
810826
BoolExpr isMapGuard = typeSystem.isMap(lhsTrans);
811827
actualValue =
812828
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
813-
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard))
814-
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard))
829+
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
830+
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
815831
.build(typeSystem.mkError());
816832
}
817833

‎verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ java_library(
1818
"//:auto_value",
1919
"//checker:standard_decl",
2020
"//common:compiler_common",
21+
"//common:operator",
2122
"//common/annotations",
2223
"//common/types",
2324
"//extensions:comprehensions",

‎verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java‎

Lines changed: 71 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,12 +15,16 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.google.common.collect.ImmutableList;
18+
import com.microsoft.z3.ArrayExpr;
1819
import com.microsoft.z3.BoolExpr;
1920
import com.microsoft.z3.Context;
2021
import com.microsoft.z3.Expr;
2122
import com.microsoft.z3.FPExpr;
2223
import com.microsoft.z3.SeqExpr;
2324
import dev.cel.common.CelFunctionDecl;
25+
import dev.cel.common.CelOverloadDecl;
26+
import dev.cel.common.Operator;
27+
import dev.cel.common.types.SimpleType;
2428
import dev.cel.extensions.CelOptionalLibrary;
2529
import dev.cel.extensions.CelOptionalLibrary.Function;
2630
import dev.cel.verifier.CelZ3TypeSystem;
@@ -84,6 +88,67 @@ final class OptionalAxioms {
8488
(ctx, ts, sink, val, other) -> {
8589
Expr<?> optRef = ts.getOptionalRef(val);
8690
return Optional.of(ctx.mkITE(ts.optHasValue(optRef), val, other));
91+
}),
92+
createBinaryAxiom(
93+
CelFunctionDecl.newFunctionDeclaration(
94+
Operator.OPTIONAL_SELECT.getFunction(),
95+
CelOverloadDecl.newGlobalOverload(
96+
"select_optional_field", SimpleType.DYN, SimpleType.DYN, SimpleType.STRING)),
97+
"select_optional_field",
98+
(ctx, ts, sink, operand, field) -> {
99+
Expr<?> optRef = ts.getOptionalRef(operand);
100+
BoolExpr isOpt = ts.isOptional(operand);
101+
BoolExpr hasValue = ts.optHasValue(optRef);
102+
Expr<?> actualOperand = ctx.mkITE(isOpt, ts.getOptionalValue(optRef), operand);
103+
104+
BoolExpr isMap = ts.isMap(actualOperand);
105+
BoolExpr isMsg = ts.isMessage(actualOperand);
106+
BoolExpr isValidTarget = ctx.mkOr(isMap, isMsg);
107+
108+
Expr<?> msgFieldZ3Str = ts.getString(field);
109+
Expr<?> mapFieldCelVal = field;
110+
111+
Expr<?> msgRef = ts.getMessageRef(actualOperand);
112+
Expr<?> mapRef = ts.getMapRef(actualOperand);
113+
114+
Expr<?> presence =
115+
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
116+
.addCase(
117+
isMsg,
118+
ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str))
119+
.addCase(
120+
isMap,
121+
ctx.mkSelect((ArrayExpr) ts.getMapPresence(mapRef), mapFieldCelVal))
122+
.build(ctx.mkFalse());
123+
124+
Expr<?> value =
125+
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
126+
.addCase(
127+
isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str))
128+
.addCase(
129+
isMap,
130+
ctx.mkSelect((ArrayExpr) ts.getMapValues(mapRef), mapFieldCelVal))
131+
.build(ts.mkError());
132+
133+
BoolExpr valNotError = ctx.mkNot(ctx.mkEq(value, ts.mkError()));
134+
BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue());
135+
sink.accept(
136+
ctx.mkImplies(
137+
CelZ3TypeSystem.mkAndFlattened(
138+
ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence),
139+
valNotError));
140+
141+
Expr<?> resultOptRef = ctx.mkApp(ts.optionalOfRefFunc(), value);
142+
sink.accept(ctx.mkEq(ts.getOptionalValue(resultOptRef), value));
143+
sink.accept(ts.optHasValue(resultOptRef));
144+
145+
Expr<?> optionalResult =
146+
ctx.mkITE(
147+
(BoolExpr) presence, ts.mkOptionalOf(resultOptRef), ts.mkOptionalNone());
148+
149+
Expr<?> result = ctx.mkITE(isValidTarget, optionalResult, ts.mkError());
150+
return Optional.of(
151+
ctx.mkITE(ctx.mkAnd(isOpt, ctx.mkNot(hasValue)), ts.mkOptionalNone(), result));
87152
}));
88153

89154
private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr<?> val) {
@@ -130,7 +195,12 @@ private static CelZ3FunctionAxiom createUnaryAxiom(
130195

131196
private static CelZ3FunctionAxiom createBinaryAxiom(
132197
Function funcEnum, String overloadId, CelZ3FunctionAxiom.BinaryTranslator translator) {
133-
return CelZ3FunctionAxiom.newBuilder(getDecl(funcEnum))
198+
return createBinaryAxiom(getDecl(funcEnum), overloadId, translator);
199+
}
200+
201+
private static CelZ3FunctionAxiom createBinaryAxiom(
202+
CelFunctionDecl funcDecl, String overloadId, CelZ3FunctionAxiom.BinaryTranslator translator) {
203+
return CelZ3FunctionAxiom.newBuilder(funcDecl)
134204
.addBinaryOverloadTranslator(overloadId, translator)
135205
.build();
136206
}

‎verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java‎

Lines changed: 35 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1557,7 +1557,39 @@ private enum EquivalenceTestCase {
15571557
OPTIONAL_PRUNE_LIST_EQUALITY("[?optional.none(), 1] == [1]", "true"),
15581558
OPTIONAL_PRUNE_LIST_COMPREHENSION("[1, ?optional.none()].all(x, x > 0)", "true"),
15591559
MAP_COMPREHENSION(
1560-
"{'a': 1, 'b': 2}.exists(k, k == 'a')", "{'a': 1, 'b': 2}.exists(k, k == 'a')");
1560+
"{'a': 1, 'b': 2}.exists(k, k == 'a')", "{'a': 1, 'b': 2}.exists(k, k == 'a')"),
1561+
OPTIONAL_FIELD_SELECTION_HAS_EQUIVALENCE(
1562+
"dyn_map.?field.orValue('default')", "has(dyn_map.field) ? dyn_map.field : 'default'"),
1563+
OPTIONAL_FIELD_SELECTION_MACRO_EQUIVALENCE(
1564+
"dyn_map.?field.hasValue() ? dyn_map.?field.value() : 'default'",
1565+
"has(dyn_map.field) ? dyn_map.field : 'default'"),
1566+
OPTIONAL_FIELD_SELECTION_CHAINED("{\"a\": {\"b\": 42}}.?a.?b", "optional.of(42)"),
1567+
OPTIONAL_INDEX_LIST_PRESENT("[1, 2, 3][?0]", "optional.of(1)"),
1568+
OPTIONAL_INDEX_LIST_MISSING("[1, 2, 3][?5]", "optional.none()"),
1569+
OPTIONAL_INDEX_MAP_MISSING("{'a': 1}[?'missing_key']", "optional.none()"),
1570+
OPTIONAL_FIELD_SELECTION_PROTO3_PRIMITIVE_ZERO(
1571+
"TestAllTypes{single_int32: 0}.?single_int32", "optional.none()"),
1572+
OPTIONAL_FIELD_SELECTION_PROTO3_PRIMITIVE_NONZERO(
1573+
"TestAllTypes{single_int32: 5}.?single_int32", "optional.of(5)"),
1574+
OPTIONAL_FIELD_SELECTION_PROTO3_MESSAGE_EMPTY(
1575+
"TestAllTypes{}.?standalone_message", "optional.none()"),
1576+
OPTIONAL_FIELD_SELECTION_PROTO3_MESSAGE_PRESENT(
1577+
"TestAllTypes{standalone_message:"
1578+
+ " TestAllTypes.NestedMessage{}}.?standalone_message.hasValue()",
1579+
"true"),
1580+
OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_NULL(
1581+
"TestAllTypes{}.?single_int64_wrapper", "optional.none()"),
1582+
OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_PRESENT(
1583+
"TestAllTypes{single_int64_wrapper: null}.?single_int64_wrapper", "optional.none()"),
1584+
OPTIONAL_FIELD_SELECTION_DYNAMIC_MISS(
1585+
"dyn_map == {'a': 1} ? dyn_map.?b : optional.none()", "optional.none()"),
1586+
OPTIONAL_FIELD_SELECTION_TYPE_GUARDING(
1587+
"type(dyn_var) == map ? dyn_var.?key == optional.none() || dyn_var.?key.hasValue() : true",
1588+
"true"),
1589+
OPTIONAL_FIELD_SELECTION_MAP_COMPREHENSION(
1590+
"{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v).?b", "optional.of(2)"),
1591+
OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)");
1592+
15611593
private final String exprA;
15621594
private final String exprB;
15631595

@@ -1961,8 +1993,8 @@ public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws
19611993
CelAbstractSyntaxTree ast =
19621994
customCel
19631995
.compile(
1964-
"d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 == 9429185123491285.0 && d1 > 100000.0 &&"
1965-
+ " d2 > 100000.0 && d3 > 100000.0 && d4 > 100000.0")
1996+
"d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 == 9429185123491285.0 && d1 > 1.0 &&"
1997+
+ " d2 > 1.0 && d3 > 1.0 && d4 > 1.0")
19661998
.getAst();
19671999

19682000
CelVerificationException e =

0 commit comments

Comments
 (0)