Merge pull request #11 from SwayamInSync/feat/type-invariant-safe-fib-mvp

feat(verify): Adding lazy `type_invariant` support in cpp-verify

Author: SwayamInSync

README.md

@@ -56,7 +56,7 @@ ninja -C build clang cpp-verify
 
 ```cpp
 int abs(int x)
-  pre(true)
+  pre(x >= -2147483647)   // every int except INT_MIN, whose negation overflows
   post(result >= 0)
 {
   return x < 0 ? -x : x;
@@ -70,6 +70,23 @@ int abs(int x)
 
 Use `-fverify-contracts` on `clang++` so `pre` / `post` are keywords. `cpp-verify` enables that flag automatically.
 
+### Supported compiler
+
+Contract syntax (`pre` / `post` / `invariant` / `spec` / …) and the
+`-fverify-contracts` flag exist **only in this repository's Clang**. To compile
+or verify code that uses contracts, you must use the shipped tools:
+
+- `./build/bin/cpp-verify file.cpp` — verify.
+- `./build/bin/clang++ -fverify-contracts … file.cpp` — compile (also runs verification).
+
+Stock GCC or upstream Clang will reject `-fverify-contracts` (unknown flag) **and**
+the contract keywords (`expected function body after function declarator` at
+`pre(...)`). There is no contract support outside the shipped Clang.
+
+Note this is a separate matter from *building* cpp-verify itself from source:
+that bootstrap step compiles ordinary C++ and works with **any** standard host
+compiler — GCC or Clang (`setup.sh` uses `${CXX:-c++}`).
+
 ## Verification backends
 
 | Backend | CLI | Role |
@@ -84,7 +101,9 @@ Use `-fverify-contracts` on `clang++` so `pre` / `post` are keywords. `cpp-verif
 |---------|------|
 | `cpp-verify file.cpp` | Verify only (Z3) |
 | `clang++ -fverify-contracts -c file.cpp` | Verify (parallel) + compile |
