From c66c8ab05d4755853b1deb394ed1778629bdbfde Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 23 Oct 2024 15:24:43 -0500 Subject: [PATCH 1/4] fix ordinals not being applied to return types of symbols --- lib/ast/definition.cpp | 76 +++++++++++++++++++++++------------------- 1 file changed, 42 insertions(+), 34 deletions(-) diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp index 96dfa4c25..ff3accf6c 100644 --- a/lib/ast/definition.cpp +++ b/lib/ast/definition.cpp @@ -172,6 +172,45 @@ SymbolMap kore_definition::get_overloads() const { return transitive_closure(overloads); } +static void process_sort_ordinal( + kore_sort *sort, + std::unordered_map &sorts, + std::vector &all_sorts_, uint32_t &next_sort) { + // We use a work list to ensure that parametric sorts get ordinals + // that are greater than the ordinals of any of their parameters. + // This invariant is usefull for serialization purposes, and given + // that all parametric sorts are statically known, it is sound to + // assign ordinals to them in such a topological order. + std::stack> worklist; + auto *ctr = dynamic_cast(sort); + worklist.push(std::make_pair(ctr, false)); + + while (!worklist.empty()) { + auto *sort_to_process = worklist.top().first; + bool params_processed = worklist.top().second; + worklist.pop(); + + if (!sorts.contains(*sort_to_process)) { + if (!params_processed) { + // Defer processing this sort until its parameter sorts have + // been processed. + worklist.push(std::make_pair(sort_to_process, true)); + for (auto const ¶m_sort : sort_to_process->get_arguments()) { + auto *param_ctr + = dynamic_cast(param_sort.get()); + worklist.push(std::make_pair(param_ctr, false)); + } + continue; + } + + sorts.emplace(*sort_to_process, next_sort++); + all_sorts_.push_back(sort_to_process); + } + + sort_to_process->set_ordinal(sorts[*sort_to_process]); + } +} + // NOLINTNEXTLINE(*-function-cognitive-complexity) void kore_definition::preprocess() { get_subsorts(); @@ -286,41 +325,10 @@ void kore_definition::preprocess() { for (auto *symbol : entry.second) { if (symbol->is_concrete()) { for (auto const &sort : symbol->get_arguments()) { - // We use a work list to ensure that parametric sorts get ordinals - // that are greater than the ordinals of any of their parameters. - // This invariant is usefull for serialization purposes, and given - // that all parametric sorts are statically known, it is sound to - // assign ordinals to them in such a topological order. - std::stack> worklist; - auto *ctr = dynamic_cast(sort.get()); - worklist.push(std::make_pair(ctr, false)); - - while (!worklist.empty()) { - auto *sort_to_process = worklist.top().first; - bool params_processed = worklist.top().second; - worklist.pop(); - - if (!sorts.contains(*sort_to_process)) { - if (!params_processed) { - // Defer processing this sort until its parameter sorts have - // been processed. - worklist.push(std::make_pair(sort_to_process, true)); - for (auto const ¶m_sort : - sort_to_process->get_arguments()) { - auto *param_ctr - = dynamic_cast(param_sort.get()); - worklist.push(std::make_pair(param_ctr, false)); - } - continue; - } - - sorts.emplace(*sort_to_process, next_sort++); - all_sorts_.push_back(sort_to_process); - } - - sort_to_process->set_ordinal(sorts[*sort_to_process]); - } + process_sort_ordinal(sort.get(), sorts, all_sorts_, next_sort); } + process_sort_ordinal( + symbol->get_sort().get(), sorts, all_sorts_, next_sort); if (!instantiations.contains(*symbol)) { instantiations.emplace(*symbol, next_symbol++); } From f7e5cc3521c00e37674c587f0bbf03b06be4c6a6 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 23 Oct 2024 15:35:12 -0500 Subject: [PATCH 2/4] fix clang tidy --- lib/ast/definition.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp index ff3accf6c..0400e3ff7 100644 --- a/lib/ast/definition.cpp +++ b/lib/ast/definition.cpp @@ -175,7 +175,7 @@ SymbolMap kore_definition::get_overloads() const { static void process_sort_ordinal( kore_sort *sort, std::unordered_map &sorts, - std::vector &all_sorts_, uint32_t &next_sort) { + std::vector &all_sorts, uint32_t &next_sort) { // We use a work list to ensure that parametric sorts get ordinals // that are greater than the ordinals of any of their parameters. // This invariant is usefull for serialization purposes, and given @@ -204,7 +204,7 @@ static void process_sort_ordinal( } sorts.emplace(*sort_to_process, next_sort++); - all_sorts_.push_back(sort_to_process); + all_sorts.push_back(sort_to_process); } sort_to_process->set_ordinal(sorts[*sort_to_process]); From 49637fdb3de55341ffefb134212e86c625d51962 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 28 Oct 2024 10:48:33 -0500 Subject: [PATCH 3/4] try to fix issues with mint segfaults --- lib/ast/definition.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp index 0400e3ff7..4e468e41e 100644 --- a/lib/ast/definition.cpp +++ b/lib/ast/definition.cpp @@ -327,8 +327,10 @@ void kore_definition::preprocess() { for (auto const &sort : symbol->get_arguments()) { process_sort_ordinal(sort.get(), sorts, all_sorts_, next_sort); } - process_sort_ordinal( - symbol->get_sort().get(), sorts, all_sorts_, next_sort); + if (symbol->get_sort()->is_concrete()) { + process_sort_ordinal( + symbol->get_sort().get(), sorts, all_sorts_, next_sort); + } if (!instantiations.contains(*symbol)) { instantiations.emplace(*symbol, next_symbol++); } From 2e9de7f56d584b369fe4743843648e6cd6aa78da Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 28 Oct 2024 10:57:03 -0500 Subject: [PATCH 4/4] update header reference --- test/binary/test_rich_header.kore.ref | Bin 17796 -> 17796 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/test/binary/test_rich_header.kore.ref b/test/binary/test_rich_header.kore.ref index 1aa578366c413f2e1778fa251a307415244bb519..45af2a23e94ce121593a0ab9f54ba3946104df93 100644 GIT binary patch delta 764 zcmZ9~xlY4C5C-6N!WHiO3Re_S(Gv&JkU)^d5g_3XhanpiFy3h6R1|5_QM#d_;suZ* zL`TB|@Bq9F-d|&oDAwA~v!2=AapO^IJZi6>iAaPomJ`y=dmo8~+(4i-x9yBHt$Xgc ztexH({(PL~>)heeba^o?YL3gL`hX4p59US1i|UKsOETu|>hWk-kSV(+rI0MBZe$Iw zlAQFO^xl<}5H{;6qc@gPsi7T0&)vmOr{#j5wN&o2j&j4jN+ zlk8acEZED&9TkE4f2K}+AF&5I) znU%JnHqtgUMan`U(hd|R?Lz(oS@xhwQVvpgp(^B|xjJzlRJ~Eb189hJ2>C$l2vRqp zRvtrrq!TDgI)%na1*nyD1`RO3zDjcrj!^Id>L6W0{Uj5bAYDN*(lsBbrJ-;USdtxOv2mmF+v@%T#{M6n{DY_03 zF0&ZVu~q)Wmiae}^Dh?S#blJ zINUN#!-QeSCCk*Bsxu(FtF&%)3nu<=Ep5tbL*bt+8p-6v#z(1|O&QI)rXI*9Z?h#n z!hG(6+UUI{KU@LvapnFaxjns?^+#_z+K0%t1mKcJY`_l6L&~8hNqLl)R6w~%MO6QV z*+m6OC6te}hl;g{`^W*(0ZJT)$RWyZ1012m4-+{?&DekwlsF}kQ&iXnlu>cg8EO`2 z{c~i5iWjI5=@K