Skip to content

Commit 0b9ee2f

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Mark uninterpreted conversions with literals as approximate
PiperOrigin-RevId: 957420089
1 parent 1dccf2f commit 0b9ee2f

5 files changed

Lines changed: 119 additions & 88 deletions

File tree

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -741,8 +741,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
741741
typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
742742
typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
743743

744+
boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true);
745+
BoolExpr isApprox = ctx.mkBool(!isDynamic);
744746
return TranslatedValue.propagateStrict(
745-
ctx, typeSystem, callRes, Optional.of(expr), ctx.mkTrue(), args);
747+
ctx, typeSystem, callRes, Optional.of(expr), isApprox, args);
746748
});
747749
}
748750

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -594,7 +594,8 @@ private TranslatedValue translateEquality(
594594
// because X == X is a tautology (or propagates errors/unknowns exactly).
595595
if (z3Arg0.equals(z3Arg1)) {
596596
Expr<?> finalResult = typeSystem.propagateErrorAndUnknown(equalityExpr, z3Arg0);
597-
return TranslatedValue.create(finalResult, typeSystem, ctx.mkFalse());
597+
return TranslatedValue.create(
598+
finalResult, typeSystem, ctx.mkOr(arg0.isApproximate(), arg1.isApproximate()));
598599
}
599600

600601
return TranslatedValue.propagateStrict(ctx, typeSystem, equalityExpr, arg0, arg1)

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

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,7 @@
2626
import com.microsoft.z3.DatatypeSort;
2727
import com.microsoft.z3.Expr;
2828
import com.microsoft.z3.FPExpr;
29+
import com.microsoft.z3.FPNum;
2930
import com.microsoft.z3.FuncDecl;
3031
import com.microsoft.z3.IntExpr;
3132
import com.microsoft.z3.SeqExpr;
@@ -280,6 +281,35 @@ Constructor optionalCons() {
280281
return optionalCons;
281282
}
282283

284+
/**
285+
* Checks if the given CelValue expression represents a statically known primitive constant.
286+
*
287+
* <p>This is useful for determining whether an uninterpreted function's result should be treated
288+
* as an approximation. If the argument is a known constant, any resulting error is an
289+
* approximation (e.g., parsing a literal string). If it's a variable, the error is an exact
290+
* runtime failure.
291+
*/
292+
public boolean isPrimitiveConstant(Expr<?> expr) {
293+
if (!expr.isApp()) {
294+
return false;
295+
}
296+
FuncDecl<?> decl = expr.getFuncDecl();
297+
if (decl.equals(stringCons.ConstructorDecl()) || decl.equals(bytesCons.ConstructorDecl())) {
298+
return expr.getArgs()[0].isString();
299+
} else if (decl.equals(intCons.ConstructorDecl())
300+
|| decl.equals(uintCons.ConstructorDecl())
301+
|| decl.equals(timestampCons.ConstructorDecl())
302+
|| decl.equals(durationCons.ConstructorDecl())) {
303+
return expr.getArgs()[0].isNumeral();
304+
} else if (decl.equals(doubleCons.ConstructorDecl())) {
305+
return expr.getArgs()[0] instanceof FPNum;
306+
} else if (decl.equals(boolCons.ConstructorDecl())) {
307+
Expr<?> inner = expr.getArgs()[0];
308+
return inner.isTrue() || inner.isFalse();
309+
}
310+
return false;
311+
}
312+
283313
/** Creates a CelValue containing a boolean. */
284314
public Expr<?> mkBool(boolean val) {
285315
return ctx.mkApp(boolCons.ConstructorDecl(), ctx.mkBool(val));

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

Lines changed: 75 additions & 78 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,13 @@
1919
import com.google.common.collect.ImmutableList;
2020
import com.microsoft.z3.BoolExpr;
2121
import com.microsoft.z3.Expr;
22+
import com.microsoft.z3.FPExpr;
2223
import com.microsoft.z3.FuncDecl;
2324
import com.microsoft.z3.IntExpr;
2425
import com.microsoft.z3.Sort;
2526
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2627
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions;
28+
import dev.cel.common.types.SimpleType;
2729
import java.util.Optional;
2830

2931
/** Axiomatization for CEL's type conversion functions. */
@@ -42,14 +44,12 @@ final class TypeConversionAxioms {
4244
return Optional.of(
4345
typeSystem.withRuntimeError(typeSystem.wrapInt(uintVal), outOfBounds));
4446
})
45-
.addUnaryOverloadTranslator(
47+
.addOverloadTranslator(
4648
Conversions.DOUBLE_TO_INT64.celOverloadDecl(),
47-
createUninterpretedConversion(Conversions.DOUBLE_TO_INT64),
48-
/* isApproximated= */ true)
49-
.addUnaryOverloadTranslator(
49+
createUninterpretedConversion(Conversions.DOUBLE_TO_INT64))
50+
.addOverloadTranslator(
5051
Conversions.STRING_TO_INT64.celOverloadDecl(),
51-
createUninterpretedConversion(Conversions.STRING_TO_INT64),
52-
/* isApproximated= */ true)
52+
createUninterpretedConversion(Conversions.STRING_TO_INT64))
5353
.addUnaryOverloadTranslator(
5454
Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(),
5555
(ctx, typeSystem, sink, arg) ->
@@ -69,79 +69,66 @@ final class TypeConversionAxioms {
6969
return Optional.of(
7070
typeSystem.withRuntimeError(typeSystem.wrapUint(intVal), outOfBounds));
7171
})
72-
.addUnaryOverloadTranslator(
72+
.addOverloadTranslator(
7373
Conversions.DOUBLE_TO_UINT64.celOverloadDecl(),
74-
createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64),
75-
/* isApproximated= */ true)
76-
.addUnaryOverloadTranslator(
74+
createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64))
75+
.addOverloadTranslator(
7776
Conversions.STRING_TO_UINT64.celOverloadDecl(),
78-
createUninterpretedConversion(Conversions.STRING_TO_UINT64),
79-
/* isApproximated= */ true)
77+
createUninterpretedConversion(Conversions.STRING_TO_UINT64))
8078
.build();
8179