-| `clang++ -fverify-contracts -fno-verify -c file.cpp` | Contracts on; skip SMT |
+| `clang++ -fno-verify -c file.cpp` | Light check — contracts on (implied), skip the solver |
+
+`-fverify-contracts` and `-fno-verify` are two axes: the first enables the contract language (and verifies by default); `-fno-verify` skips the solver and implies `-fverify-contracts`, so a lone `-fno-verify` is a fast syntax/semantics check. There is no `-fverify`.
 
 ```bash
 ./build/bin/cpp-verify --dump-ir=1,2,3,4 file.cpp   # VCR, passive, VC, Z3

clang/cmake/modules/CppVerifyZ3.cmake

@@ -26,31 +26,70 @@ set(CPPVERIFY_Z3_SOURCE_DIR "" CACHE PATH "Path to a Z3 source tree (overrides t
 get_filename_component(CPPVERIFY_REPO_ROOT
   "${CMAKE_CURRENT_LIST_DIR}/../../.." ABSOLUTE)
 
-function(cppverify_z3_apply_build_options)
-  set(Z3_BUILD_LIBZ3_SHARED OFF CACHE BOOL "" FORCE)
-  set(Z3_BUILD_EXECUTABLE OFF CACHE BOOL "" FORCE)
-  set(Z3_BUILD_TEST_EXECUTABLES OFF CACHE BOOL "" FORCE)
-endfunction()
-
-function(cppverify_z3_register_alias)
-  if(TARGET libz3)
-    if(NOT TARGET cppverify_z3)
-      add_library(cppverify_z3 ALIAS libz3)
-    endif()
-  elseif(TARGET z3)
-    if(NOT TARGET cppverify_z3)
-      add_library(cppverify_z3 ALIAS z3)
-    endif()
+# Build vendored Z3 as an isolated ExternalProject rather than add_subdirectory.
+#
+# Why ExternalProject and not add_subdirectory: Z3's CMake declares a library
+# component target literally named `opt` (z3_add_component(opt ...)). LLVM's
+# monorepo also declares an `opt` executable (llvm/tools/opt). Pulling Z3 into
+# the same CMake project via add_subdirectory/FetchContent makes both `opt`
+# targets live in one namespace and configure fails with CMP0002 (duplicate
+# target). ExternalProject runs Z3's CMake in a separate build, so its targets
+# never collide with LLVM's. We then consume the installed static lib through an
+# IMPORTED target.
+#
+# Sources for the build (either an on-disk tree or a git clone) are handled by
+# the SOURCE_DIR / GIT_REPOSITORY arguments threaded in by the callers.
+function(cppverify_z3_build_external)
+  cmake_parse_arguments(Z3EP "" "SOURCE_DIR;GIT_REPOSITORY;GIT_TAG" "" ${ARGN})
+  include(ExternalProject)
+
+  set(_prefix  "${CMAKE_BINARY_DIR}/cppverify-z3")
+  set(_install "${_prefix}/install")
+  set(_incdir  "${_install}/include")
+  set(_libpath "${_install}/lib/${CMAKE_STATIC_LIBRARY_PREFIX}z3${CMAKE_STATIC_LIBRARY_SUFFIX}")
+
+  if(Z3EP_SOURCE_DIR)
+    set(_src_args SOURCE_DIR "${Z3EP_SOURCE_DIR}")
+    message(STATUS "CppVerify: building vendored Z3 (ExternalProject) from ${Z3EP_SOURCE_DIR}")
   else()
-    message(FATAL_ERROR "Z3 build did not produce libz3 or z3 CMake target")
+    set(_src_args
+      GIT_REPOSITORY "${Z3EP_GIT_REPOSITORY}"
+      GIT_TAG        "${Z3EP_GIT_TAG}"
+      GIT_SHALLOW    TRUE)
+    message(STATUS "CppVerify: building vendored Z3 (ExternalProject) ${Z3EP_GIT_TAG} "
+      "(first build needs network)")
   endif()
-endfunction()
 
-function(cppverify_z3_from_subdirectory z3_src binary_dir)
-  cppverify_z3_apply_build_options()
-  message(STATUS "CppVerify: building vendored Z3 from ${z3_src}")
-  add_subdirectory("${z3_src}" "${binary_dir}" EXCLUDE_FROM_ALL)
-  cppverify_z3_register_alias()
+  ExternalProject_Add(cppverify_z3_ep
+    ${_src_args}
+    PREFIX "${_prefix}"
+    CMAKE_CACHE_ARGS
+      -DCMAKE_BUILD_TYPE:STRING=Release
+      -DCMAKE_INSTALL_PREFIX:PATH=${_install}
+      -DCMAKE_POSITION_INDEPENDENT_CODE:BOOL=ON
+      -DZ3_BUILD_LIBZ3_SHARED:BOOL=OFF
+      -DZ3_BUILD_EXECUTABLE:BOOL=OFF
+      -DZ3_BUILD_TEST_EXECUTABLES:BOOL=OFF
+      -DZ3_BUILD_DOCUMENTATION:BOOL=OFF
+      -DZ3_ENABLE_EXAMPLE_TARGETS:BOOL=OFF
+    BUILD_BYPRODUCTS "${_libpath}"
+    USES_TERMINAL_DOWNLOAD TRUE
+    USES_TERMINAL_BUILD TRUE)
+
+  # INTERFACE_INCLUDE_DIRECTORIES must exist at configure time.
+  file(MAKE_DIRECTORY "${_incdir}")
+
+  find_package(Threads REQUIRED)
+  add_library(cppverify_z3 STATIC IMPORTED GLOBAL)
+  set_target_properties(cppverify_z3 PROPERTIES
+    IMPORTED_LOCATION "${_libpath}"
+    INTERFACE_INCLUDE_DIRECTORIES "${_incdir}"
+    INTERFACE_LINK_LIBRARIES "Threads::Threads;${CMAKE_DL_LIBS}")
+
+  # Ensure the ExternalProject is built before anything links the imported lib.
+  # BUILD_BYPRODUCTS handles Ninja ordering; this property lets consuming targets
+  # add an explicit dependency for the Makefiles generator too.
+  set_property(GLOBAL PROPERTY CPPVERIFY_Z3_EP_TARGET cppverify_z3_ep)
 endfunction()
 
 function(cppverify_z3_try_system out_var)
@@ -101,22 +140,14 @@ function(cppverify_z3_try_local out_var)
     set(${out_var} "" PARENT_SCOPE)
     return()
   endif()
-  cppverify_z3_from_subdirectory("${_src}" "${CMAKE_BINARY_DIR}/cppverify-z3-build")
+  cppverify_z3_build_external(SOURCE_DIR "${_src}")
   set(${out_var} cppverify_z3 PARENT_SCOPE)
 endfunction()
 
 function(cppverify_z3_try_fetch out_var)
-  include(FetchContent)
-  cppverify_z3_apply_build_options()
-  message(STATUS "CppVerify: fetching Z3 ${CPPVERIFY_Z3_GIT_TAG} (first build needs network)")
-  FetchContent_Declare(
-    cppverify_z3_src
+  cppverify_z3_build_external(
     GIT_REPOSITORY https://github.com/Z3Prover/z3.git
-    GIT_TAG        ${CPPVERIFY_Z3_GIT_TAG}
-    GIT_SHALLOW    TRUE
-  )
-  FetchContent_MakeAvailable(cppverify_z3_src)
-  cppverify_z3_register_alias()
+    GIT_TAG        ${CPPVERIFY_Z3_GIT_TAG})
   set(${out_var} cppverify_z3 PARENT_SCOPE)
 endfunction()
 

clang/include/clang/AST/ASTContext.h

@@ -112,6 +112,11 @@ struct LoopContractInfo {
   SmallVector<Expr *, 2> Invariants;
   Expr *Decreases = nullptr;
 };
+
+/// Type invariant clauses on a RecordDecl (CppVerify).
+struct TypeContractInfo {
+  SmallVector<Expr *, 2> Invariants;
+};
 class CharUnits;
 class ConceptDecl;
 class CXXABI;
@@ -376,6 +381,9 @@ class ASTContext : public RefCountedBase<ASTContext> {
   /// CppVerify: contract info for loops (invariant/decreases).
   llvm::DenseMap<const Stmt *, LoopContractInfo *> LoopContracts;
 
+  /// CppVerify: type_invariant clauses on record/class types.
+  llvm::DenseMap<const RecordDecl *, TypeContractInfo *> TypeContracts;
+
   /// Mapping from GUIDs to the corresponding MSGuidDecl.
   mutable llvm::FoldingSet<MSGuidDecl> MSGuidDecls;
 
@@ -3457,6 +3465,11 @@ class ASTContext : public RefCountedBase<ASTContext> {
   /// CppVerify: get contract info for a loop, or nullptr if none.
   const LoopContractInfo *getLoopContract(const Stmt *S) const;
 
+  /// CppVerify: get or create type_invariant info for a record type.
+  TypeContractInfo &getOrCreateTypeContract(const RecordDecl *RD);
+  /// CppVerify: get type_invariant info, or nullptr if none.
+  const TypeContractInfo *getTypeContract(const RecordDecl *RD) const;
+
   /// Allocate an uninitialized TypeSourceInfo.
   ///
   /// The caller should initialize the memory held by TypeSourceInfo using

clang/include/clang/Basic/DiagnosticParseKinds.td

@@ -1898,5 +1898,9 @@ def err_result_outside_postcondition : Error<
   "'result' can only be used in postconditions">;
 def err_old_outside_postcondition : Error<
   "'old' can only be used in postconditions">;
+def warn_contract_member_function_unsupported : Warning<
+  "contracts on member functions are not yet supported and are ignored; "
+  "move the function out of the class or verify it as a free function">,
+  InGroup<DiagGroup<"contract-unsupported">>;
 
 } // end of Parser diagnostics

clang/include/clang/Basic/TokenKinds.def

@@ -450,6 +450,7 @@ KEYWORD(_Defer                      , KEYDEFERTS)
 KEYWORD(pre                         , KEYCONTRACT)
 KEYWORD(post                        , KEYCONTRACT)
 KEYWORD(invariant                   , KEYCONTRACT)
+KEYWORD(type_invariant              , KEYCONTRACT)
 KEYWORD(decreases                   , KEYCONTRACT)
 KEYWORD(ghost                       , KEYCONTRACT)
 KEYWORD(spec                        , KEYCONTRACT)

clang/include/clang/Options/Options.td

@@ -2367,20 +2367,25 @@ defm fixed_point : BoolFOption<"fixed-point",
   NegFlag<SetFalse, [], [ClangOption], "Disable">,
   BothFlags<[], [ClangOption], " fixed point types">>;
 
-// CppVerify: deductive contract verification
+// CppVerify: deductive contract verification.
+// -fverify-contracts enables the contract language (pre/post/...) and, by
+// default, runs the SMT verifier in parallel with code generation.
 defm verify_contracts : BoolFOption<"verify-contracts",
   LangOpts<"VerifyContracts">, DefaultFalse,
   PosFlag<SetTrue, [], [ClangOption, CC1Option],
-          "Enable CppVerify contract syntax (pre/post/invariant/decreases/ghost/spec/proof)">,
+          "Enable CppVerify contracts (pre/post/invariant/decreases/ghost/spec/proof) "
+          "and verify in parallel with compilation">,
   NegFlag<SetFalse, [], [ClangOption], "Disable CppVerify contract syntax">>;
 
-// CppVerify SMT backend (on by default when -fverify-contracts is used).
-defm verify : BoolFOption<"verify",
-  FrontendOpts<"RunCppVerify">, DefaultTrue,
-  PosFlag<SetTrue, [], [ClangOption, CC1Option],
-          "Run CppVerify SMT verification alongside compilation">,
-  NegFlag<SetFalse, [], [ClangOption, CC1Option],
-          "Skip CppVerify SMT verification (contract syntax and codegen only)">>;
+// Skip the CppVerify SMT step. Only the negative is exposed: the verifier runs by
+// default once contracts are enabled, and -fno-verify turns compilation into a
+// syntax/semantics-only "light check". It implies -fverify-contracts (handled in
+// the driver) because it is meaningless without the contract language.
+def fno_verify : Flag<["-"], "fno-verify">, Group<f_clang_Group>,
+  Visibility<[ClangOption, CC1Option]>,
+  HelpText<"Check contract syntax and semantics but skip CppVerify SMT verification "
+           "(implies -fverify-contracts)">,
+  MarshallingInfoNegativeFlag<FrontendOpts<"RunCppVerify">>;
 def cxx_static_destructors_EQ : Joined<["-"], "fc++-static-destructors=">, Group<f_Group>,
   HelpText<"Controls which variables C++ static destructors are registered for">,
   Values<"all,thread-local,none">,

clang/include/clang/Parse/Parser.h

@@ -7466,6 +7466,7 @@ class Parser : public CodeCompletionHandler {
   /// Parse reveal_with_fuel(fn, depth);
   StmtResult ParseRevealWithFuel();
   StmtResult ParseHideSpec();
+  void ParseTypeInvariant(Decl *TagDecl);
   StmtResult ParseRevealSpec();
 
   /// Parse forall(binder, lo, hi, body) or exists(binder, lo, hi, body).

clang/include/clang/Sema/Sema.h

@@ -10281,6 +10281,9 @@ class Sema final : public SemaBase {
   /// each contract condition expression. (SemaContract.cpp)
   ExprResult ActOnContractCondition(ExprResult E);
 
+  /// Rewrite unqualified field names to this->field for type_invariant(expr).
+  ExprResult ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record);
+
   /// PerformContextuallyConvertToObjCPointer - Perform a contextual
   /// conversion of the expression From to an Objective-C pointer type.
   /// Returns a valid but null ExprResult if no conversion sequence exists.

clang/lib/AST/ASTContext.cpp

@@ -3121,6 +3121,22 @@ const LoopContractInfo *ASTContext::getLoopContract(const Stmt *S) const {
   return I != LoopContracts.end() ? I->second : nullptr;
 }
 
+TypeContractInfo &ASTContext::getOrCreateTypeContract(const RecordDecl *RD) {
+  assert(RD && "Passed null record");
+  const RecordDecl *Key = cast<RecordDecl>(RD->getCanonicalDecl());
+  auto &Info = TypeContracts[Key];
+  if (!Info)
+    Info = new (*this) TypeContractInfo();
+  return *Info;
+}
+
+const TypeContractInfo *ASTContext::getTypeContract(const RecordDecl *RD) const {
+  if (!RD)
+    return nullptr;
+  auto I = TypeContracts.find(cast<RecordDecl>(RD->getCanonicalDecl()));
+  return I != TypeContracts.end() ? I->second : nullptr;
+}
+
 TypeSourceInfo *ASTContext::CreateTypeSourceInfo(QualType T,
                                                  unsigned DataSize) const {
   if (!DataSize)

clang/lib/Driver/ToolChains/Clang.cpp

@@ -6365,9 +6365,18 @@ void Clang::ConstructJob(Compilation &C, const JobAction &JA,
   Args.addOptInFlag(CmdArgs, options::OPT_ffixed_point,
                     options::OPT_fno_fixed_point);
 
+  // CppVerify contract language (last-wins between -f/-fno-verify-contracts).
   Args.addOptInFlag(CmdArgs, options::OPT_fverify_contracts,
                     options::OPT_fno_verify_contracts);
-  Args.addOptOutFlag(CmdArgs, options::OPT_fverify, options::OPT_fno_verify);
+  // -fno-verify skips the SMT step. It is meaningless without the contract
+  // language, so when neither -f/-fno-verify-contracts was given it implies
+  // -fverify-contracts, yielding a syntax/semantics-only "light check".
+  if (Args.hasArg(options::OPT_fno_verify)) {
+    CmdArgs.push_back("-fno-verify");
+    if (!Args.hasArg(options::OPT_fverify_contracts) &&
+        !Args.hasArg(options::OPT_fno_verify_contracts))
+      CmdArgs.push_back("-fverify-contracts");
+  }
 
   if (Arg *A = Args.getLastArg(options::OPT_fcxx_abi_EQ))
     A->render(Args, CmdArgs);