Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

include/kllvm/codegen/ProofEvent.h

@@ -83,6 +83,13 @@ class proof_event {
    */
   llvm::LoadInst *emit_get_proof_chunk_size(llvm::BasicBlock *insert_at_end);
 
+  /*
+   * Check if a value of the given `sort` corresponds to an llvm scalar and
+   * return the size in bits of that scalar. Returns 0 if the given `sort` does
+   * not correspond to an llvm scalar.
+   */
+  uint64_t get_llvm_scalar_bits(kore_composite_sort &sort);
+
   /*
    * Get the block header value for the given `sort_name`.
    */

include/runtime/header.h

@@ -346,7 +346,7 @@ void serialize_raw_term_to_file(
 void serialize_configuration_to_proof_trace(
     FILE *file, block *subject, uint32_t sort);
 void serialize_term_to_proof_trace(
-    FILE *file, void *subject, uint64_t block_header, bool indirect);
+    FILE *file, void *subject, uint64_t block_header, uint64_t bits);
 
 // The following functions are called by the generated code and runtime code to
 // ouput the proof trace data.
@@ -355,16 +355,16 @@ void write_hook_event_pre_to_proof_trace(
     char const *location_stack);
 void write_hook_event_post_to_proof_trace(
     void *proof_writer, void *hook_result, uint64_t block_header,
-    bool indirect);
+    uint64_t bits);
 void write_argument_to_proof_trace(
-    void *proof_writer, void *arg, uint64_t block_header, bool indirect);
+    void *proof_writer, void *arg, uint64_t block_header, uint64_t bits);
 void write_rewrite_event_pre_to_proof_trace(
     void *proof_writer, uint64_t ordinal, uint64_t arity);
 void write_variable_to_proof_trace(
     void *proof_writer, char const *name, void *var, uint64_t block_header,
-    bool indirect);
+    uint64_t bits);
 void write_rewrite_event_post_to_proof_trace(
-    void *proof_writer, void *config, uint64_t block_header, bool indirect);
+    void *proof_writer, void *config, uint64_t block_header, uint64_t bits);
 void write_function_event_pre_to_proof_trace(
     void *proof_writer, char const *name, char const *location_stack);
 void write_function_event_post_to_proof_trace(void *proof_writer);

include/runtime/proof_trace_writer.h

@@ -15,15 +15,15 @@ class proof_trace_writer {
       char const *name, char const *pattern, char const *location_stack)
       = 0;
   virtual void
-  hook_event_post(void *hook_result, uint64_t block_header, bool indirect)
+  hook_event_post(void *hook_result, uint64_t block_header, uint64_t bits)
       = 0;
-  virtual void argument(void *arg, uint64_t block_header, bool indirect) = 0;
+  virtual void argument(void *arg, uint64_t block_header, uint64_t bits) = 0;
   virtual void rewrite_event_pre(uint64_t ordinal, uint64_t arity) = 0;
   virtual void
-  variable(char const *name, void *var, uint64_t block_header, bool indirect)
+  variable(char const *name, void *var, uint64_t block_header, uint64_t bits)
       = 0;
   virtual void
-  rewrite_event_post(void *config, uint64_t block_header, bool indirect)
+  rewrite_event_post(void *config, uint64_t block_header, uint64_t bits)
       = 0;
   virtual void function_event_pre(char const *name, char const *location_stack)
       = 0;
@@ -106,13 +106,13 @@ class proof_trace_file_writer : public proof_trace_writer {
   }
 
   void hook_event_post(
-      void *hook_result, uint64_t block_header, bool indirect) override {
+      void *hook_result, uint64_t block_header, uint64_t bits) override {
     write_uint64(kllvm::hook_result_sentinel);
-    serialize_term_to_proof_trace(file_, hook_result, block_header, indirect);
+    serialize_term_to_proof_trace(file_, hook_result, block_header, bits);
   }
 