8280
private static final CelZ3FunctionAxiom DOUBLE_AXIOM =
8381
CelZ3FunctionAxiom.newBuilder(StandardFunction.DOUBLE.functionDecl())
8482
.addUnaryOverloadTranslator(
8583
Conversions.DOUBLE_TO_DOUBLE.celOverloadDecl(),
8684
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
87-
.addUnaryOverloadTranslator(
85+
.addOverloadTranslator(
8886
Conversions.INT64_TO_DOUBLE.celOverloadDecl(),
89-
createUninterpretedConversion(Conversions.INT64_TO_DOUBLE),
90-
/* isApproximated= */ true)
91-
.addUnaryOverloadTranslator(
87+
createUninterpretedConversion(Conversions.INT64_TO_DOUBLE))
88+
.addOverloadTranslator(
9289
Conversions.UINT64_TO_DOUBLE.celOverloadDecl(),
93-
createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE),
94-
/* isApproximated= */ true)
95-
.addUnaryOverloadTranslator(
90+
createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE))
91+
.addOverloadTranslator(
9692
Conversions.STRING_TO_DOUBLE.celOverloadDecl(),
97-
createUninterpretedConversion(Conversions.STRING_TO_DOUBLE),
98-
/* isApproximated= */ true)
93+
createUninterpretedConversion(Conversions.STRING_TO_DOUBLE))
9994
.build();
10095

10196
private static final CelZ3FunctionAxiom STRING_AXIOM =
10297
CelZ3FunctionAxiom.newBuilder(StandardFunction.STRING.functionDecl())
10398
.addUnaryOverloadTranslator(
10499
Conversions.STRING_TO_STRING.celOverloadDecl(),
105100
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
106-
.addUnaryOverloadTranslator(
101+
.addOverloadTranslator(
107102
Conversions.INT64_TO_STRING.celOverloadDecl(),
108-
createUninterpretedConversion(Conversions.INT64_TO_STRING),
109-
/* isApproximated= */ true)
110-
.addUnaryOverloadTranslator(
103+
createUninterpretedConversion(Conversions.INT64_TO_STRING))
104+
.addOverloadTranslator(
111105
Conversions.UINT64_TO_STRING.celOverloadDecl(),
112-
createUninterpretedConversion(Conversions.UINT64_TO_STRING),
113-
/* isApproximated= */ true)
114-
.addUnaryOverloadTranslator(
106+
createUninterpretedConversion(Conversions.UINT64_TO_STRING))
107+
.addOverloadTranslator(
115108
Conversions.DOUBLE_TO_STRING.celOverloadDecl(),
116-
createUninterpretedConversion(Conversions.DOUBLE_TO_STRING),
117-
/* isApproximated= */ true)
118-
.addUnaryOverloadTranslator(
109+
createUninterpretedConversion(Conversions.DOUBLE_TO_STRING))
110+
.addOverloadTranslator(
119111
Conversions.BOOL_TO_STRING.celOverloadDecl(),
120-
createUninterpretedConversion(Conversions.BOOL_TO_STRING),
121-
/* isApproximated= */ true)
122-
.addUnaryOverloadTranslator(
112+
createUninterpretedConversion(Conversions.BOOL_TO_STRING))
113+
.addOverloadTranslator(
123114
Conversions.BYTES_TO_STRING.celOverloadDecl(),
124-
createUninterpretedConversion(Conversions.BYTES_TO_STRING),
125-
/* isApproximated= */ true)
126-
.addUnaryOverloadTranslator(
115+
createUninterpretedConversion(Conversions.BYTES_TO_STRING))
116+
.addOverloadTranslator(
127117
Conversions.TIMESTAMP_TO_STRING.celOverloadDecl(),
128-
createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING),
129-
/* isApproximated= */ true)
130-
.addUnaryOverloadTranslator(
118+
createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING))
119+
.addOverloadTranslator(
131120
Conversions.DURATION_TO_STRING.celOverloadDecl(),
132-
createUninterpretedConversion(Conversions.DURATION_TO_STRING),
133-
/* isApproximated= */ true)
121+
createUninterpretedConversion(Conversions.DURATION_TO_STRING))
134122
.build();
135123

