Internal Changes

PiperOrigin-RevId: 951556122

Author: l46kok

verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

@@ -297,7 +297,10 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast
     }
 
     Expr<?> result = typeSystem.wrapList(listRef);
-    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
+    boolean hasOptionals = !createList.optionalIndices().isEmpty();
+    BoolExpr baseTaint = hasOptionals ? ctx.mkTrue() : ctx.mkFalse();
+    return TranslatedValue.propagateStrict(
+        ctx, typeSystem, result, Optional.of(celExpr), baseTaint, elementsTv);
   }
 
   private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) {
@@ -331,7 +334,11 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast)
     typeConstraints.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq));
 
     Expr<?> result = typeSystem.wrapMap(mapRef);
-    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
+    boolean hasOptionals =
+        createMap.entries().stream().anyMatch(CelExpr.CelMap.Entry::optionalEntry);
+    BoolExpr baseTaint = hasOptionals ? ctx.mkTrue() : ctx.mkFalse();
+    return TranslatedValue.propagateStrict(
+        ctx, typeSystem, result, Optional.of(celExpr), baseTaint, elementsTv);
   }
 
   private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) {
@@ -396,7 +403,11 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
     typeConstraints.add(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence));
 
     Expr<?> result = typeSystem.wrapMessage(msgRef);
-    return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
+    boolean hasOptionals =
+        createStruct.entries().stream().anyMatch(CelExpr.CelStruct.Entry::optionalEntry);
+    BoolExpr baseTaint = hasOptionals ? ctx.mkTrue() : ctx.mkFalse();
+    return TranslatedValue.propagateStrict(
+        ctx, typeSystem, result, Optional.of(celExpr), baseTaint, elementsTv);
   }
 
   private Expr<?> getDefaultValueForType(CelType type) {
@@ -644,6 +655,12 @@ private <T> T withScope(String varName, TranslatedValue value, Supplier<T> actio
   private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSyntaxTree ast) {
     CelComprehension comp = celExpr.comprehension();
     CelExpr iterRangeExpr = comp.iterRange();
+    if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.IDENT) {
+      TranslatedValue boundTv = symbolTable.get(iterRangeExpr.ident().name());
+      if (boundTv != null) {
+        iterRangeExpr = boundTv.celExpr().orElse(iterRangeExpr);
+      }
+    }
     List<IterationElement> iterationElements = new ArrayList<>();
     List<BoolExpr> taints = new ArrayList<>();
     List<Expr<?>> allRangeElems = new ArrayList<>();

verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java

@@ -42,6 +42,7 @@
 import dev.cel.common.ast.CelExpr.CelCall;
 import dev.cel.common.types.ListType;
 import dev.cel.common.types.MapType;
+import dev.cel.common.types.OptionalType;
 import dev.cel.common.types.ProtoMessageTypeProvider;
 import dev.cel.common.types.SimpleType;
 import dev.cel.common.types.StructTypeReference;
@@ -87,6 +88,7 @@ public final class CelVerifierZ3ImplTest {
           .addVar("y", SimpleType.INT)
           .addVar("a", SimpleType.BOOL)
           .addVar("b", SimpleType.BOOL)
+          .addVar("opt_var", OptionalType.create(SimpleType.INT))
           .addVar("role", SimpleType.STRING)
           .addVar("country", SimpleType.STRING)
           .addVar("port", SimpleType.INT)
@@ -1250,8 +1252,8 @@ private enum EquivalenceInconclusiveTestCase {
         "size(int_list) == 6 ? int_list.map(x, 2.0) : [1.0]"),
     TRUNCATION_DIVERGENCE_DIFFERENT_BYTES(
         "size(int_list) == 6 ? int_list.map(x, b'a') : [b'a']",
-        "size(int_list) == 6 ? int_list.map(x, b'b') : [b'a']");
-
+        "size(int_list) == 6 ? int_list.map(x, b'b') : [b'a']"),
+    OPTIONAL_DIFFERENT_VALUES("[1, ?opt_var]", "[1]");
     final String exprA;
     final String exprB;