48 #include <unordered_set>
64 for(std::size_t i=0; i<what.
size(); i++)
67 else if(
p[i]!=
'?' &&
p[i]!=what[i])
70 return p[what.
size()]==0;
98 for(std::size_t i=0; i<parameters.size(); ++i)
102 if(i==0 && parameters[i].get_this())
108 parameters[i].set_base_name(base_name);
109 parameters[i].set_identifier(identifier);
114 parameter_symbol.
mode=ID_java;
115 parameter_symbol.
name=identifier;
116 parameter_symbol.
type=parameters[i].type();
117 symbol_table.
add(parameter_symbol);
123 return pattern==what;
128 return id2string(method_name).find(
"<init>") != std::string::npos;
135 error() <<
"malformed bytecode (pop too high)" <<
eom;
141 for(std::size_t i=0; i<n; i++)
151 std::size_t residue_size=std::min(n,
stack.size());
160 for(std::size_t i=0; i<o.size(); i++)
171 const std::string &prefix,
180 tmp_symbol.
mode=ID_java;
181 tmp_symbol.
name=identifier;
182 tmp_symbol.
type=type;
186 result.set(ID_C_base_name, base_name);
215 const std::size_t number_int = numeric_cast_v<std::size_t>(arg);
229 result.set(ID_C_base_name, base_name);
256 const std::string &descriptor,
258 const std::string &class_name,
259 const std::string &method_name,
273 INVARIANT(member_type_from_descriptor.
id()==ID_code,
"Must be code type");
274 if(signature.has_value())
281 INVARIANT(member_type_from_signature.
id()==ID_code,
"Must be code type");
290 message.
warning() <<
"Method: " << class_name <<
"." << method_name
291 <<
"\n signature: " << signature.value()
292 <<
"\n descriptor: " << descriptor
293 <<
"\n different number of parameters, reverting to "
300 message.
warning() <<
"Method: " << class_name <<
"." << method_name
301 <<
"\n could not parse signature: " << signature.value()
302 <<
"\n " << e.what() <<
"\n"
303 <<
" reverting to descriptor: " << descriptor
320 const irept &lambda_method_handle = lambda_method_handles.at(index);
323 if(!lambda_method_handle.
id().
empty())
353 method_symbol.
name=method_identifier;
355 method_symbol.
mode=ID_java;
369 member_type.
set(ID_is_synchronized,
true);
371 member_type.
set(ID_is_static,
true);
385 this_p.
type()=object_ref_type;
387 parameters.insert(parameters.begin(), this_p);
413 type_checked_cast<annotated_typet>(
static_cast<typet &
>(member_type))
417 method_symbol.
type=member_type;
425 method_symbol.
type.
set(ID_C_must_not_throw,
true);
428 symbol_table.
add(method_symbol);
448 method_type.
set(ID_C_class, class_symbol.
name);
457 debug() <<
"Generating codet: class "
458 << class_symbol.
name <<
", method "
475 if(v.signature.has_value())
485 std::ostringstream id_oss;
489 result.set(ID_C_base_name, v.name);
498 newv.start_pc=v.start_pc;
499 newv.length=v.length;
506 std::size_t param_index=0;
507 for(
const auto ¶m : parameters)
514 "java_parameter_count and local computation must agree");
518 for(
auto ¶m : parameters)
527 if(param_index==0 && param.get_this())
536 base_name=
variables[param_index][0].symbol_expr.get(ID_C_base_name);
537 identifier=
variables[param_index][0].symbol_expr.get(ID_identifier);
540 if(base_name.
empty())
545 const typet &type=param.type();
551 param.set_base_name(base_name);
552 param.set_identifier(identifier);
557 parameter_symbol.
mode=ID_java;
558 parameter_symbol.
name=identifier;
559 parameter_symbol.
type=param.type();
564 variables[param_index][0].is_parameter=
true;
566 variables[param_index][0].length=std::numeric_limits<size_t>::max();
574 "java_parameter_count and local computation must agree");
578 method_symbol.
name == method_identifier,
579 "Name of method symbol shouldn't change");
582 "Base name of method symbol shouldn't change");
585 "Method symbol shouldn't have module");
587 method_symbol.
mode=ID_java;
609 "Member type should have already been marked as a constructor");
617 method_symbol.
type = method_type;
630 if(statement==p->mnemonic)
633 error() <<
"failed to find bytecode mnemonic `"
634 << statement <<
'\'' <<
eom;
653 throw "unhandled java comparison instruction";
666 fieldref.
get(ID_component_name),
686 if(g.get_destination()==old_label)
687 g.set_destination(new_label);
724 next_block_start_address,
763 assert(!tree.
branch.empty());
766 const auto afterstart=
772 auto findstart=afterstart;
783 const auto findlim_block_start_address =
793 auto child_iter = this_block.
statements().begin();
796 while(child_iter != this_block.
statements().end() &&
797 child_iter->get_statement() == ID_decl)
799 assert(child_iter != this_block.
statements().end());
800 std::advance(child_iter, child_offset);
801 assert(child_iter != this_block.
statements().end());
805 bool single_child(afterstart==findlim);
810 tree.
branch[child_offset],
814 findlim_block_start_address,
832 auto checkit=amap.
find(*findstart);
833 assert(checkit!=amap.end());
836 checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
839 for(
auto p : checkit->second.predecessors)
841 if(p<(*findstart) || p>=findlim_block_start_address)
843 debug() <<
"Generating codet: "
844 <<
"warning: refusing to create lexical block spanning "
845 << (*findstart) <<
"-" << findlim_block_start_address
846 <<
" due to incoming edge " << p <<
" -> "
847 << checkit->first <<
eom;
857 const irep_idt child_label_name=child_label.get_label();
858 std::string new_label_str =
id2string(child_label_name);
860 irep_idt new_label_irep(new_label_str);
864 auto nblocks=std::distance(findstart, findlim);
866 debug() <<
"Generating codet: combining "
867 << std::distance(findstart, findlim)
868 <<
" blocks for addresses " << (*findstart) <<
"-"
869 << findlim_block_start_address <<
eom;
872 auto &this_block_children = this_block.
statements();
873 assert(tree.
branch.size()==this_block_children.size());
874 for(
auto blockidx=child_offset, blocklim=child_offset+nblocks;
877 newblock.
add(this_block_children[blockidx]);
885 auto delfirst=this_block_children.begin();
886 std::advance(delfirst, child_offset+1);
887 auto dellim=delfirst;
888 std::advance(dellim, nblocks-1);
889 this_block_children.erase(delfirst, dellim);
890 this_block_children[child_offset].swap(newlabel);
894 auto branchstart=tree.
branch.begin();
895 std::advance(branchstart, child_offset);
896 auto branchlim=branchstart;
897 std::advance(branchlim, nblocks);
898 for(
auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
899 newnode.
branch.push_back(std::move(*branchiter));
901 tree.
branch.erase(branchstart, branchlim);
903 assert(tree.
branch.size()==this_block_children.size());
906 std::advance(branchaddriter, child_offset);
907 auto branchaddrlim=branchaddriter;
908 std::advance(branchaddrlim, nblocks);
917 tree.
branch[child_offset]=std::move(newnode);
924 this_block_children[child_offset]).code());
930 std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
932 if(e.
id()==ID_symbol)
935 auto findit = result.insert(
937 auto &var=findit.first->second;
940 var.symbol_expr=symexpr;
948 var.length+=(var.start_pc-pc);
953 var.length=std::max(var.length, (pc-var.start_pc)+1);
986 if(ty.
id()==ID_pointer)
1005 std::set<method_offsett> targets;
1007 std::vector<method_offsett> jsr_ret_targets;
1008 std::vector<instructionst::const_iterator> ret_instructions;
1010 for(
auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1013 std::pair<address_mapt::iterator, bool> a_entry=
1014 address_map.insert(std::make_pair(i_it->address, ins));
1015 assert(a_entry.second);
1018 assert(a_entry.first==--address_map.end());
1020 if(i_it->statement!=
"goto" &&
1021 i_it->statement!=
"return" &&
1022 !(i_it->statement==
patternt(
"?return")) &&
1023 i_it->statement!=
"athrow" &&
1024 i_it->statement!=
"jsr" &&
1025 i_it->statement!=
"jsr_w" &&
1026 i_it->statement!=
"ret")
1028 instructionst::const_iterator next=i_it;
1029 if(++next!=instructions.end())
1030 a_entry.first->second.successors.push_back(next->address);
1033 if(i_it->statement==
"athrow" ||
1034 i_it->statement==
"putfield" ||
1035 i_it->statement==
"getfield" ||
1036 i_it->statement==
"checkcast" ||
1037 i_it->statement==
"newarray" ||
1038 i_it->statement==
"anewarray" ||
1039 i_it->statement==
"idiv" ||
1040 i_it->statement==
"ldiv" ||
1041 i_it->statement==
"irem" ||
1042 i_it->statement==
"lrem" ||
1043 i_it->statement==
patternt(
"?astore") ||
1044 i_it->statement==
patternt(
"?aload") ||
1045 i_it->statement==
"invokestatic" ||
1046 i_it->statement==
"invokevirtual" ||
1047 i_it->statement==
"invokespecial" ||
1048 i_it->statement==
"invokeinterface" ||
1050 i_it->statement==
"monitorexit")))
1052 const std::vector<method_offsett> handler =
1054 std::list<method_offsett> &successors = a_entry.first->second.successors;
1055 successors.insert(successors.end(), handler.begin(), handler.end());
1056 targets.insert(handler.begin(), handler.end());
1059 if(i_it->statement==
"goto" ||
1060 i_it->statement==
patternt(
"if_?cmp??") ||
1061 i_it->statement==
patternt(
"if??") ||
1062 i_it->statement==
"ifnonnull" ||
1063 i_it->statement==
"ifnull" ||
1064 i_it->statement==
"jsr" ||
1065 i_it->statement==
"jsr_w")
1070 targets.insert(target);
1072 a_entry.first->second.successors.push_back(target);
1074 if(i_it->statement==
"jsr" ||
1075 i_it->statement==
"jsr_w")
1077 auto next = std::next(i_it);
1079 next != instructions.end(),
"jsr should have valid return address");
1080 targets.insert(next->address);
1081 jsr_ret_targets.push_back(next->address);
1084 else if(i_it->statement==
"tableswitch" ||
1085 i_it->statement==
"lookupswitch")
1088 for(
const auto &arg : i_it->args)
1093 targets.insert(target);
1094 a_entry.first->second.successors.push_back(target);
1099 else if(i_it->statement==
"ret")
1102 ret_instructions.push_back(i_it);
1107 for(
const auto &address : address_map)
1109 for(
auto s : address.second.successors)
1111 const auto a_it = address_map.find(s);
1113 a_it->second.predecessors.insert(address.first);
1127 std::set<method_offsett> working_set;
1129 if(!instructions.empty())
1130 working_set.insert(instructions.front().address);
1132 while(!working_set.empty())
1134 auto cur = working_set.begin();
1135 auto address_it = address_map.find(*cur);
1137 auto &instruction = address_it->second;
1139 working_set.erase(cur);
1141 if(instruction.done)
1144 instruction.successors.begin(), instruction.successors.end());
1146 instructionst::const_iterator i_it = instruction.source;
1147 stack.swap(instruction.stack);
1148 instruction.stack.clear();
1149 codet &c = instruction.code;
1152 stack.empty() || instruction.predecessors.size() <= 1 ||
1155 irep_idt statement=i_it->statement;
1162 if(statement.
size()>=2 &&
1163 statement[statement.
size()-2]==
'_' &&
1164 isdigit(statement[statement.
size()-1]))
1171 statement=std::string(
id2string(statement), 0, statement.
size()-2);
1182 if(cur_pc==it->handler_pc)
1185 catch_type !=
typet() ||
1192 catch_type=it->catch_type;
1196 codet catch_instruction;
1198 if(catch_type!=
typet())
1212 stack.push_back(catch_var);
1214 catch_instruction=catch_statement;
1221 if(statement==
"aconst_null")
1223 assert(results.size()==1);
1226 else if(statement==
"athrow")
1231 else if(statement==
"checkcast")
1239 else if(statement==
"invokedynamic")
1244 lambda_method_handles, i_it->source_location, arg0))
1250 else if(statement==
"invokestatic" &&
1252 "java::org.cprover.CProver.assume:(Z)V")
1257 "function expected to have exactly one parameter");
1261 else if(statement ==
"invokestatic" &&
1262 arg0.
get(ID_identifier) ==
1263 "java::org.cprover.CProver.atomicBegin:()V")
1265 c =
codet(ID_atomic_begin);
1268 else if(statement ==
"invokestatic" &&
1269 arg0.
get(ID_identifier) ==
1270 "java::org.cprover.CProver.atomicEnd:()V")
1272 c =
codet(ID_atomic_end);
1274 else if(statement==
"invokeinterface" ||
1275 statement==
"invokespecial" ||
1276 statement==
"invokevirtual" ||
1277 statement==
"invokestatic")
1279 convert_invoke(i_it->source_location, statement, arg0, c, results);
1281 else if(statement==
"return")
1286 else if(statement==
patternt(
"?return"))
1295 else if(statement==
patternt(
"?astore"))
1297 assert(op.size()==3 && results.empty());
1300 else if(statement==
patternt(
"?store"))
1307 else if(statement==
patternt(
"?aload"))
1312 else if(statement==
patternt(
"?load"))
1318 else if(statement==
"ldc" || statement==
"ldc_w" ||
1319 statement==
"ldc2" || statement==
"ldc2_w")
1324 arg0.
id() != ID_java_string_literal && arg0.
id() != ID_type,
1325 "String and Class literals should have been lowered in "
1326 "generate_constant_global_variables");
1330 else if(statement==
"goto" || statement==
"goto_w")
1333 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1337 else if(statement==
"jsr" || statement==
"jsr_w")
1341 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1346 std::next(i_it)->address,
1350 else if(statement==
"ret")
1356 assert(!jsr_ret_targets.empty());
1360 else if(statement==
"iconst_m1")
1362 assert(results.size()==1);
1365 else if(statement==
patternt(
"?const"))
1367 assert(results.size()==1);
1370 else if(statement==
patternt(
"?ipush"))
1374 arg0.
id()==ID_constant,
1375 "ipush argument expected to be constant");
1380 else if(statement==
patternt(
"if_?cmp??"))
1383 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1385 address_map, statement, op, number, i_it->source_location);
1387 else if(statement==
patternt(
"if??"))
1390 statement==
"ifeq"?ID_equal:
1391 statement==
"ifne"?ID_notequal:
1392 statement==
"iflt"?ID_lt:
1393 statement==
"ifge"?ID_ge:
1394 statement==
"ifgt"?ID_gt:
1395 statement==
"ifle"?ID_le:
1398 INVARIANT(!
id.empty(),
"unexpected bytecode-if");
1400 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1401 c =
convert_if(address_map, op,
id, number, i_it->source_location);
1403 else if(statement==
patternt(
"ifnonnull"))
1406 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1409 else if(statement==
patternt(
"ifnull"))
1412 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
1413 c =
convert_ifnull(address_map, op, number, i_it->source_location);
1415 else if(statement==
"iinc")
1419 else if(statement==
patternt(
"?xor"))
1424 else if(statement==
patternt(
"?or"))
1429 else if(statement==
patternt(
"?and"))
1434 else if(statement==
patternt(
"?shl"))
1439 else if(statement==
patternt(
"?shr"))
1444 else if(statement==
patternt(
"?ushr"))
1449 else if(statement==
patternt(
"?add"))
1454 else if(statement==
patternt(
"?sub"))
1459 else if(statement==
patternt(
"?div"))
1464 else if(statement==
patternt(
"?mul"))
1469 else if(statement==
patternt(
"?neg"))
1474 else if(statement==
patternt(
"?rem"))
1477 if(statement==
"frem" || statement==
"drem")
1482 else if(statement==
patternt(
"?cmp"))
1487 else if(statement==
patternt(
"?cmp?"))
1492 else if(statement==
patternt(
"?cmpl"))
1497 else if(statement==
"dup")
1500 results[0]=results[1]=op[0];
1502 else if(statement==
"dup_x1")
1509 else if(statement==
"dup_x2")
1519 else if(statement==
"dup2")
1524 else if(statement==
"dup2_x1")
1529 else if(statement==
"dup2_x2")
1534 else if(statement==
"dconst")
1538 else if(statement==
"fconst")
1542 else if(statement==
"getfield")
1547 else if(statement==
"getstatic")
1551 const auto &field_name=arg0.
get_string(ID_component_name);
1552 const bool is_assertions_disabled_field=
1553 field_name.find(
"$assertionsDisabled")!=std::string::npos;
1560 "getstatic symbol should have been created before method conversion");
1563 arg0, symbol_expr, is_assertions_disabled_field, c, results);
1565 else if(statement==
"putfield")
1570 else if(statement==
"putstatic")
1574 const auto &field_name=arg0.
get_string(ID_component_name);
1580 "putstatic symbol should have been created before method conversion");
1584 else if(statement==
patternt(
"?2?"))
1589 if(results[0].type()!=type)
1590 results[0].make_typecast(type);
1592 else if(statement==
"new")
1596 convert_new(i_it->source_location, arg0, c, results);
1598 else if(statement==
"newarray" ||
1599 statement==
"anewarray")
1605 else if(statement==
"multianewarray")
1609 const std::size_t dimension = numeric_cast_v<std::size_t>(arg1);
1612 assert(results.size()==1);
1615 else if(statement==
"arraylength")
1623 array.
set(ID_java_member_access,
true);
1629 else if(statement==
"tableswitch" ||
1630 statement==
"lookupswitch")
1635 else if(statement==
"pop" || statement==
"pop2")
1639 else if(statement==
"instanceof")
1646 else if(statement ==
"monitorenter" || statement ==
"monitorexit")
1650 else if(statement==
"swap")
1656 else if(statement==
"nop")
1671 if(catch_instruction!=
codet())
1677 if(!i_it->source_location.get_line().empty())
1682 instruction.done =
true;
1683 for(
const auto address : instruction.successors)
1685 address_mapt::iterator a_it2=address_map.find(address);
1691 if(address==exception_row.handler_pc)
1698 if(!
stack.empty() && a_it2->second.predecessors.size()>1)
1705 if(a_it2->second.stack.empty())
1707 for(stackt::iterator s_it=
stack.begin();
1721 a_it2->second.stack.size() ==
stack.size(),
1722 "Stack sizes should be the same.");
1723 stackt::const_iterator os_it=a_it2->second.stack.begin();
1724 for(
auto &expr :
stack)
1726 assert(
has_prefix(os_it->get_string(ID_C_base_name),
"$stack"));
1745 if(last_statement.get_statement()==ID_goto)
1750 last_statement.operands().begin(),
1758 a_it2->second.stack=
stack;
1768 new_symbol.
name=var.get_identifier();
1769 new_symbol.
type=var.type();
1770 new_symbol.
base_name=var.get(ID_C_base_name);
1772 new_symbol.
mode=ID_java;
1789 bool start_new_block=
true;
1790 bool has_seen_previous_address=
false;
1792 for(
const auto &address_pair : address_map)
1795 assert(address_pair.first==address_pair.second.source->address);
1796 const codet &c=address_pair.second.code;
1799 if(!start_new_block)
1800 start_new_block=targets.find(address)!=targets.end();
1803 if(!start_new_block)
1804 start_new_block=address_pair.second.predecessors.size()>1;
1806 if(!start_new_block && has_seen_previous_address)
1809 if(exception_row.start_pc==previous_address)
1811 start_new_block=
true;
1819 root_block.
add(newlabel);
1823 "Block addresses should be unique and increasing");
1831 add_to_block.add(c);
1833 start_new_block=address_pair.second.successors.size()>1;
1835 previous_address=address;
1836 has_seen_previous_address=
true;
1840 std::map<irep_idt, variablet> temporary_variable_live_ranges;
1841 for(
const auto &aentry : address_map)
1845 temporary_variable_live_ranges);
1847 std::vector<const variablet*> vars_to_process;
1849 for(
const auto &v : vlist)
1850 vars_to_process.push_back(&v);
1853 vars_to_process.push_back(
1854 &temporary_variable_live_ranges.at(v.get_identifier()));
1857 vars_to_process.push_back(
1858 &temporary_variable_live_ranges.at(v.get_identifier()));
1860 for(
const auto vp : vars_to_process)
1874 v.start_pc + v.length,
1875 std::numeric_limits<method_offsett>::max(),
1878 for(
const auto vp : vars_to_process)
1884 if(v.symbol_expr.get_identifier().empty())
1890 v.start_pc + v.length,
1891 std::numeric_limits<method_offsett>::max());
1893 block.statements().insert(block.statements().begin(), d);
1926 code_switch.
value() = op[0];
1930 bool is_label =
true;
1931 for(
auto a_it = args.begin(); a_it != args.end();
1932 a_it++, is_label = !is_label)
1939 const mp_integer number = numeric_cast_v<mp_integer>(*a_it);
1945 numeric_cast_v<method_offsett>(number);
1949 if(a_it == args.begin())
1961 code_block.
add(code_case);
1965 code_switch.
body() = code_block;
1974 const irep_idt descriptor = (statement ==
"monitorenter") ?
1975 "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
1976 "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
1989 return std::move(call);
2001 results.insert(results.end(), op.begin(), op.end());
2002 results.insert(results.end(), op.begin(), op.end());
2014 results.insert(results.end(), op.begin() + 1, op.end());
2015 results.insert(results.end(), op.begin(), op.end());
2034 results.insert(results.end(), op.begin(), op.end());
2035 results.insert(results.end(), op2.begin(), op2.end());
2036 results.insert(results.end(), op.begin(), op.end());
2044 const char type_char = statement[0];
2045 const bool is_double(
'd' == type_char);
2046 const bool is_float(
'f' == type_char);
2048 if(is_double || is_float)
2055 if(arg0.
type().
id() != ID_floatbv)
2057 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
2067 const mp_integer value = numeric_cast_v<mp_integer>(arg0);
2081 const bool use_this(statement !=
"invokestatic");
2082 const bool is_virtual(
2083 statement ==
"invokevirtual" || statement ==
"invokeinterface");
2090 if(parameters.empty() || !parameters[0].get_this())
2096 if(statement ==
"invokespecial")
2105 method_type.
set(ID_java_super_method_call,
true);
2111 parameters.insert(parameters.begin(), this_p);
2126 this_arg.
type().
id() == ID_pointer,
"first argument must be a pointer");
2134 for(std::size_t i = 0; i < parameters.size(); i++)
2136 const typet &type = parameters[i].type();
2140 type.
id() == ID_pointer)
2144 call.
arguments()[i].make_typecast(type);
2152 if(return_type.
id() != ID_empty)
2158 results[0] = promoted;
2161 assert(arg0.
id() == ID_virtual_function);
2187 symbol.
type.
set(ID_access, ID_private);
2190 symbol.
mode = ID_java;
2194 debug() <<
"Generating codet: new opaque symbol: method '" << symbol.
name
2261 c = std::move(assert_class);
2274 "java::java.lang.AssertionError")
2283 assert_location.
set(
"user-provided",
true);
2290 assume_location.
set(
"user-provided",
true);
2306 const std::set<method_offsett> &working_set,
2310 std::vector<irep_idt> exception_ids;
2311 std::vector<irep_idt> handler_labels;
2336 exception_ids.push_back(
2341 handler_labels.push_back(
2349 if(!exception_ids.empty())
2353 exception_ids.size() == handler_labels.size(),
2354 "Exception tags and handler labels should be 1-to-1");
2357 for(
size_t i = 0; i < exception_ids.size(); ++i)
2359 exception_list.push_back(
2361 exception_ids[i], handler_labels[i]));
2374 exception_ids.clear();
2375 handler_labels.clear();
2379 size_t start_pc = 0;
2382 bool first_handler =
false;
2388 cur_pc < exception_row.end_pc && !working_set.empty() &&
2389 *working_set.begin() == exception_row.end_pc)
2393 if(exception_row.start_pc != start_pc || !first_handler)
2396 first_handler =
true;
2399 start_pc = exception_row.start_pc;
2427 create.
add(assume_le_max_size);
2446 if(statement ==
"newarray")
2452 else if(
id == ID_char)
2454 else if(
id == ID_float)
2456 else if(
id == ID_double)
2458 else if(
id == ID_byte)
2460 else if(
id == ID_short)
2462 else if(
id == ID_int)
2464 else if(
id == ID_long)
2484 block.
add(assume_le_max_size);
2537 block.
add(clinit_call);
2540 "stack_static_field",
2557 arg0.
get(ID_component_name));
2565 const bool is_assertions_disabled_field,
2571 if(arg0.
type().
id() == ID_struct_tag)
2576 else if(arg0.
type().
id() == ID_pointer)
2585 else if(is_assertions_disabled_field)
2598 else if(is_assertions_disabled_field)
2610 const int nan_value(statement[4] ==
'l' ? -1 : 1);
2660 const std::size_t width = type.
get_size_t(ID_width);
2664 if(lhs.
type() != target)
2667 if(rhs.
type() != target)
2671 if(results[0].type() != op[0].type())
2672 results[0].make_typecast(op[0].type());
2692 const exprt arg1_int_type =
2697 block.
add(code_assign);
2711 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2718 address_map.at(label_number).source->source_location;
2733 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2740 address_map.at(label_number).source->source_location;
2753 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2762 address_map.at(label_number).source->source_location;
2782 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2788 address_map.at(label_number).source->source_location;
2795 const std::vector<method_offsett> &jsr_ret_targets,
2802 for(
size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2807 if(idx == idxlim - 1)
2817 branch.cond().add_source_location() = location;
2818 branch.add_source_location() = location;
2830 const char &type_char = statement[0];
2834 deref.
set(ID_java_member_access,
true);
2841 data_plus_offset.
set(ID_java_array_access,
true);
2857 exprt toassign = op[0];
2858 if(
'a' == statement[0])
2879 const char type_char = statement[0];
2883 deref.
set(ID_java_member_access,
true);
2890 data_plus_offset.
set(ID_java_array_access,
true);
2902 block.
add(array_put);
2914 lambda_method_handles,
2915 method_type.
get_int(ID_java_lambda_method_handle_index));
2916 if(lambda_method_symbol.has_value())
2917 debug() <<
"Converting invokedynamic for lambda: "
2918 << lambda_method_symbol.value().name <<
eom;
2920 debug() <<
"Converting invokedynamic for lambda with unknown handle "
2926 pop(parameters.size());
2930 if(return_type.
id() == ID_empty)
2935 if(!value.has_value())
2938 error() <<
"failed to zero-initialize return type" <<
eom;
2946 const std::vector<method_offsett> &jsr_ret_targets,
2948 std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
2949 &ret_instructions)
const
2952 for(
const auto &retinst : ret_instructions)
2954 auto &a_entry = address_map.at(retinst->address);
2955 a_entry.successors.insert(
2956 a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
2960 std::vector<java_bytecode_convert_methodt::method_offsett>
2966 std::vector<method_offsett>
result;
2967 for(
const auto &exception_row : exception_table)
2969 if(address >= exception_row.start_pc && address < exception_row.end_pc)
2970 result.push_back(exception_row.handler_pc);
2990 &local_variable_table,
3002 typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3003 std::map<std::size_t, base_name_and_identifiert> param_names;
3004 for(
const auto &v : local_variable_table)
3006 if(v.index < slots_for_parameters)
3007 param_names.emplace(
3014 std::size_t param_index = 0;
3015 for(
auto ¶m : parameters)
3024 if(param_index == 0 && param.get_this())
3032 auto param_name = param_names.find(param_index);
3033 if(param_name != param_names.end())
3035 base_name = param_name->second.first;
3036 identifier = param_name->second.second;
3043 const typet &type = param.type();
3050 param.set_base_name(base_name);
3051 param.set_identifier(identifier);
3056 parameter_symbol.
mode = ID_java;
3057 parameter_symbol.
name = identifier;
3058 parameter_symbol.
type = param.type();
3059 symbol_table.
insert(parameter_symbol);
3070 size_t max_array_length,
3071 bool throw_assertion_error,
3075 bool threading_support)
3078 if(std::regex_match(
3080 std::regex(
".*org\\.cprover\\.CProver.*")) &&
3092 throw_assertion_error,
3093 needed_lazy_methods,
3117 return inherited_method.
is_valid();
3127 const irep_idt &component_name)
const
3138 inherited_method.
is_valid(),
"static field should be in symbol table");
3150 const std::string &tmp_var_prefix,
3155 const std::function<bool(
3156 const std::function<
tvt(
const exprt &expr)>,
const exprt &expr)>
3157 entry_matches = [&entry_matches](
3158 const std::function<
tvt(
const exprt &expr)> predicate,
3159 const exprt &expr) {
3160 const tvt &tvres = predicate(expr);
3166 [&predicate, &entry_matches](
const exprt &expr) {
3167 return entry_matches(predicate, expr);
3179 const std::function<
tvt(
const exprt &expr)> has_member_entry = [&identifier](
3180 const exprt &expr) {
3181 const auto member_expr = expr_try_dynamic_cast<member_exprt>(expr);
3183 :
tvt(member_expr->get_component_name() == identifier);
3189 const std::function<
tvt(
const exprt &expr)> is_symbol_entry =
3190 [&identifier](
const exprt &expr) {
3191 const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
3193 :
tvt(symbol_expr->get_identifier() == identifier);
3199 const std::function<
tvt(
const exprt &expr)> is_dereference_entry =
3200 [](
const exprt &expr) {
3201 const auto dereference_expr =
3202 expr_try_dynamic_cast<dereference_exprt>(expr);
3206 for(
auto &stack_entry :
stack)
3213 replace = entry_matches(is_symbol_entry, stack_entry);
3216 replace = entry_matches(is_dereference_entry, stack_entry);
3219 replace = entry_matches(has_member_entry, stack_entry);
3225 tmp_var_prefix, stack_entry.type(), block, stack_entry);
3232 const std::string &tmp_var_prefix,
3233 const typet &tmp_var_type,
3237 const exprt tmp_var=
3240 stack_entry=tmp_var;