diff --git a/include/kllvm/ast/util.h b/include/kllvm/ast/util.h index 453de6768..19473b5a2 100644 --- a/include/kllvm/ast/util.h +++ b/include/kllvm/ast/util.h @@ -11,10 +11,10 @@ namespace kllvm { * the AST and other data structures. */ -[[nodiscard]] std::optional +[[nodiscard]] std::optional> get_start_line_location(kore_axiom_declaration const &axiom); [[nodiscard]] std::string trim(std::string s); } // namespace kllvm -#endif // UTIL_H \ No newline at end of file +#endif // UTIL_H diff --git a/lib/ast/util.cpp b/lib/ast/util.cpp index d486f6e6e..fc0a07679 100644 --- a/lib/ast/util.cpp +++ b/lib/ast/util.cpp @@ -5,19 +5,32 @@ using namespace kllvm; -[[nodiscard]] std::optional +[[nodiscard]] std::optional> 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( + 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( + auto str_pattern_loc = std::dynamic_pointer_cast( 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; -} \ No newline at end of file +} diff --git a/test/defn/compute-ordinal-loc/definition.kore b/test/defn/compute-ordinal-loc/definition.kore index e0d8a5156..8f3c0f714 100644 --- a/test/defn/compute-ordinal-loc/definition.kore +++ b/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)")] diff --git a/test/defn/compute-ordinal-loc/source_line_number_rule b/test/defn/compute-ordinal-loc/source_line_number_rule new file mode 100644 index 000000000..38d36b5ef --- /dev/null +++ b/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 diff --git a/tools/llvm-kompile-compute-loc/main.cpp b/tools/llvm-kompile-compute-loc/main.cpp index cb3e7d8b5..18c964d0c 100644 --- a/tools/llvm-kompile-compute-loc/main.cpp +++ b/tools/llvm-kompile-compute-loc/main.cpp @@ -20,23 +20,11 @@ cl::opt kompiled_dir( cl::opt ordinal( cl::Positional, cl::desc(""), cl::Required, cl::cat(loc_cat)); -cl::opt is_k_line( - "k-line", - cl::desc("The tool will look for the line passed as an argument in the K " - "definition"), +cl::opt 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 -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 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> +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> 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; } diff --git a/tools/llvm-kompile-compute-ordinal/main.cpp b/tools/llvm-kompile-compute-ordinal/main.cpp index fe45927a0..3cdcf5fc4 100644 --- a/tools/llvm-kompile-compute-ordinal/main.cpp +++ b/tools/llvm-kompile-compute-ordinal/main.cpp @@ -21,14 +21,19 @@ cl::opt kompiled_dir( cl::opt line( cl::Positional, cl::desc(""), cl::Required, cl::cat(ordinal_cat)); +cl::opt source( + "source", + cl::desc("The file to which the line number refers. Implies --k-line."), + cl::cat(ordinal_cat)); + cl::opt 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 -get_k_ordinal(std::string const &definition, int const &line) { +std::optional 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) {