diff --git a/clang/lib/Verify/Backend/CVC5Backend.cpp b/clang/lib/Verify/Backend/CVC5Backend.cpp index 3a53d58e3f..859c316d72 100644 --- a/clang/lib/Verify/Backend/CVC5Backend.cpp +++ b/clang/lib/Verify/Backend/CVC5Backend.cpp @@ -1,6 +1,7 @@ //===--- CVC5Backend.cpp --------------------------------------------------===// #include "CVC5Backend.h" #include "Certify.h" +#include "ChildProcess.h" #include "ObligationSerialization.h" #include "ObligationSimplify.h" #include "TaskGroup.h" @@ -25,14 +26,6 @@ #include #include -#if defined(_WIN32) -#include "llvm/Support/Windows/WindowsSupport.h" -#else -#include -#include -#include -#endif - using namespace clang; using namespace verify; @@ -1542,84 +1535,6 @@ static std::string diagnosticText(llvm::StringRef Text) { return Text.str(); } -enum class ProcessPollState { Running, Exited, Failed }; - -struct ProcessPollResult { - ProcessPollState State = ProcessPollState::Running; - int ExitCode = -1; - std::string Error; -}; - -static ProcessPollResult pollProcess(const llvm::sys::ProcessInfo &Process) { -#if defined(_WIN32) - std::string Error; - llvm::sys::ProcessInfo Waited = - llvm::sys::Wait(Process, 0, &Error, nullptr, true); - if (Waited.Pid == llvm::sys::ProcessInfo::InvalidPid) - return {ProcessPollState::Running, -1, {}}; - if (Waited.Pid != Process.Pid) - return {ProcessPollState::Failed, -1, - Error.empty() ? "cannot poll cvc5 process" : std::move(Error)}; - return {ProcessPollState::Exited, Waited.ReturnCode, std::move(Error)}; -#else - int Status = 0; - pid_t Waited; - do { - Waited = ::waitpid(Process.Pid, &Status, WNOHANG); - } while (Waited == -1 && errno == EINTR); - if (Waited == 0) - return {}; - if (Waited == -1) - return {ProcessPollState::Failed, -1, - "cannot poll cvc5 process: " + - std::error_code(errno, std::generic_category()).message()}; - if (WIFEXITED(Status)) - return {ProcessPollState::Exited, WEXITSTATUS(Status), {}}; - if (WIFSIGNALED(Status)) - return {ProcessPollState::Exited, -2, - "cvc5 terminated by signal " + std::to_string(WTERMSIG(Status))}; - return {ProcessPollState::Failed, -1, - "cvc5 changed to an unsupported process state"}; -#endif -} - -static bool terminateAndReap(const llvm::sys::ProcessInfo &Process, - std::string &Error) { -#if defined(_WIN32) - if (!::TerminateProcess(static_cast(Process.Process), 1) && - ::GetLastError() != ERROR_ACCESS_DENIED) { - Error = "cannot terminate cvc5 process"; - return false; - } - std::string WaitError; - llvm::sys::ProcessInfo Waited = - llvm::sys::Wait(Process, std::nullopt, &WaitError); - if (Waited.Pid != Process.Pid) { - Error = - WaitError.empty() ? "cannot reap cvc5 process" : std::move(WaitError); - return false; - } - return true; -#else - if (::kill(Process.Pid, SIGKILL) == -1 && errno != ESRCH) { - Error = "cannot terminate cvc5 process: " + - std::error_code(errno, std::generic_category()).message(); - return false; - } - int Status = 0; - pid_t Waited; - do { - Waited = ::waitpid(Process.Pid, &Status, 0); - } while (Waited == -1 && errno == EINTR); - if (Waited == -1 && errno != ECHILD) { - Error = "cannot reap cvc5 process: " + - std::error_code(errno, std::generic_category()).message(); - return false; - } - return true; -#endif -} - static bool startsWithSat(llvm::StringRef OutputPath) { auto Buffer = llvm::MemoryBuffer::getFileSlice(OutputPath, 4, 0, false); return Buffer && (*Buffer)->getBuffer() == "sat\n"; @@ -2548,16 +2463,16 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, bool Stopped = false; bool OutputLimitExceeded = false; while (true) { - ProcessPollResult Poll = pollProcess(Process); - if (Poll.State == ProcessPollState::Exited) { + ChildPoll Poll = pollChild(Process, "cvc5"); + if (Poll.State == ChildState::Exited) { ExitCode = Poll.ExitCode; InvocationError = std::move(Poll.Error); break; } - if (Poll.State == ProcessPollState::Failed) { + if (Poll.State == ChildState::Failed) { InvocationError = std::move(Poll.Error); std::string TerminationError; - if (!terminateAndReap(Process, TerminationError) && + if (!terminateChild(Process, "cvc5", TerminationError) && !TerminationError.empty()) InvocationError += ": " + TerminationError; break; @@ -2568,7 +2483,7 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, OutputLimitExceeded)) { InvocationError = std::move(OutputError); std::string TerminationError; - if (!terminateAndReap(Process, TerminationError) && + if (!terminateChild(Process, "cvc5", TerminationError) && !TerminationError.empty()) InvocationError += ": " + TerminationError; break; @@ -2576,14 +2491,14 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, if ((Cancelled && *Cancelled) || interruptRequested()) { Stopped = true; std::string TerminationError; - if (!terminateAndReap(Process, TerminationError)) + if (!terminateChild(Process, "cvc5", TerminationError)) InvocationError = std::move(TerminationError); break; } if (TimeoutMs != 0 && std::chrono::steady_clock::now() >= Deadline) { TimedOut = true; std::string TerminationError; - if (!terminateAndReap(Process, TerminationError)) + if (!terminateChild(Process, "cvc5", TerminationError)) InvocationError = std::move(TerminationError); break; } diff --git a/clang/lib/Verify/Backend/ChildProcess.cpp b/clang/lib/Verify/Backend/ChildProcess.cpp new file mode 100644 index 0000000000..6fcbb37b78 --- /dev/null +++ b/clang/lib/Verify/Backend/ChildProcess.cpp @@ -0,0 +1,120 @@ +#include "ChildProcess.h" +#include "llvm/Support/ConvertUTF.h" +#include + +#if defined(_WIN32) +#include "llvm/Support/Windows/WindowsSupport.h" +#else +#include +#include +#include +#if defined(__APPLE__) +#include +#define environ (*_NSGetEnviron()) +#else +extern char **environ; +#endif +#endif + +namespace clang { +namespace verify { + +ChildPoll pollChild(const llvm::sys::ProcessInfo &Process, + llvm::StringRef Name) { +#if defined(_WIN32) + std::string Error; + llvm::sys::ProcessInfo Waited = + llvm::sys::Wait(Process, 0, &Error, nullptr, true); + if (Waited.Pid == llvm::sys::ProcessInfo::InvalidPid) + return {ChildState::Running, -1, {}}; + if (Waited.Pid != Process.Pid) + return {ChildState::Failed, -1, + Error.empty() ? "cannot poll " + Name.str() + " process" + : std::move(Error)}; + return {ChildState::Exited, Waited.ReturnCode, std::move(Error)}; +#else + int Status = 0; + pid_t Waited; + do { + Waited = ::waitpid(Process.Pid, &Status, WNOHANG); + } while (Waited == -1 && errno == EINTR); + if (Waited == 0) + return {}; + if (Waited == -1) + return {ChildState::Failed, -1, + "cannot poll " + Name.str() + " process: " + + std::error_code(errno, std::generic_category()).message()}; + if (WIFEXITED(Status)) + return {ChildState::Exited, WEXITSTATUS(Status), {}}; + if (WIFSIGNALED(Status)) + return {ChildState::Exited, -2, + Name.str() + " terminated by signal " + + std::to_string(WTERMSIG(Status))}; + return {ChildState::Failed, -1, + Name.str() + " changed to an unsupported process state"}; +#endif +} + +bool terminateChild(const llvm::sys::ProcessInfo &Process, llvm::StringRef Name, + std::string &Error) { +#if defined(_WIN32) + if (!::TerminateProcess(static_cast(Process.Process), 1) && + ::GetLastError() != ERROR_ACCESS_DENIED) { + Error = "cannot terminate " + Name.str() + " process"; + return false; + } + std::string WaitError; + llvm::sys::ProcessInfo Waited = + llvm::sys::Wait(Process, std::nullopt, &WaitError); + if (Waited.Pid != Process.Pid) { + Error = WaitError.empty() ? "cannot reap " + Name.str() + " process" + : std::move(WaitError); + return false; + } + return true; +#else + if (::kill(Process.Pid, SIGKILL) == -1 && errno != ESRCH) { + Error = "cannot terminate " + Name.str() + " process: " + + std::error_code(errno, std::generic_category()).message(); + return false; + } + int Status = 0; + pid_t Waited; + do { + Waited = ::waitpid(Process.Pid, &Status, 0); + } while (Waited == -1 && errno == EINTR); + if (Waited == -1 && errno != ECHILD) { + Error = "cannot reap " + Name.str() + " process: " + + std::error_code(errno, std::generic_category()).message(); + return false; + } + return true; +#endif +} + +std::vector childEnvironment(llvm::StringRef Variable, + llvm::StringRef Value) { + std::vector Environment; + auto add = [&](llvm::StringRef Entry) { + if (!Entry.starts_with((Variable + "=").str())) + Environment.push_back(Entry.str()); + }; +#if defined(_WIN32) + if (wchar_t *Block = ::GetEnvironmentStringsW()) { + for (const wchar_t *Entry = Block; *Entry; Entry += wcslen(Entry) + 1) { + std::string Narrow; + if (llvm::convertWideToUTF8(Entry, Narrow)) + add(Narrow); + } + ::FreeEnvironmentStringsW(Block); + } +#else + for (char **Entry = environ; Entry && *Entry; ++Entry) + add(*Entry); +#endif + Environment.push_back((Variable + "=" + Value).str()); + return Environment; +} + +} // namespace verify +} // namespace clang diff --git a/clang/lib/Verify/Backend/ChildProcess.h b/clang/lib/Verify/Backend/ChildProcess.h new file mode 100644 index 0000000000..c273354403 --- /dev/null +++ b/clang/lib/Verify/Backend/ChildProcess.h @@ -0,0 +1,38 @@ +//===--- ChildProcess.h - Polling and stopping a process ----------------===// +#ifndef LLVM_CLANG_VERIFY_BACKEND_CHILDPROCESS_H +#define LLVM_CLANG_VERIFY_BACKEND_CHILDPROCESS_H + +#include "llvm/ADT/StringRef.h" +#include "llvm/Support/Program.h" +#include +#include + +namespace clang { +namespace verify { + +enum class ChildState { Running, Exited, Failed }; + +struct ChildPoll { + ChildState State = ChildState::Running; + int ExitCode = -1; + std::string Error; +}; + +/// Whether the process has ended, without waiting for it. Name is what the +/// messages call it. +ChildPoll pollChild(const llvm::sys::ProcessInfo &Process, + llvm::StringRef Name); + +/// Kills the process and reaps it. +bool terminateChild(const llvm::sys::ProcessInfo &Process, llvm::StringRef Name, + std::string &Error); + +/// This process's environment with Variable set to Value, for a child: a +/// child of several started at once cannot be given it by changing ours. +std::vector childEnvironment(llvm::StringRef Variable, + llvm::StringRef Value); + +} // namespace verify +} // namespace clang + +#endif diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt index 870d29c22c..ee25e789a6 100644 --- a/clang/lib/Verify/CMakeLists.txt +++ b/clang/lib/Verify/CMakeLists.txt @@ -40,6 +40,7 @@ add_clang_library(clangVerify Backend/ObligationSimplify.cpp Backend/ObligationSerialization.cpp Backend/ProofCache.cpp + Backend/ChildProcess.cpp Backend/CVC5Backend.cpp Backend/Z3Encode.cpp Backend/SpecAxioms.cpp diff --git a/clang/lib/Verify/Driver/LeanAutomation.h b/clang/lib/Verify/Driver/LeanAutomation.h new file mode 100644 index 0000000000..0db32bac01 --- /dev/null +++ b/clang/lib/Verify/Driver/LeanAutomation.h @@ -0,0 +1,162 @@ +//===--- LeanAutomation.h - The tactics of automatic Lean proofs -------===// +#ifndef LLVM_CLANG_VERIFY_DRIVER_LEANAUTOMATION_H +#define LLVM_CLANG_VERIFY_DRIVER_LEANAUTOMATION_H + +#include "llvm/ADT/StringRef.h" + +namespace clang { +namespace verify { + +/// Names this module's tactics: a stub or automatic proof that an earlier +/// revision wrote is tried again. +inline constexpr llvm::StringLiteral LeanAutomationRevision = "1"; + +/// The steps of cppverify_auto, each the whole proof of a goal it proves. +inline constexpr llvm::StringLiteral LeanAutomationSteps[] = { + "cppverify_auto_grind", "cppverify_auto_heap", "cppverify_auto_bv", + "cppverify_auto_decide", "cppverify_auto_simp"}; + +/// CppVerify/Auto.lean, written with every export. Its steps were chosen by +/// what proves the goals of the test suite (heap stores as the functions +/// they define, machine arithmetic as integers, then grind; stating toInt +/// ranges and removing Int.bmod first proved nothing more, the latter less), +/// each with a heartbeat budget of its own, as Vermilion's discharger ladder. +inline constexpr llvm::StringLiteral LeanAutomationSource = + R"lean(/- Generated by CppVerify: the tactics of its automatic proofs, which proof + files may use too. Regeneration replaces this file. -/ +import Lean +import CppVerify.Generated + +register_option cppverify.autoBudget : Nat := { + defValue := 50000 + descr := "the heartbeats, in thousands, each step of cppverify_auto may take" +} + +register_option cppverify.autoReport : String := { + defValue := "" + descr := "a file to which cppverify_auto adds the step that proves each goal" +} + +namespace CppVerify.Auto +open Lean Elab Tactic Meta + +/-- Adds a line to a report, written at once: a process stopped later keeps +it. -/ +def report (file line : String) : IO Unit := do + let handle ← IO.FS.Handle.mk file .append + handle.putStrLn line + handle.flush + +/-- Whether a proof depends on no axiom but Lean's foundations: a step that +proves a goal with a lemma the user has not proved is no proof. -/ +def foundational (proof : Expr) : MetaM Bool := do + for c in proof.getUsedConstants do + let axioms ← try collectAxioms c catch _ => return false + for a in axioms do + unless a == ``propext || a == ``Quot.sound || a == ``Classical.choice do + return false + return true + +end CppVerify.Auto + +open Lean Elab Command in +/-- Reports the axioms a theorem depends on, or that the environment has no +such theorem (the kernel rejected it). -/ +elab "#cppverify_axioms " file:str name:ident : command => do + let name := name.getId + let line ← liftCoreM do + if (← getEnv).contains name then + let axioms ← collectAxioms name + pure s!"axioms\t{name}\t{",".intercalate (axioms.toList.map toString)}" + else + pure s!"axioms\t{name}\tmissing" + CppVerify.Auto.report file.getString line + +open Lean Elab Tactic Meta in +/-- Unfolds a goal that is still a readable form, as one without binders is +after `apply G.of_readable`. -/ +elab "cppverify_unfold_readable" : tactic => withMainContext do + let target ← getMainTarget + if let .const name _ := target.getAppFn then + if name.isStr && name.getString! == "readable" then + let unfolded ← deltaExpand target (· == name) + replaceMainGoal [← (← getMainGoal).change unfolded] + +/-- Machine comparisons, constants, and overflow conditions as facts about +integers. -/ +macro "cppverify_norm" : tactic => `(tactic| (try simp only [cppBvSlt, cppBvSle, + cppBvUlt, cppBvUle, BitVec.slt_iff_toInt_lt, BitVec.sle_iff_toInt_le, + BitVec.ult_iff_lt, BitVec.ule_iff_le, BitVec.lt_def, BitVec.le_def, + BitVec.toInt_ofInt, BitVec.signExtend_eq, BitVec.saddOverflow, + BitVec.ssubOverflow, BitVec.smulOverflow, BitVec.negOverflow, + BitVec.sdivOverflow, BitVec.uaddOverflow, BitVec.toInt_add, BitVec.toInt_sub, + BitVec.toInt_mul, BitVec.toInt_neg, decide_eq_true_eq, decide_eq_false_iff_not, + Bool.or_eq_true, Bool.and_eq_true, Bool.not_eq_true, Bool.or_eq_false_iff, + Bool.and_eq_false_iff, ge_iff_le, gt_iff_lt, Nat.reducePow, Nat.reduceSub, + Nat.reduceAdd, Nat.reduceMul] at *)) + +/-- Memory as values: each store is the function it defines. -/ +macro "cppverify_heap" : tactic => `(tactic| ( + try simp only [heapStoreInt, heapStoreBool, heapStoreBv] at * + try subst_vars + try simp only [heapSelectInt, heapSelectBool, heapSelectBv] at *)) + +/-- The steps of `cppverify_auto`, cheapest first. -/ +macro "cppverify_auto_grind" : tactic => + `(tactic| (cppverify_unfold_readable; grind)) +macro "cppverify_auto_heap" : tactic => `(tactic| ( + cppverify_unfold_readable + cppverify_heap + cppverify_norm + all_goals grind)) +macro "cppverify_auto_bv" : tactic => `(tactic| ( + cppverify_unfold_readable + cppverify_norm + all_goals grind)) +macro "cppverify_auto_decide" : tactic => + `(tactic| (cppverify_unfold_readable; decide)) +macro "cppverify_auto_simp" : tactic => + `(tactic| (cppverify_unfold_readable; simp_all)) + +open Lean Elab Tactic in +/-- Tries each step on the goal, each with `cppverify.autoBudget` heartbeats +of its own, and keeps the first that proves it. A step that runs out of +heartbeats, leaves goals, or uses an axiom outside Lean's foundations counts +as failed and changes nothing. -/ +elab "cppverify_auto" : tactic => do + let options ← getOptions + let goal ← getMainGoal + let budget := cppverify.autoBudget.get options + let steps : List (String × Syntax.Tactic) := [ + ("cppverify_auto_grind", ← `(tactic| cppverify_auto_grind)), + ("cppverify_auto_heap", ← `(tactic| cppverify_auto_heap)), + ("cppverify_auto_bv", ← `(tactic| cppverify_auto_bv)), + ("cppverify_auto_decide", ← `(tactic| cppverify_auto_decide)), + ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp))] + for (name, step) in steps do + let attempt : TacticM Unit := do + let heartbeats ← IO.getNumHeartbeats + withTheReader Core.Context + (fun ctx => { ctx with initHeartbeats := heartbeats, + maxHeartbeats := budget * 1000 }) do + evalTactic step + unless (← getUnsolvedGoals).isEmpty do + throwError "{name} left goals" + unless ← CppVerify.Auto.foundational (← instantiateMVars (.mvar goal)) do + throwError "{name} used an axiom outside Lean's foundations" + let saved ← saveState + let proved ← tryCatchRuntimeEx (return (← tryTactic? attempt).isSome) + fun _ => do saved.restore; return false + if proved then + let file := cppverify.autoReport.get options + unless file.isEmpty do + let decl := (← Term.getDeclName?).getD .anonymous + CppVerify.Auto.report file s!"step\t{decl}\t{name}" + return + throwError "cppverify_auto did not prove the goal (tried {steps.map (·.1)})" +)lean"; + +} // namespace verify +} // namespace clang + +#endif diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h index 4b4bbd12ae..dc62393db9 100644 --- a/clang/lib/Verify/Driver/LeanCertifier.h +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -38,9 +38,9 @@ def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run | none => return .error s!"{c} is not in the environment" return .ok axioms -/-- Replays a module's own constants into the environment of its imports with -the kernel, as leanchecker does: nothing in it escaped the kernel. -/ -unsafe def replayModule (module : Name) : IO Unit := do +/-- A module's imports and its own constants, read from its compiled files. -/ +unsafe def moduleConstants (module : Name) : + IO (Array Import × Std.HashMap Name ConstantInfo) := do let file ← findOLean module let mut files := #[file] let server := OLeanLevel.server.adjustFileName file @@ -51,14 +51,24 @@ unsafe def replayModule (module : Name) : IO Unit := do files := files.push priv let parts ← readModuleDataParts files if h : parts.size = 0 then throw <| IO.userError "cannot read the module" else - let (data, _) := parts[0] - let (_, s) ← importModulesCore data.imports |>.run - let env ← finalizeImport s data.imports {} 0 false false (isModule := true) let mut constants := {} for name in parts[parts.size - 1].1.constNames, info in parts[parts.size - 1].1.constants do constants := constants.insert name info + return (parts[0].1.imports, constants) + +/-- Replays constants with the kernel into the environment of imports, as +leanchecker does: nothing in them escaped the kernel. -/ +unsafe def replayInto (imports : Array Import) + (constants : Std.HashMap Name ConstantInfo) : IO Unit := do + let (_, s) ← importModulesCore imports |>.run + let env ← finalizeImport s imports {} 0 false false (isModule := true) discard <| env.toKernelEnv.replay constants +/-- Replays a module's own constants into the environment of its imports. -/ +unsafe def replayModule (module : Name) : IO Unit := do + let (imports, constants) ← moduleConstants module + replayInto imports constants + /-- Whether the proof of a goal states exactly the goal the generated module defines and depends on no axiom outside the allowed ones. -/ def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) : @@ -107,6 +117,39 @@ unsafe def checkGoal (goal module : Name) (allowed : NameSet) (toolchain : Strin replayed.modify (·.insert m) return why +/-- Every goal checked in one environment: each proof module imported once, +and every module of the project replayed together into the environment of the +toolchain's modules they import. A check reads only kernel constants, each +in the module that declares it, so proofs imported together cannot change +each other's checks; but one bad module would stop the replay of all, and a +proof file that declares a goal's name stops the import, so then none is +reported (`none`) and each goal is checked by itself. A proof file of +cppverify_auto imports `Lean`, whose import each goal would repeat. -/ +unsafe def checkTogether (entries : Array (Name × Name)) (allowed : NameSet) + (toolchain : String) : IO (Option (Array (Option String))) := do + let modules := entries.foldl (fun ms (_, m) => if ms.contains m then ms else ms.push m) #[] + let some env ← (try some <$> importModules (modules.map ({ module := · })) {} + catch _ => pure none) | return none + let project ← env.header.moduleNames.filterM fun m => + return !(← findOLean m).toString.startsWith toolchain + let mut imports : Array Import := #[] + let mut constants : Std.HashMap Name ConstantInfo := {} + for m in project do + let (own, declared) ← moduleConstants m + for i in own do + unless project.contains i.module || imports.any (·.module == i.module) do + imports := imports.push i + -- Lean derives an equation lemma in each module that unfolds the + -- definition, the same constant every time. + for (name, info) in declared do + if let some known := constants[name]? then + unless known.type == info.type && known.value? == info.value? do + return none + continue + constants := constants.insert name info + try replayInto imports constants catch _ => return none + return some (entries.map fun (goal, module) => checkStatement env goal module allowed) + /-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal and its proof module, separated by a tab, and ALLOWED lists the axioms a proof may use, separated by commas. Prints one line per goal: `ok` or `fail`, the goal, @@ -117,12 +160,20 @@ unsafe def main (args : List String) : IO UInt32 := do initSearchPath sysroot let toolchain := (sysroot / "lib" / "lean").toString let allowed := (allowed.splitOn ",").foldl (fun s a => s.insert a.toName) ({} : NameSet) - let replayed ← IO.mkRef ({} : NameSet) + let mut entries : Array (Name × Name) := #[] for line in ← IO.FS.lines goals do let [goal, module] := line.splitOn "\t" | continue - match ← checkGoal goal.toName module.toName allowed toolchain replayed with + entries := entries.push (goal.toName, module.toName) + let report (goal : Name) : Option String → IO Unit | none => IO.println s!"ok\t{goal}" | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" + if let some results ← checkTogether entries allowed toolchain then + for (goal, _) in entries, why in results do + report goal why + return 0 + let replayed ← IO.mkRef ({} : NameSet) + for (goal, module) in entries do + report goal (← checkGoal goal module allowed toolchain replayed) return 0 )lean"; diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index d7132559b8..2a046c752f 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2,6 +2,7 @@ #include "Verifier.h" #include "../Backend/CVC5Backend.h" #include "../Backend/Certify.h" +#include "../Backend/ChildProcess.h" #include "../Backend/Induction.h" #include "../Backend/LeanBackend.h" #include "../Backend/LogicTerms.h" @@ -22,6 +23,7 @@ #include "../Transform/UBChecks.h" #include "CppVerifyVersion.h" #include "DumpIR.h" +#include "LeanAutomation.h" #include "LeanCertifier.h" #include "clang/AST/ASTContext.h" #include "clang/Basic/SourceManager.h" @@ -39,11 +41,14 @@ #include "llvm/Support/Path.h" #include "llvm/Support/Program.h" #include "llvm/Support/ThreadPool.h" +#include "llvm/Support/Threading.h" #include "llvm/Support/raw_ostream.h" +#include #include #include #include #include +#include #include using namespace clang; @@ -1052,6 +1057,9 @@ struct VerifyDiagnostic { SourceLocation Loc; std::string FunctionName; std::optional Result; + /// For an export to a Lean project: of its goals, how many cppverify_auto + /// proves. + unsigned LeanAutomatic = 0; /// A proof by a solver, by Lean, or by both, which establishes what it /// proves. bool isProof() const { @@ -1295,40 +1303,78 @@ struct LeanProofRecord { std::string Hash; std::string StableId; std::string BodyPrefix; - /// The stub cpp-verify wrote, never edited: nothing in it is the user's. + /// The file cpp-verify wrote, never edited: a stub, or the proof + /// cppverify_auto found. Nothing in it is the user's. bool Pristine = false; + /// The proof cppverify_auto found. + bool Automatic = false; + /// What the header says automation made of the goal, and which revision + /// of it. + std::string Automation; }; -// A stub proves the goal through its readable form, its names introduced. -static std::string leanProofStubHead(llvm::StringRef Goal) { - return "import CppVerify.User\n\ntheorem " + Goal.str() + - "_proof : " + Goal.str() + " := by\n apply " + Goal.str() + - ".of_readable\n"; +// A proof starts from the goal's readable form, its names introduced. Stubs +// before cppverify_auto did not import it. +static std::string leanProofHead(llvm::StringRef Goal, bool Automation = true) { + return "import CppVerify.User\n" + + std::string(Automation ? "import CppVerify.Auto\n" : "") + + "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + + " := by\n apply " + Goal.str() + ".of_readable\n"; } -static std::string leanProofStub(llvm::StringRef Goal, llvm::StringRef Intros) { - std::string Stub = leanProofStubHead(Goal); +static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, + llvm::StringRef Last) { + std::string Proof = leanProofHead(Goal); if (!Intros.empty()) - Stub += " intro " + Intros.str() + "\n"; - return Stub + " sorry\n"; + Proof += " intro " + Intros.str() + "\n"; + return Proof + " " + Last.str() + "\n"; } -static bool isLeanProofStub(llvm::StringRef Body, llvm::StringRef Goal) { - if (!Body.consume_front(leanProofStubHead(Goal)) || - !Body.consume_back(" sorry\n")) +// Whether a proof is one cpp-verify wrote and nobody edited, and if so, +// whether cppverify_auto proves it: its last line is a stub's `sorry` or a +// step of cppverify_auto. +static std::optional leanGeneratedProof(llvm::StringRef Body, + llvm::StringRef Goal) { + if (!Body.consume_front(leanProofHead(Goal)) && + !Body.consume_front(leanProofHead(Goal, /*Automation=*/false))) + return std::nullopt; + if (Body.consume_front(" intro ")) { + const size_t End = Body.find('\n'); + if (End == llvm::StringRef::npos) + return std::nullopt; + Body = Body.drop_front(End + 1); + } + if (Body == " sorry\n") return false; - return Body.empty() || (Body.consume_front(" intro ") && - Body.consume_back("\n") && !Body.contains('\n')); + for (llvm::StringRef Step : LeanAutomationSteps) + if (Body == (" " + Step + "\n").str()) + return true; + return std::nullopt; +} + +// The revision of cppverify_auto that an automation note was written by. +static std::string leanAutomationTag() { + return ("cppverify_auto " + LeanAutomationRevision + " ").str(); } -static std::string leanProofHeader(const LeanProjectGoal &Goal) { - return LeanProofMark.str() + " goal: " + Goal.Name + - "\n obligation: " + Goal.StableId + "\n hash: " + Goal.Hash + - "\n bodies: " + Goal.BodyPrefix + - "\n source: " + (Goal.Source.empty() ? "unknown" : Goal.Source) + - "\n Complete this proof. cpp-verify never rewrites it: it moves it " - "with its goal,\n and keeps it in Stale/ when no goal has its " - "statement. -/\n"; +static std::string leanProofHeader(const LeanProjectGoal &Goal, + llvm::StringRef Automation = "", + bool Automatic = false) { + std::string Header = + LeanProofMark.str() + " goal: " + Goal.Name + + "\n obligation: " + Goal.StableId + "\n hash: " + Goal.Hash + + "\n bodies: " + Goal.BodyPrefix + + "\n source: " + (Goal.Source.empty() ? "unknown" : Goal.Source); + if (!Automation.empty()) + Header += "\n automation: " + Automation.str(); + return Header + + (Automatic + ? "\n cppverify_auto proves this goal. cpp-verify rewrites " + "this file only while it\n is unedited; a proof you write " + "here is yours, kept as any other. -/\n" + : "\n Complete this proof. Once you edit it, cpp-verify never " + "rewrites it: it moves\n it with its goal, and keeps it in " + "Stale/ when no goal has its statement. -/\n"); } static std::optional readLeanProof(llvm::StringRef Path) { @@ -1353,12 +1399,18 @@ static std::optional readLeanProof(llvm::StringRef Path) { Record.Hash = Line.str(); else if (Line.consume_front("bodies: ")) Record.BodyPrefix = Line.str(); + else if (Line.consume_front("automation: ")) + Record.Automation = Line.str(); } if (Record.Goal.empty() || Record.Hash.empty()) return std::nullopt; const size_t End = Text.find("-/\n"); - Record.Pristine = End != llvm::StringRef::npos && - isLeanProofStub(Text.substr(End + 3), Record.Goal); + if (End != llvm::StringRef::npos) + if (std::optional Automatic = + leanGeneratedProof(Text.substr(End + 3), Record.Goal)) { + Record.Pristine = true; + Record.Automatic = *Automatic; + } return Record; } @@ -1614,6 +1666,10 @@ class Verifier { if (llvm::Error Error = writeTextFileIfMissing( leanProjectPath(Root, {"CppVerify", "User.lean"}), UserFile)) return std::move(Error); + if (llvm::Error Error = + writeTextFile(leanProjectPath(Root, {"CppVerify", "Auto.lean"}), + LeanAutomationSource)) + return std::move(Error); return leanProjectPath(Root, {"CppVerify", "Generated.lean"}); } @@ -1775,7 +1831,7 @@ class Verifier { ProofPath.c_str()); if (llvm::Error Error = writeTextFile( ProofPath, leanProofHeader(*Goal) + - leanProofStub(Goal->Name, Goal->Intros))) + leanProof(Goal->Name, Goal->Intros, "sorry"))) return Error; Taken.insert(ProofPath); } @@ -1871,42 +1927,53 @@ class Verifier { // goals whose proofs fail, each with why. A proof's own module must build // without `sorry`; then the certifier (LeanCertifier.h) checks the compiled // modules, which nothing in the user's source can change. - llvm::Expected> - certifyLeanProject(const std::vector &ProjectGoals) { - if (ProjectGoals.empty()) - return llvm::createStringError(llvm::inconvertibleErrorCode(), - "the project has no proof obligations"); + // How many Lean processes to run at once for Tasks of them. + unsigned leanJobs(size_t Tasks) const { + const unsigned Jobs = + Opts.LeanJobs + ? Opts.LeanJobs + : llvm::heavyweight_hardware_concurrency().compute_thread_count(); + return std::max(1, std::min(Tasks, Jobs)); + } + + // How lake runs the Lean the project pins. elan picks a toolchain by the + // working directory, not by --dir, so its proxy is given the pin; and + // whatever runs, lake must report the pinned Lean. + struct LeanLauncher { + std::string Lake; + std::vector Prefix; + std::string LogBase; + + llvm::Expected run(std::vector Arguments, + llvm::StringRef Stage, + llvm::StringRef Root) const { + std::vector Command = Prefix; + Command.push_back("--dir=" + Root.str()); + Command.insert(Command.end(), std::make_move_iterator(Arguments.begin()), + std::make_move_iterator(Arguments.end())); + return executeWithLogs(Lake, Command, LogBase + "-" + Stage.str()); + } + }; + + llvm::Expected leanLauncher(llvm::StringRef Purpose) { auto Lake = llvm::sys::findProgramByName("lake"); if (!Lake) return llvm::createStringError(Lake.getError(), "cannot find the Lean project launcher"); - - const std::string &Root = leanProjectRoot(); - const std::string LogBase = - leanProjectPath(Root, {".cppverify-certification"}); - // Every step runs the Lean the project pins. elan picks a toolchain by - // the working directory, not by --dir, so its proxy is given the pin; - // and whatever runs, lake must report the pinned Lean. - std::vector Launcher = {"lake"}; + LeanLauncher Launcher{ + *Lake, {"lake"}, leanProjectPath(leanProjectRoot(), {Purpose})}; auto Elan = llvm::sys::findProgramByName("elan"); bool ViaElan = false; if (!Elan || llvm::sys::fs::equivalent(*Lake, *Elan, ViaElan)) ViaElan = false; if (ViaElan) - Launcher.push_back(("+" + LeanToolchain).str()); - auto runLake = [&](std::vector Arguments, - llvm::StringRef Stage) -> llvm::Expected { - std::vector Command = Launcher; - Command.push_back("--dir=" + Root); - Command.insert(Command.end(), std::make_move_iterator(Arguments.begin()), - std::make_move_iterator(Arguments.end())); - return executeWithLogs(*Lake, Command, LogBase + "-" + Stage.str()); - }; + Launcher.Prefix.push_back(("+" + LeanToolchain).str()); // lake takes --version alone. - std::vector Query = Launcher; + std::vector Query = Launcher.Prefix; Query.push_back("--version"); - auto Reported = executeWithLogs(*Lake, Query, LogBase + "-version"); + auto Reported = + executeWithLogs(*Lake, Query, Launcher.LogBase + "-version"); if (!Reported) return Reported.takeError(); const llvm::StringRef Pinned = @@ -1926,8 +1993,25 @@ class Verifier { "toolchain", LeanToolchain.str().c_str(), Lake->c_str(), Version.empty() ? "of an unknown version" : Version.str().c_str()); + return Launcher; + } - if (auto Build = runLake({"build", "CppVerify.Generated", "CppVerify.User"}, + llvm::Expected> + certifyLeanProject(const std::vector &ProjectGoals) { + if (ProjectGoals.empty()) + return llvm::createStringError(llvm::inconvertibleErrorCode(), + "the project has no proof obligations"); + auto Launcher = leanLauncher(".cppverify-certification"); + if (!Launcher) + return Launcher.takeError(); + const std::string &Root = leanProjectRoot(); + auto runLake = [&](std::vector Arguments, + llvm::StringRef Stage) { + return Launcher->run(std::move(Arguments), Stage, Root); + }; + + if (auto Build = runLake({"build", "CppVerify.Generated", "CppVerify.User", + "CppVerify.Auto"}, "build"); !Build) return Build.takeError(); @@ -1950,26 +2034,46 @@ class Verifier { std::map UniqueGoals; for (const LeanProjectGoal &Goal : ProjectGoals) UniqueGoals.emplace(Goal.Name, &Goal); - std::map Failures; - std::string Built; - for (const auto &[Name, Goal] : UniqueGoals) { - std::string File; - const std::string ProofSource = - leanProjectPath(Root, leanProofComponents(*Goal, File)); - const std::string ObjectDir = - leanProjectPath(ProofBuildDir, {Goal->Group}); - if (std::error_code EC = llvm::sys::fs::create_directories(ObjectDir)) + std::vector> Proofs( + UniqueGoals.begin(), UniqueGoals.end()); + for (const auto &[Name, Goal] : Proofs) + if (std::error_code EC = llvm::sys::fs::create_directories( + leanProjectPath(ProofBuildDir, {Goal->Group}))) return llvm::createStringError( EC, "cannot create Lean proof build directory"); - const std::string ProofObject = - leanProjectPath(ObjectDir, {Name + ".olean"}); - llvm::sys::fs::remove(ProofObject); - if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", - ProofObject, ProofSource}, - Name); - !Proof) { - Failures[Name] = - llvm::StringRef(llvm::toString(Proof.takeError())).rtrim().str(); + // Each proof builds by itself, several at once. + std::vector> BuildErrors(Proofs.size()); + std::atomic NextProof{0}; + auto buildProofs = [&] { + for (size_t I; (I = NextProof++) < Proofs.size();) { + const auto &[Name, Goal] = Proofs[I]; + std::string File; + const std::string ProofSource = + leanProjectPath(Root, leanProofComponents(*Goal, File)); + const std::string ProofObject = leanProjectPath( + leanProjectPath(ProofBuildDir, {Goal->Group}), {Name + ".olean"}); + llvm::sys::fs::remove(ProofObject); + if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", + ProofObject, ProofSource}, + Name); + !Proof) + BuildErrors[I] = + llvm::StringRef(llvm::toString(Proof.takeError())).rtrim().str(); + } + }; + { + std::vector Builders; + for (unsigned J = 0, E = leanJobs(Proofs.size()); J != E; ++J) + Builders.emplace_back(buildProofs); + for (std::thread &Builder : Builders) + Builder.join(); + } + std::map Failures; + std::string Built; + for (size_t I = 0; I != Proofs.size(); ++I) { + const auto &[Name, Goal] = Proofs[I]; + if (BuildErrors[I]) { + Failures[Name] = *BuildErrors[I]; continue; } Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + "\n"; @@ -2011,6 +2115,320 @@ class Verifier { return Failures; } + // What cppverify_auto made of a goal: the step that proves it, or why it + // did not. + struct LeanTrial { + std::string Step; + std::string Why; + }; + + // Runs cppverify_auto on each goal in one Lean process, in order, and keeps + // a proof only when the kernel accepted it with Lean's foundational axioms + // alone: a probe of the suite saw a step claim a false goal with a term the + // kernel rejected. Lean reports to a file, line by line (its messages come + // from a thread of its own, buffered, and are lost when it is stopped): the + // step that proved each goal, then the axioms of its theorem, or that the + // kernel rejected it. A goal with an error is elaborated with sorryAx. A + // goal that takes longer than Limit, or stops Lean, is not proved, and the + // goals after it start again in a new process; heartbeats bound no kernel + // check. Goals Lean cannot start on are left out. + std::map + tryLeanGoals(const std::vector &Goals, + const std::string &Lean, + const std::vector &Environment, unsigned Chunk, + std::optional Limit, + std::string &Failure) { + std::map Trials; + const std::string Dir = + leanProjectPath(leanProjectRoot(), {".cppverify", "automation"}); + if (std::error_code EC = llvm::sys::fs::create_directories(Dir)) { + Failure = "cannot create " + Dir + ": " + EC.message(); + return Trials; + } + const std::string Base = + leanProjectPath(Dir, {"try-" + std::to_string(Chunk)}); + const std::string Source = Base + ".lean", Report = Base + ".report", + Log = Base + ".log"; + auto leanString = [](llvm::StringRef Text) { + std::string Quoted = "\""; + for (char C : Text) { + if (C == '\\' || C == '"') + Quoted += '\\'; + Quoted += C; + } + return Quoted + "\""; + }; + const std::string ReportName = leanString(Report); + static const llvm::StringRef Foundations[] = {"propext", "Quot.sound", + "Classical.choice"}; + const std::string Limited = + Limit + ? " within " + std::to_string((Limit->count() + 999) / 1000) + " s" + : ""; + + for (size_t Next = 0; Next < Goals.size() && !interruptRequested();) { + std::string Text = "import CppVerify.User\nimport CppVerify.Auto\n\n" + "set_option cppverify.autoReport " + + ReportName + "\n#eval CppVerify.Auto.report " + + ReportName + " \"ready\"\n"; + for (size_t I = Next; I != Goals.size(); ++I) { + const LeanProjectGoal &Goal = *Goals[I]; + const std::string Name = "cppverify_try_" + std::to_string(I); + Text += "\ntheorem " + Name + " : " + Goal.Name + " := by\n apply " + + Goal.Name + ".of_readable\n"; + if (!Goal.Intros.empty()) + Text += " intro " + Goal.Intros + "\n"; + Text += " cppverify_auto\n#cppverify_axioms " + ReportName + " " + + Name + "\n"; + } + llvm::sys::fs::remove(Report); + if (llvm::Error Error = writeTextFile(Source, Text)) { + Failure = llvm::toString(std::move(Error)); + return Trials; + } + + std::vector Args = {Lean, "-DmaxErrors=1000000", + "-DElab.async=false", Source}; + std::vector Env(Environment.begin(), Environment.end()); + std::optional Redirects[] = { + llvm::StringRef(""), llvm::StringRef(Log), llvm::StringRef(Log)}; + std::string StartError; + bool StartFailed = false; + llvm::sys::ProcessInfo Process = llvm::sys::ExecuteNoWait( + Lean, Args, Env, Redirects, 0, &StartError, &StartFailed); + if (StartFailed || Process.Pid == llvm::sys::ProcessInfo::InvalidPid) { + Failure = "cannot start Lean: " + StartError; + return Trials; + } + + bool Started = false; + std::map Steps, Axioms; + size_t Parsed = 0; + auto readReport = [&] { + auto Buffer = llvm::MemoryBuffer::getFile(Report, /*IsText=*/false, + /*RequiresNullTerminator=*/ + false); + if (!Buffer) + return; + llvm::StringRef All = (*Buffer)->getBuffer(); + while (Parsed < All.size()) { + const size_t End = All.find('\n', Parsed); + if (End == llvm::StringRef::npos) + break; + llvm::StringRef Line = All.slice(Parsed, End).rtrim('\r'); + Parsed = End + 1; + if (Line == "ready") { + Started = true; + continue; + } + llvm::SmallVector Fields; + Line.split(Fields, '\t', 2); + size_t I; + if (Fields.size() != 3 || + !Fields[1].consume_front("cppverify_try_") || + Fields[1].getAsInteger(10, I)) + continue; + (Fields[0] == "step" ? Steps : Axioms)[I] = Fields[2].str(); + } + }; + + auto Progress = std::chrono::steady_clock::now(); + size_t Finished = 0; + std::optional Stopped; + bool TimedOut = false; + while (true) { + ChildPoll Poll = pollChild(Process, "Lean"); + readReport(); + if (Axioms.size() != Finished) { + Finished = Axioms.size(); + Progress = std::chrono::steady_clock::now(); + } + if (Poll.State != ChildState::Running) { + if (Poll.State == ChildState::Failed || Poll.ExitCode < 0) + Stopped = Poll.Error; + break; + } + std::string KillError; + if (interruptRequested()) { + terminateChild(Process, "Lean", KillError); + return Trials; + } + const auto Elapsed = std::chrono::steady_clock::now() - Progress; + if (!Started && Elapsed > std::chrono::minutes(2)) { + terminateChild(Process, "Lean", KillError); + Failure = "Lean did not load the project's modules within 2 minutes"; + return Trials; + } + if (Started && Limit && Elapsed > *Limit) { + terminateChild(Process, "Lean", KillError); + TimedOut = true; + break; + } + std::this_thread::sleep_for(std::chrono::milliseconds(20)); + } + if (!Started) { + auto Output = llvm::MemoryBuffer::getFile(Log); + Failure = + "Lean could not start on the goals" + + (Output && !(*Output)->getBuffer().trim().empty() + ? ": " + (*Output)->getBuffer().trim().take_front(300).str() + : std::string()); + return Trials; + } + + size_t I = Next; + for (; I != Goals.size() && Axioms.count(I); ++I) { + LeanTrial &Trial = Trials[Goals[I]->Name]; + llvm::SmallVector Used; + llvm::StringRef(Axioms[I]).split(Used, ',', -1, false); + const bool Foundational = + Axioms[I] != "missing" && + llvm::all_of(Used, [&](llvm::StringRef Axiom) { + return llvm::is_contained(Foundations, Axiom.trim()); + }); + auto Step = Steps.find(I); + if (Foundational && Step != Steps.end() && + llvm::is_contained(LeanAutomationSteps, Step->second)) + Trial.Step = Step->second; + else + Trial.Why = "did not prove it"; + } + if (I == Goals.size()) + break; + // The goal Lean was on when it stopped, or ran out of time. + Trials[Goals[I]->Name].Why = + TimedOut ? "did not prove it" + Limited + : "did not prove it: Lean stopped" + + (Stopped && !Stopped->empty() ? " (" + *Stopped + ")" + : std::string()); + Next = I + 1; + } + return Trials; + } + + // Each export's count of the goals cppverify_auto proves, from the proof + // files as they are now. + void countLeanAutomation(const std::vector &ProjectGoals) { + std::set Automatic; + for (const LeanProjectGoal &Goal : ProjectGoals) { + std::string File; + if (!Goal.Exported || Automatic.count(Goal.Name)) + continue; + if (std::optional Record = readLeanProof(leanProjectPath( + leanProjectRoot(), leanProofComponents(Goal, File)))) + if (Record->Automatic) + Automatic.insert(Goal.Name); + } + for (VerifyDiagnostic &Diagnostic : Diags) + if (Diagnostic.K == VerifyDiagnostic::Exported && Diagnostic.Result) + Diagnostic.LeanAutomatic = llvm::count_if( + std::set(Diagnostic.Result->LeanGoals.begin(), + Diagnostic.Result->LeanGoals.end()), + [&](const std::string &Goal) { return Automatic.count(Goal); }); + } + + // Tries cppverify_auto on each goal whose proof file is still the one + // cpp-verify wrote and that this revision has not tried, as Vermilion and + // Why3 run their automation when they generate goals, and writes what it + // finds: the step that proves the goal, or a stub that says it was tried. + // It runs the pinned toolchain; without it the stubs stay as they are. + void automateLeanProject(const std::vector &ProjectGoals) { + const std::string &Root = leanProjectRoot(); + std::map Unique; + for (const LeanProjectGoal &Goal : ProjectGoals) + if (Goal.Exported) + Unique.emplace(Goal.Name, &Goal); + auto pathOf = [&](const LeanProjectGoal &Goal) { + std::string File; + return leanProjectPath(Root, leanProofComponents(Goal, File)); + }; + std::vector Candidates; + for (const auto &[Name, Goal] : Unique) + if (std::optional Record = readLeanProof(pathOf(*Goal))) + if (Record->Pristine && !llvm::StringRef(Record->Automation) + .starts_with(leanAutomationTag())) + Candidates.push_back(Goal); + if (Candidates.empty() || interruptRequested()) + return; + + auto Launcher = leanLauncher(".cppverify-automation"); + if (!Launcher) { + llvm::consumeError(Launcher.takeError()); + return; + } + auto skipped = [&](const std::string &Why) { + Diags.push_back( + {VerifyDiagnostic::Warning, + "cppverify_auto was not tried on the new Lean goals: " + Why}); + }; + if (auto Build = Launcher->run( + {"build", "CppVerify.User", "CppVerify.Auto"}, "build", Root); + !Build) + return skipped( + "the project does not build (" + + llvm::StringRef(llvm::toString(Build.takeError())).rtrim().str() + + ")"); + auto Variables = Launcher->run({"env"}, "env", Root); + if (!Variables) + return skipped(llvm::toString(Variables.takeError())); + std::string Lean, LeanPath; + for (llvm::StringRef Rest = *Variables; !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + Line = Line.rtrim("\r"); + if (Line.consume_front("LEAN=")) + Lean = Line.str(); + else if (Line.consume_front("LEAN_PATH=")) + LeanPath = Line.str(); + } + if (Lean.empty() || LeanPath.empty()) + return skipped("lake env names no Lean or LEAN_PATH"); + const std::vector Environment = + childEnvironment("LEAN_PATH", LeanPath); + + const unsigned Jobs = leanJobs(Candidates.size()); + std::vector> Chunks(Jobs); + for (size_t I = 0; I != Candidates.size(); ++I) + Chunks[I % Jobs].push_back(Candidates[I]); + std::optional Limit; + if (Opts.LeanAutoTimeoutMs) + Limit = std::chrono::milliseconds(Opts.LeanAutoTimeoutMs); + std::vector> Results(Jobs); + std::vector Failures(Jobs); + { + std::vector Threads; + for (unsigned C = 0; C != Jobs; ++C) + Threads.emplace_back([&, C] { + Results[C] = + tryLeanGoals(Chunks[C], Lean, Environment, C, Limit, Failures[C]); + }); + for (std::thread &Thread : Threads) + Thread.join(); + } + + const std::string Tag = leanAutomationTag(); + for (const std::map &Result : Results) + for (const auto &[Name, Trial] : Result) { + const LeanProjectGoal &Goal = *Unique.at(Name); + const std::string Text = + Trial.Step.empty() + ? leanProofHeader(Goal, Tag + Trial.Why) + + leanProof(Goal.Name, Goal.Intros, "sorry") + : leanProofHeader(Goal, Tag + "proves it with " + Trial.Step, + /*Automatic=*/true) + + leanProof(Goal.Name, Goal.Intros, Trial.Step); + if (llvm::Error Error = writeTextFile(pathOf(Goal), Text)) + Failures.push_back(llvm::toString(std::move(Error))); + } + std::set Reported; + for (const std::string &Failure : Failures) + if (!Failure.empty() && Reported.insert(Failure).second) + Diags.push_back({VerifyDiagnostic::Warning, + "cppverify_auto stopped before every new Lean goal " + "was tried: " + + Failure}); + } + void checkCalleeRecommendsOnFailure(const VFunction &Caller, const FunctionMap &FnMap, VerifyBackend &Backend) { @@ -2114,6 +2532,13 @@ class Verifier { "--lean-fallback"}); return false; } + if (!Opts.LeanAuto && Opts.LeanProjectPath.empty() && + Opts.LeanFallbackProjectPath.empty()) { + Diags.push_back({VerifyDiagnostic::Error, + "--no-lean-auto requires --lean-project or " + "--lean-fallback"}); + return false; + } if (Opts.LowerOnly && Opts.Backend == BackendKind::Lean) { Diags.push_back( {VerifyDiagnostic::Error, @@ -2121,11 +2546,15 @@ class Verifier { "--backend=lean to validate Lean export"}); return false; } - if (Opts.Backend == BackendKind::Lean && - (Opts.Jobs != 1 || !Opts.ProofCachePath.empty())) { - Diags.push_back( - {VerifyDiagnostic::Error, - "--jobs and --proof-cache are not supported by the Lean backend"}); + if (Opts.Backend == BackendKind::Lean && !Opts.ProofCachePath.empty()) { + Diags.push_back({VerifyDiagnostic::Error, + "--proof-cache is not supported by the Lean backend"}); + return false; + } + if (Opts.Backend == BackendKind::Lean && Opts.Jobs != 1) { + Diags.push_back({VerifyDiagnostic::Error, + "the Lean backend exports one function at a time; " + "LeanJobs sets its Lean processes"}); return false; } if (Opts.Backend == BackendKind::CVC5 && !Opts.ProofCachePath.empty()) { @@ -3726,14 +4155,18 @@ class Verifier { std::vector ExportedGoals; llvm::copy_if(LeanProjectGoals, std::back_inserter(ExportedGoals), [](const LeanProjectGoal &Goal) { return Goal.Exported; }); - if (llvm::Error Error = finalizeLeanProject( - LeanProjectGoals, - LeanFallbackBackend ? &LeanRunGroups : nullptr)) { + llvm::Error Finalized = finalizeLeanProject( + LeanProjectGoals, LeanFallbackBackend ? &LeanRunGroups : nullptr); + if (!Finalized && Opts.LeanAuto) + automateLeanProject(LeanProjectGoals); + if (!Finalized) + countLeanAutomation(LeanProjectGoals); + if (Finalized) { AllOk = false; AnyFailed = true; Diags.push_back({VerifyDiagnostic::Error, "cannot finalize Lean project (" + - llvm::toString(std::move(Error)) + ")"}); + llvm::toString(std::move(Finalized)) + ")"}); } else if (Opts.LeanCertify && !interruptRequested() && (!ExportedGoals.empty() || Opts.LeanFallbackProjectPath.empty())) { @@ -4507,6 +4940,8 @@ class Verifier { Callers.push_back(jsonText(Name)); Record["unverified_callers"] = std::move(Callers); } + if (D.K == VerifyDiagnostic::Exported && D.LeanAutomatic) + Record["lean_automatic"] = static_cast(D.LeanAutomatic); if (D.Result) { const VerifyResult &Result = *D.Result; if (!Result.BackendName.empty()) @@ -4699,7 +5134,14 @@ class Verifier { OS << "BoundedSafe: " << D.Message << "\n"; break; case VerifyDiagnostic::Exported: - OS << "Exported: " << D.Message << "\n"; + OS << "Exported: " << D.Message; + if (D.LeanAutomatic && D.Result) + OS << " (cppverify_auto proved " << D.LeanAutomatic << " of " + << std::set(D.Result->LeanGoals.begin(), + D.Result->LeanGoals.end()) + .size() + << " goals)"; + OS << "\n"; break; case VerifyDiagnostic::Certified: OS << "Certified: " << D.Message << "\n"; diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 09bd4dfaf5..887f375853 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -11,6 +11,8 @@ class ASTContext; namespace verify { inline constexpr unsigned DefaultSolverTimeoutMs = 30000; +/// cppverify_auto proves 99.8% of the suite's goals it proves within 5 s. +inline constexpr unsigned DefaultLeanAutoTimeoutMs = 20000; /// Twice the default: collection theories need more search. inline constexpr unsigned DefaultCollectionTimeoutMs = 2 * DefaultSolverTimeoutMs; @@ -40,6 +42,13 @@ struct VerifyOptions { bool LeanCertify = false; /// Delete the proofs a Lean project keeps in Stale/ once regenerated. bool LeanPruneStale = false; + /// Try cppverify_auto on each new goal of a Lean project, each for at most + /// LeanAutoTimeoutMs of wall-clock time (0: no limit). + bool LeanAuto = true; + unsigned LeanAutoTimeoutMs = DefaultLeanAutoTimeoutMs; + /// The Lean processes automation and certification run at once (0: the + /// available physical cores). + unsigned LeanJobs = 0; unsigned BMCUnroll = 10; /// Per-query solver timeout in milliseconds; 0 disables it. Non-terminating /// queries return Unknown instead of hanging the tool. diff --git a/clang/test/Verify/suite/Inputs/lean_automation.cpp b/clang/test/Verify/suite/Inputs/lean_automation.cpp new file mode 100644 index 0000000000..ae49bd4000 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_automation.cpp @@ -0,0 +1,20 @@ +unsigned a_slow() + cppverify::post(cppverify::result == 0) +{ + unsigned u = 2; + return u << 31; +} + +int next(int x) + cppverify::pre(x >= 0 && x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +int square(int x) + cppverify::pre(x >= 0 && x < 1000) + cppverify::post(cppverify::result >= 0) +{ + return x * x; +} diff --git a/clang/test/Verify/suite/Inputs/lean_automation_user.lean b/clang/test/Verify/suite/Inputs/lean_automation_user.lean new file mode 100644 index 0000000000..05b8fffa9b --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_automation_user.lean @@ -0,0 +1,5 @@ +import CppVerify.Generated + +/- An unfinished lemma, which grind would use. -/ +@[grind =] theorem cheat (x y : BitVec 32) : BitVec.saddOverflow x y = false := by + sorry diff --git a/clang/test/Verify/suite/backend_execution.test b/clang/test/Verify/suite/backend_execution.test index 8e3e04a054..76370c4652 100644 --- a/clang/test/Verify/suite/backend_execution.test +++ b/clang/test/Verify/suite/backend_execution.test @@ -42,8 +42,8 @@ # RUN: %python -c "from pathlib import Path; Path(r'%t.not-directory').write_text('x')" # RUN: not %cpp-verify --proof-cache=%t.not-directory \ # RUN: %S/Inputs/backend_cache_base.cpp -- 2>&1 | FileCheck %s --check-prefix=CACHE-IO -# RUN: not %cpp-verify --backend=lean --jobs=2 \ -# RUN: %S/Inputs/backend_cache_base.cpp -- 2>&1 | FileCheck %s --check-prefix=LEAN-JOBS +# RUN: not %cpp-verify --backend=lean --proof-cache=%t.lean-cache \ +# RUN: %S/Inputs/backend_cache_base.cpp -- 2>&1 | FileCheck %s --check-prefix=LEAN-CACHE # RUN: not %cpp-verify --lower-only --proof-cache=%t.lower-cache \ # RUN: %S/Inputs/backend_cache_base.cpp -- 2>&1 | FileCheck %s --check-prefix=LOWER-CACHE # @@ -115,7 +115,7 @@ # CACHE-IO-SAME: [reason=cache.io-failed] # CACHE-IO-SAME: proof cache path is not a directory -# LEAN-JOBS: error: --jobs and --proof-cache are not supported by the Lean backend +# LEAN-CACHE: error: --proof-cache is not supported by the Lean backend # LOWER-CACHE: error: --proof-cache cannot be combined with --lower-only # REPLAY: Proved obligations: cached_identity (dependencies not checked in replay) [backend=z3] [cache=[[RN:[1-9][0-9]*]]/[[RN]]] diff --git a/clang/test/Verify/suite/lean_automation.test b/clang/test/Verify/suite/lean_automation.test new file mode 100644 index 0000000000..0862d09576 --- /dev/null +++ b/clang/test/Verify/suite/lean_automation.test @@ -0,0 +1,95 @@ +# REQUIRES: lean +# +# cppverify_auto is tried once on each new goal of a Lean project: a goal it +# proves gets that proof, any other a stub that says it was tried. Its proofs +# are certified like any other, and a file cpp-verify wrote is rewritten only +# while nobody edited it. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-auto-timeout=3000 --jobs=1 %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean --check-prefix=PROVED +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean --check-prefix=STUB +# The goal after one that takes too long is still tried. +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_a_slow_989093/cppverify_a_slow_989093_postcondition_1555cfbf.lean --check-prefix=SLOW +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --diagnostics-format=json %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=JSON +# +# Certification checks the automatic proofs like any other. +# RUN: not %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# +# No goal is new, so nothing is tried again. +# RUN: rm -rf %t/p/.cppverify/automation +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: not test -e %t/p/.cppverify/automation +# +# An edited proof is the user's, kept as it is; it may use cppverify_auto. +# RUN: sed -i 's/^ cppverify_auto_grind$/ cppverify_auto/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EDITED +# RUN: grep -qx ' cppverify_auto' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean +# +# A stub that no revision of cppverify_auto tried, as before automation, and +# one an earlier revision tried, are tried. +# RUN: sed -i -e '/^ automation:/d' -e '/^import CppVerify.Auto$/d' -e 's/^ cppverify_auto_grind$/ sorry/' %t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean +# RUN: sed -i 's/cppverify_auto 1 did not prove it/cppverify_auto 0 did not prove it/' %t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EDITED +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_missing_return_54ae7c80.lean --check-prefix=TRIED +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_square_934e38/cppverify_square_934e38_overflow_f86973f7.lean --check-prefix=STUB +# RUN: not %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# +# A step that proves a goal with a lemma the user has not proved does not +# count; the next step, which proves it honestly, does. +# RUN: mkdir -p %t/u/CppVerify && cp %S/Inputs/lean_automation_user.lean %t/u/CppVerify/User.lean +# RUN: %cpp-verify --backend=lean --lean-project=%t/u --lean-auto-timeout=3000 --jobs=2 %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/u/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_overflow_fd7a6390.lean --check-prefix=HONEST +# +# Without automation every new goal gets a stub. +# RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/q %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=PLAIN --implicit-check-not=cppverify_auto +# RUN: not grep -r -l 'automation:' %t/q/CppVerify/Proofs +# RUN: grep -c -x ' sorry' %t/q/CppVerify/Proofs/cppverify_next_e1e917/cppverify_next_e1e917_postcondition_506f384e.lean +# +# Both options belong to a Lean project. +# RUN: not %cpp-verify --no-lean-auto %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=NO-PROJECT +# RUN: not %cpp-verify --lean-auto-timeout=1000 %S/Inputs/lean_automation.cpp -- 2>&1 | FileCheck %s --check-prefix=NO-PROJECT-TIMEOUT + +# EXPORT: Exported: lean obligation: a_slow (cppverify_auto proved 2 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: next (cppverify_auto proved 3 of 3 goals) +# EXPORT-NEXT: Exported: lean obligation: square (cppverify_auto proved 1 of 3 goals) + +# PROVED: automation: cppverify_auto 1 proves it with cppverify_auto_grind +# PROVED-NEXT: cppverify_auto proves this goal. cpp-verify rewrites this file only while it +# PROVED-NEXT: is unedited; a proof you write here is yours, kept as any other. -/ +# PROVED-NEXT: import CppVerify.User +# PROVED-NEXT: import CppVerify.Auto +# PROVED-EMPTY: +# PROVED-NEXT: theorem cppverify_next_e1e917_postcondition_506f384e_proof : cppverify_next_e1e917_postcondition_506f384e := by +# PROVED-NEXT: apply cppverify_next_e1e917_postcondition_506f384e.of_readable +# PROVED-NEXT: intro __heap_alloc_0 __heap_live_0 __result_1 x_0 h_pre_1 h_null_1 h_null_2 h_exact_1 h_exact_2 h_result_1 +# PROVED-NEXT: cppverify_auto_grind +# PROVED-EMPTY: + +# STUB: automation: cppverify_auto 1 did not prove it{{$}} +# STUB-NEXT: Complete this proof. +# STUB: {{^}} sorry{{$}} + +# SLOW: automation: cppverify_auto 1 did not prove it within 3 s +# SLOW: {{^}} sorry{{$}} + +# JSON: "function":"next","lean_automatic":3,{{.*}}"status":"exported" + +# CERTIFY: Unresolved: lean obligation: a_slow (Lean certification failed: the proof of {{.*}}::postcondition@2:37: {{.*}}declaration uses `sorry` +# CERTIFY-NEXT: Certified: next [backend=Lean] +# CERTIFY-NEXT: Unresolved: lean obligation: square (Lean certification failed: the proof of {{.*}}::overflow@19:3: {{.*}}declaration uses `sorry` + +# EDITED: Exported: lean obligation: next (cppverify_auto proved 2 of 3 goals) + +# TRIED: automation: cppverify_auto 1 proves it with cppverify_auto_grind +# TRIED: {{^}} cppverify_auto_grind{{$}} + +# HONEST: automation: cppverify_auto 1 proves it with cppverify_auto_heap +# HONEST: {{^}} cppverify_auto_heap{{$}} + +# PLAIN: Exported: lean obligation: a_slow{{$}} +# PLAIN-NEXT: Exported: lean obligation: next{{$}} +# PLAIN-NEXT: Exported: lean obligation: square{{$}} + +# NO-PROJECT: --no-lean-auto requires --lean-project or --lean-fallback +# NO-PROJECT-TIMEOUT: --lean-auto-timeout requires --lean-project or --lean-fallback diff --git a/clang/test/Verify/suite/lean_certifier.test b/clang/test/Verify/suite/lean_certifier.test index 1990b479e6..b738cacb2d 100644 --- a/clang/test/Verify/suite/lean_certifier.test +++ b/clang/test/Verify/suite/lean_certifier.test @@ -47,7 +47,7 @@ # EXPORT-NEXT: Exported: lean obligation: one # SORRY: Certified: fine [backend=Lean] -# SORRY-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: command failed with exit code 1: {{.*}}cppverify_one_99bcee_postcondition_646d2761.lean:11:8: error: declaration uses `sorry`) +# SORRY-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: command failed with exit code 1: {{.*}}cppverify_one_99bcee_postcondition_646d2761.lean:{{[0-9]+}}:8: error: declaration uses `sorry`) # REWRITTEN: Certified: fine [backend=Lean] # REWRITTEN-NEXT: Unresolved: lean obligation: one (Lean certification failed: the proof of fn_5f5a336f6e6576::postcondition@8:37: cppverify_one_99bcee_postcondition_646d2761_proof proves True, not cppverify_one_99bcee_postcondition_646d2761) diff --git a/clang/test/Verify/suite/lean_certify.cpp b/clang/test/Verify/suite/lean_certify.cpp index 0a2532b383..2cd5205c70 100644 --- a/clang/test/Verify/suite/lean_certify.cpp +++ b/clang/test/Verify/suite/lean_certify.cpp @@ -1,24 +1,24 @@ // REQUIRES: lean // // RUN: rm -rf %t.admitted %t.certified %t.axiom %t.stale -// RUN: not %cpp-verify --backend=lean --lean-project=%t.admitted --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=ADMITTED +// RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.admitted --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=ADMITTED // -// RUN: %cpp-verify --backend=lean --lean-project=%t.certified %s -- +// RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.certified %s -- // RUN: sed -i.orig 's/ sorry/ trivial/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean // RUN: sed -i.orig 's/ sorry/ trivial/' %t.certified/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_postcondition_ba8abb90.lean -// RUN: %cpp-verify --backend=lean --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED +// RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED // RUN: echo 'theorem unfinished : True := by sorry' >> %t.certified/CppVerify/User.lean -// RUN: not %cpp-verify --backend=lean --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=USER-ADMITTED +// RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.certified --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=USER-ADMITTED // -// RUN: %cpp-verify --backend=lean --lean-project=%t.axiom %s -- +// RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.axiom %s -- // RUN: echo 'axiom escape {p : Prop} : p' >> %t.axiom/CppVerify/User.lean // RUN: sed -i.orig 's/ sorry/ exact escape/' %t.axiom/CppVerify/Proofs/*/*.lean -// RUN: not %cpp-verify --backend=lean --lean-project=%t.axiom --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=AXIOM +// RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.axiom --lean-certify %s -- 2>&1 | FileCheck %s --check-prefix=AXIOM // -// RUN: %cpp-verify --backend=lean --lean-project=%t.stale %s -- +// RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.stale %s -- // RUN: sed -i.orig 's/ sorry/ trivial/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_missing_return_ba8abb90.lean // RUN: sed -i.orig 's/ sorry/ trivial/' %t.stale/CppVerify/Proofs/cppverify_trivial_3e4f5a/cppverify_trivial_3e4f5a_postcondition_ba8abb90.lean -// RUN: not %cpp-verify --backend=lean --lean-project=%t.stale --lean-certify %S/Inputs/lean_certify_stale.cpp -- 2>&1 | FileCheck %s --check-prefix=STALE +// RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.stale --lean-certify %S/Inputs/lean_certify_stale.cpp -- 2>&1 | FileCheck %s --check-prefix=STALE void trivial() cppverify::post(true) diff --git a/clang/test/Verify/suite/lean_dependencies.test b/clang/test/Verify/suite/lean_dependencies.test index d238f92634..4bab2a7032 100644 --- a/clang/test/Verify/suite/lean_dependencies.test +++ b/clang/test/Verify/suite/lean_dependencies.test @@ -9,24 +9,24 @@ # # The Lean backend, with every goal proved. An export proves nothing, so it # runs no vacuity check. -# RUN: %cpp-verify --backend=lean --lean-project=%t.backend %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND-EXPORT +# RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.backend %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND-EXPORT # RUN: sed -i.orig 's/^ sorry$/ trivial/' %t.backend/CppVerify/Proofs/*/*.lean # RUN: cp %S/Inputs/lean_dependencies_seven.lean %t.backend/CppVerify/Proofs/cppverify_seven_634ea3/cppverify_seven_634ea3_postcondition_f0d135e6.lean # RUN: cp %S/Inputs/lean_dependencies_trusting.lean %t.backend/CppVerify/Proofs/cppverify_trusting_b6301a/cppverify_trusting_b6301a_postcondition_bafafdfb.lean # RUN: cp %S/Inputs/lean_dependencies_impossible.lean %t.backend/CppVerify/Proofs/cppverify_impossible_9d6c7c/cppverify_impossible_9d6c7c_postcondition_1cd35301.lean # RUN: cp %S/Inputs/lean_dependencies_same.lean %t.backend/CppVerify/Proofs/cppverify_same_9601c2/cppverify_same_9601c2_postcondition_ce92acf8.lean # RUN: cp %S/Inputs/lean_dependencies_positive.lean %t.backend/CppVerify/Proofs/cppverify_positive_fb6abf/cppverify_positive_fb6abf_postcondition_78bdd643.lean -# RUN: not %cpp-verify --backend=lean --lean-project=%t.backend --lean-certify %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND -# RUN: not %cpp-verify --backend=lean --lean-project=%t.backend --lean-certify --diagnostics-format=json %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND-JSON +# RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.backend --lean-certify %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND +# RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.backend --lean-certify --diagnostics-format=json %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BACKEND-JSON # # The same project with an admitted lemma: nothing is certified, and what the # vacuity checks found goes with the verdicts. # RUN: echo 'theorem admitted : True := by sorry' >> %t.backend/CppVerify/User.lean -# RUN: not %cpp-verify --backend=lean --lean-project=%t.backend --lean-certify %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BROKEN +# RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.backend --lean-certify %S/Inputs/lean_dependencies_backend.cpp -- 2>&1 | FileCheck %s --check-prefix=BROKEN # # A generated check that is quiet when proved is reported when certification # fails. -# RUN: not %cpp-verify --backend=lean --lean-project=%t.inductive --lean-certify %S/Inputs/inductive_unproved.cpp -- 2>&1 | FileCheck %s --check-prefix=INDUCTIVE +# RUN: not %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.inductive --lean-certify %S/Inputs/inductive_unproved.cpp -- 2>&1 | FileCheck %s --check-prefix=INDUCTIVE # # A spec's termination proved in Lean, beside a function that fails: first # with the proof left as sorry, then completed. diff --git a/clang/test/Verify/suite/lean_fallback_partial.test b/clang/test/Verify/suite/lean_fallback_partial.test index 1b7bc677fd..e8b4c5a2de 100644 --- a/clang/test/Verify/suite/lean_fallback_partial.test +++ b/clang/test/Verify/suite/lean_fallback_partial.test @@ -11,7 +11,7 @@ # RUN: cp %S/Inputs/lean_fallback_partial_goal_2.lean %t.project/CppVerify/Proofs/cppverify_bump_ce87d1/cppverify_bump_ce87d1_assertion_06404a7a.lean # RUN: %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-certify %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=MIXED # RUN: %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-certify --diagnostics-format=json %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=MIXED-JSON -# RUN: not %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-fallback-scope=all --lean-certify %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=ALL +# RUN: %cpp-verify --solver-rlimit=100 --lean-fallback=%t.project --lean-fallback-scope=all --lean-certify %S/Inputs/lean_fallback_partial.cpp -- 2>&1 | FileCheck %s --check-prefix=ALL # EXPORT: Exported: lean fallback: bump [z3: 1 of 3 proved; lean: 2 exported] # EXPORT: Unresolved: bump [backend=z3] [reason=solver.resource-limit] @@ -26,6 +26,6 @@ # MIXED-JSON-SAME: "evidence":{"lean":["{{.*}}::overflow@5:3","{{.*}}::assertion@6:3"],"solver":"z3","solver_proved":1,"total":3} # MIXED-JSON-SAME: "status":"mixed-proof" -# The complete export includes the return check, whose proof is still `sorry`. -# ALL: Unresolved: lean fallback: bump [z3: 1 of 3 proved; lean: 3 exported] (Lean certification failed: -# ALL-SAME: declaration uses `sorry` +# The complete export includes the return check, which cppverify_auto proves, so +# Lean checks every obligation. +# ALL: Certified: bump [backend=Lean] diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp index 875879ec0b..8227146516 100644 --- a/clang/test/Verify/suite/lean_readable.cpp +++ b/clang/test/Verify/suite/lean_readable.cpp @@ -6,7 +6,7 @@ // it. // // RUN: rm -rf %t && mkdir -p %t -// RUN: %cpp-verify --backend=lean --lean-project=%t/p %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT +// RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t/p %s -- 2>&1 | FileCheck %s --check-prefix=EXPORT // RUN: FileCheck %s --input-file=%t/p/CppVerify/Generated.lean // RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_twice_edf933/cppverify_twice_edf933_postcondition_28de726e.lean --check-prefix=STUB // RUN: FileCheck %s --input-file=%t/p/CppVerify/Proofs/cppverify_poly_c94108/cppverify_poly_c94108_postcondition_fde367c1.lean --check-prefix=LETS diff --git a/clang/test/Verify/suite/lean_toolchain.test b/clang/test/Verify/suite/lean_toolchain.test index d9c30df96e..306038ccee 100644 --- a/clang/test/Verify/suite/lean_toolchain.test +++ b/clang/test/Verify/suite/lean_toolchain.test @@ -4,7 +4,9 @@ # # UNSUPPORTED: system-windows # RUN: rm -rf %t %t.project && mkdir -p %t/elan %t/plain -# RUN: %cpp-verify --backend=lean --lean-project=%t.project %S/Inputs/lean_toolchain.cpp -- +# Without automation at export, the goal is new to cppverify_auto whether or +# not Lean is installed, so the certification run below tries it first. +# RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.project %S/Inputs/lean_toolchain.cpp -- # # A fake elan, with lake as its proxy, records what it is asked. # RUN: printf '#!/bin/sh\necho "$*" >> %t/elan.log\ncase "$*" in *--version*) echo "Lake version 5.0.0 (Lean version 4.35.0)";; *) exit 1;; esac\n' > %t/elan/elan @@ -18,7 +20,10 @@ # ELAN: Unresolved: lean obligation: trivial (Lean certification failed: command failed with exit code 1 +# The trial of cppverify_auto, then certification, each with the pin. # ELAN-LOG: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} -# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User{{$}} +# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.User CppVerify.Auto{{$}} +# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} +# ELAN-LOG-NEXT: {{^}}+leanprover/lean4:v4.35.0 --dir={{.*}}.project build CppVerify.Generated CppVerify.User CppVerify.Auto{{$}} # PLAIN: Unresolved: lean obligation: trivial (Lean certification failed: the project pins leanprover/lean4:v4.35.0, but [[DIR]]/lake runs Lean 4.1.0; install elan (https://github.com/leanprover/elan), which runs the pinned toolchain) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index d4c6f0b8f2..7c27e2f10d 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -98,6 +98,18 @@ static cl::opt LeanPruneStale( "goal has their statement"), cl::init(false), cl::cat(CppVerifyCategory)); +static cl::opt + NoLeanAuto("no-lean-auto", + cl::desc("Write a stub for each new Lean goal without trying " + "cppverify_auto on it"), + cl::init(false), cl::cat(CppVerifyCategory)); + +static cl::opt LeanAutoTimeout( + "lean-auto-timeout", + cl::desc("Wall-clock milliseconds cppverify_auto may spend on one new " + "Lean goal (0 = no limit)"), + cl::init(verify::DefaultLeanAutoTimeoutMs), cl::cat(CppVerifyCategory)); + static cl::opt BMCUnroll("unroll", cl::desc("Maximum loop unroll bound for --backend=bmc"), cl::init(10), cl::cat(CppVerifyCategory)); @@ -340,13 +352,17 @@ class VerifyConsumer : public ASTConsumer { VOpts.LeanScope = LeanFallbackScope.getValue(); VOpts.LeanCertify = LeanCertify.getValue(); VOpts.LeanPruneStale = LeanPruneStale.getValue(); + VOpts.LeanAuto = !NoLeanAuto.getValue(); + VOpts.LeanAutoTimeoutMs = LeanAutoTimeout.getValue(); + VOpts.LeanJobs = Jobs.getNumOccurrences() ? Jobs.getValue() : 0; VOpts.BMCUnroll = BMCUnroll.getValue(); VOpts.SolverTimeoutMs = SolverTimeout.getValue(); VOpts.CollectionTimeoutMs = collectionTimeoutMs(); VOpts.CertifyTimeoutMs = certifyTimeoutMs(); VOpts.FunctionTimeoutMs = functionTimeoutMs(); VOpts.SolverResourceLimit = SolverResourceLimit.getValue(); - VOpts.Jobs = jobs(); + // Lean exports one function at a time; --jobs sets its Lean processes. + VOpts.Jobs = VOpts.Backend == verify::BackendKind::Lean ? 1 : jobs(); VOpts.MaxQueryNodes = MaxQueryNodes.getValue(); VOpts.IntegerEncoding = IntEncoding.getValue(); VOpts.CVC5Path = CVC5Path.getValue(); @@ -585,6 +601,9 @@ static bool resolveOptions(bool Replay) { Error = "--unroll requires --backend=bmc"; else if (given(LeanFallbackScope) && LeanFallback.empty()) Error = "--lean-fallback-scope requires --lean-fallback"; + else if (given(LeanAutoTimeout) && LeanProject.empty() && + LeanFallback.empty()) + Error = "--lean-auto-timeout requires --lean-project or --lean-fallback"; else if ((given(ProofCacheMaxMB) || given(ProofCacheMaxEntries)) && ProofCache.empty()) Error = "--proof-cache-max-mb and --proof-cache-max-entries require " @@ -614,7 +633,7 @@ static int replayObligationArchive() { return 1; } if (!LeanProject.empty() || !LeanFallback.empty() || LeanCertify || - LeanPruneStale) { + LeanPruneStale || NoLeanAuto || LeanAutoTimeout.getNumOccurrences()) { llvm::errs() << "error: archive replay supports Lean scratch-pad export " "with --lean-out, not Lean project generation or " "certification\n"; diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 63850c94f7..a4b444b589 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1641,19 +1641,60 @@ uses when the source around it changes. stub its `intro` list. On the 375 suite exports, the 351 that built before still build, with every bridge. -- **Certification** (`certifyLeanProject`) builds `Generated` and `User`, - then each proof file with `lean -EhasSorry`, recording the goals whose - proofs do not build, and runs the checker of `LeanCertifier.h`, written - into the project as `.cppverify/Certify.lean`, with `lake env lean --run` - over the goals that built. The checker elaborates none of the user's - source, so their macros and commands cannot change what it checks. For each - goal it imports the proof module (never freeing imported data, which a - later import in the process reads), checks that `G_proof` is a theorem of - type exactly `.const G []` with `G` a definition of `CppVerify.Generated`, - collects its axioms by walking the kernel constants it uses, and replays - through the kernel (as `leanchecker`'s `replayFromImports`) every module of - the import closure whose `.olean` lies outside the toolchain, each once in - a run. It prints `ok` or `fail` with the reason per goal. Each Lean result +- **Automation** (`automateLeanProject`, after `finalizeLeanProject`). Every + export writes `CppVerify/Auto.lean` (`LeanAutomation.h`): the tactic + `cppverify_auto`, a ladder of steps (`cppverify_auto_grind`, `_heap`, + `_bv`, `_decide`, `_simp`) as Vermilion's discharger is, each run with a + fresh heartbeat budget (`cppverify.autoBudget`, 50000), counting only when + it closes the goal with a proof whose axioms are Lean's foundations + (`collectAxioms` of every constant it uses), and rolled back otherwise, + runtime exceptions included. Each step first unfolds a goal left as its + readable form (one without binders); `_heap` turns every `heapStore*` + equation into the function it defines and substitutes it; `_bv` and + `_heap` rewrite the machine comparisons, constants, and overflow + predicates into integer facts before `grind`. The steps and their order + come from a probe of every goal the suite exports (9830): of the 5740 that + Z3 proves, they prove 90.2%. Stating the range of every `BitVec.toInt` + term first proved nothing more (`grind` knows the ranges), and removing + `Int.bmod` with an `omega` discharger proved 32 fewer and took longer, so + neither is a step. Heartbeats alone did not bound the time, since a kernel + check is not counted. The trial takes every exported goal whose proof file + is pristine and whose header (`automation:`) names no attempt by the + current `LeanAutomationRevision`, builds `User` and `Auto` with the pinned + toolchain, and runs `lean` itself (with the `LEAN_PATH` of `lake env`, so a + stopped process leaves no child) on a file of one theorem per goal, in + `--jobs` chunks. Lean reports to a file, line by line: the step that + proved each goal, then the axioms of its theorem or that the kernel + rejected it (its messages, written by a thread of its own, are buffered and + lost when it is stopped). A goal that takes longer than + `--lean-auto-timeout`, or stops Lean, is not proved, and the goals after it + start again in a new process. Each goal then gets the step that proved it + (an automatic proof, pristine like a stub) or a stub whose header records + the attempt. An export's `LeanAutomatic` counts its goals with automatic + proofs. Without the toolchain nothing is tried. +- **Certification** (`certifyLeanProject`) builds `Generated`, `User`, and + `Auto`, then each proof file with `lean -EhasSorry`, `--jobs` at once, + recording the goals whose proofs do not build, and runs the checker of + `LeanCertifier.h`, written into the project as `.cppverify/Certify.lean`, + with `lake env lean --run` over the goals that built. The checker + elaborates none of the user's source, so their macros and commands cannot + change what it checks. It first checks every goal in one environment: all + proof modules imported at once, and the constants of every module of the + project replayed together through the kernel into the environment of the + toolchain modules they import (a constant two modules declare, as an + equation lemma derived in each, must be the same). A check reads only + kernel constants, so proofs imported together cannot change each other's + checks; an automatic proof imports `Lean`, whose import each goal would + repeat (33 goals took 161 s, now 8 s). If that import or replay fails, as a + proof file that declares a goal's name or a module the kernel rejects + makes it, each goal is checked on its own: it imports the proof module + (never freeing imported data, which a later import in the process reads), + and every module of the import closure whose `.olean` lies outside the + toolchain is replayed (as `leanchecker`'s `replayFromImports`), each once + in a run. Either way it checks that `G_proof` is a theorem of type exactly + `.const G []` with `G` a definition of `CppVerify.Generated`, collects its + axioms by walking the kernel constants it uses, and prints `ok` or `fail` + with the reason per goal. Each Lean result records its goals (`VerifyResult::LeanGoals`), and a function is `Certified` only when all of them pass; a failure names the obligation. Before 0.2 certification parsed what `Check.lean` printed, which imports @@ -1666,7 +1707,12 @@ proof that does not build, and an axiom behind a lemma, with a function whose proofs are sound certified beside each. `lean_readable.cpp` checks the readable form of each kind of assumption, the bridge, the stubs (every one builds), a proof by hypothesis names that certifies, and a readable form that says less than its goal, which fails at -its bridge. `lean_identity.test` walks one project through each case (insertion and +its bridge. `lean_automation.test` checks what an export writes (an automatic +proof, a stub that records the attempt, a goal stopped at the time limit with +the goals after it still tried), certification of both, that nothing is +tried again, that an edited proof is kept, that a stub of no attempt or an +earlier revision's is tried, that a step proving a goal with the user's +unfinished lemma does not count, and `--no-lean-auto`. `lean_identity.test` walks one project through each case (insertion and reordering, renames of two functions at once, a changed statement, a removed function and its return, fallback runs, pruning, and a 0.1 project with proofs, stubs, and a proof of a goal that is gone) and certifies it after diff --git a/docs/DESIGN.md b/docs/DESIGN.md index acd1c9b7e9..cf30c31656 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1930,7 +1930,21 @@ Vermilion names its hypotheses), and a bridge `G.of_readable : G.readable → G`, generated and kernel-checked with the generated file: the canonical goal stays what certification checks and identity hashes, and a printer bug in the readable form cannot certify anything. A stub applies the bridge and -introduces every name. Initial generation is `Exported`. Certification +introduces every name. Each new goal is first given to `cppverify_auto`, a +tactic of the generated `CppVerify/Auto.lean`, with the pinned toolchain when +it is installed, as Vermilion, Why3, and Frama-C's WP run their automation +before a goal reaches the user: a ladder of steps (`grind`; memory stores as +the functions they define and machine arithmetic as integers, then `grind`; +`decide`; `simp_all`), each with a heartbeat budget of its own and a +wall-clock limit per goal (`--lean-auto-timeout`), since heartbeats do not +bound a kernel check. A step counts only when it closes the goal with a proof +whose axioms are Lean's foundations, so the user's unfinished lemma never +proves a goal, and a goal counts as proved only when the kernel accepted its +theorem. A goal it proves gets that proof, which certification checks like +any other; any other gets a stub that records the attempt and the revision of +`cppverify_auto` that made it. A file is tried again only when no attempt by +the current revision is recorded, and only while nobody has edited it. +Initial generation is `Exported`. Certification holds against a proof author in bad faith. It compiles the user module and each proof file on its own with `sorry` as an error, then runs a checker (`LeanCertifier.h`) on the compiled modules, which elaborates none of the diff --git a/website/scripts/check-doc-examples.py b/website/scripts/check-doc-examples.py index 2c48ef57d4..2d7fa3122d 100644 --- a/website/scripts/check-doc-examples.py +++ b/website/scripts/check-doc-examples.py @@ -13,7 +13,9 @@ .. cppverify-example: with NAME ... compiled after the named blocks .. cppverify-example: after compiled after every earlier block of the page that compiled - .. cppverify-example: flags ARGS extra cpp-verify arguments + .. cppverify-example: flags ARGS extra cpp-verify arguments, in + which {dir} is a directory of + the example's own .. cppverify-example: fails NAME ... these functions fail with a counterexample .. cppverify-example: unresolved NAME ... @@ -174,6 +176,7 @@ def run(cpp_verify, source, arguments, timeout): with tempfile.TemporaryDirectory() as directory: path = pathlib.Path(directory) / "example.cpp" path.write_text(source) + arguments = [a.replace("{dir}", directory) for a in arguments] try: done = subprocess.run([cpp_verify, *arguments, str(path), "--"], capture_output=True, text=True, @@ -205,9 +208,11 @@ def check(cpp_verify, job): f"print:\n" + "\n".join(f" {line}" for line in missing) + f"\nactual output:\n{output.strip()[:2500]}"), False return None - code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300) - if code is None or code != 0 or "error:" in output: - return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False + # A Lean export compiles the example itself; it has no lowering of its own. + if "--backend=lean" not in arguments: + code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300) + if code is None or code != 0 or "error:" in output: + return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False code, output = run(cpp_verify, source, [f"--jobs={SOLVER_JOBS}", *arguments], 900) if code is None: 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 b45d9cd41e..032f7b26aa 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -156,11 +156,13 @@ For an explicit interactive proof: # complete proof/CppVerify/Proofs/*/*.lean; put shared lemmas in User.lean cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp -``Generated.lean`` and ``Check.lean`` are machine-owned; ``Check.lean`` imports -every proof, so ``lake build CppVerify.Check`` builds them all at once. -``User.lean`` is never overwritten, and each goal has a proof file of its own, -which cpp-verify never rewrites but moves with its goal (see `Proofs that -follow their goals`_ below). +``Generated.lean``, ``Auto.lean``, and ``Check.lean`` are machine-owned; +``Check.lean`` imports every proof, so ``lake build CppVerify.Check`` builds +them all at once. ``User.lean`` is never overwritten, and each goal has a proof +file of its own: the proof ``cppverify_auto`` finds for it, or a stub (see +`Proofs cppverify_auto finds`_ below). cpp-verify rewrites that file only while +nobody has edited it; an edited one it never rewrites, but moves with its goal +(see `Proofs that follow their goals`_ below). The project pins ``leanprover/lean4:v4.35.0``, which certification runs whatever elan's default toolchain is; a project 0.1 generated, pinned to ``v4.32.2``, moves to it with a warning. Certification compiles the user @@ -196,6 +198,8 @@ obligation means, so a proof of it is a proof of the obligation: For example, the call in ``small`` must establish the precondition of ``nonnegative``: +.. cppverify-example: flags --backend=lean --lean-project={dir}/proof + .. code-block:: cpp void nonnegative(int n) @@ -210,7 +214,14 @@ For example, the call in ``small`` must establish the precondition of } ``cpp-verify --backend=lean --lean-project=proof file.cpp`` exports four -goals, three of them ``True``. The one for the call reads: +goals, three of them ``True``, and ``cppverify_auto`` proves all four: + +.. code-block:: text + + Exported: lean obligation: nonnegative (cppverify_auto proved 1 of 1 goals) + Exported: lean obligation: small (cppverify_auto proved 3 of 3 goals) + +The one for the call reads: .. code-block:: lean4 @@ -224,9 +235,10 @@ A goal is a disjunction: the negated facts it may assume, then what it must show. The first two facts describe the null pointer (no object owns address 0, and none is live with identity 0); the third is that evaluating the precondition at ``n = 3`` is defined; the last disjunct is the precondition -there, the quantifier for every ``k`` in ``[0, 3)`` and ``3 < 8``. Its proof file, -``proof/CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_precondition_4e324fa2.lean``, -proves that disjunct: +there, the quantifier for every ``k`` in ``[0, 3)`` and ``3 < 8``. A proof +by hand, written over the automatic one in its file, +``proof/CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_precondition_4e324fa2.lean`` +(below its header), proves that disjunct: .. code-block:: lean4 @@ -384,11 +396,13 @@ conclusion. The bridge, ``cppverify_twice_edf933_postcondition_28de726e.of_readable``, proves the goal from this form; Lean checks it when it builds the generated file, so a readable form that said less than its goal would fail there, not certify. A -new proof file starts from it, with every name introduced: +stub, the file of a goal ``cppverify_auto`` does not prove (and of every goal +with ``--no-lean-auto``), starts from it, with every name introduced: .. code-block:: lean4 import CppVerify.User + import CppVerify.Auto theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by apply cppverify_twice_edf933_postcondition_28de726e.of_readable @@ -409,8 +423,8 @@ and a proof uses the hypotheses by name: rw [BitVec.add_assoc] rfl -With the two calls' preconditions proved the same way and ``trivial`` for -the return check, +``cppverify_auto`` proves all four goals of ``twice`` itself. With its +proofs, or with proofs by hand like this one, ``cpp-verify --backend=lean --lean-project=proof --lean-certify file.cpp`` prints: @@ -421,6 +435,93 @@ prints: A proof of the goal itself, as the one for ``small`` above, checks as well. +Proofs cppverify_auto finds +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Each new goal is first given to ``cppverify_auto``, a tactic the project +carries in ``CppVerify/Auto.lean``, with the pinned Lean if it is installed. +For this file: + +.. cppverify-example: flags --backend=lean --lean-project={dir}/proof + +.. code-block:: cpp + + int next(int x) + cppverify::pre(x >= 0 && x < 100) + cppverify::post(cppverify::result == x + 1) + { + return x + 1; + } + + int square(int x) + cppverify::pre(x >= 0 && x < 1000) + cppverify::post(cppverify::result >= 0) + { + return x * x; + } + +``cpp-verify --backend=lean --lean-project=proof file.cpp`` prints: + +.. code-block:: text + + Exported: lean obligation: next (cppverify_auto proved 3 of 3 goals) + Exported: lean obligation: square (cppverify_auto proved 1 of 3 goals) + +A goal it proves gets that proof, with a header that says so: + +.. code-block:: lean4 + + automation: cppverify_auto 1 proves it with cppverify_auto_grind + cppverify_auto proves this goal. cpp-verify rewrites this file only while it + is unedited; a proof you write here is yours, kept as any other. -/ + import CppVerify.User + import CppVerify.Auto + + theorem cppverify_next_e1e917_postcondition_506f384e_proof : cppverify_next_e1e917_postcondition_506f384e := by + apply cppverify_next_e1e917_postcondition_506f384e.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 x_0 h_pre_1 h_null_1 h_null_2 h_exact_1 h_exact_2 h_result_1 + cppverify_auto_grind + +Any other goal gets a stub, whose header says it was tried +(``automation: cppverify_auto 1 did not prove it``). Here those are the two +goals of ``square`` that need ``x * x`` bounded: nonlinear arithmetic, which +core Lean does not decide. Certification checks the automatic proofs like any +other, so ``--lean-certify`` prints ``Certified: next [backend=Lean]``, and +``square`` stays ``Unresolved`` until its two stubs are proved. + +``cppverify_auto`` tries these steps in order, each with a budget of 50000 +heartbeats of its own (``set_option cppverify.autoBudget``), and keeps the +first that proves the goal: + +- ``cppverify_auto_grind``: ``grind``; +- ``cppverify_auto_heap``: every store of memory is turned into the function + it defines, then as below; +- ``cppverify_auto_bv``: machine comparisons, constants, and overflow + conditions are stated as facts about integers, then ``grind``; +- ``cppverify_auto_decide``: ``decide``; +- ``cppverify_auto_simp``: ``simp_all``. + +A step counts only when it proves the goal with Lean's foundations alone, so +an unfinished lemma of yours (proved by ``sorry``) never proves a goal, and a +goal counts as proved only when the kernel accepted its proof. A goal it +spends more than 20 seconds on, its kernel check included, gets a stub +(``did not prove it within 20 s``; ``--lean-auto-timeout`` sets the limit). +The steps and their order were chosen by trying candidates on every goal the +test suite exports: of the goals Z3 proves, ``cppverify_auto`` proves 90%; +most of the rest need nonlinear arithmetic, induction over a spec, or a +quantified frame. + +A goal is tried once: a later export tries a stub again only if a later +release of cpp-verify brings a new revision of ``cppverify_auto`` (the ``1`` +in the header), and never once you edit it. You can help it: a lemma in +``User.lean`` tagged ``@[grind]`` or ``@[simp]`` is used by its steps, since +the proof files import ``User.lean``; delete a stub to have it tried again. +Your own proofs may use ``cppverify_auto``, any of its steps, and the parts +they are made of (``cppverify_norm``, ``cppverify_heap``). What it writes is not taken on trust: a file it +calls proved is still certified like any other, and a ``User.lean`` that +fooled it would only change what the file holds. ``--no-lean-auto`` writes +stubs only. + Proofs that follow their goals ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -435,32 +536,31 @@ records the goal, the obligation, and the full hash. Reordering clauses or adding functions changes no statement, so every proof stays where it is. Each run puts every proof with the goal of its statement. Renaming ``small`` -of the example above to ``tiny`` moves its proofs, with the names they use, -and they certify again: +of the example above to ``tiny`` moves the proof written by hand, with the +names it uses; the automatic proofs are simply written again for the new +goals, and everything certifies again: .. code-block:: text Certified: nonnegative [backend=Lean] Certified: tiny [backend=Lean] - warning: the Lean proof of fn_5f5a3474696e7976::missing-return@synthetic moved from CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_missing_return_ba8abb90.lean to CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_missing_return_ba8abb90.lean, the file of the goal with its statement - warning: the Lean proof of fn_5f5a3474696e7976::postcondition@7:19 moved from CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_postcondition_ba8abb90.lean to CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_postcondition_ba8abb90.lean, the file of the goal with its statement warning: the Lean proof of fn_5f5a3474696e7976::precondition@9:3 moved from CppVerify/Proofs/cppverify_small_74ff94/cppverify_small_74ff94_precondition_4e324fa2.lean to CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_precondition_4e324fa2.lean, the file of the goal with its statement A changed statement never gets the old proof. With ``nonnegative(4)`` in -place of ``nonnegative(3)``, the precondition's goal is a new one, which gets -a stub, and the old proof is kept: +place of ``nonnegative(3)``, the precondition's goal is a new one, which +``cppverify_auto`` proves, and the old proof is kept: .. code-block:: text - Exported: lean obligation: nonnegative - Exported: lean obligation: tiny + Exported: lean obligation: nonnegative (cppverify_auto proved 1 of 1 goals) + Exported: lean obligation: tiny (cppverify_auto proved 3 of 3 goals) warning: the Lean proof CppVerify/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_precondition_4e324fa2.lean is kept in Stale/Proofs/cppverify_tiny_de8a22/cppverify_tiny_de8a22_precondition_4e324fa2.lean: the statement of fn_5f5a3474696e7976::precondition@9:3 changed; its goal is now cppverify_tiny_de8a22_precondition_2596f63f The kept file ends with that note. The proof comes back by itself once a goal has its statement again, as it would if the call were ``nonnegative(3)`` again, and so do the proofs of a function that is removed and later -restored. A stub nobody edited is simply removed. Nothing else is ever -deleted: ``--lean-prune-stale`` deletes what ``Stale/`` keeps, once the run +restored. A file nobody edited, a stub or an automatic proof, is simply +removed. Nothing else is ever deleted: ``--lean-prune-stale`` deletes what ``Stale/`` keeps, once the run has taken back what it needs (``warning: removed the 4 Lean proofs kept in Stale/, as --lean-prune-stale asks``). diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index b9ff374851..a7082dc386 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -220,6 +220,10 @@ nothing is verified: - ``error: --lean-fallback-scope requires --lean-fallback`` * - ``--lean-prune-stale`` without ``--lean-project`` or ``--lean-fallback`` - ``error: --lean-prune-stale requires --lean-project or --lean-fallback`` + * - ``--no-lean-auto`` without ``--lean-project`` or ``--lean-fallback`` + - ``error: --no-lean-auto requires --lean-project or --lean-fallback`` + * - ``--lean-auto-timeout=N`` without ``--lean-project`` or ``--lean-fallback`` + - ``error: --lean-auto-timeout requires --lean-project or --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 @@ -298,7 +302,13 @@ Backends ``h_call_next_2``, ``h_x_1`` for the definition of ``x_1``), and a bridge ``G.of_readable : G.readable → G`` that the kernel checks with the generated file, so a proof of either form proves ``G``. A stub - applies the bridge and introduces every name. Each + applies the bridge and introduces every name. Each new goal is first + given to ``cppverify_auto`` (``CppVerify/Auto.lean``), with the pinned + Lean if it is installed: a goal it proves gets that proof, and the + export says how many, as in ``Exported: lean obligation: next + (cppverify_auto proved 3 of 3 goals)``; any other goal gets a stub that + says it was tried (:doc:`../book/part-ii/ch17-backends-modular-calls`). + Each goal means what its obligation means: every operator keeps its grouping under Lean's precedence, a numeral has its type (``Nat`` would read ``2 - 3`` as 0), a Boolean is a proposition @@ -308,7 +318,8 @@ Backends (:doc:`../book/part-ii/ch17-backends-modular-calls`). * - ``--lean-certify`` - Build the active project with the pinned Lean 4.35.0, each proof file on - its own and without ``sorry``, then check the compiled modules with a + its own and without ``sorry`` (``--jobs`` of them at once), then check + the compiled modules with a program that elaborates none of the user's source: the kernel replays every module of the project a proof imports, the proof must state exactly its goal, and it may depend on no axiom but ``propext``, @@ -343,6 +354,15 @@ Backends ``warning: removed the 4 Lean proofs kept in Stale/, as --lean-prune-stale asks``. Without it, nothing is ever deleted but an unedited stub. Requires ``--lean-project`` or ``--lean-fallback``. + * - ``--no-lean-auto`` + - Write a stub for each new Lean goal without trying ``cppverify_auto`` + on it. Requires ``--lean-project`` or ``--lean-fallback``. + * - ``--lean-auto-timeout=N`` + - Milliseconds of wall-clock time ``cppverify_auto`` may spend on one + new goal, its kernel check included (default 20000; ``0`` disables). A + goal that takes longer gets a stub, as in ``automation: + cppverify_auto 1 did not prove it within 20 s``. Requires + ``--lean-project`` or ``--lean-fallback``. * - ``--unroll=N`` - Maximum BMC loop bound, which selects ``--backend=bmc``. Source verification explores ``0..N``; lower-only and archive replay retain one exact recorded bound, @@ -408,7 +428,9 @@ Backends are verified at once, a function's obligations run on the same workers, and its whole query races them. Results are published in source order (default: every physical core, or ``CPPVERIFY_JOBS``; - ``0`` selects every core). Lean export remains serial. + ``0`` selects every core). Lean export remains serial; ``cppverify_auto`` + and certification run this many Lean processes at once (default: every + physical core). * - ``--function-timeout=N`` - Milliseconds all queries of one function may take together (default ten times ``--timeout``; ``0`` disables). See `Time limits`_. @@ -514,7 +536,8 @@ 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 +None of these limits applies to Lean, which runs no solver; ``cppverify_auto`` +has a limit of its own, ``--lean-auto-timeout``. 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 @@ -544,7 +567,10 @@ a fixed amount of solver work (Z3 resource units), with the query timeout only as a bound in time, so on a loaded machine it stops where it stops on an idle one, unless the timeout passes first; once it has found a counterexample, the obligations that choose the failure to report get the -same work each. Lean generation and certification stay serial. The compile-time +same work each. Lean generation stays serial; ``cppverify_auto`` and +certification run Lean processes side by side; what they find does not depend +on how many, but a goal whose automation is near ``--lean-auto-timeout`` may +finish in time under one load and not under another. The compile-time verifier (``clang++ -fverify-contracts``) always uses one job and the default limits; use ``cpp-verify`` for ``--jobs`` and the other options. diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 79e5a9ee33..89e6c5332f 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -356,6 +356,25 @@ goal, which the kernel checks with the generated file. A new proof file starts from the readable form with every name introduced; a proof of the goal itself still checks (:doc:`book/part-ii/ch17-backends-modular-calls`). +**Lean proofs cppverify_auto finds.** Every goal of a Lean project was a stub, +each ``True`` included, so a project of a few functions needed tens of proofs +before it certified. Each new goal is now first given to ``cppverify_auto``, a +tactic the project carries in ``CppVerify/Auto.lean``: it tries ``grind``; then +memory stores as the functions they define and machine arithmetic as integers, +before ``grind``; then ``decide`` and ``simp_all``, each with a budget of its +own, and it keeps a step only when its proof uses Lean's foundations alone. A +goal it proves gets that proof, and the export counts them, as in +``Exported: lean obligation: next (cppverify_auto proved 3 of 3 goals)``; +certification checks those proofs like any other. Any other goal gets a stub +that says it was tried, and it is tried again only by a later revision of +``cppverify_auto``. Of the goals of the test suite that Z3 proves, it proves +90%. ``--no-lean-auto`` writes stubs only, and with ``--backend=lean``, +``--jobs``, which was an error there, sets how many Lean processes automation +and certification run at once. Certification also builds the +proofs side by side and checks them in one Lean environment: the 33 goals of +one test took 204 s and now take 12 s +(:doc:`book/part-ii/ch17-backends-modular-calls`). + **Lean 4.35.0.** Lean projects pin ``leanprover/lean4:v4.35.0``. A project 0.1 generated, pinned to ``v4.32.2``, moves to the new pin the next time cpp-verify writes it, with a warning; a proof that no longer builds needs updating for that