Skip to content

Commit 1dccf2f

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Add type constraints to uninterpreted conversions
PiperOrigin-RevId: 957417703
1 parent eb6fc20 commit 1dccf2f

2 files changed

Lines changed: 53 additions & 60 deletions

File tree

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

Lines changed: 29 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -45,11 +45,11 @@ final class TypeConversionAxioms {
4545
.addUnaryOverloadTranslator(
4646
Conversions.DOUBLE_TO_INT64.celOverloadDecl(),
4747
createUninterpretedConversion(Conversions.DOUBLE_TO_INT64),
48-
true)
48+
/* isApproximated= */ true)
4949
.addUnaryOverloadTranslator(
5050
Conversions.STRING_TO_INT64.celOverloadDecl(),
5151
createUninterpretedConversion(Conversions.STRING_TO_INT64),
52-
true)
52+
/* isApproximated= */ true)
5353
.addUnaryOverloadTranslator(
5454
Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(),
5555
(ctx, typeSystem, sink, arg) ->
@@ -72,11 +72,11 @@ final class TypeConversionAxioms {
7272
.addUnaryOverloadTranslator(
7373
Conversions.DOUBLE_TO_UINT64.celOverloadDecl(),
7474
createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64),
75-
true)
75+
/* isApproximated= */ true)
7676
.addUnaryOverloadTranslator(
7777
Conversions.STRING_TO_UINT64.celOverloadDecl(),
7878
createUninterpretedConversion(Conversions.STRING_TO_UINT64),
79-
true)
79+
/* isApproximated= */ true)
8080
.build();
8181

8282
private static final CelZ3FunctionAxiom DOUBLE_AXIOM =
@@ -87,14 +87,15 @@ final class TypeConversionAxioms {
8787
.addUnaryOverloadTranslator(
8888
Conversions.INT64_TO_DOUBLE.celOverloadDecl(),
8989
createUninterpretedConversion(Conversions.INT64_TO_DOUBLE),
90-
true)
90+
/* isApproximated= */ true)
9191
.addUnaryOverloadTranslator(
9292
Conversions.UINT64_TO_DOUBLE.celOverloadDecl(),
9393
createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE),
94-
true)
94+
/* isApproximated= */ true)
9595
.addUnaryOverloadTranslator(
9696
Conversions.STRING_TO_DOUBLE.celOverloadDecl(),
97-
createUninterpretedConversion(Conversions.STRING_TO_DOUBLE))
97+
createUninterpretedConversion(Conversions.STRING_TO_DOUBLE),
98+
/* isApproximated= */ true)
9899
.build();
99100

100101
private static final CelZ3FunctionAxiom STRING_AXIOM =
@@ -105,31 +106,31 @@ final class TypeConversionAxioms {
105106
.addUnaryOverloadTranslator(
106107
Conversions.INT64_TO_STRING.celOverloadDecl(),
107108
createUninterpretedConversion(Conversions.INT64_TO_STRING),
108-
true)
109+
/* isApproximated= */ true)
109110
.addUnaryOverloadTranslator(
110111
Conversions.UINT64_TO_STRING.celOverloadDecl(),
111112
createUninterpretedConversion(Conversions.UINT64_TO_STRING),
112-
true)
113+
/* isApproximated= */ true)
113114
.addUnaryOverloadTranslator(
114115
Conversions.DOUBLE_TO_STRING.celOverloadDecl(),
115116
createUninterpretedConversion(Conversions.DOUBLE_TO_STRING),
116-
true)
117+
/* isApproximated= */ true)
117118
.addUnaryOverloadTranslator(
118119
Conversions.BOOL_TO_STRING.celOverloadDecl(),
119120
createUninterpretedConversion(Conversions.BOOL_TO_STRING),
120-
true)
121+
/* isApproximated= */ true)
121122
.addUnaryOverloadTranslator(
122123
Conversions.BYTES_TO_STRING.celOverloadDecl(),
123124
createUninterpretedConversion(Conversions.BYTES_TO_STRING),
124-
true)
125+
/* isApproximated= */ true)
125126
.addUnaryOverloadTranslator(
126127
Conversions.TIMESTAMP_TO_STRING.celOverloadDecl(),
127128
createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING),
128-
true)
129+
/* isApproximated= */ true)
129130
.addUnaryOverloadTranslator(
130131
Conversions.DURATION_TO_STRING.celOverloadDecl(),
131132
createUninterpretedConversion(Conversions.DURATION_TO_STRING),
132-
true)
133+
/* isApproximated= */ true)
133134
.build();
134135

135136
private static final CelZ3FunctionAxiom BYTES_AXIOM =
@@ -140,7 +141,7 @@ final class TypeConversionAxioms {
140141
.addUnaryOverloadTranslator(
141142
Conversions.STRING_TO_BYTES.celOverloadDecl(),
142143
createUninterpretedConversion(Conversions.STRING_TO_BYTES),
143-
true)
144+
/* isApproximated= */ true)
144145
.build();
145146

