verify: Turn off AssertMacros.h's names without underscores on Apple targets

clang/lib/Frontend/InitPreprocessor.cpp

@@ -1659,10 +1659,18 @@ void clang::InitializePreprocessor(Preprocessor &PP,
                           InitOpts.ImplicitPCHInclude);
 
   // CppVerify: the namespace cppverify needs no #include.
-  if (PP.getLangOpts().VerifyContracts && PP.getLangOpts().CPlusPlus)
+  if (PP.getLangOpts().VerifyContracts && PP.getLangOpts().CPlusPlus) {
+    // Apple's <AssertMacros.h> defines check(assertion) unless this is 0,
+    // which would expand cppverify::check.
+    if (PP.getTargetInfo().getTriple().isOSDarwin())
+      Builder.append(
+          "#ifndef __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES\n"
+          "#define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 0\n"
+          "#endif");
     Builder.append("#if __has_include(<cppverify.h>)\n"
                    "#include <cppverify.h>\n"
                    "#endif");
+  }
 
   // Process -include directives.
   for (unsigned i = 0, e = InitOpts.Includes.size(); i != e; ++i) {

clang/test/Verify/Inputs/apple/AssertMacros.h

@@ -0,0 +1,15 @@
+// The part of Apple's <AssertMacros.h> that collides with cppverify::check:
+// unless __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES is 0, it defines
+// check(assertion) as __Check(assertion), which production code defines empty.
+
+#ifndef __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES
+#define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 1
+#endif
+
+#define __Check(assertion)
+
+#if __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES
+#ifndef check
+#define check(assertion) __Check(assertion)
+#endif
+#endif

clang/test/Verify/assert_macros_darwin.cpp

@@ -0,0 +1,28 @@
+// RUN: %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -fverify-contracts -fsyntax-only -verify -isystem %S/Inputs/apple %s
+// RUN: %clang_cc1 -triple arm64-apple-ios17.0 -std=c++17 -fverify-contracts -fsyntax-only -verify -isystem %S/Inputs/apple %s
+// RUN: not %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -fverify-contracts -fsyntax-only -D__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES=1 -isystem %S/Inputs/apple %s 2>&1 | FileCheck %s --check-prefix=OLD
+// RUN: %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -fverify-contracts -E -dM -isystem %S/Inputs/apple %s | FileCheck %s --check-prefix=OFF
+// RUN: %clang_cc1 -triple arm64-apple-macosx14.0 -std=c++17 -E -dM -isystem %S/Inputs/apple %s | FileCheck %s --check-prefix=ON
+// RUN: %clang_cc1 -triple x86_64-unknown-linux-gnu -std=c++17 -fverify-contracts -E -dM -isystem %S/Inputs/apple %s | FileCheck %s --check-prefix=ON
+//
+// Apple's <AssertMacros.h> defines check(assertion) unless
+// __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES is 0, which would expand
+// cppverify::check. -fverify-contracts sets it to 0 on Apple targets unless
+// the command line defines it.
+
+#include <AssertMacros.h>
+
+namespace cv = cppverify;
+
+int positive(int x)
+  cv::pre(x > 0)
+{
+  cv::check(x > 0);
+  cppverify::check(x != 0);
+  return x;
+}
+
+// expected-no-diagnostics
+// OLD: error: expected unqualified-id
+// OFF: #define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 0
+// ON: #define __ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES 1

docs/DESIGN.md

@@ -1530,6 +1530,11 @@ deleted functions (`void pre(bool condition) = delete;`) and the others as
 unavailable enumerators (`result`, `inductive`, `spec`, ...), so any use the
 parser does not take as a construct is an error. `InitPreprocessor` includes
 the header in every C++ translation unit compiled with `-fverify-contracts`.
+On Darwin targets it first defines
+`__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES` to 0 unless the command
+line defines it: otherwise Apple's `<AssertMacros.h>` defines
+`check(assertion)`, and a function-like macro expands inside
+`cppverify::check(...)` before the parser can recognize the construct.
 
 Misuse is diagnosed where the parser would otherwise fail: a construct in the
 wrong position (`'cppverify::pre' follows a function's parameter list`), an

website/source/language/syntax.rst

@@ -191,3 +191,62 @@ Full table:
    * - ``cppverify::valid(p, n)``
      - In ``cppverify::pre``
      - ``p`` points to ``n`` objects
+
+Macros named like a construct
+-----------------------------
+
+The preprocessor runs before the parser sees a construct, so a function-like
+macro named like a construct expands inside the qualified name. A header that
+defines ``check(condition)`` breaks every ``cppverify::check`` after it:
+
+.. cppverify-example: rejects
+
+.. code-block:: cpp
+
+   #define check(condition) ((void)0)
+
+   int positive(int x)
+     cv::pre(x > 0)
+   {
+     cv::check(x > 0);
+     return x;
+   }
+
+.. code-block:: text
+
+   macros.cpp:6:7: error: expected unqualified-id
+
+``#undef check`` after the header's ``#include`` restores the construct:
+
+.. code-block:: cpp
+
+   #define check(condition) ((void)0)
+   #undef check
+
+   int positive(int x)
+     cv::pre(x > 0)
+   {
+     cv::check(x > 0);
+     return x;
+   }
+
+.. code-block:: text
+
+   Verified: positive [backend=z3]
+
+An object-like macro has the same effect on a construct written without
+parentheses, such as ``cv::result``.
+
+On Apple platforms (macOS, iOS, and the others), ``<AssertMacros.h>``, which
+some of Apple's framework headers include, defines ``check(assertion)`` unless
+``__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES`` is ``0``. With
+``-fverify-contracts`` on an Apple target, the compiler therefore defines it
+to ``0`` before any header, unless the command line defines it, and
+``cppverify::check`` works next to that header. The header then defines only
+its ``__Check``, ``__Require``, and ``__Verify`` macros, the names Apple
+recommends. A file that uses the old names (``check``, ``require``,
+``verify``, and their variants) can switch to the ``__`` names, or keep the
+old ones with ``-D__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES=1`` on
+the command line; ``cppverify::check`` then works only after an ``#undef
+check``. Defining it to ``1`` with ``#define`` in the source also works, with
+a ``-Wmacro-redefined`` warning.

website/source/release-notes.rst

@@ -114,6 +114,13 @@ parameters did not compile. Its contracts now compile and instantiate, and
 are ignored with a ``-Wcontract-unsupported`` warning; a template without
 contracts no longer stops the file (:doc:`language/functions-loops`).
 
+**Apple's assertion macros.** On Apple targets ``<AssertMacros.h>`` defines a
+``check(assertion)`` macro, which turned every ``cppverify::check(...)`` after
+it into ``error: expected unqualified-id``. ``-fverify-contracts`` now defines
+``__ASSERT_MACROS_DEFINE_VERSIONS_WITHOUT_UNDERSCORES`` to ``0`` on Apple
+targets unless the command line defines it, so the header defines only its
+``__Check``, ``__Require``, and ``__Verify`` names (:doc:`language/syntax`).
+
 Running cpp-verify
 ~~~~~~~~~~~~~~~~~~