diff --git a/checker/src/main/java/dev/cel/checker/CelStandardDeclarations.java b/checker/src/main/java/dev/cel/checker/CelStandardDeclarations.java index 0efcd4c65..3d5175cb5 100644 --- a/checker/src/main/java/dev/cel/checker/CelStandardDeclarations.java +++ b/checker/src/main/java/dev/cel/checker/CelStandardDeclarations.java @@ -55,7 +55,7 @@ public final class CelStandardDeclarations { private final ImmutableSet celIdentDecls; /** Enumeration of Standard Functions. */ - public enum StandardFunction { + public enum StandardFunction implements CelFunctionDecl.Declarer { // Deprecated - use {@link #IN} OLD_IN( true, @@ -1504,6 +1504,7 @@ private CelFunctionDecl withOverloads(Iterable overloads) { return newCelFunctionDecl(functionName, ImmutableSet.copyOf(overloads)); } + @Override public CelFunctionDecl functionDecl() { return celFunctionDecl; } @@ -1579,8 +1580,14 @@ public CelIdentDecl identDecl() { /** General interface for defining a standard function overload. */ @Immutable - public interface StandardOverload { + public interface StandardOverload extends CelFunctionDecl.Declarer { CelOverloadDecl celOverloadDecl(); + + @Override + default CelFunctionDecl functionDecl() { + // TODO: Remove default keyword by implementing this for all standard overloads + throw new UnsupportedOperationException("Unimplemented"); + } } /** Set of all standard function names. */ diff --git a/common/src/main/java/dev/cel/common/CelFunctionDecl.java b/common/src/main/java/dev/cel/common/CelFunctionDecl.java index 12beb53d7..ea10366ff 100644 --- a/common/src/main/java/dev/cel/common/CelFunctionDecl.java +++ b/common/src/main/java/dev/cel/common/CelFunctionDecl.java @@ -38,6 +38,12 @@ public abstract class CelFunctionDecl { /** Required. List of function overloads. Must contain at least one overload. */ public abstract ImmutableSet overloads(); + /** General interface for defining an extension function overload or standard declaration. */ + @Immutable + public interface Declarer { + CelFunctionDecl functionDecl(); + } + /** Builder for configuring the {@link CelFunctionDecl}. */ @AutoValue.Builder public abstract static class Builder { diff --git a/extensions/src/main/java/dev/cel/extensions/BUILD.bazel b/extensions/src/main/java/dev/cel/extensions/BUILD.bazel index b25fdf16d..ba57a07c3 100644 --- a/extensions/src/main/java/dev/cel/extensions/BUILD.bazel +++ b/extensions/src/main/java/dev/cel/extensions/BUILD.bazel @@ -13,7 +13,9 @@ package( java_library( name = "extension_library", - srcs = ["CelExtensionLibrary.java"], + srcs = [ + "CelExtensionLibrary.java", + ], tags = [ ], deps = [ diff --git a/extensions/src/main/java/dev/cel/extensions/CelOptionalLibrary.java b/extensions/src/main/java/dev/cel/extensions/CelOptionalLibrary.java index 87a31341f..8b67d5c79 100644 --- a/extensions/src/main/java/dev/cel/extensions/CelOptionalLibrary.java +++ b/extensions/src/main/java/dev/cel/extensions/CelOptionalLibrary.java @@ -97,95 +97,148 @@ public String getFunction() { } } + private static final class Types { + private static final TypeParamType PARAM_TYPE_K = TypeParamType.create("K"); + private static final TypeParamType PARAM_TYPE_V = TypeParamType.create("V"); + private static final OptionalType OPTIONAL_TYPE_V = OptionalType.create(PARAM_TYPE_V); + private static final ListType LIST_TYPE_V = ListType.create(PARAM_TYPE_V); + private static final MapType MAP_TYPE_KV = MapType.create(PARAM_TYPE_K, PARAM_TYPE_V); + } + + /** Declarations for the optional extension library. */ + public enum OptionalDeclaration implements CelFunctionDecl.Declarer { + OPTIONAL_OF( + CelFunctionDecl.newFunctionDeclaration( + Function.OPTIONAL_OF.getFunction(), + CelOverloadDecl.newGlobalOverload( + "optional_of", Types.OPTIONAL_TYPE_V, Types.PARAM_TYPE_V))), + OPTIONAL_OF_NON_ZERO_VALUE( + CelFunctionDecl.newFunctionDeclaration( + Function.OPTIONAL_OF_NON_ZERO_VALUE.getFunction(), + CelOverloadDecl.newGlobalOverload( + "optional_ofNonZeroValue", Types.OPTIONAL_TYPE_V, Types.PARAM_TYPE_V))), + OPTIONAL_NONE( + CelFunctionDecl.newFunctionDeclaration( + Function.OPTIONAL_NONE.getFunction(), + CelOverloadDecl.newGlobalOverload("optional_none", Types.OPTIONAL_TYPE_V))), + OPTIONAL_VALUE( + CelFunctionDecl.newFunctionDeclaration( + Function.VALUE.getFunction(), + CelOverloadDecl.newMemberOverload( + "optional_value", Types.PARAM_TYPE_V, Types.OPTIONAL_TYPE_V))), + OPTIONAL_HAS_VALUE( + CelFunctionDecl.newFunctionDeclaration( + Function.HAS_VALUE.getFunction(), + CelOverloadDecl.newMemberOverload( + "optional_hasValue", SimpleType.BOOL, Types.OPTIONAL_TYPE_V))), + OPTIONAL_UNWRAP( + CelFunctionDecl.newFunctionDeclaration( + Function.OPTIONAL_UNWRAP.getFunction(), + CelOverloadDecl.newGlobalOverload( + "optional_unwrap_list", + Types.LIST_TYPE_V, + ListType.create(Types.OPTIONAL_TYPE_V)))), + OPTIONAL_OR( + CelFunctionDecl.newFunctionDeclaration( + "or", + CelOverloadDecl.newMemberOverload( + "optional_or_optional", + Types.OPTIONAL_TYPE_V, + Types.OPTIONAL_TYPE_V, + Types.OPTIONAL_TYPE_V))), + OPTIONAL_OR_VALUE( + CelFunctionDecl.newFunctionDeclaration( + "orValue", + CelOverloadDecl.newMemberOverload( + "optional_orValue_value", + Types.PARAM_TYPE_V, + Types.OPTIONAL_TYPE_V, + Types.PARAM_TYPE_V))), + OPTIONAL_SELECT( + CelFunctionDecl.newFunctionDeclaration( + Operator.OPTIONAL_SELECT.getFunction(), + CelOverloadDecl.newGlobalOverload( + "select_optional_field", + Types.OPTIONAL_TYPE_V, + SimpleType.DYN, + SimpleType.STRING))), + OPTIONAL_INDEX( + CelFunctionDecl.newFunctionDeclaration( + Operator.OPTIONAL_INDEX.getFunction(), + CelOverloadDecl.newGlobalOverload( + "list_optindex_optional_int", + Types.OPTIONAL_TYPE_V, + Types.LIST_TYPE_V, + SimpleType.INT), + CelOverloadDecl.newGlobalOverload( + "optional_list_optindex_optional_int", + Types.OPTIONAL_TYPE_V, + OptionalType.create(Types.LIST_TYPE_V), + SimpleType.INT), + CelOverloadDecl.newGlobalOverload( + "map_optindex_optional_value", + Types.OPTIONAL_TYPE_V, + Types.MAP_TYPE_KV, + Types.PARAM_TYPE_K), + CelOverloadDecl.newGlobalOverload( + "optional_map_optindex_optional_value", + Types.OPTIONAL_TYPE_V, + OptionalType.create(Types.MAP_TYPE_KV), + Types.PARAM_TYPE_K))), + OPTIONAL_INDEX_OPERAND( + CelFunctionDecl.newFunctionDeclaration( + Operator.INDEX.getFunction(), + CelOverloadDecl.newGlobalOverload( + "optional_list_index_int", + Types.OPTIONAL_TYPE_V, + OptionalType.create(Types.LIST_TYPE_V), + SimpleType.INT), + CelOverloadDecl.newGlobalOverload( + "optional_map_index_value", + Types.OPTIONAL_TYPE_V, + OptionalType.create(Types.MAP_TYPE_KV), + Types.PARAM_TYPE_K))); + + private final CelFunctionDecl celFunctionDecl; + + OptionalDeclaration(CelFunctionDecl celFunctionDecl) { + this.celFunctionDecl = celFunctionDecl; + } + + @Override + public CelFunctionDecl functionDecl() { + return celFunctionDecl; + } + } + private static final CelExtensionLibrary LIBRARY = new CelExtensionLibrary() { - final TypeParamType paramTypeK = TypeParamType.create("K"); - final TypeParamType paramTypeV = TypeParamType.create("V"); - final OptionalType optionalTypeV = OptionalType.create(paramTypeV); - final ListType listTypeV = ListType.create(paramTypeV); - final MapType mapTypeKv = MapType.create(paramTypeK, paramTypeV); - private final CelOptionalLibrary version0 = new CelOptionalLibrary( 0, ImmutableSet.of( - CelFunctionDecl.newFunctionDeclaration( - OPTIONAL_OF.getFunction(), - CelOverloadDecl.newGlobalOverload( - "optional_of", optionalTypeV, paramTypeV)), - CelFunctionDecl.newFunctionDeclaration( - OPTIONAL_OF_NON_ZERO_VALUE.getFunction(), - CelOverloadDecl.newGlobalOverload( - "optional_ofNonZeroValue", optionalTypeV, paramTypeV)), - CelFunctionDecl.newFunctionDeclaration( - OPTIONAL_NONE.getFunction(), - CelOverloadDecl.newGlobalOverload("optional_none", optionalTypeV)), - CelFunctionDecl.newFunctionDeclaration( - VALUE.getFunction(), - CelOverloadDecl.newMemberOverload( - "optional_value", paramTypeV, optionalTypeV)), - CelFunctionDecl.newFunctionDeclaration( - HAS_VALUE.getFunction(), - CelOverloadDecl.newMemberOverload( - "optional_hasValue", SimpleType.BOOL, optionalTypeV)), - CelFunctionDecl.newFunctionDeclaration( - OPTIONAL_UNWRAP.getFunction(), - CelOverloadDecl.newGlobalOverload( - "optional_unwrap_list", listTypeV, ListType.create(optionalTypeV))), + OptionalDeclaration.OPTIONAL_OF.functionDecl(), + OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE.functionDecl(), + OptionalDeclaration.OPTIONAL_NONE.functionDecl(), + OptionalDeclaration.OPTIONAL_VALUE.functionDecl(), + OptionalDeclaration.OPTIONAL_HAS_VALUE.functionDecl(), + OptionalDeclaration.OPTIONAL_UNWRAP.functionDecl(), // Note: Implementation of "or" and "orValue" are special-cased inside the // interpreter. Hence, their bindings are not provided here. - CelFunctionDecl.newFunctionDeclaration( - "or", - CelOverloadDecl.newMemberOverload( - "optional_or_optional", optionalTypeV, optionalTypeV, optionalTypeV)), - CelFunctionDecl.newFunctionDeclaration( - "orValue", - CelOverloadDecl.newMemberOverload( - "optional_orValue_value", paramTypeV, optionalTypeV, paramTypeV)), + OptionalDeclaration.OPTIONAL_OR.functionDecl(), + OptionalDeclaration.OPTIONAL_OR_VALUE.functionDecl(), // Note: Function bindings for optional field selection and indexer is defined // in {@code StandardFunctions}. - CelFunctionDecl.newFunctionDeclaration( - Operator.OPTIONAL_SELECT.getFunction(), - CelOverloadDecl.newGlobalOverload( - "select_optional_field", - optionalTypeV, - SimpleType.DYN, - SimpleType.STRING)), - CelFunctionDecl.newFunctionDeclaration( - Operator.OPTIONAL_INDEX.getFunction(), - CelOverloadDecl.newGlobalOverload( - "list_optindex_optional_int", optionalTypeV, listTypeV, SimpleType.INT), - CelOverloadDecl.newGlobalOverload( - "optional_list_optindex_optional_int", - optionalTypeV, - OptionalType.create(listTypeV), - SimpleType.INT), - CelOverloadDecl.newGlobalOverload( - "map_optindex_optional_value", optionalTypeV, mapTypeKv, paramTypeK), - CelOverloadDecl.newGlobalOverload( - "optional_map_optindex_optional_value", - optionalTypeV, - OptionalType.create(mapTypeKv), - paramTypeK)), + OptionalDeclaration.OPTIONAL_SELECT.functionDecl(), + OptionalDeclaration.OPTIONAL_INDEX.functionDecl(), // Index overloads to accommodate using an optional value as the operand - CelFunctionDecl.newFunctionDeclaration( - Operator.INDEX.getFunction(), - CelOverloadDecl.newGlobalOverload( - "optional_list_index_int", - optionalTypeV, - OptionalType.create(listTypeV), - SimpleType.INT), - CelOverloadDecl.newGlobalOverload( - "optional_map_index_value", - optionalTypeV, - OptionalType.create(mapTypeKv), - paramTypeK))), + OptionalDeclaration.OPTIONAL_INDEX_OPERAND.functionDecl()), ImmutableSet.of( CelMacro.newReceiverMacro("optMap", 2, CelOptionalLibrary::expandOptMap)), ImmutableSet.of( // Type declaration for optional_type -> type(optional_type(V)) CelVarDecl.newVarDeclaration( - OptionalType.NAME, TypeType.create(optionalTypeV)))); + OptionalType.NAME, TypeType.create(Types.OPTIONAL_TYPE_V)))); private final CelOptionalLibrary version1 = new CelOptionalLibrary( @@ -211,16 +264,16 @@ public String getFunction() { "optional_list_first", "Return the first value in a list if present, otherwise" + " optional.none()", - optionalTypeV, - listTypeV)), + Types.OPTIONAL_TYPE_V, + Types.LIST_TYPE_V)), CelFunctionDecl.newFunctionDeclaration( LAST.functionName, CelOverloadDecl.newMemberOverload( "optional_list_last", "Return the last value in a list if present, otherwise" + " optional.none()", - optionalTypeV, - listTypeV))) + Types.OPTIONAL_TYPE_V, + Types.LIST_TYPE_V))) .build(), version1.macros, version1.variables); diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index dca62bc11..955c3d530 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -243,7 +243,9 @@ private TranslatedValue translateOperatorCall( // by our axioms return TranslatedValue.propagateStrict(ctx, typeSystem, typeSystem.mkError(), args); case INDEX: - return translateIndex(args, ast); + return translateIndex(args, ast, false); + case OPTIONAL_INDEX: + return translateIndex(args, ast, true); case CONDITIONAL: return translateConditional(args, ast); case NOT_STRICTLY_FALSE: @@ -600,7 +602,8 @@ private TranslatedValue translateEquality( .withApproximation(ctx.mkFalse()); } - private Expr buildListIndex(Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard) { + private Expr buildListIndex( + Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, boolean isOptional) { Expr listRef = typeSystem.getListRef(lhsTrans); SeqExpr seq = typeSystem.getSeq(listRef); Expr index = typeSystem.getInt(rhsTrans); @@ -617,6 +620,14 @@ private Expr buildListIndex(Expr lhsTrans, Expr rhsTrans, BoolExpr type constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotUnknown)); } + if (isOptional) { + Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val); + constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); + constraintSink.accept(typeSystem.optHasValue(resultOptRef)); + return ctx.mkITE( + inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); + } + return ctx.mkITE(inBounds, val, typeSystem.mkError()); } @@ -677,7 +688,8 @@ private ProbeResult createProbeResult( return new ProbeResult(altInMap, altVal); } - private Expr buildMapIndex(Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard) { + private Expr buildMapIndex( + Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, boolean isOptional) { Expr mapRef = typeSystem.getMapRef(lhsTrans); ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); @@ -780,10 +792,19 @@ private Expr buildMapIndex(Expr lhsTrans, Expr rhsTrans, BoolExpr typeG constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotUnknown)); } + if (isOptional) { + Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal); + constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal)); + constraintSink.accept(typeSystem.optHasValue(resultOptRef)); + return ctx.mkITE( + finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); + } + return ctx.mkITE(finalInMap, finalVal, typeSystem.mkError()); } - private TranslatedValue translateIndex(List args, CelAbstractSyntaxTree ast) { + private TranslatedValue translateIndex( + List args, CelAbstractSyntaxTree ast, boolean isOptional) { Expr lhsTrans = args.get(0).z3Expr(); Expr rhsTrans = args.get(1).z3Expr(); @@ -794,13 +815,13 @@ private TranslatedValue translateIndex(List args, CelAbstractSy Expr actualValue; if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) { - actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue()); + actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional); constraintSink.accept( ctx.mkImplies( ctx.mkNot(typeSystem.isError(actualValue)), typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType()))); } else if (lhsType.kind() == CelKind.MAP) { - actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue()); + actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue(), isOptional); constraintSink.accept( ctx.mkImplies( ctx.mkNot(typeSystem.isError(actualValue)), @@ -810,8 +831,8 @@ private TranslatedValue translateIndex(List args, CelAbstractSy BoolExpr isMapGuard = typeSystem.isMap(lhsTrans); actualValue = CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard)) - .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard)) + .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional)) + .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional)) .build(typeSystem.mkError()); } diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java index 46975756c..49f2d7450 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java @@ -14,15 +14,25 @@ package dev.cel.verifier.axioms; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_HAS_VALUE; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_NONE; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OF; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OR; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OR_VALUE; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_SELECT; +import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_VALUE; + +import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; +import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.common.CelFunctionDecl; -import dev.cel.extensions.CelOptionalLibrary; -import dev.cel.extensions.CelOptionalLibrary.Function; +import dev.cel.common.CelOverloadDecl; import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; @@ -33,13 +43,11 @@ final class OptionalAxioms { static final ImmutableList ALL_AXIOMS = ImmutableList.of( createAxiom( - Function.OPTIONAL_NONE, - "optional_none", + OPTIONAL_NONE, (ctx, ts, sink, args, argApproximations) -> Optional.of(CelZ3OverloadResult.create(ts.mkOptionalNone(), ctx.mkFalse()))), createUnaryAxiom( - Function.OPTIONAL_OF, - "optional_of", + OPTIONAL_OF, (ctx, ts, sink, value) -> { Expr optRef = ctx.mkApp(ts.optionalOfRefFunc(), value); sink.accept(ctx.mkEq(ts.getOptionalValue(optRef), value)); @@ -47,8 +55,7 @@ final class OptionalAxioms { return Optional.of(ts.mkOptionalOf(optRef)); }), createUnaryAxiom( - Function.OPTIONAL_OF_NON_ZERO_VALUE, - "optional_ofNonZeroValue", + OPTIONAL_OF_NON_ZERO_VALUE, (ctx, ts, sink, value) -> { Expr optRef = ctx.mkApp(ts.optionalOfRefFunc(), value); BoolExpr isZero = isZeroValue(ctx, ts, value); @@ -58,32 +65,85 @@ final class OptionalAxioms { return Optional.of(ctx.mkITE(isZero, ts.mkOptionalNone(), ts.mkOptionalOf(optRef))); }), createUnaryAxiom( - Function.HAS_VALUE, - "optional_hasValue", + OPTIONAL_HAS_VALUE, (ctx, ts, sink, val) -> Optional.of(ts.wrapBool(ts.optHasValue(ts.getOptionalRef(val))))), createUnaryAxiom( - Function.VALUE, - "optional_value", + OPTIONAL_VALUE, (ctx, ts, sink, val) -> { Expr optRef = ts.getOptionalRef(val); return Optional.of( ctx.mkITE(ts.optHasValue(optRef), ts.getOptionalValue(optRef), ts.mkError())); }), createBinaryAxiom( - Function.OR_VALUE, - "optional_orValue_value", + OPTIONAL_OR_VALUE, (ctx, ts, sink, val, other) -> { Expr optRef = ts.getOptionalRef(val); return Optional.of( ctx.mkITE(ts.optHasValue(optRef), ts.getOptionalValue(optRef), other)); }), createBinaryAxiom( - Function.OR, - "optional_or_optional", + OPTIONAL_OR, (ctx, ts, sink, val, other) -> { Expr optRef = ts.getOptionalRef(val); return Optional.of(ctx.mkITE(ts.optHasValue(optRef), val, other)); + }), + createBinaryAxiom( + OPTIONAL_SELECT, + (ctx, ts, sink, operand, field) -> { + Expr optRef = ts.getOptionalRef(operand); + BoolExpr isOpt = ts.isOptional(operand); + BoolExpr hasValue = ts.optHasValue(optRef); + Expr actualOperand = ctx.mkITE(isOpt, ts.getOptionalValue(optRef), operand); + + BoolExpr isMap = ts.isMap(actualOperand); + BoolExpr isMsg = ts.isMessage(actualOperand); + BoolExpr isValidTarget = ctx.mkOr(isMap, isMsg); + + Expr msgFieldZ3Str = ts.getString(field); + Expr mapFieldCelVal = field; + + Expr msgRef = ts.getMessageRef(actualOperand); + Expr mapRef = ts.getMapRef(actualOperand); + + Expr presence = + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase( + isMsg, + ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str)) + .addCase( + isMap, + ctx.mkSelect((ArrayExpr) ts.getMapPresence(mapRef), mapFieldCelVal)) + .build(ctx.mkFalse()); + + Expr value = + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase( + isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str)) + .addCase( + isMap, + ctx.mkSelect((ArrayExpr) ts.getMapValues(mapRef), mapFieldCelVal)) + .build(ts.mkError()); + + BoolExpr valNotError = ctx.mkNot(ctx.mkEq(value, ts.mkError())); + BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue()); + sink.accept( + ctx.mkImplies( + CelZ3TypeSystem.mkAndFlattened( + ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence), + valNotError)); + + Expr resultOptRef = ctx.mkApp(ts.optionalOfRefFunc(), value); + sink.accept(ctx.mkEq(ts.getOptionalValue(resultOptRef), value)); + sink.accept(ts.optHasValue(resultOptRef)); + + Expr optionalResult = + ctx.mkITE( + (BoolExpr) presence, ts.mkOptionalOf(resultOptRef), ts.mkOptionalNone()); + + Expr result = ctx.mkITE(isValidTarget, optionalResult, ts.mkError()); + return Optional.of( + ctx.mkITE(ctx.mkAnd(isOpt, ctx.mkNot(hasValue)), ts.mkOptionalNone(), result)); })); private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr val) { @@ -107,32 +167,37 @@ private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr val ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse())))); } - private static CelFunctionDecl getDecl(Function funcEnum) { - return CelOptionalLibrary.INSTANCE.functions().stream() - .filter(d -> d.name().equals(funcEnum.getFunction())) - .findFirst() - .orElseThrow(() -> new IllegalArgumentException("Unknown function: " + funcEnum)); - } - private static CelZ3FunctionAxiom createAxiom( - Function funcEnum, String overloadId, CelZ3OverloadTranslator translator) { - return CelZ3FunctionAxiom.newBuilder(getDecl(funcEnum)) - .addOverloadTranslator(overloadId, translator) - .build(); + CelFunctionDecl.Declarer declarer, CelZ3OverloadTranslator translator) { + CelFunctionDecl functionDecl = declarer.functionDecl(); + CelZ3FunctionAxiom.Builder builder = CelZ3FunctionAxiom.newBuilder(functionDecl); + builder.addOverloadTranslator(getSingleOverloadOrThrow(functionDecl), translator); + return builder.build(); } private static CelZ3FunctionAxiom createUnaryAxiom( - Function funcEnum, String overloadId, CelZ3FunctionAxiom.UnaryTranslator translator) { - return CelZ3FunctionAxiom.newBuilder(getDecl(funcEnum)) - .addUnaryOverloadTranslator(overloadId, translator) - .build(); + CelFunctionDecl.Declarer declarer, CelZ3FunctionAxiom.UnaryTranslator translator) { + CelFunctionDecl functionDecl = declarer.functionDecl(); + CelZ3FunctionAxiom.Builder builder = CelZ3FunctionAxiom.newBuilder(functionDecl); + builder.addUnaryOverloadTranslator(getSingleOverloadOrThrow(functionDecl), translator); + return builder.build(); } private static CelZ3FunctionAxiom createBinaryAxiom( - Function funcEnum, String overloadId, CelZ3FunctionAxiom.BinaryTranslator translator) { - return CelZ3FunctionAxiom.newBuilder(getDecl(funcEnum)) - .addBinaryOverloadTranslator(overloadId, translator) - .build(); + CelFunctionDecl.Declarer declarer, CelZ3FunctionAxiom.BinaryTranslator translator) { + CelFunctionDecl functionDecl = declarer.functionDecl(); + CelZ3FunctionAxiom.Builder builder = CelZ3FunctionAxiom.newBuilder(functionDecl); + builder.addBinaryOverloadTranslator(getSingleOverloadOrThrow(functionDecl), translator); + return builder.build(); + } + + private static CelOverloadDecl getSingleOverloadOrThrow(CelFunctionDecl functionDecl) { + Preconditions.checkArgument( + functionDecl.overloads().size() == 1, + "Expected 1 overload for function %s, but found %s.", + functionDecl.name(), + functionDecl.overloads().size()); + return functionDecl.overloads().iterator().next(); } private OptionalAxioms() {} diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 7f9f61520..8a975f37a 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -1557,7 +1557,41 @@ private enum EquivalenceTestCase { OPTIONAL_PRUNE_LIST_EQUALITY("[?optional.none(), 1] == [1]", "true"), OPTIONAL_PRUNE_LIST_COMPREHENSION("[1, ?optional.none()].all(x, x > 0)", "true"), MAP_COMPREHENSION( - "{'a': 1, 'b': 2}.exists(k, k == 'a')", "{'a': 1, 'b': 2}.exists(k, k == 'a')"); + "{'a': 1, 'b': 2}.exists(k, k == 'a')", "{'a': 1, 'b': 2}.exists(k, k == 'a')"), + OPTIONAL_FIELD_SELECTION_HAS_EQUIVALENCE( + "dyn_map.?field.orValue('default')", "has(dyn_map.field) ? dyn_map.field : 'default'"), + OPTIONAL_FIELD_SELECTION_MACRO_EQUIVALENCE( + "dyn_map.?field.hasValue() ? dyn_map.?field.value() : 'default'", + "has(dyn_map.field) ? dyn_map.field : 'default'"), + OPTIONAL_FIELD_SELECTION_CHAINED("{\"a\": {\"b\": 42}}.?a.?b", "optional.of(42)"), + OPTIONAL_INDEX_LIST_PRESENT("[1, 2, 3][?0]", "optional.of(1)"), + OPTIONAL_INDEX_LIST_MISSING("[1, 2, 3][?5]", "optional.none()"), + OPTIONAL_INDEX_MAP_MISSING("{'a': 1}[?'missing_key']", "optional.none()"), + OPTIONAL_FIELD_SELECTION_PROTO3_PRIMITIVE_ZERO( + "TestAllTypes{single_int32: 0}.?single_int32", "optional.none()"), + OPTIONAL_FIELD_SELECTION_PROTO3_PRIMITIVE_NONZERO( + "TestAllTypes{single_int32: 5}.?single_int32", "optional.of(5)"), + OPTIONAL_FIELD_SELECTION_PROTO3_MESSAGE_EMPTY( + "TestAllTypes{}.?standalone_message", "optional.none()"), + OPTIONAL_FIELD_SELECTION_PROTO3_MESSAGE_PRESENT( + "TestAllTypes{standalone_message:" + + " TestAllTypes.NestedMessage{}}.?standalone_message.hasValue()", + "true"), + OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_NULL( + "TestAllTypes{}.?single_int64_wrapper", "optional.none()"), + OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_EXPLICIT_NULL( + "TestAllTypes{single_int64_wrapper: null}.?single_int64_wrapper", "optional.none()"), + OPTIONAL_FIELD_SELECTION_PROTO3_WRAPPER_PRESENT( + "TestAllTypes{single_int64_wrapper: 42}.?single_int64_wrapper", "optional.of(42)"), + OPTIONAL_FIELD_SELECTION_DYNAMIC_MISS( + "dyn_map == {'a': 1} ? dyn_map.?b : optional.none()", "optional.none()"), + OPTIONAL_FIELD_SELECTION_TYPE_GUARDING( + "type(dyn_var) == map ? dyn_var.?key == optional.none() || dyn_var.?key.hasValue() : true", + "true"), + OPTIONAL_FIELD_SELECTION_MAP_COMPREHENSION( + "{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v).?b", "optional.of(2)"), + OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)"); + private final String exprA; private final String exprB; @@ -1601,7 +1635,16 @@ private enum EquivalenceViolationTestCase { OPTIONAL_OR_VALUE_VIOLATION("optional.of(x).orValue(y)", "y"), OPTIONAL_VALUE_VIOLATION("optional.of(x).value()", "y"), LIST_OPTIONAL_ELEMENTS_COLLISION("[1, ?opt_var]", "[1, opt_var]"), - CROSS_NUMERIC_EQUALITY_INT_DYN_VIOLATION("1 == request", "false"); + CROSS_NUMERIC_EQUALITY_INT_DYN_VIOLATION("1 == request", "false"), + OPTIONAL_SELECTION_VS_DIRECT_ERROR( + "{'a': 1}.?missing_key", "optional.of({'a': 1}.missing_key)"), + OPTIONAL_NESTED_NONE_VS_FLAT_NONE("{'a': optional.none()}.?a", "optional.none()"), + OPTIONAL_NULL_VALUE_VS_MISSING("{'a': null}.?a", "optional.none()"), + OPTIONAL_PROTO3_PRIMITIVE_ZERO_VS_OF_ZERO( + "TestAllTypes{single_int32: 0}.?single_int32", "optional.of(0)"), + OPTIONAL_PROTO3_WRAPPER_ZERO_VS_UNSET( + "TestAllTypes{single_int64_wrapper: 0}.?single_int64_wrapper", + "TestAllTypes{}.?single_int64_wrapper"); final String exprA; final String exprB; @@ -1961,8 +2004,8 @@ public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws CelAbstractSyntaxTree ast = customCel .compile( - "d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 == 9429185123491285.0 && d1 > 100000.0 &&" - + " d2 > 100000.0 && d3 > 100000.0 && d4 > 100000.0") + "d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 * d1 * d2 * d3 * d4 ==" + + " 9429185123491285.0 && d1 > 1.0 && d2 > 1.0 && d3 > 1.0 && d4 > 1.0") .getAst(); CelVerificationException e =