146147
private static final CelZ3FunctionAxiom DYN_AXIOM =
@@ -158,7 +159,7 @@ final class TypeConversionAxioms {
158159
.addUnaryOverloadTranslator(
159160
Conversions.STRING_TO_DURATION.celOverloadDecl(),
160161
createUninterpretedConversion(Conversions.STRING_TO_DURATION),
161-
true)
162+
/* isApproximated= */ true)
162163
.build();
163164

164165
private static final CelZ3FunctionAxiom TIMESTAMP_AXIOM =
@@ -169,7 +170,7 @@ final class TypeConversionAxioms {
169170
.addUnaryOverloadTranslator(
170171
Conversions.STRING_TO_TIMESTAMP.celOverloadDecl(),
171172
createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP),
172-
true)
173+
/* isApproximated= */ true)
173174
.addUnaryOverloadTranslator(
174175
Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(),
175176
(ctx, typeSystem, sink, arg) -> {
@@ -188,7 +189,7 @@ final class TypeConversionAxioms {
188189
.addUnaryOverloadTranslator(
189190
Conversions.STRING_TO_BOOL.celOverloadDecl(),
190191
createUninterpretedConversion(Conversions.STRING_TO_BOOL),
191-
true)
192+
/* isApproximated= */ true)
192193
.build();
193194

194195
static final ImmutableList<CelZ3FunctionAxiom> ALL_AXIOMS =
@@ -213,56 +214,53 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion(
213214
typeSystem.celValueSort());
214215
Expr<?> res = ctx.mkApp(funcDecl, arg);
215216

217+
BoolExpr isValid;
216218
switch (conversion.celOverloadDecl().resultType().kind()) {
217219
case INT:
218-
BoolExpr intValid =
220+
isValid =
219221
ctx.mkAnd(
220222
typeSystem.isInt(res),
221223
ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res))));
222-
sink.accept(intValid);
223224
break;
224225
case TIMESTAMP:
225-
BoolExpr timestampValid =
226+
isValid =
226227
ctx.mkAnd(
227228
typeSystem.isTimestamp(res),
228229
ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res))));
229-
sink.accept(timestampValid);
230230
break;
231231
case DURATION:
232-
BoolExpr durationValid =
232+
isValid =
233233
ctx.mkAnd(
234234
typeSystem.isDuration(res),
235235
ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res))));
236-
sink.accept(durationValid);
237236
break;
238237
case UINT:
239-
BoolExpr uintValid =
238+
isValid =
240239
ctx.mkAnd(
241240
typeSystem.isUint(res),
242241
ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res))));
243-
sink.accept(uintValid);
244242
break;
245243
case DOUBLE:
246-
BoolExpr doubleValid =
244+
isValid =
247245
ctx.mkAnd(
248246
typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res))));
249-
sink.accept(doubleValid);
250247
break;
251248
case STRING:
252-
sink.accept(typeSystem.isString(res));
249+
isValid = typeSystem.isString(res);
253250
break;
254251
case BYTES:
255-
sink.accept(typeSystem.isBytes(res));
252+
isValid = typeSystem.isBytes(res);
256253
break;
257254
case BOOL:
258-
sink.accept(typeSystem.isBool(res));
255+
isValid = typeSystem.isBool(res);
259256
break;
260257
default:
261258
throw new IllegalArgumentException(
262259
"Unsupported uninterpreted conversion result type: "
263260
+ conversion.celOverloadDecl().resultType());
264261
}
265262

263+
sink.accept(ctx.mkOr(isValid, typeSystem.isError(res)));
266264
return Optional.of(res);
267265
};
268266
}

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

