Merge pull request #2111 from peterschrammel/bugfix/missing-java-modes

Missing language modes

Author: peterschrammel

src/goto-programs/builtin_functions.cpp

@@ -468,8 +468,8 @@ void goto_convertt::do_cpp_new(
     assert(code_type.parameters().size()==1 ||
            code_type.parameters().size()==2);
 
-    const symbolt &tmp_symbol=
-      new_tmp_symbol(return_type, "new", dest, rhs.source_location());
+    const symbolt &tmp_symbol =
+      new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
 
     tmp_symbol_expr=tmp_symbol.symbol_expr();
 
@@ -499,8 +499,8 @@ void goto_convertt::do_cpp_new(
     assert(code_type.parameters().size()==2 ||
            code_type.parameters().size()==3);
 
-    const symbolt &tmp_symbol=
-      new_tmp_symbol(return_type, "new", dest, rhs.source_location());
+    const symbolt &tmp_symbol =
+      new_tmp_symbol(return_type, "new", dest, rhs.source_location(), ID_cpp);
 
     tmp_symbol_expr=tmp_symbol.symbol_expr();
 
@@ -663,13 +663,10 @@ void goto_convertt::do_java_new_array(
   // Must directly assign the new array to a temporary
   // because goto-symex will notice `x=side_effect_exprt` but not
   // `x=typecast_exprt(side_effect_exprt(...))`
-  symbol_exprt new_array_data_symbol=
+  symbol_exprt new_array_data_symbol =
     new_tmp_symbol(
-      data_java_new_expr.type(),
-      "new_array_data",
-      dest,
-      location)
-    .symbol_expr();
+      data_java_new_expr.type(), "new_array_data", dest, location, ID_java)
+      .symbol_expr();
   goto_programt::targett t_p2=dest.add_instruction(ASSIGN);
   t_p2->code=code_assignt(new_array_data_symbol, data_java_new_expr);
   t_p2->source_location=location;
@@ -707,8 +704,9 @@ void goto_convertt::do_java_new_array(
 
     goto_programt tmp;
 
-    symbol_exprt tmp_i=
-      new_tmp_symbol(length.type(), "index", tmp, location).symbol_expr();
+    symbol_exprt tmp_i =
+      new_tmp_symbol(length.type(), "index", tmp, location, ID_java)
+        .symbol_expr();
 
     code_fort for_loop;
 
@@ -730,8 +728,9 @@ void goto_convertt::do_java_new_array(
       plus_exprt(data, tmp_i), data.type().subtype());
 
     code_blockt for_body;
-    symbol_exprt init_sym=
-      new_tmp_symbol(sub_type, "subarray_init", tmp, location).symbol_expr();
+    symbol_exprt init_sym =
+      new_tmp_symbol(sub_type, "subarray_init", tmp, location, ID_java)
+        .symbol_expr();
 
     code_assignt init_subarray(init_sym, sub_java_new);
     code_assignt assign_subarray(

src/goto-programs/goto_clean_expr.cpp

@@ -237,8 +237,8 @@ void goto_convertt::clean_expr(
 
     if(result_is_used)
     {
-      symbolt &new_symbol=
-        new_tmp_symbol(expr.type(), "if_expr", dest, source_location);
+      symbolt &new_symbol = new_tmp_symbol(
+        expr.type(), "if_expr", dest, source_location, expr.get(ID_mode));
 
       code_assignt assignment_true;
       assignment_true.lhs()=new_symbol.symbol_expr();

src/goto-programs/goto_convert.cpp

@@ -2055,16 +2055,16 @@ symbolt &goto_convertt::new_tmp_symbol(
   const typet &type,
   const std::string &suffix,
   goto_programt &dest,
-  const source_locationt &source_location)
+  const source_locationt &source_location,
+  const irep_idt &mode)
 {
-  symbolt &new_symbol=
-    get_fresh_aux_symbol(
-      type,
-      tmp_symbol_prefix,
-      "tmp_"+suffix,
-      source_location,
-      irep_idt(),
-      symbol_table);
+  symbolt &new_symbol = get_fresh_aux_symbol(
+    type,
+    tmp_symbol_prefix,
+    "tmp_" + suffix,
+    source_location,
+    mode,
+    symbol_table);
 
   code_declt decl;
   decl.symbol()=new_symbol.symbol_expr();
@@ -2081,8 +2081,8 @@ void goto_convertt::make_temp_symbol(
 {
   const source_locationt source_location=expr.find_source_location();
 
-  symbolt &new_symbol=
-    new_tmp_symbol(expr.type(), suffix, dest, source_location);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(), suffix, dest, source_location, expr.get(ID_mode));
 
   code_assignt assignment;
   assignment.lhs()=new_symbol.symbol_expr();

src/goto-programs/goto_convert_class.h

@@ -59,7 +59,8 @@ class goto_convertt:public messaget
     const typet &type,
     const std::string &suffix,
     goto_programt &dest,
-    const source_locationt &);
+    const source_locationt &,
+    const irep_idt &mode);
 
   symbol_exprt make_compound_literal(
     const exprt &expr,

src/goto-programs/goto_convert_side_effect.cpp

@@ -522,10 +522,8 @@ void goto_convertt::remove_temporary_object(
     throw 0;
   }
 
-  symbolt &new_symbol=
-    new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location());
-
-  new_symbol.mode=expr.get(ID_mode);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(), "obj", dest, expr.find_source_location(), expr.get(ID_mode));
 
   if(expr.operands().size()==1)
   {
@@ -599,8 +597,12 @@ void goto_convertt::remove_statement_expression(
 
   source_locationt source_location=last.find_source_location();
 
-  symbolt &new_symbol=
-    new_tmp_symbol(expr.type(), "statement_expression", dest, source_location);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(),
+    "statement_expression",
+    dest,
+    source_location,
+    expr.get(ID_mode));
 
   symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
   tmp_symbol_expr.add_source_location()=source_location;

src/goto-symex/symex_builtin_functions.cpp

@@ -66,6 +66,9 @@ void goto_symext::symex_allocate(
 
   exprt size=code.op0();
   typet object_type=nil_typet();
+  auto function_symbol = outer_symbol_table.lookup(state.source.pc->function);
+  INVARIANT(function_symbol, "function associated with instruction not found");
+  const irep_idt &mode = function_symbol->mode;
 
   // is the type given?
   if(code.type().id()==ID_pointer && code.type().subtype().id()!=ID_empty)
@@ -142,7 +145,7 @@ void goto_symext::symex_allocate(
       size_symbol.name="symex_dynamic::"+id2string(size_symbol.base_name);
       size_symbol.is_lvalue=true;
       size_symbol.type=tmp_size.type();
-      size_symbol.mode=ID_C;
+      size_symbol.mode = mode;
 
       state.symbol_table.add(size_symbol);
 
@@ -161,7 +164,7 @@ void goto_symext::symex_allocate(
   value_symbol.is_lvalue=true;
   value_symbol.type=object_type;
   value_symbol.type.set("#dynamic", true);
-  value_symbol.mode=ID_C;
+  value_symbol.mode = mode;
 
   state.symbol_table.add(value_symbol);
 

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -740,6 +740,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     symbol.base_name=symbol_type.get(ID_C_base_name);
     symbol.is_type=true;
     symbol.type = class_type;
+    symbol.mode = ID_java;
     symbol_table.add(symbol);
 
     // Also provide a clone method:

src/java_bytecode/java_bytecode_typecheck_type.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "java_bytecode_typecheck.h"
 
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 void java_bytecode_typecheckt::typecheck_type(typet &type)
@@ -19,17 +20,12 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
   {
     irep_idt identifier=to_symbol_type(type).get_identifier();
 
-    symbol_tablet::symbolst::const_iterator s_it=
-      symbol_table.symbols.find(identifier);
-
-    // must exist already in the symbol table
-    if(s_it==symbol_table.symbols.end())
-    {
-      error() << "failed to find type symbol "<< identifier << eom;
-      throw 0;
-    }
-
-    assert(s_it->second.is_type);
+    auto type_symbol = symbol_table.lookup(identifier);
+    DATA_INVARIANT(
+      type_symbol, "symbol " + id2string(identifier) + " must exist already");
+    DATA_INVARIANT(
+      type_symbol->is_type,
+      "symbol " + id2string(identifier) + " must be a type");
   }
   else if(type.id()==ID_pointer)
   {
@@ -55,7 +51,9 @@ void java_bytecode_typecheckt::typecheck_type(typet &type)
 
 void java_bytecode_typecheckt::typecheck_type_symbol(symbolt &symbol)
 {
-  assert(symbol.is_type);
+  DATA_INVARIANT(
+    symbol.is_type, "symbol " + id2string(symbol.name) + " must be a type");
 
+  symbol.mode = ID_java;
   typecheck_type(symbol.type);
 }

src/java_bytecode/java_string_library_preprocess.cpp

@@ -247,6 +247,7 @@ void java_string_library_preprocesst::add_string_type(
   string_symbol->pretty_name=id2string(class_name);
   string_symbol->type=string_type;
   string_symbol->is_type=true;
+  string_symbol->mode = ID_java;
 }
 
 /// add a symbol in the table with static lifetime and name containing

unit/testing-utils/load_java_class.cpp

@@ -16,6 +16,8 @@
 
 #include <goto-programs/lazy_goto_model.h>
 
+#include <langapi/mode.h>
+
 #include <java_bytecode/java_bytecode_language.h>
 #include <util/file_util.h>
 
@@ -37,11 +39,13 @@ symbol_tablet load_java_class_lazy(
   free_form_cmdlinet lazy_command_line;
   lazy_command_line.add_flag("lazy-methods");
 
+  register_language(new_java_bytecode_language);
+
   return load_java_class(
     java_class_name,
     class_path,
     main,
-    new_java_bytecode_language(),
+    get_language_from_mode(ID_java),
     lazy_command_line);
 }
 
@@ -59,8 +63,10 @@ symbol_tablet load_java_class(
   const std::string &class_path,
   const std::string &main)
 {
+  register_language(new_java_bytecode_language);
+
   return load_java_class(
-    java_class_name, class_path, main, new_java_bytecode_language());
+    java_class_name, class_path, main, get_language_from_mode(ID_java));
 }
 
 /// Go through the process of loading, type-checking and finalising loading a