Extend the usage of method_offsett

Author: tautschnig

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

@@ -196,7 +196,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)
 {
   const std::size_t number_int =
     numeric_cast_v<std::size_t>(to_constant_expr(arg));
@@ -942,7 +942,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)
 {
@@ -964,7 +964,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));
       }
     }
   }
@@ -1136,7 +1137,8 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       // clang-format on
       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);
@@ -1157,7 +1159,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       {
         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);
         }
@@ -2001,7 +2003,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       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);
   }
@@ -2017,7 +2019,7 @@ java_bytecode_convert_methodt::convert_instructions(const methodt &method)
       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);
@@ -3172,7 +3174,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)
@@ -3211,7 +3213,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

@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_METHOD_CLASS_H
 
 #include "java_bytecode_convert_class.h"
+#include "java_utils.h"
 
 #include <util/expanding_vector.h>
 #include <util/message.h>
@@ -74,8 +75,6 @@ class java_bytecode_convert_methodt
     convert(class_symbol, method, method_context);
   }
 
-  typedef uint16_t method_offsett;
-
 protected:
   messaget log;
   symbol_table_baset &symbol_table;
@@ -126,8 +125,8 @@ class java_bytecode_convert_methodt
   {
   public:
     symbol_exprt symbol_expr;
-    size_t start_pc;
-    size_t length;
+    method_offsett start_pc;
+    method_offsett length;
     bool is_parameter = false;
     std::vector<holet> holes;
 
@@ -183,7 +182,7 @@ class java_bytecode_convert_methodt
 
   // return corresponding reference of variable
   const variablet &find_variable_for_slot(
-    size_t address,
+    method_offsett address,
     variablest &var_list);
 
   // JVM local variables
@@ -193,7 +192,7 @@ class java_bytecode_convert_methodt
     NO_CAST
   };
 
-  exprt variable(const exprt &arg, char type_char, size_t address);
+  exprt variable(const exprt &arg, char type_char, method_offsett address);
 
   // temporary variables
   std::list<symbol_exprt> tmp_vars;

jbmc/src/java_bytecode/java_bytecode_parse_tree.h

@@ -19,6 +19,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <map>
 #include <set>
 
+typedef uint16_t method_offsett;
+
 struct java_bytecode_parse_treet
 {
   // Disallow copy construction and copy assignment, but allow move construction
@@ -55,7 +57,7 @@ struct java_bytecode_parse_treet
   struct instructiont
   {
     source_locationt source_location;
-    unsigned address;
+    method_offsett address;
     u8 bytecode;
     typedef std::vector<exprt> argst;
     argst args;
@@ -112,9 +114,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;
     };
 
@@ -128,9 +130,9 @@ struct java_bytecode_parse_treet
       irep_idt name;
       std::string descriptor;
       std::optional<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

@@ -913,7 +913,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
     instructions.emplace_back();
     instructiont &instruction=instructions.back();
     instruction.bytecode = bytecode;
-    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));
 
@@ -1594,7 +1594,7 @@ void java_bytecode_parsert::rinner_classes_attribute(
   classt &parsed_class = parse_tree.parsed_class;
   std::string name = parsed_class.name.c_str();
   const u2 number_of_classes = read<u2>();
-  const u4 number_of_bytes_to_be_read = number_of_classes * 8 + 2;
+  const 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

@@ -27,9 +27,9 @@ 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 grapht<
     cfg_base_nodet<T, java_bytecode_convert_methodt::method_offsett>>
@@ -51,7 +51,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;
     }
@@ -238,14 +238,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
@@ -262,10 +261,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)
     {
@@ -332,7 +338,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(),
@@ -445,22 +452,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=
@@ -507,7 +512,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());
@@ -555,16 +560,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 "
@@ -850,7 +856,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)

jbmc/src/java_bytecode/java_utils.cpp

@@ -144,12 +144,13 @@ unsigned java_local_variable_slots(const typet &t)
   return bitwidth == 64 ? 2u : 1u;
 }
 
-unsigned java_method_parameter_slots(const java_method_typet &t)
+method_offsett java_method_parameter_slots(const java_method_typet &t)
 {
-  unsigned slots=0;
+  method_offsett slots = 0;
 
   for(const auto &p : t.parameters())
-    slots+=java_local_variable_slots(p.type());
+    slots =
+      static_cast<method_offsett>(slots + java_local_variable_slots(p.type()));
 
   return slots;
 }

jbmc/src/java_bytecode/java_utils.h

@@ -83,7 +83,7 @@ unsigned java_local_variable_slots(const typet &t);
 
 /// Returns the the number of JVM local variables (slots) used by the JVM to
 /// pass, upon call, the arguments of a Java method whose type is \p t.
-unsigned java_method_parameter_slots(const java_method_typet &t);
+method_offsett java_method_parameter_slots(const java_method_typet &t);
 
 const std::string java_class_to_package(const std::string &canonical_classname);