Lines changed: 24 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -93,6 +93,7 @@ public final class CelVerifierZ3ImplTest {
9393
.addVar("b", SimpleType.BOOL)
9494
.addVar("role", SimpleType.STRING)
9595
.addVar("country", SimpleType.STRING)
96+
.addVar("string_var", SimpleType.STRING)
9697
.addVar("port", SimpleType.INT)
9798
.addVar("dur", SimpleType.DURATION)
9899
.addVar("ts", SimpleType.TIMESTAMP)
@@ -325,13 +326,6 @@ public void isSatisfiable_timeout_throwsException() throws Exception {
325326

326327
private enum IsAlwaysTrueTestCase {
327328
LOGICAL_OR_CONSTANTS("true || false"),
328-
DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION(
329-
"type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :"
330-
+ " true"),
331-
TIMESTAMP_STRING_CONVERSION_VALID(
332-
"timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"),
333-
DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"),
334-
TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"),
335329
TIMESTAMP_GREATER_EQUALS("timestamp(200) >= timestamp(100)"),
336330
DURATION_GREATER_EQUALS(
337331
"(timestamp(200) - timestamp(100)) >= (timestamp(150) - timestamp(100))"),
@@ -675,29 +669,7 @@ private enum IsAlwaysTrueTestCase {
675669
TYPE_CONVERSION_DYN_IDENTITY("dyn(1) == 1"),
676670
TYPE_CONVERSION_UINT_TO_INT("int(1u) == 1"),
677671
TYPE_CONVERSION_INT_TO_UINT("uint(1) == 1u"),
678-
TYPE_CONVERSION_INT_FROM_DOUBLE("int(1.0) == int(1.0)"),
679-
TYPE_CONVERSION_INT_FROM_STRING("int('1') == int('1')"),
680-
TYPE_CONVERSION_INT_FROM_TIMESTAMP(
681-
"int(timestamp('1970-01-01T00:00:00Z')) == int(timestamp('1970-01-01T00:00:00Z'))"),
682-
TYPE_CONVERSION_UINT_FROM_DOUBLE("uint(1.0) == uint(1.0)"),
683-
TYPE_CONVERSION_UINT_FROM_STRING("uint('1') == uint('1')"),
684-
TYPE_CONVERSION_DOUBLE_FROM_INT("double(1) == double(1)"),
685-
TYPE_CONVERSION_DOUBLE_FROM_UINT("double(1u) == double(1u)"),
686-
TYPE_CONVERSION_DOUBLE_FROM_STRING("double('1.0') == double('1.0')"),
687-
TYPE_CONVERSION_STRING_FROM_INT("string(1) == string(1)"),
688-
TYPE_CONVERSION_STRING_FROM_UINT("string(1u) == string(1u)"),
689-
TYPE_CONVERSION_STRING_FROM_DOUBLE("string(1.0) == string(1.0)"),
690-
TYPE_CONVERSION_STRING_FROM_BOOL("string(true) == string(true)"),
691-
TYPE_CONVERSION_STRING_FROM_BYTES("string(b'foo') == string(b'foo')"),
692-
TYPE_CONVERSION_STRING_FROM_TIMESTAMP(
693-
"string(timestamp('1970-01-01T00:00:00Z')) == string(timestamp('1970-01-01T00:00:00Z'))"),
694-
TYPE_CONVERSION_STRING_FROM_DURATION("string(duration('1s')) == string(duration('1s'))"),
695-
TYPE_CONVERSION_BYTES_FROM_STRING("bytes('foo') == bytes('foo')"),
696-
TYPE_CONVERSION_DURATION_FROM_STRING("duration('1s') == duration('1s')"),
697-
TYPE_CONVERSION_TIMESTAMP_FROM_STRING(
698-
"timestamp('1970-01-01T00:00:00Z') == timestamp('1970-01-01T00:00:00Z')"),
699672
TYPE_CONVERSION_TIMESTAMP_FROM_INT("timestamp(1) == timestamp(1)"),
700-
TYPE_CONVERSION_BOOL_FROM_STRING("bool('true') == bool('true')"),
701673
TYPE_CONVERSION_INT_TO_UINT_ZERO("uint(0) == 0u"),
702674

703675
TYPE_AXIOM_OPTIONAL("type(optional.of(1)) == optional_type"),
@@ -1369,6 +1341,24 @@ private enum IsAlwaysTrueViolationTestCase {
13691341
"Counterexample input:",
13701342
"x = -9223372036854775808",
13711343
"y = -1"),
1344+
UNINTERPRETED_CONVERSION_CAN_ERROR_INT_FROM_STRING(
1345+
"int(string_var) == int(string_var)",
1346+
"Condition is not always true\\.",
1347+
"Counterexample input:"),
1348+
UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP_FROM_STRING(
1349+
"timestamp(string_var) == timestamp(string_var)",
1350+
"Condition is not always true\\.",
1351+
"Counterexample input:"),
1352+
UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION_FROM_STRING(
1353+
"duration(string_var) == duration(string_var)",
1354+
"Condition is not always true\\.",
1355+
"Counterexample input:"),
1356+
// TODO: Implement RFC 3339 spec in conversion
1357+
TIMESTAMP_STRING_CONVERSION_VALID(
1358+
"timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')",
1359+
"Condition is not always true\\."),
1360+
DURATION_STRING_CONVERSION_VALID(
1361+
"duration('100s') == duration('100s')", "Condition is not always true\\."),
13721362
;
13731363

13741364
final String expr;
@@ -1395,6 +1385,11 @@ public void isAlwaysTrue_violation_returnsFalse(
13951385

13961386
private enum IsInconclusiveTestCase {
13971387
TIMESTAMP_ADD_DURATION_OVERFLOW("timestamp(253402300799) + duration('100s') > timestamp(0)"),
1388+
DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION(
1389+
"type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :"
1390+
+ " true"),
1391+
// TODO: Implement RFC 3339 spec in conversion
1392+
TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"),
13981393
UNINTERPRETED_FUNCTION("request.matches('^[a-z]+$')"),
13991394
INT_STRING_UNINTERPRETED("int('123') == 123"),
14001395
LIST_WITH_APPROXIMATE_ELEMENT("[request.matches('a')]"),

0 commit comments

Comments
 (0)