Skip to content

Commit 4fcf94d

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Prevent spurious counterexamples on maps by tightening its domain
PiperOrigin-RevId: 956295539
1 parent 75e0900 commit 4fcf94d

10 files changed

Lines changed: 108 additions & 69 deletions

File tree

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

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -741,7 +741,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
741741
typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
742742
typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
743743

744-
boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true);
744+
boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
745745
BoolExpr isApprox = ctx.mkBool(!isDynamic);
746746
return TranslatedValue.propagateStrict(
747747
ctx, typeSystem, callRes, Optional.of(expr), isApprox, args);
@@ -877,10 +877,6 @@ private TranslatedValue translateDynamicComprehension(
877877
ArrayExpr mapPresence =
878878
isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null;
879879

880-
if (isMap) {
881-
applyBoundedMapBijection(mapPresence, seq, lengthExpr);
882-
}
883-
884880
BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit));
885881
truncationConditions.add(isTruncated);
886882

@@ -893,14 +889,15 @@ private TranslatedValue translateDynamicComprehension(
893889
}
894890
}
895891

896-
private void applyBoundedMapBijection(
892+
private BoolExpr getBoundedMapBijection(
897893
ArrayExpr mapPresence, SeqExpr<?> seq, ArithExpr lengthExpr) {
894+
List<BoolExpr> constraints = new ArrayList<>();
898895
for (int i = 0; i < comprehensionUnrollLimit; i++) {
899896
for (int j = i + 1; j < comprehensionUnrollLimit; j++) {
900897
BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr);
901898
BoolExpr notEqual =
902899
ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j))));
903-
typeConstraints.add(ctx.mkImplies(validPair, notEqual));
900+
constraints.add(ctx.mkImplies(validPair, notEqual));
904901
}
905902
}
906903

@@ -915,7 +912,8 @@ private void applyBoundedMapBijection(
915912
ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()),
916913
seqMap);
917914
}
918-
typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
915+
constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
916+
return CelZ3TypeSystem.mkAndFlattened(ctx, constraints);
919917
}
920918

921919
private TranslatedValue[] evaluateLoopCondAndStep(
@@ -1335,6 +1333,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
13351333

13361334
List<BoolExpr> boundsAndTypes = new ArrayList<>();
13371335
boundsAndTypes.add(isMap);
1336+
boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length));
13381337

13391338
for (int i = 0; i < comprehensionUnrollLimit; i++) {
13401339
IntExpr idx = ctx.mkInt(i);

‎verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -303,8 +303,10 @@ CelVerificationResult verifyImplication(
303303
/* isCounterexample= */ true));
304304
case TRUNCATED:
305305
return CelVerificationResult.inconclusive(
306-
String.format("Inconclusive: %s holds within the current loop unroll limit, but"
307-
+ " may be violated for larger collections.", subjectName.toLowerCase(Locale.US)));
306+
String.format(
307+
"Inconclusive: %s holds within the current loop unroll limit, but"
308+
+ " may be violated for larger collections.",
309+
subjectName.toLowerCase(Locale.US)));
308310
case NO_MATCH:
309311
return CelVerificationResult.verified();
310312
case SOLVER_UNKNOWN:

‎verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java‎

Lines changed: 32 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -179,14 +179,26 @@ private static String reconstructList(
179179

180180
private static String reconstructMap(
181181
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
182-
Expr<?> presenceArray =
182+
List<Expr<?>> keys = new ArrayList<>();
183+
Expr<?> lenExpr =
183184
evaluateStrict(
184185
model,
185-
typeSystem.getMapPresence(mapRef),
186-
String.format("Z3 failed to evaluate presence array natively for map %s", mapRef));
187-
188-
List<Expr<?>> keys = new ArrayList<>();
189-
extractKeys(presenceArray, keys);
186+
ctx.mkLength(typeSystem.getMapKeys(mapRef)),
187+
String.format("Z3 failed to evaluate length for map %s", mapRef));
188+
if (lenExpr instanceof IntNum) {
189+
int length = ((IntNum) lenExpr).getInt();
190+
int printLimit = Math.min(length, 100);
191+
for (int i = 0; i < printLimit; i++) {
192+
Expr<?> elem =
193+
evaluateStrict(
194+
model,
195+
ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)),
196+
String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef));
197+
if (!keys.contains(elem)) {
198+
keys.add(elem);
199+
}
200+
}
201+
}
190202

