Skip to content

Select fields from and index optionals, and error on .? of undeclared fields #1469

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

Select fields from and index optionals, and error on .? of undeclared fields #1469

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
18 changes: 11 additions & 7 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 @@ -107,13 +109,6 @@ Set<Expr<?>> getInputVariables() {
return context.inputVariables();
}

/**
* Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true.
*/
BoolExpr isTrue(Expr<?> celValue) {
return ctx.mkAnd(typeSystem.isBool(celValue), (BoolExpr) typeSystem.unwrapBool(celValue));
}

/**
* 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.
Expand Down Expand Up @@ -446,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 Down
6 changes: 3 additions & 3 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 @@ -273,8 +273,8 @@ CelVerificationResult verifyImplication(
TranslatedValue assumeTv = translator.translate(assumeAst);
TranslatedValue assertTv = translator.translate(assertAst);

BoolExpr assumeCondition = translator.isTrue(assumeTv.z3Expr());
BoolExpr assertCondition = translator.isTrue(assertTv.z3Expr());
BoolExpr assumeCondition = translator.getTypeSystem().isTrue(assumeTv.z3Expr());
BoolExpr assertCondition = translator.getTypeSystem().isTrue(assertTv.z3Expr());
BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition));

BoolExpr combinedTaint =
Expand Down Expand Up @@ -305,7 +305,7 @@ private CelVerificationResult checkSatisfiability(
CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false);

TranslatedValue tv = translator.translate(ast);
BoolExpr isTrue = translator.isTrue(tv.z3Expr());
BoolExpr isTrue = translator.getTypeSystem().isTrue(tv.z3Expr());
if (searchForCounterexample) {
return search(
ctx,
Expand Down
651 changes: 400 additions & 251 deletions verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java
View file
Open in desktop

Large diffs are not rendered by default.

76 changes: 63 additions & 13 deletions verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@
import com.microsoft.z3.SeqExpr;
import dev.cel.common.CelAbstractSyntaxTree;
import dev.cel.common.ast.CelExpr;
import dev.cel.common.ast.CelExpr.ExprKind;
import dev.cel.common.internal.ProtoTimeUtils;
import dev.cel.common.types.CelKind;
import dev.cel.common.types.CelType;
Expand Down Expand Up @@ -536,25 +537,53 @@ private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGua
return new FieldAccess(presence, value);
}

/**
* Translates {@code e.f}, {@code has(e.f)} or {@code e.?f} (an optional of {@code e.f} if {@code
* has(e.f)}, else empty).
*/
TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
CelExpr.CelSelect select = celExpr.select();
boolean isOptional = celExpr.getKind() == ExprKind.Kind.CALL;
CelExpr operandExpr = isOptional ? celExpr.call().args().get(0) : celExpr.select().operand();
String field =
isOptional
? celExpr.call().args().get(1).constant().stringValue()
: celExpr.select().field();
boolean testOnly = !isOptional && celExpr.select().testOnly();
long exprId = celExpr.id();
TranslatedValue operandTv = translateExpr(select.operand(), ast);
TranslatedValue operandTv = translateExpr(operandExpr, ast);
Expr<?> operand = operandTv.z3Expr();
String field = select.field();
CelType operandType = extractAstTypeOrDefault(ast, select.operand().id());
CelType operandType = extractAstTypeOrDefault(ast, operandExpr.id());
// Selecting from an optional selects from its value optionally (e.g. `optional.of({}).a` is
// `optional.none()`). Performance only: an operand of a known type other than optional isn't.
boolean mayBeOptional =
operandType instanceof OptionalType
|| !CelZ3OperatorTranslator.isStaticallyKnown(operandType);
BoolExpr isOptionalOperand = ctx.mkFalse();
BoolExpr hasValue = ctx.mkFalse();
BoolExpr shouldEvaluate = ctx.mkTrue();
if (mayBeOptional) {
Expr<?> optRef = typeSystem.getOptionalRef(operand);
isOptionalOperand = typeSystem.isOptional(operand);
hasValue = typeSystem.optHasValue(optRef);
shouldEvaluate = (BoolExpr) ctx.mkITE(isOptionalOperand, hasValue, ctx.mkTrue());
operand = ctx.mkITE(isOptionalOperand, typeSystem.getOptionalValue(optRef), operand);
}
if (operandType instanceof OptionalType) {
// Performance only: reads the value by its static type.
operandType = operandType.parameters().get(0);
}

Expr<?> presenceResult;
Expr<?> valueResult;
BoolExpr unmodeledMessage = ctx.mkFalse();
BoolExpr presenceError = ctx.mkFalse();

