Disable iterative matching when proof hints are enabled (#887)

When proof hint generation is enabled, we want to be able to emit every
intermediate configuration into the trace; the current implementation
only does so when we are at a rewrite step that has not used iterative
compilation to merge two decision tree matrices. This PR disables the
use of iterative compilation and residuals when generating code with
trace instrumentation.

Doing so has no effect on the soundness of the generated code; iterative
compilation is a rarely-used optimization.

The first 3 commits in this PR are a slight refactoring of our usage of
command-line options when running code generation.

include/kllvm/codegen/Debug.h

@@ -17,8 +17,6 @@
 
 namespace kllvm {
 
-extern int CODEGEN_DEBUG;
-
 extern std::string SOURCE_ATT;
 extern std::string LOCATION_ATT;
 

include/kllvm/codegen/Options.h

@@ -0,0 +1,25 @@
+#ifndef CODEGEN_OPTIONS_H
+#define CODEGEN_OPTIONS_H
+
+#include "llvm/Support/CommandLine.h"
+
+enum class opt_level { O0, O1, O2, O3 };
+
+extern llvm::cl::OptionCategory CodegenLibCat;
+
+extern llvm::cl::opt<bool> Debug;
+extern llvm::cl::opt<bool> NoOptimize;
+extern llvm::cl::opt<bool> EmitObject;
+extern llvm::cl::opt<bool> BinaryIR;
+extern llvm::cl::opt<bool> ForceBinary;
+extern llvm::cl::opt<bool> ProofHintInstrumentation;
+extern llvm::cl::opt<bool> KeepFramePointer;
+extern llvm::cl::opt<opt_level> OptimizationLevel;
+
+namespace kllvm {
+
+void validate_codegen_args(bool is_tty);
+
+}
+
+#endif

lib/codegen/ApplyPasses.cpp

@@ -1,4 +1,5 @@
 #include <kllvm/codegen/ApplyPasses.h>
+#include <kllvm/codegen/Options.h>
 
 #include "runtime/header.h"
 
@@ -23,32 +24,14 @@
 
 using namespace llvm;
 
-enum opt_level { O0, O1, O2, O3 };
-
-extern cl::OptionCategory CodegenCat;
-
-cl::opt<bool> KeepFramePointer(
-    "fno-omit-frame-pointer",
-    cl::desc("Keep frame pointer in compiled code for debugging purposes"),
-    cl::cat(CodegenCat));
-
-cl::opt<opt_level> OptimizationLevel(
-    cl::desc("Choose optimization level"),
-    cl::values(
-        clEnumVal(O0, "No optimizations"),
-        clEnumVal(O1, "Enable trivial optimizations"),
-        clEnumVal(O2, "Enable default optimizations"),
-        clEnumVal(O3, "Enable expensive optimizations")),
-    cl::cat(CodegenCat));
-
 namespace kllvm {
 
 CodeGenOpt::Level get_opt_level() {
   switch (OptimizationLevel) {
-  case O0: return CodeGenOpt::None;
-  case O1: return CodeGenOpt::Less;
-  case O2: return CodeGenOpt::Default;
-  case O3: return CodeGenOpt::Aggressive;
+  case opt_level::O0: return CodeGenOpt::None;
+  case opt_level::O1: return CodeGenOpt::Less;
+  case opt_level::O2: return CodeGenOpt::Default;
+  case opt_level::O3: return CodeGenOpt::Aggressive;
   }
 }
 

lib/codegen/CMakeLists.txt

@@ -6,6 +6,7 @@ add_library(Codegen
   Decision.cpp
   DecisionParser.cpp
   EmitConfigParser.cpp
+  Options.cpp
   ProofEvent.cpp
   Util.cpp
 )

lib/codegen/Debug.cpp

@@ -20,8 +20,6 @@
 
 namespace kllvm {
 
-int CODEGEN_DEBUG;
-
 std::string SOURCE_ATT = "org'Stop'kframework'Stop'attributes'Stop'Source";
 std::string LOCATION_ATT = "org'Stop'kframework'Stop'attributes'Stop'Location";
 

lib/codegen/Options.cpp

@@ -0,0 +1,63 @@
+#include <kllvm/codegen/Options.h>
+
+using namespace llvm;
+
+cl::OptionCategory CodegenLibCat("Internal codegen options");
+
+cl::opt<bool> ProofHintInstrumentation(
+    "proof-hint-instrumentation",
+    llvm::cl::desc("Enable instrumentation for generation of proof hints"),
+    llvm::cl::cat(CodegenLibCat));
+
+cl::opt<bool> KeepFramePointer(
+    "fno-omit-frame-pointer",
+    cl::desc("Keep frame pointer in compiled code for debugging purposes"),
+    cl::cat(CodegenLibCat));
+
+cl::opt<opt_level> OptimizationLevel(
+    cl::desc("Choose optimization level"),
+    cl::values(
+        clEnumVal(opt_level::O0, "No optimizations"),
+        clEnumVal(opt_level::O1, "Enable trivial optimizations"),
+        clEnumVal(opt_level::O2, "Enable default optimizations"),
+        clEnumVal(opt_level::O3, "Enable expensive optimizations")),
+    cl::cat(CodegenLibCat));
+
+cl::opt<bool> Debug(
+    "debug", cl::desc("Enable debug information"), cl::ZeroOrMore,
+    cl::cat(CodegenLibCat));
+
+cl::opt<bool> NoOptimize(
+    "no-optimize",
+    cl::desc("Don't run optimization passes before producing output"),
+    cl::cat(CodegenLibCat));
+
+cl::opt<bool> EmitObject(
+    "emit-object",
+    cl::desc("Directly emit an object file to avoid separately invoking llc"),
+    cl::cat(CodegenLibCat));
+
+cl::opt<bool> BinaryIR(
+    "binary-ir", cl::desc("Emit binary IR rather than text"),
+    cl::cat(CodegenLibCat));
+
+cl::opt<bool> ForceBinary(
+    "f", cl::desc("Force binary bitcode output to stdout"), cl::Hidden,
+    cl::cat(CodegenLibCat));
+
+namespace kllvm {
+
+void validate_codegen_args(bool is_tty) {
+  if (EmitObject && (BinaryIR || NoOptimize)) {
+    throw std::runtime_error(
+        "Cannot specify --emit-object with --binary-ir or --no-optimize");
+  }
+
+  if ((EmitObject || BinaryIR) && is_tty && !ForceBinary) {
+    throw std::runtime_error(
+        "Not printing binary file to stdout; use -o to specify output path "
+        "or force binary with -f\n");
+  }
+}
+
+} // namespace kllvm

lib/codegen/ProofEvent.cpp

@@ -1,18 +1,12 @@
 #include "kllvm/codegen/ProofEvent.h"
 #include "kllvm/codegen/CreateTerm.h"
+#include "kllvm/codegen/Options.h"
 
 #include "llvm/IR/IRBuilder.h"
 #include "llvm/Support/CommandLine.h"
 
 #include <fmt/format.h>
 
-extern llvm::cl::OptionCategory CodegenCat;
-
-llvm::cl::opt<bool> ProofHintInstrumentation(
-    "proof-hint-instrumentation",
-    llvm::cl::desc("Enable instrumentation for generation of proof hints"),
-    llvm::cl::cat(CodegenCat));
-
 namespace kllvm {
 
 /*

tools/llvm-kompile-codegen/main.cpp

@@ -5,6 +5,7 @@
 #include <kllvm/codegen/Decision.h>
 #include <kllvm/codegen/DecisionParser.h>
 #include <kllvm/codegen/EmitConfigParser.h>
+#include <kllvm/codegen/Options.h>
 #include <kllvm/parser/KOREParser.h>
 #include <kllvm/parser/location.h>
 
@@ -38,46 +39,26 @@ using namespace kllvm::parser;
 
 namespace fs = std::filesystem;
 
-cl::OptionCategory CodegenCat("llvm-kompile-codegen options");
+cl::OptionCategory CodegenToolCat("llvm-kompile-codegen options");
 
 cl::opt<std::string> Definition(
     cl::Positional, cl::desc("<definition.kore>"), cl::Required,
-    cl::cat(CodegenCat));
+    cl::cat(CodegenToolCat));
 
 cl::opt<std::string> DecisionTree(
-    cl::Positional, cl::desc("<dt.yaml>"), cl::Required, cl::cat(CodegenCat));
+    cl::Positional, cl::desc("<dt.yaml>"), cl::Required,
+    cl::cat(CodegenToolCat));
 
 cl::opt<std::string> Directory(
-    cl::Positional, cl::desc("<dir>"), cl::Required, cl::cat(CodegenCat));
-
-cl::opt<bool> Debug(
-    "debug", cl::desc("Enable debug information"), cl::ZeroOrMore,
-    cl::cat(CodegenCat));
-
-cl::opt<bool> NoOptimize(
-    "no-optimize",
-    cl::desc("Don't run optimization passes before producing output"),
-    cl::cat(CodegenCat));
-
-cl::opt<bool> EmitObject(
-    "emit-object",
-    cl::desc("Directly emit an object file to avoid separately invoking llc"),
-    cl::cat(CodegenCat));
+    cl::Positional, cl::desc("<dir>"), cl::Required, cl::cat(CodegenToolCat));
 
 cl::opt<std::string> OutputFile(
-    "output", cl::desc("Output file path"), cl::init("-"), cl::cat(CodegenCat));
+    "output", cl::desc("Output file path"), cl::init("-"),
+    cl::cat(CodegenToolCat));
 
 cl::alias OutputFileAlias(
     "o", cl::desc("Alias for --output"), cl::aliasopt(OutputFile),
-    cl::cat(CodegenCat));
-
-cl::opt<bool> BinaryIR(
-    "binary-ir", cl::desc("Emit binary IR rather than text"),
-    cl::cat(CodegenCat));
-
-cl::opt<bool> ForceBinary(
-    "f", cl::desc("Force binary bitcode output to stdout"), cl::Hidden,
-    cl::cat(CodegenCat));
+    cl::cat(CodegenToolCat));
 
 namespace {
 
@@ -129,30 +110,15 @@ void initialize_llvm() {
   InitializeAllAsmPrinters();
 }
 
-void validate_args() {
-  if (EmitObject && (BinaryIR || NoOptimize)) {
-    throw std::runtime_error(
-        "Cannot specify --emit-object with --binary-ir or --no-optimize");
-  }
-
-  if ((EmitObject || BinaryIR) && (OutputFile == "-") && !ForceBinary) {
-    throw std::runtime_error(
-        "Not printing binary file to stdout; use -o to specify output path "
-        "or force binary with -f\n");
-  }
-}
-
 } // namespace
 
 int main(int argc, char **argv) {
   initialize_llvm();
 
-  cl::HideUnrelatedOptions({&CodegenCat});
+  cl::HideUnrelatedOptions({&CodegenToolCat, &CodegenLibCat});
   cl::ParseCommandLineOptions(argc, argv);
 
-  validate_args();
-
-  CODEGEN_DEBUG = Debug ? 1 : 0;
+  validate_codegen_args(OutputFile == "-");
 
   KOREParser parser(Definition);
   ptr<KOREDefinition> definition = parser.definition();
@@ -161,22 +127,23 @@ int main(int argc, char **argv) {
   llvm::LLVMContext Context;
   std::unique_ptr<llvm::Module> mod = newModule("definition", Context);
 
-  if (CODEGEN_DEBUG) {
+  if (Debug) {
     initDebugInfo(mod.get(), Definition);
   }
 
   auto kompiled_dir = fs::absolute(Definition.getValue()).parent_path();
-  addKompiledDirSymbol(Context, kompiled_dir, mod.get(), CODEGEN_DEBUG);
+  addKompiledDirSymbol(Context, kompiled_dir, mod.get(), Debug);
 
   for (auto axiom : definition->getAxioms()) {
     makeSideConditionFunction(axiom, definition.get(), mod.get());
     if (!axiom->isTopAxiom()) {
       makeApplyRuleFunction(axiom, definition.get(), mod.get());
     } else {
-      auto filename = dt_dir() / fmt::format("dt_{}.yaml", axiom->getOrdinal());
-      if (fs::exists(filename)) {
+      auto dt_filename
+          = dt_dir() / fmt::format("dt_{}.yaml", axiom->getOrdinal());
+      if (fs::exists(dt_filename) && !ProofHintInstrumentation) {
         auto residuals = parseYamlSpecialDecisionTree(
-            mod.get(), filename, definition->getAllSymbols(),
+            mod.get(), dt_filename, definition->getAllSymbols(),
             definition->getHookedSorts());
         makeApplyRuleFunction(
             axiom, definition.get(), mod.get(), residuals.residuals);
@@ -185,10 +152,11 @@ int main(int argc, char **argv) {
         makeApplyRuleFunction(axiom, definition.get(), mod.get(), true);
       }
 
-      filename = dt_dir() / fmt::format("match_{}.yaml", axiom->getOrdinal());
-      if (fs::exists(filename)) {
+      auto match_filename
+          = dt_dir() / fmt::format("match_{}.yaml", axiom->getOrdinal());
+      if (fs::exists(match_filename)) {
         auto dt = parseYamlDecisionTree(
-            mod.get(), filename, definition->getAllSymbols(),
+            mod.get(), match_filename, definition->getAllSymbols(),
             definition->getHookedSorts());
         makeMatchReasonFunction(definition.get(), mod.get(), axiom, dt);
       }
@@ -229,7 +197,7 @@ int main(int argc, char **argv) {
     }
   }
 
-  if (CODEGEN_DEBUG) {
+  if (Debug) {
     finalizeDebugInfo();
   }