Skip to content

Commit

Permalink
Cleanup type conversions in java_bytecode_parsert::read
Browse files Browse the repository at this point in the history
We can safely read signed values and don't need to defer the type
conversion to the call site.
  • Loading branch information
tautschnig committed Feb 7, 2025
1 parent 66004dc commit debf665
Showing 1 changed file with 18 additions and 17 deletions.
35 changes: 18 additions & 17 deletions jbmc/src/java_bytecode/java_bytecode_parser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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);
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -942,15 +943,15 @@ 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;
break;

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(
Expand All @@ -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(
Expand Down Expand Up @@ -994,15 +995,15 @@ 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;
}
else // local variable index (one byte) plus one signed byte
{
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;
}
Expand Down Expand Up @@ -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(
Expand All @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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;
Expand Down

0 comments on commit debf665

Please sign in to comment.