Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

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) {