verify: Try cppverify_auto on each new Lean goal, and certify it faster

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 <set>
 #include <thread>
 
-#if defined(_WIN32)
-#include "llvm/Support/Windows/WindowsSupport.h"
-#else
-#include <cerrno>
-#include <csignal>
-#include <sys/wait.h>
-#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<HANDLE>(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,22 +2483,22 @@ 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;
     }
     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;
     }

clang/lib/Verify/Backend/ChildProcess.cpp

@@ -0,0 +1,120 @@
+#include "ChildProcess.h"
+#include "llvm/Support/ConvertUTF.h"
+#include <system_error>
+
+#if defined(_WIN32)
+#include "llvm/Support/Windows/WindowsSupport.h"
+#else
+#include <cerrno>
+#include <csignal>
+#include <sys/wait.h>
+#if defined(__APPLE__)
+#include <crt_externs.h>
+#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<HANDLE>(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<std::string> childEnvironment(llvm::StringRef Variable,
+                                          llvm::StringRef Value) {
+  std::vector<std::string> 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

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 <string>
+#include <vector>
+
+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<std::string> childEnvironment(llvm::StringRef Variable,
+                                          llvm::StringRef Value);
+
+} // namespace verify
+} // namespace clang
+
+#endif

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