136124
private static final CelZ3FunctionAxiom BYTES_AXIOM =
137125
CelZ3FunctionAxiom.newBuilder(StandardFunction.BYTES.functionDecl())
138126
.addUnaryOverloadTranslator(
139127
Conversions.BYTES_TO_BYTES.celOverloadDecl(),
140128
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
141-
.addUnaryOverloadTranslator(
129+
.addOverloadTranslator(
142130
Conversions.STRING_TO_BYTES.celOverloadDecl(),
143-
createUninterpretedConversion(Conversions.STRING_TO_BYTES),
144-
/* isApproximated= */ true)
131+
createUninterpretedConversion(Conversions.STRING_TO_BYTES))
145132
.build();
146133

147134
private static final CelZ3FunctionAxiom DYN_AXIOM =
@@ -156,21 +143,19 @@ final class TypeConversionAxioms {
156143
.addUnaryOverloadTranslator(
157144
Conversions.DURATION_TO_DURATION.celOverloadDecl(),
158145
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
159-
.addUnaryOverloadTranslator(
146+
.addOverloadTranslator(
160147
Conversions.STRING_TO_DURATION.celOverloadDecl(),
161-
createUninterpretedConversion(Conversions.STRING_TO_DURATION),
162-
/* isApproximated= */ true)
148+
createUninterpretedConversion(Conversions.STRING_TO_DURATION))
163149
.build();
164150

165151
private static final CelZ3FunctionAxiom TIMESTAMP_AXIOM =
166152
CelZ3FunctionAxiom.newBuilder(StandardFunction.TIMESTAMP.functionDecl())
167153
.addUnaryOverloadTranslator(
168154
Conversions.TIMESTAMP_TO_TIMESTAMP.celOverloadDecl(),
169155
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
170-
.addUnaryOverloadTranslator(
156+
.addOverloadTranslator(
171157
Conversions.STRING_TO_TIMESTAMP.celOverloadDecl(),
172-
createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP),
173-
/* isApproximated= */ true)
158+
createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP))
174159
.addUnaryOverloadTranslator(
175160
Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(),
176161
(ctx, typeSystem, sink, arg) -> {
@@ -186,10 +171,9 @@ final class TypeConversionAxioms {
186171
.addUnaryOverloadTranslator(
187172
Conversions.BOOL_TO_BOOL.celOverloadDecl(),
188173
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
189-
.addUnaryOverloadTranslator(
174+
.addOverloadTranslator(
190175
Conversions.STRING_TO_BOOL.celOverloadDecl(),
191-
createUninterpretedConversion(Conversions.STRING_TO_BOOL),
192-
/* isApproximated= */ true)
176+
createUninterpretedConversion(Conversions.STRING_TO_BOOL))
193177
.build();
194178

195179
static final ImmutableList<CelZ3FunctionAxiom> ALL_AXIOMS =
@@ -204,64 +188,77 @@ final class TypeConversionAxioms {
204188
TIMESTAMP_AXIOM,
205189
BOOL_AXIOM);
206190

207-
private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion(
208-
Conversions conversion) {
209-
return (ctx, typeSystem, sink, arg) -> {
191+
private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions conversion) {
192+
return (ctx, typeSystem, sink, unwrappedArgs, argApproximations) -> {
193+
Expr<?> arg = unwrappedArgs.get(0);
194+
BoolExpr baseApprox = argApproximations.get(0);
195+
210196
FuncDecl<?> funcDecl =
211197
typeSystem.internFuncDecl(
212198
conversion.celOverloadDecl().overloadId(),
213199
new Sort[] {typeSystem.celValueSort()},
214200
typeSystem.celValueSort());
215201
Expr<?> res = ctx.mkApp(funcDecl, arg);
216202

217-
BoolExpr isValid;
218203
switch (conversion.celOverloadDecl().resultType().kind()) {
219204
case INT:
220-
isValid =
221-
ctx.mkAnd(
205+
sink.accept(ctx.mkOr(typeSystem.isInt(res), typeSystem.isError(res)));
206+
sink.accept(
207+
ctx.mkImplies(
222208
typeSystem.isInt(res),
223-
ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res))));
209+
ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))));
224210
break;
225211
case TIMESTAMP:
226-
isValid =
227-
ctx.mkAnd(
212+
sink.accept(ctx.mkOr(typeSystem.isTimestamp(res), typeSystem.isError(res)));
213+
sink.accept(
214+
ctx.mkImplies(
228215
typeSystem.isTimestamp(res),
229-
ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res))));
216+
ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res)))));
230217
break;
231218
case DURATION:
232-
isValid =
233-
ctx.mkAnd(
219+
sink.accept(ctx.mkOr(typeSystem.isDuration(res), typeSystem.isError(res)));
220+
sink.accept(
221+
ctx.mkImplies(
234222
typeSystem.isDuration(res),
235-
ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res))));
223+
ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res)))));
236224
break;
237225
case UINT:
238-
isValid =
239-
ctx.mkAnd(
226+
sink.accept(ctx.mkOr(typeSystem.isUint(res), typeSystem.isError(res)));
227+
sink.accept(
228+
ctx.mkImplies(
240229
typeSystem.isUint(res),
241-
ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res))));
230+
ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))));
242231
break;
243232
case DOUBLE:
244-
isValid =
245-
ctx.mkAnd(
246-
typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res))));
233+
sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res)));
234+
sink.accept(
235+
ctx.mkImplies(
236+
typeSystem.isDouble(res),
237+
ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res)))));
247238
break;
248239
case STRING:
249-
isValid = typeSystem.isString(res);
240+
sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res)));
250241
break;
251242
case BYTES:
252-
isValid = typeSystem.isBytes(res);
243+
sink.accept(ctx.mkOr(typeSystem.isBytes(res), typeSystem.isError(res)));
253244
break;
254245
case BOOL:
255-
isValid = typeSystem.isBool(res);
246+
sink.accept(ctx.mkOr(typeSystem.isBool(res), typeSystem.isError(res)));
256247
break;
257248
default:
258249
throw new IllegalArgumentException(
259250
"Unsupported uninterpreted conversion result type: "
260251
+ conversion.celOverloadDecl().resultType());
261252
}
262253

