Merge pull request #5595 from tautschnig/messaget-interpreter

interpretert isn't a messaget

Author: tautschnig

src/goto-programs/interpreter.cpp

@@ -39,20 +39,20 @@ const std::size_t interpretert::npos=std::numeric_limits<size_t>::max();
 
 void interpretert::operator()()
 {
-  status() << "0- Initialize:" << eom;
+  output.status() << "0- Initialize:" << messaget::eom;
   initialize(true);
   try
   {
-    status() << "Type h for help\n" << eom;
+    output.status() << "Type h for help\n" << messaget::eom;
 
     while(!done)
       command();
 
-    status() << total_steps << "- Program End.\n" << eom;
+    output.status() << total_steps << "- Program End.\n" << messaget::eom;
   }
   catch (const char *e)
   {
-    error() << e << "\n" << eom;
+    output.error() << e << "\n" << messaget::eom;
   }
 
   while(!done)
@@ -113,22 +113,19 @@ void interpretert::show_state()
 {
   if(!show)
     return;
-  status() << "\n"
-           << total_steps+1
-           << " ----------------------------------------------------\n";
+  output.status() << "\n"
+                  << total_steps + 1
+                  << " ----------------------------------------------------\n";
 
   if(pc==function->second.body.instructions.end())
   {
-    status() << "End of function '" << function->first << "'\n";
+    output.status() << "End of function '" << function->first << "'\n";
   }
   else
     function->second.body.output_instruction(
-      ns,
-      function->first,
-      status(),
-      *pc);
+      ns, function->first, output.status(), *pc);
 
-  status() << eom;
+  output.status() << messaget::eom;
 }
 
 /// reads a user command and executes it.
@@ -147,18 +144,18 @@ void interpretert::command()
     done=true;
   else if(ch=='h')
   {
-    status() << "Interpreter help\n"
-             << "h: display this menu\n"
-             << "j: output json trace\n"
-             << "m: output memory dump\n"
-             << "o: output goto trace\n"
-             << "q: quit\n"
-             << "r: run up to entry point\n"
-             << "s#: step a number of instructions\n"
-             << "sa: step across a function\n"
-             << "so: step out of a function\n"
-             << "se: step until end of program\n"
-             << eom;
+    output.status() << "Interpreter help\n"
+                    << "h: display this menu\n"
+                    << "j: output json trace\n"
+                    << "m: output memory dump\n"
+                    << "o: output goto trace\n"
+                    << "q: quit\n"
+                    << "r: run up to entry point\n"
+                    << "s#: step a number of instructions\n"
+                    << "sa: step across a function\n"
+                    << "so: step out of a function\n"
+                    << "se: step until end of program\n"
+                    << messaget::eom;
   }
   else if(ch=='j')
   {
@@ -176,7 +173,7 @@ void interpretert::command()
         return;
       }
     }
-    json_steps.output(result());
+    json_steps.output(output.result());
   }
   else if(ch=='m')
   {
@@ -197,7 +194,7 @@ void interpretert::command()
         return;
       }
     }
-    steps.output(ns, result());
+    steps.output(ns, output.result());
   }
   else if(ch=='r')
   {
@@ -408,8 +405,9 @@ void interpretert::execute_other()
     mp_integer size=get_size(pc->code.op0().type());
     while(rhs.size()<size) rhs.insert(rhs.end(), tmp.begin(), tmp.end());
     if(size!=rhs.size())
-      error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
-              << size << ")\n" << eom;
+      output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
+                     << size << ")\n"
+                     << messaget::eom;
     else
     {
       assign(address, rhs);
@@ -637,9 +635,9 @@ exprt interpretert::get_value(
         symbol_expr, from_integer(offset_from_address, integer_typet()));
     }
 
-    error() << "interpreter: invalid pointer "
-            << rhs[numeric_cast_v<std::size_t>(offset)] << " > object count "
-            << memory.size() << eom;
+    output.error() << "interpreter: invalid pointer "
+                   << rhs[numeric_cast_v<std::size_t>(offset)]
+                   << " > object count " << memory.size() << messaget::eom;
 
     throw "interpreter: reading from invalid pointer";
   }
@@ -671,10 +669,9 @@ void interpretert::execute_assign()
     mp_integer size=get_size(code_assign.lhs().type());
 
     if(size!=rhs.size())
-      error() << "!! failed to obtain rhs ("
-              << rhs.size() << " vs. "
-              << size << ")\n"
-              << eom;
+      output.error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
+                     << size << ")\n"
+                     << messaget::eom;
     else
     {
       goto_trace_stept &trace_step=steps.get_last_step();
@@ -716,11 +713,11 @@ void interpretert::assign(
       memory_cellt &cell = memory[numeric_cast_v<std::size_t>(address_val)];
       if(show)
       {
-        status() << total_steps << " ** assigning "
-                 << address_to_symbol(address_val).get_identifier() << "["
-                 << address_to_offset(address_val)
-                 << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
-                 << eom;
+        output.status() << total_steps << " ** assigning "
+                        << address_to_symbol(address_val).get_identifier()
+                        << "[" << address_to_offset(address_val)
+                        << "]:=" << rhs[numeric_cast_v<std::size_t>(i)] << "\n"
+                        << messaget::eom;
       }
       cell.value = rhs[numeric_cast_v<std::size_t>(i)];
       if(cell.initialized==memory_cellt::initializedt::UNKNOWN)
@@ -740,8 +737,8 @@ void interpretert::execute_assert()
   if(!evaluate_boolean(pc->get_condition()))
   {
     if(show)
-      error() << "assertion failed at " << pc->location_number
-              << "\n" << eom;
+      output.error() << "assertion failed at " << pc->location_number << "\n"
+                     << messaget::eom;
   }
 }
 
@@ -847,7 +844,7 @@ void interpretert::execute_function_call()
     }
 
     if(show)
