From cfd4a3d12a8f2956d58e1e3f5e861325001d226d Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 28 Oct 2026 16:04:54 -0700 Subject: [PATCH] Make counterexample generator resilient against self references PiperOrigin-RevId: 1009240915 --- .../cel/verifier/CelZ3CounterexampleGenerator.java | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 95fe6f461..571a005e5 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -45,6 +45,7 @@ final class CelZ3CounterexampleGenerator { private final Context ctx; private final CelZ3TypeSystem typeSystem; private final Model model; + private final Set> valuesOnPath; static String generate( Context ctx, @@ -78,6 +79,16 @@ static String generate( // Formats a model value as a CEL literal where one exists. private String format(Expr expr) { + // Refs are uninterpreted, so Z3 may return a cyclic model (e.g. a map containing itself). + if (!valuesOnPath.add(expr)) { + return ""; + } + String formatted = formatValue(expr); + valuesOnPath.remove(expr); + return formatted; + } + + private String formatValue(Expr expr) { FuncDecl decl = expr.getFuncDecl(); Expr[] args = expr.getArgs(); @@ -274,5 +285,6 @@ private CelZ3CounterexampleGenerator(Context ctx, CelZ3TypeSystem typeSystem, Mo this.ctx = ctx; this.typeSystem = typeSystem; this.model = model; + this.valuesOnPath = new HashSet<>(); } }