if (operandType instanceof MapType) {
FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue());
FieldAccess mapAcc = getMapAccess(operand, field, shouldEvaluate);
presenceResult = mapAcc.presence;
valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
} else if (operandType.kind() == CelKind.STRUCT) {
FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue());
FieldAccess msgAcc = getMsgAccess(operand, field, shouldEvaluate);
presenceResult = msgAcc.presence;
Expr<?> defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId));
valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal);
Expand All @@ -563,8 +592,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
BoolExpr isMap = typeSystem.isMap(operand);
BoolExpr isMessage = typeSystem.isMessage(operand);

FieldAccess mapAcc = getMapAccess(operand, field, isMap);
FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkAnd(shouldEvaluate, isMap));
FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkAnd(shouldEvaluate, isMessage));

presenceResult =
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
Expand All @@ -590,13 +619,13 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
msgRead.addCase(isType, typeSystem.mkError());
continue;
}
if (select.testOnly()) {
if (testOnly) {
continue;
}
CelType fieldType = declared.get().type();
context.addConstraint(
ctx.mkImplies(
ctx.mkAnd(isMessage, isType, msgAcc.presence),
ctx.mkAnd(shouldEvaluate, isMessage, isType, msgAcc.presence),
typeConstraintGenerator.createTypeConstraintForType(msgAcc.value, fieldType)));
msgRead.addCase(
isType, ctx.mkITE(msgAcc.presence, msgAcc.value, getDefaultValueForType(fieldType)));
Expand All @@ -605,7 +634,10 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
unmodeledMessage =
context.recordApproximation(
"messages of types the type provider doesn't declare",
ctx.mkAnd(isMessage, ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType))));
ctx.mkAnd(
shouldEvaluate,
isMessage,
ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType))));
Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
// Testing an undeclared field, or a field of something other than a map or message, errors.
presenceError =
Expand All @@ -622,10 +654,27 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
.build(typeSystem.mkError());
}

// has(e.f), else e.f, or for e.?f and an optional e, an optional of e.f if has(e.f).
Expr<?> fieldAccess =
select.testOnly()
testOnly
? typeSystem.withRuntimeError(typeSystem.wrapBool(presenceResult), presenceError)
: valueResult;
Expr<?> chained = fieldAccess;
if (!testOnly && (isOptional || mayBeOptional)) {
chained =
ctx.mkITE(
presenceError,
typeSystem.mkError(),
ctx.mkITE(
(BoolExpr) presenceResult,
context.mkOptionalOf(valueResult),
typeSystem.mkOptionalNone()));
fieldAccess = isOptional ? chained : valueResult;
}
if (mayBeOptional) {
Expr<?> empty = testOnly ? typeSystem.mkBool(false) : typeSystem.mkOptionalNone();
fieldAccess = ctx.mkITE(isOptionalOperand, ctx.mkITE(hasValue, chained, empty), fieldAccess);
}

context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast));

Expand All @@ -636,7 +685,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) {
return operandType.kind() == CelKind.STRUCT
? result
: result.withApproximation(
CelZ3Exprs.mkOrFlattened(ctx, context.isTruncatedMap(operand), unmodeledMessage));
CelZ3Exprs.mkOrFlattened(
ctx, ctx.mkAnd(shouldEvaluate, context.isTruncatedMap(operand)), unmodeledMessage));
}

private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) {
Expand Down
8 changes: 8 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,14 @@ void constrainValidValue(BoolExpr guard, Expr<?> value) {
addConstraint(ctx.mkImplies(guard, typeSystem.isValidValue(value)));
}

/** Returns an optional holding {@code value}. */
Expr<?> mkOptionalOf(Expr<?> value) {
Expr<?> optRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), value);
addConstraint(ctx.mkEq(typeSystem.getOptionalValue(optRef), value));
addConstraint(typeSystem.optHasValue(optRef));
return typeSystem.mkOptionalOf(optRef);
}

void addInputVariable(Expr<?> variable, CelType declaredType) {
inputVariableTypes.put(variable, declaredType);
}
Expand Down
5 changes: 5 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -360,6 +360,11 @@ public FPExpr mkFpDouble(double val) {
return ctx.mkFP(val, ctx.mkFPSortDouble());
}

/** Whether the given CelValue is the bool true. */
BoolExpr isTrue(Expr<?> celValue) {
return ctx.mkAnd(isBool(celValue), (BoolExpr) unwrapBool(celValue));
}

