evaluation function of interpreter const again

passes a pointer to the main messaget to the interpreter

Author: mgudemann

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -428,7 +428,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("interpreter"))
     {
       status() << "Starting interpreter" << eom;
-      interpreter(symbol_table, goto_functions, get_message_handler());
+      interpreter(symbol_table, goto_functions, this);
       return 0;
     }
 

src/goto-programs/interpreter.cpp

@@ -41,17 +41,17 @@ Function: interpretert::operator()
 void interpretert::operator()()
 {
   show=true;
-  status() << "Initialize:" << eom;
+  message->status() << "Initialize:" << messaget::eom;
   initialise(true);
   try
   {
     std::cout << "Type h for help" << std::endl;
     while(!done) command();
-    status() << "Program End." << messaget::endl << eom;
+    message->status() << "Program End." << messaget::endl << messaget::eom;
   }
   catch (const char *e)
   {
-    error() << e << messaget::endl << eom;
+    message->error() << e << messaget::endl << messaget::eom;
   }
   while(!done) command();
 }
@@ -119,19 +119,19 @@ Function: interpretert::show_state
 void interpretert::show_state()
 {
   if(!show) return;
-  status() << messaget::endl << eom;
-  status() << "----------------------------------------------------"
-           << messaget::endl << eom;
+  message->status() << messaget::endl << messaget::eom;
+  message->status() << "----------------------------------------------------"
+           << messaget::endl << messaget::eom;
 
   if(PC==function->second.body.instructions.end())
   {
-      status() << "End of function `"
+      message->status() << "End of function `"
               << function->first << "'" << messaget::endl;
   }
   else
-    function->second.body.output_instruction(ns, function->first, status(), PC);
+    function->second.body.output_instruction(ns, function->first, message->status(), PC);
 
-  status() << eom;
+  message->status() << messaget::eom;
 }
 
 /*******************************************************************\
@@ -210,7 +210,7 @@ void interpretert::command()
         return;
       }
     }
-    json_steps.output(result());
+    json_steps.output(message->result());
   }
   else if(ch=='m')
   {
@@ -231,7 +231,7 @@ void interpretert::command()
         return;
       }
     }
-    steps.output(ns, result());
+    steps.output(ns, message->result());
   }
   else if(ch=='r')
   {
@@ -470,8 +470,8 @@ void interpretert::execute_other()
     unsigned 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 << ")" << messaget::endl << eom;
+      message->error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
+                      << size << ")" << messaget::endl << messaget::eom;
     else
     {
       assign(address, rhs);
@@ -682,8 +682,8 @@ exprt interpretert::get_value(const typet &type, std::vector<mp_integer> &rhs,un
       index_exprt index_expr(symbol_expr,from_integer(cell.offset, integer_typet()));
       return index_expr;
     }
-    error() << "pointer out of memory " << rhs[offset] << ">"
-                    << memory.size() << messaget::endl << eom;
+    message->error() << "pointer out of memory " << rhs[offset] << ">"
+                    << memory.size() << messaget::endl << messaget::eom;
     throw "pointer out of memory";
   }
   return from_integer(rhs[offset], type);
@@ -715,8 +715,8 @@ void interpretert::execute_assign()
     unsigned size=get_size(code_assign.lhs().type());
 
     if(size!=rhs.size())
-      error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
-                      << size << ")" << messaget::endl << eom;
+      message->error() << "!! failed to obtain rhs (" << rhs.size() << " vs. "
+                      << size << ")" << messaget::endl << messaget::eom;
     else
     {
       goto_trace_stept &trace_step=steps.get_last_step();
@@ -770,8 +770,8 @@ void interpretert::assign(
     {
       memory_cellt &cell=memory[integer2unsigned(address)];
       if(show) {
-        status() << "** assigning " << cell.identifier << "["
-            << cell.offset << "]:=" << rhs[i] << messaget::endl << eom;
+        message->status() << "** assigning " << cell.identifier << "["
+            << cell.offset << "]:=" << rhs[i] << messaget::endl << messaget::eom;
       }
       cell.value=rhs[i];
       if(cell.initialised==0) cell.initialised=1;
@@ -816,7 +816,7 @@ void interpretert::execute_assert()
     if ((targetAssert==PC) || stop_on_assertion)
       throw "assertion failed";
     else if (show)
-      error() << "assertion failed" << messaget::endl << eom;
+      message->error() << "assertion failed" << messaget::endl << messaget::eom;
   }
 }
 
@@ -940,7 +940,7 @@ void interpretert::execute_function_call()
       return;
     }
     if (show)
-      error() << "no body for "+id2string(identifier) << eom;//TODO:used to be throw. need some better approach? need to check state of buffers (and by refs)
+      message->error() << "no body for "+id2string(identifier) << messaget::eom;//TODO:used to be throw. need some better approach? need to check state of buffers (and by refs)
   }
 }
 
@@ -1154,13 +1154,13 @@ void interpretert::list_non_bodied() {
     }
   }
 
-  result() << "non bodied varibles " << funcs << messaget::endl << eom;
+  message->result() << "non bodied varibles " << funcs << messaget::endl << messaget::eom;
   std::map<const irep_idt,const irep_idt>::const_iterator it;
 /*for(it=function_input_vars.begin(); it!=function_input_vars.end(); it++)
   {
-    message.result() << it->first << "=" << it->second.front() << messaget::endl;
+    message->result() << it->first << "=" << it->second.front() << messaget::endl;
   }*/
