verify: Reject the solver options with the Lean backend

clang/test/Verify/suite/backend_options.cpp

@@ -15,9 +15,21 @@
 // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --check-ub 2>&1 | FileCheck %s --check-prefix=REPLAY-UB
 // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --profile-quantifiers 2>&1 | FileCheck %s --check-prefix=REPLAY-PROFILE
 // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --unroll=1 2>&1 | FileCheck %s --check-prefix=REPLAY-UNROLL
+// RUN: not %cpp-verify --lean-out=%t/budget.lean --timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=TIMEOUT
+// RUN: not %cpp-verify --lean-project=%t/budget --function-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=FUNCTION
+// RUN: not test -e %t/budget
+// RUN: not %cpp-verify --backend=lean --collection-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=COLLECTION
+// RUN: not %cpp-verify --lean-out=%t/budget.lean --certify-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFY
+// RUN: not %cpp-verify --lean-out=%t/budget.lean --solver-rlimit=100000 %s -- 2>&1 | FileCheck %s --check-prefix=RLIMIT
+// RUN: not %cpp-verify --lean-out=%t/budget.lean --max-query-nodes=100000 %s -- 2>&1 | FileCheck %s --check-prefix=NODES
+// RUN: not test -e %t/budget.lean
+// RUN: not %cpp-verify --obligation-in=%t/goals.cpv --lean-out=%t/budget.lean --timeout=1000 2>&1 | FileCheck %s --check-prefix=TIMEOUT
+// RUN: %cpp-verify --timeout=20000 --function-timeout=200000 --solver-rlimit=50000000 --max-query-nodes=1000000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER
+// RUN: %cpp-verify --lean-fallback=%t/fallback --timeout=20000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER
 //
 // An option one backend alone uses selects it when no backend is named, and
-// an option the run would ignore is an error.
+// an option the run would ignore is an error: Lean export runs no solver, so
+// no solver option applies to it.
 
 int count(int n)
   cppverify::pre(0 <= n && n <= 2)
@@ -45,3 +57,10 @@ int count(int n)
 // REPLAY-UB: error: --check-ub and --no-check-ub apply to source verification
 // REPLAY-PROFILE: error: --profile-quantifiers applies to source verification
 // REPLAY-UNROLL: error: --unroll requires a BMC-transformed archive
+// TIMEOUT: error: --timeout requires a backend that runs an SMT solver
+// FUNCTION: error: --function-timeout requires a backend that runs an SMT solver
+// COLLECTION: error: --collection-timeout requires a backend that runs an SMT solver
+// CERTIFY: error: --certify-timeout requires a backend that runs an SMT solver
+// RLIMIT: error: --solver-rlimit requires a backend that runs an SMT solver
+// NODES: error: --max-query-nodes requires a backend that runs an SMT solver
+// SOLVER: Verified: count [backend=z3]

clang/test/Verify/suite/lean_backend_failure.cpp

@@ -1,5 +1,5 @@
 // RUN: %clang -std=c++17 -fverify-contracts -fsyntax-only %s
-// RUN: %cpp-verify --backend=lean --timeout=1 --lean-out=%t.lean %s -- 2>&1 | FileCheck %s
+// RUN: %cpp-verify --backend=lean --lean-out=%t.lean %s -- 2>&1 | FileCheck %s
 // RUN: grep -q 'unchecked Lean scratch-pad' %t.lean
 // RUN: grep -Eq 'theorem cppverify_invalid_lean_export_fn_[0-9a-f]+_correct' %t.lean
 // RUN: grep -Eq 'theorem cppverify_invalid_lean_export_fn_[0-9a-f]+_obligation_[0-9]+' %t.lean

clang/tools/cpp-verify/Main.cpp

@@ -558,6 +558,13 @@ static bool resolveOptions(bool Replay) {
       BackendOpt.setValue("bmc");
   }
   const StringRef Backend = BackendOpt.getValue();
+  const cl::Option *SolverOption = nullptr;
+  for (const cl::Option *Option : std::initializer_list<const cl::Option *>{
+           &SolverTimeout, &CollectionTimeout, &CertifyTimeout,
+           &FunctionTimeout, &SolverResourceLimit, &MaxQueryNodes,
+           &IntEncoding})
+    if (!SolverOption && given(*Option))
+      SolverOption = Option;
   std::string Error;
   if (Backend != "z3" && Backend != "cvc5" && Backend != "portfolio" &&
       Backend != "race" && Backend != "lean" && Backend != "bmc")
