Do not use global variable that requires an initializer function

tautschnig · tautschnig · commit 78d138dbb4c1 · 2018-12-29T21:15:17.000Z
In particular don't use one that depends on other globals to be initialized
first.
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me:()V' --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me2:()V' --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading --unwind 3
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Sync.class
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized/test.desc b/jbmc/regression/jbmc-concurrency/synchronized/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Sync.class
 --java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init1/test1.desc b/jbmc/regression/jbmc/static_init1/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 static_init.class
 --function static_init.main --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init2/test1.desc b/jbmc/regression/jbmc/static_init2/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 static_init.class
 --function static_init.main --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init_order/test3.desc b/jbmc/regression/jbmc/static_init_order/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 static_init_order.class
 --function static_init_order.test1 --trace --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init_order/test4.desc b/jbmc/regression/jbmc/static_init_order/test4.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 static_init_order.class
 --function static_init_order.test2 --java-threading
 ^EXIT=10$
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -44,7 +44,10 @@ enum class clinit_statest
   INIT_COMPLETE
 };
 
-const typet clinit_states_type = java_byte_type();
+static typet clinit_states_type()
+{
+  return java_byte_type();
+}
 
 // Disable linter here to allow a std::string constant, since that holds
 // a length, whereas a cstr would require strlen every time.
@@ -158,7 +161,7 @@ static code_assignt
 gen_clinit_assign(const exprt &expr, const clinit_statest state)
 {
   mp_integer initv(static_cast<int>(state));
-  constant_exprt init_s = from_integer(initv, clinit_states_type);
+  constant_exprt init_s = from_integer(initv, clinit_states_type());
   return code_assignt(expr, init_s);
 }
 
@@ -174,7 +177,7 @@ static equal_exprt
 gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 {
   mp_integer initv(static_cast<int>(state));
-  constant_exprt init_s = from_integer(initv, clinit_states_type);
+  constant_exprt init_s = from_integer(initv, clinit_states_type());
   return equal_exprt(expr, init_s);
 }
 
@@ -312,23 +315,23 @@ static void create_clinit_wrapper_symbols(
   if(thread_safe)
   {
     exprt not_init_value = from_integer(
-      static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type);
+      static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type());
 
     // Create two global static synthetic "fields" for the class "id"
     // these two variables hold the state of the class initialization algorithm
     // across calls to the clinit_wrapper
     add_new_variable_symbol(
       symbol_table,
       clinit_state_var_name(class_name),
-      clinit_states_type,
+      clinit_states_type(),
       not_init_value,
       false,
       true);
 
     add_new_variable_symbol(
       symbol_table,
       clinit_thread_local_state_var_name(class_name),
-      clinit_states_type,
+      clinit_states_type(),
       not_init_value,
       true,
       true);

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE`
`2`	`2`	`A.class`
`3`	`3`	--function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
`4`	`4`	`^VERIFICATION SUCCESSFUL$`