-  result() << eom;
+  message->result() << messaget::eom;
 }
 
 char interpretert::is_opaque_function(const goto_programt::instructionst::const_iterator &it, irep_idt &id)
@@ -1345,10 +1345,10 @@ void interpretert::print_inputs() {
     list_inputs();
   for(input_varst::iterator it=input_vars.begin();it!=input_vars.end();
       it++) {
-    result() << it->first << "=" << from_expr(ns, it->first, it->second)
-             << "[" << it->second.type().id() << "]" << messaget::endl << eom;
+    message->result() << it->first << "=" << from_expr(ns, it->first, it->second)
+             << "[" << it->second.type().id() << "]" << messaget::endl << messaget::eom;
   }
-  result() << eom;
+  message->result() << messaget::eom;
 }
 
 /*******************************************************************
@@ -1365,10 +1365,10 @@ void interpretert::print_memory(bool input_flags) {
   for(unsigned i=0;i<memory.size();i++)
   {
     memory_cellt &cell=memory[i];
-    debug() << cell.identifier << "[" << cell.offset << "]"
-            << "=" << cell.value << eom;
-    if(input_flags) debug() << "(" << (int)cell.initialised << ")" << eom;
-    debug() << messaget::endl << eom;
+    message->debug() << cell.identifier << "[" << cell.offset << "]"
+            << "=" << cell.value << messaget::eom;
+    if(input_flags) message->debug() << "(" << (int)cell.initialised << ")" << messaget::eom;
+    message->debug() << messaget::endl << messaget::eom;
   }
 }
 
@@ -1447,7 +1447,7 @@ void interpretert::prune_inputs(input_varst &inputs,list_input_varst& function_i
     }
     catch (const char *e)
     {
-      error() << e << messaget::endl << eom;
+      message->error() << e << messaget::endl << messaget::eom;
     }
     list_inputs();
     list_inputs(inputs);
@@ -1667,8 +1667,8 @@ void interpretert::get_value_tree(const irep_idt& capture_symbol,
   auto findit=inputs.find(capture_symbol);
   if(findit==inputs.end())
   {
-    error() << "Stub method returned without defining " << capture_symbol
-            << ". Did the program trace end inside a stub?\n" << eom;
+    message->error() << "Stub method returned without defining " << capture_symbol
+            << ". Did the program trace end inside a stub?\n" << messaget::eom;
     return;
   }
 
@@ -1841,7 +1841,7 @@ Function: interpreter
 void interpreter(
   const symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
-  message_handlert &message_handler)
+  messaget *message_handler)
 {
   interpretert interpreter(symbol_table,goto_functions,message_handler);
   interpreter();

src/goto-programs/interpreter.h

@@ -16,6 +16,6 @@ Author: Daniel Kroening, [email protected]
 void interpreter(
   const symbol_tablet &symbol_table,
   const goto_functionst &goto_functions,
-  message_handlert &message_handler);
+  messaget *);
 
 #endif

src/goto-programs/interpreter_class.h

@@ -15,18 +15,19 @@
 
 \*******************************************************************/
 
-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),
+    messaget *_message_handler):
   symbol_table(_symbol_table),
   ns(_symbol_table),
-  goto_functions(_goto_functions)
+    goto_functions(_goto_functions)
   {
+        message = _message_handler;
+
   }
 
   void operator()();
@@ -60,6 +61,7 @@ class interpretert:public messaget
   const namespacet ns;
   const goto_functionst &goto_functions;
   typedef std::map<const irep_idt,const typet> dynamic_typest;
+  messaget *message;
   mutable dynamic_typest dynamic_types;
   mutable memory_mapt memory_map;
 
@@ -142,7 +144,7 @@ class interpretert:public messaget
   int stack_depth;
   int thread_id;
 
