Addressing comments

runtimeverification · Apr 26, 2024 · 169a356 · 169a356
1 parent 790103f
commit 169a356
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 9 deletions.
diff --git a/include/kllvm/ast/AST.h b/include/kllvm/ast/AST.h
@@ -914,8 +914,8 @@ class kore_definition {
 
   kore_symbol *inj_symbol_{};
 
-  SubsortMap *subsorts_ = nullptr;
-  SubsortMap *subsorts_inverted_ = nullptr;
+  std::optional<SubsortMap> subsorts_;
+  std::optional<SubsortMap> subsorts_inverted_;
 
   /*
    * Insert symbols into this definition that have knowable labels, but cannot
@@ -967,7 +967,16 @@ class kore_definition {
    *   S |-> {T . S is a subsort of T}
    */
   [[nodiscard]] SubsortMap get_subsorts();
-  [[nodiscard]] SubsortMap get_inverted_subsorts();
+
+  /*
+   * Build this definition's inverted subsort relation from axioms that have the
+   * `subsort` attribute.
+   *
+   * The returned map is as follows:
+   *
+   * S |-> {T . S is a direct supersort of T}
+   */
+  [[nodiscard]] SubsortMap get_supersort();
 
   /*
    * Build this definition's overload relation from axioms that have the

diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp
@@ -106,7 +106,7 @@ void kore_definition::insert_reserved_symbols() {
 
 SubsortMap kore_definition::get_subsorts() {
 
-  if (subsorts_ != nullptr) {
+  if (subsorts_.has_value()) {
     return *subsorts_;
   }
 
@@ -123,13 +123,14 @@ SubsortMap kore_definition::get_subsorts() {
     }
   }
 
-  subsorts_ = new SubsortMap(transitive_closure(subsorts));
+  subsorts_
+      = std::optional<SubsortMap>(SubsortMap(transitive_closure(subsorts)));
   return *subsorts_;
 }
 
-SubsortMap kore_definition::get_inverted_subsorts() {
+SubsortMap kore_definition::get_supersort() {
 
-  if (subsorts_inverted_ != nullptr) {
+  if (subsorts_inverted_.has_value()) {
     return *subsorts_inverted_;
   }
 
@@ -141,7 +142,7 @@ SubsortMap kore_definition::get_inverted_subsorts() {
     }
   }
 
-  subsorts_inverted_ = new SubsortMap(inverted_subsorts);
+  subsorts_inverted_ = std::optional<SubsortMap>(SubsortMap(inverted_subsorts));
   return inverted_subsorts;
 }
 

diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
@@ -956,7 +956,7 @@ std::pair<llvm::Value *, bool> create_term::create_allocation(
         = dynamic_cast<kore_composite_sort *>(symbol->get_arguments()[0].get());
         symbol_decl->attributes().contains(attribute_set::key::SortInjection)
         && (sort->get_category(definition_).cat == sort_category::Symbol)
-        && definition_->get_inverted_subsorts()[sort].empty()) {
+        && definition_->get_supersort()[sort].empty()) {
       std::pair<llvm::Value *, bool> val = create_allocation(
           constructor->get_arguments()[0].get(), location_stack);
       if (val.second) {