use bytecode_info instead of bytecode vector

The run-time generated bytecode table is replaced by bytecode_info.  The
linear search for the mnemonic is replaced by an array access.

Author: Daniel Kroening

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -595,18 +595,6 @@ void java_bytecode_convert_methodt::convert(
       to_java_class_type(class_symbol.type).lambda_method_handles());
 }
 
-const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info(
-  const irep_idt &statement)
-{
-  for(const bytecode_infot *p=bytecode_info; p->mnemonic!=nullptr; p++)
-    if(statement==p->mnemonic)
-      return *p;
-
-  error() << "failed to find bytecode mnemonic `"
-          << statement << '\'' << eom;
-  throw 0;
-}
-
 static irep_idt get_if_cmp_operator(const irep_idt &stmt)
 {
   if(stmt==patternt("if_?cmplt"))
@@ -1012,37 +1000,29 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     // a new maximal key
     assert(a_entry.first==--address_map.end());
 
-    if(i_it->statement!="goto" &&
-       i_it->statement!="return" &&
-       !(i_it->statement==patternt("?return")) &&
-       i_it->statement!="athrow" &&
-       i_it->statement!="jsr" &&
-       i_it->statement!="jsr_w" &&
-       i_it->statement!="ret")
+    const std::string statement = bytecode_info[i_it->bytecode].mnemonic;
+
+    if(
+      statement != "goto" && statement != "return" &&
+      !(statement == patternt("?return")) && statement != "athrow" &&
+      statement != "jsr" && statement != "jsr_w" && statement != "ret")
     {
       instructionst::const_iterator next=i_it;
       if(++next!=instructions.end())
         a_entry.first->second.successors.push_back(next->address);
     }
 
-    if(i_it->statement=="athrow" ||
-       i_it->statement=="putfield" ||
-       i_it->statement=="getfield" ||
-       i_it->statement=="checkcast" ||
-       i_it->statement=="newarray" ||
-       i_it->statement=="anewarray" ||
-       i_it->statement=="idiv" ||
-       i_it->statement=="ldiv" ||
-       i_it->statement=="irem" ||
-       i_it->statement=="lrem" ||
-       i_it->statement==patternt("?astore") ||
-       i_it->statement==patternt("?aload") ||
-       i_it->statement=="invokestatic" ||
-       i_it->statement=="invokevirtual" ||
-       i_it->statement=="invokespecial" ||
-       i_it->statement=="invokeinterface" ||
-       (threading_support && (i_it->statement=="monitorenter" ||
-       i_it->statement=="monitorexit")))
+    if(
+      statement == "athrow" || statement == "putfield" ||
+      statement == "getfield" || statement == "checkcast" ||
+      statement == "newarray" || statement == "anewarray" ||
+      statement == "idiv" || statement == "ldiv" || statement == "irem" ||
+      statement == "lrem" || statement == patternt("?astore") ||
+      statement == patternt("?aload") || statement == "invokestatic" ||
+      statement == "invokevirtual" || statement == "invokespecial" ||
+      statement == "invokeinterface" ||
+      (threading_support &&
+       (statement == "monitorenter" || statement == "monitorexit")))
     {
       const std::vector<method_offsett> handler =
         try_catch_handler(i_it->address, method.exception_table);
@@ -1051,13 +1031,10 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       targets.insert(handler.begin(), handler.end());
     }
 
-    if(i_it->statement=="goto" ||
-       i_it->statement==patternt("if_?cmp??") ||
-       i_it->statement==patternt("if??") ||
-       i_it->statement=="ifnonnull" ||
-       i_it->statement=="ifnull" ||
-       i_it->statement=="jsr" ||
-       i_it->statement=="jsr_w")
+    if(
+      statement == "goto" || statement == patternt("if_?cmp??") ||
+      statement == patternt("if??") || statement == "ifnonnull" ||
+      statement == "ifnull" || statement == "jsr" || statement == "jsr_w")
     {
       PRECONDITION(!i_it->args.empty());
 
@@ -1066,8 +1043,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
 
       a_entry.first->second.successors.push_back(target);
 
-      if(i_it->statement=="jsr" ||
-         i_it->statement=="jsr_w")
+      if(statement == "jsr" || statement == "jsr_w")
       {
         auto next = std::next(i_it);
         DATA_INVARIANT(
@@ -1076,8 +1052,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
         jsr_ret_targets.push_back(next->address);
       }
     }
-    else if(i_it->statement=="tableswitch" ||
-            i_it->statement=="lookupswitch")
+    else if(statement == "tableswitch" || statement == "lookupswitch")
     {
       bool is_label=true;
       for(const auto &arg : i_it->args)
@@ -1091,7 +1066,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
         is_label=!is_label;
       }
     }
-    else if(i_it->statement=="ret")
+    else if(statement == "ret")
     {
       // Finish these later, once we've seen all jsr instructions.
       ret_instructions.push_back(i_it);
@@ -1147,11 +1122,11 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       stack.empty() || instruction.predecessors.size() <= 1 ||
       has_prefix(stack.front().get_string(ID_C_base_name), "$stack"));
 
-    irep_idt statement=i_it->statement;
     exprt arg0=i_it->args.size()>=1?i_it->args[0]:nil_exprt();
     exprt arg1=i_it->args.size()>=2?i_it->args[1]:nil_exprt();
 
-    const bytecode_infot &stmt_bytecode_info = get_bytecode_info(statement);
+    const bytecode_infot &stmt_bytecode_info = bytecode_info[i_it->bytecode];
+    std::string statement = stmt_bytecode_info.mnemonic;
 
     // deal with _idx suffixes
     if(statement.size()>=2 &&
@@ -1163,7 +1138,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
           string2integer(
             std::string(id2string(statement), statement.size()-1, 1)),
           java_int_type());
-      statement=std::string(id2string(statement), 0, statement.size()-2);
+      statement = std::string(statement, 0, statement.size() - 2);
     }
 
     typet catch_type;

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -304,8 +304,6 @@ class java_bytecode_convert_methodt:public messaget
     const methodt &,
     const java_class_typet::java_lambda_method_handlest &);
 