-  bool evaluate_boolean(const exprt &expr)
+  bool evaluate_boolean(const exprt &expr) const
   {
     std::vector<mp_integer> v;
     evaluate(expr, v);
@@ -161,9 +163,9 @@ class interpretert:public messaget
 
   void evaluate(
     const exprt &expr,
-    std::vector<mp_integer> &dest);
+    std::vector<mp_integer> &dest) const;
 
-  mp_integer evaluate_address(const exprt &expr);
+  mp_integer evaluate_address(const exprt &expr) const;
 
   void initialise(bool init);
   void show_state();

src/goto-programs/interpreter_evaluate.cpp

@@ -197,7 +197,7 @@ Function: interpretert::evaluate
 
 void interpretert::evaluate(
   const exprt &expr,
-  std::vector<mp_integer> &dest)
+  std::vector<mp_integer> &dest) const
 {
   if(expr.id()==ID_constant)
   {
@@ -269,7 +269,7 @@ void interpretert::evaluate(
       irep_idt value=to_constant_expr(expr).get_value();
       const char *str=value.c_str();
       unsigned length=strlen(str)+1;
-      if (show) warning() << "string decoding not fully implemented " << length << messaget::endl << eom;
+      if (show) message->warning() << "string decoding not fully implemented " << length << messaget::endl << messaget::eom;
       mp_integer tmp=value.get_no();
       dest.push_back(tmp);
       return;
@@ -318,12 +318,12 @@ void interpretert::evaluate(
     side_effect_exprt side_effect=to_side_effect_expr(expr);
     if(side_effect.get_statement()==ID_nondet)
     {
-      if (show) error() << "nondet not implemented" << messaget::endl << eom;
+      if (show) message->error() << "nondet not implemented" << messaget::endl << messaget::eom;
       return;
     }
     else if(side_effect.get_statement()==ID_malloc)
     {
-      if (show) error() << "malloc not fully implemented " << expr.type().subtype().pretty() << messaget::endl << eom;
+      if (show) message->error() << "malloc not fully implemented " << expr.type().subtype().pretty() << messaget::endl << messaget::eom;
       std::stringstream buffer;
       num_dynamic_objects++;
       buffer <<"symex_dynamic::dynamic_object" << num_dynamic_objects;
@@ -332,7 +332,7 @@ void interpretert::evaluate(
      dest.push_back(address);
       return;
     }
-    if (show) error() << "side effect not implemented " << side_effect.get_statement() << messaget::endl << eom;
+    if (show) message->error() << "side effect not implemented " << side_effect.get_statement() << messaget::endl << messaget::eom;
   }
   else if(expr.id()==ID_bitor)
   {
@@ -835,10 +835,10 @@ void interpretert::evaluate(
     return;
   }
 //  if (!show) return;
-  error() << "!! failed to evaluate expression: "
+  message->error() << "!! failed to evaluate expression: "
             << from_expr(ns, function->first, expr)
-          << messaget::endl << eom;
-  error() << expr.id() << "[" << expr.type().id() << "]" << messaget::endl << eom;
+          << messaget::endl << messaget::eom;
+  message->error() << expr.id() << "[" << expr.type().id() << "]" << messaget::endl << messaget::eom;
 }
 
 /*******************************************************************\
@@ -853,7 +853,7 @@ Function: interpretert::evaluate_address
 
 \*******************************************************************/
 
-mp_integer interpretert::evaluate_address(const exprt &expr)
+mp_integer interpretert::evaluate_address(const exprt &expr) const
 {
   if(expr.id()==ID_symbol)
   {
@@ -938,9 +938,9 @@ mp_integer interpretert::evaluate_address(const exprt &expr)
 
   if (show)
   {
-    error() << "!! failed to evaluate address: "
+    message->error() << "!! failed to evaluate address: "
               << from_expr(ns, function->first, expr)
-              << messaget::endl << eom;
+              << messaget::endl << messaget::eom;
   }
   return 0;
 }

src/test_gen/java_test_case_generator.cpp

@@ -25,7 +25,7 @@ bool java_test_case_generatort::is_meta(const irep_idt &id)
 inputst java_test_case_generatort::generate_inputs(const symbol_tablet &st, const goto_functionst &gf,
                         const goto_tracet &trace, interpretert::list_input_varst& opaque_function_returns)
 {
-  interpretert interpreter(st, gf, get_message_handler());
+  interpretert interpreter(st, gf, this);
   inputst res(interpreter.load_counter_example_inputs(trace, opaque_function_returns));
   for (inputst::const_iterator it(res.begin()); it != res.end();)
     if (is_meta(it->first)) it=res.erase(it);