Extract convert_getstatic function

NathanJPhillips · Jun 13, 2018 · f1edff9 · f1edff9
1 parent 68bddf1
commit f1edff9
Show file tree

Hide file tree

Showing 2 changed files with 52 additions and 34 deletions.
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1788,40 +1788,8 @@ codet java_bytecode_convert_methodt::convert_instructions(
         symbol_table.has_symbol(symbol_expr.get_identifier()),
         "getstatic symbol should have been created before method conversion");
 
-      if(needed_lazy_methods)
-      {
-        if(arg0.type().id()==ID_symbol)
-        {
-          needed_lazy_methods->add_needed_class(
-            to_symbol_type(arg0.type()).get_identifier());
-        }
-        else if(arg0.type().id()==ID_pointer)
-        {
-          const auto &pointer_type=to_pointer_type(arg0.type());
-          if(pointer_type.subtype().id()==ID_symbol)
-          {
-            needed_lazy_methods->add_needed_class(
-              to_symbol_type(pointer_type.subtype()).get_identifier());
-          }
-        }
-        else if(is_assertions_disabled_field)
-        {
-          needed_lazy_methods->add_needed_class(arg0.get_string(ID_class));
-        }
-      }
-      results[0]=java_bytecode_promotion(symbol_expr);
-
-      // Note this initializer call deliberately inits the class used to make
-      // the reference, which may be a child of the class that actually defines
-      // the field.
-      codet clinit_call=get_clinit_call(arg0.get_string(ID_class));
-      if(clinit_call.get_statement()!=ID_skip)
-        c=clinit_call;
-      else if(is_assertions_disabled_field)
-      {
-        // set $assertionDisabled to false
-        c=code_assignt(symbol_expr, false_exprt());
-      }
+      convert_getstatic(
+        arg0, symbol_expr, is_assertions_disabled_field, c, results);
     }
     else if(statement=="putfield")
     {
@@ -2465,6 +2433,49 @@ codet java_bytecode_convert_methodt::convert_instructions(
   return code;
 }
 
+void java_bytecode_convert_methodt::convert_getstatic(
+  exprt &arg0,
+  const symbol_exprt &symbol_expr,
+  const bool is_assertions_disabled_field,
+  codet &c,
+  exprt::operandst &results)
+{
+  if(needed_lazy_methods)
+  {
+    if(arg0.type().id() == ID_symbol)
+    {
+      needed_lazy_methods->add_needed_class(
+        to_symbol_type(arg0.type()).get_identifier());
+    }
+    else if(arg0.type().id() == ID_pointer)
+    {
+      const auto &pointer_type = to_pointer_type(arg0.type());
+      if(pointer_type.subtype().id() == ID_symbol)
+      {
+        needed_lazy_methods->add_needed_class(
+          to_symbol_type(pointer_type.subtype()).get_identifier());
+      }
+    }
+    else if(is_assertions_disabled_field)
+    {
+      needed_lazy_methods->add_needed_class(arg0.get_string(ID_class));
+    }
+  }
+  results[0] = java_bytecode_promotion(symbol_expr);
+
+  // Note this initializer call deliberately inits the class used to make
+  // the reference, which may be a child of the class that actually defines
+  // the field.
+  codet clinit_call = get_clinit_call(arg0.get_string(ID_class));
+  if(clinit_call.get_statement() != ID_skip)
+    c = clinit_call;
+  else if(is_assertions_disabled_field)
+  {
+    // set $assertionDisabled to false
+    c = code_assignt(symbol_expr, false_exprt());
+  }
+}
+
 exprt::operandst &java_bytecode_convert_methodt::convert_cmp2(
   const irep_idt &statement,
   const exprt::operandst &op,

diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h
@@ -380,5 +380,12 @@ class java_bytecode_convert_methodt:public messaget
     const irep_idt &statement,
     const exprt::operandst &op,
     exprt::operandst &results) const;
+
+  void convert_getstatic(
+    const exprt &arg0,
+    const symbol_exprt &symbol_expr,
+    bool is_assertions_disabled_field,
+    codet &c,
+    exprt::operandst &results);
 };
 #endif