263-
sink.accept(ctx.mkOr(isValid, typeSystem.isError(res)));
264-
return Optional.of(res);
254+
boolean isArgConstant = typeSystem.isPrimitiveConstant(arg);
255+
boolean isStringParseConversion =
256+
conversion.celOverloadDecl().parameterTypes().get(0).equals(SimpleType.STRING);
257+
258+
BoolExpr finalApprox =
259+
(!isArgConstant && isStringParseConversion) ? baseApprox : ctx.mkTrue();
260+
261+
return Optional.of(CelZ3OverloadResult.create(res, finalApprox));
265262
};
266263
}
267264

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

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -154,8 +154,6 @@ private enum IsSatisfiableTestCase {
154154
NULL_SATISFIABLE("unknown_var == null"),
155155
DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0"),
156156
DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5"),
157-
TIMESTAMP_EQUALITY_TAUTOLOGY(
158-
"timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"),
159157
CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"),
160158
MACRO_LIMIT("dyn_list.all(x, x == 1)"),
161159
STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"),
@@ -1353,12 +1351,10 @@ private enum IsAlwaysTrueViolationTestCase {
13531351
"duration(string_var) == duration(string_var)",
13541352
"Condition is not always true\\.",
13551353
"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\\."),
1354+
UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL_FROM_STRING(
1355+
"bool(string_var) == bool(string_var)",
1356+
"Condition is not always true\\.",
1357+
"Counterexample input:"),
13621358
;
13631359

13641360
final String expr;
@@ -1384,6 +1380,11 @@ public void isAlwaysTrue_violation_returnsFalse(
13841380
}
13851381

13861382
private enum IsInconclusiveTestCase {
1383+
// TODO: Implement RFC 3339 spec in conversion
1384+
TIMESTAMP_STRING_CONVERSION_VALID(
1385+
"timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"),
1386+
DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"),
1387+
BOOL_STRING_UNINTERPRETED("bool('true') == true"),
13871388
TIMESTAMP_ADD_DURATION_OVERFLOW("timestamp(253402300799) + duration('100s') > timestamp(0)"),
13881389
DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION(
13891390
"type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :"

0 commit comments

Comments
 (0)