From eb143f0e268b32222bf8f288ceec2314d1f46d25 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 05:27:46 +0530 Subject: [PATCH 1/4] test: Limit cvc5 to 1 MB in cvc5_memory_limit.cpp, which 1.4.2 needs. --- clang/test/Verify/suite/cvc5_memory_limit.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/clang/test/Verify/suite/cvc5_memory_limit.cpp b/clang/test/Verify/suite/cvc5_memory_limit.cpp index eba3e165cc..97512d3b17 100644 --- a/clang/test/Verify/suite/cvc5_memory_limit.cpp +++ b/clang/test/Verify/suite/cvc5_memory_limit.cpp @@ -1,11 +1,11 @@ // REQUIRES: cvc5, system-linux -// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=5 %s -- 2>&1 \ +// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=1 %s -- 2>&1 \ // RUN: | FileCheck %s // // Each cvc5 process may allocate --memory-limit megabytes; on Linux that is -// its data (RLIMIT_DATA). cvc5 needs more than 5 to start solving, so every +// its data (RLIMIT_DATA). cvc5 needs more than 1 to solve this query, so every // query runs out, which cvc5 reports as std::bad_alloc or as its SAT solver's -// OutOfMemoryException. +// OutOfMemoryException. cvc5 1.4.2 solves it within 5. int small(int x) cppverify::pre(x < 100) @@ -13,4 +13,4 @@ int small(int x) { return x + 1; } -// CHECK: Unresolved: small [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 5 MB (--memory-limit)) +// CHECK: Unresolved: small [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 1 MB (--memory-limit)) From d81d6df0ace48631b36688f9090a0cef9bea6f89 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 05:34:54 +0530 Subject: [PATCH 2/4] test: Give spec_post_unfolded.cpp a budget whose refinement slice survives a slow core. --- clang/test/Verify/suite/spec_post_unfolded.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/spec_post_unfolded.cpp b/clang/test/Verify/suite/spec_post_unfolded.cpp index dd01246d14..4b3d1d9f73 100644 --- a/clang/test/Verify/suite/spec_post_unfolded.cpp +++ b/clang/test/Verify/suite/spec_post_unfolded.cpp @@ -1,4 +1,4 @@ -// RUN: not %cpp-verify --timeout=10000 %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --timeout=40000 %s -- 2>&1 | FileCheck %s // RUN: %cpp-verify --lower-only --dump-ir=4 %s -- 2>&1 | FileCheck %s --check-prefix=DUMP // // A spec's proved postcondition holds at every application the solver sees, @@ -30,7 +30,10 @@ cppverify::proof void fibo_monotone(int i, int j) // DUMP: (>= (spec${{[^ ]+}} (- j_0 2)) 0) // The facts are theorems, so a false claim still fails with a certified -// counterexample: fibo(-2) == fibo(-1) == 0. +// counterexample: fibo(-2) == fibo(-1) == 0. Refinement and the search for +// the ends of a domain, which find it, get 5% of --timeout, at least 500 ms; +// on a slow or busy core (macOS runners, or one core shared with two busy +// loops) 500 ms was too little in 2 of 4 runs, and the RUN line gives 2 s. cppverify::proof void fibo_strict(int i, int j) cppverify::pre(i < j) cppverify::post(fibo(i) < fibo(j)) From 68735e7e0ee5a839c5ed568c12f427eacaa2931b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 09:05:16 +0530 Subject: [PATCH 3/4] test: Run cvc5_memory_limit.cpp out of memory while bit-blasting, past the limits where cvc5 crashes. --- clang/test/Verify/suite/cvc5_memory_limit.cpp | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/clang/test/Verify/suite/cvc5_memory_limit.cpp b/clang/test/Verify/suite/cvc5_memory_limit.cpp index 97512d3b17..848c96a1bc 100644 --- a/clang/test/Verify/suite/cvc5_memory_limit.cpp +++ b/clang/test/Verify/suite/cvc5_memory_limit.cpp @@ -1,16 +1,19 @@ // REQUIRES: cvc5, system-linux -// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=1 %s -- 2>&1 \ +// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=16 %s -- 2>&1 \ // RUN: | FileCheck %s // // Each cvc5 process may allocate --memory-limit megabytes; on Linux that is -// its data (RLIMIT_DATA). cvc5 needs more than 1 to solve this query, so every -// query runs out, which cvc5 reports as std::bad_alloc or as its SAT solver's -// OutOfMemoryException. cvc5 1.4.2 solves it within 5. +// its data (RLIMIT_DATA). Bit-blasting these 64-bit products needs far more +// than 16, so every query runs out once it is solving, which cvc5 reports as +// std::bad_alloc or as its SAT solver's OutOfMemoryException. At a few +// megabytes cvc5 may instead crash where an allocation fails, at limits that +// differ between versions and builds (1.1.2 at 1 and 6, 1.4.2 at 2 and 3), +// and 1.4.2 solves a small query within 4. -int small(int x) - cppverify::pre(x < 100) - cppverify::post(cppverify::result == x + 1) +unsigned long long mix(unsigned long long a, unsigned long long b, + unsigned long long c) + cppverify::post(cppverify::result == (a ^ b) * (b ^ c) * (c ^ a)) { - return x + 1; + return (a ^ b) * (b ^ c) * (c ^ a); } -// CHECK: Unresolved: small [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 1 MB (--memory-limit)) +// CHECK: Unresolved: mix [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 16 MB (--memory-limit)) From ea2843dc5bd080a0c40ce5b4b1e71e85d3ed8d13 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 28 Oct 2026 08:45:46 +0530 Subject: [PATCH 4/4] test: Make extent_separation.cpp's wrong copy write zeros, which the solver refutes at once. --- clang/test/Verify/suite/extent_separation.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/extent_separation.cpp b/clang/test/Verify/suite/extent_separation.cpp index 4219158d5d..19b811bed6 100644 --- a/clang/test/Verify/suite/extent_separation.cpp +++ b/clang/test/Verify/suite/extent_separation.cpp @@ -50,6 +50,9 @@ void copy(const int *a, int *out, int n) // VCR-NEXT: a // VCR-NEXT: post +// A copy that writes zeros: its invariant fails where a holds anything else, +// which the solver finds at once (a reversed copy took 30 to 60 s, and on a +// slow runner timed out). void wrong_copy(const int *a, int *out, int n) cppverify::pre(n >= 0 && valid(a, n) && valid(out, n)) cppverify::modifies(*out) @@ -61,7 +64,7 @@ void wrong_copy(const int *a, int *out, int n) cppverify::invariant(cppverify::forall(j, 0, i, out[j] == a[j])) cppverify::decreases(n - i) { - out[i] = a[n - 1 - i]; + out[i] = 0; i = i + 1; } }