Skip to content

Don't trust static types that the type checker narrowed from dyn #1470

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

Open
copybara-service wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Don't trust static types that the type checker narrowed from dyn #1470

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
86 changes: 48 additions & 38 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@

package dev.cel.verifier;

import static com.google.common.base.Preconditions.checkArgument;

import com.google.common.collect.ImmutableList;
import com.google.common.collect.ImmutableSet;
import com.google.common.collect.ImmutableSortedSet;
Expand Down Expand Up @@ -111,8 +113,8 @@ Set<Expr<?>> getInputVariables() {
* Binds an identifier name in the symbol table to an already-translated value. Used to bind
* reserved policy symbols such as 'rule.result' to the composed policy graph.
*/
void bindSymbol(String varName, TranslatedValue value) {
context.bindSymbol(varName, value);
void bindSymbol(String varName, TranslatedValue value, CelAbstractSyntaxTree ast) {
context.bindSymbol(varName, value, ast);
}

TranslatedValue translate(CelAbstractSyntaxTree ast) {
Expand Down Expand Up @@ -439,6 +441,15 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
long exprId = expr.id();
String functionName = call.function();
ImmutableList<CelExpr> argsAst = call.args();
if (functionName.equals(Operator.OPTIONAL_SELECT.getFunction())) {
checkArgument(
!call.target().isPresent()
&& argsAst.size() == 2
&& argsAst.get(1).constantOrDefault().getKind() == CelConstant.Kind.STRING_VALUE,
"Malformed AST: operator %s expects an operand and a field name",
Operator.OPTIONAL_SELECT);
return structTranslator.translateSelect(expr, ast);
}

List<TranslatedValue> args = new ArrayList<>();

Expand All @@ -453,42 +464,41 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {

return operatorTranslator
.translateFunctionCall(functionName, args, exprId, ast)
.map(
tv -> {
if (mayEmbedArgs(functionName, ast.getTypeOrThrow(exprId))) {
propagateTruncatedTypeConstraint(
tv.z3Expr(), Iterables.transform(args, TranslatedValue::z3Expr));
}
return TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate());
})
.orElseGet(
() -> {
// Uninterpreted function
Sort[] argSorts = new Sort[args.size()];
Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
FuncDecl<?> funcDecl =
typeSystem.internFuncDecl(
uninterpretedFunctionSymbol(exprId, ast),
argSorts,
typeSystem.celValueSort());

Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
context.addConstraint(
typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast));
context.addConstraint(ctx.mkNot(typeSystem.isUnknown(callRes)));
context.addConstraint(ctx.mkNot(typeSystem.isError(callRes)));

// The solver picks the result freely, so a model depending on it is never exact.
return TranslatedValue.propagateStrict(
ctx,
typeSystem,
functionName,
callRes,
Optional.of(expr),
/* baseTaint= */ context.recordCallApproximation(functionName, ctx.mkTrue()),
args);
});
.map(tv -> {
if (mayEmbedArgs(functionName, ast.getTypeOrThrow(exprId))) {
propagateTruncatedTypeConstraint(
tv.z3Expr(), Iterables.transform(args, TranslatedValue::z3Expr));
}
return TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate());
})
.orElseGet(() -> {
// Uninterpreted function
Sort[] argSorts = new Sort[args.size()];
Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
FuncDecl<?> funcDecl =
typeSystem.internFuncDecl(
uninterpretedFunctionSymbol(exprId, ast), argSorts, typeSystem.celValueSort());

Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
// A narrowed result's static type doesn't constrain it.
if (!context.mayBeNarrowed(expr, ast)) {
context.addConstraint(
typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast));
}
context.addConstraint(ctx.mkNot(typeSystem.isUnknown(callRes)));
context.addConstraint(ctx.mkNot(typeSystem.isError(callRes)));

// The solver picks the result freely, so a model depending on it is never exact.
return TranslatedValue.propagateStrict(
ctx,
typeSystem,
functionName,
callRes,
Optional.of(expr),
/* baseTaint= */ context.recordCallApproximation(functionName, ctx.mkTrue()),
args);
});
}

/**
Expand Down
2 changes: 1 addition & 1 deletion 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 @@ -267,7 +267,7 @@ CelVerificationResult verifyImplication(

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

TranslatedValue assumeTv = translator.translate(assumeAst);
Expand Down
31 changes: 25 additions & 6 deletions verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -187,13 +187,32 @@ private TranslatedValue translateDynamicComprehension(
ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))));
context.addUnmodeledResult(isTruncated);

if (isAllMacro(comp) || isExistsMacro(comp)) {
return unrollAllAndExists(
celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
} else {
return unrollMapAndFilter(
celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
TranslatedValue result =
isAllMacro(comp) || isExistsMacro(comp)
? unrollAllAndExists(
celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv)
: unrollMapAndFilter(
celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv);
// Only for speed: a range that isn't narrowed always has its static kind.
if (!context.mayBeNarrowed(comp.iterRange(), ast)) {
return result;
}
// The type checker may have narrowed the range's type (e.g. `dyn_var.orValue([1])` is typed
// list(int)), so it may be the other kind, or not a list or map at all.
BoolExpr isListOrMap = ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange));
BoolExpr isOtherKind =
context.recordApproximation(
"comprehensions over `dyn` values", ctx.mkAnd(ctx.mkNot(isValidRange), isListOrMap));
context.addUnmodeledResult(isOtherKind);
BoolExpr isNotRange = ctx.mkNot(ctx.mkOr(isListOrMap, typeSystem.isErrorOrUnknown(iterRange)));
return TranslatedValue.create(
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
.addCase(isOtherKind, mkParameterizedUnknown(celExpr, ast))
.addCase(isNotRange, typeSystem.mkError())
.build(result.z3Expr()),
celExpr,
typeSystem,
CelZ3Exprs.mkOrFlattened(ctx, result.isApproximate(), isOtherKind));
}

private <T> T withIterationScope(
Expand Down
Loading
Loading