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: 117 119 98.3 %
Date: 2020-07-11 00:44:39 Functions: 15 16 93.8 %
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             : 
      10             : #include "mcrl2/atermpp/aterm_io_binary.h"
      11             : 
      12             : namespace atermpp
      13             : {
      14             : using namespace mcrl2::utilities;
      15             : 
      16             : /// \brief The magic value for a binary aterm format stream.
      17             : /// \details As of version 0x8305 the magic and version are written as 2 bytes not encoded as variable-width integers. To ensure
      18             : ///          compatibility with older formats the previously variable-width encoding is mimicked by prefixing them with 1000 (0x8).
      19             : static constexpr std::uint16_t BAF_MAGIC = 0x8baf;
      20             : 
      21             : /// \brief The BAF_VERSION constant is the version number of the ATerms written in BAF
      22             : ///        format. As of 29 August 2013 this version number is used by the mCRL2
      23             : ///        toolset. Whenever the file format of mCRL2 files is changed, the BAF_VERSION
      24             : ///        has to be increased.
      25             : ///
      26             : /// \details History:
      27             : ///
      28             : /// before 2013       : version 0x0300
      29             : /// 29 August 2013    : version changed to 0x0301
      30             : /// 23 November 2013  : version changed to 0x0302 (introduction of index for variable types)
      31             : /// 24 September 2014 : version changed to 0x0303 (introduction of stochastic distribution)
      32             : ///  2 April 2017     : version changed to 0x0304 (removed a few superfluous fields in the format)
      33             : /// 19 July 2019      : version changed to 0x8305 (introduction of the streamable aterm format)
      34             : /// 28 February 2020  : version changed to 0x8306 (added ability to stream aterm_int, implemented structured streaming for all objects)
      35             : static constexpr std::uint16_t BAF_VERSION = 0x8306;
      36             : 
      37             : /// \brief Each packet has a header consisting of a type.
      38             : /// \details Either indicates a function symbol, a term (either shared or output) or an arbitrary integer.
      39             : enum class packet_type
      40             : {
      41             :   function_symbol = 0,
      42             :   aterm,
      43             :   aterm_output,
      44             :   aterm_int_output
      45             : };
      46             : 
      47             : /// \brief The number of bits needed to store an element of packet_type.
      48             : static constexpr unsigned int packet_bits = 2;
      49             : 
      50         135 : binary_aterm_ostream::binary_aterm_ostream(std::ostream& stream)
      51         135 :   : m_stream(stream)
      52             : {
      53             :   // The term with function symbol index 0 indicates the end of the stream, its actual value does not matter.
      54         135 :   m_function_symbols.insert(function_symbol("end_of_stream", 0));
      55         135 :   m_function_symbol_index_width = 1;
      56             : 
      57             :   // Write the header of the binary aterm format.
      58         135 :   m_stream.write_bits(0, 8);
      59         135 :   m_stream.write_bits(BAF_MAGIC, 16);
      60         135 :   m_stream.write_bits(BAF_VERSION, 16);
      61         135 : }
      62             : 
      63         270 : binary_aterm_ostream::~binary_aterm_ostream()
      64             : {
      65             :   // Write the end of the stream.
      66         135 :   m_stream.write_bits(static_cast<std::size_t>(packet_type::aterm), packet_bits);
      67         135 :   m_stream.write_bits(0, function_symbol_index_width());
      68         135 : }
      69             : 
      70             : /// \brief Keep track of whether the term can be written to the stream.
      71             : struct write_todo
      72             : {
      73             :   const aterm_appl& term;
      74             :   bool write = false;
      75             : 
      76       22862 :   write_todo(const aterm_appl& term)
      77       22862 :    : term(term)
      78       22862 :   {}
      79             : };
      80             : 
      81        9605 : void binary_aterm_ostream::put(const aterm& term)
      82             : {
      83             :   // Traverse the term bottom up and store the subterms (and function symbol) before the actual term.
      84       19210 :   std::stack<write_todo> stack;
      85        9605 :   stack.emplace(static_cast<const aterm_appl&>(term));
      86             : 
      87       36004 :   do
      88             :   {
      89       45609 :     write_todo& current = stack.top();
      90       91218 :     aterm_appl transformed = m_transformer(current.term);
      91             : 
      92             :     // Indicates that this term is output and not a subterm, these should always be written.
      93       45609 :     bool is_output = stack.size() == 1;
      94       45609 :     if (m_terms.index(current.term) >= m_terms.size() || is_output)
      95             :     {
      96       45494 :       if (current.write)
      97             :       {
      98       22747 :         if (transformed.type_is_int())
      99             :         {
     100        4361 :           if (is_output)
     101             :           {
     102             :             // If the integer is output, write the header and just an integer
     103        4357 :             m_stream.write_bits(static_cast<std::size_t>(packet_type::aterm_int_output), packet_bits);
     104        4357 :             m_stream.write_integer(reinterpret_cast<const aterm_int&>(current.term).value());
     105             :           }
     106             :           else
     107             :           {
     108           4 :             std::size_t symbol_index = write_function_symbol(transformed.function());
     109             : 
     110             :             // Write the packet identifier of an aterm_int followed by its value.
     111           4 :             m_stream.write_bits(static_cast<std::size_t>(packet_type::aterm), packet_bits);
     112           4 :             m_stream.write_bits(symbol_index, function_symbol_index_width());
     113           4 :             m_stream.write_integer(reinterpret_cast<const aterm_int&>(current.term).value());
     114             :           }
     115             :         }
     116             :         else
     117             :         {
     118       18386 :           std::size_t symbol_index = write_function_symbol(transformed.function());
     119             : 
     120             :           // Write the packet identifier, followed by the indices of its function symbol and arguments.
     121       18386 :           m_stream.write_bits(static_cast<std::size_t>(is_output ? packet_type::aterm_output : packet_type::aterm), packet_bits);
     122       18386 :           m_stream.write_bits(symbol_index, function_symbol_index_width());
     123             : 
     124       47751 :           for (const aterm& argument : transformed)
     125             :           {
     126       29365 :             std::size_t index = m_terms.index(argument);
     127       29365 :             assert(index < m_terms.size()); // Every argument must already be written.
     128       29365 :             m_stream.write_bits(index, term_index_width());
     129             :           }
     130             :         }
     131             : 
     132       22747 :         if (!is_output)
     133             :         {
     134             :           // Only regular terms (not output) are shared and as such need a unique index.
     135       13142 :           bool assigned = m_terms.insert(current.term).second;
     136       13142 :           assert(assigned); mcrl2_unused(assigned); // This term should have a new index assigned.
     137       13142 :           m_term_index_width = static_cast<std::uint8_t>(std::log2(m_terms.size()) + 1);
     138             :         }
     139             : 
     140       22747 :         stack.pop();
     141             :       }
     142             :       else
     143             :       {
     144             :         // Add all the arguments to the stack; to be processed first.
     145       52112 :         for (const aterm& argument : transformed)
     146             :         {
     147       29365 :           const aterm_appl& term = static_cast<const aterm_appl&>(argument);
     148       29365 :           if (m_terms.index(term) >= m_terms.size())
     149             :           {
     150             :             // Only add arguments that have not been written before.
     151       13257 :             stack.emplace(term);
     152             :           }
     153             :         }
     154             : 
     155       22747 :         current.write = true;
     156             :       }
     157             :     }
     158             :     else
     159             :     {
     160         115 :      stack.pop(); // This term was already written and as such should be skipped. This can happen if
     161             :                   // one term has two equal subterms.
     162             :     }
     163             :   }
     164       45609 :   while (!stack.empty());
     165        9605 : }
     166             : 
     167       29365 : unsigned int binary_aterm_ostream::term_index_width()
     168             : {
     169       29365 :   assert(m_term_index_width == static_cast<unsigned int>(std::log2(m_terms.size()) + 1));
     170       29365 :   return m_term_index_width;
     171             : }
     172             : 
     173       18525 : unsigned int binary_aterm_ostream::function_symbol_index_width()
     174             : {
     175       18525 :   assert(m_function_symbol_index_width == static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1));
     176       18525 :   return m_function_symbol_index_width;
     177             : }
     178             : 
     179         137 : binary_aterm_istream::binary_aterm_istream(std::istream& is)
     180         138 :   : m_stream(is)
     181             : {
     182             :   // The term with function symbol index 0 indicates the end of the stream.
     183         137 :   m_function_symbols.emplace_back();
     184         137 :   m_function_symbol_index_width = 1;
     185             : 
     186             :   // Read the binary aterm format header.
     187         137 :   if (m_stream.read_bits(8) != 0 || m_stream.read_bits(16) != BAF_MAGIC)
     188             :   {
     189           1 :     throw mcrl2::runtime_error("Error while reading: missing the BAF_MAGIC control sequence.");
     190             :   }
     191             : 
     192         136 :   std::size_t version = m_stream.read_bits(16);
     193         136 :   if (version != BAF_VERSION)
     194             :   {
     195           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) +
     196           0 :                                ") of this tool. The input file must be regenerated. ");
     197             :   }
     198         136 : }
     199             : 
     200       18390 : std::size_t binary_aterm_ostream::write_function_symbol(const function_symbol& symbol)
     201             : {
     202       18390 :   std::size_t result = m_function_symbols.index(symbol);
     203             : 
     204       18390 :   if (result < m_function_symbols.size())
     205             :   {
     206       13862 :     return result;
     207             :   }
     208             :   else
     209             :   {
     210             :     // The function symbol has not been written yet, write it now and return its index.
     211        4528 :     m_stream.write_bits(static_cast<std::size_t>(packet_type::function_symbol), packet_bits);
     212        4528 :     m_stream.write_string(symbol.name());
     213        4528 :     m_stream.write_integer(symbol.arity());
     214             : 
     215        4528 :     auto result = m_function_symbols.insert(symbol);
     216        4528 :     m_function_symbol_index_width = static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1);
     217             : 
     218        4528 :     return result.first;
     219             :   }
     220             : }
     221             : 
     222       28200 : aterm binary_aterm_istream::get()
     223             : {
     224             :   while(true)
     225             :   {
     226             :     // Determine the type of the next packet.
     227       28200 :     std::size_t header = m_stream.read_bits(packet_bits);
     228       28200 :     packet_type packet = static_cast<packet_type>(header);
     229             : 
     230       28200 :     if (packet == packet_type::function_symbol)
     231             :     {
     232             :       // Read a single function symbol and insert it into the already read function symbols.
     233        9370 :       std::string name = m_stream.read_string();
     234        4685 :       std::size_t arity = m_stream.read_integer();
     235        4685 :       m_function_symbols.emplace_back(name, arity);
     236        4685 :       m_function_symbol_index_width = static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1);
     237             :     }
     238       23515 :     else if (packet == packet_type::aterm_int_output)
     239             :     {
     240             :       // Read the integer from the stream and construct an aterm_int.
     241        4378 :       std::size_t value = m_stream.read_integer();
     242        4378 :       return aterm_int(value);
     243             :     }
     244       19137 :     else if (packet == packet_type::aterm || packet == packet_type::aterm_output)
     245             :     {
     246             :       // First read the function symbol of the following term.
     247       32813 :       function_symbol symbol = m_function_symbols[m_stream.read_bits(function_symbol_index_width())];
     248             : 
     249       19137 :       if (!symbol.defined())
     250             :       {
     251             :         // The term with function symbol zero marks the end of the stream.
     252         116 :         return aterm();
     253             :       }
     254       19021 :       else if (symbol == detail::g_as_int)
     255             :       {
     256             :         // Read the integer from the stream and construct a shared aterm_int in the index.
     257           4 :         std::size_t value = m_stream.read_integer();
     258           4 :         m_terms.emplace_back(aterm_int(value));
     259           4 :         m_term_index_width = static_cast<unsigned int>(std::log2(m_terms.size()) + 1);
     260             :       }
     261             :       else
     262             :       {
     263             :         // Read arity number of arguments from the stream and search them in the already defined set of terms.
     264       32689 :         std::vector<aterm> arguments(symbol.arity());
     265       49459 :         for (std::size_t argument = 0; argument < symbol.arity(); ++argument)
     266             :         {
     267       30442 :           arguments[argument] = m_terms[m_stream.read_bits(term_index_width())];
     268             :         }
     269             : 
     270             :         // Transform the resulting term.
     271       32689 :         aterm transformed = m_transformer(aterm_appl(symbol, arguments.begin(), arguments.end()));
     272             : 
     273       19017 :         if (packet == packet_type::aterm_output)
     274             :         {
     275             :           // This aterm was marked as output in the file so return it.
     276        5345 :           return transformed;
     277             :         }
     278             :         else
     279             :         {
     280             :           // Construct the term appl from the function symbol and the already read arguments and insert it.
     281       13672 :           m_terms.emplace_back(transformed);
     282       13672 :           m_term_index_width = static_cast<unsigned int>(std::log2(m_terms.size()) + 1);
     283             :         }
     284             :       }
     285             :     }
     286       18361 :   }
     287             : }
     288             : 
     289       30442 : unsigned int binary_aterm_istream::term_index_width()
     290             : {
     291       30442 :   assert(m_term_index_width == static_cast<unsigned int>(std::log2(m_terms.size()) + 1));
     292       30442 :   return m_term_index_width;
     293             : }
     294             : 
     295       19137 : unsigned int binary_aterm_istream::function_symbol_index_width()
     296             : {
     297       19137 :   assert(m_function_symbol_index_width == static_cast<unsigned int>(std::log2(m_function_symbols.size()) + 1));
     298       19137 :   return m_function_symbol_index_width;
     299             : }
     300             : 
     301           6 : void write_term_to_binary_stream(const aterm& t, std::ostream& os)
     302             : {
     303           6 :   binary_aterm_ostream(os) << t;
     304           6 : }
     305             : 
     306           6 : aterm read_term_from_binary_stream(std::istream& is)
     307             : {
     308           6 :   return binary_aterm_istream(is).get();
     309             : }
     310             : 
     311         423 : } // namespace atermpp

Generated by: LCOV version 1.13