From 3d9e3a32a181c55330b9662368d1060bd10ca427 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 29 Nov 2025 20:11:40 +0100
Subject: [PATCH] Java bytecode front-end: fix static field is_static_lifetime
 flag

Ensure static fields accessed via getstatic bytecode are properly marked
with is_static_lifetime=true in the symbol table. This fixes an issue
where static fields from missing classes were not properly initialized.

Fixes: #851
---
 .../jbmc/static_field_missing_class/a.class       | Bin 0 -> 513 bytes
 .../jbmc/static_field_missing_class/a.java        |   5 +++++
 .../jbmc/static_field_missing_class/test.desc     |   7 +++++++
 .../src/java_bytecode/java_bytecode_typecheck.cpp |  10 ++++++++++
 .../java_bytecode_typecheck_expr.cpp              |  11 ++++++++++-
 5 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100644 jbmc/regression/jbmc/static_field_missing_class/a.class
 create mode 100644 jbmc/regression/jbmc/static_field_missing_class/a.java
 create mode 100644 jbmc/regression/jbmc/static_field_missing_class/test.desc

diff --git a/jbmc/regression/jbmc/static_field_missing_class/a.class b/jbmc/regression/jbmc/static_field_missing_class/a.class
new file mode 100644
index 0000000000000000000000000000000000000000..8ed5bb7751a024c162bcfa916e86cb9b59620aa8
GIT binary patch
literal 513
zcmYLG%Syvg5IvK`rb(l1ZPog&kA=F>jVlqc_yEDjLJ{olHn~b_O(YNTTLjmxRZvjS
zy&omc4Ygei_uQE|bI#oR^ZW4ypn(M&8gvteg8}3SrM9>eYaJ0>t(~;m(oG1tO+WCH
zErPzZd~P8R%Y^Nq0Ea+=P+1glEThB^gLv1EMXMt{t~4zSp=hGypp0Qov^efL4op-D
zwZ2f}pS~AGVPvBM-NqPdCdM61V3JVmH}7;<jWFuT*pH;w<DMoWNx8r#n*?Jg^d$2R
z{Xib4H!T^RDPLT^OasCoce~d|;<lU3Z@QiClJ;qsMy}lVRd-ITDrMApYmMKFN;S1N
zBb|dE41_60(|nT3th|Gs84#zCl@+!y(`((x1_2{4FdtBU!QdkbpQv2CW8_;=wT!C1
zMX6L_U^YWkWfS$@ob^l)C=ch~F!}(~c!Ht7!tBpb?v%XZ4?uIamB~52Xqf*4TJlz)

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/static_field_missing_class/a.java b/jbmc/regression/jbmc/static_field_missing_class/a.java
new file mode 100644
index 00000000000..85cc44c62cc
--- /dev/null
+++ b/jbmc/regression/jbmc/static_field_missing_class/a.java
@@ -0,0 +1,5 @@
+class a  {
+  public static void fun() {
+    assert b.x > 0;
+  }
+}
diff --git a/jbmc/regression/jbmc/static_field_missing_class/test.desc b/jbmc/regression/jbmc/static_field_missing_class/test.desc
new file mode 100644
index 00000000000..08e470a236c
--- /dev/null
+++ b/jbmc/regression/jbmc/static_field_missing_class/test.desc
@@ -0,0 +1,7 @@
+CORE
+a.class
+--function a.fun --show-symbol-table
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
index 716121bb636..382272ea6fc 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck.cpp
@@ -26,6 +26,16 @@ std::string java_bytecode_typecheckt::to_string(const typet &type)
 void java_bytecode_typecheckt::typecheck_non_type_symbol(symbolt &symbol)
 {
   PRECONDITION(!symbol.is_type);
+
+  // Static fields should be marked with is_static_lifetime.
+  // In case the symbol was created without this flag (e.g., through stubbing),
+  // ensure it's set correctly based on whether this is a static field.
+  // Static fields have ID_C_field set on their type.
+  if(symbol.type.find(ID_C_field).is_not_nil() && !symbol.is_static_lifetime)
+  {
+    symbol.is_static_lifetime = true;
+  }
+
   typecheck_type(symbol.type);
   typecheck_expr(symbol.value);
 }
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
index 682ec957091..c724a7bec02 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
@@ -71,10 +71,19 @@ void java_bytecode_typecheckt::typecheck_expr_symbol(symbol_exprt &expr)
 
   // the java_bytecode_convert_class and java_bytecode_convert_method made sure
   // "identifier" exists in the symbol table
-  const symbolt &symbol = symbol_table.lookup_ref(identifier);
+  symbolt &symbol = symbol_table.get_writeable_ref(identifier);
 
   INVARIANT(!symbol.is_type, "symbol identifier should not be a type");
 
+  // Static fields should be marked with is_static_lifetime.
+  // In case the symbol was created without this flag (e.g., through stubbing),
+  // ensure it's set correctly based on whether this is a static field.
+  // Static fields have ID_C_field set on their type.
+  if(symbol.type.find(ID_C_field).is_not_nil() && !symbol.is_static_lifetime)
+  {
+    symbol.is_static_lifetime = true;
+  }
+
   // type the expression
   expr.type() = symbol.type;
 }