diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 159a66a77..e3bb1bfaf 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -741,8 +741,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); + boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true); + BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( - ctx, typeSystem, callRes, Optional.of(expr), ctx.mkTrue(), args); + ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); }); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 59795c6c5..3051fbd87 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -594,7 +594,8 @@ private TranslatedValue translateEquality( // because X == X is a tautology (or propagates errors/unknowns exactly). if (z3Arg0.equals(z3Arg1)) { Expr finalResult = typeSystem.propagateErrorAndUnknown(equalityExpr, z3Arg0); - return TranslatedValue.create(finalResult, typeSystem, ctx.mkFalse()); + return TranslatedValue.create( + finalResult, typeSystem, ctx.mkOr(arg0.isApproximate(), arg1.isApproximate())); } return TranslatedValue.propagateStrict(ctx, typeSystem, equalityExpr, arg0, arg1) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index 5c0b87fbe..e9a1872c9 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -26,6 +26,7 @@ import com.microsoft.z3.DatatypeSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; +import com.microsoft.z3.FPNum; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.SeqExpr; @@ -280,6 +281,35 @@ Constructor optionalCons() { return optionalCons; } + /** + * Checks if the given CelValue expression represents a statically known primitive constant. + * + *

This is useful for determining whether an uninterpreted function's result should be treated + * as an approximation. If the argument is a known constant, any resulting error is an + * approximation (e.g., parsing a literal string). If it's a variable, the error is an exact + * runtime failure. + */ + public boolean isPrimitiveConstant(Expr expr) { + if (!expr.isApp()) { + return false; + } + FuncDecl decl = expr.getFuncDecl(); + if (decl.equals(stringCons.ConstructorDecl()) || decl.equals(bytesCons.ConstructorDecl())) { + return expr.getArgs()[0].isString(); + } else if (decl.equals(intCons.ConstructorDecl()) + || decl.equals(uintCons.ConstructorDecl()) + || decl.equals(timestampCons.ConstructorDecl()) + || decl.equals(durationCons.ConstructorDecl())) { + return expr.getArgs()[0].isNumeral(); + } else if (decl.equals(doubleCons.ConstructorDecl())) { + return expr.getArgs()[0] instanceof FPNum; + } else if (decl.equals(boolCons.ConstructorDecl())) { + Expr inner = expr.getArgs()[0]; + return inner.isTrue() || inner.isFalse(); + } + return false; + } + /** Creates a CelValue containing a boolean. */ public Expr mkBool(boolean val) { return ctx.mkApp(boolCons.ConstructorDecl(), ctx.mkBool(val)); diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index feccfd04e..8cd844214 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -19,11 +19,13 @@ import com.google.common.collect.ImmutableList; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; +import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Sort; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions; +import dev.cel.common.types.SimpleType; import java.util.Optional; /** Axiomatization for CEL's type conversion functions. */ @@ -42,14 +44,12 @@ final class TypeConversionAxioms { return Optional.of( typeSystem.withRuntimeError(typeSystem.wrapInt(uintVal), outOfBounds)); }) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.DOUBLE_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_INT64), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_INT64)) + .addOverloadTranslator( Conversions.STRING_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_INT64), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_INT64)) .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> @@ -69,14 +69,12 @@ final class TypeConversionAxioms { return Optional.of( typeSystem.withRuntimeError(typeSystem.wrapUint(intVal), outOfBounds)); }) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.DOUBLE_TO_UINT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64)) + .addOverloadTranslator( Conversions.STRING_TO_UINT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_UINT64), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_UINT64)) .build(); private static final CelZ3FunctionAxiom DOUBLE_AXIOM = @@ -84,18 +82,15 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DOUBLE_TO_DOUBLE.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.INT64_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_DOUBLE), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.INT64_TO_DOUBLE)) + .addOverloadTranslator( Conversions.UINT64_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE)) + .addOverloadTranslator( Conversions.STRING_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_DOUBLE), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_DOUBLE)) .build(); private static final CelZ3FunctionAxiom STRING_AXIOM = @@ -103,34 +98,27 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_STRING.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.INT64_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_STRING), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.INT64_TO_STRING)) + .addOverloadTranslator( Conversions.UINT64_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.UINT64_TO_STRING), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.UINT64_TO_STRING)) + .addOverloadTranslator( Conversions.DOUBLE_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_STRING), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_STRING)) + .addOverloadTranslator( Conversions.BOOL_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.BOOL_TO_STRING), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.BOOL_TO_STRING)) + .addOverloadTranslator( Conversions.BYTES_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.BYTES_TO_STRING), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.BYTES_TO_STRING)) + .addOverloadTranslator( Conversions.TIMESTAMP_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING), - /* isApproximated= */ true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING)) + .addOverloadTranslator( Conversions.DURATION_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.DURATION_TO_STRING), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.DURATION_TO_STRING)) .build(); private static final CelZ3FunctionAxiom BYTES_AXIOM = @@ -138,10 +126,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.BYTES_TO_BYTES.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_BYTES.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_BYTES), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_BYTES)) .build(); private static final CelZ3FunctionAxiom DYN_AXIOM = @@ -156,10 +143,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DURATION_TO_DURATION.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_DURATION.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_DURATION), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_DURATION)) .build(); private static final CelZ3FunctionAxiom TIMESTAMP_AXIOM = @@ -167,10 +153,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_TIMESTAMP.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP)) .addUnaryOverloadTranslator( Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> { @@ -186,10 +171,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.BOOL_TO_BOOL.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_BOOL.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_BOOL), - /* isApproximated= */ true) + createUninterpretedConversion(Conversions.STRING_TO_BOOL)) .build(); static final ImmutableList ALL_AXIOMS = @@ -204,9 +188,11 @@ final class TypeConversionAxioms { TIMESTAMP_AXIOM, BOOL_AXIOM); - private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( - Conversions conversion) { - return (ctx, typeSystem, sink, arg) -> { + private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions conversion) { + return (ctx, typeSystem, sink, unwrappedArgs, argApproximations) -> { + Expr arg = unwrappedArgs.get(0); + BoolExpr baseApprox = argApproximations.get(0); + FuncDecl funcDecl = typeSystem.internFuncDecl( conversion.celOverloadDecl().overloadId(), @@ -214,45 +200,50 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( typeSystem.celValueSort()); Expr res = ctx.mkApp(funcDecl, arg); - BoolExpr isValid; switch (conversion.celOverloadDecl().resultType().kind()) { case INT: - isValid = - ctx.mkAnd( + sink.accept(ctx.mkOr(typeSystem.isInt(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( typeSystem.isInt(res), - ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))); + ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res))))); break; case TIMESTAMP: - isValid = - ctx.mkAnd( + sink.accept(ctx.mkOr(typeSystem.isTimestamp(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( typeSystem.isTimestamp(res), - ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res)))); + ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res))))); break; case DURATION: - isValid = - ctx.mkAnd( + sink.accept(ctx.mkOr(typeSystem.isDuration(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( typeSystem.isDuration(res), - ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res)))); + ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res))))); break; case UINT: - isValid = - ctx.mkAnd( + sink.accept(ctx.mkOr(typeSystem.isUint(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( typeSystem.isUint(res), - ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))); + ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res))))); break; case DOUBLE: - isValid = - ctx.mkAnd( - typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))); + sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isDouble(res), + ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res))))); break; case STRING: - isValid = typeSystem.isString(res); + sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res))); break; case BYTES: - isValid = typeSystem.isBytes(res); + sink.accept(ctx.mkOr(typeSystem.isBytes(res), typeSystem.isError(res))); break; case BOOL: - isValid = typeSystem.isBool(res); + sink.accept(ctx.mkOr(typeSystem.isBool(res), typeSystem.isError(res))); break; default: throw new IllegalArgumentException( @@ -260,8 +251,14 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( + conversion.celOverloadDecl().resultType()); } - sink.accept(ctx.mkOr(isValid, typeSystem.isError(res))); - return Optional.of(res); + boolean isArgConstant = typeSystem.isPrimitiveConstant(arg); + boolean isStringParseConversion = + conversion.celOverloadDecl().parameterTypes().get(0).equals(SimpleType.STRING); + + BoolExpr finalApprox = + (!isArgConstant && isStringParseConversion) ? baseApprox : ctx.mkTrue(); + + return Optional.of(CelZ3OverloadResult.create(res, finalApprox)); }; } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 446f2776c..e8783af86 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -154,8 +154,6 @@ private enum IsSatisfiableTestCase { NULL_SATISFIABLE("unknown_var == null"), DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0"), DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5"), - TIMESTAMP_EQUALITY_TAUTOLOGY( - "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"), MACRO_LIMIT("dyn_list.all(x, x == 1)"), STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"), @@ -1353,12 +1351,10 @@ private enum IsAlwaysTrueViolationTestCase { "duration(string_var) == duration(string_var)", "Condition is not always true\\.", "Counterexample input:"), - // TODO: Implement RFC 3339 spec in conversion - TIMESTAMP_STRING_CONVERSION_VALID( - "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')", - "Condition is not always true\\."), - DURATION_STRING_CONVERSION_VALID( - "duration('100s') == duration('100s')", "Condition is not always true\\."), + UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL_FROM_STRING( + "bool(string_var) == bool(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), ; final String expr; @@ -1384,6 +1380,11 @@ public void isAlwaysTrue_violation_returnsFalse( } private enum IsInconclusiveTestCase { + // TODO: Implement RFC 3339 spec in conversion + TIMESTAMP_STRING_CONVERSION_VALID( + "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), + DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"), + BOOL_STRING_UNINTERPRETED("bool('true') == true"), TIMESTAMP_ADD_DURATION_OVERFLOW("timestamp(253402300799) + duration('100s') > timestamp(0)"), DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION( "type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :"