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 fabdd3d9b..feccfd04e 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -45,11 +45,11 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DOUBLE_TO_INT64.celOverloadDecl(), createUninterpretedConversion(Conversions.DOUBLE_TO_INT64), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.STRING_TO_INT64.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_INT64), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> @@ -72,11 +72,11 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DOUBLE_TO_UINT64.celOverloadDecl(), createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.STRING_TO_UINT64.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_UINT64), - true) + /* isApproximated= */ true) .build(); private static final CelZ3FunctionAxiom DOUBLE_AXIOM = @@ -87,14 +87,15 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.INT64_TO_DOUBLE.celOverloadDecl(), createUninterpretedConversion(Conversions.INT64_TO_DOUBLE), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.UINT64_TO_DOUBLE.celOverloadDecl(), createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.STRING_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_DOUBLE)) + createUninterpretedConversion(Conversions.STRING_TO_DOUBLE), + /* isApproximated= */ true) .build(); private static final CelZ3FunctionAxiom STRING_AXIOM = @@ -105,31 +106,31 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.INT64_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.INT64_TO_STRING), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.UINT64_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.UINT64_TO_STRING), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.DOUBLE_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.DOUBLE_TO_STRING), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.BOOL_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.BOOL_TO_STRING), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.BYTES_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.BYTES_TO_STRING), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.DURATION_TO_STRING.celOverloadDecl(), createUninterpretedConversion(Conversions.DURATION_TO_STRING), - true) + /* isApproximated= */ true) .build(); private static final CelZ3FunctionAxiom BYTES_AXIOM = @@ -140,7 +141,7 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_BYTES.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_BYTES), - true) + /* isApproximated= */ true) .build(); private static final CelZ3FunctionAxiom DYN_AXIOM = @@ -158,7 +159,7 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_DURATION.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_DURATION), - true) + /* isApproximated= */ true) .build(); private static final CelZ3FunctionAxiom TIMESTAMP_AXIOM = @@ -169,7 +170,7 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_TIMESTAMP.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP), - true) + /* isApproximated= */ true) .addUnaryOverloadTranslator( Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> { @@ -188,7 +189,7 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_BOOL.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_BOOL), - true) + /* isApproximated= */ true) .build(); static final ImmutableList ALL_AXIOMS = @@ -213,49 +214,45 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( typeSystem.celValueSort()); Expr res = ctx.mkApp(funcDecl, arg); + BoolExpr isValid; switch (conversion.celOverloadDecl().resultType().kind()) { case INT: - BoolExpr intValid = + isValid = ctx.mkAnd( typeSystem.isInt(res), ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))); - sink.accept(intValid); break; case TIMESTAMP: - BoolExpr timestampValid = + isValid = ctx.mkAnd( typeSystem.isTimestamp(res), ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res)))); - sink.accept(timestampValid); break; case DURATION: - BoolExpr durationValid = + isValid = ctx.mkAnd( typeSystem.isDuration(res), ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res)))); - sink.accept(durationValid); break; case UINT: - BoolExpr uintValid = + isValid = ctx.mkAnd( typeSystem.isUint(res), ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))); - sink.accept(uintValid); break; case DOUBLE: - BoolExpr doubleValid = + isValid = ctx.mkAnd( typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))); - sink.accept(doubleValid); break; case STRING: - sink.accept(typeSystem.isString(res)); + isValid = typeSystem.isString(res); break; case BYTES: - sink.accept(typeSystem.isBytes(res)); + isValid = typeSystem.isBytes(res); break; case BOOL: - sink.accept(typeSystem.isBool(res)); + isValid = typeSystem.isBool(res); break; default: throw new IllegalArgumentException( @@ -263,6 +260,7 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( + conversion.celOverloadDecl().resultType()); } + sink.accept(ctx.mkOr(isValid, typeSystem.isError(res))); return Optional.of(res); }; } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 8759422c3..446f2776c 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -93,6 +93,7 @@ public final class CelVerifierZ3ImplTest { .addVar("b", SimpleType.BOOL) .addVar("role", SimpleType.STRING) .addVar("country", SimpleType.STRING) + .addVar("string_var", SimpleType.STRING) .addVar("port", SimpleType.INT) .addVar("dur", SimpleType.DURATION) .addVar("ts", SimpleType.TIMESTAMP) @@ -325,13 +326,6 @@ public void isSatisfiable_timeout_throwsException() throws Exception { private enum IsAlwaysTrueTestCase { LOGICAL_OR_CONSTANTS("true || false"), - DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION( - "type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :" - + " true"), - TIMESTAMP_STRING_CONVERSION_VALID( - "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), - DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"), - TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"), TIMESTAMP_GREATER_EQUALS("timestamp(200) >= timestamp(100)"), DURATION_GREATER_EQUALS( "(timestamp(200) - timestamp(100)) >= (timestamp(150) - timestamp(100))"), @@ -675,29 +669,7 @@ private enum IsAlwaysTrueTestCase { TYPE_CONVERSION_DYN_IDENTITY("dyn(1) == 1"), TYPE_CONVERSION_UINT_TO_INT("int(1u) == 1"), TYPE_CONVERSION_INT_TO_UINT("uint(1) == 1u"), - TYPE_CONVERSION_INT_FROM_DOUBLE("int(1.0) == int(1.0)"), - TYPE_CONVERSION_INT_FROM_STRING("int('1') == int('1')"), - TYPE_CONVERSION_INT_FROM_TIMESTAMP( - "int(timestamp('1970-01-01T00:00:00Z')) == int(timestamp('1970-01-01T00:00:00Z'))"), - TYPE_CONVERSION_UINT_FROM_DOUBLE("uint(1.0) == uint(1.0)"), - TYPE_CONVERSION_UINT_FROM_STRING("uint('1') == uint('1')"), - TYPE_CONVERSION_DOUBLE_FROM_INT("double(1) == double(1)"), - TYPE_CONVERSION_DOUBLE_FROM_UINT("double(1u) == double(1u)"), - TYPE_CONVERSION_DOUBLE_FROM_STRING("double('1.0') == double('1.0')"), - TYPE_CONVERSION_STRING_FROM_INT("string(1) == string(1)"), - TYPE_CONVERSION_STRING_FROM_UINT("string(1u) == string(1u)"), - TYPE_CONVERSION_STRING_FROM_DOUBLE("string(1.0) == string(1.0)"), - TYPE_CONVERSION_STRING_FROM_BOOL("string(true) == string(true)"), - TYPE_CONVERSION_STRING_FROM_BYTES("string(b'foo') == string(b'foo')"), - TYPE_CONVERSION_STRING_FROM_TIMESTAMP( - "string(timestamp('1970-01-01T00:00:00Z')) == string(timestamp('1970-01-01T00:00:00Z'))"), - TYPE_CONVERSION_STRING_FROM_DURATION("string(duration('1s')) == string(duration('1s'))"), - TYPE_CONVERSION_BYTES_FROM_STRING("bytes('foo') == bytes('foo')"), - TYPE_CONVERSION_DURATION_FROM_STRING("duration('1s') == duration('1s')"), - TYPE_CONVERSION_TIMESTAMP_FROM_STRING( - "timestamp('1970-01-01T00:00:00Z') == timestamp('1970-01-01T00:00:00Z')"), TYPE_CONVERSION_TIMESTAMP_FROM_INT("timestamp(1) == timestamp(1)"), - TYPE_CONVERSION_BOOL_FROM_STRING("bool('true') == bool('true')"), TYPE_CONVERSION_INT_TO_UINT_ZERO("uint(0) == 0u"), TYPE_AXIOM_OPTIONAL("type(optional.of(1)) == optional_type"), @@ -1369,6 +1341,24 @@ private enum IsAlwaysTrueViolationTestCase { "Counterexample input:", "x = -9223372036854775808", "y = -1"), + UNINTERPRETED_CONVERSION_CAN_ERROR_INT_FROM_STRING( + "int(string_var) == int(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP_FROM_STRING( + "timestamp(string_var) == timestamp(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION_FROM_STRING( + "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\\."), ; final String expr; @@ -1395,6 +1385,11 @@ public void isAlwaysTrue_violation_returnsFalse( private enum IsInconclusiveTestCase { 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') :" + + " true"), + // TODO: Implement RFC 3339 spec in conversion + TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"), UNINTERPRETED_FUNCTION("request.matches('^[a-z]+$')"), INT_STRING_UNINTERPRETED("int('123') == 123"), LIST_WITH_APPROXIMATE_ELEMENT("[request.matches('a')]"),