From debf6656e2e5084c99f6aa92e5cde87ed52d71b9 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 7 Feb 2025 13:00:56 +0000
Subject: [PATCH] Cleanup type conversions in java_bytecode_parsert::read

We can safely read signed values and don't need to defer the type
conversion to the call site.
---
 .../java_bytecode/java_bytecode_parser.cpp    | 35 ++++++++++---------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index e036b06bdc4..a1cec6955c8 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -132,9 +132,10 @@ class java_bytecode_parsert final : public parsert
   T read()
   {
     static_assert(
-      std::is_unsigned<T>::value, "T should be an unsigned integer");
+      std::is_unsigned<T>::value || std::is_signed<T>::value,
+      "T should be a signed or unsigned integer");
     const constexpr size_t bytes = sizeof(T);
-    u8 result = 0;
+    T result = 0;
     for(size_t i = 0; i < bytes; i++)
     {
       if(!*in)
@@ -145,7 +146,7 @@ class java_bytecode_parsert final : public parsert
       result <<= 8u;
       result |= static_cast<u1>(in->get());
     }
-    return narrow_cast<T>(result);
+    return result;
   }
 
   void store_unknown_method_handle(size_t bootstrap_method_index);
@@ -700,7 +701,7 @@ void java_bytecode_parsert::rconstant_pool()
         std::string s;
         s.resize(bytes);
         for(auto &ch : s)
-          ch = read<u1>();
+          ch = read<std::string::value_type>();
         it->s = s; // Add to string table
       }
       break;
@@ -942,7 +943,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
 
     case 'b': // a signed byte
       {
-        const s1 c = read<u1>();
+        const s1 c = read<s1>();
         instruction.args.push_back(from_integer(c, signedbv_typet(8)));
       }
       address+=1;
@@ -950,7 +951,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
 
     case 'o': // two byte branch offset, signed
       {
-        const s2 offset = read<u2>();
+        const s2 offset = read<s2>();
         // By converting the signed offset into an absolute address (by adding
         // the current address) the number represented becomes unsigned.
         instruction.args.push_back(
@@ -961,7 +962,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
 
     case 'O': // four byte branch offset, signed
       {
-        const s4 offset = read<u4>();
+        const s4 offset = read<s4>();
         // By converting the signed offset into an absolute address (by adding
         // the current address) the number represented becomes unsigned.
         instruction.args.push_back(
@@ -994,7 +995,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
       {
         const u2 v = read<u2>();
         instruction.args.push_back(from_integer(v, unsignedbv_typet(16)));
-        const s2 c = read<u2>();
+        const s2 c = read<s2>();
         instruction.args.push_back(from_integer(c, signedbv_typet(16)));
         address+=4;
       }
@@ -1002,7 +1003,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
       {
         const u1 v = read<u1>();
         instruction.args.push_back(from_integer(v, unsignedbv_typet(8)));
-        const s1 c = read<u1>();
+        const s1 c = read<s1>();
         instruction.args.push_back(from_integer(c, signedbv_typet(8)));
         address+=2;
       }
@@ -1032,7 +1033,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
         }
 
         // now default value
-        const s4 default_value = read<u4>();
+        const s4 default_value = read<s4>();
         // By converting the signed offset into an absolute address (by adding
         // the current address) the number represented becomes unsigned.
         instruction.args.push_back(
@@ -1045,8 +1046,8 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
 
         for(std::size_t i=0; i<npairs; i++)
         {
-          const s4 match = read<u4>();
-          const s4 offset = read<u4>();
+          const s4 match = read<s4>();
+          const s4 offset = read<s4>();
           instruction.args.push_back(
             from_integer(match, signedbv_typet(32)));
           // By converting the signed offset into an absolute address (by adding
@@ -1070,23 +1071,23 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
         }
 
         // now default value
-        const s4 default_value = read<u4>();
+        const s4 default_value = read<s4>();
         instruction.args.push_back(
           from_integer(base_offset+default_value, signedbv_typet(32)));
         address+=4;
 
         // now low value
-        const s4 low_value = read<u4>();
+        const s4 low_value = read<s4>();
         address+=4;
 
         // now high value
-        const s4 high_value = read<u4>();
+        const s4 high_value = read<s4>();
         address+=4;
 
         // there are high-low+1 offsets, and they are signed
         for(s4 i=low_value; i<=high_value; i++)
         {
-          s4 offset = read<u4>();
+          s4 offset = read<s4>();
           instruction.args.push_back(from_integer(i, signedbv_typet(32)));
           // By converting the signed offset into an absolute address (by adding
           // the current address) the number represented becomes unsigned.
@@ -1130,7 +1131,7 @@ void java_bytecode_parsert::rbytecode(std::vector<instructiont> &instructions)
 
     case 's': // a signed short
       {
-        const s2 s = read<u2>();
+        const s2 s = read<s2>();
         instruction.args.push_back(from_integer(s, signedbv_typet(16)));
       }
       address+=2;