Skip to content

Internal Changes #1262

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
copybara-service wants to merge 1 commit into from
Closed

Internal Changes #1262

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions verifier/src/main/java/dev/cel/verifier/BUILD.bazel
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
317 changes: 146 additions & 171 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop

Large diffs are not rendered by default.

87 changes: 43 additions & 44 deletions verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down Expand Up @@ -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 {
Expand All @@ -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) {
Expand All @@ -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;
}
Expand Down Expand Up @@ -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(
Expand All @@ -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);
Expand Down Expand Up @@ -262,10 +263,10 @@ CelVerificationResult verifyImplication(
Map<String, CelAbstractSyntaxTree> 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<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
Preconditions.checkArgument(
checkArgument(
entry.getValue().isChecked(),
"boundSymbol AST for '%s' must be type-checked.",
entry.getKey());
Expand All @@ -276,22 +277,20 @@ CelVerificationResult verifyImplication(
new CelAstToZ3Translator(
ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider);

List<BoolExpr> taints = new ArrayList<>();
for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
TranslatedValue tv = translator.translate(entry.getValue());
translator.bindSymbol(entry.getKey(), tv);
}

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()),
Expand Down Expand Up @@ -513,21 +512,6 @@ private static String getCounterexampleString(
ctx, typeSystem, model, isApproximate, isCounterexample);
}

CelVerifierZ3Impl(
Duration timeout,
int comprehensionUnrollLimit,
ImmutableSet<String> 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,
Expand All @@ -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);
Expand Down Expand Up @@ -567,4 +551,19 @@ private SolverRunResult(SolverOutcome outcome, @Nullable Model model, @Nullable
this.reason = reason;
}
}

private CelVerifierZ3Impl(
Duration timeout,
int comprehensionUnrollLimit,
ImmutableSet<String> 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;
}
}
Loading
Loading