Skip to content

Commit 9655200

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Allow double(string) to return NaN
PiperOrigin-RevId: 1003575251
1 parent 04050ab commit 9655200

11 files changed

Lines changed: 186 additions & 102 deletions

File tree

‎verifier/README.md‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -370,14 +370,12 @@ public class InvariantsExample {
370370

371371
### Limitations
372372

373-
* **Unsupported Standard Functions (Uninterpreted Functions):** Not all
374-
CEL standard library functions have SMT axioms defined yet. Unsupported
375-
functions are treated as *uninterpreted functions* by Z3 (the solver
376-
only guarantees that identical inputs yield identical outputs, but does
377-
not understand the function's internal logic or return types).
378-
Consequently, verifications that rely on the specific semantics of
379-
these functions may return `VerificationStatus.INCONCLUSIVE`. Support for
380-
more standard library functions will be added incrementally.
373+
* **Uninterpreted Functions:** Custom functions, and standard library
374+
functions that don't have SMT axioms yet, are treated as uninterpreted:
375+
the solver only knows that identical inputs yield identical outputs.
376+
Results that depend on their return values are `INCONCLUSIVE`, and a
377+
`VERIFIED` result assumes they return a value of their declared type
378+
rather than an error.
381379

382380
### Best Practices & Performance
383381

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

Lines changed: 25 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@
1616

1717
import com.google.common.collect.ImmutableList;
1818
import com.google.common.collect.ImmutableSet;
19+
import com.google.common.collect.ImmutableSortedSet;
1920
import com.google.common.collect.Iterables;
2021
import com.google.common.collect.Streams;
2122
import com.microsoft.z3.ArithExpr;
@@ -83,6 +84,7 @@ final class CelAstToZ3Translator {
8384
private static final String EMPTY_MSG_REF_PREFIX = "!empty_msg_ref_";
8485
private static final String EMPTY_LIST_PREFIX = "!empty_list";
8586
private static final String EMPTY_MAP_PREFIX = "!empty_map";
87+
private static final String FUNCTION_PREFIX = "!fn_";
8688
private static final String NULL_VALUE_FIELD = "null_value";
8789
private static final String SECONDS_FIELD = "seconds";
8890
private static final String NANOS_FIELD = "nanos";
@@ -927,21 +929,40 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
927929
Sort[] argSorts = new Sort[args.size()];
928930
Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
929931
FuncDecl<?> funcDecl =
930-
typeSystem.internFuncDecl(functionName, argSorts, typeSystem.celValueSort());
932+
typeSystem.internFuncDecl(
933+
uninterpretedFunctionSymbol(exprId, ast),
934+
argSorts,
935+
typeSystem.celValueSort());
931936

932937
Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
933938
Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
934939
typeConstraints.add(createTypeConstraint(callRes, exprId, ast));
935940
typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
936941
typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
937942

938-
boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
939-
BoolExpr isApprox = ctx.mkBool(!isDynamic);
943+
// The solver picks the result freely, so a model depending on it is never exact.
940944
return TranslatedValue.propagateStrict(
941-
ctx, typeSystem, functionName, callRes, Optional.of(expr), isApprox, args);
945+
ctx,
946+
typeSystem,
947+
functionName,
948+
callRes,
949+
Optional.of(expr),
950+
/* baseTaint= */ ctx.mkTrue(),
951+
args);
942952
});
943953
}
944954