@@ -581,8 +588,9 @@ static bool resolveOptions(bool Replay) {
   else if (ProfileQuantifiers && (Backend == "cvc5" || Backend == "lean"))
     Error = "--profile-quantifiers requires a backend that runs Z3: z3, "
             "portfolio, race, or bmc";
-  else if (given(IntEncoding) && Backend == "lean")
-    Error = "--int-encoding requires a backend that runs an SMT solver";
+  else if (SolverOption && Backend == "lean")
+    Error = "--" + SolverOption->ArgStr.str() +
+            " requires a backend that runs an SMT solver";
   else if ((given(CheckUB) || given(NoCheckUB)) && Replay)
     Error = "--check-ub and --no-check-ub apply to source verification; an "
             "archive keeps the checks it was written with";

website/source/language/tooling.rst

@@ -162,13 +162,20 @@ nothing is verified:
      - ``error: --cvc5-path requires --backend=cvc5, --backend=portfolio, or --backend=race``
    * - ``--backend=cvc5 --profile-quantifiers``
      - ``error: --profile-quantifiers requires a backend that runs Z3: z3, portfolio, race, or bmc``
-   * - ``--lean-out=FILE --int-encoding=bitvector``
-     - ``error: --int-encoding requires a backend that runs an SMT solver``
+   * - ``--lean-out=FILE --timeout=60000``
+     - ``error: --timeout requires a backend that runs an SMT solver``
    * - ``--proof-cache-max-mb=N`` without ``--proof-cache``
      - ``error: --proof-cache-max-mb and --proof-cache-max-entries require --proof-cache``
    * - ``--lean-fallback-scope=all`` without ``--lean-fallback``
      - ``error: --lean-fallback-scope requires --lean-fallback``
 
+Lean export runs no solver, so every solver option is an error with
+``--backend=lean``, ``--lean-out``, or ``--lean-project``, the same way as
+``--timeout`` above: ``--timeout``, ``--collection-timeout``,
+``--certify-timeout``, ``--function-timeout``, ``--solver-rlimit``,
+``--max-query-nodes``, and ``--int-encoding``. ``--lean-fallback`` runs Z3
+first, and accepts all of them.
+
 The same rules hold when replaying an archive: ``--check-ub`` and
 ``--profile-quantifiers`` are errors there, since an archive keeps the checks
 it was written with, and ``--unroll`` must match the bound a BMC archive
@@ -273,26 +280,31 @@ Backends
    * - ``--timeout=N``
      - Per-query solver timeout in milliseconds (default 30000; ``0`` disables).
        A query that exceeds it is reported as unresolved instead of hanging.
+       Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--certify-timeout=N``
      - The milliseconds checking one counterexample against the true
        definitions may take (default half of the query timeout; ``0`` lets
        it take the query's own time). A slow check leaves the rest of the
        query's time to other models and later stages; when it is reached the
        reason says so (``the time one counterexample check may take (N ms,
        --certify-timeout) was spent``).
+       Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--collection-timeout=N``
      - Per-query timeout for a function whose queries involve sequences,
        sets, multisets, or maps, whose theories need more search (default
        twice ``--timeout``; ``0`` disables).
+       Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--solver-rlimit=N``
      - Deterministic per-query Z3/cvc5 resource budget (default ``0``, disabled).
        Exhaustion is ``Unresolved``. Z3 reports ``solver.resource-limit``;
        cvc5 may report the conservative ``solver.unknown``.
+       Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--max-query-nodes=N``
      - Reject a solver-backed canonical obligation module larger than ``N``
        expression nodes before verification, lower-only encoding, or a requested
        Z3 dump (default ``0``, disabled). Exhaustion is fail-closed with reason
        ``query.size-limit``.
+       Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--int-encoding=MODE``
      - Solver representation of machine integers for Z3, cvc5, portfolio, and
        BMC: ``auto`` (default; integers reduced modulo ``2^N`` unless a query
@@ -308,6 +320,7 @@ Backends
    * - ``--function-timeout=N``
      - Milliseconds all queries of one function may take together (default
        ten times ``--timeout``; ``0`` disables). See `Time limits`_.
+       Not accepted with ``--backend=lean``, which runs no solver.
    * - ``--proof-cache=DIR``
      - Persist successful dependency-scoped Z3 or BMC proofs. In portfolio mode
        this caches only the Z3 component and cvc5 still runs on every query.
@@ -409,6 +422,13 @@ The limits are wall-clock times and depend on the machine. For results that
 must repeat exactly across machines, use ``--solver-rlimit``, a
 deterministic per-query budget of solver steps.
 
+None of these limits applies to Lean, which runs no solver. Lean
+certification (``--lean-certify``) gives each ``lake`` step 300 seconds:
+building the generated module, compiling your module, compiling each proof,
+and the final check. A step that takes longer leaves every result
+``Unresolved`` with reason ``lean.export-failed``, and its message gives the
+command's error.
+
 Parallel solving and proof caching
 ----------------------------------
 

website/source/release-notes.rst

@@ -124,8 +124,10 @@ function as ``Interrupted``, and exits with status 130
 
 **Options select their backend, and unused options are errors.**
 ``--lean-out`` and ``--lean-project`` select Lean and ``--unroll`` selects BMC;
-an option the run would not use, such as ``--unroll`` with ``--backend=z3``, is
-an error that names what it needs, where it was ignored (:doc:`language/tooling`).
+an option the run would not use, such as ``--unroll`` with ``--backend=z3``, or
+``--timeout`` and the other solver budgets with Lean export, which runs no
+solver, is an error that names what it needs, where it was ignored
+(:doc:`language/tooling`).
 
 **Compiler errors stop their file, and headers are C++.** An error in a command
 line was printed and then ignored, and a ``.h`` input was compiled as C. Now