about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-06-23 22:34:12 +0100
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2023-07-21 10:00:02 +0100
commit7082eafd05b4f268132ab94772c0243dbebf5087 (patch)
tree549f66608f0cb4e50cee2e51c53206e798ab82cd
parent974f140d79a621785b1fe4a0fc7fe321ba1089e2 (diff)
downloadklee-7082eafd05b4f268132ab94772c0243dbebf5087.tar.gz
Add code to only keep in the --help menu the KLEE/Kleaver option categories
-rw-r--r--include/klee/Solver/SolverCmdLine.h12
-rw-r--r--lib/Solver/SolverCmdLine.cpp16
-rw-r--r--tools/kleaver/main.cpp6
-rw-r--r--tools/klee/main.cpp23
4 files changed, 31 insertions, 26 deletions
diff --git a/include/klee/Solver/SolverCmdLine.h b/include/klee/Solver/SolverCmdLine.h
index 90c162ee..4414dc7a 100644
--- a/include/klee/Solver/SolverCmdLine.h
+++ b/include/klee/Solver/SolverCmdLine.h
@@ -24,6 +24,8 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/CommandLine.h"
 DISABLE_WARNING_POP
 
+#include <set>
+
 namespace klee {
 
 extern llvm::cl::opt<bool> UseFastCexSolver;
@@ -86,12 +88,12 @@ extern llvm::cl::opt<klee::MetaSMTBackendType> MetaSMTBackend;
 
 class KCommandLine {
 public:
-  /// Hide all options in the specified category
-  static void HideOptions(llvm::cl::OptionCategory &Category);
-
-  /// Hide all options except the ones in the specified category
-  static void HideUnrelatedOptions(llvm::cl::OptionCategory &Category);
+  /// Keep only the options in the provided categories,
+  /// together with --help, --help-list, --version and --color
+  static void
+  KeepOnlyCategories(std::set<llvm::cl::OptionCategory *> const &categories);
 };
+
 } // namespace klee
 
 #endif /* KLEE_SOLVERCMDLINE_H */
diff --git a/lib/Solver/SolverCmdLine.cpp b/lib/Solver/SolverCmdLine.cpp
index b0bff6e6..a371d5e4 100644
--- a/lib/Solver/SolverCmdLine.cpp
+++ b/lib/Solver/SolverCmdLine.cpp
@@ -112,16 +112,24 @@ cl::opt<bool> UseAssignmentValidatingSolver(
     cl::desc("Debug the correctness of generated assignments (default=false)"),
     cl::cat(SolvingCat));
 
-
-void KCommandLine::HideOptions(llvm::cl::OptionCategory &Category) {
+void KCommandLine::KeepOnlyCategories(
+    std::set<llvm::cl::OptionCategory *> const &categories) {
   StringMap<cl::Option *> &map = cl::getRegisteredOptions();
 
   for (auto &elem : map) {
+    if (elem.first() == "version" || elem.first() == "color" ||
+        elem.first() == "help"    || elem.first() == "help-list")
+      continue;
+
+    bool keep = false;
     for (auto &cat : elem.second->Categories) {
-      if (cat == &Category) {
-        elem.second->setHiddenFlag(cl::Hidden);
+      if (categories.find(cat) != categories.end()) {
+        keep = true;
+        break;
       }
     }
+    if (!keep)
+      elem.second->setHiddenFlag(cl::Hidden);
   }
 }
 
diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp
index 51298dfb..42ca0c55 100644
--- a/tools/kleaver/main.cpp
+++ b/tools/kleaver/main.cpp
@@ -382,11 +382,7 @@ static bool printInputAsSMTLIBv2(const char *Filename,
 }
 
 int main(int argc, char **argv) {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(13, 0)
-  KCommandLine::HideOptions(llvm::cl::getGeneralCategory());
-#else
-  KCommandLine::HideOptions(llvm::cl::GeneralCategory);
-#endif
+  KCommandLine::KeepOnlyCategories({&ExprCat, &SolvingCat});
 
   bool success = true;
 
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 483397c1..a3062d24 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -9,18 +9,18 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "klee/ADT/KTest.h"
 #include "klee/ADT/TreeStream.h"
 #include "klee/Config/Version.h"
 #include "klee/Core/Interpreter.h"
 #include "klee/Expr/Expr.h"
-#include "klee/ADT/KTest.h"
-#include "klee/Support/OptionCategories.h"
-#include "klee/Statistics/Statistics.h"
 #include "klee/Solver/SolverCmdLine.h"
+#include "klee/Statistics/Statistics.h"
 #include "klee/Support/Debug.h"
 #include "klee/Support/ErrorHandling.h"
 #include "klee/Support/FileHandling.h"
 #include "klee/Support/ModuleUtil.h"
+#include "klee/Support/OptionCategories.h"
 #include "klee/Support/PrintVersion.h"
 #include "klee/System/Time.h"
 
@@ -44,15 +44,15 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS
 #include "llvm/Support/Path.h"
 #include "llvm/Support/raw_ostream.h"
 
-#include "llvm/Support/TargetSelect.h"
 #include "llvm/Support/Signals.h"
+#include "llvm/Support/TargetSelect.h"
 DISABLE_WARNING_POP
 
 #include <dirent.h>
 #include <signal.h>
-#include <unistd.h>
 #include <sys/stat.h>
 #include <sys/wait.h>
+#include <unistd.h>
 
 #include <cerrno>
 #include <ctime>
@@ -61,7 +61,6 @@ DISABLE_WARNING_POP
 #include <iterator>
 #include <sstream>
 
-
 using namespace llvm;
 using namespace klee;
 
@@ -1118,13 +1117,13 @@ linkWithUclibc(StringRef libDir, std::string opt_suffix,
 }
 
 int main(int argc, char **argv, char **envp) {
-  atexit(llvm_shutdown);  // Call llvm_shutdown() on exit.
+  atexit(llvm_shutdown); // Call llvm_shutdown() on exit
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(13, 0)
-  KCommandLine::HideOptions(llvm::cl::getGeneralCategory());
-#else
-  KCommandLine::HideOptions(llvm::cl::GeneralCategory);
-#endif
+  KCommandLine::KeepOnlyCategories(
+     {&ChecksCat,      &DebugCat,    &ExtCallsCat, &ExprCat,   &LinkCat,
+      &MemoryCat,      &MergeCat,    &MiscCat,     &ModuleCat, &ReplayCat,
+      &SearchCat,      &SeedingCat,  &SolvingCat,  &StartCat,  &StatsCat,
+      &TerminationCat, &TestCaseCat, &TestGenCat});
 
   llvm::InitializeNativeTarget();