-  const bytecode_infot &get_bytecode_info(const irep_idt &statement);
-
   codet get_clinit_call(const irep_idt &classname);
 
   bool is_method_inherited(

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -311,8 +311,9 @@ static void infer_opaque_type_fields(
     for(const java_bytecode_parse_treet::instructiont &instruction :
           method.instructions)
     {
-      if(instruction.statement == "getfield" ||
-         instruction.statement == "putfield")
+      const std::string statement =
+        bytecode_info[instruction.bytecode].mnemonic;
+      if(statement == "getfield" || statement == "putfield")
       {
         const fieldref_exprt &fieldref =
           expr_dynamic_cast<fieldref_exprt>(instruction.args[0]);
@@ -456,10 +457,11 @@ static void generate_constant_global_variables(
     {
       // ldc* instructions are Java bytecode "load constant" ops, which can
       // retrieve a numeric constant, String literal, or Class literal.
-      if(instruction.statement == "ldc" ||
-         instruction.statement == "ldc2" ||
-         instruction.statement == "ldc_w" ||
-         instruction.statement == "ldc2_w")
+      const std::string statement =
+        bytecode_info[instruction.bytecode].mnemonic;
+      if(
+        statement == "ldc" || statement == "ldc2" || statement == "ldc_w" ||
+        statement == "ldc2_w")
       {
         INVARIANT(
           instruction.args.size() != 0,
@@ -584,8 +586,9 @@ static void create_stub_global_symbols(
     for(const java_bytecode_parse_treet::instructiont &instruction :
           method.instructions)
     {
-      if(instruction.statement == "getstatic" ||
-         instruction.statement == "putstatic")
+      const std::string statement =
+        bytecode_info[instruction.bytecode].mnemonic;
+      if(statement == "getstatic" || statement == "putstatic")
       {
         INVARIANT(
           instruction.args.size() > 0,

jbmc/src/java_bytecode/java_bytecode_parse_tree.cpp

@@ -161,7 +161,7 @@ void java_bytecode_parse_treet::methodt::output(std::ostream &out) const
       out << "    // " << i.source_location << '\n';
 
     out << "    " << i.address << ": ";
-    out << i.statement;
+    out << bytecode_info[i.bytecode].mnemonic;
 
     bool first = true;
     for(const auto &arg : i.args)

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -56,7 +56,7 @@ struct java_bytecode_parse_treet
   {
     source_locationt source_location;
     unsigned address;
-    irep_idt statement;
+    u8 bytecode;
     typedef std::vector<exprt> argst;
     argst args;
   };

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -36,7 +36,6 @@ class java_bytecode_parsert:public parsert
   explicit java_bytecode_parsert(bool skip_instructions)
     : skip_instructions(skip_instructions)
   {
-    populate_bytecode_mnemonics_table();
   }
 
   virtual bool parse();
@@ -72,14 +71,6 @@ class java_bytecode_parsert:public parsert
   constant_poolt constant_pool;
 
 protected:
-  class bytecodet
-  {
-  public:
-    irep_idt mnemonic;
-    char format;
-  };
-
-  std::vector<bytecodet> bytecodes;
   const bool skip_instructions = false;
 
   pool_entryt &pool_entry(u2 index)
@@ -104,23 +95,6 @@ class java_bytecode_parsert:public parsert
     return *java_type_from_string(id2string(pool_entry(index).s));
   }
 
-  void populate_bytecode_mnemonics_table()
-  {
-    // This is only useful for rbytecodes, which in turn is only useful to
-    // parse method instructions.
-    if(skip_instructions)
-      return;
-
-    // pre-hash the mnemonics, so we do this only once
-    bytecodes.resize(256);
-    for(const bytecode_infot *p=bytecode_info; p->mnemonic!=nullptr; p++)
-    {
-      assert(p->opcode<bytecodes.size());
-      bytecodes[p->opcode].mnemonic=p->mnemonic;
-      bytecodes[p->opcode].format=p->format;
-    }
-  }
-
   void rClassFile();
   void rconstant_pool();
   void rinterfaces(classt &parsed_class);
@@ -954,9 +928,6 @@ void java_bytecode_parsert::rfields(classt &parsed_class)
 void java_bytecode_parsert::rbytecode(
   methodt::instructionst &instructions)
 {
-  INVARIANT(
-    bytecodes.size() == 256, "bytecode mnemonics should have been populated");
-
   u4 code_length=read_u4();
 
   u4 address;
@@ -978,19 +949,20 @@ void java_bytecode_parsert::rbytecode(
       // [ifald]load, [ifald]store, ret and iinc
       // All of these have either format of v, or V
       INVARIANT(
-        bytecodes[bytecode].format == 'v' || bytecodes[bytecode].format == 'V',
-        "Unexpected wide instruction: " +
-          id2string(bytecodes[bytecode].mnemonic));
+        bytecode_info[bytecode].format == 'v' ||
+          bytecode_info[bytecode].format == 'V',
+        std::string("Unexpected wide instruction: ") +
+          bytecode_info[bytecode].mnemonic);
     }
 
     instructions.push_back(instructiont());
     instructiont &instruction=instructions.back();
-    instruction.statement=bytecodes[bytecode].mnemonic;
+    instruction.bytecode = bytecode;
     instruction.address=start_of_instruction;
     instruction.source_location
       .set_java_bytecode_index(std::to_string(bytecode_index));
 
-    switch(bytecodes[bytecode].format)
+    switch(bytecode_info[bytecode].format)
     {
     case ' ': // no further bytes
       break;

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -184,7 +184,8 @@ static bool is_store_to_slot(
   const java_bytecode_convert_methodt::instructiont &inst,
   unsigned slotidx)
 {
-  const std::string prevstatement=id2string(inst.statement);
+  const std::string prevstatement = bytecode_info[inst.bytecode].mnemonic;
+
   if(!(prevstatement.size()>=1 && prevstatement.substr(1, 5)=="store"))
     return false;