work on monitorenter and monitorexit

Author: Daniel Kroening

regression/cbmc-java/monitorenter1/monitorenter1.class

@@ -1,16 +1,18 @@
 public class monitorenter1
 {
-  public boolean doIt(boolean b)
+  public int doIt(int what)
   {
-    boolean a;
+    int some;
+    
     synchronized(this) {
-      a = !b;
+      some=what;
     }
-    return a;
+
+    return some;
   }
 
   public void test()
   {
-    assert doIt(false);
+    assert doIt(1)==1;
   }
 }

regression/cbmc-java/monitorenter1/monitorenter1.java

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 virtual1.class
 --function monitorenter1.test
 ^EXIT=0$

regression/cbmc-java/monitorenter1/test.desc

@@ -3,7 +3,7 @@ SRC = java_bytecode_language.cpp java_bytecode_parse_tree.cpp \
       java_bytecode_convert_class.cpp java_types.cpp java_entry_point.cpp \
       java_bytecode_typecheck_code.cpp java_bytecode_typecheck_expr.cpp \
       java_bytecode_typecheck_type.cpp java_bytecode_internal_additions.cpp \
-      java_class_identifier.cpp java_bytecode_parser.cpp bytecode_info.cpp \
+      java_root_class.cpp java_bytecode_parser.cpp bytecode_info.cpp \
       java_class_loader.cpp jar_file.cpp java_object_factory.cpp \
       java_bytecode_convert_method.cpp
 

src/java_bytecode/Makefile

@@ -13,7 +13,7 @@ Author: Daniel Kroening, [email protected]
 #endif
 
 #include "java_bytecode_convert_class.h"
-#include "java_class_identifier.h"
+#include "java_root_class.h"
 #include "java_types.h"
 #include "java_bytecode_convert_method.h"
 
@@ -127,7 +127,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
 
   // is this a root class?
   if(c.extends.empty())
-    create_class_identifier(*class_symbol);
+    java_root_class(*class_symbol);
 }
 
 /*******************************************************************\
@@ -169,8 +169,8 @@ void java_bytecode_convert_classt::generate_class_stub(const irep_idt &class_nam
   }
   else
   {
-    // create the class identifier
-    create_class_identifier(*class_symbol);
+    // create the class identifier etc
+    java_root_class(*class_symbol);
   }
 }
 

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1401,11 +1401,32 @@ codet java_bytecode_convert_methodt::convert_instructions(
         binary_predicate_exprt(op[0], "java_instanceof", arg0);
     }
     else if(statement=="monitorenter")
-      warning() << "critical section with lock object is ignored ("
-                << i_it->source_location << ")" << eom;
+    {
+      // becomes a function call
+      code_typet type;
+      type.return_type()=void_typet();
+      type.parameters().resize(1);
+      type.parameters()[0].type()=reference_typet(void_typet());
+      code_function_callt call;
+      call.function()=symbol_exprt("java::monitorenter", type);
+      call.lhs().make_nil();
+      call.arguments().push_back(op[0]);
+      call.add_source_location()=i_it->source_location;
+      c=call;
+    }
     else if(statement=="monitorexit")
-      // just skip, is always preceeded with "monitorenter"
     {
+      // becomes a function call
+      code_typet type;
+      type.return_type()=void_typet();
+      type.parameters().resize(1);
+      type.parameters()[0].type()=reference_typet(void_typet());
+      code_function_callt call;
+      call.function()=symbol_exprt("java::monitorexit", type);
+      call.lhs().make_nil();
+      call.arguments().push_back(op[0]);
+      call.add_source_location()=i_it->source_location;
+      c=call;
     }
     else
     {

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/i2string.h>
 #include <util/namespace.h>
+#include <util/expr_util.h>
 
 #include "java_object_factory.h"
 
@@ -115,6 +116,11 @@ void gen_nondet_init(
         code_assignt code(me, ci);
         init_code.copy_to_operands(code);
       }
+      else if(name=="@lock")
+      {
+        code_assignt code(me, gen_zero(me.type()));
+        init_code.copy_to_operands(code);
+      }
       else
       {
         assert(!name.empty());

src/java_bytecode/java_class_identifier.cpp

@@ -0,0 +1,54 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include <util/symbol.h>
+#include <util/std_types.h>
+
+#include "java_types.h"
+#include "java_root_class.h"
+
+/*******************************************************************
+
+ Function: java_root_class
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void java_root_class(symbolt &class_symbol)
+{
+  struct_typet &struct_type=to_struct_type(class_symbol.type);
+  struct_typet::componentst &components=struct_type.components();
+  
+  {
+    // for monitorenter/monitorexit
+    struct_typet::componentt component;
+    component.set_name("@lock");
+    component.set_pretty_name("@lock");
+    component.type()=java_boolean_type();
+  
+    // add at the beginning
+    components.insert(components.begin(), component);
+  }
+
+  {
+    // the class identifier is used for stuff such as 'instanceof'
+    struct_typet::componentt component;
+    component.set_name("@class_identifier");
+    component.set_pretty_name("@class_identifier");
+    component.type()=string_typet();
+  
+    // add at the beginning
+    components.insert(components.begin(), component);
+  }
+}
+

src/java_bytecode/java_object_factory.cpp

@@ -6,12 +6,15 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#ifndef CPROVER_JAVA_CLASS_IDENTIFIER_H
-#define CPROVER_JAVA_CLASS_IDENTIFIER_H
+#ifndef CPROVER_JAVA_ROOT_CLASS_H
+#define CPROVER_JAVA_ROOT_CLASS_H
 
 #include <util/std_expr.h>
 
-void create_class_identifier(
+// adds expected members for a root class,
+// which is usually java.lang.Object
+
+void java_root_class(
   class symbolt &class_symbol);
 
-#endif /* CPROVER_JAVA_CLASS_IDENTIFIER_H */
+#endif /* CPROVER_JAVA_ROOT_CLASS_H */