Skip to content

Commit 6ef4a7b

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Don't report exact verdicts that depend on uninterpreted conversion results
PiperOrigin-RevId: 1004343119
1 parent 409cd49 commit 6ef4a7b

4 files changed

Lines changed: 16 additions & 80 deletions

File tree

‎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/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: 4 additions & 13 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:
@@ -257,14 +253,9 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions
257253
+ conversion.celOverloadDecl().resultType());
258254
}
259255

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));
256+
// Uninterpreted: the solver may pick a result (or error) no real input yields, so never
257+
// exact.
258+
return Optional.of(CelZ3OverloadResult.create(res, ctx.mkTrue()));
268259
};
269260
}
270261

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

Lines changed: 10 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -214,15 +214,6 @@ private IsSatisfiableTestCase(String expr, String... expectedFragments) {
214214
}
215215
}
216216

217-
@Test
218-
public void isSatisfiable_typeConversionApproximation() throws Exception {
219-
CelAbstractSyntaxTree astInt = CEL.compile("type(int('1')) == int").getAst();
220-
assertThat(VERIFIER.isSatisfiable(astInt).status()).isEqualTo(VerificationStatus.VERIFIED);
221-
222-
CelAbstractSyntaxTree astDouble = CEL.compile("type(double('1.5')) == double").getAst();
223-
assertThat(VERIFIER.isSatisfiable(astDouble).status()).isEqualTo(VerificationStatus.VERIFIED);
224-
}
225-
226217
@Test
227218
public void isSatisfiable_success(@TestParameter IsSatisfiableTestCase testCase)
228219
throws Exception {
@@ -373,6 +364,11 @@ private enum IsSatisfiableInconclusiveTestCase {
373364
APPROXIMATED_INT_TO_STRING("string(123) == '123'"),
374365
APPROXIMATED_RANGE("int('123') > 100 && int('123') < 200"),
375366
APPROXIMATED_BRANCHING("int('123') == 123 ? x > 5 : false"),
367+
APPROXIMATED_STRING_TO_INT_CONSTRAINED("string_var == 'abc' && int(string_var) == 5"),
368+
// int('x') errors at runtime, so type() of an approximate argument is approximate too.
369+
APPROXIMATED_TYPE_OF_CONVERSION("type(int('1')) == int"),
370+
APPROXIMATED_TYPE_OF_CONSTRAINED_CONVERSION(
371+
"string_var == 'abc' && type(int(string_var)) == int"),
376372
// Containers are only type-constrained up to the unroll limit, so observing one through dyn may
377373
// expose an element beyond it that violates the static type.
378374
BEYOND_BMC_LIMIT_DYN_LIST_LITERAL_EQUALITY(
@@ -1679,22 +1675,6 @@ private enum IsAlwaysTrueViolationTestCase {
16791675
"Counterexample input:",
16801676
"x = -9223372036854775808",
16811677
"y = -1"),
1682-
UNINTERPRETED_CONVERSION_CAN_ERROR_INT_FROM_STRING(
1683-
"int(string_var) == int(string_var)",
1684-
"Condition is not always true\\.",
1685-
"Counterexample input:"),
1686-
UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP_FROM_STRING(
1687-
"timestamp(string_var) == timestamp(string_var)",
1688-
"Condition is not always true\\.",
1689-
"Counterexample input:"),
1690-
UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION_FROM_STRING(
1691-
"duration(string_var) == duration(string_var)",
1692-
"Condition is not always true\\.",
1693-
"Counterexample input:"),
1694-
UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL_FROM_STRING(
1695-
"bool(string_var) == bool(string_var)",
1696-
"Condition is not always true\\.",
1697-
"Counterexample input:"),
16981678
LIST_INDEX_OUT_OF_BOUNDS_AT_BMC_LIMIT(
16991679
"size(int_list) == 5 ? int_list[5] == 1 : true",
17001680
"Condition is not always true\\.",
@@ -1760,6 +1740,8 @@ private enum IsInconclusiveTestCase {
17601740
TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"),
17611741
UNINTERPRETED_FUNCTION("request.matches('^[a-z]+$')"),
17621742
INT_STRING_UNINTERPRETED("int('123') == 123"),
1743+
INT_STRING_VAR_UNINTERPRETED("int(string_var) == int(string_var)"),
1744+
INT_CONSTRAINED_STRING_VAR_UNINTERPRETED("string_var != '5' || int(string_var) == 5"),
17631745
LIST_WITH_APPROXIMATE_ELEMENT("[request.matches('a')]"),
17641746
MAP_WITH_APPROXIMATE_KEY("{request.matches('a'): 1}"),
17651747
MAP_WITH_APPROXIMATE_VALUE("{1: request.matches('a')}"),
@@ -1830,6 +1812,9 @@ private enum EquivalenceInconclusiveTestCase {
18301812
"int_list == [1, 2, 3, 4, 5, 6] ? int_list.all(x, x > 0) : true",
18311813
"int_list == [1, 2, 3, 4, 5, 6] ? (int_list.all(x, x > 0) || size(int_list) == 6) : true"),
18321814
APPROXIMATION_DIVERGENCE("request.matches('a') == true", "request.matches('a') == false"),
1815+
TIMESTAMP_STRING_CONVERSION_NOT_BOUNDED_BY_WHOLE_SECONDS(
1816+
"timestamp(string_var) <= timestamp(253402300799)",
1817+
"timestamp(string_var) == timestamp(string_var)"),
18331818
IDENTITY_ERASURE_INCONGRUENCE(
18341819
"size(int_list) == 6 && size(int_list_2) == 6 ? (int_list.map(x, x + 1) + [1]) : [1]",
18351820
"size(int_list) == 6 && size(int_list_2) == 6 ? (int_list_2.map(x, x + 1) + [1]) : [1]"),
@@ -2458,9 +2443,6 @@ private enum EquivalenceViolationTestCase {
24582443
"google.protobuf.Duration{seconds: 100, nanos: 500}",
24592444
"google.protobuf.Duration{seconds: 100}"),
24602445
TIMESTAMP_VARIABLE_NOT_BOUNDED_BY_WHOLE_SECONDS("ts <= timestamp(253402300799)", "true"),
2461-
TIMESTAMP_STRING_CONVERSION_NOT_BOUNDED_BY_WHOLE_SECONDS(
2462-
"timestamp(string_var) <= timestamp(253402300799)",
2463-
"timestamp(string_var) == timestamp(string_var)"),
24642446
TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_NEGATIVE_NANOS_FAILS(
24652447
"int(google.protobuf.Timestamp{seconds: -1, nanos: -1}) == -1", "false"),
24662448
TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_NANOS_TOO_LARGE_FAILS(

0 commit comments

Comments
 (0)