191203
List<String> entries = new ArrayList<>();
192204
for (Expr<?> key : keys) {
@@ -215,11 +227,11 @@ private static String reconstructMap(
215227

216228
private static String reconstructMessage(
217229
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> msgRef) {
218-
Expr<?> valuesArray =
230+
Expr<?> presenceArray =
219231
evaluateStrict(
220232
model,
221-
typeSystem.getMsgValues(msgRef),
222-
String.format("Z3 failed to evaluate values array natively for msg %s", msgRef));
233+
typeSystem.getMsgPresence(msgRef),
234+
String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef));
223235

224236
Expr<?> typeNameExpr =
225237
evaluateStrict(
@@ -230,7 +242,7 @@ private static String reconstructMessage(
230242
String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");
231243

232244
List<Expr<?>> keys = new ArrayList<>();
233-
extractKeys(valuesArray, keys);
245+
extractKeys(presenceArray, keys);
234246

235247
List<String> entries = new ArrayList<>();
236248
for (Expr<?> key : keys) {
@@ -268,16 +280,17 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
268280
FuncDecl<?> decl = arrayExpr.getFuncDecl();
269281
String declName = decl.getName().toString();
270282

271-
if (!declName.equals("store")) {
272-
break;
283+
if (declName.equals("store")) {
284+
Expr<?>[] args = arrayExpr.getArgs();
285+
Preconditions.checkState(
286+
args.length == 3, "Z3 store array operation must have exactly 3 arguments");
287+
if (!keys.contains(args[1])) {
288+
keys.add(args[1]);
289+
}
290+
arrayExpr = args[0];
291+
continue;
273292
}
274-
275-
Expr<?>[] args = arrayExpr.getArgs();
276-
Preconditions.checkState(
277-
args.length == 3, "Z3 store array operation must have exactly 3 arguments");
278-
keys.add(args[1]);
279-
280-
arrayExpr = args[0];
293+
break;
281294
}
282295
}
283296

‎verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18-
import com.microsoft.z3.FPExpr;
1918
import com.microsoft.z3.SeqExpr;
2019
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2120
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -56,9 +55,7 @@ final class GreaterAxiom {
5655
(ctx, typeSystem, constraintSink, lhs, rhs) ->
5756
Optional.of(
5857
typeSystem.wrapBool(
59-
ctx.mkFPGt(
60-
(FPExpr) typeSystem.getDouble(lhs),
61-
(FPExpr) typeSystem.getDouble(rhs)))))
58+
ctx.mkFPGt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs)))))
6259
.addBinaryOverloadTranslator(
6360
Comparison.GREATER_STRING.celOverloadDecl(),
6461
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -82,7 +79,7 @@ final class GreaterAxiom {
8279
typeSystem.wrapBool(
8380
AxiomHelpers.mkFpLtReal(
8481
ctx,
85-
(FPExpr) typeSystem.getDouble(rhs),
82+
typeSystem.getDouble(rhs),
8683
ctx.mkInt2Real(typeSystem.getInt(lhs))))))
8784
.addBinaryOverloadTranslator(
8885
Comparison.GREATER_UINT64_DOUBLE.celOverloadDecl(),
@@ -91,7 +88,7 @@ final class GreaterAxiom {
9188
typeSystem.wrapBool(
9289
AxiomHelpers.mkFpLtReal(
9390
ctx,
94-
(FPExpr) typeSystem.getDouble(rhs),
91+
typeSystem.getDouble(rhs),
9592
ctx.mkInt2Real(typeSystem.getUint(lhs))))))
9693
.addBinaryOverloadTranslator(
9794
Comparison.GREATER_DOUBLE_INT64.celOverloadDecl(),
@@ -101,7 +98,7 @@ final class GreaterAxiom {
10198
AxiomHelpers.mkRealLtFp(
10299
ctx,
103100
ctx.mkInt2Real(typeSystem.getInt(rhs)),
104-
(FPExpr) typeSystem.getDouble(lhs)))))
101+
typeSystem.getDouble(lhs)))))
105102
.addBinaryOverloadTranslator(
106103
Comparison.GREATER_DOUBLE_UINT64.celOverloadDecl(),
107104
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -110,7 +107,7 @@ final class GreaterAxiom {
110107
AxiomHelpers.mkRealLtFp(
111108
ctx,
112109
ctx.mkInt2Real(typeSystem.getUint(rhs)),
113-
(FPExpr) typeSystem.getDouble(lhs)))))
110+
typeSystem.getDouble(lhs)))))
114111
.addBinaryOverloadTranslator(
115112
Comparison.GREATER_INT64_UINT64.celOverloadDecl(),
116113
(ctx, typeSystem, constraintSink, lhs, rhs) ->

‎verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18-
import com.microsoft.z3.FPExpr;
1918
import com.microsoft.z3.SeqExpr;
2019
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2120
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -56,9 +55,7 @@ final class GreaterEqualsAxiom {
5655
(ctx, typeSystem, constraintSink, lhs, rhs) ->
5756
Optional.of(
5857
typeSystem.wrapBool(
59-
ctx.mkFPGEq(
60-
(FPExpr) typeSystem.getDouble(lhs),
61-
(FPExpr) typeSystem.getDouble(rhs)))))
58+
ctx.mkFPGEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs)))))
6259
.addBinaryOverloadTranslator(
6360
Comparison.GREATER_EQUALS_STRING.celOverloadDecl(),
6461
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -82,7 +79,7 @@ final class GreaterEqualsAxiom {
8279
typeSystem.wrapBool(
8380
AxiomHelpers.mkFpLeReal(
8481
ctx,
85-
(FPExpr) typeSystem.getDouble(rhs),
82+
typeSystem.getDouble(rhs),
8683
ctx.mkInt2Real(typeSystem.getInt(lhs))))))
8784
.addBinaryOverloadTranslator(
8885
Comparison.GREATER_EQUALS_UINT64_DOUBLE.celOverloadDecl(),
@@ -91,7 +88,7 @@ final class GreaterEqualsAxiom {
9188
typeSystem.wrapBool(
9289
AxiomHelpers.mkFpLeReal(
9390
ctx,
94-
(FPExpr) typeSystem.getDouble(rhs),
91+
typeSystem.getDouble(rhs),
9592
ctx.mkInt2Real(typeSystem.getUint(lhs))))))
9693
.addBinaryOverloadTranslator(
9794
Comparison.GREATER_EQUALS_DOUBLE_INT64.celOverloadDecl(),
@@ -101,7 +98,7 @@ final class GreaterEqualsAxiom {
10198
AxiomHelpers.mkRealLeFp(
10299
ctx,
103100
ctx.mkInt2Real(typeSystem.getInt(rhs)),
104-
(FPExpr) typeSystem.getDouble(lhs)))))
101+
typeSystem.getDouble(lhs)))))
105102
.addBinaryOverloadTranslator(
106103
Comparison.GREATER_EQUALS_DOUBLE_UINT64.celOverloadDecl(),
107104
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -110,7 +107,7 @@ final class GreaterEqualsAxiom {
110107
AxiomHelpers.mkRealLeFp(
111108
ctx,
112109
ctx.mkInt2Real(typeSystem.getUint(rhs)),
113-
(FPExpr) typeSystem.getDouble(lhs)))))
110+
typeSystem.getDouble(lhs)))))
114111
.addBinaryOverloadTranslator(
115112
Comparison.GREATER_EQUALS_INT64_UINT64.celOverloadDecl(),
116113
(ctx, typeSystem, constraintSink, lhs, rhs) ->

‎verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18-
import com.microsoft.z3.FPExpr;
1918
import com.microsoft.z3.SeqExpr;
2019
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2120
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -56,9 +55,7 @@ final class LessAxiom {
5655
(ctx, typeSystem, constraintSink, lhs, rhs) ->
5756
Optional.of(
5857
typeSystem.wrapBool(
59-
ctx.mkFPLt(
60-
(FPExpr) typeSystem.getDouble(lhs),
61-
(FPExpr) typeSystem.getDouble(rhs)))))
58+
ctx.mkFPLt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs)))))
6259
.addBinaryOverloadTranslator(
6360
Comparison.LESS_STRING.celOverloadDecl(),
6461
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -83,7 +80,7 @@ final class LessAxiom {
8380
AxiomHelpers.mkRealLtFp(
8481
ctx,
8582
ctx.mkInt2Real(typeSystem.getInt(lhs)),
86-
(FPExpr) typeSystem.getDouble(rhs)))))
83+
typeSystem.getDouble(rhs)))))
8784
.addBinaryOverloadTranslator(
8885
Comparison.LESS_UINT64_DOUBLE.celOverloadDecl(),
8986
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -92,15 +89,15 @@ final class LessAxiom {
9289
AxiomHelpers.mkRealLtFp(
9390
ctx,
9491
ctx.mkInt2Real(typeSystem.getUint(lhs)),
95-
(FPExpr) typeSystem.getDouble(rhs)))))
92+
typeSystem.getDouble(rhs)))))
9693
.addBinaryOverloadTranslator(
9794
Comparison.LESS_DOUBLE_INT64.celOverloadDecl(),
9895
(ctx, typeSystem, constraintSink, lhs, rhs) ->
9996
Optional.of(
10097
typeSystem.wrapBool(
10198
AxiomHelpers.mkFpLtReal(
10299
ctx,
103-
(FPExpr) typeSystem.getDouble(lhs),
100+
typeSystem.getDouble(lhs),
104101
ctx.mkInt2Real(typeSystem.getInt(rhs))))))
105102
.addBinaryOverloadTranslator(
106103
Comparison.LESS_DOUBLE_UINT64.celOverloadDecl(),
@@ -109,7 +106,7 @@ final class LessAxiom {
109106
typeSystem.wrapBool(
110107
AxiomHelpers.mkFpLtReal(
111108
ctx,
112-
(FPExpr) typeSystem.getDouble(lhs),
109+
typeSystem.getDouble(lhs),
113110
ctx.mkInt2Real(typeSystem.getUint(rhs))))))
114111
.addBinaryOverloadTranslator(
115112
Comparison.LESS_INT64_UINT64.celOverloadDecl(),

‎verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java‎

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@
1515
package dev.cel.verifier.axioms;
1616

1717
import com.microsoft.z3.ArithExpr;
18-
import com.microsoft.z3.FPExpr;
1918
import com.microsoft.z3.SeqExpr;
2019
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2120
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison;
@@ -56,9 +55,7 @@ final class LessEqualsAxiom {
5655
(ctx, typeSystem, constraintSink, lhs, rhs) ->
5756
Optional.of(
5857
typeSystem.wrapBool(
59-
ctx.mkFPLEq(
60-
(FPExpr) typeSystem.getDouble(lhs),
61-
(FPExpr) typeSystem.getDouble(rhs)))))
58+
ctx.mkFPLEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs)))))
6259
.addBinaryOverloadTranslator(
6360
Comparison.LESS_EQUALS_STRING.celOverloadDecl(),
6461
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -83,7 +80,7 @@ final class LessEqualsAxiom {
8380
AxiomHelpers.mkRealLeFp(
8481
ctx,
8582
ctx.mkInt2Real(typeSystem.getInt(lhs)),
86-
(FPExpr) typeSystem.getDouble(rhs)))))
83+
typeSystem.getDouble(rhs)))))
8784
.addBinaryOverloadTranslator(
8885
Comparison.LESS_EQUALS_UINT64_DOUBLE.celOverloadDecl(),
8986
(ctx, typeSystem, constraintSink, lhs, rhs) ->
@@ -92,15 +89,15 @@ final class LessEqualsAxiom {
9289
AxiomHelpers.mkRealLeFp(
9390
ctx,
9491
ctx.mkInt2Real(typeSystem.getUint(lhs)),
95-
(FPExpr) typeSystem.getDouble(rhs)))))
92+
typeSystem.getDouble(rhs)))))
9693
.addBinaryOverloadTranslator(
9794
Comparison.LESS_EQUALS_DOUBLE_INT64.celOverloadDecl(),
9895
(ctx, typeSystem, constraintSink, lhs, rhs) ->
9996
Optional.of(
10097
typeSystem.wrapBool(
10198
AxiomHelpers.mkFpLeReal(
10299
ctx,
103-
(FPExpr) typeSystem.getDouble(lhs),
100+
typeSystem.getDouble(lhs),
104101
ctx.mkInt2Real(typeSystem.getInt(rhs))))))
105102
.addBinaryOverloadTranslator(
106103
Comparison.LESS_EQUALS_DOUBLE_UINT64.celOverloadDecl(),
@@ -109,7 +106,7 @@ final class LessEqualsAxiom {
109106
typeSystem.wrapBool(
110107
AxiomHelpers.mkFpLeReal(
111108
ctx,
112-
(FPExpr) typeSystem.getDouble(lhs),
109+
typeSystem.getDouble(lhs),
113110
ctx.mkInt2Real(typeSystem.getUint(rhs))))))
114111
.addBinaryOverloadTranslator(
115112
Comparison.LESS_EQUALS_INT64_UINT64.celOverloadDecl(),

‎verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
import com.google.common.collect.ImmutableList;
2020
import com.microsoft.z3.BoolExpr;
2121
import com.microsoft.z3.Expr;
22-
import com.microsoft.z3.FPExpr;
2322
import com.microsoft.z3.FuncDecl;
2423
import com.microsoft.z3.IntExpr;
2524
import com.microsoft.z3.Sort;
@@ -233,8 +232,7 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions
233232
sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res)));
234233
sink.accept(
235234
ctx.mkImplies(
236-
typeSystem.isDouble(res),
237-
ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res)))));
235+
typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))));
238236
break;
239237
case STRING:
240238
sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res)));

‎verifier/src/test/java/dev/cel/verifier/BUILD.bazel‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ java_library(
6161

6262
junit4_test_suites(
6363
name = "test_suites",
64-
shard_count = 4,
64+
shard_count = 8,
6565
sizes = [
6666
"small",
6767
"medium",

0 commit comments

Comments
 (0)