/** Checks if the given CelValue is a double. */
public BoolExpr isDouble(Expr<?> val) {
return (BoolExpr) ctx.mkApp(doubleCons.getTesterDecl(), val);
Expand Down
2 changes: 2 additions & 0 deletions verifier/src/main/java/dev/cel/verifier/TranslatedValue.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -199,6 +199,8 @@ private static String extractOpName(CelExpr expr) {
switch (expr.exprKind().getKind()) {
case SELECT:
return "select_" + expr.select().field() + "_" + expr.select().testOnly();
case CALL: // e.?f
return "optional_select_" + expr.call().args().get(1).constant().stringValue();
case STRUCT:
StringBuilder structSb = new StringBuilder("struct_").append(expr.struct().messageName());
for (CelExpr.CelStruct.Entry entry : expr.struct().entries()) {
Expand Down
80 changes: 9 additions & 71 deletions verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,88 +14,26 @@

package dev.cel.verifier.axioms;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Expr;
import com.microsoft.z3.FPExpr;
import com.microsoft.z3.IntExpr;
import com.microsoft.z3.SeqExpr;
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
import java.util.Optional;

/** Axiomatization for CEL's in operator/function (list and map overloads). */
@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types.
public final class InAxiom {
final class InAxiom {

static final CelZ3FunctionAxiom INSTANCE =
CelZ3FunctionAxiom.newBuilder(StandardFunction.IN.functionDecl())
// Matches by terms, which is CEL equality when lhs has the list's element type and that
// type compares by terms; the operator translator compares other lists by CEL equality.
.addBinaryOverloadTranslator(
StandardFunction.Overload.InternalOperator.IN_LIST.celOverloadDecl(),
(ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) -> {
Expr<?> listRef = typeSystem.getListRef(rhsTrans);
SeqExpr<?> seq = typeSystem.getSeq(listRef);

BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(lhsTrans));

BoolExpr isDouble = typeSystem.isDouble(lhsTrans);
FPExpr fpVal = (FPExpr) typeSystem.getDouble(lhsTrans);

BoolExpr isNaN = ctx.mkFPIsNaN(fpVal);
BoolExpr isDoubleZero = ctx.mkFPIsZero(fpVal);

Expr<?> posZeroCel = typeSystem.wrapDouble(typeSystem.mkFpDouble(0.0));
Expr<?> negZeroCel = typeSystem.wrapDouble(typeSystem.mkFpDouble(-0.0));
Expr<?> intZeroCel = typeSystem.wrapInt(ctx.mkInt(0));
Expr<?> uintZeroCel = typeSystem.wrapUint(ctx.mkInt(0));

// CEL follows IEEE-754 where 0.0 == -0.0, and cross-type equality means they also
// equal int 0 and uint 0.
BoolExpr containsAnyZero =
ctx.mkOr(
ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(posZeroCel)),
ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(negZeroCel)),
ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(intZeroCel)),
ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(uintZeroCel)));

// CEL follows IEEE-754 where NaN != NaN.
BoolExpr doubleInList =
(BoolExpr)
ctx.mkITE(
isNaN,
ctx.mkFalse(),
ctx.mkITE(isDoubleZero, containsAnyZero, structContains));

BoolExpr isInt = typeSystem.isInt(lhsTrans);
BoolExpr isUint = typeSystem.isUint(lhsTrans);
BoolExpr isIntOrUint = ctx.mkOr(isInt, isUint);

IntExpr intVal =
(IntExpr)
ctx.mkITE(isInt, typeSystem.getInt(lhsTrans), typeSystem.getUint(lhsTrans));
BoolExpr isIntOrUintZero = ctx.mkEq(intVal, ctx.mkInt(0));

BoolExpr containsIntOrUint =
ctx.mkOr(
ctx.mkAnd(
ctx.mkNot(typeSystem.checkIntOverflow(intVal)),
ctx.mkContains(
(Expr) seq, (Expr) ctx.mkUnit(typeSystem.wrapInt(intVal)))),
ctx.mkAnd(
ctx.mkNot(typeSystem.checkUintOverflow(intVal)),
ctx.mkContains(
(Expr) seq, (Expr) ctx.mkUnit(typeSystem.wrapUint(intVal)))));

BoolExpr intOrUintInList =
(BoolExpr) ctx.mkITE(isIntOrUintZero, containsAnyZero, containsIntOrUint);

BoolExpr isMatch =
(BoolExpr)
ctx.mkITE(
isDouble,
doubleInList,
ctx.mkITE(isIntOrUint, intOrUintInList, structContains));

return Optional.of(typeSystem.wrapBool(isMatch));
})
(ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) ->
Optional.of(
typeSystem.wrapBool(
ctx.mkContains(
(Expr) typeSystem.getSeq(typeSystem.getListRef(rhsTrans)),
(Expr) ctx.mkUnit(lhsTrans)))))
.addBinaryOverloadTranslator(
StandardFunction.Overload.InternalOperator.IN_MAP.celOverloadDecl(),
(ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) ->
Expand Down
Loading
Loading