-  void argument(void *arg, uint64_t block_header, bool indirect) override {
-    serialize_term_to_proof_trace(file_, arg, block_header, indirect);
+  void argument(void *arg, uint64_t block_header, uint64_t bits) override {
+    serialize_term_to_proof_trace(file_, arg, block_header, bits);
   }
 
   void rewrite_event_pre(uint64_t ordinal, uint64_t arity) override {
@@ -123,15 +123,15 @@ class proof_trace_file_writer : public proof_trace_writer {
 
   void variable(
       char const *name, void *var, uint64_t block_header,
-      bool indirect) override {
+      uint64_t bits) override {
     write_null_terminated_string(name);
-    serialize_term_to_proof_trace(file_, var, block_header, indirect);
+    serialize_term_to_proof_trace(file_, var, block_header, bits);
   }
 
   void rewrite_event_post(
-      void *config, uint64_t block_header, bool indirect) override {
+      void *config, uint64_t block_header, uint64_t bits) override {
     write_uint64(kllvm::config_sentinel);
-    serialize_term_to_proof_trace(file_, config, block_header, indirect);
+    serialize_term_to_proof_trace(file_, config, block_header, bits);
   }
 
   void
@@ -191,17 +191,17 @@ class proof_trace_callback_writer : public proof_trace_writer {
   struct kore_term_construction {
     void *subject;
     uint64_t block_header;
-    bool indirect;
+    uint64_t bits;
 
     kore_term_construction()
         : subject(nullptr)
         , block_header(0)
-        , indirect(false) { }
+        , bits(0) { }
 
-    kore_term_construction(void *subject, uint64_t block_header, bool indirect)
+    kore_term_construction(void *subject, uint64_t block_header, uint64_t bits)
         : subject(subject)
         , block_header(block_header)
-        , indirect(indirect) { }
+        , bits(bits) { }
   };
 
   struct kore_configuration_construction {
@@ -301,13 +301,13 @@ class proof_trace_callback_writer : public proof_trace_writer {
   }
 
   void hook_event_post(
-      void *hook_result, uint64_t block_header, bool indirect) override {
-    current_call_event_->result.emplace(hook_result, block_header, indirect);
+      void *hook_result, uint64_t block_header, uint64_t bits) override {
+    current_call_event_->result.emplace(hook_result, block_header, bits);
     hook_event_callback(current_call_event_.value());
   }
 
-  void argument(void *arg, uint64_t block_header, bool indirect) override {
-    current_call_event_->arguments.emplace_back(arg, block_header, indirect);
+  void argument(void *arg, uint64_t block_header, uint64_t bits) override {
+    current_call_event_->arguments.emplace_back(arg, block_header, bits);
   }
 
   void rewrite_event_pre(uint64_t ordinal, uint64_t arity) override {
@@ -320,21 +320,21 @@ class proof_trace_callback_writer : public proof_trace_writer {
 
   void variable(
       char const *name, void *var, uint64_t block_header,
-      bool indirect) override {
+      uint64_t bits) override {
     auto &p = current_rewrite_event_->substitution[current_rewrite_event_->pos];
     p.first = name;
     p.second.subject = var;
     p.second.block_header = block_header;
-    p.second.indirect = indirect;
+    p.second.bits = bits;
     size_t new_pos = ++current_rewrite_event_->pos;
     if (new_pos == current_rewrite_event_->arity) {
       rewrite_event_callback(current_rewrite_event_.value());
     }
   }
 
   void rewrite_event_post(
-      void *config, uint64_t block_header, bool indirect) override {
-    kore_term_construction configuration(config, block_header, indirect);
+      void *config, uint64_t block_header, uint64_t bits) override {
+    kore_term_construction configuration(config, block_header, bits);
     configuration_term_event_callback(configuration);
   }
 

lib/ast/definition.cpp

@@ -1,6 +1,7 @@
 #include <kllvm/ast/AST.h>
 
 #include <iostream>
+#include <stack>
 #include <string>
 #include <unordered_set>
 
@@ -285,12 +286,40 @@ 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<std::pair<kore_composite_sort *, bool>> worklist;
           auto *ctr = dynamic_cast<kore_composite_sort *>(sort.get());
-          if (!sorts.contains(*ctr)) {
-            sorts.emplace(*ctr, next_sort++);
-            all_sorts_.push_back(ctr);
+          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 &param_sort :
+                     sort_to_process->get_arguments()) {
+                  auto *param_ctr
+                      = dynamic_cast<kore_composite_sort *>(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]);
           }
-          ctr->set_ordinal(sorts[*ctr]);
         }
         if (!instantiations.contains(*symbol)) {
           instantiations.emplace(*symbol, next_symbol++);

lib/binary/serializer.cpp

@@ -179,11 +179,18 @@ void emit_kore_rich_header(std::ostream &os, kore_definition *definition) {
   for (uint32_t i = 0; i < num_sorts; i++) {
     uint32_t idx = i + num_tags;
     os.write(reinterpret_cast<char const *>(&idx), 4);
-    if (!definition->get_all_sorts()[i]->get_arguments().empty()) {
-      throw std::runtime_error(
-          "cannot yet serialize sorts with sort parameters");
+    auto const &sort = definition->get_all_sorts().at(i);
+    uint8_t num_sort_params = sort->get_arguments().size();
+    os.write(reinterpret_cast<char const *>(&num_sort_params), 1);
+    for (uint8_t j = 0; j < num_sort_params; j++) {
+      auto *param_sort
+          = dynamic_cast<kore_composite_sort *>(sort->get_arguments()[j].get());
+      uint32_t param_ordinal = param_sort->get_ordinal();
+      if (param_ordinal >= i) {
+        throw std::runtime_error("found sort ordinal not in topological order");
+      }
+      os.write(reinterpret_cast<char const *>(&param_ordinal), 4);
     }
-    os.put('\000');
   }
 
   for (uint32_t i = 0; i < num_tags; i++) {