diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index d48faf98f..fead780a5 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -164,6 +164,7 @@ java_library( "CelZ3ExtensionalityAxioms.java", "CelZ3FunctionRegistry.java", "CelZ3OperatorTranslator.java", + "CelZ3TranslationContext.java", "CelZ3TypeConstraintGenerator.java", "TranslatedValue.java", ], diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 20050cd82..98b451480 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -91,15 +91,13 @@ final class CelAstToZ3Translator { private static final long MAX_UINT32 = 0xFFFFFFFFL; private final Context ctx; private final CelZ3TypeSystem typeSystem; - private final CelZ3OperatorTranslator operatorTranslator; + private final CelZ3TranslationContext context; private final CelZ3TypeConstraintGenerator typeConstraintGenerator; + private final CelZ3OperatorTranslator operatorTranslator; private final Map symbolTable; - private final Set typeConstraints; - private final Map, CelType> inputVariableTypes; private final ImmutableSet unknownIdentifiers; private final int comprehensionUnrollLimit; private final CelTypeProvider typeProvider; - private final List truncationConditions; private final Map> emptyMessageCache; private final Map> listLiteralCache; private Expr emptyListCache; @@ -109,11 +107,11 @@ final class CelAstToZ3Translator { * Returns a set of Z3 boolean expressions representing type constraints for the translated AST. */ Set getTypeConstraints() { - return typeConstraints; + return context.constraints(); } BoolExpr hasTruncation() { - return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions); + return context.hasTruncation(); } CelZ3TypeSystem getTypeSystem() { @@ -149,13 +147,13 @@ TranslatedValue translate(CelAbstractSyntaxTree ast) { Set> mapRefs = new LinkedHashSet<>(); Set> msgRefs = new LinkedHashSet<>(); - for (Expr constraint : typeConstraints) { + for (Expr constraint : context.constraints()) { collectReferences(constraint, visited, listRefs, mapRefs, msgRefs); } collectReferences(result.z3Expr(), visited, listRefs, mapRefs, msgRefs); - this.typeConstraints.addAll( - CelZ3ExtensionalityAxioms.generateAxioms(ctx, typeSystem, listRefs, mapRefs, msgRefs)); + CelZ3ExtensionalityAxioms.generateAxioms(ctx, typeSystem, listRefs, mapRefs, msgRefs) + .forEach(context::addConstraint); return result; } @@ -260,18 +258,18 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as name, n -> { Expr v = ctx.mkConst(n, typeSystem.celValueSort()); - inputVariableTypes.put(v, type); + context.addInputVariable(v, type); // Variables at rest can never be pre-cooked Errors // Basically prevents error being a counterexample of var == var - typeConstraints.add(ctx.mkNot(typeSystem.isError(v))); + context.addConstraint(ctx.mkNot(typeSystem.isError(v))); BoolExpr constraint = typeConstraintGenerator.createTypeConstraint(v, exprId, ast); if (unknownIdentifiers.contains(name)) { - typeConstraints.add(ctx.mkOr(typeSystem.isUnknown(v), constraint)); + context.addConstraint(ctx.mkOr(typeSystem.isUnknown(v), constraint)); } else { - typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(v))); - typeConstraints.add(constraint); + context.addConstraint(ctx.mkNot(typeSystem.isUnknown(v))); + context.addConstraint(constraint); } return TranslatedValue.create( @@ -325,7 +323,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast elementsTv.add(elem); } listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX); - typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq)); + context.addConstraint(ctx.mkEq(typeSystem.getSeq(listRef), seq)); propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values); Expr finalListRef = listRef; cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef)); @@ -380,9 +378,9 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) ctx.mkITE(finalPresence, ctx.mkStore(mapPresence, key, ctx.mkTrue()), mapPresence); } - typeConstraints.add(ctx.mkEq(typeSystem.getMapValues(mapRef), mapValues)); - typeConstraints.add(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence)); - typeConstraints.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); + context.addConstraint(ctx.mkEq(typeSystem.getMapValues(mapRef), mapValues)); + context.addConstraint(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence)); + context.addConstraint(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); Expr result = typeSystem.wrapMap(mapRef); propagateTruncatedTypeConstraint(result, values); @@ -399,7 +397,7 @@ private void propagateTruncatedTypeConstraint(Expr container, Iterable element : elements) { - typeConstraints.add( + context.addConstraint( ctx.mkImplies(typeSystem.hasTruncatedTypeConstraint(element), hasTruncated)); } } @@ -488,10 +486,10 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a ctx.mkITE(shouldBypass, msgPresence, ctx.mkStore(msgPresence, key, ctx.mkTrue())); } - typeConstraints.add( + context.addConstraint( ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString(createStruct.messageName()))); - typeConstraints.add(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues)); - typeConstraints.add(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence)); + context.addConstraint(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues)); + context.addConstraint(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence)); Expr result = typeSystem.wrapMessage(msgRef); return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv); @@ -744,7 +742,7 @@ private Expr getDefaultValueForType(CelType type) { if (type instanceof ListType) { if (emptyListCache == null) { emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getSeq(emptyListCache), ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())))); @@ -754,15 +752,15 @@ private Expr getDefaultValueForType(CelType type) { if (type instanceof MapType) { if (emptyMapCache == null) { emptyMapCache = typeSystem.mkMapRefConst(EMPTY_MAP_PREFIX); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMapPresence(emptyMapCache), ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()))); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMapValues(emptyMapCache), ctx.mkConstArray(typeSystem.celValueSort(), typeSystem.mkUnknown()))); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMapKeys(emptyMapCache), ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())))); @@ -776,15 +774,15 @@ private Expr getDefaultValueForType(CelType type) { messageName, name -> { Expr ref = typeSystem.mkMessageRefConst(EMPTY_MSG_REF_PREFIX + name); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMsgPresence(ref), ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse()))); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMsgValues(ref), ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown()))); - typeConstraints.add(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name))); + context.addConstraint(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name))); return ref; }); return typeSystem.wrapMessage(msgRef); @@ -808,7 +806,7 @@ private FieldAccess getMapAccess(Expr operand, String field, BoolExpr typeGua BoolExpr presence = (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str); Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str); - constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); + context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } @@ -818,14 +816,10 @@ private FieldAccess getMsgAccess(Expr operand, String field, BoolExpr typeGua BoolExpr presence = (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str); Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str); - constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); + context.constrainValidValue(CelZ3Exprs.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(); @@ -873,7 +867,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a Expr fieldAccess = select.testOnly() ? typeSystem.wrapBool(presenceResult) : valueResult; - typeConstraints.add(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast)); + context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast)); TranslatedValue result = TranslatedValue.propagateStrict( @@ -938,10 +932,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { Expr[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new); Expr callRes = ctx.mkApp(funcDecl, exprArgs); - typeConstraints.add( + context.addConstraint( typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast)); - typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); - typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); + 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( @@ -1120,7 +1114,7 @@ private TranslatedValue translateDynamicComprehension( BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange); BoolExpr isTruncated = ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))); - truncationConditions.add(isTruncated); + context.addTruncationCondition(isTruncated); if (isAllMacro(comp) || isExistsMacro(comp)) { return unrollAllAndExists( @@ -1312,13 +1306,13 @@ private void constrainIterationElement( // Constrain out-of-bounds elements to prevent MBQI from infinitely instantiating list/map // axioms BoolExpr outOfBounds = ctx.mkGe(idx, lengthExpr); - typeConstraints.add(ctx.mkImplies(outOfBounds, ctx.mkEq(xVal, typeSystem.mkUnknown()))); + context.addConstraint(ctx.mkImplies(outOfBounds, ctx.mkEq(xVal, typeSystem.mkUnknown()))); // If we are iterating over a map, we can optionally bind the sequence elements // to the map presence array to ensure the solver knows they correspond. if (mapPresence != null) { Expr selectExpr = ctx.mkSelect(mapPresence, xVal); - typeConstraints.add(ctx.mkImplies(inBounds, (BoolExpr) selectExpr)); + context.addConstraint(ctx.mkImplies(inBounds, (BoolExpr) selectExpr)); } } @@ -1502,24 +1496,13 @@ private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) this.ctx = ctx; this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.typeSystem = new CelZ3TypeSystem(ctx, parameterizeUnknowns); - this.typeConstraints = new LinkedHashSet<>(); - this.inputVariableTypes = new HashMap<>(); - this.typeConstraintGenerator = - new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit); - this.operatorTranslator = - new CelZ3OperatorTranslator( - ctx, - typeSystem, - this.typeConstraints::add, - typeConstraintGenerator::createTypeConstraintForType, - val -> inputVariableTypes.getOrDefault(val, SimpleType.DYN), - functionRegistry, - comprehensionUnrollLimit); + this.context = new CelZ3TranslationContext(ctx, typeSystem, comprehensionUnrollLimit); + this.typeConstraintGenerator = context.typeConstraintGenerator(); + this.operatorTranslator = new CelZ3OperatorTranslator(context, functionRegistry); 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/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index eb4b7636e..587f18f19 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -47,18 +47,14 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import java.util.function.BiFunction; -import java.util.function.Consumer; -import java.util.function.Function; /** Handles mapping CEL Operators to Z3 SMT logic. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3OperatorTranslator { private final Context ctx; private final CelZ3TypeSystem typeSystem; - private final Consumer constraintSink; - private final BiFunction, CelType, BoolExpr> typeConstraintGenerator; - private final Function, CelType> guaranteedTypes; + private final CelZ3TranslationContext context; + private final CelZ3TypeConstraintGenerator typeConstraintGenerator; private final CelZ3FunctionRegistry functionRegistry; private final int comprehensionUnrollLimit; @@ -117,7 +113,7 @@ Optional translateFunctionCall( } Optional evaluatedResultOpt = - translator.translate(ctx, typeSystem, constraintSink, z3Args, argApproximations); + translator.translate(ctx, typeSystem, context::addConstraint, z3Args, argApproximations); if (!evaluatedResultOpt.isPresent()) { continue; @@ -197,10 +193,10 @@ private BoolExpr constrainInWitnessTypes( SeqExpr seq = typeSystem.getSeq(typeSystem.getListRef(rhs)); for (Expr cand : candidates) { BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(cand)); - constraintSink.accept( + context.addConstraint( ctx.mkImplies( ctx.mkAnd(typeSystem.isList(rhs), structContains), - typeConstraintGenerator.apply(cand, elemType))); + typeConstraintGenerator.createTypeConstraintForType(cand, elemType))); } // With a concrete element type, the constraints above cover any match in rhs. return isConcrete(elemType) @@ -210,10 +206,12 @@ private BoolExpr constrainInWitnessTypes( // 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( + context.addConstraint( ctx.mkImplies( ctx.mkAnd(typeSystem.isMap(rhs), inMap), - typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType()))); + context + .typeConstraintGenerator() + .createTypeConstraintForType(lhs, ((MapType) rhsType).keyType()))); return isTruncatedMap(rhs); } return CelZ3Exprs.mkOrFlattened( @@ -677,10 +675,12 @@ private BoolExpr unrollListEquality( private void constrainListElement(SeqExpr seq, IntExpr idx, Expr elem, CelType listType) { if (listType instanceof ListType) { - constraintSink.accept( + context.addConstraint( ctx.mkImplies( ctx.mkLt(idx, ctx.mkLength(seq)), - typeConstraintGenerator.apply(elem, ((ListType) listType).elemType()))); + context + .typeConstraintGenerator() + .createTypeConstraintForType(elem, ((ListType) listType).elemType()))); } } @@ -754,12 +754,12 @@ private Expr buildListIndex( ctx.mkLt((ArithExpr) index, ctx.mkLength(seq))); Expr val = ctx.mkNth(seq, (ArithExpr) index); - constrainValidElement(ctx.mkAnd(typeGuard, inBounds), val); + context.constrainValidValue(ctx.mkAnd(typeGuard, inBounds), val); if (isOptional) { Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val); - constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); - constraintSink.accept(typeSystem.optHasValue(resultOptRef)); + context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); + context.addConstraint(typeSystem.optHasValue(resultOptRef)); return ctx.mkITE( inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); } @@ -767,10 +767,6 @@ 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(); @@ -925,12 +921,12 @@ private Expr buildMapIndex( .addCase(isDouble, doubleProbe.altVal) .build(valOrig); - constrainValidElement(ctx.mkAnd(typeGuard, finalInMap), finalVal); + context.constrainValidValue(ctx.mkAnd(typeGuard, finalInMap), finalVal); if (isOptional) { Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal); - constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal)); - constraintSink.accept(typeSystem.optHasValue(resultOptRef)); + context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal)); + context.addConstraint(typeSystem.optHasValue(resultOptRef)); return ctx.mkITE( finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); } @@ -1030,9 +1026,10 @@ private TranslatedValue buildAndConstrainIndex( CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType; BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))); - BoolExpr typeConstraint = typeConstraintGenerator.apply(actualValue, finalType); + BoolExpr typeConstraint = + typeConstraintGenerator.createTypeConstraintForType(actualValue, finalType); if (isLhsTypeGuaranteed) { - constraintSink.accept(ctx.mkImplies(isDefined, typeConstraint)); + context.addConstraint(ctx.mkImplies(isDefined, typeConstraint)); return TranslatedValue.create(actualValue, typeSystem, ctx.mkFalse()); } // The type checker may narrow other static types (e.g. `(['a'] + dyn_var)[1]` is typed @@ -1118,7 +1115,7 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS * so constraints derived from those could exclude valid inputs. */ private CelType guaranteedType(TranslatedValue val) { - return guaranteedTypes.apply(val.z3Expr()); + return context.guaranteedType(val.z3Expr()); } /** @@ -1170,20 +1167,12 @@ private BoolExpr mayObserveTruncatedTypeConstraint( .collect(toImmutableList())); } - CelZ3OperatorTranslator( - Context ctx, - CelZ3TypeSystem typeSystem, - Consumer constraintSink, - BiFunction, CelType, BoolExpr> typeConstraintGenerator, - Function, CelType> guaranteedTypes, - CelZ3FunctionRegistry functionRegistry, - int comprehensionUnrollLimit) { - this.ctx = ctx; - this.typeSystem = typeSystem; - this.constraintSink = constraintSink; - this.typeConstraintGenerator = typeConstraintGenerator; - this.guaranteedTypes = guaranteedTypes; + CelZ3OperatorTranslator(CelZ3TranslationContext context, CelZ3FunctionRegistry functionRegistry) { + this.ctx = context.ctx(); + this.typeSystem = context.typeSystem(); + this.context = context; + this.typeConstraintGenerator = context.typeConstraintGenerator(); this.functionRegistry = functionRegistry; - this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.comprehensionUnrollLimit = context.comprehensionUnrollLimit(); } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java new file mode 100644 index 000000000..14c8bdd8e --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java @@ -0,0 +1,98 @@ +// Copyright 2026 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +package dev.cel.verifier; + +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import dev.cel.common.types.CelType; +import dev.cel.common.types.SimpleType; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Set; + +/** State shared by the translators of a single verification query. */ +final class CelZ3TranslationContext { + + private final Context ctx; + private final CelZ3TypeSystem typeSystem; + private final CelZ3TypeConstraintGenerator typeConstraintGenerator; + private final int comprehensionUnrollLimit; + private final Set constraints; + private final Map, CelType> inputVariableTypes; + private final List truncationConditions; + + Context ctx() { + return ctx; + } + + CelZ3TypeSystem typeSystem() { + return typeSystem; + } + + CelZ3TypeConstraintGenerator typeConstraintGenerator() { + return typeConstraintGenerator; + } + + int comprehensionUnrollLimit() { + return comprehensionUnrollLimit; + } + + /** Returns the constraints asserted so far, in insertion order. */ + Set constraints() { + return Collections.unmodifiableSet(constraints); + } + + void addConstraint(BoolExpr constraint) { + constraints.add(constraint); + } + + /** Constrains {@code value} to be neither an error nor unknown whenever {@code guard} holds. */ + void constrainValidValue(BoolExpr guard, Expr value) { + addConstraint(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value)))); + } + + void addInputVariable(Expr variable, CelType declaredType) { + inputVariableTypes.put(variable, declaredType); + } + + /** Returns the declared type of an input variable, or dyn for any other value. */ + CelType guaranteedType(Expr value) { + return inputVariableTypes.getOrDefault(value, SimpleType.DYN); + } + + void addTruncationCondition(BoolExpr condition) { + truncationConditions.add(condition); + } + + BoolExpr hasTruncation() { + return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions); + } + + CelZ3TranslationContext(Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) { + this.ctx = ctx; + this.typeSystem = typeSystem; + this.typeConstraintGenerator = + new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit); + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.constraints = new LinkedHashSet<>(); + this.inputVariableTypes = new HashMap<>(); + this.truncationConditions = new ArrayList<>(); + } +}