Merge pull request #4916 from MatWise/bugfix/stl-goto-conversion

STL frontend: Fix goto conversion issues

Author: pkesseli

src/goto-programs/goto_convert_functions.cpp

@@ -22,8 +22,8 @@ Date: June 2003
 
 goto_convert_functionst::goto_convert_functionst(
   symbol_table_baset &_symbol_table,
-  message_handlert &_message_handler):
-  goto_convertt(_symbol_table, _message_handler)
+  message_handlert &_message_handler)
+  : goto_convertt(_symbol_table, _message_handler)
 {
 }
 
@@ -44,7 +44,9 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
       !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
       symbol_pair.second.type.id() == ID_code &&
       (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
-       symbol_pair.second.mode == ID_java || symbol_pair.second.mode == "jsil"))
+       symbol_pair.second.mode == ID_java ||
+       symbol_pair.second.mode == "jsil" ||
+       symbol_pair.second.mode == ID_statement_list))
     {
       symbol_list.push_back(symbol_pair.first);
     }
@@ -57,8 +59,8 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
 
   functions.compute_location_numbers();
 
-  // this removes the parse tree of the bodies from memory
-  #if 0
+// this removes the parse tree of the bodies from memory
+#if 0
   for(const auto &symbol_pair, symbol_table.symbols)
   {
     if(!symbol_pair.second.is_type &&
@@ -68,7 +70,7 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
       symbol_pair.second.value=codet();
     }
   }
-  #endif
+#endif
 }
 
 bool goto_convert_functionst::hide(const goto_programt &goto_program)
