Extend the usage of method_offsett

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -204,7 +204,7 @@ symbol_exprt java_bytecode_convert_methodt::tmp_variable(
 exprt java_bytecode_convert_methodt::variable(
   const exprt &arg,
   char type_char,
-  size_t address,
+  method_offsett address,
   java_bytecode_convert_methodt::variable_cast_argumentt do_cast)
 {
   typet t=java_type_from_char(type_char);
@@ -555,7 +555,8 @@ void java_bytecode_convert_methodt::convert(
     variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr();
     variables[param_index][0].is_parameter=true;
     variables[param_index][0].start_pc=0;
-    variables[param_index][0].length=std::numeric_limits<size_t>::max();
+    variables[param_index][0].length =
+      std::numeric_limits<method_offsett>::max();
     param_index+=java_local_variable_slots(param.type());
   }
 
@@ -937,7 +938,7 @@ code_blockt &java_bytecode_convert_methodt::get_or_create_block_for_pcrange(
 }
 
 static void gather_symbol_live_ranges(
-  java_bytecode_convert_methodt::method_offsett pc,
+  method_offsett pc,
   const exprt &e,
   std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
 {
@@ -962,7 +963,8 @@ static void gather_symbol_live_ranges(
       }
       else
       {
-        var.length=std::max(var.length, (pc-var.start_pc)+1);
+        var.length = std::max(
+          var.length, static_cast<method_offsett>((pc - var.start_pc) + 1));
       }
     }
   }
@@ -1078,7 +1080,8 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
     {
       PRECONDITION(!i_it->args.empty());
 
-      auto target = numeric_cast_v<unsigned>(to_constant_expr(i_it->args[0]));
+      auto target =
+        numeric_cast_v<method_offsett>(to_constant_expr(i_it->args[0]));
       targets.insert(target);
 
       a_entry.first->second.successors.push_back(target);
@@ -1101,7 +1104,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       {
         if(is_label)
         {
-          auto target = numeric_cast_v<unsigned>(to_constant_expr(arg));
+          auto target = numeric_cast_v<method_offsett>(to_constant_expr(arg));
           targets.insert(target);
           a_entry.first->second.successors.push_back(target);
         }
@@ -1878,7 +1881,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       root,
       root_block,
       v.start_pc,
-      v.start_pc + v.length,
+      static_cast<method_offsett>(v.start_pc + v.length),
       std::numeric_limits<method_offsett>::max(),
       address_map);
   }
@@ -1894,7 +1897,7 @@ code_blockt java_bytecode_convert_methodt::convert_instructions(
       root,
       root_block,
       v.start_pc,
-      v.start_pc + v.length,
+      static_cast<method_offsett>(v.start_pc + v.length),
       std::numeric_limits<method_offsett>::max());
     code_declt d(v.symbol_expr);
     block.statements().insert(block.statements().begin(), d);
@@ -2986,7 +2989,7 @@ void java_bytecode_convert_methodt::draw_edges_from_ret_to_jsr(
   }
 }
 
-std::vector<java_bytecode_convert_methodt::method_offsett>
+std::vector<method_offsett>
 java_bytecode_convert_methodt::try_catch_handler(
   const method_offsett address,
   const java_bytecode_parse_treet::methodt::exception_tablet &exception_table)
@@ -3025,7 +3028,7 @@ void java_bytecode_initialize_parameter_names(
   java_method_typet::parameterst &parameters = method_type.parameters();
 
   // Find number of parameters
-  unsigned slots_for_parameters = java_method_parameter_slots(method_type);
+  auto slots_for_parameters = java_method_parameter_slots(method_type);
 
   // Find parameter names in the local variable table:
   typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;

jbmc/src/java_bytecode/java_bytecode_convert_method_class.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ci_lazy_methods_needed.h"
 #include "java_bytecode_parse_tree.h"
 #include "java_bytecode_convert_class.h"
+#include "java_utils.h"
 
 #include <util/expanding_vector.h>
 #include <util/message.h>
@@ -66,8 +67,6 @@ class java_bytecode_convert_methodt:public messaget
     convert(class_symbol, method);
   }
 
-  typedef uint16_t method_offsett;
-
 protected:
   symbol_table_baset &symbol_table;
   namespacet ns;
@@ -116,8 +115,8 @@ class java_bytecode_convert_methodt:public messaget
   {
   public:
     symbol_exprt symbol_expr;
-    size_t start_pc;
-    size_t length;
+    method_offsett start_pc;
+    method_offsett length;
     bool is_parameter;
     std::vector<holet> holes;
 
@@ -143,7 +142,7 @@ class java_bytecode_convert_methodt:public messaget
 
   // return corresponding reference of variable
   const variablet &find_variable_for_slot(
-    size_t address,
+    method_offsett address,
     variablest &var_list);
 
   // JVM local variables
@@ -156,7 +155,7 @@ class java_bytecode_convert_methodt:public messaget
   exprt variable(
     const exprt &arg,
     char type_char,
-    size_t address,
+    method_offsett address,
     variable_cast_argumentt do_cast);
 
   // temporary variables

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "bytecode_info.h"
 
+typedef uint16_t method_offsett;
+
 struct java_bytecode_parse_treet
 {
   // Disallow copy construction and copy assignment, but allow move construction
@@ -57,7 +59,7 @@ struct java_bytecode_parse_treet
   struct instructiont
   {
     source_locationt source_location;
-    unsigned address;
+    method_offsett address;
     irep_idt statement;
     typedef std::vector<exprt> argst;
     argst args;
@@ -114,9 +116,9 @@ struct java_bytecode_parse_treet
       {
       }
 
-      std::size_t start_pc;
-      std::size_t end_pc;
-      std::size_t handler_pc;
+      method_offsett start_pc;
+      method_offsett end_pc;
+      method_offsett handler_pc;
       struct_tag_typet catch_type;
     };
 
@@ -130,9 +132,9 @@ struct java_bytecode_parse_treet
       irep_idt name;
       std::string descriptor;
       optionalt<std::string> signature;
-      std::size_t index;
-      std::size_t start_pc;
-      std::size_t length;
+      method_offsett index;
+      method_offsett start_pc;
+      method_offsett length;
     };
 
     typedef std::vector<local_variablet> local_variable_tablet;

jbmc/src/java_bytecode/java_bytecode_parser.cpp

@@ -986,7 +986,7 @@ void java_bytecode_parsert::rbytecode(
     instructions.push_back(instructiont());
     instructiont &instruction=instructions.back();
     instruction.statement=bytecodes[bytecode].mnemonic;
-    instruction.address=start_of_instruction;
+    instruction.address=static_cast<method_offsett>(start_of_instruction);
     instruction.source_location
       .set_java_bytecode_index(std::to_string(bytecode_index));
 
@@ -1655,7 +1655,7 @@ void java_bytecode_parsert::rinner_classes_attribute(
 {
   std::string name = parsed_class.name.c_str();
   u2 number_of_classes = read_u2();
-  u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
+  u4 number_of_bytes_to_be_read = static_cast<u4>(number_of_classes * 8 + 2);
   INVARIANT(
     number_of_bytes_to_be_read == attribute_length,
     "The number of bytes to be read for the InnerClasses attribute does not "

jbmc/src/java_bytecode/java_local_variable_table.cpp

@@ -28,14 +28,12 @@ template <class T>
 struct procedure_local_cfg_baset<
   T,
   java_bytecode_convert_methodt::method_with_amapt,
-  java_bytecode_convert_methodt::method_offsett>
+  method_offsett>
   : public grapht<
-      cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
+      cfg_base_nodet<T, method_offsett>>
 {
   typedef java_bytecode_convert_methodt::method_with_amapt method_with_amapt;
-  typedef std::map<java_bytecode_convert_methodt::method_offsett,
-                   java_bytecode_convert_methodt::method_offsett>
-    entry_mapt;
+  typedef std::map<method_offsett, method_offsett> entry_mapt;
   entry_mapt entry_map;
 
   procedure_local_cfg_baset() {}
@@ -47,7 +45,7 @@ struct procedure_local_cfg_baset<
     for(const auto &inst : amap)
     {
       // Map instruction PCs onto node indices:
-      entry_map[inst.first]=this->add_node();
+      entry_map[inst.first] = static_cast<method_offsett>(this->add_node());
       // Map back:
       (*this)[entry_map[inst.first]].PC=inst.first;
     }
@@ -85,14 +83,12 @@ struct procedure_local_cfg_baset<
     }
   }
 
-  java_bytecode_convert_methodt::method_offsett
-  get_first_node(const method_with_amapt &args) const
+  method_offsett get_first_node(const method_with_amapt &args) const
   {
     return args.second.begin()->first;
   }
 
-  java_bytecode_convert_methodt::method_offsett
-  get_last_node(const method_with_amapt &args) const
+  method_offsett get_last_node(const method_with_amapt &args) const
   {
     return (--args.second.end())->first;
   }
@@ -216,14 +212,13 @@ static bool is_store_to_slot(
 /// \param [out] var: A hole is added to `var`, unless it would be of zero size
 static void maybe_add_hole(
   local_variable_with_holest &var,
-  java_bytecode_convert_methodt::method_offsett from,
-  java_bytecode_convert_methodt::method_offsett to)
+  method_offsett from,
+  method_offsett to)
 {
   PRECONDITION(to>=from);
   if(to!=from)
     var.holes.push_back(
-      {from,
-       static_cast<java_bytecode_convert_methodt::method_offsett>(to - from)});
+      {from, static_cast<method_offsett>(to - from)});
 }
 
 /// See above
@@ -240,10 +235,17 @@ static void populate_variable_address_map(
 {
   for(auto it=firstvar, itend=varlimit; it!=itend; ++it)
   {
-    if(it->var.start_pc+it->var.length>live_variable_at_address.size())
-      live_variable_at_address.resize(it->var.start_pc+it->var.length);
+    if(
+      static_cast<std::size_t>(it->var.start_pc + it->var.length) >
+      live_variable_at_address.size())
+    {
+      live_variable_at_address.resize(
+        static_cast<std::size_t>(it->var.start_pc + it->var.length));
+    }
 
-    for(auto idx = it->var.start_pc, idxlim = it->var.start_pc + it->var.length;
+    for(method_offsett idx = it->var.start_pc,
+                       idxlim = static_cast<method_offsett>(
+                         it->var.start_pc + it->var.length);
         idx != idxlim;
         ++idx)
     {
@@ -310,7 +312,8 @@ static void populate_predecessor_map(
 #endif
 
     // Find the last instruction within the live range:
-    const auto end_pc = it->var.start_pc + it->var.length;
+    const auto end_pc =
+      static_cast<method_offsett>(it->var.start_pc + it->var.length);
     auto amapit=amap.find(end_pc);
     INVARIANT(
       amapit!=amap.begin(),
@@ -423,22 +426,20 @@ static void populate_predecessor_map(
 /// \return Returns the bytecode address of the closest common dominator of all
 ///   given variable table entries. In the worst case the function entry point
 ///   should always satisfy this criterion.
-static java_bytecode_convert_methodt::method_offsett get_common_dominator(
+static method_offsett get_common_dominator(
   const std::set<local_variable_with_holest *> &merge_vars,
   const java_cfg_dominatorst &dominator_analysis)
 {
   PRECONDITION(!merge_vars.empty());
 
-  auto first_pc =
-    std::numeric_limits<java_bytecode_convert_methodt::method_offsett>::max();
+  auto first_pc = std::numeric_limits<method_offsett>::max();
   for(auto v : merge_vars)
   {
     if(v->var.start_pc<first_pc)
       first_pc=v->var.start_pc;
   }
 
-  std::vector<java_bytecode_convert_methodt::method_offsett>
-    candidate_dominators;
+  std::vector<method_offsett> candidate_dominators;
   for(auto v : merge_vars)
   {
     const auto &dominator_nodeidx=
@@ -485,7 +486,7 @@ static java_bytecode_convert_methodt::method_offsett get_common_dominator(
 static void populate_live_range_holes(
   local_variable_with_holest &merge_into,
   const std::set<local_variable_with_holest *> &merge_vars,
-  java_bytecode_convert_methodt::method_offsett expanded_live_range_start)
+  method_offsett expanded_live_range_start)
 {
   std::vector<local_variable_with_holest *> sorted_by_startpc(
     merge_vars.begin(), merge_vars.end());
@@ -495,14 +496,16 @@ static void populate_live_range_holes(
     merge_into,
     expanded_live_range_start,
     sorted_by_startpc[0]->var.start_pc);
-  for(java_bytecode_convert_methodt::method_offsett idx = 0;
+  for(method_offsett idx = 0;
       idx < sorted_by_startpc.size() - 1;
       ++idx)
   {
     maybe_add_hole(
       merge_into,
-      sorted_by_startpc[idx]->var.start_pc+sorted_by_startpc[idx]->var.length,
-      sorted_by_startpc[idx+1]->var.start_pc);
+      static_cast<method_offsett>(
+        sorted_by_startpc[idx]->var.start_pc +
+        sorted_by_startpc[idx]->var.length),
+      sorted_by_startpc[static_cast<method_offsett>(idx + 1)]->var.start_pc);
   }
 }
 
@@ -533,16 +536,17 @@ static void merge_variable_table_entries(
   // as it was not visible in the original local variable table)
   populate_live_range_holes(merge_into, merge_vars, found_dominator);
 
-  java_bytecode_convert_methodt::method_offsett last_pc = 0;
+  method_offsett last_pc = 0;
   for(auto v : merge_vars)
   {
-    if(v->var.start_pc+v->var.length>last_pc)
-      last_pc=v->var.start_pc+v->var.length;
+    if(static_cast<method_offsett>(v->var.start_pc + v->var.length) > last_pc)
+      last_pc = static_cast<method_offsett>(v->var.start_pc + v->var.length);
   }
 
   // Apply the changes:
   merge_into.var.start_pc=found_dominator;
-  merge_into.var.length=last_pc-found_dominator;
+  merge_into.var.length =
+    static_cast<method_offsett>(last_pc - found_dominator);
 
 #ifdef DEBUG
   debug_out << "Merged " << merge_vars.size() << " variables named "
@@ -837,7 +841,7 @@ void java_bytecode_convert_methodt::setup_local_variables(
 ///   nothing covers `address`.
 const java_bytecode_convert_methodt::variablet &
 java_bytecode_convert_methodt::find_variable_for_slot(
-  size_t address,
+  method_offsett address,
   variablest &var_list)
 {
   for(const variablet &var : var_list)
@@ -865,6 +869,6 @@ java_bytecode_convert_methodt::find_variable_for_slot(
   size_t list_length=var_list.size();
   var_list.resize(list_length+1);
   var_list[list_length].start_pc=0;
-  var_list[list_length].length=std::numeric_limits<size_t>::max();
+  var_list[list_length].length = std::numeric_limits<method_offsett>::max();
   return var_list[list_length];
 }