From 148e60ecf56fc982cd2384f2bc5c5547a5dd12f1 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Fri, 25 Sep 2026 16:32:55 -0700 Subject: [PATCH] Internal Changes PiperOrigin-RevId: 988561594 --- .../main/java/dev/cel/verifier/BUILD.bazel | 1 + .../cel/verifier/CelAstToZ3Translator.java | 317 ++++++++---------- .../dev/cel/verifier/CelVerifierZ3Impl.java | 87 +++-- .../cel/verifier/CelZ3OperatorTranslator.java | 206 +++++++++--- .../dev/cel/verifier/CelZ3TypeSystem.java | 170 +++++----- .../dev/cel/verifier/TranslatedValue.java | 109 +++--- .../cel/verifier/CelVerifierZ3ImplTest.java | 48 ++- 7 files changed, 537 insertions(+), 401 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 3396b6df4..888af79a5 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -118,6 +118,7 @@ java_library( ], deps = [ ":numeric_bounds", + "//:auto_value", "//common/internal:proto_time_utils", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index ba63e9693..f87f0023f 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -591,10 +591,10 @@ private Expr getDefaultValueForType(CelType type) { } private static final class FieldAccess { - final Expr presence; - final Expr value; + private final BoolExpr presence; + private final Expr value; - FieldAccess(Expr presence, Expr value) { + private FieldAccess(BoolExpr presence, Expr value) { this.presence = presence; this.value = value; } @@ -603,43 +603,27 @@ private static final class FieldAccess { private FieldAccess getMapAccess(Expr operand, String field, BoolExpr typeGuard) { Expr mapRef = typeSystem.getMapRef(operand); Expr mapFieldZ3Str = typeSystem.mkString(field); - Expr presence = ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str); + BoolExpr presence = + (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str); Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str); - - BoolExpr valNotError = ctx.mkNot(ctx.mkEq(value, typeSystem.mkError())); - typeConstraints.add( - ctx.mkImplies( - CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError)); - if (unknownIdentifiers.isEmpty()) { - BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value)); - typeConstraints.add( - ctx.mkImplies( - CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotUnknown)); - } - + constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } private FieldAccess getMsgAccess(Expr operand, String field, BoolExpr typeGuard) { Expr msgRef = typeSystem.getMessageRef(operand); Expr msgFieldZ3Str = ctx.mkString(field); - Expr presence = ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str); + BoolExpr presence = + (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str); Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str); - - BoolExpr valNotError = ctx.mkNot(ctx.mkEq(value, typeSystem.mkError())); - typeConstraints.add( - ctx.mkImplies( - CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError)); - if (unknownIdentifiers.isEmpty()) { - BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value)); - typeConstraints.add( - ctx.mkImplies( - CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotUnknown)); - } - + constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } + private void constrainPresentValue(BoolExpr guard, Expr value) { + typeConstraints.add(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value)))); + } + private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { CelExpr.CelSelect select = celExpr.select(); long exprId = celExpr.id(); @@ -654,12 +638,12 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a if (operandType instanceof MapType) { FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue()); presenceResult = mapAcc.presence; - valueResult = ctx.mkITE((BoolExpr) mapAcc.presence, mapAcc.value, typeSystem.mkError()); + valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError()); } else if (operandType.kind() == CelKind.STRUCT) { FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue()); presenceResult = msgAcc.presence; Expr defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId)); - valueResult = ctx.mkITE((BoolExpr) msgAcc.presence, msgAcc.value, defaultVal); + valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal); } else { // Dynamic type: generate the full SMT decision tree BoolExpr isMap = typeSystem.isMap(operand); @@ -675,8 +659,8 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a .build(ctx.mkFalse()); Expr defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId)); - Expr msgRead = ctx.mkITE((BoolExpr) msgAcc.presence, msgAcc.value, defaultVal); - Expr mapRead = ctx.mkITE((BoolExpr) mapAcc.presence, mapAcc.value, typeSystem.mkError()); + Expr msgRead = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal); + Expr mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError()); valueResult = CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) @@ -744,7 +728,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN); BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( - ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); + ctx, typeSystem, functionName, callRes, Optional.of(expr), isApprox, args); }); } @@ -810,32 +794,40 @@ private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSynta for (IterationElement iterElem : iterationElements) { Expr currentAccu = accu; - TranslatedValue[] condAndStep = - evaluateLoopCondAndStep( - comp, ast, iterElem.keyOrIndex, iterElem.value, currentAccu, isMap, isTwoVar); - Expr condition = condAndStep[0].z3Expr(); - Expr step = condAndStep[1].z3Expr(); - taints.add(condAndStep[1].isApproximate()); - - Expr stepVal = ctx.mkITE((BoolExpr) typeSystem.unwrapBool(condition), step, currentAccu); - Expr typeErrorOrStep = - typeSystem.withRuntimeError(stepVal, ctx.mkNot(typeSystem.isBool(condition))); - - accu = typeSystem.propagateErrorAndUnknown(typeErrorOrStep, condition); + accu = + withIterationScope( + comp, + iterElem.keyOrIndex, + iterElem.value, + currentAccu, + isMap, + isTwoVar, + () -> { + TranslatedValue condTv = translateExpr(comp.loopCondition(), ast); + TranslatedValue stepTv = translateExpr(comp.loopStep(), ast); + taints.add(stepTv.isApproximate()); + return ctx.mkITE( + (BoolExpr) typeSystem.unwrapBool(condTv.z3Expr()), + stepTv.z3Expr(), + currentAccu); + }); } TranslatedValue resultTv = withScope( comp.accuVar(), - TranslatedValue.create(accu, typeSystem, ctx.mkFalse()), + TranslatedValue.create(accu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)), () -> translateExpr(comp.result(), ast)); - taints.add(resultTv.isApproximate()); Expr result = resultTv.z3Expr(); return TranslatedValue.create( - typeSystem.propagateErrorAndUnknown(result, allRangeElems), + typeSystem.propagateErrorAndUnknown( + "comprehension", + result, + allRangeElems, + ImmutableList.>builder().add(result).addAll(allRangeElems).build()), celExpr, typeSystem, - CelZ3TypeSystem.mkOrFlattened(ctx, taints)); + resultTv.isApproximate()); } private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) { @@ -843,10 +835,10 @@ private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long i } private static final class BoundedIteration { - final BoolExpr inBounds; - final TranslatedValue stepResult; + private final BoolExpr inBounds; + private final TranslatedValue stepResult; - BoundedIteration(BoolExpr inBounds, TranslatedValue stepResult) { + private BoundedIteration(BoolExpr inBounds, TranslatedValue stepResult) { this.inBounds = inBounds; this.stepResult = stepResult; } @@ -877,7 +869,9 @@ private TranslatedValue translateDynamicComprehension( ArrayExpr mapPresence = isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null; - BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)); + BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange); + BoolExpr isTruncated = + ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))); truncationConditions.add(isTruncated); if (isAllMacro(comp) || isExistsMacro(comp)) { @@ -916,26 +910,20 @@ private BoolExpr getBoundedMapBijection( return CelZ3TypeSystem.mkAndFlattened(ctx, constraints); } - private TranslatedValue[] evaluateLoopCondAndStep( + private T withIterationScope( CelComprehension comp, - CelAbstractSyntaxTree ast, Expr keyOrIndex, Expr value, Expr currentAccu, boolean isMap, - boolean isTwoVar) { - Supplier evalBody = - () -> - new TranslatedValue[] { - translateExpr(comp.loopCondition(), ast), translateExpr(comp.loopStep(), ast) - }; - - Supplier bindAccu = + boolean isTwoVar, + Supplier action) { + Supplier bindAccu = () -> withScope( comp.accuVar(), TranslatedValue.create(currentAccu, typeSystem, ctx.mkFalse()), - evalBody); + action); if (isTwoVar) { return withScope( @@ -1005,19 +993,19 @@ private TranslatedValue unrollAllAndExists( IterationElement iterElem = getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar); - TranslatedValue[] condAndStep = - evaluateLoopCondAndStep( - comp, ast, iterElem.keyOrIndex, iterElem.value, accuInitExpr, isMap, isTwoVar); - iterations.add(new BoundedIteration(inBounds, condAndStep[1])); + TranslatedValue stepTv = + withIterationScope( + comp, + iterElem.keyOrIndex, + iterElem.value, + accuInitExpr, + isMap, + isTwoVar, + () -> translateExpr(comp.loopStep(), ast)); + iterations.add(new BoundedIteration(inBounds, stepTv)); } - TranslatedValue reducedTv = - reduceAllOrExists(iterations, isTruncated, iterRangeTv, isAllMacro(comp), celExpr, ast); - return TranslatedValue.create( - typeSystem.propagateErrorAndUnknown(reducedTv.z3Expr(), iterRangeTv.z3Expr()), - celExpr, - typeSystem, - reducedTv.isApproximate()); + return reduceAllOrExists(iterations, isTruncated, iterRangeTv, isAllMacro(comp), celExpr, ast); } private TranslatedValue unrollMapAndFilter( @@ -1036,7 +1024,6 @@ private TranslatedValue unrollMapAndFilter( boolean isMap = mapPresence != null; boolean isTwoVar = !comp.iterVar2().isEmpty(); - List brokeConds = new ArrayList<>(); List taints = new ArrayList<>(); taints.add(chainedAccuTv.isApproximate()); taints.add(iterRangeTv.isApproximate()); @@ -1049,59 +1036,51 @@ private TranslatedValue unrollMapAndFilter( constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence); Expr currentAccu = chainedAccu; - BoolExpr currentHasBroken = CelZ3TypeSystem.mkOrFlattened(ctx, brokeConds); - IterationElement iterElem = getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar); - TranslatedValue[] condAndStep = - evaluateLoopCondAndStep( - comp, ast, iterElem.keyOrIndex, iterElem.value, currentAccu, isMap, isTwoVar); - Expr condExpr = condAndStep[0].z3Expr(); - Expr stepExpr = condAndStep[1].z3Expr(); - - BoolExpr condIsBool = typeSystem.isBool(condExpr); - BoolExpr condIsTrue = ctx.mkAnd(condIsBool, (BoolExpr) typeSystem.unwrapBool(condExpr)); - BoolExpr condIsNotTrue = ctx.mkNot(condIsTrue); + TranslatedValue stepTv = + withIterationScope( + comp, + iterElem.keyOrIndex, + iterElem.value, + currentAccu, + isMap, + isTwoVar, + () -> translateExpr(comp.loopStep(), ast)); - BoolExpr isActive = ctx.mkAnd(inBounds, ctx.mkNot(currentHasBroken)); - - Expr stepVal = - ctx.mkITE((BoolExpr) typeSystem.unwrapBool(condExpr), stepExpr, currentAccu); - Expr typeErrorOrStep = typeSystem.withRuntimeError(stepVal, ctx.mkNot(condIsBool)); - // Standard macros' loop condition can't be approximate. However, we still - // keep the check here for custom macros to be safe. - taints.add(ctx.mkAnd(isActive, condAndStep[0].isApproximate())); - taints.add(ctx.mkAnd(isActive, condAndStep[1].isApproximate())); - - chainedAccu = - ctx.mkITE( - isActive, - typeSystem.propagateErrorAndUnknown(typeErrorOrStep, condExpr), - currentAccu); - - brokeConds.add(ctx.mkAnd(inBounds, condIsNotTrue)); + taints.add(ctx.mkAnd(inBounds, stepTv.isApproximate())); + chainedAccu = ctx.mkITE(inBounds, stepTv.z3Expr(), currentAccu); } TranslatedValue resultTv = withScope( comp.accuVar(), - TranslatedValue.create(chainedAccu, typeSystem, ctx.mkFalse()), + TranslatedValue.create( + chainedAccu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)), () -> translateExpr(comp.result(), ast)); - taints.add(resultTv.isApproximate()); - + Expr iterRangeExpr = iterRangeTv.z3Expr(); + BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr); + BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr); BoolExpr isNotError = ctx.mkNot(typeSystem.isError(resultTv.z3Expr())); BoolExpr shouldYieldUnknown = ctx.mkAnd(isTruncated, isNotError); - taints.add(shouldYieldUnknown); - return TranslatedValue.create( - typeSystem.propagateErrorAndUnknown( - ctx.mkITE(shouldYieldUnknown, mkParameterizedUnknown(celExpr, ast), resultTv.z3Expr()), - iterRangeTv.z3Expr()), - celExpr, - typeSystem, - CelZ3TypeSystem.mkOrFlattened(ctx, taints)); + Expr finalResult = + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(rangeIsError, typeSystem.mkError()) + .addCase( + ctx.mkOr(rangeIsUnknown, shouldYieldUnknown), mkParameterizedUnknown(celExpr, ast)) + .build(resultTv.z3Expr()); + + BoolExpr finalTaint = + (BoolExpr) + ctx.mkITE( + ctx.mkOr(rangeIsError, rangeIsUnknown), + iterRangeTv.isApproximate(), + CelZ3TypeSystem.mkOrFlattened(ctx, resultTv.isApproximate(), shouldYieldUnknown)); + + return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint); } private void constrainIterationElement( @@ -1170,35 +1149,40 @@ private TranslatedValue reduceAllOrExists( BoolExpr hasMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasMatchList); BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, hasErrorList); BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasUnknownList); + BoolExpr rangeIsError = typeSystem.isError(iterRangeTv.z3Expr()); + BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeTv.z3Expr()); BoolExpr hasSafeMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeMatchList); BoolExpr hasSafeError = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeErrorList); BoolExpr hasSafeUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeUnknownList); BoolExpr anyActiveTaint = CelZ3TypeSystem.mkOrFlattened(ctx, activeTaints); + Expr comprehensionUnknown = mkParameterizedUnknown(compExpr, ast); Expr result = CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(rangeIsError, typeSystem.mkError()) + .addCase(rangeIsUnknown, comprehensionUnknown) .addCase(hasMatch, typeSystem.mkBool(!isAll)) - .addCase(ctx.mkOr(hasUnknown, isTruncated), mkParameterizedUnknown(compExpr, ast)) + .addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown) .addCase(hasError, typeSystem.mkError()) .build(typeSystem.mkBool(isAll)); BoolExpr baseTaint = - CelZ3TypeSystem.mkOrFlattened( - ctx, Arrays.asList(anyActiveTaint, iterRangeTv.isApproximate())); + CelZ3TypeSystem.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate()); // Taint identically shadows the value flow's short-circuit control structure BoolExpr resultTaint = (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasMatch, ctx.mkNot(hasSafeMatch)) + .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate()) + .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch))) .addCase( ctx.mkOr(hasUnknown, isTruncated), - ctx.mkOr(isTruncated, ctx.mkNot(hasSafeUnknown))) - .addCase(hasError, ctx.mkNot(hasSafeError)) + ctx.mkOr(iterRangeTv.isApproximate(), isTruncated, ctx.mkNot(hasSafeUnknown))) + .addCase(hasError, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeError))) .build(baseTaint); - return TranslatedValue.create(result, typeSystem, resultTaint); + return TranslatedValue.create(result, compExpr, typeSystem, resultTaint); } private static boolean isAllMacro(CelComprehension comp) { @@ -1262,30 +1246,24 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); } if (type.equals(SimpleType.BOOL)) { - return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val); + return typeSystem.isBool(val); } if (type.equals(SimpleType.INT)) { - Expr unwrapped = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], val); - return ctx.mkAnd( - ctx.mkApp(typeSystem.intCons().getTesterDecl(), val), - ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MIN_INT64)), - ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_INT64))); + IntExpr unwrapped = typeSystem.getInt(val); + return ctx.mkAnd(typeSystem.isInt(val), ctx.mkNot(typeSystem.checkIntOverflow(unwrapped))); } if (type.equals(SimpleType.UINT)) { - Expr unwrapped = ctx.mkApp(typeSystem.uintCons().getAccessorDecls()[0], val); - return ctx.mkAnd( - ctx.mkApp(typeSystem.uintCons().getTesterDecl(), val), - ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(0)), - ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_UINT64))); + IntExpr unwrapped = typeSystem.getUint(val); + return ctx.mkAnd(typeSystem.isUint(val), ctx.mkNot(typeSystem.checkUintOverflow(unwrapped))); } if (type.equals(SimpleType.DOUBLE)) { - return (BoolExpr) ctx.mkApp(typeSystem.doubleCons().getTesterDecl(), val); + return typeSystem.isDouble(val); } if (type.equals(SimpleType.STRING)) { - return (BoolExpr) ctx.mkApp(typeSystem.stringCons().getTesterDecl(), val); + return typeSystem.isString(val); } if (type.equals(SimpleType.BYTES)) { - return (BoolExpr) ctx.mkApp(typeSystem.bytesCons().getTesterDecl(), val); + return typeSystem.isBytes(val); } if (type.equals(SimpleType.TIMESTAMP)) { IntExpr seconds = typeSystem.getTimestamp(val); @@ -1362,10 +1340,7 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { BoolExpr validEntry = ctx.mkAnd(validIndex, presence); Expr mapVal = ctx.mkSelect(mapValues, key); - BoolExpr valNotError = - unknownIdentifiers.isEmpty() - ? ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal)) - : ctx.mkNot(typeSystem.isError(mapVal)); + BoolExpr valNotError = ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal)); boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); } @@ -1382,37 +1357,11 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { return ctx.mkTrue(); } - CelAstToZ3Translator( - Context ctx, - int comprehensionUnrollLimit, - ImmutableSet unknownIdentifiers, - CelZ3FunctionRegistry functionRegistry, - CelTypeProvider typeProvider) { - this.ctx = ctx; - this.comprehensionUnrollLimit = comprehensionUnrollLimit; - this.typeSystem = new CelZ3TypeSystem(ctx); - this.typeConstraints = new LinkedHashSet<>(); - this.operatorTranslator = - new CelZ3OperatorTranslator( - ctx, - typeSystem, - this.typeConstraints::add, - this::createTypeConstraintForType, - !unknownIdentifiers.isEmpty(), - functionRegistry); - this.symbolTable = new HashMap<>(); - this.unknownIdentifiers = unknownIdentifiers; - this.emptyMessageCache = new HashMap<>(); - this.listLiteralCache = new HashMap<>(); - this.typeProvider = typeProvider; - this.truncationConditions = new ArrayList<>(); - } - - private static class IterationElement { - final Expr keyOrIndex; - final Expr value; + private static final class IterationElement { + private final Expr keyOrIndex; + private final Expr value; - IterationElement(Expr keyOrIndex, Expr value) { + private IterationElement(Expr keyOrIndex, Expr value) { this.keyOrIndex = keyOrIndex; this.value = value; } @@ -1453,4 +1402,30 @@ private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) return typeSystem.mkParameterizedUnknown(sig.staticHash(), smtArgs.build()); } + + CelAstToZ3Translator( + Context ctx, + int comprehensionUnrollLimit, + ImmutableSet unknownIdentifiers, + CelZ3FunctionRegistry functionRegistry, + CelTypeProvider typeProvider) { + this.ctx = ctx; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.typeSystem = new CelZ3TypeSystem(ctx); + this.typeConstraints = new LinkedHashSet<>(); + this.operatorTranslator = + new CelZ3OperatorTranslator( + ctx, + typeSystem, + this.typeConstraints::add, + this::createTypeConstraintForType, + functionRegistry, + comprehensionUnrollLimit); + this.symbolTable = new HashMap<>(); + this.unknownIdentifiers = unknownIdentifiers; + this.emptyMessageCache = new HashMap<>(); + this.listLiteralCache = new HashMap<>(); + this.typeProvider = typeProvider; + this.truncationConditions = new ArrayList<>(); + } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 04f3d3476..2e957622c 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -14,8 +14,10 @@ package dev.cel.verifier; +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; + import com.google.common.annotations.VisibleForTesting; -import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; @@ -38,9 +40,7 @@ import dev.cel.verifier.axioms.CelZ3FunctionAxiom; import dev.cel.verifier.axioms.CelZ3StandardAxioms; import java.time.Duration; -import java.util.ArrayList; import java.util.Arrays; -import java.util.List; import java.util.Locale; import java.util.Map; import java.util.Optional; @@ -78,7 +78,7 @@ static Builder newBuilder() { } static Builder newBuilder(Cel cel) { - return new Builder(Preconditions.checkNotNull(cel)); + return new Builder(checkNotNull(cel)); } static final class Builder implements CelVerifierBuilder { @@ -89,15 +89,6 @@ static final class Builder implements CelVerifierBuilder { private final Cel cel; private CelTypeProvider typeProvider; - private Builder(Cel cel) { - this.timeout = Duration.ofSeconds(10); - this.comprehensionUnrollLimit = 5; - this.unknownIdentifiers = ImmutableSet.builder(); - this.functionAxioms = ImmutableList.builder(); - this.typeProvider = EMPTY_TYPE_PROVIDER; - this.cel = cel; - } - @Override @CanIgnoreReturnValue public Builder setTimeout(Duration timeout) { @@ -118,14 +109,14 @@ public CelVerifierBuilder addUnknownIdentifier(String identifier) { @Override @CanIgnoreReturnValue public CelVerifierBuilder setTypeProvider(CelTypeProvider typeProvider) { - this.typeProvider = Preconditions.checkNotNull(typeProvider); + this.typeProvider = checkNotNull(typeProvider); return this; } @Override @CanIgnoreReturnValue public CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit) { - Preconditions.checkArgument(unrollLimit >= 0, "unrollLimit must be non-negative"); + checkArgument(unrollLimit >= 0, "unrollLimit must be non-negative"); this.comprehensionUnrollLimit = unrollLimit; return this; } @@ -158,27 +149,36 @@ public CelVerifier build() { typeProvider, cel); } + + private Builder(Cel cel) { + this.timeout = Duration.ofSeconds(10); + this.comprehensionUnrollLimit = 5; + this.unknownIdentifiers = ImmutableSet.builder(); + this.functionAxioms = ImmutableList.builder(); + this.typeProvider = EMPTY_TYPE_PROVIDER; + this.cel = cel; + } } @Override public CelVerificationResult isSatisfiable(CelAbstractSyntaxTree ast) throws CelVerificationException { - Preconditions.checkArgument(ast.isChecked(), "AST must be type-checked."); + checkArgument(ast.isChecked(), "AST must be type-checked."); return checkSatisfiability(ast, /* searchForCounterexample= */ false); } @Override public CelVerificationResult isAlwaysTrue(CelAbstractSyntaxTree ast) throws CelVerificationException { - Preconditions.checkArgument(ast.isChecked(), "AST must be type-checked."); + checkArgument(ast.isChecked(), "AST must be type-checked."); return checkSatisfiability(ast, /* searchForCounterexample= */ true); } @Override public CelVerificationResult verifyEquivalence( CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB) throws CelVerificationException { - Preconditions.checkArgument(astA.isChecked(), "astA must be type-checked."); - Preconditions.checkArgument(astB.isChecked(), "astB must be type-checked."); + checkArgument(astA.isChecked(), "astA must be type-checked."); + checkArgument(astB.isChecked(), "astB must be type-checked."); CelOptimizer optimizer = CelOptimizerFactory.standardCelOptimizerBuilder(cel) .addAstOptimizers( @@ -195,6 +195,7 @@ public CelVerificationResult verifyEquivalence( CelAstToZ3Translator translator = new CelAstToZ3Translator( ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider); + translator.getTypeSystem().enableParameterizedUnknownPropagation(); TranslatedValue tvA = translator.translate(astA); TranslatedValue tvB = translator.translate(astB); @@ -262,10 +263,10 @@ CelVerificationResult verifyImplication( Map boundSymbols, String subjectName) throws CelVerificationException { - Preconditions.checkArgument(assumeAst.isChecked(), "assumeAst must be type-checked."); - Preconditions.checkArgument(assertAst.isChecked(), "assertAst must be type-checked."); + checkArgument(assumeAst.isChecked(), "assumeAst must be type-checked."); + checkArgument(assertAst.isChecked(), "assertAst must be type-checked."); for (Map.Entry entry : boundSymbols.entrySet()) { - Preconditions.checkArgument( + checkArgument( entry.getValue().isChecked(), "boundSymbol AST for '%s' must be type-checked.", entry.getKey()); @@ -276,7 +277,6 @@ CelVerificationResult verifyImplication( new CelAstToZ3Translator( ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider); - List taints = new ArrayList<>(); for (Map.Entry entry : boundSymbols.entrySet()) { TranslatedValue tv = translator.translate(entry.getValue()); translator.bindSymbol(entry.getKey(), tv); @@ -284,14 +284,13 @@ CelVerificationResult verifyImplication( TranslatedValue assumeTv = translator.translate(assumeAst); TranslatedValue assertTv = translator.translate(assertAst); - taints.add(assumeTv.isApproximate()); - taints.add(assertTv.isApproximate()); BoolExpr assumeCondition = translator.isTrue(assumeTv.z3Expr()); BoolExpr assertCondition = translator.isTrue(assertTv.z3Expr()); BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition)); - BoolExpr combinedTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints); + BoolExpr combinedTaint = + CelZ3TypeSystem.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate()); BoolExpr unknownCondition = ctx.mkOr( translator.getTypeSystem().isUnknown(assumeTv.z3Expr()), @@ -513,21 +512,6 @@ private static String getCounterexampleString( ctx, typeSystem, model, isApproximate, isCounterexample); } - CelVerifierZ3Impl( - Duration timeout, - int comprehensionUnrollLimit, - ImmutableSet unknownIdentifiers, - CelZ3FunctionRegistry functionRegistry, - CelTypeProvider typeProvider, - Cel cel) { - this.timeout = timeout; - this.comprehensionUnrollLimit = comprehensionUnrollLimit; - this.unknownIdentifiers = unknownIdentifiers; - this.functionRegistry = functionRegistry; - this.typeProvider = typeProvider; - this.cel = cel; - } - private enum SolverOutcome { EXACT_MATCH, APPROXIMATE_MATCH, @@ -537,9 +521,9 @@ private enum SolverOutcome { } private static final class SolverRunResult { - final SolverOutcome outcome; - final @Nullable Model model; - final @Nullable String reason; + private final SolverOutcome outcome; + private final @Nullable Model model; + private final @Nullable String reason; static SolverRunResult exactMatch(Model model) { return new SolverRunResult(SolverOutcome.EXACT_MATCH, model, null); @@ -567,4 +551,19 @@ private SolverRunResult(SolverOutcome outcome, @Nullable Model model, @Nullable this.reason = reason; } } + + private CelVerifierZ3Impl( + Duration timeout, + int comprehensionUnrollLimit, + ImmutableSet unknownIdentifiers, + CelZ3FunctionRegistry functionRegistry, + CelTypeProvider typeProvider, + Cel cel) { + this.timeout = timeout; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.unknownIdentifiers = unknownIdentifiers; + this.functionRegistry = functionRegistry; + this.typeProvider = typeProvider; + this.cel = cel; + } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index bd5c8874e..1744b81d0 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -56,8 +56,8 @@ final class CelZ3OperatorTranslator { private final CelZ3TypeSystem typeSystem; private final Consumer constraintSink; private final BiFunction, CelType, BoolExpr> typeConstraintGenerator; - private final boolean allowUnknowns; private final CelZ3FunctionRegistry functionRegistry; + private final int comprehensionUnrollLimit; Optional translateFunctionCall( String functionName, List args, long exprId, CelAbstractSyntaxTree ast) { @@ -71,7 +71,9 @@ Optional translateFunctionCall( opOpt .map(op -> translateOperatorCall(op, args, ast)) .orElseGet( - () -> TranslatedValue.propagateStrict(ctx, typeSystem, typeSystem.mkError(), args)); + () -> + TranslatedValue.propagateStrict( + ctx, typeSystem, functionName, typeSystem.mkError(), args)); CelReference reference = ast.getReferenceMap().get(exprId); CelFunctionDecl decl = functionRegistry.getDeclaration(functionName).orElse(null); @@ -128,13 +130,62 @@ Optional translateFunctionCall( return opOpt.isPresent() ? Optional.of(resultChain) : Optional.empty(); } + if (opOpt.isPresent() && opOpt.get() == Operator.IN) { + constrainInWitnessTypes( + z3Args.get(0), z3Args.get(1), extractAstTypeOrDefault(args.get(1), ast)); + } + return Optional.of( TranslatedValue.create( - typeSystem.propagateErrorAndUnknown(currentZ3Result, z3Args), + typeSystem.propagateErrorAndUnknown(functionName, currentZ3Result, z3Args, z3Args), typeSystem, currentApprox)); } + /** + * Constrains every value that {@code InAxiom} may find in {@code rhs} to the static element (or + * key) type. + * + *

Container type constraints are only unrolled up to the comprehension unroll limit, so + * without this, a match beyond it could be an ill-typed value (e.g. a string found in a list of + * ints). + */ + private void constrainInWitnessTypes(Expr lhs, Expr rhs, CelType rhsType) { + if (rhsType instanceof ListType) { + // IN_LIST probes lhs itself, its int/uint reinterpretation for cross-type numeric equality, + // and every zero (0.0 == -0.0 == 0 == 0u). + IntExpr intVal = + (IntExpr) + ctx.mkITE(typeSystem.isInt(lhs), typeSystem.getInt(lhs), typeSystem.getUint(lhs)); + ImmutableList> candidates = + ImmutableList.of( + lhs, + typeSystem.wrapInt(intVal), + typeSystem.wrapUint(intVal), + typeSystem.mkDouble(0.0), + typeSystem.mkDouble(-0.0), + typeSystem.mkInt(0), + typeSystem.mkUint(0)); + CelType elemType = ((ListType) rhsType).elemType(); + SeqExpr seq = typeSystem.getSeq(typeSystem.getListRef(rhs)); + for (Expr cand : candidates) { + BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(cand)); + constraintSink.accept( + ctx.mkImplies( + ctx.mkAnd(typeSystem.isList(rhs), structContains), + typeConstraintGenerator.apply(cand, elemType))); + } + } else if (rhsType instanceof MapType) { + // IN_MAP only probes the presence of lhs itself. + ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs)); + BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, lhs); + constraintSink.accept( + ctx.mkImplies( + ctx.mkAnd(typeSystem.isMap(rhs), inMap), + typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType()))); + } + } + private BoolExpr mkTypeGuard(Expr arg, CelType expectedType) { switch (expectedType.kind()) { case LIST: @@ -241,7 +292,8 @@ private TranslatedValue translateOperatorCall( case IN: // Indicates a type-mismatch in an operator that's not handled // by our axioms - return TranslatedValue.propagateStrict(ctx, typeSystem, typeSystem.mkError(), args); + return TranslatedValue.propagateStrict( + ctx, typeSystem, op.getFunction(), typeSystem.mkError(), args); case INDEX: return translateIndex(args, ast, false); case OPTIONAL_INDEX: @@ -253,7 +305,8 @@ private TranslatedValue translateOperatorCall( return translateNotStrictlyFalse(args); default: // For operators we haven't implemented cleanly, just wrap uninterpreted for now. - return TranslatedValue.propagateStrict(ctx, typeSystem, typeSystem.mkUnknown(), args) + return TranslatedValue.propagateStrict( + ctx, typeSystem, op.getFunction(), typeSystem.mkUnknown(), args) .withApproximation(ctx.mkTrue()); } } @@ -297,7 +350,11 @@ private TranslatedValue translateBinaryLogicalAndOr( ctx.mkAnd(a.isZ3Unknown(), ctx.mkNot(a.isApproximate())), ctx.mkAnd(b.isZ3Unknown(), ctx.mkNot(b.isApproximate()))); - Expr unknownResult = ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr()); + String opName = isAnd ? Operator.LOGICAL_AND.getFunction() : Operator.LOGICAL_OR.getFunction(); + Expr unknownResult = + typeSystem.isParameterizingUnknowns() + ? typeSystem.mkPropagatedUnknown(opName, ImmutableList.of(a.z3Expr(), b.z3Expr())) + : ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr()); Expr resultZ3 = CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) @@ -306,11 +363,16 @@ private TranslatedValue translateBinaryLogicalAndOr( .addCase(hasError, typeSystem.mkError()) .build(typeSystem.mkBool(isAnd)); + BoolExpr unknownTaint = + typeSystem.isParameterizingUnknowns() + ? ctx.mkOr(a.isApproximate(), b.isApproximate()) + : ctx.mkNot(hasSafeUnknown); + BoolExpr resultTaint = (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) .addCase(hasMatch, ctx.mkNot(hasSafeMatch)) - .addCase(hasUnknown, ctx.mkNot(hasSafeUnknown)) + .addCase(hasUnknown, unknownTaint) .addCase(hasError, ctx.mkNot(hasSafeError)) .build(ctx.mkOr(a.isApproximate(), b.isApproximate())); @@ -327,7 +389,8 @@ private TranslatedValue translateLogicalNot( baseResult = typeSystem.withRuntimeError(baseResult, ctx.mkNot(arg.isZ3Bool())); } - return TranslatedValue.propagateStrict(ctx, typeSystem, baseResult, args); + return TranslatedValue.propagateStrict( + ctx, typeSystem, Operator.LOGICAL_NOT.getFunction(), baseResult, args); } private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTree ast) { @@ -354,7 +417,8 @@ private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTr .addCase(typeSystem.isDouble(z3Expr), doubleResult) .build(typeSystem.mkError()); } - return TranslatedValue.propagateStrict(ctx, typeSystem, result, arg); + return TranslatedValue.propagateStrict( + ctx, typeSystem, Operator.NEGATE.getFunction(), result, arg); } private BoolExpr isNumeric(Expr arg) { @@ -542,6 +606,8 @@ private BoolExpr unrollListEquality( TranslatedValue listA, TranslatedValue listB, CelAbstractSyntaxTree ast) { CelExpr literalListAst = listA.isLiteral(ExprKind.Kind.LIST) ? listA.celExpr().get() : listB.celExpr().get(); + CelType type0 = extractAstTypeOrDefault(listA, ast); + CelType type1 = extractAstTypeOrDefault(listB, ast); SeqExpr seq0 = typeSystem.getSeq(typeSystem.getListRef(listA.z3Expr())); SeqExpr seq1 = typeSystem.getSeq(typeSystem.getListRef(listB.z3Expr())); @@ -551,8 +617,14 @@ private BoolExpr unrollListEquality( int size = literalListAst.list().elements().size(); for (int i = 0; i < size; i++) { - Expr elem0 = ctx.mkNth(seq0, ctx.mkInt(i)); - Expr elem1 = ctx.mkNth(seq1, ctx.mkInt(i)); + IntExpr idx = ctx.mkInt(i); + Expr elem0 = ctx.mkNth(seq0, idx); + Expr elem1 = ctx.mkNth(seq1, idx); + + if (i >= comprehensionUnrollLimit) { + constrainListElement(seq0, idx, elem0, type0); + constrainListElement(seq1, idx, elem1, type1); + } TranslatedValue elemA = TranslatedValue.create(elem0, listA.listElementAt(i), typeSystem, listA.isApproximate()); @@ -571,6 +643,15 @@ private BoolExpr unrollListEquality( return CelZ3TypeSystem.mkAndFlattened(ctx, equalities); } + private void constrainListElement(SeqExpr seq, IntExpr idx, Expr elem, CelType listType) { + if (listType instanceof ListType) { + constraintSink.accept( + ctx.mkImplies( + ctx.mkLt(idx, ctx.mkLength(seq)), + typeConstraintGenerator.apply(elem, ((ListType) listType).elemType()))); + } + } + private TranslatedValue translateEquality( TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast, boolean isEquals) { Expr z3Arg0 = arg0.z3Expr(); @@ -622,19 +703,9 @@ private TranslatedValue translateEquality( } Expr equalityExpr = typeSystem.wrapBool(equality); + String opName = isEquals ? Operator.EQUALS.getFunction() : Operator.NOT_EQUALS.getFunction(); - // If the operands are structurally identical, the equality result is exact (not approximated) - // 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.mkOr(arg0.isApproximate(), arg1.isApproximate())); - } - - return TranslatedValue.propagateStrict(ctx, typeSystem, equalityExpr, arg0, arg1) - // Mathematically redundant, but needed to prevent exponentially branching Z3 logic tree of - // mkOr tracking exact unknowns and errors - .withApproximation(ctx.mkFalse()); + return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1); } private Expr buildListIndex( @@ -648,12 +719,7 @@ private Expr buildListIndex( ctx.mkLt((ArithExpr) index, ctx.mkLength(seq))); Expr val = ctx.mkNth(seq, (ArithExpr) index); - BoolExpr valNotError = ctx.mkNot(ctx.mkEq(val, typeSystem.mkError())); - constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotError)); - if (!allowUnknowns) { - BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(val)); - constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotUnknown)); - } + constrainValidElement(ctx.mkAnd(typeGuard, inBounds), val); if (isOptional) { Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val); @@ -666,6 +732,10 @@ private Expr buildListIndex( return ctx.mkITE(inBounds, val, typeSystem.mkError()); } + private void constrainValidElement(BoolExpr guard, Expr val) { + constraintSink.accept(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(val)))); + } + private Optional extractIntNumSafe(Expr expr) { Expr simplified = expr.simplify(); @@ -686,10 +756,10 @@ private Optional extractIntNumSafe(Expr expr) { } private static final class ProbeResult { - final BoolExpr altInMap; - final Expr altVal; + private final BoolExpr altInMap; + private final Expr altVal; - ProbeResult(BoolExpr altInMap, Expr altVal) { + private ProbeResult(BoolExpr altInMap, Expr altVal) { this.altInMap = altInMap; this.altVal = altVal; } @@ -820,12 +890,7 @@ private Expr buildMapIndex( .addCase(isDouble, doubleProbe.altVal) .build(valOrig); - BoolExpr valNotError = ctx.mkNot(ctx.mkEq(finalVal, typeSystem.mkError())); - constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotError)); - if (!allowUnknowns) { - BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(finalVal)); - constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotUnknown)); - } + constrainValidElement(ctx.mkAnd(typeGuard, finalInMap), finalVal); if (isOptional) { Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal); @@ -843,7 +908,6 @@ private TranslatedValue translateIndex( TranslatedValue lhs = args.get(0); TranslatedValue rhs = args.get(1); CelType lhsType = extractAstTypeOrDefault(lhs, ast); - CelType rhsType = extractAstTypeOrDefault(rhs, ast); Expr lhsTrans = lhs.z3Expr(); Expr rhsTrans = rhs.z3Expr(); @@ -866,7 +930,7 @@ private TranslatedValue translateIndex( } Expr actualValue = - buildAndConstrainIndex(lhsTrans, rhsTrans, lhsType, rhsType, shouldEvaluate, isOptional); + buildAndConstrainIndex(lhsTrans, rhsTrans, lhsType, shouldEvaluate, isOptional); if (isOptional) { actualValue = @@ -876,28 +940,54 @@ private TranslatedValue translateIndex( actualValue); } - return TranslatedValue.propagateStrict(ctx, typeSystem, actualValue, args); + String opName = + isOptional ? Operator.OPTIONAL_INDEX.getFunction() : Operator.INDEX.getFunction(); + BoolExpr isListIndexTruncated = + ctx.mkAnd( + shouldEvaluate, + typeSystem.isList(lhsTrans), + typeSystem.isInt(rhsTrans), + ctx.mkGe(typeSystem.getInt(rhsTrans), ctx.mkInt(comprehensionUnrollLimit)), + ctx.mkLt( + typeSystem.getInt(rhsTrans), + ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(lhsTrans))))); + BoolExpr isMapIndexTruncated = + ctx.mkAnd( + shouldEvaluate, + typeSystem.isMap(lhsTrans), + ctx.mkGt( + ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(lhsTrans))), + ctx.mkInt(comprehensionUnrollLimit))); + return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args) + .withApproximation(ctx.mkOr(isListIndexTruncated, isMapIndexTruncated)); } private Expr buildAndConstrainIndex( Expr lhsTrans, Expr rhsTrans, CelType lhsType, - CelType rhsType, BoolExpr shouldEvaluate, boolean isOptional) { CelType expectedElemType = null; - if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) { + if (lhsType.kind() == CelKind.LIST) { expectedElemType = ((ListType) lhsType).elemType(); } else if (lhsType.kind() == CelKind.MAP) { expectedElemType = ((MapType) lhsType).valueType(); } if (expectedElemType != null) { - Expr actualValue = - lhsType.kind() == CelKind.LIST - ? buildListIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional) - : buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional); + Expr actualValue; + if (lhsType.kind() == CelKind.MAP) { + actualValue = buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional); + } else { + BoolExpr isIntIndex = typeSystem.isInt(rhsTrans); + actualValue = + ctx.mkITE( + isIntIndex, + buildListIndex( + lhsTrans, rhsTrans, ctx.mkAnd(shouldEvaluate, isIntIndex), isOptional), + typeSystem.mkError()); + } CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType; @@ -934,20 +1024,32 @@ private TranslatedValue translateConditional( hasError = ctx.mkOr(hasError, ctx.mkNot(cond.isZ3Bool())); } + Expr unknownResult = + typeSystem.isParameterizingUnknowns() + ? typeSystem.mkPropagatedUnknown( + Operator.CONDITIONAL.getFunction(), + ImmutableList.of(cond.z3Expr(), trueBranch.z3Expr(), falseBranch.z3Expr())) + : cond.z3Expr(); + Expr resultZ3 = CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasUnknown, cond.z3Expr()) + .addCase(hasUnknown, unknownResult) .addCase(hasError, typeSystem.mkError()) .addCase(condTrue, trueBranch.z3Expr()) .build(falseBranch.z3Expr()); BoolExpr hasSafeError = ctx.mkAnd(hasError, ctx.mkNot(cond.isApproximate())); BoolExpr hasSafeUnknown = ctx.mkAnd(hasUnknown, ctx.mkNot(cond.isApproximate())); + BoolExpr unknownTaint = + typeSystem.isParameterizingUnknowns() + ? ctx.mkOr( + cond.isApproximate(), trueBranch.isApproximate(), falseBranch.isApproximate()) + : ctx.mkNot(hasSafeUnknown); BoolExpr resultTaint = (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasUnknown, ctx.mkNot(hasSafeUnknown)) + .addCase(hasUnknown, unknownTaint) .addCase(hasError, ctx.mkNot(hasSafeError)) .addCase(condTrue, ctx.mkOr(cond.isApproximate(), trueBranch.isApproximate())) .build(ctx.mkOr(cond.isApproximate(), falseBranch.isApproximate())); @@ -981,13 +1083,13 @@ private static boolean isNumericType(CelType type) { CelZ3TypeSystem typeSystem, Consumer constraintSink, BiFunction, CelType, BoolExpr> typeConstraintGenerator, - boolean allowUnknowns, - CelZ3FunctionRegistry functionRegistry) { + CelZ3FunctionRegistry functionRegistry, + int comprehensionUnrollLimit) { this.ctx = ctx; this.typeSystem = typeSystem; this.constraintSink = constraintSink; this.typeConstraintGenerator = typeConstraintGenerator; - this.allowUnknowns = allowUnknowns; this.functionRegistry = functionRegistry; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index dc19a8d3a..b3d1c3538 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -14,6 +14,8 @@ package dev.cel.verifier; +import com.google.auto.value.AutoValue; +import com.google.common.collect.ImmutableList; import com.google.common.collect.Lists; import com.google.common.collect.ObjectArrays; import com.google.common.primitives.UnsignedLongs; @@ -35,7 +37,6 @@ import dev.cel.common.internal.ProtoTimeUtils; import java.util.ArrayList; import java.util.Arrays; -import java.util.Collection; import java.util.HashMap; import java.util.List; import java.util.Map; @@ -132,42 +133,7 @@ public final class CelZ3TypeSystem { private static final String FUNC_MSG_TYPE_NAME = "msg_type_name"; private final Context ctx; - - private static final class FuncDeclKey { - private final String name; - private final Sort[] domain; - private final Sort range; - - FuncDeclKey(String name, Sort[] domain, Sort range) { - this.name = name; - this.domain = domain; - this.range = range; - } - - @Override - public boolean equals(Object o) { - if (this == o) { - return true; - } - if (!(o instanceof FuncDeclKey)) { - return false; - } - FuncDeclKey that = (FuncDeclKey) o; - return name.equals(that.name) - && Arrays.equals(domain, that.domain) - && range.equals(that.range); - } - - @Override - public int hashCode() { - int result = name.hashCode(); - result = 31 * result + Arrays.hashCode(domain); - result = 31 * result + range.hashCode(); - return result; - } - } - - private final Map> funcDeclCache = new HashMap<>(); + private final Map> funcDeclCache; private final DatatypeSort celValueSort; private final Constructor boolCons; @@ -204,6 +170,8 @@ public int hashCode() { private final FuncDecl msgPresenceFunc; private final FuncDecl msgTypeNameFunc; + private boolean propagateParameterizedUnknowns; + public Expr mkListRefConst(String prefix) { return ctx.mkFreshConst(prefix, listRefSort); } @@ -223,7 +191,7 @@ public Expr mkMessageRefConst(String prefix) { * avoiding redundant JNI calls to Z3. */ public FuncDecl internFuncDecl(String name, Sort[] domain, Sort range) { - FuncDeclKey cacheKey = new FuncDeclKey(name, domain, range); + FuncDeclKey cacheKey = FuncDeclKey.create(name, domain, range); return funcDeclCache.computeIfAbsent(cacheKey, k -> ctx.mkFuncDecl(name, domain, range)); } @@ -241,35 +209,35 @@ public Sort listRefSort() { return listRefSort; } - public Constructor boolCons() { + Constructor boolCons() { return boolCons; } - public Constructor intCons() { + Constructor intCons() { return intCons; } - public Constructor uintCons() { + Constructor uintCons() { return uintCons; } - public Constructor doubleCons() { + Constructor doubleCons() { return doubleCons; } - public Constructor stringCons() { + Constructor stringCons() { return stringCons; } - public Constructor bytesCons() { + Constructor bytesCons() { return bytesCons; } - public Constructor timestampCons() { + Constructor timestampCons() { return timestampCons; } - public Constructor durationCons() { + Constructor durationCons() { return durationCons; } @@ -277,6 +245,18 @@ Constructor optionalCons() { return optionalCons; } + Constructor errorCons() { + return errorCons; + } + + Constructor nullCons() { + return nullCons; + } + + Constructor unknownCons() { + return unknownCons; + } + /** * Checks if the given CelValue expression represents a statically known primitive constant. * @@ -464,77 +444,80 @@ public Expr mkNull() { return ctx.mkConst(nullCons.ConstructorDecl()); } - public Constructor errorCons() { - return errorCons; - } - - public Constructor nullCons() { - return nullCons; - } - /** Creates a CelValue representing an unknown value. */ public Expr mkUnknown() { return mkUnknown(ctx.mkConst(GENERIC_UNKNOWN_ID, unknownIdSort)); } /** Creates a CelValue representing an unknown value with a specific ID. */ - public Expr mkUnknown(Expr unknownId) { + private Expr mkUnknown(Expr unknownId) { return ctx.mkApp(unknownCons.ConstructorDecl(), unknownId); } /** Creates a parameterized unknown representing a truncated comprehension. */ - public Expr mkParameterizedUnknown(long staticHash, List> smtArgs) { + Expr mkParameterizedUnknown(long staticHash, List> smtArgs) { Sort[] domain = new Sort[smtArgs.size()]; for (int i = 0; i < smtArgs.size(); i++) { domain[i] = celValueSort(); } String ufName = "!trunc_" + Long.toHexString(staticHash); - FuncDecl truncUf = internFuncDecl(ufName, domain, unknownIdSort()); + FuncDecl truncUf = internFuncDecl(ufName, domain, unknownIdSort); Expr uniqueUnknownId = smtArgs.isEmpty() - ? ctx.mkConst(ufName, unknownIdSort()) + ? ctx.mkConst(ufName, unknownIdSort) : ctx.mkApp(truncUf, smtArgs.toArray(new Expr[0])); return mkUnknown(uniqueUnknownId); } - /** Gets the sort used for unknown identifiers. */ - public Sort unknownIdSort() { - return unknownIdSort; + void enableParameterizedUnknownPropagation() { + this.propagateParameterizedUnknowns = true; + } + + boolean isParameterizingUnknowns() { + return propagateParameterizedUnknowns; } /** - * Wraps the result in an ITE expression that short-circuits to Error or Unknown. + * Creates a parameterized unknown representing an operation applied to one or more unknown + * values, preserving EUF congruence only when both the operation and all arguments match. * - * @see #propagateErrorAndUnknown(Expr, Collection) + *

Only use this when {@link #isParameterizingUnknowns()} is true. Otherwise, verification only + * observes whether a value is unknown, not which unknown it is. */ - Expr propagateErrorAndUnknown(Expr result, Expr... args) { - return propagateErrorAndUnknown(result, Arrays.asList(args)); + Expr mkPropagatedUnknown(String opName, List> allArgs) { + Sort[] domain = new Sort[allArgs.size()]; + Arrays.fill(domain, celValueSort()); + FuncDecl propUf = internFuncDecl(opName, domain, unknownIdSort); + return mkUnknown(ctx.mkApp(propUf, allArgs.toArray(new Expr[0]))); } /** - * Wraps the result in an ITE expression that short-circuits to Error or Unknown if any of the - * provided arguments evaluate to Error or Unknown. + * Wraps the result in an ITE expression that short-circuits to Unknown, or else Error, if any of + * {@code checkArgs} evaluates to Unknown or Error. + * + * @param opName names the operation when unknowns are parameterized + * @param checkArgs the arguments that may evaluate to Unknown or Error + * @param allArgs the terms keying the parameterized unknown: every operand, including any omitted + * from {@code checkArgs} */ - Expr propagateErrorAndUnknown(Expr result, Collection> args) { - if (args.isEmpty()) { + Expr propagateErrorAndUnknown( + String opName, Expr result, List> checkArgs, List> allArgs) { + if (checkArgs.isEmpty()) { return result; } - List> argsList = new ArrayList<>(args); - BoolExpr[] errors = new BoolExpr[argsList.size()]; - BoolExpr[] unknowns = new BoolExpr[argsList.size()]; - Expr unknownResult = mkUnknown(); - // Walk backwards to preserve the earliest unknown in case of multiple unknowns (applicable for - // nested ITE chain) - for (int i = argsList.size() - 1; i >= 0; i--) { - Expr arg = argsList.get(i); - errors[i] = isError(arg); - BoolExpr isUnknown = isUnknown(arg); - unknowns[i] = isUnknown; - unknownResult = ctx.mkITE(isUnknown, arg, unknownResult); + BoolExpr[] errors = new BoolExpr[checkArgs.size()]; + BoolExpr[] unknowns = new BoolExpr[checkArgs.size()]; + for (int i = 0; i < checkArgs.size(); i++) { + errors[i] = isError(checkArgs.get(i)); + unknowns[i] = isUnknown(checkArgs.get(i)); } + // Only equivalence checks, which parameterize unknowns, can tell unknowns apart. The other + // checks only observe whether a value is unknown, so the generic unknown suffices for them. + Expr unknownResult = + propagateParameterizedUnknowns ? mkPropagatedUnknown(opName, allArgs) : mkUnknown(); BoolExpr hasError = ctx.mkOr(errors); BoolExpr hasUnknown = ctx.mkOr(unknowns); // Unknowns have higher precedence than error @@ -557,10 +540,6 @@ public Expr withRuntimeError( return ctx.mkITE(condition, mkError(), result); } - public Constructor unknownCons() { - return unknownCons; - } - /** Checks if the given CelValue is an error. */ public BoolExpr isError(Expr val) { return (BoolExpr) ctx.mkApp(errorCons.getTesterDecl(), val); @@ -846,10 +825,10 @@ public SeqExpr mkConcatSafe(Expr arg1, Expr arg2) { public static final class SwitchBuilder { private static final class SwitchCase { - final BoolExpr condition; - final Expr value; + private final BoolExpr condition; + private final Expr value; - SwitchCase(BoolExpr condition, Expr value) { + private SwitchCase(BoolExpr condition, Expr value) { this.condition = condition; this.value = value; } @@ -890,6 +869,19 @@ private SwitchBuilder(Context ctx) { } } + @AutoValue + abstract static class FuncDeclKey { + abstract String name(); + + abstract ImmutableList domain(); + + abstract Sort range(); + + private static FuncDeclKey create(String name, Sort[] domain, Sort range) { + return new AutoValue_CelZ3TypeSystem_FuncDeclKey(name, ImmutableList.copyOf(domain), range); + } + } + /** * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs. * @@ -968,6 +960,7 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { CelZ3TypeSystem(Context ctx) { this.ctx = ctx; + this.funcDeclCache = new HashMap<>(); this.boolCons = ctx.mkConstructor( CONS_BOOL, IS_BOOL, new String[] {GET_BOOL}, new Sort[] {ctx.getBoolSort()}, null); @@ -1106,5 +1099,6 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { ctx.mkArraySort(ctx.getStringSort(), ctx.getBoolSort())); this.msgTypeNameFunc = ctx.mkFuncDecl(FUNC_MSG_TYPE_NAME, new Sort[] {this.messageRefSort}, ctx.getStringSort()); + this.propagateParameterizedUnknowns = false; } } diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java index 506f0bbc7..f7aa95bdb 100644 --- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java +++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java @@ -107,37 +107,35 @@ static TranslatedValue create( * *

Otherwise, it computes whether the final result is tainted by any approximate values. */ - static TranslatedValue propagateStrict( - Context ctx, CelZ3TypeSystem ts, Expr baseResult, Collection args) { - return propagateStrict(ctx, ts, baseResult, Optional.empty(), args); - } - - static TranslatedValue propagateStrict( - Context ctx, CelZ3TypeSystem ts, Expr baseResult, TranslatedValue... args) { - return propagateStrict(ctx, ts, baseResult, Optional.empty(), Arrays.asList(args)); - } - static TranslatedValue propagateStrict( Context ctx, CelZ3TypeSystem ts, + String opName, Expr baseResult, - CelExpr celExpr, Collection args) { - return propagateStrict(ctx, ts, baseResult, Optional.of(celExpr), args); + return propagateStrict(ctx, ts, opName, baseResult, Optional.empty(), ctx.mkFalse(), args); + } + + static TranslatedValue propagateStrict( + Context ctx, CelZ3TypeSystem ts, String opName, Expr baseResult, TranslatedValue... args) { + return propagateStrict( + ctx, ts, opName, baseResult, Optional.empty(), ctx.mkFalse(), Arrays.asList(args)); } static TranslatedValue propagateStrict( Context ctx, CelZ3TypeSystem ts, Expr baseResult, - Optional celExpr, + CelExpr celExpr, Collection args) { - return propagateStrict(ctx, ts, baseResult, celExpr, ctx.mkFalse(), args); + return propagateStrict( + ctx, ts, extractOpName(celExpr), baseResult, Optional.of(celExpr), ctx.mkFalse(), args); } static TranslatedValue propagateStrict( Context ctx, CelZ3TypeSystem ts, + String opName, Expr baseResult, Optional celExpr, BoolExpr baseTaint, @@ -145,50 +143,49 @@ static TranslatedValue propagateStrict( List exactErrors = new ArrayList<>(); List exactUnknowns = new ArrayList<>(); List unknowns = new ArrayList<>(); - List taints = new ArrayList<>(); - taints.add(baseTaint); - - boolean hasNonConstantArgs = false; - List argsList = new ArrayList<>(args); - for (int i = argsList.size() - 1; i >= 0; i--) { - TranslatedValue arg = argsList.get(i); - taints.add(arg.isApproximate()); + List argTaints = new ArrayList<>(args.size()); + List> nonConstZ3Args = new ArrayList<>(); + List> allZ3Args = new ArrayList<>(args.size()); + + for (TranslatedValue arg : args) { + Expr z3Expr = arg.z3Expr(); + BoolExpr isApprox = arg.isApproximate(); + allZ3Args.add(z3Expr); + argTaints.add(isApprox); if (arg.isLiteral(ExprKind.Kind.CONSTANT)) { continue; } - hasNonConstantArgs = true; + nonConstZ3Args.add(z3Expr); - Expr z3Expr = arg.z3Expr(); - BoolExpr isApprox = arg.isApproximate(); BoolExpr isError = ts.isError(z3Expr); BoolExpr isUnknown = ts.isUnknown(z3Expr); + BoolExpr isExact = CelZ3TypeSystem.mkNotFlattened(ctx, isApprox); unknowns.add(isUnknown); - - exactErrors.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, Arrays.asList(isError, CelZ3TypeSystem.mkNotFlattened(ctx, isApprox)))); - exactUnknowns.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, Arrays.asList(isUnknown, CelZ3TypeSystem.mkNotFlattened(ctx, isApprox)))); + exactErrors.add(CelZ3TypeSystem.mkAndFlattened(ctx, isError, isExact)); + if (!ts.isParameterizingUnknowns()) { + exactUnknowns.add(CelZ3TypeSystem.mkAndFlattened(ctx, isUnknown, isExact)); + } } - BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints); - if (!hasNonConstantArgs) { + BoolExpr anyArgTaint = CelZ3TypeSystem.mkOrFlattened(ctx, argTaints); + BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, baseTaint, anyArgTaint); + if (nonConstZ3Args.isEmpty()) { return create(baseResult, celExpr, ts, anyTaint); } - List> z3Args = new ArrayList<>(); - for (TranslatedValue arg : argsList) { - if (!arg.isLiteral(ExprKind.Kind.CONSTANT)) { - z3Args.add(arg.z3Expr()); - } - } - Expr finalResult = ts.propagateErrorAndUnknown(baseResult, z3Args); + Expr finalResult = + ts.propagateErrorAndUnknown(opName, baseResult, nonConstZ3Args, allZ3Args); BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors); - BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns); + // A parameterized unknown is keyed on every argument, so it is only exact if no argument (not + // just the unknown one) is approximate. + BoolExpr hasExactUnknown = + ts.isParameterizingUnknowns() + ? CelZ3TypeSystem.mkAndFlattened( + ctx, hasUnknown, CelZ3TypeSystem.mkNotFlattened(ctx, anyArgTaint)) + : CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); BoolExpr isSafe = CelZ3TypeSystem.mkOrFlattened( @@ -201,6 +198,32 @@ static TranslatedValue propagateStrict( return create(finalResult, celExpr, ts, CelZ3TypeSystem.mkNotFlattened(ctx, isSafe)); } + /** + * Names the operation performed by {@code expr} for parameterized unknowns. The name encodes the + * expression's shape so that EUF does not equate unknowns produced by different expressions over + * the same arguments. + */ + private static String extractOpName(CelExpr expr) { + switch (expr.exprKind().getKind()) { + case SELECT: + return "select_" + expr.select().field() + "_" + expr.select().testOnly(); + case STRUCT: + StringBuilder structSb = new StringBuilder("struct_").append(expr.struct().messageName()); + for (CelExpr.CelStruct.Entry entry : expr.struct().entries()) { + structSb.append('_').append(entry.fieldKey()).append(':').append(entry.optionalEntry()); + } + return structSb.toString(); + case MAP: + StringBuilder mapSb = new StringBuilder("MAP"); + for (CelExpr.CelMap.Entry entry : expr.map().entries()) { + mapSb.append('_').append(entry.optionalEntry()); + } + return mapSb.toString(); + default: + return "LIST_" + expr.list().optionalIndices(); + } + } + /** * Returns a new TranslatedValue with an additional approximation condition OR'd into the * approximation flag. @@ -210,7 +233,7 @@ TranslatedValue withApproximation(BoolExpr approxCondition) { z3Expr(), celExpr(), typeSystem(), - typeSystem().ctx().mkOr(isApproximate(), approxCondition)); + CelZ3TypeSystem.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition)); } } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 55bc5bccf..51f3fa40f 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -441,6 +441,19 @@ private enum IsUnsatisfiableTestCase { INT_OUT_OF_BOUNDS_LARGE_DOUBLE_EQUALITY("dyn(x) == 1e100"), INT_OUT_OF_BOUNDS_LARGE_NEG_DOUBLE_EQUALITY("dyn(x) == -1e100"), UINT_OUT_OF_BOUNDS_LARGE_DOUBLE_EQUALITY("dyn(u) == 1e100"), + BEYOND_BMC_LIMIT_UNCONSTRAINED_LIST_ELEMENT_TYPE( + "size(int_list) == 6 && dyn('not_an_int') in int_list"), + BEYOND_BMC_LIMIT_UNCONSTRAINED_MAP_BIJECTION( + "size(string_int_map) == 6 && string_int_map == {'a': 1}"), + BEYOND_BMC_LIMIT_CROSS_TYPE_UINT_IN_NESTED_LIST( + "size(nested_list) == 6 && dyn(1u) in nested_list"), + BEYOND_BMC_LIMIT_LITERAL_LIST_EQUALITY_TYPE_MISMATCH( + "int_list == [1, 2, 3, 4, 5, dyn('not_an_int')]"), + BEYOND_BMC_LIMIT_LITERAL_LIST_EQUALITY_TYPE_MISMATCH_REVERSED( + "[1, 2, 3, 4, 5, dyn('not_an_int')] == int_list"), + BEYOND_BMC_LIMIT_UNCONSTRAINED_MAP_KEY_TYPE( + "size(string_int_map) == 6 && dyn(1) in string_int_map"), + LIST_INDEX_DYN_STRING_KEY("int_list[dyn('0')] == 1"), ; final String expr; @@ -882,6 +895,8 @@ private enum IsAlwaysTrueTestCase { DYNAMIC_NESTED_LIST_EQUALITY_NEEDS_EXTENSIONALITY( "int_list == [x] && int_list_2 == [y] && x == y ? int_list == int_list_2 : true"), LIST_INDEX_TYPE_CONSTRAINT("size(int_list) > 15 ? type(int_list[15]) == int : true"), + LIST_INDEX_DYN_KEY_TYPE_CONSTRAINT( + "size(int_list) > 15 ? type(int_list[dyn(15)]) == int : true"), MAP_INDEX_TYPE_CONSTRAINT( "'key' in string_int_map ? type(string_int_map['key']) == int : true"), LITERAL_LIST_INDEX("[1, 2][0] == 1"), @@ -1401,14 +1416,14 @@ private enum IsAlwaysTrueViolationTestCase { "int_list == [1, 2] ? int_list.exists_one(x, x == 1 || unknown_var) : true", "Condition is not always true\\.", "Counterexample input:", - "unknown_var = (true|false|\\d+)", + "unknown_var = .+", "int_list = \\[1, 2\\]"), DYNAMIC_LIST_EXISTS_ONE_UNKNOWN_POISONING( "int_list == [1, 2] ? !(int_list.exists_one(x, x == 1 || unknown_var) == true ||" + " int_list.exists_one(x, x == 1 || unknown_var) == false) : true", "Condition is not always true\\.", "Counterexample input:", - "unknown_var = (true|false)", + "unknown_var = .+", "int_list = \\[1, 2\\]"), DYNAMIC_ITERATION_OVER_SCALAR_RETURNS_UNKNOWN( "unknown_var == 1 ? !(unknown_var.all(x, false) == true || unknown_var.all(x, false) ==" @@ -1553,6 +1568,10 @@ private enum IsAlwaysTrueViolationTestCase { "bool(string_var) == bool(string_var)", "Condition is not always true\\.", "Counterexample input:"), + LIST_INDEX_OUT_OF_BOUNDS_AT_BMC_LIMIT( + "size(int_list) == 5 ? int_list[5] == 1 : true", + "Condition is not always true\\.", + "Counterexample input:"), ; final String expr; @@ -1621,6 +1640,8 @@ private enum IsInconclusiveTestCase { COMPREHENSION_BYTES_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, b'abc')) == 6 : true"), COMPREHENSION_FREE_VAR_INDEX_DEDUPLICATION( "x == y && y == port ? dyn_list.all(e, x == x) == dyn_list.all(e, y == port) : true"), + LIST_INDEX_BEYOND_BMC_LIMIT("size(int_list) == 6 ? int_list[5] == 1 : true"), + MAP_INDEX_BEYOND_BMC_LIMIT("size(string_int_map) == 6 ? string_int_map['a'] == 1 : true"), ; final String expr; @@ -1684,7 +1705,28 @@ private enum EquivalenceInconclusiveTestCase { "duration('10s') + (duration('20s') + duration('30s'))"), TIMESTAMP_DURATION_MATH_ASSOCIATIVITY( "(timestamp(10) + duration('20s')) + duration('30s')", - "timestamp(10) + (duration('20s') + duration('30s'))"); + "timestamp(10) + (duration('20s') + duration('30s'))"), + MAP_SIZE_BOUND_DIVERGENCE("size(int_list.map(x, x)) <= 5", "size(int_list.map(x, x)) <= 6"), + TRUNCATED_EQUALITY_DIFFERENT_CONSTANT_OPERANDS( + "size(int_list.map(x, x)) == 6", "size(int_list.map(x, x)) == 7"), + LITERAL_RANGE_TRUNCATED_ELEMENT_DIFFERENT_RESULTS( + "[int_list.map(x, x)].all(l, size(l) <= 5)", "[int_list.map(x, x)].all(l, size(l) <= 6)"), + LITERAL_RANGE_DIFFERENT_TRUNCATED_ELEMENTS( + "[int_list.transformList(i, v, i < 5 ? v : 1 / 0)].exists(l, true)", + "[int_list.transformList(i, v, v)].exists(l, true)"), + CHAINED_MAP_ALL_INDEX_BOUND_DIVERGENCE( + "int_list.map(x, x).all(i, v, i < 5)", "int_list.map(x, x).all(i, v, i >= 0)"), + EXISTS_ONE_EQUALITY_MASKING_DIVERGENCE( + "int_list.exists_one(x, x > 0) == (size(int_list) <= 5)", "int_list.exists_one(x, x > 0)"), + ALL_GUARDED_OUTER_EQUALITY_DIVERGENCE( + "int_list.all(x, x > 0) && (int_list.all(x, x > 0) == (size(int_list) <= 5))", + "int_list.all(x, x > 0)"), + CONDITIONAL_ON_TRUNCATED_ALL_DIVERGENCE( + "int_list.all(i, v, i < 5) ? 100 : 200", "int_list.all(i, v, i < 5) ? 100 : 999"), + STRUCT_DIFFERENT_DEFAULT_FIELDS_WITH_TRUNCATED_VALUE( + "TestAllTypes{single_int64: int_list.all(i, v, i < 5) ? 0 : 1}", + "TestAllTypes{single_sint64: int_list.all(i, v, i < 5) ? 0 : 1}"), + CHAINED_MAP_ALL_TRUE_INCONCLUSIVE("int_list.map(x, 1).all(v, v == 1)", "true"); final String exprA; final String exprB;