Introducing llvm-kompile compute-ordinal and compute-loc tools (#1056)

Robertorosmaninho · rv-jenkins · web-flow · commit 5553a299878b · 2024-05-21T03:41:58.000-06:00
These tools are meant to replace the old `llvm-kompile-compute-ordinal`
and `llvm-kompile-compute-loc` bash scripts with an appropriate C++
infrastructure.

The new tools can work in two ways:
- Parsing the definition and looking for/using the K file location to
compute the ordinal and location info.
- Using the `definition.kore` lines to compute the ordinal and returning
the line in the definition when computing the location.

The interface of the new tools is defined as follows:
```bash
llvm-kompile-compute-loc [options] &lt;kompiled-dir&gt; &lt;ordinal&gt; [is-k-line]
```
and
```bash
llvm-kompile-compute-ordinal [options] &lt;kompiled-dir&gt; &lt;line&gt; [is-k-line]
```

in both cases, `is-k-line` is false by default to have the same behavior
as the old scripts.

---------

Co-authored-by: rv-jenkins &lt;admin@runtimeverification.com&gt;
diff --git a/bin/llvm-kompile-compute-loc b/bin/llvm-kompile-compute-loc
diff --git a/bin/llvm-kompile-compute-ordinal b/bin/llvm-kompile-compute-ordinal
diff --git a/include/kllvm/ast/util.h b/include/kllvm/ast/util.h
@@ -0,0 +1,20 @@
+#ifndef UTIL_H
+#define UTIL_H
+
+#include <kllvm/ast/AST.h>
+
+namespace kllvm {
+
+/*
+ * This file contains utility functions that are used in multiple tools and
+ * are not specific to any one tool. These functions are used to manipulate
+ * the AST and other data structures.
+*/
+
+[[nodiscard]] std::optional<int64_t>
+get_start_line_location(kore_axiom_declaration const &axiom);
+
+[[nodiscard]] std::string trim(std::string s);
+} // namespace kllvm
+
+#endif // UTIL_H
diff --git a/lib/ast/CMakeLists.txt b/lib/ast/CMakeLists.txt
@@ -2,6 +2,7 @@ add_library(AST
   AST.cpp
   attribute_set.cpp
   pattern_matching.cpp
+  util.cpp
   definition.cpp
 )
 
diff --git a/lib/ast/util.cpp b/lib/ast/util.cpp
@@ -0,0 +1,29 @@
+#include "kllvm/ast/util.h"
+
+#include <algorithm>
+#include <string>
+
+using namespace kllvm;
+
+[[nodiscard]] std::optional<int64_t>
+kllvm::get_start_line_location(kore_axiom_declaration const &axiom) {
+  auto location_att = axiom.attributes().get(attribute_set::key::Location);
+  assert(location_att->get_arguments().size() == 1);
+
+  auto str_pattern = std::dynamic_pointer_cast<kore_string_pattern>(
+      location_att->get_arguments()[0]);
+  std::string location = str_pattern->get_contents();
+
+  size_t l_paren = location.find_first_of('(');
+  size_t first_comma = location.find_first_of(',');
+  size_t length = first_comma - l_paren - 1;
+  return std::stoi(location.substr(l_paren + 1, length));
+}
+
+// trim the string from the start
+[[nodiscard]] std::string kllvm::trim(std::string s) {
+  s.erase(s.begin(), std::find_if(s.begin(), s.end(), [](int c) {
+            return !std::isspace(c);
+          }));
+  return s;
+}
diff --git a/test/defn/compute-ordinal-loc/definition.kore b/test/defn/compute-ordinal-loc/definition.kore
diff --git a/test/defn/compute-ordinal-loc/k-files/inc.k b/test/defn/compute-ordinal-loc/k-files/inc.k
@@ -0,0 +1,10 @@
+module INC 
+  imports INT
+  imports BOOL
+
+  rule I => I +Int 1
+    requires I >Int 0 andBool I <Int 100
+  rule I => I -Int 1
+    requires I <Int 0 andBool I >Int -100
+
+endmodule
diff --git a/test/defn/compute-ordinal-loc/line_number_rule b/test/defn/compute-ordinal-loc/line_number_rule
@@ -0,0 +1 @@
+5
diff --git a/test/lit.cfg.py b/test/lit.cfg.py
@@ -104,6 +104,8 @@ def one_line(s):
     ('%arity', 'kore-arity'),
     ('%apply-rule', 'k-rule-apply'),
     ('%find-rule', 'k-rule-find'),
+    ('%compute-loc', 'llvm-kompile-compute-loc %S'),
+    ('%compute-ordinal', 'llvm-kompile-compute-ordinal %S'),
 
     ('%kllvm-clang', 'clang -I %include-path -I Inputs Inputs/api.c'),
 
diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
@@ -23,6 +23,8 @@ endmacro(kllvm_add_tool)
 
 add_subdirectory(llvm-backend-version)
 add_subdirectory(llvm-kompile-codegen)
+add_subdirectory(llvm-kompile-compute-loc)
+add_subdirectory(llvm-kompile-compute-ordinal)
 add_subdirectory(llvm-kompile-gc-stats)
 add_subdirectory(kprint)
 add_subdirectory(kore-arity)
diff --git a/tools/llvm-kompile-compute-loc/CMakeLists.txt b/tools/llvm-kompile-compute-loc/CMakeLists.txt
@@ -0,0 +1,12 @@
+kllvm_add_tool(llvm-kompile-compute-loc
+  main.cpp
+)
+
+target_link_libraries(llvm-kompile-compute-loc
+  PUBLIC Parser AST Codegen
+)
+
+install(
+  TARGETS llvm-kompile-compute-loc
+  RUNTIME DESTINATION bin
+)
diff --git a/tools/llvm-kompile-compute-loc/main.cpp b/tools/llvm-kompile-compute-loc/main.cpp
@@ -0,0 +1,78 @@
+#include <kllvm/ast/AST.h>
+#include <kllvm/ast/util.h>
+#include <kllvm/parser/KOREParser.h>
+
+#include <llvm/Support/CommandLine.h>
+
+#include <cstdlib>
+#include <fstream>
+#include <iostream>
+#include <string>
+
+using namespace llvm;
+using namespace kllvm;
+
+cl::OptionCategory loc_cat("llvm-kompile-compute-loc options");
+
+cl::opt<std::string> kompiled_dir(
+    cl::Positional, cl::desc("<kompiled-dir>"), cl::Required, cl::cat(loc_cat));
+
+cl::opt<int> ordinal(
+    cl::Positional, cl::desc("<ordinal>"), cl::Required, cl::cat(loc_cat));
+
+cl::opt<bool> is_k_line(
+    "k-line",
+    cl::desc("The tool will look for the line passed as an argument in the K "
+             "definition"),
+    cl::init(false), cl::cat(loc_cat));
+
+std::optional<int64_t>
+get_k_location(std::string &definition, int const &ordinal) {
+  // Parse the definition.kore to get the AST.
+  kllvm::parser::kore_parser parser(definition);
+  auto kore_ast = parser.definition();
+  kore_ast->preprocess();
+
+  auto axiom = kore_ast->get_axiom_by_ordinal(ordinal);
+  return get_start_line_location(axiom);
+}
+
+std::optional<int64_t>
+get_kore_location(std::string &definition, int const &ordinal) {
+
+  int64_t line_num = 0;
+  int64_t ordinal_num = 0;
+
+  std::ifstream file(definition);
+  std::string line;
+
+  while (std::getline(file, line)) {
+    line_num++;
+    line = trim(line);
+    if (line.starts_with("axiom")) {
+      if (ordinal_num == ordinal) {
+        return line_num;
+      }
+      ordinal_num++;
+    }
+  }
+
+  return std::nullopt;
+}
+
+int main(int argc, char **argv) {
+  cl::HideUnrelatedOptions({&loc_cat});
+  cl::ParseCommandLineOptions(argc, argv);
+
+  auto definition = kompiled_dir + "/definition.kore";
+
+  auto location = is_k_line ? get_k_location(definition, ordinal)
+                            : get_kore_location(definition, ordinal);
+
+  if (location) {
+    std::cout << *location << "\n";
+    return 0;
+  }
+
+  return 1;
+}
diff --git a/tools/llvm-kompile-compute-ordinal/CMakeLists.txt b/tools/llvm-kompile-compute-ordinal/CMakeLists.txt
@@ -0,0 +1,12 @@
+kllvm_add_tool(llvm-kompile-compute-ordinal
+  main.cpp
+)
+
+target_link_libraries(llvm-kompile-compute-ordinal
+  PUBLIC Parser AST Codegen
+)
+
+install(
+  TARGETS llvm-kompile-compute-ordinal
+  RUNTIME DESTINATION bin
+)
diff --git a/tools/llvm-kompile-compute-ordinal/main.cpp b/tools/llvm-kompile-compute-ordinal/main.cpp
@@ -0,0 +1,88 @@
+#include <kllvm/ast/AST.h>
+#include <kllvm/ast/util.h>
+#include <kllvm/parser/KOREParser.h>
+
+#include <llvm/Support/CommandLine.h>
+
+#include <cstdlib>
+#include <fstream>
+#include <iostream>
+#include <string>
+
+using namespace llvm;
+using namespace kllvm;
+
+cl::OptionCategory ordinal_cat("llvm-kompile-compute-ordinal options");
+
+cl::opt<std::string> kompiled_dir(
+    cl::Positional, cl::desc("<kompiled-dir>"), cl::Required,
+    cl::cat(ordinal_cat));
+
+cl::opt<int> line(
+    cl::Positional, cl::desc("<line>"), cl::Required, cl::cat(ordinal_cat));
+
+cl::opt<bool> is_k_line(
+    "k-line",
+    cl::desc("The tool will look for the line passed as an argument in the K "
+             "definition"),
+    cl::init(false), cl::cat(ordinal_cat));
+
+std::optional<int64_t>
+get_k_ordinal(std::string const &definition, int const &line) {
+  // Parse the definition.kore to get the AST.
+  kllvm::parser::kore_parser parser(definition);
+  auto kore_ast = parser.definition();
+  kore_ast->preprocess();
+
+  // Iterate through axioms.
+  for (auto *axiom : kore_ast->get_axioms()) {
+    if (axiom->attributes().contains(attribute_set::key::Location)) {
+      auto start_line = get_start_line_location(*axiom);
+      if (start_line == line) {
+        return axiom->get_ordinal();
+      }
+    }
+  }
+
+  return std::nullopt;
+}
+
+std::optional<int64_t>
+get_kore_ordinal(std::string const &definition, int const &line) {
+
+  int64_t line_num = 0;
+  int64_t ordinal_num = 0;
+
+  std::ifstream file(definition);
+  std::string l;
+
+  while (std::getline(file, l)) {
+    line_num++;
+    l = trim(l);
+    if (l.starts_with("axiom")) {
+      if (line_num == line) {
+        return ordinal_num;
+      }
+      ordinal_num++;
+    }
+  }
+
+  return std::nullopt;
+}
+
+int main(int argc, char **argv) {
+  cl::HideUnrelatedOptions({&ordinal_cat});
+  cl::ParseCommandLineOptions(argc, argv);
+
+  auto definition = kompiled_dir + "/definition.kore";
+
+  auto location = is_k_line ? get_k_ordinal(definition, line)
+                            : get_kore_ordinal(definition, line);
+
+  if (location) {
+    std::cout << *location << "\n";
+    return 0;
+  }
+
+  return 1;
+}

Original file line number	Diff line number	Diff line change
`@@ -2,6 +2,7 @@ add_library(AST`
`2`	`2`	`AST.cpp`
`3`	`3`	`attribute_set.cpp`
`4`	`4`	`pattern_matching.cpp`
	`5`	`+ util.cpp`
`5`	`6`	`definition.cpp`
`6`	`7`	`)`
`7`	`8`