diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 005289b83..460d48c18 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -23,6 +23,7 @@ import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.FuncDecl; +import com.microsoft.z3.Model; import com.microsoft.z3.Quantifier; import com.microsoft.z3.SeqExpr; import com.microsoft.z3.Sort; @@ -89,6 +90,14 @@ BoolExpr hasTruncation() { return context.hasTruncation(); } + ImmutableList approximationSources(Model model, BoolExpr taint) { + return context.approximationSources(model, taint); + } + + BoolExpr recordApproximation(String description, BoolExpr condition) { + return context.recordApproximation(description, condition); + } + CelZ3TypeSystem getTypeSystem() { return typeSystem; } @@ -450,7 +459,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { functionName, callRes, Optional.of(expr), - /* baseTaint= */ ctx.mkTrue(), + /* baseTaint= */ context.recordCallApproximation(functionName, ctx.mkTrue()), args); }); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 131b3c24c..d98e4f0d4 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -231,7 +231,9 @@ public CelVerificationResult verifyEquivalence( ctx, tvA.isApproximate(), tvB.isApproximate(), - ctx.mkAnd(tvA.isZ3Unknown(), tvB.isZ3Unknown())); + translator.recordApproximation( + "unknown results, which are compared only by their origin", + ctx.mkAnd(tvA.isZ3Unknown(), tvB.isZ3Unknown()))); Solver solver = newSolver(ctx); for (BoolExpr constraint : translator.getTypeConstraints()) { @@ -259,8 +261,7 @@ public CelVerificationResult verifyEquivalence( "Equivalence violation detected.", extractWitness(ctx, translator, result.model)); case APPROXIMATE_MATCH: return CelVerificationResult.inconclusive( - "Inconclusive: a divergence may exist, but it depends on approximations, missing" - + " theories, or loop bounds.", + inconclusiveReason("a divergence", translator, result.model, combinedTaint), extractWitness(ctx, translator, result.model), /* isCounterexample= */ true); case TRUNCATED: @@ -336,8 +337,7 @@ CelVerificationResult verifyImplication( extractWitness(ctx, translator, result.model)); case APPROXIMATE_MATCH: return CelVerificationResult.inconclusive( - "Inconclusive: a counterexample may exist, but it depends on approximations, missing" - + " theories, or loop bounds.", + inconclusiveReason("a counterexample", translator, result.model, combinedTaint), extractWitness(ctx, translator, result.model), /* isCounterexample= */ true); case TRUNCATED: @@ -390,14 +390,12 @@ private CelVerificationResult checkSatisfiability( : CelVerificationResult.verified("Condition is satisfiable.", witness); case APPROXIMATE_MATCH: - String prefix = - searchForCounterexample - ? "Inconclusive: a counterexample may exist, but it depends on approximations," - + " missing theories, or loop bounds." - : "Inconclusive: a satisfying model may exist, but it depends on" - + " approximations, missing theories, or loop bounds."; return CelVerificationResult.inconclusive( - prefix, + inconclusiveReason( + searchForCounterexample ? "a counterexample" : "a satisfying input", + translator, + result.model, + tv.isApproximate()), extractWitness(ctx, translator, result.model), /* isCounterexample= */ searchForCounterexample); @@ -502,6 +500,15 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn parameterizeUnknowns); } + private static String inconclusiveReason( + String candidate, CelAstToZ3Translator translator, Model model, BoolExpr taint) { + ImmutableList sources = translator.approximationSources(model, taint); + return "Inconclusive: " + + candidate + + " may exist, but it depends on what the verifier doesn't model exactly" + + (sources.isEmpty() ? "." : ": " + String.join(", ", sources) + "."); + } + private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) { return CelZ3CounterexampleGenerator.generate( ctx, diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java index 79bcd0e42..a047b0a45 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java @@ -154,7 +154,9 @@ private TranslatedValue translateDynamicComprehension( boolean isMap = rangeType instanceof MapType; if (!isList && !isMap) { BoolExpr isRuntimeListOrMap = - ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange)); + context.recordApproximation( + "comprehensions over `dyn` values", + ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange))); Expr result = ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError()); return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap); @@ -171,7 +173,8 @@ private TranslatedValue translateDynamicComprehension( BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange); BoolExpr isTruncated = - ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))); + context.recordUnrollLimitApproximation( + ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)))); context.addTruncationCondition(isTruncated); if (isAllMacro(comp) || isExistsMacro(comp)) { @@ -338,7 +341,10 @@ private TranslatedValue unrollMapAndFilter( // TODO: Model the loop condition for custom macros; until then, abstract the // result of any non-true condition, since the unrolled value ignores early exits. - BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition())); + BoolExpr isConditionUnmodeled = + context.recordApproximation( + "comprehensions with a loop condition", + ctx.mkBool(!isLiteralTrue(comp.loopCondition()))); BoolExpr isAbstracted = CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled); // An error is not final when truncated: an unknown from a later iteration overrides it. diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 55aa62882..d796fcf22 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -130,7 +130,12 @@ Optional translateFunctionCall( BoolExpr typeGuard = CelZ3Exprs.mkAndFlattened(ctx, typeGuards); currentZ3Result = ctx.mkITE(typeGuard, evaluatedResult.z3Expr(), currentZ3Result); currentApprox = - (BoolExpr) ctx.mkITE(typeGuard, evaluatedResult.isApproximate(), currentApprox); + (BoolExpr) + ctx.mkITE( + typeGuard, + attributeApproximation( + functionName, evaluatedResult.isApproximate(), argApproximations), + currentApprox); } if (!matchedAny) { @@ -160,6 +165,24 @@ Optional translateFunctionCall( currentApprox)); } + // Returns an overload's approximation with the part it adds itself recorded as a call + // approximation. + private BoolExpr attributeApproximation( + String functionName, BoolExpr approx, ImmutableList argApproximations) { + // A literal `true` can't be substituted without also replacing the overload's own `true`. + ImmutableList substitutable = + argApproximations.stream().filter(a -> !a.isTrue()).collect(toImmutableList()); + // Approximations only grow with their arguments', so approx is equivalent to the overload's own + // part (its value with exact arguments) or approx under some approximate argument. + BoolExpr own = + context.recordCallApproximation( + functionName, + (BoolExpr) context.withoutApproximation(approx, substitutable).simplify()); + BoolExpr inherited = + CelZ3Exprs.mkAndFlattened(ctx, approx, CelZ3Exprs.mkOrFlattened(ctx, argApproximations)); + return CelZ3Exprs.mkOrFlattened(ctx, own, inherited); + } + /** * Constrains every value that {@code InAxiom} may find in {@code rhs} to its guaranteed element * (or key) type, and returns the condition under which the result remains approximate. @@ -339,7 +362,7 @@ private TranslatedValue translateOperatorCall( // For operators we haven't implemented cleanly, just wrap uninterpreted for now. return TranslatedValue.propagateStrict( ctx, typeSystem, op.getFunction(), typeSystem.mkUnknown(), args) - .withApproximation(ctx.mkTrue()); + .withApproximation(context.recordCallApproximation(op.getFunction(), ctx.mkTrue())); } } @@ -977,14 +1000,15 @@ private TranslatedValue translateIndex( 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))))); + context.recordUnrollLimitApproximation( + 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, context.isTruncatedMap(lhsTrans)); return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args) .withApproximation( @@ -1148,11 +1172,12 @@ private BoolExpr mayObserveTruncatedTypeConstraint( if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) { return ctx.mkFalse(); } - return CelZ3Exprs.mkOrFlattened( - ctx, - Arrays.stream(args) - .map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr())) - .collect(toImmutableList())); + return context.recordUnrollLimitApproximation( + CelZ3Exprs.mkOrFlattened( + ctx, + Arrays.stream(args) + .map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr())) + .collect(toImmutableList()))); } CelZ3OperatorTranslator(CelZ3TranslationContext context, CelZ3FunctionRegistry functionRegistry) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java index 8e52da1b9..e3599d517 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java @@ -14,12 +14,17 @@ package dev.cel.verifier; +import static com.google.common.collect.ImmutableList.toImmutableList; + +import com.google.common.collect.ImmutableList; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; +import com.microsoft.z3.Model; import dev.cel.common.types.CelType; import dev.cel.common.types.SimpleType; import java.util.ArrayList; +import java.util.Arrays; import java.util.Collections; import java.util.HashMap; import java.util.LinkedHashMap; @@ -41,6 +46,7 @@ final class CelZ3TranslationContext { private final Set constraints; private final Map, CelType> inputVariableTypes; private final List truncationConditions; + private final Map> approximationTerms; private final Map symbolTable; private final Map localScope; @@ -93,11 +99,65 @@ CelType guaranteedType(Expr value) { * not linked to its keys. */ BoolExpr isTruncatedMap(Expr val) { - return ctx.mkAnd( - typeSystem.isMap(val), - ctx.mkGt( - ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))), - ctx.mkInt(comprehensionUnrollLimit))); + return recordUnrollLimitApproximation( + ctx.mkAnd( + typeSystem.isMap(val), + ctx.mkGt( + ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))), + ctx.mkInt(comprehensionUnrollLimit)))); + } + + /** + * Records {@code description} as a reason results are approximate where {@code condition} holds, + * and returns the term to use for {@code condition}, so that it can be told apart in a taint. + */ + BoolExpr recordApproximation(String description, BoolExpr condition) { + BoolExpr term = condition; + if (condition.isTrue()) { + // A literal `true` is shared by every other unconditional approximation. + term = (BoolExpr) ctx.mkFreshConst("!approx", ctx.getBoolSort()); + constraints.add(term); + } + approximationTerms.computeIfAbsent(description, k -> new ArrayList<>()).add(term); + return term; + } + + BoolExpr recordUnrollLimitApproximation(BoolExpr condition) { + return recordApproximation( + "lists and maps longer than the unroll limit (" + comprehensionUnrollLimit + ")", + condition); + } + + BoolExpr recordCallApproximation(String functionName, BoolExpr condition) { + return recordApproximation("calls to `" + functionName + "`", condition); + } + + /** + * Returns the descriptions of the approximations that are enough on their own to make {@code + * taint} hold in {@code model}, which leaves out those in short-circuited operands or untaken + * branches. + */ + ImmutableList approximationSources(Model model, BoolExpr taint) { + return approximationTerms.keySet().stream() + .filter(description -> holds(model, withoutApproximation(taint, termsExcept(description)))) + .collect(toImmutableList()); + } + + private ImmutableList termsExcept(String description) { + return approximationTerms.entrySet().stream() + .filter(source -> !source.getKey().equals(description)) + .flatMap(source -> source.getValue().stream()) + .collect(toImmutableList()); + } + + BoolExpr withoutApproximation(BoolExpr expr, List terms) { + BoolExpr[] falses = new BoolExpr[terms.size()]; + Arrays.fill(falses, ctx.mkFalse()); + return (BoolExpr) expr.substitute(terms.toArray(new BoolExpr[0]), falses); + } + + private static boolean holds(Model model, BoolExpr condition) { + return model.evaluate(condition, /* completion= */ true).isTrue(); } void addTruncationCondition(BoolExpr condition) { @@ -148,6 +208,7 @@ T withScope(String varName, TranslatedValue value, Supplier action) { this.constraints = new LinkedHashSet<>(); this.inputVariableTypes = new LinkedHashMap<>(); this.truncationConditions = new ArrayList<>(); + this.approximationTerms = new LinkedHashMap<>(); this.symbolTable = new HashMap<>(); this.localScope = new HashMap<>(); } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index fc8f55105..d1af0420f 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -579,6 +579,100 @@ public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exc + " of input state)"); } + private enum ApproximationSourceTestCase { + PARTIALLY_MODELED_FUNCTION("int(string_var) == 5", "calls to `int`"), + // `type` is exact; only its argument is approximate. + APPROXIMATE_ARGUMENT("type(int(string_var)) == int", "calls to `int`"), + APPROXIMATE_ARGUMENT_OF_UNCONDITIONAL_SOURCE( + "type(string_var.matches('a')) == bool", "calls to `matches`"), + UNROLL_LIMIT( + "size(int_list) == 7 && int_list[6] == 1", + "lists and maps longer than the unroll limit (5)"), + MULTIPLE_SOURCES( + "int(string_var) == 5 && size(int_list) == 7 && int_list[6] == 1", + "calls to `int`, lists and maps longer than the unroll limit (5)"), + // Still approximate within the unroll limit, so `int` is a source of its own. + APPROXIMATE_FUNCTION_OF_APPROXIMATE_ARGUMENT( + "size(dyn_list) == 7 && type(dyn_list[6]) == string && int(dyn_list[6]) == 5", + "lists and maps longer than the unroll limit (5), calls to `int`"), + SHORT_CIRCUITED_CALL( + "(false && string_var.matches('a')) || (size(int_list) == 7 && int_list[6] == 1)", + "lists and maps longer than the unroll limit (5)"), + SHORT_CIRCUITED_CALL_AMONG_SOURCES( + "(false && string_var.matches('a'))" + + " || (size(int_list) == 7 && int_list[6] == 1 && int(string_var) == 5)", + "lists and maps longer than the unroll limit (5), calls to `int`"), + UNTAKEN_BRANCH( + "size(int_list) == 7 && (b ? int_list[6] == 1 : int(string_var) == 5) && !b", + "calls to `int`"), + OPTIONAL_SELECT_WITH_AXIOM( + "(false && string_int_map.?k.hasValue()) || int(string_var) == 5", "calls to `int`"); + + private final String expr; + private final String expectedSources; + + ApproximationSourceTestCase(String expr, String expectedSources) { + this.expr = expr; + this.expectedSources = expectedSources; + } + } + + @Test + public void isSatisfiable_approximate_listsApproximationSources( + @TestParameter ApproximationSourceTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.reason()) + .isEqualTo( + "Inconclusive: a satisfying input may exist, but it depends on what the verifier" + + " doesn't model exactly: " + + testCase.expectedSources + + "."); + } + + private enum UninterpretedFunctionSourceTestCase { + TWO_FUNCTIONS("f(x) == 1 && g(y) == 2", "calls to `f`, calls to `g`"), + SHORT_CIRCUITED_FUNCTION("(false && f(x) == 1) || g(y) == 2", "calls to `g`"), + SAME_FUNCTION_TWICE("f(x) == 1 && f(y) == 2", "calls to `f`"); + + private final String expr; + private final String expectedSources; + + UninterpretedFunctionSourceTestCase(String expr, String expectedSources) { + this.expr = expr; + this.expectedSources = expectedSources; + } + } + + @Test + public void isSatisfiable_uninterpretedFunctions_listsApproximationSources( + @TestParameter UninterpretedFunctionSourceTestCase testCase) throws Exception { + CelCompiler celCompiler = + CEL.toCompilerBuilder() + .addFunctionDeclarations( + CelFunctionDecl.newFunctionDeclaration( + "f", + CelOverloadDecl.newGlobalOverload("f_int", SimpleType.INT, SimpleType.INT)), + CelFunctionDecl.newFunctionDeclaration( + "g", + CelOverloadDecl.newGlobalOverload("g_int", SimpleType.INT, SimpleType.INT))) + .build(); + CelAbstractSyntaxTree ast = celCompiler.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER_WITHOUT_ORACLE.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.reason()) + .isEqualTo( + "Inconclusive: a satisfying input may exist, but it depends on what the verifier" + + " doesn't model exactly: " + + testCase.expectedSources + + "."); + } + @Test public void isSatisfiable_approximate_returnsPotentialSatisfyingInput() throws Exception { CelAbstractSyntaxTree ast = CEL.compile("int('123') == 123 ? x > 5 : false").getAst(); @@ -586,7 +680,7 @@ public void isSatisfiable_approximate_returnsPotentialSatisfyingInput() throws E CelVerificationResult result = VERIFIER.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); - assertThat(result.message()).contains("Inconclusive: a satisfying model may exist"); + assertThat(result.message()).contains("Inconclusive: a satisfying input may exist"); assertThat(result.message()).contains("Potential satisfying input:"); assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)"); } @@ -1318,7 +1412,8 @@ public void isAlwaysTrue_approximateOperandWithUnknown_inconclusive() throws Exc CelVerificationResult result = verifier.isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); - assertThat(result.message()).contains("depends on approximations"); + assertThat(result.message()) + .contains("doesn't model exactly: lists and maps longer than the unroll limit (5)."); } @Test @@ -2130,6 +2225,34 @@ private EquivalenceInconclusiveTestCase(String exprA, String exprB) { } } + @Test + public void verifyEquivalence_dynComprehensionRange_listedAsApproximationSource() + throws Exception { + CelAbstractSyntaxTree astA = CEL.compile("dyn_var.all(e, e > 0)").getAst(); + CelAbstractSyntaxTree astB = CEL.compile("dyn_var.all(e, e < 0)").getAst(); + + CelVerificationResult result = VERIFIER.verifyEquivalence(astA, astB); + + assertThat(result.reason()) + .isEqualTo( + "Inconclusive: a divergence may exist, but it depends on what the verifier doesn't" + + " model exactly: comprehensions over `dyn` values."); + } + + @Test + public void verifyEquivalence_unknownResults_listedAsApproximationSource() throws Exception { + CelAbstractSyntaxTree astA = CEL.compile("unknown_var * 1").getAst(); + CelAbstractSyntaxTree astB = CEL.compile("unknown_var + 0").getAst(); + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.addUnknownIdentifier("unknown_var")); + + CelVerificationResult result = verifier.verifyEquivalence(astA, astB); + + assertThat(result.reason()) + .isEqualTo( + "Inconclusive: a divergence may exist, but it depends on what the verifier doesn't" + + " model exactly: unknown results, which are compared only by their origin."); + } + @Test public void verifyEquivalence_inconclusive( @TestParameter EquivalenceInconclusiveTestCase testCase) throws Exception { @@ -3020,7 +3143,7 @@ public void isAlwaysTrue_dynamicFunction_inconclusive() throws Exception { CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); - assertThat(result.message()).contains("depends on approximations"); + assertThat(result.message()).contains("doesn't model exactly: calls to `request`."); } @Test @@ -3718,7 +3841,8 @@ public void isAlwaysTrue_customComprehensionWithLoopCondition_inconclusive() thr CelVerificationResult result = verifier.isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); - assertThat(result.message()).contains("depends on approximations"); + assertThat(result.message()) + .contains("doesn't model exactly: comprehensions with a loop condition."); } @Test