-      error() << "no body for "+id2string(identifier) << eom;
+      output.error() << "no body for " << identifier << messaget::eom;
   }
 }
 
@@ -903,16 +900,17 @@ typet interpretert::concretize_type(const typet &type)
     if(computed_size.size()==1 &&
        computed_size[0]>=0)
     {
-      result() << "Concretized array with size " << computed_size[0]
-               << eom;
+      output.result() << "Concretized array with size " << computed_size[0]
+                      << messaget::eom;
       return
         array_typet(
           type.subtype(),
           from_integer(computed_size[0], integer_typet()));
     }
     else
     {
-      warning() << "Failed to concretize variable array" << eom;
+      output.warning() << "Failed to concretize variable array"
+                       << messaget::eom;
     }
   }
   return type;
@@ -1067,11 +1065,12 @@ void interpretert::print_memory(bool input_flags)
     const memory_cellt &cell=cell_address.second;
     const auto identifier = address_to_symbol(i).get_identifier();
     const auto offset=address_to_offset(i);
-    status() << identifier << "[" << offset << "]"
-             << "=" << cell.value << eom;
+    output.status() << identifier << "[" << offset << "]"
+                    << "=" << cell.value << messaget::eom;
     if(input_flags)
-      status() << "(" << static_cast<int>(cell.initialized) << ")" << eom;
-    status() << eom;
+      output.status() << "(" << static_cast<int>(cell.initialized) << ")"
+                      << messaget::eom;
+    output.status() << messaget::eom;
   }
 }
 

src/goto-programs/interpreter.h

@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_GOTO_PROGRAMS_INTERPRETER_H
 #define CPROVER_GOTO_PROGRAMS_INTERPRETER_H
 
-#include <util/message.h>
-
 #include "goto_model.h"
 
+class message_handlert;
+
 void interpreter(
   const goto_modelt &,
   message_handlert &);

src/goto-programs/interpreter_class.h

@@ -24,14 +24,14 @@ Author: Daniel Kroening, [email protected]
 #include "goto_trace.h"
 #include "json_goto_trace.h"
 
-class interpretert:public messaget
+class interpretert
 {
 public:
   interpretert(
     const symbol_tablet &_symbol_table,
     const goto_functionst &_goto_functions,
     message_handlert &_message_handler)
-    : messaget(_message_handler),
+    : output(_message_handler),
       symbol_table(_symbol_table),
       ns(_symbol_table),
       goto_functions(_goto_functions),
@@ -97,6 +97,7 @@ class interpretert:public messaget
   const dynamic_typest &get_dynamic_types() { return dynamic_types; }
 
 protected:
+  messaget output;
   const symbol_tablet &symbol_table;
 
   // This is a cache so that we don't have to create it when a call needs it

src/goto-programs/interpreter_evaluate.cpp

@@ -404,8 +404,8 @@ void interpretert::evaluate(
     {
       const std::string &value = id2string(to_constant_expr(expr).get_value());
       if(show)
-        warning() << "string decoding not fully implemented "
-                  << value.size() + 1 << eom;
+        output.warning() << "string decoding not fully implemented "
+                         << value.size() + 1 << messaget::eom;
       dest.push_back(get_string_container()[value]);
       return;
     }
@@ -457,15 +457,14 @@ void interpretert::evaluate(
     if(side_effect.get_statement()==ID_nondet)
     {
       if(show)
-        error() << "nondet not implemented" << eom;
+        output.error() << "nondet not implemented" << messaget::eom;
       return;
     }
     else if(side_effect.get_statement()==ID_allocate)
     {
       if(show)
-        error() << "heap memory allocation not fully implemented "
-                << expr.type().subtype().pretty()
-                << eom;
+        output.error() << "heap memory allocation not fully implemented "
+                       << expr.type().subtype().pretty() << messaget::eom;
       std::stringstream buffer;
       num_dynamic_objects++;
       buffer << "interpreter::dynamic_object" << num_dynamic_objects;
@@ -478,9 +477,8 @@ void interpretert::evaluate(
       return;
     }
     if(show)
-      error() << "side effect not implemented "
-              << side_effect.get_statement()
-              << eom;
+      output.error() << "side effect not implemented "
+                     << side_effect.get_statement() << messaget::eom;
   }
   else if(expr.id()==ID_bitor)
   {
@@ -1041,14 +1039,14 @@ void interpretert::evaluate(
   {
     if(expr.type().id()==ID_signedbv)
     {
-      warning() << "Infinite size arrays not supported" << eom;
+      output.warning() << "Infinite size arrays not supported" << messaget::eom;
       return;
     }
   }
-  error() << "!! failed to evaluate expression: "
-          << from_expr(ns, function->first, expr) << "\n"
-          << expr.id() << "[" << expr.type().id() << "]"
-          << eom;
+  output.error() << "!! failed to evaluate expression: "
+                 << from_expr(ns, function->first, expr) << "\n"
+                 << expr.id() << "[" << expr.type().id() << "]"
+                 << messaget::eom;
 }
 
 mp_integer interpretert::evaluate_address(
@@ -1157,9 +1155,8 @@ mp_integer interpretert::evaluate_address(
 
   if(!fail_quietly)
   {
-    error() << "!! failed to evaluate address: "
-            << from_expr(ns, function->first, expr)
-            << eom;
+    output.error() << "!! failed to evaluate address: "
+                   << from_expr(ns, function->first, expr) << messaget::eom;
   }
 
   return 0;