LCOV - code coverage report
Current view: top level - atermpp/source - aterm_io_binary.cpp (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 281 289 97.2 %
Date: 2019-06-20 00:49:45 Functions: 38 38 100.0 %
Legend: Lines: hit not hit

          Line data    Source code
       1             : // Author(s): Jan Friso Groote
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file atermpp/source/aterm_io_binary.cpp
      10             : /// \brief This file allows to read and write terms in compact binary aterm`
      11             : ///        format. This code stems largely from the ATerm library designed by
      12             : ///        Paul Klint cs. 
      13             : 
      14             : 
      15             : /* includes */
      16             : 
      17             : #include "mcrl2/atermpp/aterm.h"
      18             : #include "mcrl2/atermpp/aterm_int.h"
      19             : #include "mcrl2/atermpp/aterm_io.h"
      20             : #include "mcrl2/atermpp/aterm_list.h"
      21             : #include "mcrl2/atermpp/detail/aterm_io_implementation.h"
      22             : 
      23             : #include "mcrl2/utilities/block_allocator.h"
      24             : #include "mcrl2/utilities/exception.h"
      25             : #include "mcrl2/utilities/indexed_set.h"
      26             : #include "mcrl2/utilities/logger.h"
      27             : #include "mcrl2/utilities/platform.h"
      28             : #include "mcrl2/utilities/unordered_map.h"
      29             : #include "mcrl2/utilities/unused.h"
      30             : 
      31             : #include <cstring>
      32             : #include <cstdio>
      33             : #include <cstdlib>
      34             : #include <cassert>
      35             : #include <stdexcept>
      36             : #include <bitset>
      37             : 
      38             : #ifdef MCRL2_PLATFORM_WINDOWS
      39             : #include <io.h>
      40             : #include <fcntl.h>
      41             : #endif
      42             : 
      43             : /* Integers in BAF are always exactly 32 or 64 bits.  The size must be fixed so that
      44             :  *  *  * BAF terms can be exchanged between platforms. */
      45             : static const std::size_t INT_SIZE_IN_BAF = 64;
      46             : 
      47             : 
      48             : namespace atermpp
      49             : {
      50             : 
      51             : using detail::readInt;
      52             : using detail::writeInt;
      53             : 
      54             : using namespace std;
      55             : 
      56         140 : static void aterm_io_init(std::ios& stream)
      57             : {
      58         140 :   mcrl2::utilities::mcrl2_unused(stream);
      59             : 
      60             : #ifdef MCRL2_PLATFORM_WINDOWS
      61             :   std::string name;
      62             :   FILE* handle;
      63             :   if (stream.rdbuf() == std::cin.rdbuf())
      64             :   {
      65             :     name = "cin";
      66             :     handle = stdin;
      67             :   }
      68             :   else
      69             :   if (stream.rdbuf() == std::cout.rdbuf())
      70             :   {
      71             :     name = "cout";
      72             :     handle = stdout;
      73             :     fflush(stdout);
      74             :   }
      75             :   else
      76             :   if (stream.rdbuf() == std::cerr.rdbuf())
      77             :   {
      78             :     name = "cerr";
      79             :     handle = stderr;
      80             :     fflush(stderr);
      81             :   }
      82             :   if (!name.empty())
      83             :   {
      84             :     if (_setmode(_fileno(handle), _O_BINARY) == -1)
      85             :     {
      86             :       mCRL2log(mcrl2::log::warning) << "Cannot set " << name << " to binary mode.\n";
      87             :     }
      88             :     else
      89             :     {
      90             :       mCRL2log(mcrl2::log::debug) << "Converted " << name << " to binary mode.\n";
      91             :     }
      92             :   }
      93             : #endif // MCRL2_PLATFORM_WINDOWS
      94         140 : }
      95             : 
      96             : static const std::size_t BAF_MAGIC = 0xbaf;
      97             : 
      98             : // The BAF_VERSION constant is the version number of the ATerms written in BAF
      99             : // format. As of 29 August 2013 this version number is used by the mCRL2
     100             : // toolset. Whenever the file format of mCRL2 files is changed, the BAF_VERSION
     101             : // has to be increased.
     102             : //
     103             : // History:
     104             : //
     105             : // before 2013       : version 0x0300
     106             : // 29 August 2013    : version changed to 0x0301
     107             : // 23 November 2013  : version changed to 0x0302 (introduction of index for variable types)
     108             : // 24 September 2014 : version changed to 0x0303 (introduction of stochastic distribution)
     109             : //  2 April 2017     : version changed to 0x0304 (removed a few superfluous fields in the format)
     110             : 
     111             : static const std::size_t BAF_VERSION = 0x0304;
     112             : 
     113             : struct top_symbol
     114             : {
     115             :   /// \brief index into the vector with all sym_write_entries
     116             :   std::size_t index;
     117             :   /// \brief Identification number of this function symbol in the output
     118             :   std::size_t code;
     119             : 
     120        4831 :   top_symbol(std::size_t index_, std::size_t code_)
     121        4831 :    : index(index_), code(code_)
     122        4831 :   {}
     123             : };
     124             : 
     125        5640 : class top_symbols_t
     126             : {
     127             :   public:
     128             :     std::size_t code_width;          /**< This is the log of the number of symbols both for "symbols" and "index_into_symbols". */
     129             :     std::vector<top_symbol> symbols; /**< The set of symbols that occur directly below the top symbol.
     130             :                                         The order of the symbols in this vector is important. */
     131             :     mcrl2::utilities::indexed_set<function_symbol> index_into_symbols;
     132             :                                      /**< This mapping helps to find the entry in symbols with the given
     133             :                                           function symbol */
     134             : };
     135             : 
     136       10318 : class sym_write_entry
     137             : {
     138             :   public:
     139             :     /// \brief The function symbol that this write entry is about
     140             :     const function_symbol id;
     141             :     /**
     142             :      * \brief After executing compute_num_bits, this stores the number of bits required
     143             :      * to uniquely identify each occurrence of id.
     144             :      */
     145             :     std::size_t term_width;
     146             :     /**
     147             :      * \brief The number of unique occurrences of id, i.e. the number of term that
     148             :      * have id as their function symbol.
     149             :      */
     150             :     std::size_t num_terms;
     151             :     /**
     152             :      * \brief Maps each argument index to a table with function symbols that may
     153             :      * occur at that index
     154             :      * top_symbols.size() == id.arity()
     155             :      */
     156             :     std::vector<top_symbols_t> top_symbols;
     157             :     /**
     158             :      * \brief Counter to indicate which argument is being worked on
     159             :      */
     160             :     std::size_t cur_index;
     161             : 
     162        2682 :     sym_write_entry(const function_symbol& id_)
     163             :      : id(id_),
     164             :        term_width(0),
     165             :        num_terms(0),
     166        2682 :        cur_index(0)
     167        2682 :     {}
     168             : };
     169             : 
     170        2863 : class sym_read_entry
     171             : {
     172             :   public:
     173             :     function_symbol sym;
     174             :     std::size_t term_width;
     175             :     std::vector<aterm> terms;
     176             :     std::vector<vector<std::size_t> > topsyms;
     177             :     std::vector<std::size_t> sym_width;
     178             : 
     179        2863 :     sym_read_entry():
     180        2863 :        term_width(0)
     181             :     {
     182        2863 :     }
     183             : };
     184             : 
     185             : static char* text_buffer = nullptr;
     186             : static std::size_t text_buffer_size = 0;
     187             : 
     188             : static std::size_t  bits_in_buffer = 0; /* how many bits in bit_buffer are used */
     189             : /**
     190             :  * \brief Buffer that is filled starting from bit 127 when reading or writing
     191             :  */
     192             : static std::bitset<128> read_write_buffer(0);
     193             : 
     194             : /**
     195             :  * \brief Reverse the order of bits in val.
     196             :  * \details In BAF version 0x0304 the bits are written in reverse order. When bumping
     197             :  * the version number, one should also consider to remove this reversal.
     198             :  */
     199       57609 : static void reverse_bit_order(std::size_t& val)
     200             : {
     201             :   if(std::numeric_limits<std::size_t>::digits == 64)
     202             :   {
     203       57609 :     val = ((val << 32) & 0xFFFFFFFF00000000) | ((val >> 32) & 0x00000000FFFFFFFF);
     204             :   }
     205       57609 :   val = ((val << 16) & 0xFFFF0000FFFF0000) | ((val >> 16) & 0x0000FFFF0000FFFF);
     206       57609 :   val = ((val << 8)  & 0xFF00FF00FF00FF00) | ((val >> 8)  & 0x00FF00FF00FF00FF);
     207       57609 :   val = ((val << 4)  & 0xF0F0F0F0F0F0F0F0) | ((val >> 4)  & 0x0F0F0F0F0F0F0F0F);
     208       57609 :   val = ((val << 2)  & 0xCCCCCCCCCCCCCCCC) | ((val >> 2)  & 0x3333333333333333);
     209       57609 :   val = ((val << 1)  & 0xAAAAAAAAAAAAAAAA) | ((val >> 1)  & 0x5555555555555555);
     210       57609 : }
     211             : 
     212             : /**
     213             :  * \brief Write the nr_bits least significant bits from val to os
     214             :  */
     215       40185 : static void writeBits(std::size_t val, const std::size_t nr_bits, ostream& os)
     216             : {
     217       40185 :   if(nr_bits == 0)
     218             :   {
     219       12273 :     return;
     220             :   }
     221       27912 :   reverse_bit_order(val);
     222             :   // Add val to the buffer
     223       27912 :   read_write_buffer |= std::bitset<128>(val) << (128 - std::numeric_limits<std::size_t>::digits - bits_in_buffer);
     224       27912 :   bits_in_buffer += nr_bits;
     225             :   // Write 8 bytes if available
     226       27912 :   if(bits_in_buffer >= 64)
     227             :   {
     228        2592 :     unsigned long long write_value = (read_write_buffer >> 64).to_ullong();
     229        2592 :     read_write_buffer <<= 64;
     230        2592 :     bits_in_buffer -= 64;
     231       23328 :     for(uint32_t i = 8; i > 0; --i)
     232             :     {
     233       20736 :       os.put((write_value >> (8*(i-1))) & 0xFF);
     234             :     }
     235             :   }
     236             : }
     237             : 
     238             : /**
     239             :  * \brief Flush the remaining bits in the buffer to os.
     240             :  */
     241          69 : static void flushBitsToWriter(ostream& os)
     242             : {
     243          69 :   if (bits_in_buffer > 0)
     244             :   {
     245          64 :     unsigned long long write_value = (read_write_buffer >> 64).to_ullong();
     246         369 :     for(uint32_t i = 8; i > 7 - bits_in_buffer / 8; --i)
     247             :     {
     248         305 :       os.put((write_value >> (8*(i-1))) & 0xFF);
     249             :     }
     250          64 :     if (os.fail())
     251             :     {
     252           0 :       throw mcrl2::runtime_error("Failed to write the last byte to the output file/stream.");
     253             :     }
     254          64 :     read_write_buffer = std::bitset<128>(0);
     255          64 :     bits_in_buffer = 0;
     256             :   }
     257          69 : }
     258             : 
     259             : /**
     260             :  * @brief readBits Reads an n-bit integer from the input stream.
     261             :  * @param val      Variable to store integer in.
     262             :  * @param nr_bits  Number of bits to read from the input stream.
     263             :  * @param is       The input stream.
     264             :  * @return true on success, false on failure (EOF).
     265             :  */
     266             : static
     267       42607 : bool readBits(std::size_t& val, const unsigned int nr_bits, istream& is)
     268             : {
     269       42607 :   val = 0;
     270       42607 :   if(nr_bits == 0)
     271             :   {
     272       12910 :     return true;
     273             :   }
     274       73617 :   while(bits_in_buffer < nr_bits)
     275             :   {
     276             :     // Read bytes until the buffer is sufficiently full
     277       21960 :     int byte = is.get();
     278       21960 :     if(is.fail())
     279             :     {
     280           0 :       return false;
     281             :     }
     282       21960 :     read_write_buffer |= std::bitset<128>(byte) << (56 + 64 - bits_in_buffer);
     283       21960 :     bits_in_buffer += 8;
     284             :   }
     285       89091 :   val = (read_write_buffer >> (128 - std::numeric_limits<std::size_t>::digits)).to_ullong() &
     286       59394 :       (std::numeric_limits<std::size_t>::max() <<
     287       59394 :          (std::numeric_limits<std::size_t>::digits - std::min(nr_bits, static_cast<unsigned int>(std::numeric_limits<std::size_t>::digits))));
     288       29697 :   bits_in_buffer -= nr_bits;
     289       29697 :   read_write_buffer <<= nr_bits;
     290       29697 :   reverse_bit_order(val);
     291       29697 :   return true;
     292             : }
     293             : 
     294        2682 : static void writeString(const std::string& str, ostream& os)
     295             : {
     296             :   /* Write length. */
     297        2682 :   writeInt(str.size(), os);
     298             : 
     299             :   /* Write actual string. */
     300        2682 :   os.write(str.c_str(), str.size());
     301        2682 : }
     302             : 
     303             : 
     304        2863 : static std::size_t readString(istream& is)
     305             : {
     306             :   std::size_t len;
     307             : 
     308             :   /* Get length of string */
     309        2863 :   len = readInt(is);
     310             : 
     311             :   /* Assure buffer can hold the string */
     312        2863 :   if (text_buffer_size < (len+1))
     313             :   {
     314          13 :     text_buffer_size = 2*len;
     315          13 :     text_buffer = (char*) realloc(text_buffer, text_buffer_size);
     316          13 :     if (!text_buffer)
     317             :     {
     318           0 :       throw mcrl2::runtime_error("Out of memory while reading the input file. Fail to claim a block of memory of size "+ std::to_string(text_buffer_size) + ".");
     319             :     }
     320             :   }
     321             : 
     322             :   /* Read the actual string */
     323        2863 :   is.read(text_buffer, len);
     324             : 
     325             :   /* Ok, return length of string */
     326        2863 :   return len;
     327             : }
     328             : 
     329             : /**
     330             :  * Write a symbol to file.
     331             :  */
     332        2682 : static void write_symbol(const function_symbol& sym, ostream& os)
     333             : {
     334        2682 :   writeString(sym.name(), os);
     335        2682 :   writeInt(sym.arity(), os);
     336        2682 : }
     337             : 
     338             : /**
     339             :  * \brief Get the function symbol from an aterm
     340             :  * \details This function is necessary only becuase aterm::function() is protected
     341             :  */
     342      139905 : static const function_symbol& get_function_symbol(const aterm& t)
     343             : {
     344      139905 :   assert(t.type_is_int() || t.type_is_list() || t.type_is_appl());
     345      139905 :   return detail::address(t)->function();
     346             : }
     347             : 
     348             : /**
     349             :  * \brief Retrieve the index into the sym_write_entry table belonging to the top symbol
     350             :  * of a term. Could be a special symbol (AS_INT, etc) when the term is not an application.
     351             :  * \details sym_entries[result].id == t.function()
     352             :  */
     353       19783 : static std::size_t get_fn_symbol_index(const aterm& t, const mcrl2::utilities::indexed_set_large<function_symbol>& index)
     354             : {
     355       19783 :   const function_symbol& sym = get_function_symbol(t);
     356       19783 :   std::size_t result = index.at(sym);
     357       19783 :   return result;
     358             : }
     359             : 
     360             : /**
     361             :  * How many bits are needed to represent val?
     362             :  * Basically, this function is equal to log2(val), except that it maps 0 to 0
     363             :  */
     364       11320 : static std::size_t bit_width(std::size_t val)
     365             : {
     366       11320 :   std::size_t nr_bits = 0;
     367             : 
     368       11320 :   if (val <= 1)
     369             :   {
     370        8542 :     return 0;
     371             :   }
     372             : 
     373       18300 :   while (val)
     374             :   {
     375        7761 :     val>>=1;
     376        7761 :     nr_bits++;
     377             :   }
     378             : 
     379        2778 :   return nr_bits;
     380             : }
     381             : 
     382             : /**
     383             :  * \brief Get argument number i (zero indexed) from term t.
     384             :  */
     385       59142 : static const aterm& subterm(const aterm& t, std::size_t i)
     386             : {
     387       59142 :   if (t.type_is_appl())
     388             :   {
     389       40932 :     assert(i < down_cast<const aterm_appl>(t).function().arity());
     390       40932 :     return atermpp::down_cast<const aterm_appl>(t)[i];
     391             :   }
     392             :   else
     393             :   {
     394       18210 :     assert(t.type_is_list() && t != aterm_list());
     395       18210 :     assert(i < 2);
     396        9105 :     return i == 0 ? atermpp::down_cast<const aterm_list>(t).front()
     397       27315 :                   : atermpp::down_cast<const aterm_list>(t).tail();
     398             :   }
     399             : }
     400             : 
     401             : /**
     402             :  * \brief Add a term to the global term table. Update the symbol tables.
     403             :  */
     404       10695 : static void add_term(sym_write_entry& entry, const aterm& term,
     405             :   const mcrl2::utilities::indexed_set_large<function_symbol>& symbol_index_map,
     406             :   mcrl2::utilities::unordered_map_large<aterm, std::size_t>& term_index_map,
     407             :   std::vector<sym_write_entry>& sym_entries)
     408             : {
     409       10695 :   term_index_map[term] = entry.num_terms++;
     410       10695 :   std::size_t arity = entry.id.arity();
     411             :   // Initialize the vector if necessary
     412       10695 :   if(entry.top_symbols.size() != arity)
     413             :   {
     414        1245 :     entry.top_symbols = std::vector<top_symbols_t>(arity);
     415             :   }
     416             : 
     417       10695 :   if (entry.id != detail::g_term_pool().as_int())
     418             :   {
     419             :     // For every argument, check whether the term should be added to the table
     420       29652 :     for (std::size_t cur_arg=0; cur_arg<arity; cur_arg++)
     421             :     {
     422       19714 :       const aterm& arg = subterm(term, cur_arg);
     423       19714 :       top_symbols_t& tss = entry.top_symbols[cur_arg];
     424       19714 :       std::size_t top_symbol_index = get_fn_symbol_index(arg, symbol_index_map);
     425       19714 :       const function_symbol& top_symbol = sym_entries[top_symbol_index].id;
     426             : 
     427       19714 :       auto put_result = tss.index_into_symbols.insert(top_symbol);
     428       19714 :       if (put_result.second)
     429             :       {
     430        4831 :         tss.symbols.emplace_back(top_symbol_index, (*put_result.first).second);
     431             :       }
     432             :     }
     433             :   }
     434       10695 : }
     435             : 
     436             : struct write_todo
     437             : {
     438             :   const aterm& term;
     439             :   std::size_t arg;
     440             : 
     441       30478 :   write_todo(const aterm& t)
     442             :    :  term(t),
     443       30478 :       arg(0)
     444       30478 :   {}
     445             : };
     446             : 
     447             : /**
     448             :  * \brief If we see this function symbol for the first time, we initialize data
     449             :  * for it in symbol_index_map and sym_entries.
     450             :  * \return The sym_write_entry belonging to func.
     451             :  */
     452       10695 : static sym_write_entry& initialize_function_symbol(const function_symbol& func,
     453             :   mcrl2::utilities::indexed_set_large<function_symbol>& symbol_index_map,
     454             :   std::vector<sym_write_entry>& sym_entries)
     455             : {
     456       10695 :   auto insert_result = symbol_index_map.insert(func);
     457       10695 :   if(insert_result.second)
     458             :   {
     459             :     // We just found a new function symbol, it has 1 occurrence so far
     460        2682 :     sym_entries.emplace_back(func);
     461             :   }
     462       10695 :   return sym_entries[(*insert_result.first).second];
     463             : }
     464             : 
     465             : /**
     466             :  * \brief Collect all terms in the term tables of each symbol
     467             :  */
     468          69 : static void collect_terms(const aterm& t,
     469             :   mcrl2::utilities::indexed_set_large<function_symbol>& symbol_index_map,
     470             :   mcrl2::utilities::unordered_map_large<aterm, std::size_t>& term_index_map,
     471             :   std::vector<sym_write_entry>& sym_entries)
     472             : {
     473         138 :   std::stack<write_todo> stack;
     474          69 :   stack.emplace(t);
     475             : 
     476             :   // Traverse the term in a postfix order: for every term, we first process each
     477             :   // of its arguments, before processing the term itself
     478       30409 :   do
     479             :   {
     480       30409 :     write_todo& current = stack.top();
     481       30409 :     if (current.term.type_is_int() || current.arg >= get_function_symbol(current.term).arity())
     482             :     {
     483             :       // This term is an int or we are finished processing its arguments (arg >= arity)
     484       10695 :       sym_write_entry& we = initialize_function_symbol(get_function_symbol(current.term), symbol_index_map, sym_entries);
     485       10695 :       add_term(we, current.term, symbol_index_map, term_index_map, sym_entries);
     486       10695 :       stack.pop();
     487             :     }
     488             :     else
     489             :     {
     490             :       // Take the argument according to current.arg and increase the counter
     491       19714 :       const aterm& t = subterm(current.term, current.arg++);
     492       19714 :       if (term_index_map.count(t) == 0)
     493             :       {
     494       10626 :         stack.emplace(t);
     495             :       }
     496             :     }
     497             :   }
     498       30409 :   while (!stack.empty());
     499          69 : }
     500             : 
     501             : /**
     502             :  * \brief Calculate the amount of bits required to store the top symbol for every
     503             :  * argument of every function symbol and the term for every function symbol.
     504             :  */
     505          69 : static void compute_num_bits(std::vector<sym_write_entry>& sym_entries)
     506             : {
     507        2751 :   for(sym_write_entry& cur_entry: sym_entries)
     508             :   {
     509        5502 :     for(std::size_t cur_arg = 0; cur_arg < cur_entry.id.arity(); cur_arg++)
     510             :     {
     511        2820 :       top_symbols_t& tss = cur_entry.top_symbols[cur_arg];
     512        2820 :       tss.code_width = bit_width(tss.symbols.size());
     513             :     }
     514        2682 :     cur_entry.term_width = bit_width(cur_entry.num_terms);
     515             :   }
     516          69 : }
     517             : 
     518             : /**
     519             :  * Write all symbols in a term to file.
     520             :  */
     521          69 : static void write_all_symbols(ostream& os, const std::vector<sym_write_entry>& sym_entries)
     522             : {
     523        2751 :   for(const sym_write_entry& cur_sym: sym_entries)
     524             :   {
     525        2682 :     write_symbol(cur_sym.id, os);
     526        2682 :     writeInt(cur_sym.num_terms, os);
     527             : 
     528        5502 :     for (std::size_t arg_idx=0; arg_idx<cur_sym.id.arity(); arg_idx++)
     529             :     {
     530        2820 :       std::size_t nr_symbols = cur_sym.top_symbols[arg_idx].symbols.size();
     531        2820 :       writeInt(nr_symbols, os);
     532        7651 :       for (std::size_t top_idx=0; top_idx<nr_symbols; top_idx++)
     533             :       {
     534        4831 :         const top_symbol& ts = cur_sym.top_symbols[arg_idx].symbols[top_idx];
     535        4831 :         writeInt(ts.index, os);
     536             :       }
     537             :     }
     538             :   }
     539          69 : }
     540             : 
     541             : /**
     542             :  * \brief Write the term t to os in BAF
     543             :  */
     544          69 : static void write_term(const aterm& t, ostream& os,
     545             :   const mcrl2::utilities::indexed_set_large<function_symbol>& symbol_index_map,
     546             :   const mcrl2::utilities::unordered_map_large<aterm, std::size_t>& term_index_map,
     547             :   std::vector<sym_write_entry>& sym_entries)
     548             : {
     549         138 :   std::stack<write_todo> stack;
     550          69 :   stack.emplace(t);
     551             : 
     552       30409 :   do
     553             :   {
     554       30409 :     write_todo& current = stack.top();
     555       30409 :     sym_write_entry& cur_entry = sym_entries[symbol_index_map.at(get_function_symbol(current.term))];
     556             : 
     557       30409 :     if (current.term.type_is_int())
     558             :     {
     559             :       // If aterm integers are > 32 bits, then they cannot be read on a 32 bit machine.
     560         757 :       writeBits(atermpp::down_cast<aterm_int>(current.term).value(), INT_SIZE_IN_BAF, os);
     561             :     }
     562       29652 :     else if (current.arg < get_function_symbol(current.term).arity())
     563             :     {
     564       19714 :       write_todo item(subterm(current.term, current.arg));
     565       19714 :       sym_write_entry& item_entry = sym_entries[symbol_index_map.at(get_function_symbol(item.term))];
     566             : 
     567       19714 :       const top_symbols_t& symbol_table = cur_entry.top_symbols.at(current.arg);
     568       19714 :       const top_symbol& ts = symbol_table.symbols.at(symbol_table.index_into_symbols.at(item_entry.id));
     569       19714 :       writeBits(ts.code, symbol_table.code_width, os);
     570       19714 :       const sym_write_entry& arg_sym = sym_entries.at(ts.index);
     571       19714 :       std::size_t arg_trm_idx = term_index_map.at(item.term);
     572       19714 :       writeBits(arg_trm_idx, arg_sym.term_width, os);
     573             : 
     574       19714 :       ++current.arg;
     575             : 
     576       19714 :       if (arg_trm_idx >= arg_sym.cur_index)
     577             :       {
     578       10626 :         stack.push(item);
     579             :       }
     580       19714 :       continue;
     581             :     }
     582             : 
     583       10695 :     ++cur_entry.cur_index;
     584       10695 :     stack.pop();
     585             :   }
     586       30409 :   while (!stack.empty());
     587          69 :   flushBitsToWriter(os);
     588          69 : }
     589             : 
     590             : 
     591          69 : static void write_baf(const aterm& t, ostream& os)
     592             : {
     593             :   /* Initialize bit buffer */
     594          69 :   read_write_buffer = std::bitset<128>(0);
     595          69 :   bits_in_buffer = 0; /* how many bits in bit_buffer are used */
     596             : 
     597         138 :   mcrl2::utilities::indexed_set_large<function_symbol> symbol_index_map;
     598         138 :   mcrl2::utilities::unordered_map_large<aterm, std::size_t> term_index_map;
     599         138 :   std::vector<sym_write_entry> sym_entries;
     600             : 
     601          69 :   collect_terms(t, symbol_index_map, term_index_map, sym_entries);
     602          69 :   compute_num_bits(sym_entries);
     603             : 
     604             :   /* write header */
     605          69 :   writeInt(0, os);
     606          69 :   writeInt(BAF_MAGIC, os);
     607          69 :   writeInt(BAF_VERSION, os);
     608          69 :   writeInt(sym_entries.size(), os);
     609          69 :   write_all_symbols(os, sym_entries);
     610             : 
     611             :   /* Write the top symbol */
     612          69 :   writeInt(get_fn_symbol_index(t,symbol_index_map), os);
     613             : 
     614          69 :   write_term(t, os, symbol_index_map, term_index_map, sym_entries);
     615          69 : }
     616             : 
     617          69 : void write_term_to_binary_stream(const aterm& t, std::ostream& os)
     618             : {
     619          69 :   aterm_io_init(os);
     620          69 :   write_baf(t, os);
     621          69 : }
     622             : 
     623             : /**
     624             :   * Read a single symbol from file.
     625             :   */
     626             : 
     627        2863 : static function_symbol read_symbol(istream& is)
     628             : {
     629        2863 :   std::size_t len=readString(is);
     630             : 
     631        2863 :   text_buffer[len] = '\0';
     632             : 
     633        2863 :   std::size_t arity = readInt(is);
     634             : 
     635        2863 :   return function_symbol(text_buffer, arity);
     636             : }
     637             : 
     638             : /**
     639             :  * Read all symbols from file.
     640             :  */
     641             : 
     642          70 : static void read_all_symbols(istream& is, std::size_t nr_unique_symbols, std::vector<sym_read_entry>& read_symbols)
     643             : {
     644             :   std::size_t val;
     645             : 
     646        2933 :   for (std::size_t i=0; i<nr_unique_symbols; i++)
     647             :   {
     648             :     /* Read the actual symbol */
     649             : 
     650        5726 :     function_symbol sym = read_symbol(is);
     651        2863 :     read_symbols[i].sym = sym;
     652             : 
     653             :     /* Read term count and allocate space */
     654        2863 :     val = readInt(is);
     655        2863 :     if (val == 0)
     656             :     {
     657           0 :       throw mcrl2::runtime_error("Read file: internal file error: failed to read all function symbols.");
     658             :     }
     659        2863 :     read_symbols[i].term_width = bit_width(val);
     660        2863 :     read_symbols[i].terms = std::vector<aterm>(val);
     661             : 
     662             :     /*  Allocate space for topsymbol information */
     663        2863 :     read_symbols[i].sym_width = std::vector<std::size_t>(sym.arity());
     664        2863 :     read_symbols[i].topsyms = std::vector< vector <std::size_t> > (sym.arity());
     665             : 
     666        5818 :     for (std::size_t j=0; j<sym.arity(); j++)
     667             :     {
     668        2955 :       val = readInt(is);
     669        2955 :       read_symbols[i].sym_width[j] = bit_width(val);
     670        2955 :       read_symbols[i].topsyms[j] = std::vector<std::size_t>(val);
     671             : 
     672        8087 :       for (std::size_t k=0; k<read_symbols[i].topsyms[j].size(); k++)
     673             :       {
     674        5132 :         read_symbols[i].topsyms[j][k] = readInt(is);
     675             :       }
     676             :     }
     677             :   }
     678             : 
     679          70 :   return;
     680             : }
     681             : 
     682       11369 : struct read_todo
     683             : {
     684             :   sym_read_entry* sym;
     685             :   std::vector<aterm> args;
     686             :   aterm* result;
     687             :   aterm* callresult;
     688             : 
     689       11369 :   read_todo(sym_read_entry* s, aterm* r)
     690       11369 :    : sym(s), result(r), callresult(nullptr)
     691             :   {
     692       11369 :     args.reserve(sym->sym.arity());
     693       11369 :   }
     694             : };
     695             : 
     696          70 : static aterm read_term(sym_read_entry* sym, istream& is, std::vector<sym_read_entry>& read_symbols)
     697             : {
     698          70 :   aterm result;
     699             :   std::size_t value;
     700         140 :   std::stack<read_todo> stack;
     701          70 :   stack.emplace(sym, &result);
     702             : 
     703       32294 :   do
     704             :   {
     705       32294 :     read_todo& current = stack.top();
     706             : 
     707       32294 :     if (current.callresult != nullptr)
     708             :     {
     709       20925 :       current.args.push_back(*current.callresult);
     710       20925 :       current.callresult = nullptr;
     711             :     }
     712             :     // AS_INT is registered as having 1 argument, but that needs to be retrieved in a special way.
     713       32294 :     if (current.sym->sym != detail::g_term_pool().as_int() && current.args.size() < current.sym->sym.arity())
     714             :     {
     715       41850 :       if (readBits(value, current.sym->sym_width[current.args.size()], is) &&
     716       20925 :           value < current.sym->topsyms[current.args.size()].size())
     717             :       {
     718       20925 :         sym_read_entry* arg_sym = &read_symbols[current.sym->topsyms[current.args.size()][value]];
     719       41850 :         if (readBits(value, arg_sym->term_width, is) &&
     720       20925 :             value < arg_sym->terms.size())
     721             :         {
     722       20925 :           current.callresult = &arg_sym->terms[value];
     723       20925 :           if (!current.callresult->defined())
     724             :           {
     725       11299 :             stack.emplace(arg_sym, current.callresult);
     726             :           }
     727       20925 :           continue;
     728             :         }
     729             :       }
     730           0 :       throw mcrl2::runtime_error("Could not read valid aterm from stream.");
     731             :     }
     732             : 
     733       11369 :     if (current.sym->sym == detail::g_term_pool().as_int())
     734             :     {
     735         757 :       if (readBits(value, INT_SIZE_IN_BAF, is))
     736             :       {
     737         757 :         *current.result = aterm_int(value);
     738             :       }
     739             :     }
     740       10612 :     else if (current.sym->sym== detail::g_term_pool().as_empty_list())
     741             :     {
     742          67 :       *current.result = aterm_list();
     743             :     }
     744       10545 :     else if (current.sym->sym == detail::g_term_pool().as_list())
     745             :     {
     746        6470 :       aterm_list result = atermpp::down_cast<aterm_list>(current.args[1]);
     747        3235 :       result.push_front(current.args[0]);
     748        3235 :       *current.result = result;
     749             :     }
     750             :     else // sym is a function application
     751             :     {
     752        7310 :       *current.result = aterm_appl(current.sym->sym, current.args.begin(), current.args.end());
     753             :     }
     754       11369 :     stack.pop();
     755             :   }
     756       32294 :   while (!stack.empty());
     757             : 
     758         140 :   return result;
     759             : }
     760             : 
     761             : /**
     762             :  * Read a term from a BAF reader.
     763             :  */
     764             : 
     765             : static
     766          71 : aterm read_baf(istream& is)
     767             : {
     768             :   // Initialize bit buffer
     769          71 :   read_write_buffer = std::bitset<128>(0);
     770          71 :   bits_in_buffer = 0; // how many bits in bit_buffer are used
     771             : 
     772             :   // Read header
     773          71 :   std::size_t val = readInt(is);
     774          71 :   if (val == 0)
     775             :   {
     776          70 :     val = readInt(is);
     777             :   }
     778          71 :   if (val != BAF_MAGIC)
     779             :   {
     780           1 :     throw mcrl2::runtime_error("Error while reading file: The file is not correct as it does not have the BAF_MAGIC control sequence at the right place.");
     781             :   }
     782             : 
     783          70 :   std::size_t version = readInt(is);
     784          70 :   if (version != BAF_VERSION)
     785             :   {
     786           0 :     throw mcrl2::runtime_error("The BAF version (" + std::to_string(version) + ") of the input file is incompatible with the version (" + std::to_string(BAF_VERSION) +
     787           0 :                                ") of this tool. The input file must be regenerated. ");
     788             :   }
     789             : 
     790          70 :   std::size_t nr_unique_symbols = readInt(is);
     791             : 
     792             :   // Allocate symbol space
     793         140 :   std::vector<sym_read_entry> read_symbols(nr_unique_symbols);
     794             : 
     795          70 :   read_all_symbols(is, nr_unique_symbols, read_symbols);
     796             : 
     797          70 :   val = readInt(is);
     798          70 :   aterm result=read_term(&read_symbols[val], is, read_symbols);
     799         140 :   return result;
     800             : }
     801             : 
     802             : 
     803          71 : aterm read_term_from_binary_stream(istream& is)
     804             : {
     805          71 :   aterm_io_init(is);
     806          71 :   aterm result=read_baf(is);
     807          70 :   if (!result.defined())
     808             :   {
     809           0 :     throw mcrl2::runtime_error("Failed to read a term from the input. The file is not a proper binary file.");
     810             :   }
     811          70 :   return result;
     812             : }
     813             : 
     814         420 : } // namespace atermpp

Generated by: LCOV version 1.12