diff --git a/.github/workflows/cppverify-differential.yml b/.github/workflows/cppverify-differential.yml new file mode 100644 index 0000000000..a9f985aa97 --- /dev/null +++ b/.github/workflows/cppverify-differential.yml @@ -0,0 +1,81 @@ +name: CppVerify differential execution + +# Every night, each differential case (clang/utils/cppverify-differential) is +# verified in every configuration it lists and run natively under UBSan on its +# inputs. The job fails when a verdict and the execution disagree. + +on: + schedule: + - cron: "43 2 * * *" + workflow_dispatch: + +permissions: + contents: read + +env: + CVC5_VERSION: "1.4.2" + +jobs: + differential: + name: Differential execution + runs-on: ubuntu-24.04 + timeout-minutes: 355 + env: + CCACHE_DIR: ${{ github.workspace }}/.ccache + CCACHE_MAXSIZE: 4G + CCACHE_COMPRESS: "1" + steps: + - name: Free disk space + run: | + sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc /opt/hostedtoolcache/CodeQL + df -h / + + - uses: actions/checkout@v4 + with: + submodules: recursive + + - name: Install build tools and cvc5 + run: | + sudo apt-get update + sudo apt-get install -y ninja-build ccache + curl -sSfL -o "$RUNNER_TEMP/cvc5.zip" \ + "https://github.com/cvc5/cvc5/releases/download/cvc5-$CVC5_VERSION/cvc5-Linux-x86_64-static.zip" + unzip -q "$RUNNER_TEMP/cvc5.zip" -d "$RUNNER_TEMP/cvc5" + dirname "$(find "$RUNNER_TEMP/cvc5" -name cvc5 -type f)" >> "$GITHUB_PATH" + + - uses: actions/cache/restore@v4 + with: + path: .ccache + key: ccache-linux-release-${{ github.sha }} + restore-keys: ccache-linux-release- + + - name: Configure + run: | + cmake -S llvm -B build -G Ninja \ + -DCMAKE_BUILD_TYPE=Release \ + -DLLVM_ENABLE_PROJECTS=clang \ + -DLLVM_TARGETS_TO_BUILD=Native \ + -DCPPVERIFY_VENDOR_Z3=ON \ + -DCPPVERIFY_PREFER_SYSTEM_Z3=OFF \ + -DLLVM_ENABLE_ASSERTIONS=OFF \ + -DLLVM_CCACHE_BUILD=ON + + - name: Build + run: ninja -C build clang cpp-verify + + - name: Report the versions + run: | + build/bin/cpp-verify --version + cvc5 --version | head -1 + + - name: Run the differential cases + run: | + python3 clang/utils/cppverify-differential/run.py \ + --cpp-verify build/bin/cpp-verify --jobs "$(nproc)" \ + --work "$RUNNER_TEMP/differential" --report differential.json + + - uses: actions/upload-artifact@v4 + if: always() + with: + name: differential-report + path: differential.json diff --git a/clang/test/Verify/differential.test b/clang/test/Verify/differential.test new file mode 100644 index 0000000000..d7ef360ae6 --- /dev/null +++ b/clang/test/Verify/differential.test @@ -0,0 +1,28 @@ +# The differential tool (clang/utils/cppverify-differential), which runs nightly +# over every case, on its own cases: verdicts that execution confirms pass, and +# a verdict that disagrees with execution is reported. Two of the cases state +# their contract wrongly in Python on purpose, so a right verdict reads as +# UNSOUND and a right counterexample as BADCEX. A read past a buffer traps on +# the page after it, and a contract undefined at an input is no failure of the +# body. +# +# UNSUPPORTED: system-windows +# RUN: rm -rf %t +# RUN: not %python %S/../../utils/cppverify-differential/run.py --suite selftest \ +# RUN: --cpp-verify %cpp-verify --clang %clang --work %t --jobs 1 --report %t.json \ +# RUN: | FileCheck %s +# RUN: %python -c "import json, sys; r = {c['case']: c for c in json.load(open(sys.argv[1]))}; \ +# RUN: print(sorted(r), r['self_overflow']['counterexamples'])" %t.json | FileCheck %s --check-prefix=REPORT + +# CHECK-DAG: {{^}}self_add {{ *}}z3=verified admitted=65536 violations=0{{$}} +# CHECK-DAG: {{^}}self_overflow {{ *}}z3=failed:overflow admitted=20188 violations=21 counterexamples: z3 confirmed: undefined behavior at (2147483647,){{$}} +# CHECK-DAG: {{^}}self_sum {{ *}}z3=verified admitted=25 violations=0{{$}} +# CHECK-DAG: {{^}}self_read_past {{ *}}z3=failed:bounds admitted=4 violations=4 counterexamples: z3 no input values{{$}} +# CHECK-DAG: {{^}}self_contract_div {{ *}}z3=failed:division-by-zero admitted=256 violations=0 counterexamples: z3 the contract is undefined there (division-by-zero){{$}} +# CHECK-DAG: {{^}}self_bound {{ *}}z3=verified admitted=32768 violations=1{{$}} +# CHECK-DAG: {{^}} problem: UNSOUND[z3]: verified, yet 1 admitted inputs misbehave, such as [((0,), 'POST', 0)]{{$}} +# CHECK-DAG: {{^}}self_wrong_at_5 {{ *}}z3=failed:postcondition admitted=256 violations=0{{$}} +# CHECK-DAG: {{^}} problem: BADCEX[z3]: (5,) returns 6 and meets the contract (verification failed: self_wrong_at_5 +# CHECK: {{^}}7 cases, 2 problems{{$}} + +# REPORT: ['self_add', 'self_bound', 'self_contract_div', 'self_overflow', 'self_read_past', 'self_sum', 'self_wrong_at_5'] {'z3': 'confirmed: undefined behavior at (2147483647,)'} diff --git a/clang/utils/cppverify-differential/cases/__init__.py b/clang/utils/cppverify-differential/cases/__init__.py new file mode 100644 index 0000000000..e69de29bb2 diff --git a/clang/utils/cppverify-differential/cases/bit_int.py b/clang/utils/cppverify-differential/cases/bit_int.py new file mode 100644 index 0000000000..4135583b47 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/bit_int.py @@ -0,0 +1,83 @@ +"""_BitInt(N) (no integer promotion; rank by width).""" +import differential as diff +from differential import * # noqa: F401,F403 + +for n in (2, 3, 7, 13, 31, 33, 63, 65, 127): + diff.TYPES['_BitInt(%d)' % n] = (n, True) +for n in (1, 3, 7, 13, 31, 33, 63, 65, 127): + diff.TYPES['unsigned _BitInt(%d)' % n] = (n, False) + +def wrap_n(v, n): + v &= (1 << n) - 1 + return v - (1 << n) if v >= 1 << (n - 1) else v + +def boundary_n(n): + lo, hi = -(1 << (n - 1)), (1 << (n - 1)) - 1 + return sorted(set(v for v in [lo, lo + 1, -1, 0, 1, 2, hi - 1, hi, -5, 5] if lo <= v <= hi)) + + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + k.setdefault('vflags', ['--extra-arg=-Wno-bit-int-extension']) + C.append(Case(*a, **k)) + +def M(n): + # 2^63 and above have no C++ literal. + return '%d' % (1 << n) if n < 63 else '((__int128)1 << %d)' % n + +for n in (3, 7, 13, 33, 65): + u = 'unsigned _BitInt(%d)' % n + s = '_BitInt(%d)' % n + ret = '__int128' + case('bi_uadd_%d' % n, [(u, 'a'), (u, 'b')], ret, + 'cppverify::post(%s == (a + b) %% %s)' % (R, M(n)), 'return a + b;', + post=lambda a, b, r, n=n: r == (a + b) % (1 << n)) + case('bi_umul_%d' % n, [(u, 'a'), (u, 'b')], ret, + 'cppverify::post(%s == (a * b) %% %s)' % (R, M(n)), 'return a * b;', + post=lambda a, b, r, n=n: r == (a * b) % (1 << n)) + case('bi_usub_%d' % n, [(u, 'a'), (u, 'b')], ret, + 'cppverify::post(%s == (a - b + %s) %% %s)' % (R, M(n), M(n)), 'return a - b;', + post=lambda a, b, r, n=n: r == (a - b) % (1 << n)) + case('bi_sadd_%d' % n, [(s, 'a'), (s, 'b')], ret, + 'cppverify::post(%s == a + b)' % R, 'return a + b;', + post=lambda a, b, r: r == a + b) + case('bi_sadd_guard_%d' % n, [(s, 'a'), (s, 'b')], ret, + 'cppverify::pre(a + b >= -%s && a + b < %s)\ncppverify::post(%s == a + b)' % (M(n - 1), M(n - 1), R), 'return a + b;', + pre=lambda a, b, n=n: -(1 << (n - 1)) <= a + b < (1 << (n - 1)), post=lambda a, b, r: r == a + b) + case('bi_sdiv_%d' % n, [(s, 'a'), (s, 'b')], ret, + 'cppverify::pre(b != 0)\ncppverify::post(%s == a / b)' % R, 'return a / b;', + pre=lambda a, b: b != 0, post=lambda a, b, r: r == tdiv(a, b)) + case('bi_srem_%d' % n, [(s, 'a'), (s, 'b')], ret, + 'cppverify::pre(b != 0 && !(a == -%s && b == -1))\ncppverify::post(%s == a %% b)' % (M(n - 1), R), 'return a % b;', + pre=lambda a, b, n=n: b != 0 and not (a == -(1 << (n - 1)) and b == -1), post=lambda a, b, r: r == tmod(a, b)) + case('bi_sneg_%d' % n, [(s, 'a')], ret, + 'cppverify::post(%s == -a)' % R, 'return -a;', post=lambda a, r: r == -a) + case('bi_conv_from_long_%d' % n, [('long', 'x')], ret, + 'cppverify::post(%s >= -%s && %s < %s)' % (R, M(n - 1), R, M(n - 1)), 'return (%s)x;' % s, + post=lambda x, r, n=n: -(1 << (n - 1)) <= r < (1 << (n - 1))) + case('bi_conv_val_%d' % n, [('long', 'x')], ret, + 'cppverify::post(%s == ((x %% %s) + %s + %s) %% %s - %s)' % (R, M(n), M(n), M(n - 1), M(n), M(n - 1)), 'return (%s)x;' % s, + post=lambda x, r, n=n: r == wrap_n(x, n)) + case('bi_mix_int_%d' % n, [(s, 'a'), ('int', 'b')], ret, + 'cppverify::pre(b > -1000 && b < 1000)\ncppverify::post(%s == a + b || true)' % R, 'return a + b;', + pre=lambda a, b: -1000 < b < 1000, post=lambda a, b, r: True) + case('bi_inc_%d' % n, [(s, 'a')], ret, + 'cppverify::post(true)', 'a++; return a;', post=lambda a, r: True) + case('bi_cmp_us_%d' % n, [(u, 'a'), (s, 'b')], 'bool', + 'cppverify::post(%s == (a < (b < 0 ? b + %s : b)))' % (R, M(n)), 'return a < b;', + post=lambda a, b, r, n=n: r == (1 if a < b % (1 << n) else 0)) + case('bi_shl_%d' % n, [(s, 'a'), ('int', 'k')], ret, + 'cppverify::pre(k >= 0 && k < %d && a >= 0 && a < 2)\ncppverify::post(%s == (k == %d ? -%s : a * (((__int128)1) << k)) || a == 0)' % (n, R, n - 1, M(n - 1)), + 'return a << k;', pre=lambda a, k, n=n: 0 <= k < n and 0 <= a < 2, + post=lambda a, k, r, n=n: a == 0 or r == (-(1 << (n - 1)) if k == n - 1 else a << k), + domain=[(a, k) for a in (-1, 0, 1) for k in range(-1, n + 2)]) + case('bi_shr_%d' % n, [(s, 'a'), ('int', 'k')], ret, + 'cppverify::pre(k >= 0 && k < %d)\ncppverify::post(%s * (((__int128)1) << k) <= a && a < (%s + 1) * (((__int128)1) << k))' % (n, R, R), + 'return a >> k;', pre=lambda a, k, n=n: 0 <= k < n, + post=lambda a, k, r: r * 2**k <= a < (r + 1) * 2**k, + domain=[(a, k) for a in boundary_n(n) for k in range(-1, n + 2)]) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/calls.py b/clang/utils/cppverify-differential/cases/calls.py new file mode 100644 index 0000000000..74bb66c530 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/calls.py @@ -0,0 +1,165 @@ +"""Modular calls, argument/result conversions, recursion.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +INC8 = '''int8_t inc8(int8_t x) + cppverify::pre(x < 127) + cppverify::post(cppverify::result == x + 1) +{ return x + 1; }''' +case('m_conv_arg_ok', [('int', 'y')], 'int', + 'cppverify::pre(y == 200)\ncppverify::post(%s == -55)' % R, 'return inc8(y);', + prelude=INC8, pre=lambda y: y == 200, post=lambda y, r: r == -55, domain=[(200,), (199,), (201,)]) +case('m_conv_arg_wrong', [('int', 'y')], 'int', + 'cppverify::pre(y == 200)\ncppverify::post(%s == 201)' % R, 'return inc8(y);', + prelude=INC8, pre=lambda y: y == 200, post=lambda y, r: r == 201, domain=[(200,)]) +case('m_conv_arg_range', [('int', 'y')], 'int', + 'cppverify::pre(y >= 0 && y < 1000 && y %% 256 != 127)\ncppverify::post(%s == ((y + 128) %% 256) - 128 + 1)' % R, + 'return inc8(y);', prelude=INC8, pre=lambda y: 0 <= y < 1000 and y % 256 != 127, + post=lambda y, r: r == wrap(y, 'int8_t') + 1, domain=[(y,) for y in range(-5, 1005)]) +case('m_conv_arg_pre_violated', [('int', 'y')], 'int', + 'cppverify::pre(y == 383)\ncppverify::post(true)', 'return inc8(y);', + prelude=INC8, pre=lambda y: y == 383, post=lambda y, r: True, domain=[(383,)]) +TW = '''unsigned twice(unsigned x) + cppverify::pre(x < 1000) + cppverify::post(cppverify::result == 2 * x) +{ return 2 * x; }''' +case('m_unsigned_arg_neg', [('int', 'y')], 'unsigned', + 'cppverify::pre(y > -5 && y < 5)\ncppverify::post(%s < 10)' % R, 'return twice(y);', + prelude=TW, pre=lambda y: -5 < y < 5, post=lambda y, r: r < 10, domain=[(y,) for y in range(-10, 10)]) +LONGRET = '''long big(int x) + cppverify::post(cppverify::result == x * 1000L) +{ return x * 1000L; }''' +case('m_ret_narrow', [('int', 'x')], 'int8_t', + 'cppverify::pre(x >= 0 && x < 100)\ncppverify::post(%s == x * 1000)' % R, 'int8_t r = big(x); return r;', + prelude=LONGRET, pre=lambda x: 0 <= x < 100, post=lambda x, r: r == x * 1000, domain=[(x,) for x in range(-2, 102)]) +case('m_ret_narrow_ok', [('int', 'x')], 'int8_t', + 'cppverify::pre(x >= 0 && x < 100)\ncppverify::post(%s == ((x * 1000 + 128) %% 256) - 128)' % R, 'int8_t r = big(x); return r;', + prelude=LONGRET, pre=lambda x: 0 <= x < 100, post=lambda x, r: r == wrap(x * 1000, 'int8_t'), domain=[(x,) for x in range(-2, 102)]) +BOOLP = '''int b2i(bool b) + cppverify::post(cppverify::result == (b ? 1 : 0)) +{ return b ? 1 : 0; }''' +case('m_bool_arg', [('int', 'x')], 'int', + 'cppverify::post(%s == (x != 0 ? 1 : 0))' % R, 'return b2i(x);', + prelude=BOOLP, post=lambda x, r: r == (1 if x != 0 else 0)) +case('m_bool_arg_wrong', [('int', 'x')], 'int', + 'cppverify::post(%s == x %% 2)' % R, 'return b2i(x);', + prelude=BOOLP, post=lambda x, r: r == tmod(x, 2), domain=[(x,) for x in range(-3, 300)]) +REASSIGN = '''int bump(int x) + cppverify::pre(x < 1000 && x > -1000) + cppverify::post(cppverify::result == x + 1) +{ x = x + 1; return x; }''' +case('m_callee_reassigns', [('int', 'y')], 'int', + 'cppverify::pre(y > -100 && y < 100)\ncppverify::post(%s == y + 2)' % R, 'return bump(bump(y));', + prelude=REASSIGN, pre=lambda y: -100 < y < 100, post=lambda y, r: r == y + 2, domain=[(y,) for y in range(-105, 105)]) +case('m_callee_reassigns_wrong', [('int', 'y')], 'int', + 'cppverify::pre(y > -100 && y < 100)\ncppverify::post(%s == y + 3)' % R, 'return bump(bump(y));', + prelude=REASSIGN, pre=lambda y: -100 < y < 100, post=lambda y, r: r == y + 3, domain=[(y,) for y in range(-105, 105)]) +case('m_nested_pre', [('int', 'y')], 'int', + 'cppverify::pre(y == 998)\ncppverify::post(true)', 'return bump(bump(y));', + prelude=REASSIGN, pre=lambda y: y == 998, post=lambda y, r: True, domain=[(998,)]) +HELPER = '''int helper(int x) { return x * 2; }''' +case('m_uncontracted_callee', [('int', 'x')], 'int', + 'cppverify::post(%s == 2 * x)' % R, 'return helper(x);', + prelude=HELPER, post=lambda x, r: r == 2 * x) +case('m_uncontracted_callee_guard', [('int', 'x')], 'int', + 'cppverify::pre(x > -1000 && x < 1000)\ncppverify::post(%s == 2 * x)' % R, 'return helper(x);', + prelude=HELPER, pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 2 * x) +case('m_uncontracted_callee_wrong', [('int', 'x')], 'int', + 'cppverify::pre(x > -1000 && x < 1000)\ncppverify::post(%s == 3 * x)' % R, 'return helper(x);', + prelude=HELPER, pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 3 * x) +CEX = '''constexpr int cx(int x) { return x * 2; }''' +case('m_constexpr_callee_exec', [('int', 'x')], 'int', + 'cppverify::post(%s == 2 * x)' % R, 'return cx(x);', + prelude=CEX, post=lambda x, r: r == 2 * x) +case('m_constexpr_callee_exec_wrong', [('int', 'x')], 'int', + 'cppverify::pre(x > -1000 && x < 1000)\ncppverify::post(%s == 3 * x)' % R, 'return cx(x);', + prelude=CEX, pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 3 * x) +FACT = '''int fact(int n) + cppverify::pre(n >= 0 && n <= 12) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 1) +{ if (n == 0) return 1; int r = fact(n - 1); return n * r; }''' +case('m_rec_fact', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 12)\ncppverify::post(%s >= 1)' % R, 'return fact(n);', + prelude=FACT, pre=lambda n: 0 <= n <= 12, post=lambda n, r: r >= 1, domain=[(n,) for n in range(-2, 15)]) +FACT13 = '''int fact13(int n) + cppverify::pre(n >= 0 && n <= 13) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 1) +{ if (n == 0) return 1; int r = fact13(n - 1); return n * r; }''' +case('m_rec_fact13', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 13)\ncppverify::post(%s >= 1)' % R, 'return fact13(n);', + prelude=FACT13, pre=lambda n: 0 <= n <= 13, post=lambda n, r: r >= 1, domain=[(n,) for n in range(-2, 15)]) +EVENODD = '''bool is_odd(int n); +bool is_even(int n) + cppverify::pre(n >= 0) + cppverify::decreases(n) + cppverify::post(cppverify::result == (n % 2 == 0)) +{ if (n == 0) return true; return is_odd(n - 1); } +bool is_odd(int n) + cppverify::pre(n >= 0) + cppverify::decreases(n) + cppverify::post(cppverify::result == (n % 2 == 1)) +{ if (n == 0) return false; return is_even(n - 1); }''' +case('m_mutual_rec', [('int', 'n')], 'bool', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == (n %% 2 == 0))' % R, 'return is_even(n);', + prelude=EVENODD, + pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == (1 if n % 2 == 0 else 0), domain=[(n,) for n in range(0, 1001)]) +DEFARG = '''int addd(int x, int y = 5) + cppverify::pre(x < 1000 && x > -1000) + cppverify::post(cppverify::result == x + y) +{ return x + y; }''' +case('m_default_arg', [('int', 'x')], 'int', + 'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == x + 5)' % R, 'return addd(x);', + prelude=DEFARG, + pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == x + 5) +case('m_default_arg_ub', [('int', 'x')], 'int', + 'cppverify::post(true)', 'return addd(1, x);', + prelude=DEFARG, + post=lambda x, r: True) +OVL = '''int ov(int x) cppverify::post(cppverify::result == 1) { return 1; } +int ov(long x) cppverify::post(cppverify::result == 2) { return 2; } +int ov(unsigned x) cppverify::post(cppverify::result == 3) { return 3; }''' +case('m_overload', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == 1)' % R, 'return ov(x);', prelude=OVL, post=lambda x, r: r == 1) +case('m_overload_u8', [('uint8_t', 'x')], 'int', + 'cppverify::post(%s == 1)' % R, 'return ov(x);', prelude=OVL, post=lambda x, r: r == 1) +case('m_overload_long', [('long', 'x')], 'int', + 'cppverify::post(%s == 2)' % R, 'return ov(x);', prelude=OVL, post=lambda x, r: r == 2) +case('m_overload_u', [('uint16_t', 'x')], 'int', + 'cppverify::post(%s == 3)' % R, 'return ov(x + 0u);', prelude=OVL, post=lambda x, r: r == 3) +SDIV = '''int sdiv(int x, int y) + cppverify::pre(y != 0 && !(x == -2147483647 - 1 && y == -1)) + cppverify::post(cppverify::result == x / y) +{ return x / y; }''' +case('m_short_circuit_call', [('int', 'x'), ('int', 'y')], 'bool', + 'cppverify::post(true)', 'return y != 0 && y != -1 && sdiv(x, y) > 0;', + prelude=SDIV, post=lambda x, y, r: True) +case('m_short_circuit_call_bad', [('int', 'x'), ('int', 'y')], 'bool', + 'cppverify::post(true)', 'return y != 0 && sdiv(x, y) > 0;', + prelude=SDIV, post=lambda x, y, r: True) +case('m_ternary_call', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::post(y == 0 || y == -1 || %s == x / y)' % R, 'return (y == 0 || y == -1) ? 0 : sdiv(x, y);', + prelude=SDIV, post=lambda x, y, r: y == 0 or y == -1 or r == tdiv(x, y)) +WEAK = '''int weak(int x) + cppverify::post(cppverify::result >= x) +{ return x < 100 ? 100 : x; }''' +case('m_weak_post', [('int', 'x')], 'int', + 'cppverify::post(%s >= 100)' % R, 'return weak(x);', + prelude=WEAK, post=lambda x, r: r >= 100) +case('m_arg_eval_conv', [('uint8_t', 'a'), ('uint8_t', 'b')], 'int', + 'cppverify::post(%s == a + b)' % R, 'return sum16(a + b);', + prelude='int sum16(int16_t v) cppverify::post(cppverify::result == v) { return v; }', + post=lambda a, b, r: r == a + b) +case('m_arg_conv_u16', [('int', 'x')], 'int', + 'cppverify::pre(x >= 65530 && x <= 65540)\ncppverify::post(%s == x)' % R, 'return idu16(x);', + prelude='int idu16(uint16_t v) cppverify::post(cppverify::result == v) { return v; }', + pre=lambda x: 65530 <= x <= 65540, post=lambda x, r: r == x, domain=[(x,) for x in range(65525, 65545)]) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/contracts.py b/clang/utils/cppverify-differential/cases/contracts.py new file mode 100644 index 0000000000..da47322a6c --- /dev/null +++ b/clang/utils/cppverify-differential/cases/contracts.py @@ -0,0 +1,140 @@ +"""Contract-expression semantics, old/result, constexpr vs spec.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +O = 'cppverify::old' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +# contract arithmetic is mathematical +case('c_inc_gt', [('int', 'x')], 'int', + 'cppverify::pre(x < 2147483647)\ncppverify::post(%s + 1 > %s)' % (R, R), 'return x + 1;', + pre=lambda x: x < 2**31 - 1, post=lambda x, r: r + 1 > r) +case('c_neg_unsigned', [('unsigned', 'x')], 'unsigned', + 'cppverify::post(%s == -x)' % R, 'return -x;', + post=lambda x, r: r == -x) +case('c_sum_u_math', [('unsigned', 'a'), ('unsigned', 'b')], 'unsigned', + 'cppverify::post(%s == a + b || %s == a + b - 4294967296)' % (R, R), 'return a + b;', + post=lambda a, b, r: r == a + b or r == a + b - 2**32) +case('c_mixed_cmp', [('int', 'x'), ('unsigned', 'u')], 'bool', + 'cppverify::post(%s == (x < 0 || x < u))' % R, 'return x < 0 || (unsigned)x < u;', + post=lambda x, u, r: r == (1 if (x < 0 or x < u) else 0)) +case('c_mixed_cmp_wrong', [('int', 'x'), ('unsigned', 'u')], 'bool', + 'cppverify::post(%s == (x < u))' % R, 'return x < u;', + post=lambda x, u, r: r == (1 if x < u else 0)) +case('c_div_intmin', [('int', 'x')], 'int', + 'cppverify::pre(x != -2147483647 - 1)\ncppverify::post(%s == x / -1)' % R, 'return -x;', + pre=lambda x: x != -2**31, post=lambda x, r: r == -x) +case('c_div_math', [('int', 'x')], 'long', + 'cppverify::post(%s == x / -1)' % R, 'return -(long)x;', + post=lambda x, r: r == -x) +case('c_mod_sign', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::pre(y > 0)\ncppverify::post(x >= 0 ? %s >= 0 : %s <= 0)' % (R, R), 'return x % y;', + pre=lambda x, y: y > 0, post=lambda x, y, r: (r >= 0) if x >= 0 else (r <= 0)) +case('c_div_by_zero_in_post', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::post(y == 0 || %s == x / y || true)' % R, 'return 0;', + post=lambda x, y, r: True) +case('c_div_by_zero_unguarded', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::post(%s == x / y || true)' % R, 'return 0;', + post=lambda x, y, r: True) +# bitwise ops and shifts in contracts are machine operations +case('c_bitand', [('int', 'x')], 'int', + 'cppverify::post((%s & 255) == (x & 255))' % R, 'return x;', + post=lambda x, r: (r & 255) == (x & 255)) +case('c_bitand_math_operand', [('int', 'x')], 'int', + 'cppverify::post(((x + 1) & 1) == 0 || ((x + 1) & 1) == 1)', 'return 0;', + post=lambda x, r: True) +case('c_shl_contract', [('int', 'x')], 'int', + 'cppverify::post(%s == (x << 1))' % R, 'return x * 2;', + post=lambda x, r: True) +case('c_shr_contract', [('int', 'x')], 'int', + 'cppverify::post(%s == (x >> 1))' % R, 'return x >= 0 ? x / 2 : (x - 1) / 2;', + post=lambda x, r: r == x >> 1) +case('c_bitnot_contract_u', [('unsigned', 'x')], 'unsigned', + 'cppverify::post(%s == ~x)' % R, 'return 4294967295u - x;', + post=lambda x, r: r == 2**32 - 1 - x) +case('c_bitnot_contract_u8', [('uint8_t', 'x')], 'int', + 'cppverify::post(%s == ~x)' % R, 'return -1 - x;', + post=lambda x, r: r == -1 - x) +case('c_xor_contract', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::post(%s == (x ^ y))' % R, 'return (x | y) & ~(x & y);', + post=lambda x, y, r: r == x ^ y) +case('c_cast_contract', [('int', 'x')], 'int', + 'cppverify::post((unsigned char)%s == (unsigned char)x)' % R, 'return x + 256 * (x > 0 ? -1 : 1);', + post=lambda x, r: True) +case('c_cast_contract_signed', [('unsigned', 'x')], 'int', + 'cppverify::post(%s == (int)x)' % R, 'return x;', + post=lambda x, r: r == wrap(x, 'int')) +case('c_cast_contract_narrow_math', [('int', 'x')], 'int', + 'cppverify::post((int)(x + 1) == x + 1 || x == 2147483647)', 'return 0;', + post=lambda x, r: True) +# old and parameters reassigned +case('c_old_param', [('int', 'x')], 'int', + 'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == %s(x) + 1 && %s == x + 1)' % (R, O, R), + 'x = x + 1; return x;', pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == x + 1) +case('c_old_param_loop', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == n)' % R, + 'int c = 0;\nwhile (n > 0)\n cppverify::invariant(n >= 0 && c + n == cppverify::old(n))\n cppverify::decreases(n)\n{ n = n - 1; c = c + 1; }\nreturn c;', + pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == n) +case('c_old_param_wrong', [('int', 'x')], 'int', + 'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == x)' % R, + 'x = x + 1; return x;', pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == x) +case('c_result_small', [('int', 'x')], 'int8_t', + 'cppverify::post(%s != 200)' % R, 'return x;', post=lambda x, r: r != 200) +case('c_result_u8_cmp_neg', [('int', 'x')], 'uint8_t', + 'cppverify::post(%s > -1)' % R, 'return x;', post=lambda x, r: r > -1) +case('c_bool_result', [('int', 'x')], 'bool', + 'cppverify::post(%s == (x > 0))' % R, 'return x > 0;', post=lambda x, r: r == (1 if x > 0 else 0)) +case('c_bool_plus', [('bool', 'a')], 'bool', + 'cppverify::post(%s + %s == 2 * a)' % (R, R), 'return a;', post=lambda a, r: 2 * r == 2 * a) +# constexpr helper (machine) vs spec (mathematical) +case('c_constexpr_sq', [('int', 'x')], 'int', + 'cppverify::post(sq(x) >= 0)', 'return 0;', + prelude='constexpr int sq(int v) { return v * v; }', post=lambda x, r: True) +case('c_constexpr_sq_guard', [('int', 'x')], 'int', + 'cppverify::pre(x > -46000 && x < 46000)\ncppverify::post(sq(x) >= 0)', 'return 0;', + prelude='constexpr int sq(int v) { return v * v; }', pre=lambda x: -46000 < x < 46000, post=lambda x, r: True) +case('c_spec_sq', [('int', 'x')], 'int', + 'cppverify::post(sq(x) >= 0)', 'return 0;', + prelude='cppverify::spec int sq(int v) { return v * v; }', post=lambda x, r: True) +case('c_constexpr_wrap', [('unsigned', 'x')], 'unsigned', + 'cppverify::post(%s == inc(x))' % R, 'return x + 1;', + prelude='constexpr unsigned inc(unsigned v) { return v + 1; }', post=lambda x, r: r == (x + 1) % 2**32) +case('c_constexpr_narrow_arg', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0 && x < 1000)\ncppverify::post(%s == g(x))' % R, 'return x % 256;', + prelude='constexpr int g(uint8_t v) { return v; }', pre=lambda x: 0 <= x < 1000, post=lambda x, r: r == x % 256) +case('c_constexpr_shift', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0 && x < 31)\ncppverify::post(%s == p2(x))' % R, 'return 1 << x;', + prelude='constexpr int p2(int v) { return 1 << v; }', pre=lambda x: 0 <= x < 31, post=lambda x, r: r == 2**x) +case('c_constexpr_branch_ub', [('int', 'x')], 'int', + 'cppverify::post(f(x) >= -1)', 'return 0;', + prelude='constexpr int f(int v) { return v > 0 ? v + 1 : -1; }', post=lambda x, r: True) +case('c_spec_div', [('int', 'x')], 'int', + 'cppverify::post(%s == half(x))' % R, 'return x / 2;', + prelude='cppverify::spec int half(int v) { return v / 2; }', post=lambda x, r: r == tdiv(x, 2)) +case('c_spec_mod_neg', [('int', 'x')], 'int', + 'cppverify::post(%s == m3(x))' % R, 'return x % -3;', + prelude='cppverify::spec int m3(int v) { return v % -3; }', post=lambda x, r: r == tmod(x, -3)) +case('c_spec_u8_param', [('int', 'x')], 'int', + 'cppverify::pre(x == 300)\ncppverify::post(id8(x) == 300)', 'return 0;', + prelude='cppverify::spec int id8(uint8_t v) { return v; }', pre=lambda x: x == 300, post=lambda x, r: True, + domain=[(300,)]) +case('c_spec_bool_ret', [('int', 'x')], 'int', + 'cppverify::post(b(x) == (x != 0))', 'return 0;', + prelude='cppverify::spec bool b(int v) { return v; }', post=lambda x, r: True) +case('c_spec_u_ret', [('int', 'x')], 'int', + 'cppverify::post(u(x) >= 0)', 'return 0;', + prelude='cppverify::spec unsigned u(int v) { return v; }', + # A spec's integers are mathematical: u(x) is x, whatever its type. + post=lambda x, r: x >= 0) +case('c_spec_shift', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0 && x < 40)\ncppverify::post(sh(x) > 0)', 'return 0;', + prelude='cppverify::spec long sh(int v) { return 1L << v; }', pre=lambda x: 0 <= x < 40, post=lambda x, r: True) +case('c_ternary_mixed_contract', [('bool', 'c')], 'long', + 'cppverify::post(%s == (c ? -1 : 0u))' % R, 'return c ? -1 : 0;', + post=lambda c, r: r == (-1 if c else 0)) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/expressions.py b/clang/utils/cppverify-differential/cases/expressions.py new file mode 100644 index 0000000000..6d0539854b --- /dev/null +++ b/clang/utils/cppverify-differential/cases/expressions.py @@ -0,0 +1,179 @@ +"""Switch, literal types, assignment/comma expressions, bitwise identities.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +# --- integer literal types -------------------------------------------------- +case('lit_hex_unsigned_cmp', [('int', 'x')], 'bool', + 'cppverify::post(%s == (x >= 0))' % R, 'return x < 0x80000000;', + post=lambda x, r: r == (1 if x >= 0 else 0)) +case('lit_hex_eq', [('int', 'x')], 'bool', + 'cppverify::post(%s == (x == -1))' % R, 'return x == 0xFFFFFFFF;', + post=lambda x, r: r == (1 if x == -1 else 0)) +case('lit_dec_long', [('int', 'x')], 'bool', + 'cppverify::post(%s == true)' % R, 'return x < 2147483648;', + post=lambda x, r: r == 1) +case('lit_neg_long', [('int', 'x')], 'bool', + 'cppverify::post(%s == true)' % R, 'return x >= -2147483648;', + post=lambda x, r: r == 1) +case('lit_hex_long', [('int', 'x')], 'long', + 'cppverify::post(%s == 4294967295)' % R, 'long l = 0xFFFFFFFF; return l + 0 * x;', + post=lambda x, r: r == 4294967295) +case('lit_int_from_hex', [('int', 'x')], 'int', + 'cppverify::post(%s == -1)' % R, 'int v = 0xFFFFFFFF; return v + 0 * x;', + post=lambda x, r: r == -1) +case('lit_char_xff', [('int', 'x')], 'int', + 'cppverify::post(%s == -1)' % R, "char c = '\\xff'; return c + 0 * x;", + post=lambda x, r: r == -1) +case('lit_uchar_cmp', [('unsigned char', 'c')], 'bool', + 'cppverify::post(%s == false)' % R, "return c == '\\xff';", + post=lambda c, r: r == 0) +case('lit_octal', [('int', 'x')], 'int', + 'cppverify::post(%s == 8)' % R, 'return 010 + 0 * x;', post=lambda x, r: r == 8) +case('lit_u_suffix_mix', [('int', 'x')], 'bool', + 'cppverify::post(%s == (x == 0))' % R, 'return x * 0 - 1 > 0u + (unsigned)x * 0 + 4294967294u - 4294967294u + (x != 0 ? 4294967295u : 0u);', + post=lambda x, r: r == (1 if x == 0 else 0)) +case('lit_sizeof', [('int', 'x')], 'bool', + 'cppverify::post(%s == false)' % R, 'return -1 < sizeof(int) + 0 * x;', + post=lambda x, r: r == 0) +case('lit_ll_ul', [('long long', 'x')], 'bool', + 'cppverify::post(%s == (x >= 0))' % R, 'return x < 9223372036854775808ULL;', + post=lambda x, r: r == (1 if x >= 0 else 0)) + +# --- switch --------------------------------------------------------------------- +case('sw_basic', [('int', 'x')], 'int', + 'cppverify::post(x == 1 ? %s == 10 : x == 2 ? %s == 20 : %s == 0)' % (R, R, R), + 'switch (x) { case 1: return 10; case 2: return 20; default: return 0; }', + post=lambda x, r: r == (10 if x == 1 else 20 if x == 2 else 0)) +case('sw_fallthrough', [('int', 'x')], 'int', + 'cppverify::post(x == 1 ? %s == 3 : x == 2 ? %s == 2 : %s == 0)' % (R, R, R), + 'int r = 0; switch (x) { case 1: r += 1; case 2: r += 2; break; default: r = 0; } return r;', + post=lambda x, r: r == (3 if x == 1 else 2 if x == 2 else 0)) +case('sw_u8_cond', [('uint8_t', 'c')], 'int', + 'cppverify::post(%s == (c == 255 ? 1 : 0))' % R, + 'switch (c) { case 255: return 1; case -1: return 2; default: return 0; }', + post=lambda c, r: r == (1 if c == 255 else 0)) +case('sw_char_cond', [('char', 'c')], 'int', + 'cppverify::post(%s == (c == -1 ? 2 : 0))' % R, + "switch (c) { case 255: return 1; case -1: return 2; default: return 0; }", + post=lambda c, r: r == (2 if c == -1 else 0)) +case('sw_default_first', [('int', 'x')], 'int', + 'cppverify::post(x == 5 ? %s == 1 : %s == 2)' % (R, R), + 'int r = 0; switch (x) { default: r = 2; break; case 5: r = 1; } return r;', + post=lambda x, r: r == (1 if x == 5 else 2)) +case('sw_no_default', [('int', 'x')], 'int', + 'cppverify::post(x == 3 ? %s == 7 : %s == 9)' % (R, R), + 'int r = 9; switch (x) { case 3: r = 7; } return r;', + post=lambda x, r: r == (7 if x == 3 else 9)) +case('sw_long_cond', [('long', 'x')], 'int', + 'cppverify::post(%s == (x == 4294967296 ? 1 : 0))' % R, + 'switch (x) { case 4294967296L: return 1; case 0: return 0; default: return 0; }', + post=lambda x, r: r == (1 if x == 2**32 else 0)) + +# --- assignment / comma expressions ---------------------------------------------- +case('ex_chain_assign', [('int', 'x')], 'int', + 'cppverify::post(%s == 2 * ((x + 128) %% 256 - 128 + 256) %% 256 - 0 || true)' % R, + 'int8_t a; int b; b = a = x; return a + b;', + post=lambda x, r: r == 2 * wrap(x, 'int8_t')) +case('ex_chain_assign_val', [('int', 'x')], 'int', + 'cppverify::post(%s == 2 * (((x %% 256) + 384) %% 256 - 128))' % R, + 'int8_t a; int b; b = a = x; return a + b;', + post=lambda x, r: r == 2 * wrap(x, 'int8_t')) +case('ex_comma', [('int', 'x')], 'int', + 'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == x + 2)' % R, + 'int y = (x++, x + 1); return y;', pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == x + 2) +case('ex_assign_in_cond', [('int', 'x')], 'int', + 'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == (x + 1 > 0 ? x + 1 : -1))' % R, + 'int y; if ((y = x + 1) > 0) return y; return -1;', pre=lambda x: -1000 < x < 1000, + post=lambda x, r: r == (x + 1 if x + 1 > 0 else -1)) +case('ex_compound_value', [('int', 'x')], 'int', + 'cppverify::pre(x < 1000 && x > -1000)\ncppverify::post(%s == 2 * x + 10)' % R, + 'int y = (x += 5); return x + y;', pre=lambda x: -1000 < x < 1000, post=lambda x, r: r == 2 * x + 10) +case('ex_preinc_value', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == 2 * (x == 127 ? -128 : x + 1))' % R, + 'int y = ++x; return x + y;', post=lambda x, r: r == 2 * wrap(x + 1, 'int8_t')) +case('ex_short_circuit_side', [('int', 'x')], 'int', + 'cppverify::post(%s == (x > 0 ? 5 : 0))' % R, + 'int y = 0; if (x > 0 && (y = 5) > 0) { } return y;', post=lambda x, r: r == (5 if x > 0 else 0)) +case('ex_or_side', [('int', 'x')], 'int', + 'cppverify::post(%s == (x > 0 ? 0 : 5))' % R, + 'int y = 0; if (x > 0 || (y = 5) > 0) { } return y;', post=lambda x, r: r == (0 if x > 0 else 5)) +case('ex_ternary_lvalue', [('bool', 'c')], 'int', + 'cppverify::post(%s == (c ? 5 : 50))' % R, + 'int a = 0, b = 0; (c ? a : b) = 5; return a + 10 * b;', post=lambda c, r: r == (5 if c else 50)) +case('ex_sub_assign_unsigned', [('unsigned', 'u')], 'unsigned', + 'cppverify::post(%s == (u + 1) %% 4294967296)' % R, 'u -= -1; return u;', + post=lambda u, r: r == (u + 1) % 2**32) +case('ex_int_minus_assign_neg_unsigned', [('int', 'x')], 'int', + 'cppverify::post(x == 2147483647 ? %s == -2147483647 - 1 : %s == x + 1)' % (R, R), 'x -= -1u; return x;', + post=lambda x, r: r == wrap(x + 1, 'int')) + +# --- bitwise identities across mixed types ----------------------------------------- +TYPEPAIRS = [('int8_t', 'int8_t'), ('uint8_t', 'int8_t'), ('int8_t', 'uint16_t'), ('int', 'unsigned'), + ('long', 'unsigned'), ('unsigned long', 'int'), ('int16_t', 'unsigned'), ('char', 'bool')] +def ctype_of(ta, tb): + """usual arithmetic conversions after promotion (LP64).""" + def prom(t): + b, s = TYPES[t] + if b < 32: + return 'int' + return t + pa, pb = prom(ta), prom(tb) + rank = {'int': 1, 'unsigned': 1, 'long': 2, 'unsigned long': 2} + canon = {'int': 'int', 'unsigned': 'unsigned', 'long': 'long', 'unsigned long': 'unsigned long', 'int32_t': 'int', 'uint32_t': 'unsigned', 'int64_t': 'long', 'uint64_t': 'unsigned long'} + pa, pb = canon[pa], canon[pb] + if pa == pb: + return pa + sa, sb = TYPES[pa][1], TYPES[pb][1] + if sa == sb: + return pa if rank[pa] > rank[pb] else pb + u, s = (pa, pb) if not sa else (pb, pa) + if rank[u] >= rank[s]: + return u + if TYPES[s][0] > TYPES[u][0]: + return s + return {'long': 'unsigned long'}[s] +for ta, tb in TYPEPAIRS: + ct = ctype_of(ta, tb) + nm = (ta + '_' + tb).replace(' ', '') + case('bw_andor_' + nm, [(ta, 'a'), (tb, 'b')], 'long', + 'cppverify::post(%s + (a | b) == a + b || %s)' % (R, 'false'), + 'return a & b;', post=lambda a, b, r, ct=ct: r + wrap(wrap(a, ct) | wrap(b, ct), ct) == a + b) + case('bw_xor_' + nm, [(ta, 'a'), (tb, 'b')], 'long', + 'cppverify::post(%s + 2 * (a & b) == (a | b) + (a & b))' % R, + 'return a ^ b;', post=lambda a, b, r, ct=ct: r + 2 * (wrap(a, ct) & wrap(b, ct)) == (wrap(a, ct) | wrap(b, ct)) + (wrap(a, ct) & wrap(b, ct))) + case('bw_val_and_' + nm, [(ta, 'a'), (tb, 'b')], 'long', + 'cppverify::post(%s == (a & b))' % R, + 'return a & b;', post=lambda a, b, r, ct=ct: r == wrap(wrap(a, ct) & wrap(b, ct), ct)) + case('bw_val_or_' + nm, [(ta, 'a'), (tb, 'b')], 'long', + 'cppverify::post(%s == (a | b))' % R, + 'return a | b;', post=lambda a, b, r, ct=ct: r == wrap(wrap(a, ct) | wrap(b, ct), ct)) + case('bw_ret_xor_cmp_' + nm, [(ta, 'a'), (tb, 'b')], 'bool', + 'cppverify::post(%s == ((a ^ b) < 0))' % R, + 'return (a ^ b) < 0;', post=lambda a, b, r, ct=ct: r == (1 if wrap(wrap(a, ct) ^ wrap(b, ct), ct) < 0 else 0)) +for t in ('int8_t', 'uint8_t', 'int16_t', 'uint16_t', 'int', 'unsigned', 'long', 'unsigned long', 'bool', 'char'): + nm = t.replace(' ', '') + pt = 'int' if TYPES[t][0] < 32 else t + case('bw_not_' + nm, [(t, 'a')], 'long', + 'cppverify::post(%s == ~a)' % R, 'return ~a;', + post=lambda a, r, pt=pt: r == wrap(~a, pt)) + case('bw_not_id_' + nm, [(t, 'a')], 'bool', + 'cppverify::post(%s == true)' % R, 'return (~a & a) == 0 && (~a | a) == ~0 * 0 + (%s)~(%s)0;' % (pt, pt), + post=lambda a, r: r == 1) + case('bw_shr_floor_' + nm, [(t, 'a'), ('int', 'k')], 'long', + 'cppverify::pre(k >= 0 && k < %d)\ncppverify::post(%s * (1L << k) <= a && a < (%s + 1) * (1L << k))' % (min(TYPES[pt][0], 63), R, R), + 'return a >> k;', pre=lambda a, k, pt=pt: 0 <= k < min(TYPES[pt][0], 63), + post=lambda a, k, r: r * 2**k <= a < (r + 1) * 2**k, + domain=[(a, k) for a in boundary(t) for k in range(-1, TYPES[pt][0] + 1)]) + case('bw_shr_mask_' + nm, [(t, 'a'), ('int', 'k')], 'bool', + 'cppverify::pre(k >= 0 && k < 31)\ncppverify::post(%s == true)' % R, + 'return (a >> k) * (1L << k) + (a & ((1L << k) - 1)) == a;', pre=lambda a, k: 0 <= k < 31, + post=lambda a, k, r: r == 1, + domain=[(a, k) for a in boundary(t) for k in range(-1, 33)]) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/integers.py b/clang/utils/cppverify-differential/cases/integers.py new file mode 100644 index 0000000000..f3a98ac6e9 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/integers.py @@ -0,0 +1,186 @@ +"""Integer promotions, small types, conversions, shifts, division.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +# --- promotions of small types ------------------------------------------- +case('u16mul', [('uint16_t', 'a'), ('uint16_t', 'b')], 'int', + 'cppverify::post(%s == a * b)' % R, 'return a * b;', + post=lambda a, b, r: r == a * b) +case('u16mul_u', [('uint16_t', 'a'), ('uint16_t', 'b')], 'unsigned', + 'cppverify::post(%s == (a * b) %% 4294967296)' % R, 'return a * b;', + post=lambda a, b, r: r == (a * b) % 2**32) +case('u16mul_compound', [('uint16_t', 'a')], 'uint16_t', + 'cppverify::post(%s == (a * a) %% 65536)' % R, 'a *= a; return a;', + post=lambda a, r: r == (a * a) % 65536) +case('u16mul_guard', [('uint16_t', 'a'), ('uint16_t', 'b')], 'int', + 'cppverify::pre(a <= 46340 && b <= 46340)\ncppverify::post(%s == a * b)' % R, 'return a * b;', + pre=lambda a, b: a <= 46340 and b <= 46340, post=lambda a, b, r: r == a * b) +case('u8add', [('uint8_t', 'a'), ('uint8_t', 'b')], 'int', + 'cppverify::post(%s == a + b)' % R, 'return a + b;', + post=lambda a, b, r: r == a + b) +case('u8sub_int', [('uint8_t', 'a'), ('uint8_t', 'b')], 'int', + 'cppverify::post(%s == a - b)' % R, 'return a - b;', + post=lambda a, b, r: r == a - b) +case('u8sub_u8', [('uint8_t', 'a'), ('uint8_t', 'b')], 'uint8_t', + 'cppverify::post(%s == (a - b + 256) %% 256)' % R, 'return a - b;', + post=lambda a, b, r: r == (a - b) % 256) +case('u8sub_unsigned', [('uint8_t', 'a'), ('uint8_t', 'b')], 'unsigned', + 'cppverify::post(a >= b ? %s == a - b : %s == 4294967296 + a - b)' % (R, R), 'return a - b;', + post=lambda a, b, r: r == (a - b) % 2**32) +case('i8neg', [('int8_t', 'x')], 'int8_t', + 'cppverify::post(x == -128 ? %s == -128 : %s == -x)' % (R, R), 'return -x;', + post=lambda x, r: r == wrap(-x, 'int8_t')) +case('i8neg_int', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == -x)' % R, 'return -x;', + post=lambda x, r: r == -x) +case('i8_compound_add', [('int8_t', 'x'), ('int8_t', 'y')], 'int8_t', + 'cppverify::post(%s == ((x + y + 384) %% 256) - 128)' % R, 'x += y; return x;', + post=lambda x, y, r: r == wrap(x + y, 'int8_t')) +case('i8_inc', [('int8_t', 'x')], 'int8_t', + 'cppverify::post(x == 127 ? %s == -128 : %s == x + 1)' % (R, R), 'x++; return x;', + post=lambda x, r: r == wrap(x + 1, 'int8_t')) +case('i8_postinc_val', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == x + (x == 127 ? -128 : x + 1))' % R, 'int8_t y = x++; return y + x;', + post=lambda x, r: r == x + wrap(x + 1, 'int8_t')) +case('u8_dec', [('uint8_t', 'x')], 'uint8_t', + 'cppverify::post(x == 0 ? %s == 255 : %s == x - 1)' % (R, R), '--x; return x;', + post=lambda x, r: r == (x - 1) % 256) +case('i16_mul_compound', [('int16_t', 'x')], 'int16_t', + 'cppverify::post(%s == ((x * x + 32768) %% 65536) - 32768)' % R, 'x *= x; return x;', + post=lambda x, r: r == wrap(x * x, 'int16_t')) +case('i16_cube', [('int16_t', 'x')], 'int', + 'cppverify::post(%s == x * x * x)' % R, 'return x * x * x;', + post=lambda x, r: r == x ** 3) +case('i8_pow4', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == x * x * x * x)' % R, 'return x * x * x * x;', + post=lambda x, r: r == x ** 4) +case('u8_mul_back', [('uint8_t', 'a'), ('uint8_t', 'b')], 'uint8_t', + 'cppverify::post(%s == (a * b) %% 256)' % R, 'uint8_t c = a * b; return c;', + post=lambda a, b, r: r == (a * b) % 256) + +# --- char signedness and narrowing ---------------------------------------- +case('char_sign', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0 && x <= 255)\ncppverify::post(x >= 128 ? %s == x - 256 : %s == x)' % (R, R), + 'char c = x; return c;', pre=lambda x: 0 <= x <= 255, post=lambda x, r: r == wrap(x, 'int8_t'), + domain=[(x,) for x in range(-5, 300)]) +case('char_lt0', [('char', 'c')], 'bool', + 'cppverify::post(%s == (c < 0))' % R, 'return c < 0;', + post=lambda c, r: r == (1 if c < 0 else 0)) +case('uchar_from_int', [('int', 'x')], 'unsigned char', + 'cppverify::post(%s == ((x %% 256) + 256) %% 256)' % R, 'return x;', + post=lambda x, r: r == x % 256) +case('schar_from_uint', [('unsigned', 'x')], 'signed char', + 'cppverify::post(%s == ((x + 128) %% 256) - 128)' % R, 'return x;', + post=lambda x, r: r == wrap(x, 'int8_t')) +case('int_from_long', [('long', 'x')], 'int', + 'cppverify::post(%s == ((x %% 4294967296 + 4294967296 + 2147483648) %% 4294967296) - 2147483648)' % R, + 'return x;', post=lambda x, r: r == wrap(x, 'int')) +case('uint_from_long', [('long', 'x')], 'unsigned', + 'cppverify::post(%s == (x %% 4294967296 + 4294967296) %% 4294967296)' % R, + 'return x;', post=lambda x, r: r == x % 2**32) +case('long_from_ulong', [('unsigned long', 'x')], 'long', + 'cppverify::post(x > 9223372036854775807 ? %s == x - 18446744073709551615 - 1 : %s == x)' % (R, R), + 'return x;', post=lambda x, r: r == wrap(x, 'long')) +case('i8_to_u8_to_int', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == (x < 0 ? x + 256 : x))' % R, 'return (uint8_t)x;', + post=lambda x, r: r == x % 256) +case('u8_to_i8_to_int', [('uint8_t', 'x')], 'int', + 'cppverify::post(%s == (x > 127 ? x - 256 : x))' % R, 'return (int8_t)x;', + post=lambda x, r: r == wrap(x, 'int8_t')) +case('u16_to_short', [('uint16_t', 'x')], 'int', + 'cppverify::post(%s == (x > 32767 ? x - 65536 : x))' % R, 'short s = x; return s;', + post=lambda x, r: r == wrap(x, 'int16_t')) + +# --- bool conversions --------------------------------------------------------- +case('bool_from_int', [('int', 'x')], 'bool', + 'cppverify::post(%s == (x != 0))' % R, 'return x;', + post=lambda x, r: r == (1 if x != 0 else 0)) +case('bool_from_u8', [('uint8_t', 'x')], 'int', + 'cppverify::post(%s == (x != 0 ? 1 : 0))' % R, 'bool b = x; return b;', + post=lambda x, r: r == (1 if x != 0 else 0)) +case('bool_from_long_even', [('long', 'x')], 'int', + 'cppverify::post(%s == (x != 0 ? 1 : 0))' % R, 'bool b = (bool)x; return b + 0;', + post=lambda x, r: r == (1 if x != 0 else 0)) +case('bool_arith', [('bool', 'a'), ('bool', 'b')], 'int', + 'cppverify::post(%s == a + b + a)' % R, 'return a + b + a;', + post=lambda a, b, r: r == 2 * a + b) +case('bool_compound_sub', [('bool', 'a')], 'bool', + 'cppverify::post(%s == true)' % R, 'a -= 1; a -= 1; return a;', + post=lambda a, r: r == 1) +case('bool_compound_add', [('bool', 'a'), ('int', 'k')], 'bool', + 'cppverify::post(%s == (a + k != 0))' % R, 'a += k; return a;', + post=lambda a, k, r: r == (1 if a + k != 0 else 0)) +case('bool_neg', [('bool', 'a')], 'int', + 'cppverify::post(%s == -a)' % R, 'return -a;', post=lambda a, r: r == -a) +case('bool_not_int', [('int', 'x')], 'int', + 'cppverify::post(%s == (x == 0 ? 1 : 0))' % R, 'return !x;', post=lambda x, r: r == (1 if x == 0 else 0)) +case('bool_bitnot', [('bool', 'a')], 'int', + 'cppverify::post(%s == -1 - a)' % R, 'return ~a;', post=lambda a, r: r == -1 - a) + +# --- mixed signed/unsigned ------------------------------------------------- +case('mixed_lt', [('int', 'x'), ('unsigned', 'u')], 'bool', + 'cppverify::post(%s == ((x < 0 ? x + 4294967296 : x) < u))' % R, 'return x < u;', + post=lambda x, u, r: r == (1 if (x % 2**32) < u else 0)) +case('mixed_lt_long_uint', [('long', 'x'), ('unsigned', 'u')], 'bool', + 'cppverify::post(%s == (x < u))' % R, 'return x < u;', + post=lambda x, u, r: r == (1 if x < u else 0)) +case('mixed_lt_ll_ul', [('long long', 'x'), ('unsigned long', 'u')], 'bool', + 'cppverify::post(%s == ((x < 0 ? x + 18446744073709551615 + 1 : x) < u))' % R, 'return x < u;', + post=lambda x, u, r: r == (1 if (x % 2**64) < u else 0)) +case('mixed_add_long', [('int', 'x'), ('unsigned', 'u')], 'long', + 'cppverify::post(%s == (x + u + 4294967296) %% 4294967296)' % R, 'long l = x + u; return l;', + post=lambda x, u, r: r == (x + u) % 2**32) +case('mixed_eq_neg1', [('unsigned', 'u')], 'bool', + 'cppverify::post(%s == (u == 4294967295))' % R, 'return u == -1;', + post=lambda u, r: r == (1 if u == 2**32 - 1 else 0)) +case('mixed_u8_vs_i8', [('uint8_t', 'a'), ('int8_t', 'b')], 'bool', + 'cppverify::post(%s == (a < b))' % R, 'return a < b;', + post=lambda a, b, r: r == (1 if a < b else 0)) +case('mixed_u32_vs_i8', [('unsigned', 'a'), ('int8_t', 'b')], 'bool', + 'cppverify::post(%s == (a < (b < 0 ? b + 4294967296 : b)))' % R, 'return a < b;', + post=lambda a, b, r: r == (1 if a < b % 2**32 else 0)) +case('int_plus_1u', [('int', 'x')], 'int', + 'cppverify::post(x == 2147483647 ? %s == -2147483647 - 1 : %s == x + 1)' % (R, R), 'x += 1u; return x;', + post=lambda x, r: r == wrap(x + 1, 'int')) +case('int_times_2u', [('int', 'x')], 'int', + 'cppverify::post(%s == ((2 * x %% 4294967296 + 4294967296 + 2147483648) %% 4294967296) - 2147483648)' % R, + 'x = x * 2u; return x;', post=lambda x, r: r == wrap(2 * x, 'int')) +case('long_plus_1u', [('long', 'x')], 'long', + 'cppverify::post(%s == x + 1)' % R, 'x += 1u; return x;', post=lambda x, r: r == x + 1) +case('ternary_mixed', [('bool', 'c')], 'long', + 'cppverify::post(c ? %s == 4294967295 : %s == 0)' % (R, R), 'return c ? -1 : 0u;', + post=lambda c, r: r == (2**32 - 1 if c else 0)) +case('ternary_small', [('bool', 'c'), ('int8_t', 'a'), ('uint8_t', 'b')], 'int', + 'cppverify::post(%s == (c ? a : b))' % R, 'return c ? a : b;', + post=lambda c, a, b, r: r == (a if c else b), domain=[(c, a, b) for c in (0, 1) for a in range(-128, 128, 3) for b in range(0, 256, 3)]) +case('ternary_int_uint', [('bool', 'c'), ('int', 'a'), ('unsigned', 'b')], 'long', + 'cppverify::post(%s == (c ? (a < 0 ? a + 4294967296 : a) : b))' % R, 'return c ? a : b;', + post=lambda c, a, b, r: r == (a % 2**32 if c else b)) +case('ternary_long_uint', [('bool', 'c'), ('long', 'a'), ('unsigned', 'b')], 'long', + 'cppverify::post(%s == (c ? a : b))' % R, 'return c ? a : b;', + post=lambda c, a, b, r: r == (a if c else b)) + +# --- unary on unsigned ----------------------------------------------------- +case('neg_unsigned', [('unsigned', 'u')], 'unsigned', + 'cppverify::post(%s == (4294967296 - u) %% 4294967296)' % R, 'return -u;', + post=lambda u, r: r == (-u) % 2**32) +case('neg_u8', [('uint8_t', 'u')], 'int', + 'cppverify::post(%s == -u)' % R, 'return -u;', post=lambda u, r: r == -u) +case('bitnot_u8', [('uint8_t', 'u')], 'int', + 'cppverify::post(%s == -1 - u)' % R, 'return ~u;', post=lambda u, r: r == -1 - u) +case('bitnot_u8_back', [('uint8_t', 'u')], 'uint8_t', + 'cppverify::post(%s == 255 - u)' % R, 'return ~u;', post=lambda u, r: r == 255 - u) +case('bitnot_u16_cmp', [('uint16_t', 'u')], 'bool', + 'cppverify::post(%s == false)' % R, 'return ~u == 65535 - u;', + post=lambda u, r: r == 0) +case('neg_ulong', [('unsigned long', 'u')], 'unsigned long', + 'cppverify::post(%s == (u == 0 ? 0 : 18446744073709551615 - u + 1))' % R, 'return -u;', + post=lambda u, r: r == (-u) % 2**64) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/loops.py b/clang/utils/cppverify-differential/cases/loops.py new file mode 100644 index 0000000000..0c0b7935dc --- /dev/null +++ b/clang/utils/cppverify-differential/cases/loops.py @@ -0,0 +1,252 @@ +"""Scalar loops (break/continue/return, do-while, nested, termination).""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +def d1(lo, hi, extra=()): + return [(v,) for v in sorted(set(list(range(lo, hi)) + list(extra)))] + +INTB = [-2**31, -2**31 + 1, 2**31 - 1, 2**31 - 2, 65535, 65536, 46340, 46341, 100000, 1000000] + +def tri(n): + return n * (n + 1) // 2 + +case('l_sum', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == n * (n + 1) / 2)' % R, + '''int s = 0; +for (int i = 1; i <= n; i++) + cppverify::invariant(1 <= i && i <= n + 1 && s == (i - 1) * i / 2) + cppverify::decreases(n + 1 - i) +{ s += i; } +return s;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == tri(n), domain=d1(-5, 1010)) +case('l_sum_overflow', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 100000)\ncppverify::post(%s == n * (n + 1) / 2)' % R, + '''int s = 0; +for (int i = 1; i <= n; i++) + cppverify::invariant(1 <= i && i <= n + 1 && s == (i - 1) * i / 2) + cppverify::decreases(n + 1 - i) +{ s += i; } +return s;''', pre=lambda n: 0 <= n <= 100000, post=lambda n, r: r == tri(n), + domain=d1(65530, 65540, [0, 1, 1000, 65535, 65536, 92681, 100000])) +case('l_counter_overflow', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0)\ncppverify::post(%s == n + 1)' % R, + '''int c = 0; +for (int i = 0; i <= n; i++) + cppverify::invariant(0 <= i && i <= n + 1 && c == i) + cppverify::decreases(n + 1 - i) +{ c++; } +return c;''', pre=lambda n: n >= 0, post=lambda n, r: r == n + 1, + domain=d1(0, 50, [10**6, 2**31 - 1]), alarm_ms=20000) +case('l_u8_counter', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 300)\ncppverify::post(%s == n)' % R, + '''int c = 0; +for (uint8_t i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c == i) + cppverify::decreases(n - i) +{ c++; } +return c;''', pre=lambda n: 0 <= n <= 300, post=lambda n, r: r == n, + domain=d1(250, 260, [0, 1, 255, 256, 300]), alarm_ms=300) +case('l_u8_counter_le', [('uint8_t', 'n')], 'int', + 'cppverify::post(%s == n + 1)' % R, + '''int c = 0; +for (uint8_t i = 0; i <= n; i++) + cppverify::invariant(0 <= i && i <= n && c == i) + cppverify::decreases(n - i) +{ c++; if (i == n) break; } +return c;''', post=lambda n, r: r == n + 1, alarm_ms=300) +case('l_u8_counter_le_nobreak', [('uint8_t', 'n')], 'int', + 'cppverify::post(%s == n + 1)' % R, + '''int c = 0; +uint8_t i = 0; +while (i <= n) + cppverify::invariant(c == i && i <= n + 1) + cppverify::decreases(n + 1 - i) +{ c++; i++; } +return c;''', post=lambda n, r: r == n + 1, alarm_ms=300) +case('l_break_find', [('int', 'n'), ('int', 't')], 'int', + 'cppverify::pre(n >= 0 && n <= 100 && t >= 0)\ncppverify::post(t < n ? %s == t : %s == n)' % (R, R), + '''int i = 0; +while (i < n) + cppverify::invariant(0 <= i && i <= n && (i <= t)) + cppverify::decreases(n - i) +{ if (i == t) break; i++; } +return i;''', pre=lambda n, t: 0 <= n <= 100 and t >= 0, post=lambda n, t, r: r == (t if t < n else n), + domain=[(n, t) for n in range(-1, 30) for t in range(-1, 35)]) +case('l_continue_sum_even', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == (n / 2) * (n / 2 + 1))' % R, + '''int s = 0; +for (int i = 0; i <= n; i++) + cppverify::invariant(0 <= i && i <= n + 1 && s == ((i + 1) / 2 - 1) * ((i + 1) / 2)) + cppverify::decreases(n + 1 - i) +{ if (i % 2 != 0) continue; s += i; } +return s;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == (n // 2) * (n // 2 + 1), domain=d1(-2, 1005)) +case('l_continue_simple', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == n / 2)' % R, + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c == i / 2) + cppverify::decreases(n - i) +{ if (i % 2 == 0) continue; c++; } +return c;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == n // 2, domain=d1(-2, 1005)) +case('l_continue_wrong', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == (n + 1) / 2)' % R, + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c == (i + 1) / 2) + cppverify::decreases(n - i) +{ if (i % 2 == 0) continue; c++; } +return c;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == (n + 1) // 2, domain=d1(-2, 1005)) +case('l_early_return', [('int', 'n'), ('int', 't')], 'int', + 'cppverify::pre(n >= 0 && n <= 100)\ncppverify::post((0 <= t && t < n) ? %s == t * 2 : %s == -1)' % (R, R), + '''for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && (t < 0 || t >= i)) + cppverify::decreases(n - i) +{ if (i == t) return i * 2; } +return -1;''', pre=lambda n, t: 0 <= n <= 100, post=lambda n, t, r: r == (2 * t if 0 <= t < n else -1), + domain=[(n, t) for n in range(-1, 30) for t in range(-3, 35)]) +case('l_do_while', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == (n == 0 ? 1 : n))' % R, + '''int i = 0; +do { + i = i + 1; +} while (i < n) + cppverify::invariant(i >= 1 && (i <= n || i == 1)) + cppverify::decreases(n - i); +return i;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == (1 if n == 0 else n), domain=d1(-2, 1005)) +case('l_do_while_wrong', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == n)' % R, + '''int i = 0; +do { + i = i + 1; +} while (i < n) + cppverify::invariant(i >= 1 && (i <= n || i == 1)) + cppverify::decreases(n - i); +return i;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == n, domain=d1(-2, 1005)) +case('l_do_while_overflow', [('int', 'x')], 'int', + 'cppverify::post(%s >= x)' % R, + '''do { + x = x + 1; +} while (x < 10) + cppverify::invariant(true) + cppverify::decreases(10 - x); +return x;''', post=lambda x, r: r >= x, domain=d1(-50, 50, INTB)) +case('l_nested', [('int', 'n'), ('int', 'm')], 'int', + 'cppverify::pre(n >= 0 && n <= 50 && m >= 0 && m <= 50)\ncppverify::post(%s == n * m)' % R, + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c == i * m) + cppverify::decreases(n - i) +{ + for (int j = 0; j < m; j++) + cppverify::invariant(0 <= j && j <= m && c == i * m + j) + cppverify::decreases(m - j) + { c++; } +} +return c;''', pre=lambda n, m: 0 <= n <= 50 and 0 <= m <= 50, post=lambda n, m, r: r == n * m, + domain=[(n, m) for n in range(-1, 53) for m in range(-1, 53)]) +case('l_nested_break', [('int', 'n')], 'int', + 'cppverify::pre(n >= 1 && n <= 50)\ncppverify::post(%s == n * (n + 1) / 2)' % R, + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c == i * (i + 1) / 2) + cppverify::decreases(n - i) +{ + int j = 0; + while (true) + cppverify::invariant(0 <= j && j <= i && c == i * (i + 1) / 2 + j) + cppverify::decreases(i - j) + { c++; if (j == i) break; j++; } +} +return c;''', pre=lambda n: 1 <= n <= 50, post=lambda n, r: r == tri(n), domain=d1(-1, 55)) +case('l_nested_break_wrong', [('int', 'n')], 'int', + 'cppverify::pre(n >= 1 && n <= 50)\ncppverify::post(%s == n * (n - 1) / 2)' % R, + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c == i * (i + 1) / 2) + cppverify::decreases(n - i) +{ + int j = 0; + while (true) + cppverify::invariant(0 <= j && j <= i && c == i * (i + 1) / 2 + j) + cppverify::decreases(i - j) + { c++; if (j == i) break; j++; } +} +return c;''', pre=lambda n: 1 <= n <= 50, post=lambda n, r: r == n * (n - 1) // 2, domain=d1(-1, 55)) +case('l_while_true_return', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0 && x <= 1000)\ncppverify::post(%s == x %% 7)' % R, + '''while (true) + cppverify::invariant(x >= 0 && x % 7 == cppverify::old(x) % 7) + cppverify::decreases(x) +{ if (x < 7) return x; x -= 7; }''', pre=lambda x: 0 <= x <= 1000, post=lambda x, r: r == x % 7, domain=d1(-3, 1003)) +case('l_cond_ub', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0)\ncppverify::post(%s * %s <= n)' % (R, R), + '''int i = 0; +while ((i + 1) * (i + 1) <= n) + cppverify::invariant(i >= 0 && i * i <= n) + cppverify::decreases(n - i) +{ i++; } +return i;''', pre=lambda n: n >= 0, post=lambda n, r: r * r <= n, + domain=d1(0, 100, [2**31 - 1, 2**31 - 2, 2147395600, 2147395599, 2147488281 - 2**31 + 2**31 - 1])) +case('l_step2_neq', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 100)\ncppverify::post(%s == n)' % R, + '''int i = 0; +while (i != n) + cppverify::invariant(i >= 0 && i <= n) + cppverify::decreases(n - i) +{ i += 2; } +return i;''', pre=lambda n: 0 <= n <= 100, post=lambda n, r: r == n, domain=d1(0, 10), alarm_ms=300) +case('l_post_assign_param', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == 2 * n)' % R, + '''int r = 0; +while (n > 0) + cppverify::invariant(n >= 0 && r == 2 * (cppverify::old(n) - n)) + cppverify::decreases(n) +{ n--; r += 2; } +return r;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == 2 * n, domain=d1(-2, 1003)) +case('l_small_type_acc', [('uint8_t', 'n')], 'uint8_t', + 'cppverify::post(%s == (n * (n + 1) / 2) %% 256)' % R, + '''uint8_t s = 0; +for (int i = 1; i <= n; i++) + cppverify::invariant(1 <= i && i <= n + 1 && s == ((i - 1) * i / 2) % 256) + cppverify::decreases(n + 1 - i) +{ s += i; } +return s;''', post=lambda n, r: r == tri(n) % 256) +case('l_short_acc', [('int', 'n')], 'short', + 'cppverify::pre(n >= 0 && n <= 1000)\ncppverify::post(%s == ((n * (n + 1) / 2 + 32768) %% 65536) - 32768)' % R, + '''short s = 0; +for (int i = 1; i <= n; i++) + cppverify::invariant(1 <= i && i <= n + 1 && s == (((i - 1) * i / 2 + 32768) % 65536) - 32768) + cppverify::decreases(n + 1 - i) +{ s += i; } +return s;''', pre=lambda n: 0 <= n <= 1000, post=lambda n, r: r == wrap(tri(n), 'short'), domain=d1(-2, 1003)) +case('l_mul_acc_overflow', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 20)\ncppverify::post(%s >= 1)' % R, + '''int p = 1; +for (int i = 1; i <= n; i++) + cppverify::invariant(1 <= i && i <= n + 1 && p >= 1) + cppverify::decreases(n + 1 - i) +{ p *= i; } +return p;''', pre=lambda n: 0 <= n <= 20, post=lambda n, r: r >= 1, domain=d1(-1, 22)) +case('l_decreases_wrong_sign', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 100)\ncppverify::post(%s == n)' % R, + '''int i = 0; +while (i < n) + cppverify::invariant(0 <= i && i <= n) + cppverify::decreases(i) +{ i++; } +return i;''', pre=lambda n: 0 <= n <= 100, post=lambda n, r: r == n, domain=d1(0, 101)) +case('l_decreases_lex', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 20)\ncppverify::post(%s == n * 3)' % R, + '''int a = n; int b = 0; int c = 0; +while (a > 0 || b > 0) + cppverify::invariant(a >= 0 && b >= 0 && b <= 2 && c == (n - a) * 3 - b) + cppverify::decreases(a, b) +{ if (b > 0) { b--; c++; } else { a--; b = 2; c++; } } +return c;''', pre=lambda n: 0 <= n <= 20, post=lambda n, r: r == 3 * n, domain=d1(-1, 22)) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/loops_bmc.py b/clang/utils/cppverify-differential/cases/loops_bmc.py new file mode 100644 index 0000000000..a93f506bf6 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/loops_bmc.py @@ -0,0 +1,108 @@ +"""BMC backend on loops whose trip count the precondition bounds.""" +import differential as diff +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +def tri(n): + return n * (n + 1) // 2 + +case('b_sum', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == n * (n + 1) / 2)' % R, + 'int s = 0;\nfor (int i = 1; i <= n; i++) { s += i; }\nreturn s;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == tri(n), domain=[(n,) for n in range(-3, 10)]) +case('b_sum_wrong_at4', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == n * (n + 1) / 2)' % R, + 'int s = 0;\nfor (int i = 1; i <= n; i++) { if (i == 4) s += 1; s += i; }\nreturn s;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == tri(n), domain=[(n,) for n in range(-3, 10)]) +case('b_continue', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == n / 2)' % R, + 'int c = 0;\nfor (int i = 0; i < n; i++) { if (i % 2 == 0) continue; c++; }\nreturn c;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == n // 2, domain=[(n,) for n in range(-3, 10)]) +case('b_continue_wrong', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == (n + 1) / 2)' % R, + 'int c = 0;\nfor (int i = 0; i < n; i++) { if (i % 2 == 0) continue; c++; }\nreturn c;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == (n + 1) // 2, domain=[(n,) for n in range(-3, 10)]) +case('b_continue_while', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == n - n / 2)' % R, + 'int c = 0; int i = 0;\nwhile (i < n) { i++; if (i % 2 == 0) continue; c++; }\nreturn c;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == n - n // 2, domain=[(n,) for n in range(-3, 10)]) +case('b_break', [('int', 'n'), ('int', 't')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == (t >= 0 && t < n ? t : n))' % R, + 'int i = 0;\nwhile (i < n) { if (i == t) break; i++; }\nreturn i;', + pre=lambda n, t: 0 <= n <= 5, post=lambda n, t, r: r == (t if 0 <= t < n else n), + domain=[(n, t) for n in range(-1, 8) for t in range(-2, 8)]) +case('b_break_wrong', [('int', 'n'), ('int', 't')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == (t >= 0 && t <= n ? t : n))' % R, + 'int i = 0;\nwhile (i < n) { if (i == t) break; i++; }\nreturn i;', + pre=lambda n, t: 0 <= n <= 5, post=lambda n, t, r: r == (t if 0 <= t <= n else n), + domain=[(n, t) for n in range(-1, 8) for t in range(-2, 8)]) +case('b_return_in_loop', [('int', 'n'), ('int', 't')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == (t >= 0 && t < n ? 2 * t : -1))' % R, + 'for (int i = 0; i < n; i++) { if (i == t) return 2 * i; }\nreturn -1;', + pre=lambda n, t: 0 <= n <= 5, post=lambda n, t, r: r == (2 * t if 0 <= t < n else -1), + domain=[(n, t) for n in range(-1, 8) for t in range(-2, 8)]) +case('b_do_while', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == (n == 0 ? 1 : n))' % R, + 'int i = 0;\ndo { i = i + 1; } while (i < n);\nreturn i;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == (1 if n == 0 else n), domain=[(n,) for n in range(-3, 10)]) +case('b_do_while_wrong', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 5)\ncppverify::post(%s == n)' % R, + 'int i = 0;\ndo { i = i + 1; } while (i < n);\nreturn i;', + pre=lambda n: 0 <= n <= 5, post=lambda n, r: r == n, domain=[(n,) for n in range(-3, 10)]) +case('b_nested', [('int', 'n'), ('int', 'm')], 'int', + 'cppverify::pre(n >= 0 && n <= 3 && m >= 0 && m <= 3)\ncppverify::post(%s == n * m)' % R, + 'int c = 0;\nfor (int i = 0; i < n; i++) { for (int j = 0; j < m; j++) { c++; } }\nreturn c;', + pre=lambda n, m: 0 <= n <= 3 and 0 <= m <= 3, post=lambda n, m, r: r == n * m, + domain=[(n, m) for n in range(-1, 6) for m in range(-1, 6)]) +case('b_nested_break_inner', [('int', 'n')], 'int', + 'cppverify::pre(n >= 1 && n <= 3)\ncppverify::post(%s == n * (n + 1) / 2)' % R, + 'int c = 0;\nfor (int i = 0; i < n; i++) { int j = 0; while (true) { c++; if (j == i) break; j++; } }\nreturn c;', + pre=lambda n: 1 <= n <= 3, post=lambda n, r: r == tri(n), domain=[(n,) for n in range(-1, 6)]) +case('b_nested_continue_outer', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 4)\ncppverify::post(%s == (n / 2) * n)' % R, + 'int c = 0;\nfor (int i = 0; i < n; i++) { if (i % 2 == 0) continue; for (int j = 0; j < n; j++) c++; }\nreturn c;', + pre=lambda n: 0 <= n <= 4, post=lambda n, r: r == (n // 2) * n, domain=[(n,) for n in range(-1, 7)]) +case('b_overflow_iter3', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0)\ncppverify::post(true)', + 'int r = x;\nfor (int i = 0; i < 3; i++) { r = r * 2; }\nreturn r;', + pre=lambda x: x >= 0, post=lambda x, r: True) +case('b_overflow_guarded', [('int', 'x')], 'int', + 'cppverify::pre(x >= 0 && x < 100000000)\ncppverify::post(%s == 8 * x)' % R, + 'int r = x;\nfor (int i = 0; i < 3; i++) { r = r * 2; }\nreturn r;', + pre=lambda x: 0 <= x < 10**8, post=lambda x, r: r == 8 * x) +case('b_unbounded_loop', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0)\ncppverify::post(%s == n)' % R, + 'int i = 0;\nwhile (i < n) { i++; }\nreturn i;', + pre=lambda n: n >= 0, post=lambda n, r: r == n, domain=[(n,) for n in range(0, 200)] + [(2**31 - 1,)], alarm_ms=20000) +case('b_unbounded_bug_late', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 100)\ncppverify::post(%s == n)' % R, + 'int i = 0;\nwhile (i < n) { if (i == 50) i++; i++; }\nreturn i;', + pre=lambda n: 0 <= n <= 100, post=lambda n, r: r == n, domain=[(n,) for n in range(0, 101)]) +case('b_while_cond_side', [('int', 'n')], 'int', + 'cppverify::pre(n >= 0 && n <= 4)\ncppverify::post(%s == n)' % R, + 'int i = 0; int c = 0;\nwhile (i < n && c < 100) { i++; c++; }\nreturn c;', + pre=lambda n: 0 <= n <= 4, post=lambda n, r: r == n, domain=[(n,) for n in range(-1, 7)]) +case('b_u8_wrap_loop', [('uint8_t', 'n')], 'int', + 'cppverify::pre(n <= 4)\ncppverify::post(%s == n)' % R, + 'int c = 0;\nfor (uint8_t i = n; i != 0; i--) { c++; }\nreturn c;', + pre=lambda n: n <= 4, post=lambda n, r: r == n) +case('b_dec_unsigned', [('unsigned', 'n')], 'int', + 'cppverify::pre(n <= 4)\ncppverify::post(%s == n)' % R, + 'int c = 0;\nfor (unsigned i = n; i > 0; --i) { c++; }\nreturn c;', + pre=lambda n: n <= 4, post=lambda n, r: r == n, domain=[(n,) for n in range(0, 10)] + [(2**32 - 1,)], alarm_ms=60000) +case('b_last_iter_ub', [('int', 'n')], 'int', + 'cppverify::pre(n >= 1 && n <= 5)\ncppverify::post(true)', + 'int r = 0;\nfor (int i = 0; i < n; i++) { r = 100 / (4 - i); }\nreturn r;', + pre=lambda n: 1 <= n <= 5, post=lambda n, r: True, domain=[(n,) for n in range(-1, 8)]) +case('b_last_iter_ub_ok', [('int', 'n')], 'int', + 'cppverify::pre(n >= 1 && n <= 4)\ncppverify::post(true)', + 'int r = 0;\nfor (int i = 0; i < n; i++) { r = 100 / (4 - i); }\nreturn r;', + pre=lambda n: 1 <= n <= 4, post=lambda n, r: True, domain=[(n,) for n in range(-1, 8)]) + +CASES = C +CONFIGS = ('bmc6', 'bmc10', 'bmc6bv') diff --git a/clang/utils/cppverify-differential/cases/pointers.py b/clang/utils/cppverify-differential/cases/pointers.py new file mode 100644 index 0000000000..e84bf2cd0e --- /dev/null +++ b/clang/utils/cppverify-differential/cases/pointers.py @@ -0,0 +1,256 @@ +"""Pointers, buffers, frames, aliasing, references.""" +import itertools +import random +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +O = 'cppverify::old' +FA = 'cppverify::forall' +EX = 'cppverify::exists' +V = 'cppverify::valid' +C = [] + + +def rbuf(rng, n, t, lo=None, hi=None): + a, b = trange(t) + if lo is not None: + a = max(a, lo) + if hi is not None: + b = min(b, hi) + out = [] + for _ in range(n): + r = rng.random() + if r < 0.15: + out.append(rng.choice([a, b, 0, 1, -1 if a < 0 else 0])) + elif r < 0.6: + out.append(rng.randint(max(a, -20), min(b, 20))) + else: + out.append(rng.randint(a, b)) + return out + +def case(*a, **k): + C.append(PCase(*a, **k)) + +def gen_buf_n(t, nmax=8, count=400, lo=None, hi=None, extra_scalars=None, seed=1): + def g(): + rng = random.Random(seed) + out = [] + for _ in range(count): + n = rng.randint(0, nmax) + d = {'n': n, 'a': rbuf(rng, n, t, lo, hi)} + if extra_scalars: + for k, f in extra_scalars.items(): + d[k] = f(rng) + out.append(d) + return out + return g + +def objs(t, names, vals): + return [dict(zip(names, combo)) for combo in itertools.product(vals, repeat=len(names))] + +IV = [-2**31, -2**31 + 1, -1000, -1, 0, 1, 7, 1000, 2**31 - 2, 2**31 - 1] + +case('p_swap', [('o', 'int', 'a'), ('o', 'int', 'b')], 'void', + 'cppverify::pre(a != nullptr && b != nullptr)\ncppverify::modifies(*a, *b)\ncppverify::post(*a == %s(*b) && *b == %s(*a))' % (O, O), + 'int t = *a; *a = *b; *b = t;', inputs=objs('int', ['a', 'b'], IV), + post=lambda i, b, r: b[0] == [i['b']] and b[1] == [i['a']]) +case('p_frame_violation', [('o', 'int', 'a'), ('o', 'int', 'b')], 'void', + 'cppverify::pre(a != nullptr && b != nullptr)\ncppverify::modifies(*a)\ncppverify::post(*a == 1)', + '*a = 1; *b = 2;', inputs=objs('int', ['a', 'b'], [0, 1]), + post=lambda i, b, r: b[0] == [1]) +case('p_frame_ok', [('o', 'int', 'a'), ('o', 'int', 'b')], 'void', + 'cppverify::pre(a != nullptr && b != nullptr)\ncppverify::modifies(*a)\ncppverify::post(*b == %s(*b) && *a == 1)' % O, + '*a = 1;', inputs=objs('int', ['a', 'b'], IV), + post=lambda i, b, r: b[1] == [i['b']] and b[0] == [1]) +case('p_no_modifies_write', [('o', 'int', 'a')], 'void', + 'cppverify::pre(a != nullptr)\ncppverify::post(true)', + '*a = 1;', inputs=objs('int', ['a'], [0]), post=lambda i, b, r: True) +case('p_inc_i8', [('o', 'int8_t', 'p')], 'void', + 'cppverify::pre(p != nullptr)\ncppverify::modifies(*p)\ncppverify::post(*p == (%s(*p) == 127 ? -128 : %s(*p) + 1))' % (O, O), + '++*p;', inputs=[{'p': v} for v in range(-128, 128)], + post=lambda i, b, r: b[0] == [wrap(i['p'] + 1, 'int8_t')]) +case('p_compound_u16', [('o', 'uint16_t', 'p')], 'void', + 'cppverify::pre(p != nullptr)\ncppverify::modifies(*p)\ncppverify::post(*p == (%s(*p) * %s(*p)) %% 65536)' % (O, O), + '*p *= *p;', inputs=[{'p': v} for v in range(0, 65536, 7)] + [{'p': 65535}, {'p': 46341}, {'p': 46340}], + post=lambda i, b, r: b[0] == [(i['p'] ** 2) % 65536]) +case('p_compound_i16_ptrs', [('o', 'int16_t', 'p'), ('o', 'int16_t', 'q')], 'void', + 'cppverify::pre(p != nullptr && q != nullptr)\ncppverify::modifies(*p)\ncppverify::post(*p == ((%s(*p) * *q) %% 65536 + 65536 + 32768) %% 65536 - 32768)' % O, + '*p = *p * *q;', inputs=objs('int16_t', ['p', 'q'], [-32768, -32767, -1, 0, 1, 255, 32767]), + post=lambda i, b, r: b[0] == [wrap(i['p'] * i['q'], 'int16_t')]) +case('p_sum_bounded', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000 && %s(k, 0, n, a[k] >= -1000 && a[k] <= 1000))\ncppverify::post(%s >= -1000 * n && %s <= 1000 * n)' % (V, FA, R, R), + '''int s = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && s >= -1000 * i && s <= 1000 * i) + cppverify::decreases(n - i) +{ s += a[i]; } +return s;''', inputs=gen_buf_n('int', lo=-1000, hi=1000), + pre=lambda i: True, post=lambda i, b, r: -1000 * i['n'] <= r <= 1000 * i['n']) +case('p_sum_unbounded', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(true)' % V, + '''int s = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n) + cppverify::decreases(n - i) +{ s += a[i]; } +return s;''', inputs=gen_buf_n('int'), post=lambda i, b, r: True) +case('p_oob_read', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(true)' % V, + '''int s = 0; +for (int i = 0; i <= n; i++) + cppverify::invariant(0 <= i && i <= n + 1) + cppverify::decreases(n + 1 - i) +{ s = a[i]; } +return s;''', inputs=gen_buf_n('int'), post=lambda i, b, r: True) +case('p_reverse', [('b', 'int', 'a', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 100000)\ncppverify::modifies(*a)\ncppverify::post(%s(k, 0, n, a[k] == %s(a[n - 1 - k])))' % (V, FA, O), + '''int i = 0; +int j = n - 1; +while (i < j) + cppverify::invariant(0 <= i && i <= n && j == n - 1 - i && i <= j + 1) + cppverify::invariant(cppverify::forall(k, 0, i, a[k] == cppverify::old(a[n - 1 - k]))) + cppverify::invariant(cppverify::forall(k, j + 1, n, a[k] == cppverify::old(a[n - 1 - k]))) + cppverify::invariant(cppverify::forall(k, i, j + 1, a[k] == cppverify::old(a[k]))) + cppverify::decreases(j - i) +{ int t = a[i]; a[i] = a[j]; a[j] = t; i = i + 1; j = j - 1; }''', inputs=gen_buf_n('int'), + post=lambda i, b, r: b[0] == list(reversed(i['a']))) +case('p_max', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 1 && n <= 1000)\ncppverify::post(%s(k, 0, n, %s >= a[k]) && %s(k, 0, n, %s == a[k]))' % (V, FA, R, EX, R), + '''int m = a[0]; +for (int i = 1; i < n; i++) + cppverify::invariant(1 <= i && i <= n && cppverify::forall(k, 0, i, m >= a[k]) && cppverify::exists(k, 0, i, m == a[k])) + cppverify::decreases(n - i) +{ if (a[i] > m) m = a[i]; } +return m;''', inputs=gen_buf_n('int'), pre=lambda i: i['n'] >= 1, + post=lambda i, b, r: r == max(i['a'])) +case('p_find', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'x')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(%s == -1 ? %s(k, 0, n, a[k] != x) : (0 <= %s && %s < n && a[%s] == x && %s(k, 0, %s, a[k] != x)))' % (V, R, FA, R, R, R, FA, R), + '''for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && cppverify::forall(k, 0, i, a[k] != x)) + cppverify::decreases(n - i) +{ if (a[i] == x) return i; } +return -1;''', inputs=gen_buf_n('int', lo=-3, hi=3, extra_scalars={'x': lambda r: r.randint(-3, 3)}), + post=lambda i, b, r: r == (i['a'].index(i['x']) if i['x'] in i['a'] else -1)) +case('p_count_bad_post', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'x')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(%s < n)' % (V, R), + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && 0 <= c && c <= i) + cppverify::decreases(n - i) +{ if (a[i] == x) c++; } +return c;''', inputs=gen_buf_n('int', lo=-2, hi=2, extra_scalars={'x': lambda r: r.randint(-2, 2)}), + post=lambda i, b, r: r < i['n']) +case('p_copy', [('b', 'int', 'd', 'n'), ('b', 'const int', 's', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(d, n) && %s(s, n) && n >= 0 && n <= 1000)\ncppverify::modifies(*d)\ncppverify::post(%s(k, 0, n, d[k] == s[k]))' % (V, V, FA), + '''int j = 0; +while (j < n) + cppverify::invariant(0 <= j && j <= n && cppverify::forall(k, 0, j, d[k] == s[k])) + cppverify::decreases(n - j) +{ d[j] = s[j]; j = j + 1; }''', + inputs=lambda: [{'n': n, 'd': [0] * n, 's': list(range(n))} for n in range(0, 9)], + post=lambda i, b, r: b[0] == i['s']) +case('p_write_read_other', [('o', 'int', 'a'), ('o', 'int', 'b')], 'int', + 'cppverify::pre(a != nullptr && b != nullptr)\ncppverify::modifies(*a)\ncppverify::post(%s == %s(*b))' % (R, O), + '*a = 5; return *b;', inputs=objs('int', ['a', 'b'], [0, 5, 7]), post=lambda i, b, r: r == i['b']) +case('p_alias_opt_out', [('o', 'int', 'a'), ('a', 'int', 'b', 'a')], 'int', + 'cppverify::aliases(a, b)\ncppverify::pre(a != nullptr && b != nullptr)\ncppverify::modifies(*a)\ncppverify::post(%s == %s(*b))' % (R, O), + '*a = 5; return *b;', inputs=objs('int', ['a'], [0, 5, 7]), post=lambda i, b, r: r == i['a']) +case('p_alias_ok', [('o', 'int', 'a'), ('a', 'int', 'b', 'a')], 'int', + 'cppverify::aliases(a, b)\ncppverify::pre(a != nullptr && b != nullptr)\ncppverify::modifies(*a)\ncppverify::post(%s == 5 || %s == %s(*b))' % (R, R, O), + '*a = 5; return *b;', inputs=objs('int', ['a'], [0, 5, 7]), post=lambda i, b, r: r == 5 or r == i['a']) +case('p_null_deref', [('n', 'int', 'p')], 'int', + 'cppverify::post(true)', 'return *p;', inputs=[{}], post=lambda i, b, r: True) +case('p_single_obj_idx1', [('o', 'int', 'p')], 'int', + 'cppverify::pre(p != nullptr)\ncppverify::post(true)', 'return p[1];', inputs=[{'p': 3}], post=lambda i, b, r: True) +case('p_arith_past_end', [('b', 'int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 1 && n <= 100)\ncppverify::post(true)' % V, + 'int *q = a + n + 1; return q == a ? 1 : 0;', inputs=gen_buf_n('int', count=20), pre=lambda i: i['n'] >= 1, + post=lambda i, b, r: True) +case('p_one_past_end_ok', [('b', 'int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 1 && n <= 100)\ncppverify::post(%s == 0)' % (V, R), + 'int *q = a + n; return q == a ? 1 : 0;', inputs=gen_buf_n('int', count=20), pre=lambda i: i['n'] >= 1, + post=lambda i, b, r: r == 0) +case('p_ref_inc', [('r', 'int', 'x')], 'void', + 'cppverify::pre(x < 100)\ncppverify::modifies(x)\ncppverify::post(x == %s(x) + 1)' % O, + 'x++;', inputs=[{'x': v} for v in IV], pre=lambda i: i['x'] < 100, post=lambda i, b, r: b[0] == [i['x'] + 1]) +case('p_ref_frame', [('r', 'int', 'x'), ('r', 'int', 'y')], 'void', + 'cppverify::modifies(x)\ncppverify::post(x == 1)', 'x = 1; y = 2;', inputs=[{'x': 0, 'y': 0}], + post=lambda i, b, r: b[0] == [1]) +case('p_ref_i8_compound', [('r', 'int8_t', 'x'), ('s', 'int', 'k')], 'void', + 'cppverify::modifies(x)\ncppverify::post(x == ((%s(x) + k) %% 256 + 256 + 128) %% 256 - 128)' % O, + 'x += k;', inputs=[{'x': x, 'k': k} for x in (-128, -1, 0, 1, 127) for k in IV + [128, 255, 256, -129]], + post=lambda i, b, r: b[0] == [wrap(i['x'] + i['k'], 'int8_t')]) +case('p_struct_swap', [('o', 'S', 's')], 'void', + 'cppverify::pre(s != nullptr)\ncppverify::modifies(*s)\ncppverify::post(s->x == %s(s->y) && s->y == %s(s->x))' % (O, O), + 'int t = s->x; s->x = s->y; s->y = t;', + prelude='struct S { int x; int y; };', inputs=[], post=None) +case('p_u8_sum', [('b', 'const uint8_t', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(%s >= 0 && %s <= 255 * n)' % (V, R, R), + '''int s = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && s >= 0 && s <= 255 * i) + cppverify::decreases(n - i) +{ s += a[i]; } +return s;''', inputs=gen_buf_n('uint8_t'), post=lambda i, b, r: r == sum(i['a'])) +case('p_char_neg_count', [('b', 'const char', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(%s >= 0 && %s <= n)' % (V, R, R), + '''int c = 0; +for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && c >= 0 && c <= i) + cppverify::decreases(n - i) +{ if (a[i] < 0) c++; } +return c;''', inputs=gen_buf_n('char'), post=lambda i, b, r: r == sum(1 for v in i['a'] if v < 0)) +case('p_memset_u8', [('b', 'uint8_t', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'v')], 'void', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::modifies(*a)\ncppverify::post(%s(k, 0, n, a[k] == (uint8_t)v))' % (V, FA), + '''for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && cppverify::forall(k, 0, i, a[k] == (uint8_t)v)) + cppverify::decreases(n - i) +{ a[i] = v; }''', inputs=gen_buf_n('uint8_t', extra_scalars={'v': lambda r: r.choice([-1, 0, 255, 256, 300, -129, 2**31 - 1])}), + post=lambda i, b, r: b[0] == [i['v'] % 256] * i['n']) +case('p_memset_u8_wrong', [('b', 'uint8_t', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'v')], 'void', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::modifies(*a)\ncppverify::post(%s(k, 0, n, a[k] == v))' % (V, FA), + '''for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n && cppverify::forall(k, 0, i, a[k] == (uint8_t)v)) + cppverify::decreases(n - i) +{ a[i] = v; }''', inputs=gen_buf_n('uint8_t', extra_scalars={'v': lambda r: r.choice([-1, 0, 255, 256, 300, -129])}), + post=lambda i, b, r: all(x == i['v'] for x in b[0])) +case('p_incall', [('b', 'int', 'a', 'n'), ('s', 'int', 'n')], 'void', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 100 && %s(k, 0, n, a[k] < 1000))\ncppverify::modifies(*a)\ncppverify::post(%s(k, 0, n, a[k] == %s(a[k]) + 1))' % (V, FA, FA, O), + '''for (int i = 0; i < n; i++) + cppverify::invariant(0 <= i && i <= n) + cppverify::invariant(cppverify::forall(k, 0, i, a[k] == cppverify::old(a[k]) + 1)) + cppverify::invariant(cppverify::forall(k, i, n, a[k] == cppverify::old(a[k]))) + cppverify::decreases(n - i) +{ a[i] = a[i] + 1; }''', inputs=gen_buf_n('int', hi=999), post=lambda i, b, r: b[0] == [x + 1 for x in i['a']]) +case('p_index_u8', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'i')], 'int', + 'cppverify::pre(%s(a, n) && n >= 1 && n <= 300 && i >= 0 && i < n)\ncppverify::post(%s == a[(uint8_t)i])' % (V, R), + 'return a[(uint8_t)i];', + inputs=lambda: [{'n': n, 'a': list(range(n)), 'i': i} for n in (1, 2, 255, 256, 257, 300) for i in range(0, n, 1 if n < 10 else 13)], + pre=lambda i: 1 <= i['n'] <= 300 and 0 <= i['i'] < i['n'], post=lambda i, b, r: r == i['a'][i['i'] % 256]) +case('p_index_neg', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n'), ('s', 'int', 'i')], 'int', + 'cppverify::pre(%s(a, n) && n >= 1 && n <= 10 && i >= -1 && i < n)\ncppverify::post(true)' % V, + 'return a[i];', inputs=lambda: [{'n': n, 'a': list(range(n)), 'i': i} for n in (1, 3) for i in range(-1, n)], + pre=lambda i: True, post=lambda i, b, r: True) +case('p_ptr_walk', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000 && %s(k, 0, n, a[k] >= 0 && a[k] <= 10))\ncppverify::post(%s >= 0 && %s <= 10 * n)' % (V, FA, R, R), + '''int s = 0; +const int *q = a; +int i = 0; +while (i < n) + cppverify::invariant(0 <= i && i <= n && q == a + i && s >= 0 && s <= 10 * i) + cppverify::decreases(n - i) +{ s += *q; q = q + 1; i = i + 1; } +return s;''', inputs=gen_buf_n('int', lo=0, hi=10), post=lambda i, b, r: r == sum(i['a'])) +case('p_ptr_walk_oob', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(%s(a, n) && n >= 0 && n <= 1000)\ncppverify::post(true)' % V, + '''int s = 0; +const int *q = a; +int i = 0; +while (i <= n) + cppverify::invariant(0 <= i && i <= n + 1 && q == a + i) + cppverify::decreases(n + 1 - i) +{ s = *q; q = q + 1; i = i + 1; } +return s;''', inputs=gen_buf_n('int'), post=lambda i, b, r: True) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/pointers_bmc.py b/clang/utils/cppverify-differential/cases/pointers_bmc.py new file mode 100644 index 0000000000..7654bd0f60 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/pointers_bmc.py @@ -0,0 +1,15 @@ +"""The pointer cases under bounded model checking. A bounded-safe verdict +covers the executions within the bound: a buffer of n elements takes n +iterations.""" +import copy + +from cases import pointers + +CASES = [] +for case in pointers.CASES: + if case.domain != []: + bounded = copy.copy(case) + bounded.name = case.name + '_bmc' + bounded.iterations = lambda inp: inp.get('n', 0) + CASES.append(bounded) +CONFIGS = ('bmc10', 'bmc10bv') diff --git a/clang/utils/cppverify-differential/cases/records.py b/clang/utils/cppverify-differential/cases/records.py new file mode 100644 index 0000000000..5b007c370e --- /dev/null +++ b/clang/utils/cppverify-differential/cases/records.py @@ -0,0 +1,72 @@ +"""Structs by value with small-type fields, struct returns, nested structs.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +S = 'struct S { int8_t a; uint16_t b; int c; };' +case('st_fields_promote', [('int8_t', 'a'), ('uint16_t', 'b')], 'int', + 'cppverify::post(%s == a * b)' % R, 'S s; s.a = a; s.b = b; s.c = 0; return s.a * s.b;', + prelude=S, post=lambda a, b, r: r == a * b, + domain=[(a, b) for a in range(-128, 128) for b in (0, 1, 2, 255, 256, 32767, 32768, 65534, 65535)]) +case('st_field_compound', [('int8_t', 'a'), ('int', 'k')], 'int', + 'cppverify::pre(k > -1000 && k < 1000)\ncppverify::post(%s == ((a + k) %% 256 + 256 + 128) %% 256 - 128)' % R, + 'S s; s.a = a; s.b = 0; s.c = 0; s.a += k; return s.a;', prelude=S, + pre=lambda a, k: -1000 < k < 1000, post=lambda a, k, r: r == wrap(a + k, 'int8_t'), + domain=[(a, k) for a in range(-128, 128) for k in (-999, -300, -129, -128, -1, 0, 1, 127, 128, 255, 256, 999)]) +case('st_field_inc_u16', [('uint16_t', 'b')], 'int', + 'cppverify::post(%s == (b + 1) %% 65536)' % R, 'S s; s.a = 0; s.b = b; s.c = 0; s.b++; return s.b;', + prelude=S, post=lambda b, r: r == (b + 1) % 65536) +case('st_field_mul_u16', [('uint16_t', 'b')], 'int', + 'cppverify::post(%s == (b * b) %% 65536)' % R, 'S s; s.a = 0; s.b = b; s.c = 0; s.b *= s.b; return s.b;', + prelude=S, post=lambda b, r: r == (b * b) % 65536) +SP = S + ''' +S mk(int8_t a, uint16_t b, int c) + cppverify::post(cppverify::result.a == a && cppverify::result.b == b && cppverify::result.c == c) +{ S s; s.a = a; s.b = b; s.c = c; return s; }''' +case('st_ret_use', [('int', 'x')], 'int', + 'cppverify::post(%s == ((x %% 256) + 384) %% 256 - 128)' % R, 'S s = mk(x, 0, 0); return s.a;', + prelude=SP, post=lambda x, r: r == wrap(x, 'int8_t')) +case('st_ret_use_wrong', [('int', 'x')], 'int', + 'cppverify::post(%s == x)' % R, 'S s = mk(x, 0, 0); return s.a;', + prelude=SP, post=lambda x, r: r == x) +SPASS = S + ''' +int sum3(S s) + cppverify::post(cppverify::result == s.a + s.b + s.c || true) +{ return s.a + s.b; }''' +case('st_pass_by_value', [('int8_t', 'a'), ('uint16_t', 'b')], 'int', + 'cppverify::post(%s == a + b)' % R, 'S s; s.a = a; s.b = b; s.c = 7; int r = sum3(s); return r;', + prelude=SPASS, post=lambda a, b, r: True) +SMOD = S + ''' +S bump(S s) + cppverify::pre(s.c < 1000 && s.c > -1000) + cppverify::post(cppverify::result.c == s.c + 1 && cppverify::result.a == s.a) +{ s.c = s.c + 1; return s; }''' +case('st_callee_modifies_copy', [('int', 'c')], 'int', + 'cppverify::pre(c < 900 && c > -900)\ncppverify::post(%s == c)' % R, 'S s; s.a = 1; s.b = 2; s.c = c; S t = bump(s); return s.c;', + prelude=SMOD, pre=lambda c: -900 < c < 900, post=lambda c, r: r == c, domain=[(c,) for c in range(-905, 905)]) +case('st_callee_result', [('int', 'c')], 'int', + 'cppverify::pre(c < 900 && c > -900)\ncppverify::post(%s == c + 1)' % R, 'S s; s.a = 1; s.b = 2; s.c = c; S t = bump(s); return t.c;', + prelude=SMOD, pre=lambda c: -900 < c < 900, post=lambda c, r: r == c + 1, domain=[(c,) for c in range(-905, 905)]) +case('st_copy_independent', [('int', 'c')], 'int', + 'cppverify::post(%s == c)' % R, 'S s; s.a = 1; s.b = 2; s.c = c; S t = s; t.c = 0; return s.c;', + prelude=S, post=lambda c, r: r == c) +case('st_assign_copy', [('int', 'c')], 'int', + 'cppverify::post(%s == 0)' % R, 'S s; s.a = 1; s.b = 2; s.c = c; S t; t = s; t.c = 0; return t.c;', + prelude=S, post=lambda c, r: r == 0) +NEST = 'struct In { int8_t v; }; struct Out { In i; uint8_t w; };' +case('st_nested', [('int', 'x')], 'int', + 'cppverify::post(%s == (((x %% 256) + 384) %% 256 - 128) + (x %% 256 + 256) %% 256)' % R, + 'Out o; o.i.v = x; o.w = x; return o.i.v + o.w;', prelude=NEST, + post=lambda x, r: r == wrap(x, 'int8_t') + x % 256) +case('st_uninit_field', [('int', 'x')], 'int', + 'cppverify::post(true)', 'S s; s.a = 1; return s.c;', prelude=S, post=lambda x, r: True) +case('st_bool_field', [('int', 'x')], 'int', + 'cppverify::post(%s == (x != 0 ? 2 : 0))' % R, + 'struct B { bool f; } b; b.f = x; return b.f + b.f;', post=lambda x, r: r == (2 if x != 0 else 0)) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/cases/selftest.py b/clang/utils/cppverify-differential/cases/selftest.py new file mode 100644 index 0000000000..37dfd80e7c --- /dev/null +++ b/clang/utils/cppverify-differential/cases/selftest.py @@ -0,0 +1,39 @@ +"""Cases that check the tool itself. Two restate their contract wrongly in +Python on purpose, so that a right verdict reads as a problem: the tool must +report it.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' + +CASES = [ + Case('self_add', [('int8_t', 'x'), ('int8_t', 'y')], 'int', + 'cppverify::post(%s == x + y)' % R, 'return x + y;', + post=lambda x, y, r: r == x + y), + Case('self_overflow', [('int', 'x')], 'int', + 'cppverify::post(%s == x + 1)' % R, 'return x + 1;', + post=lambda x, r: r == x + 1), + Case('self_bound', [('int16_t', 'x')], 'int16_t', + 'cppverify::pre(x >= 0)\ncppverify::post(%s >= 0)' % R, 'return x;', + pre=lambda x: x >= 0, post=lambda x, r: r > 0), + Case('self_wrong_at_5', [('int8_t', 'x')], 'int', + 'cppverify::post(%s == x)' % R, 'return x == 5 ? 6 : x;', + post=lambda x, r: True), + Case('self_contract_div', [('int8_t', 'x')], 'int', + 'cppverify::post(100 / x == 100 / x)', 'return 0;'), + PCase('self_read_past', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'int', + 'cppverify::pre(cppverify::valid(a, n) && n >= 1 && n <= 4)', + 'return a[n];', + [{'n': n, 'a': [7] * n} for n in range(1, 5)], + pre=lambda inp: 1 <= inp['n'] <= 4), + PCase('self_sum', [('b', 'const int', 'a', 'n'), ('s', 'int', 'n')], 'long', + 'cppverify::pre(cppverify::valid(a, n) && n >= 0 && n <= 4)\n' + 'cppverify::post(%s >= -8589934592 && %s <= 8589934588)' % (R, R), + 'long s = 0;\nfor (int i = 0; i < n; i++)\n' + ' cppverify::invariant(0 <= i && i <= n && s >= -2147483648L * i && s <= 2147483647L * i)\n' + ' cppverify::decreases(n - i)\n' + '{ s += a[i]; }\nreturn s;', + [{'n': n, 'a': [v] * n} for n in range(5) for v in (-2**31, -1, 0, 1, 2**31 - 1)], + pre=lambda inp: 0 <= inp['n'] <= 4, + post=lambda inp, bufs, r: -8589934592 <= r <= 8589934588), +] +CONFIGS = ('z3',) diff --git a/clang/utils/cppverify-differential/cases/shifts_division.py b/clang/utils/cppverify-differential/cases/shifts_division.py new file mode 100644 index 0000000000..f92adcbd66 --- /dev/null +++ b/clang/utils/cppverify-differential/cases/shifts_division.py @@ -0,0 +1,224 @@ +"""Shifts, division/modulo, __int128, enums, character types.""" +from differential import * # noqa: F401,F403 + +R = 'cppverify::result' +C = [] + +def case(*a, **k): + C.append(Case(*a, **k)) + +def shdom(xt, lo=-3, hi=40): + xs = boundary(xt) + list(range(-20, 21)) + xs = sorted(set(v for v in xs if in_range(v, xt))) + return [(x, s) for x in xs for s in range(lo, hi)] + +W32 = '((%s) + 2147483648) %% 4294967296 - 2147483648' + +# --- left shifts ----------------------------------------------------------- +for std in ('c++17', 'c++20'): + sfx = std[-2:] + case('shl_any_' + sfx, [('int', 'x'), ('int', 's')], 'int', + 'cppverify::pre(0 <= s && s < 32)\ncppverify::post(%s == %s)' % (R, W32 % ('x * (1L << s) % 4294967296 + 4294967296')), + 'return x << s;', pre=lambda x, s: 0 <= s < 32, + post=lambda x, s, r: r == wrap(x << s, 'int'), std=std, domain=shdom('int')) + case('shl_u8_' + sfx, [('uint8_t', 'a'), ('int', 's')], 'int', + 'cppverify::pre(0 <= s && s < 32)\ncppverify::post(%s == %s)' % (R, W32 % ('a * (1L << s) % 4294967296')), + 'return a << s;', pre=lambda a, s: 0 <= s < 32, + post=lambda a, s, r: r == wrap(a << s, 'int'), std=std, + domain=[(a, s) for a in range(256) for s in range(-2, 34)]) + case('shl_i8_' + sfx, [('int8_t', 'a'), ('int', 's')], 'int', + 'cppverify::pre(0 <= s && s < 32)\ncppverify::post(%s == %s)' % (R, W32 % ('a * (1L << s) % 4294967296 + 4294967296')), + 'return a << s;', pre=lambda a, s: 0 <= s < 32, + post=lambda a, s, r: r == wrap(a << s, 'int'), std=std, + domain=[(a, s) for a in range(-128, 128) for s in range(-2, 34)]) + case('shl_assign_i8_' + sfx, [('int8_t', 'a'), ('int', 's')], 'int8_t', + 'cppverify::pre(0 <= s && s < 8)\ncppverify::post(%s == (a * (1 << s) %% 256 + 384) %% 256 - 128)' % R, + 'a <<= s; return a;', pre=lambda a, s: 0 <= s < 8, + post=lambda a, s, r: r == wrap(a << s, 'int8_t'), std=std, + domain=[(a, s) for a in range(-128, 128) for s in range(-2, 12)]) + case('shl_long_' + sfx, [('long', 'x'), ('int', 's')], 'long', + 'cppverify::pre(0 <= s && s < 64 && x >= 0 && x <= (9223372036854775807L >> s))\ncppverify::post(%s >= x)' % R, + 'return x << s;', pre=lambda x, s: 0 <= s < 64 and 0 <= x <= ((2**63 - 1) >> s), + post=lambda x, s, r: r >= x, std=std, domain=shdom('long', -2, 70)) + case('shr_neg_' + sfx, [('int', 'x'), ('int', 's')], 'int', + 'cppverify::pre(0 <= s && s < 32)\ncppverify::post(%s * (1L << s) <= x && x < (%s + 1) * (1L << s))' % (R, R), + 'return x >> s;', pre=lambda x, s: 0 <= s < 32, + post=lambda x, s, r: r * 2**s <= x < (r + 1) * 2**s, std=std, domain=shdom('int')) + case('shr_i8_' + sfx, [('int8_t', 'x'), ('int', 's')], 'int8_t', + 'cppverify::pre(0 <= s && s < 32)\ncppverify::post(%s * (1L << s) <= x && x < (%s + 1) * (1L << s))' % (R, R), + 'x >>= s; return x;', pre=lambda x, s: 0 <= s < 32, + post=lambda x, s, r: r * 2**s <= x < (r + 1) * 2**s, std=std, + domain=[(a, s) for a in range(-128, 128) for s in range(-2, 34)]) + case('shl_unsigned_' + sfx, [('unsigned', 'x'), ('unsigned', 's')], 'unsigned', + 'cppverify::pre(s < 32)\ncppverify::post(%s == x * (1L << s) %% 4294967296)' % R, + 'return x << s;', pre=lambda x, s: s < 32, + post=lambda x, s, r: r == (x << s) % 2**32, std=std, + domain=[(x, s) for x in boundary('unsigned') for s in range(0, 40)]) + case('shl_one31_' + sfx, [('int', 's')], 'int', + 'cppverify::pre(s >= 0 && s <= 31)\ncppverify::post(s == 31 ? %s == -2147483647 - 1 : %s == (1L << s))' % (R, R), + 'return 1 << s;', pre=lambda s: 0 <= s <= 31, + post=lambda s, r: r == wrap(1 << s, 'int'), std=std, domain=[(s,) for s in range(-5, 40)]) + case('shl_two31_' + sfx, [('int', 's')], 'int', + 'cppverify::pre(s >= 0 && s <= 31)\ncppverify::post(true)', + 'return 2 << s;', pre=lambda s: 0 <= s <= 31, + post=lambda s, r: True, std=std, domain=[(s,) for s in range(-5, 40)]) + case('shl_amount_u8_' + sfx, [('int', 'x'), ('uint8_t', 's')], 'int', + 'cppverify::pre(x >= 0 && x <= 1 && s <= 30)\ncppverify::post(%s == x * (1L << s))' % R, + 'return x << s;', pre=lambda x, s: 0 <= x <= 1 and s <= 30, + post=lambda x, s, r: r == x * 2**s, std=std, domain=[(x, s) for x in range(-2, 4) for s in range(256)]) + case('shl_amount_long_' + sfx, [('int', 'x'), ('long', 's')], 'int', + 'cppverify::pre(x == 1 && s >= 0 && s <= 30)\ncppverify::post(%s == (1L << s))' % R, + 'return x << s;', pre=lambda x, s: x == 1 and 0 <= s <= 30, + post=lambda x, s, r: r == 2**s, std=std, + domain=[(x, s) for x in range(-2, 4) for s in list(range(-3, 70)) + [2**32, 2**32 + 1, -2**63, 2**63 - 1]]) + case('shl_large_amount_' + sfx, [('int', 'x'), ('int', 's')], 'int', + 'cppverify::pre(x == 0 && s >= 0 && s < 40)\ncppverify::post(%s == 0)' % R, + 'return x << s;', pre=lambda x, s: x == 0 and 0 <= s < 40, + post=lambda x, s, r: r == 0, std=std, domain=[(x, s) for x in (0, 1) for s in range(-3, 45)]) + case('shr_large_amount_' + sfx, [('unsigned', 'x'), ('int', 's')], 'unsigned', + 'cppverify::pre(s >= 0 && s <= 32)\ncppverify::post(%s <= x)' % R, + 'return x >> s;', pre=lambda x, s: 0 <= s <= 32, + post=lambda x, s, r: r <= x, std=std, domain=[(x, s) for x in boundary('unsigned') for s in range(-3, 40)]) + case('shl_u64_' + sfx, [('uint64_t', 'x'), ('int', 's')], 'uint64_t', + 'cppverify::pre(s >= 0 && s < 64)\ncppverify::post(%s == x * (1UL << s) %% 18446744073709551615 + 0 || true)' % R, + 'return x << s;', pre=lambda x, s: 0 <= s < 64, + post=lambda x, s, r: True, std=std, domain=[(x, s) for x in boundary('uint64_t') for s in range(-2, 70)]) + case('shl_u16_assign_' + sfx, [('uint16_t', 'a'), ('int', 's')], 'uint16_t', + 'cppverify::pre(0 <= s && s < 32)\ncppverify::post(%s == a * (1L << s) %% 65536)' % R, + 'a <<= s; return a;', pre=lambda a, s: 0 <= s < 32, + post=lambda a, s, r: r == (a << s) % 65536, std=std, + domain=[(a, s) for a in list(range(0, 300)) + list(range(32700, 32800)) + list(range(65000, 65536)) for s in range(-2, 34)]) + +# --- division / modulo ----------------------------------------------------- +case('div_int', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x / y)' % R, 'return x / y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tdiv(x, y)) +case('rem_int', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x %% y)' % R, 'return x % y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tmod(x, y)) +case('rem_int_noguard_minus1', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::pre(y != 0 && x != -2147483647 - 1)\ncppverify::post(%s == x - (x / y) * y)' % R, 'return x % y;', + pre=lambda x, y: y != 0 and x != -2**31, post=lambda x, y, r: r == x - tdiv(x, y) * y) +case('rem_long', [('long', 'x'), ('long', 'y')], 'long', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x %% y)' % R, 'return x % y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tmod(x, y)) +case('div_i8', [('int8_t', 'x'), ('int8_t', 'y')], 'int', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x / y)' % R, 'return x / y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tdiv(x, y)) +case('rem_i8', [('int8_t', 'x'), ('int8_t', 'y')], 'int8_t', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x %% y)' % R, 'return x % y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tmod(x, y)) +case('div_i8_ret8', [('int8_t', 'x'), ('int8_t', 'y')], 'int8_t', + 'cppverify::pre(y != 0)\ncppverify::post(x == -128 && y == -1 ? %s == -128 : %s == x / y)' % (R, R), + 'return x / y;', pre=lambda x, y: y != 0, post=lambda x, y, r: r == wrap(tdiv(x, y), 'int8_t')) +case('div_assign_i8', [('int8_t', 'x'), ('int8_t', 'y')], 'int8_t', + 'cppverify::pre(y != 0)\ncppverify::post(x == -128 && y == -1 ? %s == -128 : %s == x / y)' % (R, R), + 'x /= y; return x;', pre=lambda x, y: y != 0, post=lambda x, y, r: r == wrap(tdiv(x, y), 'int8_t')) +case('rem_assign_i16', [('int16_t', 'x'), ('int16_t', 'y')], 'int16_t', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x %% y)' % R, + 'x %= y; return x;', pre=lambda x, y: y != 0, post=lambda x, y, r: r == tmod(x, y)) +case('div_mixed', [('int', 'a'), ('unsigned', 'b')], 'unsigned', + 'cppverify::pre(b != 0)\ncppverify::post(%s == (a < 0 ? a + 4294967296 : a) / b)' % R, 'return a / b;', + pre=lambda a, b: b != 0, post=lambda a, b, r: r == (a % 2**32) // b) +case('rem_mixed', [('int', 'a'), ('unsigned', 'b')], 'unsigned', + 'cppverify::pre(b != 0)\ncppverify::post(%s == (a < 0 ? a + 4294967296 : a) %% b)' % R, 'return a % b;', + pre=lambda a, b: b != 0, post=lambda a, b, r: r == (a % 2**32) % b) +case('div_int_by_long', [('int', 'x'), ('long', 'y')], 'long', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x / y)' % R, 'return x / y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tdiv(x, y)) +case('div_long', [('long', 'x'), ('long', 'y')], 'long', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x / y)' % R, 'return x / y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tdiv(x, y)) +case('urem_neg3', [('unsigned', 'u')], 'unsigned', + 'cppverify::post(%s == u %% 4294967293)' % R, 'return u % -3;', + post=lambda u, r: r == u % 4294967293) +case('div_u16', [('uint16_t', 'a'), ('uint16_t', 'b')], 'int', + 'cppverify::pre(b != 0)\ncppverify::post(%s == a / b)' % R, 'return a / b;', + pre=lambda a, b: b != 0, post=lambda a, b, r: r == a // b) +case('div_short_circuit', [('int', 'x'), ('int', 'y')], 'bool', + 'cppverify::post(%s == (y != 0 && y != -1 && x / y > 1))' % R, 'return y != 0 && y != -1 && x / y > 1;', + post=lambda x, y, r: r == (1 if (y != 0 and y != -1 and tdiv(x, y) > 1) else 0)) +case('div_short_circuit_bad', [('int', 'x'), ('int', 'y')], 'bool', + 'cppverify::post(true)', 'return y != 0 && x / y > 1;', + post=lambda x, y, r: True) +case('rem_ternary_guard', [('int', 'x'), ('int', 'y')], 'int', + 'cppverify::post(true)', 'return (y == 0 || y == -1) ? 0 : x % y;', + post=lambda x, y, r: True) +case('rem_or_guard', [('int', 'x'), ('int', 'y')], 'bool', + 'cppverify::post(true)', 'return y == 0 || x % y == 0;', + post=lambda x, y, r: True) +case('div_by_constant_neg', [('int', 'x')], 'int', + 'cppverify::post(%s == x / -7)' % R, 'return x / -7;', + post=lambda x, r: r == tdiv(x, -7)) +case('rem_by_constant_neg', [('int', 'x')], 'int', + 'cppverify::post(%s == x %% -7)' % R, 'return x % -7;', + post=lambda x, r: r == tmod(x, -7)) + +# --- __int128 -------------------------------------------------------------- +case('i128_mul64', [('long', 'a'), ('long', 'b')], '__int128', + 'cppverify::post(%s == a * b)' % R, 'return (__int128)a * b;', + post=lambda a, b, r: r == a * b) +case('i128_add', [('__int128', 'a'), ('__int128', 'b')], '__int128', + 'cppverify::post(%s == a + b)' % R, 'return a + b;', + post=lambda a, b, r: r == a + b) +case('u128_add', [('unsigned __int128', 'a'), ('unsigned __int128', 'b')], 'unsigned __int128', + 'cppverify::post(%s == (a + b) %% (((unsigned __int128)1) << 127) || true)' % R, 'return a + b;', + post=lambda a, b, r: True) +case('i128_hi', [('__int128', 'x')], 'long', + 'cppverify::post(true)', 'return (long)(x >> 64);', + post=lambda x, r: r == x >> 64) +case('i128_hi_eq', [('__int128', 'x')], 'long', + 'cppverify::post(%s * 18446744073709551615 + %s <= x)' % (R, R), 'return (long)(x >> 64);', + post=lambda x, r: r * 2**64 <= x) +case('i128_to_long', [('__int128', 'x')], 'long', + 'cppverify::pre(x >= 0 && x < 18446744073709551615)\ncppverify::post(x > 9223372036854775807 ? %s < 0 : %s == x)' % (R, R), + 'return (long)x;', pre=lambda x: 0 <= x < 2**64 - 1, + post=lambda x, r: r < 0 if x > 2**63 - 1 else r == x) +case('i128_div', [('__int128', 'x'), ('__int128', 'y')], '__int128', + 'cppverify::pre(y != 0)\ncppverify::post(%s == x / y)' % R, 'return x / y;', + pre=lambda x, y: y != 0, post=lambda x, y, r: r == tdiv(x, y)) +case('i128_shl', [('__int128', 'x'), ('int', 's')], '__int128', + 'cppverify::pre(s >= 0 && s < 128 && x >= 0 && x < 2)\ncppverify::post(%s >= 0 || s == 127)' % R, + 'return x << s;', pre=lambda x, s: 0 <= s < 128 and 0 <= x < 2, + post=lambda x, s, r: r >= 0 or s == 127, domain=[(x, s) for x in (-1, 0, 1, 2) for s in range(-2, 132)]) + +# --- enums ----------------------------------------------------------------- +case('enum_range', [('int', 'v')], 'int', + 'cppverify::pre(v >= 0 && v <= 3)\ncppverify::post(%s != 3)' % R, 'E e = (E)v; return e;', + prelude='enum E { A, B, C };', + pre=lambda v: 0 <= v <= 3, post=lambda v, r: r != 3, domain=[(v,) for v in range(-3, 10)]) +case('enum_param', [('E', 'e')], 'int', + 'cppverify::post(%s <= 2)' % R, 'return e;', + prelude='enum E { A, B, C };', + post=lambda e, r: r <= 2, domain=[(v,) for v in range(0, 4)]) +case('enum_param_neg', [('G', 'g')], 'int', + 'cppverify::post(%s >= -1)' % R, 'return g;', + prelude='enum G { M = -1, N = 1 };', + post=lambda g, r: r >= -1, domain=[(v,) for v in range(-2, 2)]) +case('enum_fixed', [('F', 'f')], 'int', + 'cppverify::post(%s == 1 || %s == 2)' % (R, R), 'return (int)f;', + prelude='enum class F : uint8_t { X = 1, Y = 2 };', + post=lambda f, r: r in (1, 2), domain=[(v,) for v in range(0, 256)]) +case('enum_from_int_oob', [('int', 'v')], 'int', + 'cppverify::post(true)', 'E e = (E)v; return e;', + prelude='enum E { A, B, C };', + post=lambda v, r: True, domain=[(v,) for v in range(-3, 10)]) +case('enum_cmp', [('E', 'e')], 'bool', + 'cppverify::post(%s == (e == A || e == B || e == C))' % R, 'return e < 3;', + prelude='enum E { A, B, C };', + post=lambda e, r: r == (1 if e in (0, 1, 2) else 0), domain=[(v,) for v in range(0, 4)]) + +# --- character types --------------------------------------------------------- +case('char16_mul', [('char16_t', 'a'), ('char16_t', 'b')], 'int', + 'cppverify::post(%s == a * b)' % R, 'return a * b;', post=lambda a, b, r: r == a * b) +case('char32_add', [('char32_t', 'a')], 'unsigned', + 'cppverify::post(%s == (a + 1) %% 4294967296)' % R, 'return a + 1;', post=lambda a, r: r == (a + 1) % 2**32) +case('char32_add_int', [('char32_t', 'a')], 'long', + 'cppverify::post(%s == a + 1)' % R, 'return a + 1;', post=lambda a, r: r == a + 1) +case('wchar_add', [('wchar_t', 'a')], 'int', + 'cppverify::post(%s == a + 1)' % R, 'return a + 1;', post=lambda a, r: r == a + 1) +case('wchar_neg', [('wchar_t', 'a')], 'bool', + 'cppverify::post(%s == (a < 0))' % R, 'return a < 0;', post=lambda a, r: r == (1 if a < 0 else 0)) + +CASES = C +CONFIGS = ('z3', 'bv', 'int', 'cvc5') diff --git a/clang/utils/cppverify-differential/differential.py b/clang/utils/cppverify-differential/differential.py new file mode 100644 index 0000000000..bfa8f4cb0b --- /dev/null +++ b/clang/utils/cppverify-differential/differential.py @@ -0,0 +1,582 @@ +"""Differential execution: cpp-verify's verdicts against the C++ they are about. + +A case is a contracted C++ function. cpp-verify verifies it in each +configuration (a backend and an integer encoding). The same source, compiled by +clang with -fverify-contracts -fno-verify (contracts emit no code) and +-fsanitize=undefined in trap mode, runs on every input of a domain: every value +of small parameter types, otherwise boundary values and samples. The case's +precondition and postcondition, restated in Python over mathematical integers +as contract arithmetic is, judge each run. A problem is: + +- UNSOUND: a configuration verified the function, or found it bounded-safe + where the input stays within the bound, yet an admitted input runs into + undefined behavior or breaks the postcondition; +- BADCEX: a certified counterexample whose input the precondition rejects, or + on which the function runs without undefined behavior and meets its + postcondition; +- DISAGREE: two configurations reach different decisive verdicts. +""" +import itertools +import json +import os +import random +import subprocess +import zlib + +TYPES = { + 'bool': (1, False), + 'char': (8, True), + 'signed char': (8, True), 'int8_t': (8, True), + 'unsigned char': (8, False), 'uint8_t': (8, False), + 'short': (16, True), 'int16_t': (16, True), + 'unsigned short': (16, False), 'uint16_t': (16, False), 'char16_t': (16, False), + 'int': (32, True), 'int32_t': (32, True), 'wchar_t': (32, True), + 'unsigned': (32, False), 'unsigned int': (32, False), 'uint32_t': (32, False), + 'char32_t': (32, False), + 'long': (64, True), 'long long': (64, True), 'int64_t': (64, True), + 'unsigned long': (64, False), 'unsigned long long': (64, False), + 'uint64_t': (64, False), 'size_t': (64, False), + '__int128': (128, True), 'unsigned __int128': (128, False), +} + +CONFIGS = { + 'z3': [], + 'bv': ['--int-encoding=bitvector'], + 'int': ['--int-encoding=integer'], + 'cvc5': ['--backend=cvc5'], + 'bmc6': ['--backend=bmc', '--unroll=6'], + 'bmc10': ['--backend=bmc', '--unroll=10'], + 'bmc6bv': ['--backend=bmc', '--unroll=6', '--int-encoding=bitvector'], + 'bmc10bv': ['--backend=bmc', '--unroll=10', '--int-encoding=bitvector'], +} + +DECISIVE = ('verified', 'failed') + +# The failures a run can show: a broken postcondition, or undefined behavior +# that UBSan, a guard page, or the alarm stops. Others are claims about +# annotations (checks, invariants, measures, frames, callees' preconditions) +# or undefined behavior UBSan does not see (uninitialized reads). +OBSERVABLE = ('postcondition', 'overflow', 'division-by-zero', 'shift', 'bounds', + 'dereference', 'missing-return', 'unreachable') + + +def bound_of(config): + for flag in CONFIGS[config]: + if flag.startswith('--unroll='): + return int(flag.split('=')[1]) + return None + + +def trange(t): + bits, signed = TYPES[t] + if t == 'bool': + return 0, 1 + if signed: + return -(1 << (bits - 1)), (1 << (bits - 1)) - 1 + return 0, (1 << bits) - 1 + + +def boundary(t): + lo, hi = trange(t) + if t == 'bool': + return [0, 1] + bits, _ = TYPES[t] + vals = {lo, lo + 1, lo + 2, hi, hi - 1, hi - 2, 0, 1, 2, 3, -1, -2, -3, 5, 7, + 10, 100, -100} + for k in range(0, bits + 1): + for d in (-1, 0, 1): + vals.add((1 << k) + d) + vals.add(-(1 << k) + d) + for k in (8, 16, 32, 64): + if k < bits: + vals.add((1 << k) - 1) + return sorted(v for v in vals if lo <= v <= hi) + + +def wrap(v, t): + """The C++ conversion of a mathematical value to integer type t.""" + if t == 'bool': + return 1 if v != 0 else 0 + bits, signed = TYPES[t] + v &= (1 << bits) - 1 + if signed and v >= 1 << (bits - 1): + v -= 1 << bits + return v + + +def in_range(v, t): + lo, hi = trange(t) + return lo <= v <= hi + + +def tdiv(a, b): + """C++ division, truncating toward zero.""" + q = abs(a) // abs(b) + return q if (a >= 0) == (b >= 0) else -q + + +def tmod(a, b): + return a - b * tdiv(a, b) + + +def seeded(name): + return random.Random(zlib.crc32(name.encode())) + + +HARNESS_HEAD = r''' +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +static sigjmp_buf cv_env; +static void cv_handler(int s) { siglongjmp(cv_env, s); } +static __int128 cv_parse(const char *s) { + bool neg = false; if (*s == '-') { neg = true; ++s; } + unsigned __int128 v = 0; while (*s >= '0' && *s <= '9') { v = v * 10 + (*s - '0'); ++s; } + return (__int128)(neg ? (unsigned __int128)0 - v : v); +} +static void cv_print(__int128 v) { + char buf[64]; int n = 0; bool neg = v < 0; + unsigned __int128 u = neg ? -(unsigned __int128)v : (unsigned __int128)v; + if (u == 0) buf[n++] = '0'; + while (u) { buf[n++] = '0' + (int)(u % 10); u /= 10; } + if (neg) putchar('-'); + while (n) putchar(buf[--n]); +} +static char cv_altstack[1 << 16]; +static void cv_install() { + stack_t ss; ss.ss_sp = cv_altstack; ss.ss_size = sizeof cv_altstack; ss.ss_flags = 0; + sigaltstack(&ss, nullptr); + struct sigaction sa; memset(&sa, 0, sizeof sa); sa.sa_handler = cv_handler; + sigemptyset(&sa.sa_mask); sa.sa_flags = SA_NODEFER | SA_ONSTACK; + int sigs[] = {SIGILL, SIGFPE, SIGSEGV, SIGTRAP, SIGBUS, SIGALRM}; + for (int s : sigs) sigaction(s, &sa, nullptr); +} +static void cv_alarm(int ms) { + struct itimerval it; memset(&it, 0, sizeof it); + it.it_value.tv_sec = ms / 1000; it.it_value.tv_usec = (ms % 1000) * 1000; + setitimer(ITIMER_REAL, &it, nullptr); +} +struct cv_guard { char *base; size_t total; }; +static void *cv_galloc(size_t bytes, int layout, cv_guard *g) { + size_t pg = (size_t)sysconf(_SC_PAGESIZE); + size_t dp = (bytes + pg - 1) / pg; if (dp == 0) dp = 1; + g->total = (dp + 2) * pg; + g->base = (char *)mmap(nullptr, g->total, PROT_NONE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + char *data = g->base + pg; mprotect(data, dp * pg, PROT_READ | PROT_WRITE); + return layout == 0 ? (void *)(data + dp * pg - bytes) : (void *)data; +} +static void cv_gfree(cv_guard *g) { munmap(g->base, g->total); } +''' + + +class Tools: + def __init__(self, cpp_verify, clang, workdir, timeout_ms=30000): + self.cpp_verify = cpp_verify + self.clang = clang + self.workdir = workdir + self.timeout_ms = timeout_ms + + +class Case: + """A function over integer parameters [(type, name)].""" + + def __init__(self, name, params, ret, contract, body, pre=None, post=None, + prelude='', std='c++17', domain=None, vflags=None, nsamples=20000, + call=None, alarm_ms=1000, iterations=None): + self.name = name + self.params = params + self.ret = ret + self.contract = contract + self.body = body + self.pre = pre + self.post = post + self.prelude = prelude + self.std = std + self.domain = domain + self.vflags = vflags or [] + self.nsamples = nsamples + self.call = call + self.alarm_ms = alarm_ms + self.iterations = iterations + + def sig(self): + params = ', '.join('%s %s' % (t, n) for t, n in self.params) + return '%s %s(%s)' % (self.ret, self.name, params) + + def source(self): + return ('#include \n#include \n' + self.prelude + '\n' + + self.sig() + '\n' + self.contract + '\n{\n' + self.body + '\n}\n') + + def contract_lines(self): + first = ('#include \n#include \n' + self.prelude + '\n' + + self.sig() + '\n').count('\n') + 1 + return range(first, first + self.contract.count('\n') + 1) + + def harness(self): + args = ', '.join('(%s)cv_parse(tok[%d])' % (t, i) + for i, (t, _) in enumerate(self.params)) + call = self.call or '%s(%s)' % (self.name, args) + if self.ret == 'void': + run = '%s; printf("R 0\\n");' % call + else: + run = '__int128 r = (__int128)(%s); printf("R "); cv_print(r); printf("\\n");' % call + return HARNESS_HEAD + self.source() + r''' +int main() { + cv_install(); + static char line[4096]; + while (fgets(line, sizeof line, stdin)) { + const char *tok[16]; int nt = 0; char *p = strtok(line, " \n"); + while (p && nt < 16) { tok[nt++] = p; p = strtok(nullptr, " \n"); } + int s = sigsetjmp(cv_env, 1); + if (s == 0) { + cv_alarm(%d); + %s + cv_alarm(0); + } else { cv_alarm(0); printf("U %%d\n", s); } + } + return 0; +} +''' % (self.alarm_ms, run) + + def inputs(self): + if self.domain is not None: + dom = self.domain() if callable(self.domain) else self.domain + return [tuple(x) for x in dom] + types = [t for t, _ in self.params] + total = 1 + for t in types: + lo, hi = trange(t) + total *= hi - lo + 1 + if total <= 70000: + return list(itertools.product(*[range(trange(t)[0], trange(t)[1] + 1) + for t in types])) + rng = seeded(self.name) + bounds = [boundary(t) for t in types] + count = 1 + for b in bounds: + count *= len(b) + out = [] + if count <= 200000: + out.extend(itertools.product(*bounds)) + else: + out.extend(tuple(rng.choice(b) for b in bounds) for _ in range(100000)) + for _ in range(self.nsamples): + tup = [] + for t, b in zip(types, bounds): + lo, hi = trange(t) + r = rng.random() + if r < 0.3: + tup.append(rng.choice(b)) + elif r < 0.6: + tup.append(rng.randint(max(lo, -300), min(hi, 300))) + else: + tup.append(rng.randint(lo, hi)) + out.append(tuple(tup)) + return out + + def encode(self, inp): + return [' '.join(str(v) for v in inp)] + + def parse(self, line): + kind, value = line.split() + return ('UB', int(value), None) if kind == 'U' else ('R', int(value), None) + + def admitted(self, inp): + return self.pre is None or bool(self.pre(*inp)) + + def holds(self, inp, result, buffers): + return self.post is None or bool(self.post(*inp, result)) + + def model_input(self, entry): + """The parameters' entry values in a counterexample, 0 where undetermined.""" + if not entry.get('model'): + return None + values = {} + for m in entry.get('model') or []: + values.setdefault(m.get('name'), {})[m.get('ssa_name', '')] = m.get('value') + tup = [] + for _, n in self.params: + cand = values.get(n) + v = None + if cand: + v = cand.get(n + '_0', cand[sorted(cand)[0]]) + if v in (None, ''): + v = 0 + if v in ('true', 'false'): + v = int(v == 'true') + tup.append(int(v)) + return tuple(tup) + + +class PCase(Case): + """A function over scalars and memory. Each parameter is one of: + + ('s', type, name) a scalar + ('b', elem, name, length) a buffer of exactly `length` elements + ('o', type, name) a pointer to one object + ('r', type, name) a reference to one object + ('n', type, name) a null pointer to type + ('a', type, name, other) a pointer to the memory of parameter other + + An input is a dict {name: int | list}. Each input runs twice, with every + buffer ending at an inaccessible page and then starting after one. + """ + + def __init__(self, name, params, ret, contract, body, inputs, pre=None, post=None, + prelude='', std='c++17', vflags=None, alarm_ms=1000, iterations=None): + super().__init__(name, params, ret, contract, body, pre=pre, post=post, + prelude=prelude, std=std, vflags=vflags, alarm_ms=alarm_ms, + iterations=iterations) + self.domain = inputs + + def decl(self, p): + if p[0] == 's': + return '%s %s' % (p[1], p[2]) + if p[0] == 'r': + return '%s &%s' % (p[1], p[2]) + return '%s *%s' % (p[1], p[2]) + + def sig(self): + return '%s %s(%s)' % (self.ret, self.name, ', '.join(self.decl(p) for p in self.params)) + + def harness(self): + decls, args, frees, prints = [], [], [], [] + for i, p in enumerate(self.params): + k = p[0] + if k == 's': + decls.append(' %s v%d = (%s)cv_parse(tok[ti++]);' % (p[1], i, p[1])) + args.append('v%d' % i) + elif k in ('b', 'o', 'r'): + t = p[1].replace('const ', '') + decls.append(' long c%d = (long)cv_parse(tok[ti++]); cv_guard g%d; ' + '%s *v%d = (%s *)cv_galloc(c%d * sizeof(%s), layout, &g%d);' + % (i, i, t, i, t, i, t, i)) + decls.append(' for (long j = 0; j < c%d; ++j) v%d[j] = (%s)cv_parse(tok[ti++]);' + % (i, i, t)) + args.append('*v%d' % i if k == 'r' else 'v%d' % i) + frees.append('cv_gfree(&g%d);' % i) + prints.append(' printf(" |"); for (long j = 0; j < c%d; ++j) ' + '{ printf(" "); cv_print((__int128)v%d[j]); }' % (i, i)) + elif k == 'n': + args.append('(%s *)nullptr' % p[1]) + elif k == 'a': + args.append('v%d' % [q[2] for q in self.params].index(p[3])) + call = '%s(%s)' % (self.name, ', '.join(args)) + if self.ret == 'void': + run = '%s; cv_alarm(0); printf("R 0");' % call + else: + run = '__int128 r = (__int128)(%s); cv_alarm(0); printf("R "); cv_print(r);' % call + return (HARNESS_HEAD + self.source() + + 'int main() {\n cv_install();\n static char line[1 << 16];\n' + ' while (fgets(line, sizeof line, stdin)) {\n' + ' const char *tok[4096]; int nt = 0; char *p = strtok(line, " \\n");\n' + ' while (p && nt < 4096) { tok[nt++] = p; p = strtok(nullptr, " \\n"); }\n' + ' int ti = 0; int layout = (int)cv_parse(tok[ti++]);\n' + + '\n'.join(decls) + '\n' + ' int s = sigsetjmp(cv_env, 1);\n if (s == 0) {\n' + ' cv_alarm(%d);\n %s\n' % (self.alarm_ms, run) + + '\n'.join(prints) + '\n' + ' printf("\\n");\n } else { cv_alarm(0); printf("U %d\\n", s); }\n' + ' ' + ' '.join(frees) + '\n }\n return 0;\n}\n') + + def inputs(self): + return list(self.domain() if callable(self.domain) else self.domain) + + def encode(self, inp): + lines = [] + for layout in (0, 1): + toks = [str(layout)] + for p in self.params: + if p[0] == 's': + toks.append(str(inp[p[2]])) + elif p[0] in ('b', 'o', 'r'): + vals = inp[p[2]] + if not isinstance(vals, list): + vals = [vals] + toks.append(str(len(vals))) + toks.extend(str(v) for v in vals) + lines.append(' '.join(toks)) + return lines + + def parse(self, line): + if line.startswith('U '): + return ('UB', int(line.split()[1]), None) + parts = line[2:].split(' |') + return ('R', int(parts[0]), [[int(x) for x in q.split()] for q in parts[1:]]) + + def admitted(self, inp): + return self.pre is None or bool(self.pre(inp)) + + def holds(self, inp, result, buffers): + return self.post is None or bool(self.post(inp, buffers, result)) + + def model_input(self, entry): + return None + + +def run_verifier(tools, path, std, flags): + cmd = ([tools.cpp_verify, '--diagnostics-format=json', '--timeout=%d' % tools.timeout_ms] + + flags + [path, '--', '-std=' + std]) + try: + p = subprocess.run(cmd, capture_output=True, text=True, + timeout=10 * tools.timeout_ms / 1000 + 60) + except subprocess.TimeoutExpired: + return None, cmd + records = {} + for line in p.stdout.splitlines(): + line = line.strip() + if not line.startswith('{'): + continue + try: + record = json.loads(line) + except ValueError: + continue + records.setdefault(record.get('function'), []).append(record) + return records, cmd + + +def verdict_of(records): + for record in records: + if record.get('status') in ('verified', 'failed', 'unresolved', 'bounded-safe', 'trusted'): + return record.get('status'), record + if records: + return records[0].get('status'), records[0] + return 'missing', None + + +def label(status, record): + if status == 'failed' and record: + return 'failed:' + (record.get('obligation') or {}).get('kind', '?') + if status == 'unresolved' and record: + return 'unresolved:' + str(record.get('reason')) + return status + + +def disagreement(verdicts): + if len({v[0] for v in verdicts.values() if v[0] in DECISIVE}) > 1: + return ['DISAGREE: %s' % {c: v[0] for c, v in verdicts.items()}] + return [] + + +def abstracted(record): + """Whether a counterexample passes a call or an arbitrary loop iteration, + where it is relative to a callee's contract or a loop's invariant.""" + return any(e.get('kind') == 'call' or + (e.get('kind') == 'loop' and e.get('message') == 'inductive iteration') + for e in record.get('trace') or []) + + +def run_case(tools, case, configs): + base = os.path.join(tools.workdir, case.name) + with open(base + '.cpp', 'w') as f: + f.write(case.source()) + verdicts = {} + for config in configs: + records, cmd = run_verifier(tools, base + '.cpp', case.std, CONFIGS[config] + case.vflags) + if records is None: + verdicts[config] = ('timeout', None) + continue + verdicts[config] = verdict_of(records.get(case.name, [])) + + inputs = [inp for inp in case.inputs() if case.admitted(inp)] + if not inputs: + line = '%-40s %s (no inputs to run)' % ( + case.name, ' '.join('%s=%s' % (c, label(*v)) for c, v in verdicts.items())) + return {'case': case.name, 'verdicts': {c: label(*v) for c, v in verdicts.items()}, + 'admitted': 0, 'violations': 0, 'counterexamples': {}, + 'problems': disagreement(verdicts), 'line': line} + + with open(base + '.harness.cpp', 'w') as f: + f.write(case.harness()) + p = subprocess.run([tools.clang, '--driver-mode=g++', '-std=' + case.std, '-O0', '-w', + '-fverify-contracts', '-fno-verify', '-fsanitize=undefined', + '-fno-sanitize=vptr,function', '-fsanitize-trap=undefined', + base + '.harness.cpp', '-o', base + '.harness'], + capture_output=True, text=True) + if p.returncode != 0: + raise RuntimeError('the harness does not compile:\n' + p.stderr[:3000]) + + counterexamples = {} + for config, (status, record) in verdicts.items(): + if status == 'failed' and record is not None: + counterexamples[config] = case.model_input(record) + extra = [c for c in counterexamples.values() if c is not None and case.admitted(c)] + encoded = [case.encode(inp) for inp in inputs + extra] + lines = [line for runs in encoded for line in runs] + q = subprocess.run([base + '.harness'], input='\n'.join(lines) + '\n', + capture_output=True, text=True, timeout=3600) + results = q.stdout.splitlines() + if len(results) != len(lines): + raise RuntimeError('the harness ran %d of %d inputs: %s' + % (len(results), len(lines), q.stderr[:2000])) + outs, at = [], 0 + for runs in encoded: + outs.append([case.parse(line) for line in results[at:at + len(runs)]]) + at += len(runs) + + admitted, violations = len(inputs), [] + for inp, runs in zip(inputs, outs): + for kind, result, buffers in runs: + if kind == 'UB': + violations.append((inp, 'UB', result)) + break + if not case.holds(inp, result, buffers): + violations.append((inp, 'POST', result)) + break + + problems = [] + checked = {} + for config, (status, record) in verdicts.items(): + bound = bound_of(config) + if status == 'verified' or (status == 'bounded-safe' and case.iterations is not None): + within = violations + if status == 'bounded-safe': + within = [v for v in violations if case.iterations(v[0]) < bound] + if within: + problems.append('UNSOUND[%s]: %s, yet %d admitted inputs misbehave, such as %s' + % (config, status, len(within), within[:3])) + if status != 'failed' or record is None: + continue + obligation = record.get('obligation') or {} + kind = obligation.get('kind', '') + if kind not in OBSERVABLE: + checked[config] = 'not observable by running (%s)' % kind + continue + if (kind != 'postcondition' and + (obligation.get('source') or {}).get('line') in case.contract_lines()): + checked[config] = 'the contract is undefined there (%s)' % kind + continue + cex = counterexamples.get(config) + if cex is None: + checked[config] = 'no input values' + continue + if not case.admitted(cex): + problems.append('BADCEX[%s]: %s, which the precondition rejects' % (config, cex)) + continue + k, r, _ = outs[len(inputs) + extra.index(cex)][0] + if k == 'UB': + checked[config] = 'confirmed: undefined behavior at %s' % (cex,) + elif not case.holds(cex, r, None): + checked[config] = 'confirmed: %s returns %d' % (cex, r) + elif abstracted(record): + checked[config] = ('not reproduced at %s, relative to the contract of a callee ' + 'or a loop invariant' % (cex,)) + else: + problems.append('BADCEX[%s]: %s returns %d and meets the contract (%s)' + % (config, cex, r, (record.get('message') or '')[:300])) + problems += disagreement(verdicts) + line = '%-40s %s admitted=%d violations=%d' % ( + case.name, ' '.join('%s=%s' % (c, label(*v)) for c, v in verdicts.items()), + admitted, len(violations)) + if checked: + line += ' counterexamples: ' + '; '.join('%s %s' % c for c in checked.items()) + return {'case': case.name, 'verdicts': {c: label(*v) for c, v in verdicts.items()}, + 'admitted': admitted, 'violations': len(violations), 'counterexamples': checked, + 'problems': problems, 'line': line} diff --git a/clang/utils/cppverify-differential/run.py b/clang/utils/cppverify-differential/run.py new file mode 100644 index 0000000000..d6e20cb034 --- /dev/null +++ b/clang/utils/cppverify-differential/run.py @@ -0,0 +1,93 @@ +#!/usr/bin/env python3 +"""Runs the differential cases and exits with 1 when any has a problem. + + run.py --cpp-verify BUILD/bin/cpp-verify [--clang BUILD/bin/clang] + [--suite NAME]... [--case TEXT]... [--configs z3,cvc5,...] + [--jobs N] [--timeout MS] [--work DIR] [--report FILE] + +A suite is a module of cases/ with CASES and the CONFIGS it runs in. +""" +import argparse +import importlib +import json +import os +import shutil +import sys +import tempfile +from concurrent.futures import ThreadPoolExecutor + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.dont_write_bytecode = True +sys.path.insert(0, HERE) +import differential # noqa: E402 + +SUITES = ['integers', 'shifts_division', 'contracts', 'loops', 'calls', 'pointers', + 'pointers_bmc', 'expressions', 'loops_bmc', 'bit_int', 'records', 'selftest'] +DEFAULT = [s for s in SUITES if s != 'selftest'] + + +def main(): + parser = argparse.ArgumentParser(description=__doc__, + formatter_class=argparse.RawDescriptionHelpFormatter) + parser.add_argument('--cpp-verify', required=True) + parser.add_argument('--clang') + parser.add_argument('--suite', action='append', choices=SUITES) + parser.add_argument('--case', action='append') + parser.add_argument('--configs') + parser.add_argument('--jobs', type=int, default=os.cpu_count() or 1) + parser.add_argument('--timeout', type=int, default=30000) + parser.add_argument('--work') + parser.add_argument('--report') + args = parser.parse_args() + + clang = args.clang or os.path.join(os.path.dirname(args.cpp_verify), 'clang') + work = args.work or tempfile.mkdtemp(prefix='cppverify-differential-') + os.makedirs(work, exist_ok=True) + tools = differential.Tools(os.path.abspath(args.cpp_verify), os.path.abspath(clang), + os.path.abspath(work), args.timeout) + + jobs = [] + for name in args.suite or DEFAULT: + suite = importlib.import_module('cases.' + name) + configs = args.configs.split(',') if args.configs else list(suite.CONFIGS) + if 'cvc5' in configs and not shutil.which('cvc5'): + print('note: cvc5 is not on PATH; %s runs without it' % name) + configs.remove('cvc5') + for case in suite.CASES: + if not args.case or any(text in case.name for text in args.case): + jobs.append((name, case, configs)) + + def run(job): + name, case, configs = job + suite_tools = differential.Tools(tools.cpp_verify, tools.clang, + os.path.join(tools.workdir, name), tools.timeout_ms) + os.makedirs(suite_tools.workdir, exist_ok=True) + try: + result = differential.run_case(suite_tools, case, configs) + except Exception as e: # A case that cannot run is a problem too. + result = {'case': case.name, 'problems': ['ERROR: %s' % e], + 'line': '%-40s ERROR' % case.name} + result['suite'] = name + return result + + results = [] + with ThreadPoolExecutor(max(1, args.jobs)) as pool: + for result in pool.map(run, jobs): + results.append(result) + print(result['line']) + for problem in result['problems']: + print(' problem: ' + problem[:2000]) + sys.stdout.flush() + + problems = [(r['case'], p) for r in results for p in r['problems']] + print('\n%d cases, %d problems' % (len(results), len(problems))) + for case, problem in problems: + print('%s: %s' % (case, problem[:2000])) + if args.report: + with open(args.report, 'w') as f: + json.dump(results, f, indent=1, default=str) + return 1 if problems else 0 + + +if __name__ == '__main__': + sys.exit(main()) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 11925a64e6..4913f0cd7b 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2977,6 +2977,24 @@ stops before VCR conversion. - Backend fidelity gate: `clang/test/Verify/suite/backend_fidelity_gate.test` requires cvc5 and pinned Lean 4.35.0 and runs the permanent differential matrix under every machine-integer encoding. +- Differential execution: `clang/utils/cppverify-differential/run.py` + verifies 484 contracted functions (`cases/`) in each configuration their + suite lists (Z3 in each machine-integer encoding, cvc5, BMC at two bounds), + compiles the same source with `-fverify-contracts -fno-verify` and + `-fsanitize=undefined -fsanitize-trap=undefined`, and runs it on every input + of small parameter types, otherwise on boundary values and samples seeded + by the function's name, each buffer against an inaccessible page on one + side and then the other. Each case restates its pre- and postcondition in + Python over mathematical integers, which judge each run. A problem is a + `Verified` function (or one `BoundedSafe` within its bound) that + misbehaves on an admitted input, a counterexample whose input the + precondition rejects or on which the function behaves (pointer cases' + counterexamples are not replayed, and one against an invariant, measure, + or frame is relative to that abstraction), or two configurations that + decide differently. `.github/workflows/cppverify-differential.yml` runs + every case nightly; `differential.test` runs the tool's own cases, two of + which state their contract wrongly in Python so that the tool must report + them. - Instrumented coverage: `scripts/coverage-verify.sh` (region target on `clang/lib/Verify`). Every new semantic feature needs layered oracles rather than a solver result diff --git a/docs/REPO_LAYOUT.md b/docs/REPO_LAYOUT.md index 43e941262b..cc41fc7382 100644 --- a/docs/REPO_LAYOUT.md +++ b/docs/REPO_LAYOUT.md @@ -9,6 +9,7 @@ This repository **is** the CppVerify codebase: an LLVM monorepo fork extended at | `clang/tools/cpp-verify/` | Standalone verifier | | `clang/test/Verify/` | Frontend lit tests; `suite/` holds the end-to-end programs, the case studies and backend tests included | | `clang/unittests/Verify/` | Encoding oracle and parity unit tests (`VerifyTests`) | +| `clang/utils/cppverify-differential/` | Differential execution of verdicts against UBSan-instrumented runs, nightly in CI | | `llvm/` | CMake entry for LLVM + Clang | | `website/` | Published user docs (Sphinx + Doxygen) | | `docs/` | Design notes | diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 04fb031093..e1ae4a965d 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -104,6 +104,71 @@ artifacts. cvc5 may conservatively return ``unknown`` for designated valid quantified or inductive goals; every false matrix goal must remain decisive, and any solver disagreement fails the gate. +Differential execution +---------------------- + +A verdict is also checked against the program it is about. +``clang/utils/cppverify-differential`` holds 484 contracted functions over +integers, ``_BitInt``, pointers and buffers, and records, each with its +precondition and postcondition restated in Python. For each one it: + +- verifies the function with Z3 in each integer encoding and with cvc5, or + with BMC at two bounds; +- compiles the same source with ``-fverify-contracts -fno-verify`` (contracts + emit no code) and ``-fsanitize=undefined -fsanitize-trap=undefined``, and + runs it on every input of small parameter types, otherwise on boundary + values and samples seeded by the function's name, each buffer ending at an + inaccessible page and then starting after one; +- judges every run the precondition admits by the Python restatement, over + mathematical integers as contract arithmetic is. + +It reports a problem when a function is ``Verified`` (or ``BoundedSafe`` for +an input within the bound) yet an admitted input has undefined behavior or +breaks the postcondition, when a counterexample's input is not admitted or +runs without either, and when two configurations decide differently. CI runs +every case each night; ``clang/test/Verify/differential.test`` runs the tool's +own cases on every change. From the repository root: + +.. code-block:: bash + + ninja -C build clang cpp-verify + python3 clang/utils/cppverify-differential/run.py \ + --cpp-verify build/bin/cpp-verify --suite integers --suite calls + +Each line gives a function's verdict in each configuration, the inputs its +precondition admits, how many of them misbehave, and what each counterexample +showed when run: + +.. code-block:: text + + u16mul_guard z3=verified bv=verified int=verified cvc5=verified admitted=17225 violations=0 + long_plus_1u z3=failed:overflow ... admitted=20380 violations=16 counterexamples: z3 confirmed: undefined behavior at (9223372036854775807,); ... + +A failure is evidence relative to the contracts it uses, so not every +counterexample reproduces when the program runs. Here ``weak`` promises less +than it does: + +.. cppverify-example: fails m_weak_post + +.. code-block:: cpp + + int weak(int x) + cppverify::post(cppverify::result >= x) + { return x < 100 ? 100 : x; } + + int m_weak_post(int x) + cppverify::post(cppverify::result >= 100) + { return weak(x); } + +``m_weak_post`` fails at ``x = 0`` relative to the contract of ``weak``, while +running it returns 100. The tool runs every counterexample it can read. One +that passes a call or an arbitrary loop iteration and does not reproduce is +reported as relative to that abstraction, and so is a failure that a run +cannot show: a check, an invariant, a measure, a frame, a callee's +precondition, an uninitialized read, or a contract that is undefined at the +input (only its body runs). A counterexample of a pointer function, or one +cvc5 found, carries no values to run. + Parallel solving and persistent proofs -------------------------------------- diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 96ef7e7129..75e4ff4816 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -704,11 +704,15 @@ Assurance and testing gaps -------------------------- Every current checkpoint uses positive programs, nearby false programs, and -layered lowering checks. Broader trust additionally requires: +layered lowering checks. Every night, 484 contracted functions over integers, +pointers, and records are also verified by each backend and run natively +under UBSan on enumerated or sampled inputs, and a verdict that execution +contradicts fails CI (:doc:`../book/part-ii/ch17-backends-modular-calls`). +Broader trust additionally requires: - grammar-guided fuzzing of supported and neighboring unsupported C++; - metamorphic and AST/VCR/SMT translation-validation tests; -- bounded differential execution against compiled Clang programs; +- differential execution of classes, templates, and dynamic storage; - X86-64/AArch64 target-layout and language-mode matrices; - solver-time, memory, VC-size, and random-seed stability benchmarks; - stale-cache, timeout, quantifier, aliasing, and model-adversarial tests; diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 33aec573e2..4778d1087b 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -683,6 +683,18 @@ refuses a ``lake`` outside elan that reports another Lean **clang-format.** A range footprint is written ``p[lo : n]``, not ``p [lo:n]`` (:doc:`language/tooling`). +Testing +~~~~~~~ + +**Verdicts are checked against execution every night.** 484 contracted +functions over integers, pointers, and records are verified by Z3 in each +integer encoding, by cvc5, and by BMC, then compiled with +``-fsanitize=undefined`` and run on every input of small parameter types, or +on boundary values and samples. CI fails when a ``Verified`` function +misbehaves on an input its precondition admits, when a counterexample does not +reproduce, or when two backends decide differently +(:doc:`book/part-ii/ch17-backends-modular-calls`). + Data formats ~~~~~~~~~~~~