955+
/**
956+
* Returns the Z3 symbol for an uninterpreted call. Each set of candidate overloads gets its own
957+
* symbol, since distinct overloads may have different implementations even on equal values (e.g.
958+
* empty lists of different element types). The prefix keeps it apart from variables and internal
959+
* symbols.
960+
*/
961+
private static String uninterpretedFunctionSymbol(long exprId, CelAbstractSyntaxTree ast) {
962+
ImmutableList<String> overloadIds = ast.getReferenceOrThrow(exprId).overloadIds();
963+
return FUNCTION_PREFIX + String.join("|", ImmutableSortedSet.copyOf(overloadIds));
964+
}
965+
945966
/**
946967
* Whether a call may construct a container that embeds its args (e.g. list concatenation, map
947968
* insertion or optional.of). Indexing and conditionals return existing values instead, so

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,14 @@ Optional<TranslatedValue> translateFunctionCall(
8585
return opOpt.isPresent() ? Optional.of(resultChain) : Optional.empty();
8686
}
8787

88+
// A candidate overload without an axiom (e.g. a custom overload of a standard operator) is
89+
// treated as an uninterpreted call, rather than falling through to the type-mismatch error.
90+
if (reference != null
91+
&& reference.overloadIds().stream()
92+
.anyMatch(id -> !functionRegistry.getTranslator(id).isPresent())) {
93+
return Optional.empty();
94+
}
95+
8896
boolean matchedAny = false;
8997
Expr<?> currentZ3Result = resultChain.z3Expr();
9098
BoolExpr currentApprox = resultChain.isApproximate();

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

Lines changed: 0 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,6 @@
2828
import com.microsoft.z3.DatatypeSort;
2929
import com.microsoft.z3.Expr;
3030
import com.microsoft.z3.FPExpr;
31-
import com.microsoft.z3.FPNum;
3231
import com.microsoft.z3.FuncDecl;
3332
import com.microsoft.z3.IntExpr;
3433
import com.microsoft.z3.SeqExpr;
@@ -279,35 +278,6 @@ Constructor unknownCons() {
279278
return unknownCons;
280279
}
281280

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

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class GreaterAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.GREATER_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkAnd(
36+
(BoolExpr) typeSystem.unwrapBool(lhs),
37+
ctx.mkNot((BoolExpr) typeSystem.unwrapBool(rhs))))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.GREATER_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class GreaterEqualsAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.GREATER_EQUALS.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.GREATER_EQUALS_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkImplies(
36+
(BoolExpr) typeSystem.unwrapBool(rhs),
37+
(BoolExpr) typeSystem.unwrapBool(lhs)))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.GREATER_EQUALS_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class LessAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.LESS.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.LESS_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkAnd(
36+
ctx.mkNot((BoolExpr) typeSystem.unwrapBool(lhs)),
37+
(BoolExpr) typeSystem.unwrapBool(rhs)))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.LESS_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18+
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.SeqExpr;
1920
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2021
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -26,6 +27,14 @@ final class LessEqualsAxiom {
2627

2728
static final CelZ3FunctionAxiom INSTANCE =
2829
CelZ3FunctionAxiom.newBuilder(StandardFunction.LESS_EQUALS.functionDecl())
30+
.addBinaryOverloadTranslator(
31+
Comparison.LESS_EQUALS_BOOL.celOverloadDecl(),
32+
(ctx, typeSystem, constraintSink, lhs, rhs) ->
33+
Optional.of(
34+
typeSystem.wrapBool(
35+
ctx.mkImplies(
36+
(BoolExpr) typeSystem.unwrapBool(lhs),
37+
(BoolExpr) typeSystem.unwrapBool(rhs)))))
2938
.addBinaryOverloadTranslator(
3039
Comparison.LESS_EQUALS_INT64.celOverloadDecl(),
3140
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 2 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.google.common.base.Preconditions;
18-
import com.microsoft.z3.BoolExpr;
1918
import com.microsoft.z3.Context;
2019
import com.microsoft.z3.Expr;
2120
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
@@ -41,16 +40,10 @@ final class TypeAxiom {
4140
Preconditions.checkArgument(argApproximations.size() == 1);
4241

4342
Expr<?> val = unwrappedArgs.get(0);
44-
BoolExpr argApprox = argApproximations.get(0);
45-
4643
Expr<?> result = getTypeExpression(ctx, typeSystem, val);
4744

48-
// Custom approximation logic for type(): it is only approximate if the argument
49-
// is approximate AND the argument is an Error or Unknown.
50-
BoolExpr isErrOrUnk = typeSystem.isErrorOrUnknown(val);
51-
BoolExpr typeApprox = ctx.mkAnd(argApprox, isErrOrUnk);
52-
53-
return Optional.of(CelZ3OverloadResult.create(result, typeApprox));
45+
// An approximate argument may have a different kind (or be an error) at runtime.
46+
return Optional.of(CelZ3OverloadResult.create(result, argApproximations.get(0)));
5447
})
5548
.build();
5649

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

Lines changed: 10 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,6 @@
2424
import com.microsoft.z3.Sort;
2525
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2626
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions;
27-
import dev.cel.common.types.SimpleType;
2827
import dev.cel.verifier.CelZ3TypeSystem;
2928
import java.util.Optional;
3029

@@ -197,15 +196,12 @@ final class TypeConversionAxioms {
197196

198197
private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions conversion) {
199198
return (ctx, typeSystem, sink, unwrappedArgs, argApproximations) -> {
200-
Expr<?> arg = unwrappedArgs.get(0);
201-
BoolExpr baseApprox = argApproximations.get(0);
202-
203199
FuncDecl<?> funcDecl =
204200
typeSystem.internFuncDecl(
205201
conversion.celOverloadDecl().overloadId(),
206202
new Sort[] {typeSystem.celValueSort()},
207203
typeSystem.celValueSort());
208-
Expr<?> res = ctx.mkApp(funcDecl, arg);
204+
Expr<?> res = ctx.mkApp(funcDecl, unwrappedArgs.get(0));
209205

210206
switch (conversion.celOverloadDecl().resultType().kind()) {
211207
case INT:
@@ -238,9 +234,12 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions
238234
break;
239235
case DOUBLE:
240236
sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res)));
241-
sink.accept(
242-
ctx.mkImplies(
243-
typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))));
237+
// Numeric conversions never yield NaN, but parsing does (double('NaN')).
238+
if (conversion != Conversions.STRING_TO_DOUBLE) {
239+
sink.accept(
240+
ctx.mkImplies(
241+
typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))));
242+
}
244243
break;
245244
case STRING:
246245
sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res)));
@@ -257,14 +256,9 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions
257256
+ conversion.celOverloadDecl().resultType());
258257
}
259258

260-
boolean isArgConstant = typeSystem.isPrimitiveConstant(arg);
261-
boolean isStringParseConversion =
262-
conversion.celOverloadDecl().parameterTypes().get(0).equals(SimpleType.STRING);
263-
264-
BoolExpr finalApprox =
265-
(!isArgConstant && isStringParseConversion) ? baseApprox : ctx.mkTrue();
266-
267-
return Optional.of(CelZ3OverloadResult.create(res, finalApprox));
259+
// Uninterpreted: the solver may pick a result (or error) no real input yields, so never
260+
// exact.
261+
return Optional.of(CelZ3OverloadResult.create(res, ctx.mkTrue()));
268262
};
269263
}
270264

0 commit comments

Comments
 (0)