update llvm-kompile-compute-loc and llvm-kompile-compute-ordinal (#1094)

These binaries were not quite feature-complete with their original
intended purpose, probably primarily because at the time at which they
were reimplemented, the past version of them was somewhat broken.

This PR adds the following features:

1. Outputting the k location is the default in llvm-kompile-compute-loc
2. If a k location does not exist, it falls back to the kore location
rather than crashing.
3. The output is formatted with both a filename and a line number.
4. In llvm-kompile-compute-ordinal, you can specify a filename and it
will search for the ordinal of a k rule on that line of that file in the
input definition.

include/kllvm/ast/util.h

@@ -11,10 +11,10 @@ namespace kllvm {
  * the AST and other data structures.
 */
 
-[[nodiscard]] std::optional<int64_t>
+[[nodiscard]] std::optional<std::pair<std::string, uint64_t>>
 get_start_line_location(kore_axiom_declaration const &axiom);
 
 [[nodiscard]] std::string trim(std::string s);
 } // namespace kllvm
 
-#endif // UTIL_H
+#endif // UTIL_H

lib/ast/util.cpp

@@ -5,19 +5,32 @@
 
 using namespace kllvm;
 
-[[nodiscard]] std::optional<int64_t>
+[[nodiscard]] std::optional<std::pair<std::string, uint64_t>>
 kllvm::get_start_line_location(kore_axiom_declaration const &axiom) {
+  if (!axiom.attributes().contains(attribute_set::key::Source)
+      || !axiom.attributes().contains(attribute_set::key::Location)) {
+    return std::nullopt;
+  }
+  auto source_att = axiom.attributes().get(attribute_set::key::Source);
+  assert(source_att->get_arguments().size() == 1);
+
+  auto str_pattern_source = std::dynamic_pointer_cast<kore_string_pattern>(
+      source_att->get_arguments()[0]);
+  std::string source = str_pattern_source->get_contents();
+
   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>(
+  auto str_pattern_loc = std::dynamic_pointer_cast<kore_string_pattern>(
       location_att->get_arguments()[0]);
-  std::string location = str_pattern->get_contents();
+  std::string location = str_pattern_loc->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));
+  return std::make_pair(
+      source.substr(7, source.size() - 8),
+      std::stoi(location.substr(l_paren + 1, length)));
 }
 
 // trim the string from the start
@@ -26,4 +39,4 @@ kllvm::get_start_line_location(kore_axiom_declaration const &axiom) {
             return !std::isspace(c);
           }));
   return s;
-}
+}

test/defn/compute-ordinal-loc/definition.kore

@@ -1,7 +1,7 @@
 // RUN: %compute-ordinal $(cat %S/line_number_rule) --k-line > %t0
-// RUN: %compute-loc $(cat %t0) --k-line | diff - %S/line_number_rule
-// RUN: %compute-loc $(cat %t0) > %t1
-// RUN: %compute-ordinal $(cat %t1) | diff - %t0
+// RUN: %compute-loc $(cat %t0) | diff - %S/source_line_number_rule
+// RUN: %compute-loc $(cat %t0) --kore-line > %t1
+// RUN: %compute-ordinal $(cat %t1 | awk -F ':' '{print $2}') | diff - %t0
 
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/temp/inc.k)")]
 

test/defn/compute-ordinal-loc/source_line_number_rule

@@ -0,0 +1 @@
+/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/temp/inc.k:5

tools/llvm-kompile-compute-loc/main.cpp

@@ -20,23 +20,11 @@ cl::opt<std::string> kompiled_dir(
 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::opt<bool> is_kore_line(
+    "kore-line",
+    cl::desc("The tool will output the line in the KORE 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) {
 
@@ -60,17 +48,41 @@ get_kore_location(std::string &definition, int const &ordinal) {
   return std::nullopt;
 }
 
+std::optional<std::pair<std::string, int64_t>>
+get_k_or_kore_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);
+  auto k_loc = get_start_line_location(axiom);
+  if (k_loc) {
+    return k_loc;
+  }
+  auto kore_loc = get_kore_location(definition, ordinal);
+  if (kore_loc) {
+    return std::make_pair(definition, *kore_loc);
+  }
+  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);
+  std::optional<std::pair<std::string, uint64_t>> location;
+  if (is_kore_line) {
+    auto line = get_kore_location(definition, ordinal);
+    location = std::make_pair(definition, *line);
+  } else {
+    location = get_k_or_kore_location(definition, ordinal);
+  }
 
   if (location) {
-    std::cout << *location << "\n";
+    std::cout << location->first << ":" << location->second << "\n";
     return 0;
   }
 

tools/llvm-kompile-compute-ordinal/main.cpp

@@ -21,14 +21,19 @@ cl::opt<std::string> kompiled_dir(
 cl::opt<int> line(
     cl::Positional, cl::desc("<line>"), cl::Required, cl::cat(ordinal_cat));
 
+cl::opt<std::string> source(
+    "source",
+    cl::desc("The file to which the line number refers. Implies --k-line."),
+    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) {
+std::optional<int64_t> get_k_ordinal(
+    std::string const &definition, std::string const &source, int const &line) {
   // Parse the definition.kore to get the AST.
   kllvm::parser::kore_parser parser(definition);
   auto kore_ast = parser.definition();
@@ -37,8 +42,8 @@ get_k_ordinal(std::string const &definition, int const &line) {
   // 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) {
+      auto loc = get_start_line_location(*axiom);
+      if (loc->first.ends_with(source) && loc->second == line) {
         return axiom->get_ordinal();
       }
     }
@@ -74,9 +79,13 @@ int main(int argc, char **argv) {
   cl::HideUnrelatedOptions({&ordinal_cat});
   cl::ParseCommandLineOptions(argc, argv);
 
+  if (!source.empty()) {
+    is_k_line = true;
+  }
+
   auto definition = kompiled_dir + "/definition.kore";
 
-  auto location = is_k_line ? get_k_ordinal(definition, line)
+  auto location = is_k_line ? get_k_ordinal(definition, source, line)
                             : get_kore_ordinal(definition, line);
 
   if (location) {