@@ -87,7 +89,7 @@ void goto_convert_functionst::add_return(
   goto_functionst::goto_functiont &f,
   const source_locationt &source_location)
 {
-  #if 0
+#if 0
   if(!f.body.instructions.empty() &&
      f.body.instructions.back().is_return())
     return; // not needed, we have one already
@@ -97,12 +99,11 @@ void goto_convert_functionst::add_return(
      f.body.instructions.back().is_goto() &&
      f.body.instructions.back().guard.is_true())
     return;
-  #else
+#else
 
   if(!f.body.instructions.empty())
   {
-    goto_programt::const_targett last_instruction=
-      f.body.instructions.end();
+    goto_programt::const_targett last_instruction = f.body.instructions.end();
     last_instruction--;
 
     while(true)
@@ -120,16 +121,17 @@ void goto_convert_functionst::add_return(
         return;
 
       // advance if it's a 'dead' without branch target
-      if(last_instruction->is_dead() &&
-         last_instruction!=f.body.instructions.begin() &&
-         !last_instruction->is_target())
+      if(
+        last_instruction->is_dead() &&
+        last_instruction != f.body.instructions.begin() &&
+        !last_instruction->is_target())
         last_instruction--;
       else
         break; // give up
     }
   }
 
-  #endif
+#endif
 
   side_effect_expr_nondett rhs(f.type.return_type(), source_location);
 
@@ -141,22 +143,23 @@ void goto_convert_functionst::convert_function(
   const irep_idt &identifier,
   goto_functionst::goto_functiont &f)
 {
-  const symbolt &symbol=ns.lookup(identifier);
+  const symbolt &symbol = ns.lookup(identifier);
   const irep_idt mode = symbol.mode;
 
   if(f.body_available())
     return; // already converted
 
   // make tmp variables local to function
-  tmp_symbol_prefix=id2string(symbol.name)+"::$tmp";
+  tmp_symbol_prefix = id2string(symbol.name) + "::$tmp";
 
   // store the parameter identifiers in the goto functions
   const code_typet &code_type = to_code_type(symbol.type);
   f.type = code_type;
   f.set_parameter_identifiers(code_type);
 
-  if(symbol.value.is_nil() ||
-     symbol.is_compiled()) /* goto_inline may have removed the body */
+  if(
+    symbol.value.is_nil() ||
+    symbol.is_compiled()) /* goto_inline may have removed the body */
     return;
 
   // we have a body, make sure all parameter names are valid
@@ -172,25 +175,24 @@ void goto_convert_functionst::convert_function(
   lifetime = identifier == INITIALIZE_FUNCTION ? lifetimet::STATIC_GLOBAL
                                                : lifetimet::AUTOMATIC_LOCAL;
 
-  const codet &code=to_code(symbol.value);
+  const codet &code = to_code(symbol.value);
 
   source_locationt end_location;
 
-  if(code.get_statement()==ID_block)
-    end_location=to_code_block(code).end_location();
+  if(code.get_statement() == ID_block)
+    end_location = to_code_block(code).end_location();
   else
     end_location.make_nil();
 
   goto_programt tmp_end_function;
   goto_programt::targett end_function =
     tmp_end_function.add(goto_programt::make_end_function(end_location));
 
-  targets=targetst();
+  targets = targetst();
   targets.set_return(end_function);
-  targets.has_return_value=
-    f.type.return_type().id()!=ID_empty &&
-    f.type.return_type().id()!=ID_constructor &&
-    f.type.return_type().id()!=ID_destructor;
+  targets.has_return_value = f.type.return_type().id() != ID_empty &&
+                             f.type.return_type().id() != ID_constructor &&
+                             f.type.return_type().id() != ID_destructor;
 
   goto_convert_rec(code, f.body, mode);
 
@@ -199,12 +201,13 @@ void goto_convert_functionst::convert_function(
     add_return(f, end_location);
 
   // handle SV-COMP's __VERIFIER_atomic_
-  if(!f.body.instructions.empty() &&
-      has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
+  if(
+    !f.body.instructions.empty() &&
+    has_prefix(id2string(identifier), "__VERIFIER_atomic_"))
   {
     goto_programt::instructiont a_begin;
     a_begin = goto_programt::make_atomic_begin();
-    a_begin.source_location=f.body.instructions.front().source_location;
+    a_begin.source_location = f.body.instructions.front().source_location;
     f.body.insert_before_swap(f.body.instructions.begin(), a_begin);
 
     goto_programt::targett a_end =
@@ -231,9 +234,7 @@ void goto_convert_functionst::convert_function(
   lifetime = parent_lifetime;
 }
 
-void goto_convert(
-  goto_modelt &goto_model,
-  message_handlert &message_handler)
+void goto_convert(goto_modelt &goto_model, message_handlert &message_handler)
 {
   symbol_table_buildert symbol_table_builder =
     symbol_table_buildert::wrap(goto_model.symbol_table);

src/statement-list/statement_list_entry_point.cpp

@@ -108,7 +108,7 @@ static void add_main_function_block_call(
     id2string(data_block_interface.get_base_name()) + DB_ENTRY_POINT_POSTFIX;
   instance_data_block.type = data_block_interface.type().subtype();
   instance_data_block.is_static_lifetime = true;
-  instance_data_block.mode = STATEMENT_LIST_MODE;
+  instance_data_block.mode = ID_statement_list;
   symbol_table.add(instance_data_block);
   const address_of_exprt data_block_ref{instance_data_block.symbol_expr()};
 
@@ -124,6 +124,7 @@ static void generate_statement_list_init_function(symbol_tablet &symbol_table)
 {
   symbolt init;
   init.name = INITIALIZE_FUNCTION;
+  init.mode = ID_statement_list;
   init.type = code_typet({}, empty_typet{});
 
   code_blockt dest;

src/statement-list/statement_list_typecheck.cpp

@@ -118,7 +118,7 @@ void statement_list_typecheckt::typecheck_function_block_declaration(
   function_block_sym.name = function_block.name;
   function_block_sym.base_name = function_block_sym.name;
   function_block_sym.pretty_name = function_block_sym.name;
-  function_block_sym.mode = STATEMENT_LIST_MODE;
+  function_block_sym.mode = ID_statement_list;
 
   // When calling function blocks, the passed parameters are value-copied to a
   // corresponding instance data block. This block contains all input, inout,
@@ -134,7 +134,7 @@ void statement_list_typecheckt::typecheck_function_block_declaration(
   data_block.name =
     id2string(function_block_sym.name) + DATA_BLOCK_TYPE_POSTFIX;
   data_block.base_name = data_block.name;
-  data_block.mode = STATEMENT_LIST_MODE;
+  data_block.mode = ID_statement_list;
   symbol_table.add(data_block);
 
   // Create and add parameter symbol.
@@ -146,7 +146,7 @@ void statement_list_typecheckt::typecheck_function_block_declaration(
   param_sym.name = param.get_identifier();
   param_sym.base_name = DATA_BLOCK_PARAMETER_NAME;
   param_sym.pretty_name = param_sym.base_name;
-  param_sym.mode = STATEMENT_LIST_MODE;
+  param_sym.mode = ID_statement_list;
   symbol_table.add(param_sym);
 
   // Setup FB symbol type and value.
@@ -166,7 +166,7 @@ void statement_list_typecheckt::typecheck_function_declaration(
   function_sym.name = function.name;
   function_sym.base_name = function_sym.name;
   function_sym.pretty_name = function_sym.name;
-  function_sym.mode = STATEMENT_LIST_MODE;
+  function_sym.mode = ID_statement_list;
   code_typet::parameterst params;
   typecheck_function_var_decls(
     function.var_input, params, function.name, ID_statement_list_var_input);
@@ -192,7 +192,7 @@ void statement_list_typecheckt::typecheck_tag_list()
     tag_sym.base_name = tag_sym.name;
     tag_sym.pretty_name = tag_sym.name;
     tag_sym.type = tag.type();
-    tag_sym.mode = STATEMENT_LIST_MODE;
+    tag_sym.mode = ID_statement_list;
     symbol_table.add(tag_sym);
   }
 }
@@ -245,7 +245,7 @@ void statement_list_typecheckt::typecheck_function_var_decls(
                      "::" + id2string(declaration.variable.get_identifier());
     param_sym.base_name = declaration.variable.get_identifier();
     param_sym.pretty_name = param_sym.base_name;
-    param_sym.mode = STATEMENT_LIST_MODE;
+    param_sym.mode = ID_statement_list;
     symbol_table.add(param_sym);
 
     code_typet::parametert param{declaration.variable.type()};
@@ -269,7 +269,7 @@ void statement_list_typecheckt::typecheck_temp_var_decls(
     temp_sym.base_name = declaration.variable.get_identifier();
     temp_sym.pretty_name = temp_sym.base_name;
     temp_sym.type = declaration.variable.type();
-    temp_sym.mode = STATEMENT_LIST_MODE;
+    temp_sym.mode = ID_statement_list;
     temp_sym.module = module;
     symbol_table.add(temp_sym);
 

src/statement-list/statement_list_typecheck.h

@@ -17,8 +17,6 @@ Author: Matthias Weiss, [email protected]
 
 #include "statement_list_parse_tree.h"
 
-#define STATEMENT_LIST_MODE "Statement List"
-
 /// Create a new statement_list_typecheckt object and perform a type check to
 /// fill the symbol table.
 /// \param parse_tree: Parse tree generated by parsing a Statement List file.

src/util/irep_ids.def

@@ -762,6 +762,7 @@ IREP_ID_ONE(__sync_or_and_fetch)
 IREP_ID_ONE(__sync_sub_and_fetch)
 IREP_ID_ONE(__sync_val_compare_and_swap)
 IREP_ID_ONE(__sync_xor_and_fetch)
+IREP_ID_TWO(statement_list, Statement List)
 IREP_ID_ONE(statement_list_type)
 IREP_ID_ONE(statement_list_function)
 IREP_ID_ONE(statement_list_function_block)