53 #include <unordered_set>
76 for(std::size_t i=0; i<parameters.size(); ++i)
80 if(i==0 && parameters[i].get_this())
86 parameters[i].set_base_name(base_name);
87 parameters[i].set_identifier(identifier);
92 parameter_symbol.
mode=ID_java;
93 parameter_symbol.
name=identifier;
94 parameter_symbol.
type=parameters[i].type();
95 symbol_table.
add(parameter_symbol);
111 symbol.
name = identifier;
115 symbol.
type.
set(ID_access, ID_private);
118 symbol.
mode = ID_java;
123 log.
debug() <<
"Generating codet: new opaque symbol: method '" << symbol.
name
125 symbol_table.
add(symbol);
130 return id2string(method_name).find(
"<init>") != std::string::npos;
137 error() <<
"malformed bytecode (pop too high)" <<
eom;
143 for(std::size_t i=0; i<n; i++)
153 std::size_t residue_size=std::min(n,
stack.size());
162 for(std::size_t i=0; i<o.size(); i++)
173 const std::string &prefix,
182 tmp_symbol.
mode=ID_java;
183 tmp_symbol.
name=identifier;
184 tmp_symbol.
type=type;
188 result.set(ID_C_base_name, base_name);
210 const std::size_t number_int =
226 result.set(ID_C_base_name, base_name);
239 const std::string &descriptor,
241 const std::string &class_name,
242 const std::string &method_name,
257 member_type_from_descriptor.has_value() &&
258 member_type_from_descriptor->id() == ID_code,
259 "Must be code type");
260 if(signature.has_value())
264 auto member_type_from_signature =
267 member_type_from_signature.has_value() &&
268 member_type_from_signature->id() == ID_code,
269 "Must be code type");
278 message.debug() <<
"Method: " << class_name <<
"." << method_name
279 <<
"\n signature: " << signature.value()
280 <<
"\n descriptor: " << descriptor
281 <<
"\n different number of parameters, reverting to "
288 message.debug() <<
"Method: " << class_name <<
"." << method_name
289 <<
"\n could not parse signature: " << signature.value()
290 <<
"\n " << e.what() <<
"\n"
291 <<
" reverting to descriptor: " << descriptor
324 method_symbol.
name=method_identifier;
326 method_symbol.
mode=ID_java;
340 member_type.
set(ID_is_synchronized,
true);
342 member_type.
set(ID_is_static,
true);
358 parameters.insert(parameters.begin(), this_p);
384 type_checked_cast<annotated_typet>(
static_cast<typet &
>(member_type))
388 method_symbol.
type=member_type;
397 method_symbol.
type.
set(ID_C_must_not_throw,
true);
407 m, method_identifier, parameters, slots_for_parameters);
409 symbol_table.
add(method_symbol);
414 new_method.set_base_name(method_symbol.
base_name);
415 new_method.set_pretty_name(method_symbol.
pretty_name);
421 .emplace_back(std::move(new_method));
446 if(v.index >= slots_for_parameters)
449 std::ostringstream id_oss;
450 id_oss << method_identifier <<
"::" << v.name;
453 result.
set(ID_C_base_name, v.name);
459 variables[v.index].emplace_back(result, v.start_pc, v.length);
466 std::size_t param_index = 0;
467 for(
const auto ¶m : parameters)
470 variables[param_index].size() <= 1,
471 "should have at most one entry per index");
475 param_index == slots_for_parameters,
476 "java_parameter_count and local computation must agree");
478 for(
auto ¶m : parameters)
487 if(param_index == 0 && param.get_this())
493 else if(!variables[param_index].empty())
496 base_name = variables[param_index][0].symbol_expr.get(ID_C_base_name);
497 identifier = variables[param_index][0].symbol_expr.get(ID_identifier);
508 param.set_base_name(base_name);
509 param.set_identifier(identifier);
515 param_index == slots_for_parameters,
516 "java_parameter_count and local computation must agree");
525 std::size_t param_index = 0;
526 for(
const auto ¶m : parameters)
529 parameter_symbol.
base_name = param.get_base_name();
530 parameter_symbol.
mode = ID_java;
531 parameter_symbol.
name = param.get_identifier();
532 parameter_symbol.
type = param.type();
533 symbol_table.
add(parameter_symbol);
536 variables[param_index].clear();
537 variables[param_index].emplace_back(
540 std::numeric_limits<size_t>::max(),
578 debug() <<
"Generating codet: class " << class_symbol.
name <<
", method "
588 method_symbol.
name == method_identifier,
589 "Name of method symbol shouldn't change");
592 "Base name of method symbol shouldn't change");
595 "Method symbol shouldn't have module");
597 method_symbol.
mode=ID_java;
619 "Member type should have already been marked as a constructor");
627 method_symbol.
type = method_type;
633 if(!method_context || (*method_context)(
id2string(method_identifier)))
637 method_symbol.
value = std::move(code);
644 if(bytecode ==
patternt(
"if_?cmplt"))
646 if(bytecode ==
patternt(
"if_?cmple"))
648 if(bytecode ==
patternt(
"if_?cmpgt"))
650 if(bytecode ==
patternt(
"if_?cmpge"))
652 if(bytecode ==
patternt(
"if_?cmpeq"))
654 if(bytecode ==
patternt(
"if_?cmpne"))
657 throw "unhandled java comparison instruction";
669 const exprt &pointer,
675 const exprt typed_pointer =
681 const auto type_of = [&ns](
const exprt &object) {
687 while(type_of(accessed_object).get_component(component_name).is_nil())
689 const auto components = type_of(accessed_object).components();
691 components.size() != 0,
692 "infer_opaque_type_fields should guarantee that a member access has a "
693 "corresponding field");
696 accessed_object =
member_exprt(accessed_object, components.front());
699 accessed_object, type_of(accessed_object).get_component(component_name));
716 if(g.get_destination()==old_label)
717 g.set_destination(new_label);
754 next_block_start_address,
793 assert(!tree.
branch.empty());
796 const auto afterstart=
802 auto findstart=afterstart;
813 const auto findlim_block_start_address =
823 auto child_iter = this_block.
statements().begin();
826 while(child_iter != this_block.
statements().end() &&
827 child_iter->get_statement() == ID_decl)
829 assert(child_iter != this_block.
statements().end());
830 std::advance(child_iter, child_offset);
831 assert(child_iter != this_block.
statements().end());
835 bool single_child(afterstart==findlim);
840 tree.
branch[child_offset],
844 findlim_block_start_address,
862 auto checkit=amap.
find(*findstart);
863 assert(checkit!=amap.end());
866 checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
869 for(
auto p : checkit->second.predecessors)
871 if(p<(*findstart) || p>=findlim_block_start_address)
873 debug() <<
"Generating codet: "
874 <<
"warning: refusing to create lexical block spanning "
875 << (*findstart) <<
"-" << findlim_block_start_address
876 <<
" due to incoming edge " << p <<
" -> "
877 << checkit->first <<
eom;
887 const irep_idt child_label_name=child_label.get_label();
888 std::string new_label_str =
id2string(child_label_name);
890 irep_idt new_label_irep(new_label_str);
894 auto nblocks=std::distance(findstart, findlim);
896 debug() <<
"Generating codet: combining "
897 << std::distance(findstart, findlim)
898 <<
" blocks for addresses " << (*findstart) <<
"-"
899 << findlim_block_start_address <<
eom;
902 auto &this_block_children = this_block.
statements();
903 assert(tree.
branch.size()==this_block_children.size());
904 for(
auto blockidx=child_offset, blocklim=child_offset+nblocks;
907 newblock.
add(this_block_children[blockidx]);
915 auto delfirst=this_block_children.begin();
916 std::advance(delfirst, child_offset+1);
917 auto dellim=delfirst;
918 std::advance(dellim, nblocks-1);
919 this_block_children.erase(delfirst, dellim);
920 this_block_children[child_offset].swap(newlabel);
924 auto branchstart=tree.
branch.begin();
925 std::advance(branchstart, child_offset);
926 auto branchlim=branchstart;
927 std::advance(branchlim, nblocks);
928 for(
auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
929 newnode.
branch.push_back(std::move(*branchiter));
931 tree.
branch.erase(branchstart, branchlim);
933 assert(tree.
branch.size()==this_block_children.size());
936 std::advance(branchaddriter, child_offset);
937 auto branchaddrlim=branchaddriter;
938 std::advance(branchaddrlim, nblocks);
947 tree.
branch[child_offset]=std::move(newnode);
954 this_block_children[child_offset]).code());
960 std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
962 if(e.
id()==ID_symbol)
965 auto findit = result.emplace(
966 std::piecewise_construct,
967 std::forward_as_tuple(symexpr.get_identifier()),
968 std::forward_as_tuple(symexpr, pc, 1));
971 auto &var = findit.first->second;
975 var.length+=(var.start_pc-pc);
980 var.length=std::max(var.length, (pc-var.start_pc)+1);
1013 if(ty.
id()==ID_pointer)
1026 std::size_t param_index = method_type.
has_this() ? 1 : 0;
1029 "parameters and parameter annotations mismatch");
1035 param_annotations,
"java::javax.validation.constraints.NotNull") ||
1037 param_annotations,
"java::org.jetbrains.annotations.NotNull") ||
1039 param_annotations,
"org.eclipse.jdt.annotation.NonNull") ||
1041 param_annotations,
"java::edu.umd.cs.findbugs.annotations.NonNull"))
1044 parameters[param_index].get_identifier();
1046 const auto param_type =
1047 type_try_dynamic_cast<pointer_typet>(param_symbol.
type);
1053 check_loc.
set_comment(
"Not null annotation check");
1057 code.
add(std::move(code_assert));
1079 std::set<method_offsett> targets;
1081 std::vector<method_offsett> jsr_ret_targets;
1082 std::vector<instructionst::const_iterator> ret_instructions;
1084 for(
auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1087 std::pair<address_mapt::iterator, bool> a_entry=
1088 address_map.insert(std::make_pair(i_it->address, ins));
1089 assert(a_entry.second);
1092 assert(a_entry.first==--address_map.end());
1094 const auto bytecode = i_it->bytecode;
1107 instructionst::const_iterator next=i_it;
1108 if(++next!=instructions.end())
1109 a_entry.first->second.successors.push_back(next->address);
1133 const std::vector<method_offsett> handler =
1135 std::list<method_offsett> &successors = a_entry.first->second.successors;
1136 successors.insert(successors.end(), handler.begin(), handler.end());
1137 targets.insert(handler.begin(), handler.end());
1142 bytecode ==
patternt(
"if_?cmp??") ||
1153 targets.insert(target);
1155 a_entry.first->second.successors.push_back(target);
1159 auto next = std::next(i_it);
1161 next != instructions.end(),
"jsr should have valid return address");
1162 targets.insert(next->address);
1163 jsr_ret_targets.push_back(next->address);
1169 for(
const auto &arg : i_it->args)
1174 targets.insert(target);
1175 a_entry.first->second.successors.push_back(target);
1180 else if(bytecode ==
BC_ret)
1183 ret_instructions.push_back(i_it);
1188 for(
const auto &address : address_map)
1190 for(
auto s : address.second.successors)
1192 const auto a_it = address_map.find(s);
1194 a_it->second.predecessors.insert(address.first);
1208 std::set<method_offsett> working_set;
1210 if(!instructions.empty())
1211 working_set.insert(instructions.front().address);
1213 while(!working_set.empty())
1215 auto cur = working_set.begin();
1216 auto address_it = address_map.find(*cur);
1218 auto &instruction = address_it->second;
1220 working_set.erase(cur);
1222 if(instruction.done)
1225 instruction.successors.begin(), instruction.successors.end());
1227 instructionst::const_iterator i_it = instruction.source;
1228 stack.swap(instruction.stack);
1229 instruction.stack.clear();
1230 codet &c = instruction.code;
1233 stack.empty() || instruction.predecessors.size() <= 1 ||
1239 const auto bytecode = i_it->bytecode;
1241 const std::string statement = stmt_bytecode_info.
mnemonic;
1244 if(statement.size()>=2 &&
1245 statement[statement.size()-2]==
'_' &&
1246 isdigit(statement[statement.size()-1]))
1251 std::string(
id2string(statement), statement.size()-1, 1)),
1263 if(cur_pc==it->handler_pc)
1266 catch_type !=
typet() ||
1273 catch_type=it->catch_type;
1279 if(catch_type!=
typet())
1293 stack.push_back(catch_var);
1303 assert(results.size()==1);
1331 "java::org.cprover.CProver.assume:(Z)V")
1336 "function expected to have exactly one parameter");
1342 arg0.
get(ID_identifier) ==
"java::org.cprover.CProver.atomicBegin:()V")
1344 c =
codet(ID_atomic_begin);
1349 arg0.
get(ID_identifier) ==
"java::org.cprover.CProver.atomicEnd:()V")
1351 c =
codet(ID_atomic_end);
1358 expr_try_dynamic_cast<class_method_descriptor_exprt>(arg0);
1361 class_method_descriptor,
1362 "invokeinterface, invokespecial, invokevirtual and invokestatic should "
1363 "be called with a class method descriptor expression as arg0");
1366 i_it->source_location, statement, *class_method_descriptor, c, results);
1373 else if(bytecode ==
patternt(
"?return"))
1382 else if(bytecode ==
patternt(
"?astore"))
1387 else if(bytecode ==
patternt(
"?store") || bytecode ==
patternt(
"?store_?"))
1394 else if(bytecode ==
patternt(
"?aload"))
1402 results[0] =
convert_load(arg0, statement[0], i_it->address);
1410 "String and Class literals should have been lowered in "
1411 "generate_constant_global_variables");
1433 std::next(i_it)->address,
1437 else if(bytecode ==
BC_ret)
1443 assert(!jsr_ret_targets.empty());
1449 assert(results.size()==1);
1452 else if(bytecode ==
patternt(
"?const_?"))
1454 assert(results.size()==1);
1457 else if(bytecode ==
patternt(
"?ipush"))
1461 arg0.
id()==ID_constant,
1462 "ipush argument expected to be constant");
1465 else if(bytecode ==
patternt(
"if_?cmp??"))
1471 address_map, bytecode, op, number, i_it->source_location);
1473 else if(bytecode ==
patternt(
"if??"))
1477 bytecode ==
BC_ifeq ? ID_equal :
1478 bytecode ==
BC_ifne ? ID_notequal :
1486 INVARIANT(!
id.empty(),
"unexpected bytecode-if");
1490 c =
convert_if(address_map, op,
id, number, i_it->source_location);
1492 else if(bytecode ==
patternt(
"ifnonnull"))
1499 else if(bytecode ==
patternt(
"ifnull"))
1504 c =
convert_ifnull(address_map, op, number, i_it->source_location);
1510 else if(bytecode ==
patternt(
"?xor"))
1515 else if(bytecode ==
patternt(
"?or"))
1520 else if(bytecode ==
patternt(
"?and"))
1525 else if(bytecode ==
patternt(
"?shl"))
1530 else if(bytecode ==
patternt(
"?shr"))
1535 else if(bytecode ==
patternt(
"?ushr"))
1540 else if(bytecode ==
patternt(
"?add"))
1545 else if(bytecode ==
patternt(
"?sub"))
1550 else if(bytecode ==
patternt(
"?div"))
1555 else if(bytecode ==
patternt(
"?mul"))
1560 else if(bytecode ==
patternt(
"?neg"))
1565 else if(bytecode ==
patternt(
"?rem"))
1573 else if(bytecode ==
patternt(
"?cmp"))
1578 else if(bytecode ==
patternt(
"?cmp?"))
1583 else if(bytecode ==
patternt(
"?cmpl"))
1588 else if(bytecode ==
BC_dup)
1591 results[0]=results[1]=op[0];
1629 to_member(op[0], expr_dynamic_cast<fieldref_exprt>(arg0),
ns));
1634 const auto &field_name=arg0.
get_string(ID_component_name);
1635 const bool is_assertions_disabled_field=
1636 field_name.find(
"$assertionsDisabled")!=std::string::npos;
1646 i_it->source_location,
1649 is_assertions_disabled_field,
1661 const auto &field_name=arg0.
get_string(ID_component_name);
1672 else if(bytecode ==
patternt(
"?2?"))
1687 else if(bytecode ==
BC_new)
1691 convert_new(i_it->source_location, arg0, c, results);
1703 const std::size_t dimension =
1707 assert(results.size()==1);
1717 array.set(ID_java_member_access,
true);
1747 else if(bytecode ==
BC_nop)
1762 if(catch_instruction.has_value())
1769 if(!i_it->source_location.get_line().empty())
1774 instruction.done =
true;
1775 for(
const auto address : instruction.successors)
1777 address_mapt::iterator a_it2=address_map.find(address);
1783 if(address==exception_row.handler_pc)
1790 if(!
stack.empty() && a_it2->second.predecessors.size()>1)
1797 if(a_it2->second.stack.empty())
1799 for(stackt::iterator s_it=
stack.begin();
1813 a_it2->second.stack.size() ==
stack.size(),
1814 "Stack sizes should be the same.");
1815 stackt::const_iterator os_it=a_it2->second.stack.begin();
1816 for(
auto &expr :
stack)
1818 assert(
has_prefix(os_it->get_string(ID_C_base_name),
"$stack"));
1839 if(last_statement.get_statement()==ID_goto)
1842 if(last_statement.get_statement() != ID_block)
1846 last_statement.operands().begin(),
1854 a_it2->second.stack=
stack;
1864 new_symbol.
name=var.get_identifier();
1865 new_symbol.
type=var.type();
1866 new_symbol.
base_name=var.get(ID_C_base_name);
1868 new_symbol.
mode=ID_java;
1885 bool start_new_block=
true;
1886 bool has_seen_previous_address=
false;
1888 for(
const auto &address_pair : address_map)
1891 assert(address_pair.first==address_pair.second.source->address);
1892 const codet &c=address_pair.second.code;
1895 if(!start_new_block)
1896 start_new_block=targets.find(address)!=targets.end();
1899 if(!start_new_block)
1900 start_new_block=address_pair.second.predecessors.size()>1;
1905 if(!start_new_block && has_seen_previous_address)
1908 if(exception_row.start_pc==previous_address)
1910 start_new_block=
true;
1922 "Block addresses should be unique and increasing");
1930 add_to_block.add(c);
1932 start_new_block=address_pair.second.successors.size()>1;
1934 previous_address=address;
1935 has_seen_previous_address=
true;
1939 std::map<irep_idt, variablet> temporary_variable_live_ranges;
1940 for(
const auto &aentry : address_map)
1944 temporary_variable_live_ranges);
1946 std::vector<const variablet*> vars_to_process;
1948 for(
const auto &v : vlist)
1949 vars_to_process.push_back(&v);
1952 vars_to_process.push_back(
1953 &temporary_variable_live_ranges.at(v.get_identifier()));
1956 vars_to_process.push_back(
1957 &temporary_variable_live_ranges.at(v.get_identifier()));
1959 for(
const auto vp : vars_to_process)
1973 v.start_pc + v.length,
1974 std::numeric_limits<method_offsett>::max(),
1977 for(
const auto vp : vars_to_process)
1983 if(v.symbol_expr.get_identifier().empty())
1989 v.start_pc + v.length,
1990 std::numeric_limits<method_offsett>::max());
1992 block.statements().insert(block.statements().begin(), d);
2026 bool is_label =
true;
2027 for(
auto a_it = args.begin(); a_it != args.end();
2028 a_it++, is_label = !is_label)
2039 numeric_cast_v<method_offsett>(number);
2043 if(a_it == args.begin())
2048 code_block.
add(std::move(code_case), location);
2057 code_block.
add(std::move(code_case), location);
2062 code_switcht code_switch(op[0], std::move(code_block));
2072 const irep_idt descriptor = (statement ==
"monitorenter") ?
2073 "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
2074 "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
2087 return std::move(call);
2099 results.insert(results.end(), op.begin(), op.end());
2100 results.insert(results.end(), op.begin(), op.end());
2112 results.insert(results.end(), op.begin() + 1, op.end());
2113 results.insert(results.end(), op.begin(), op.end());
2132 results.insert(results.end(), op.begin(), op.end());
2133 results.insert(results.end(), op2.begin(), op2.end());
2134 results.insert(results.end(), op.begin(), op.end());
2142 const char type_char = statement[0];
2143 const bool is_double(
'd' == type_char);
2144 const bool is_float(
'f' == type_char);
2146 if(is_double || is_float)
2153 if(arg0.
type().
id() != ID_floatbv)
2155 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
2165 const mp_integer value = numeric_cast_v<mp_integer>(arg0);
2181 parameters.size() == arguments.size(),
2182 "for each parameter there must be exactly one argument");
2183 for(std::size_t i = 0; i < parameters.size(); i++)
2185 const typet &type = parameters[i].type();
2189 type.
id() == ID_pointer)
2203 const bool use_this(statement !=
"invokestatic");
2204 const bool is_virtual(
2205 statement ==
"invokevirtual" || statement ==
"invokeinterface");
2209 !invoked_method_id.
empty(),
2210 "invoke statement arg0 must have an identifier");
2225 "Function return type must not change in kind");
2226 class_method_descriptor.
type() = method_symbol->second.type;
2240 if(parameters.empty() || !parameters[0].get_this())
2247 parameters.insert(parameters.begin(), this_p);
2252 if(statement ==
"invokespecial")
2261 method_type.
set(ID_java_super_method_call,
true);
2271 !use_this || arguments.front().type().id() == ID_pointer,
2272 "first argument must be a pointer");
2280 if(return_type.
id() != ID_empty)
2286 results[0] = promoted;
2304 class_method_descriptor.
class_id(),
2313 class_method_descriptor.
class_id(),
2324 function = class_method_descriptor;
2331 function =
symbol_exprt(invoked_method_id, method_type);
2341 std::move(lhs), std::move(
function), std::move(arguments));
2384 c = std::move(assert_class);
2397 "java::java.lang.AssertionError") &&
2406 assert_location.set(
"user-provided",
true);
2407 assert_location.set_property_class(ID_assertion);
2408 assert_code.add_source_location() = assert_location;
2412 assume_location.
set(
"user-provided",
true);
2413 assume_code.add_source_location() = assume_location;
2428 const std::set<method_offsett> &working_set,
2437 typedef std::vector<std::reference_wrapper<
2439 std::map<std::size_t, exceptionst> exceptions_by_end;
2444 exceptions_by_end[exception.
end_pc].push_back(exception);
2446 for(
const auto &exceptions : exceptions_by_end)
2454 : exceptions.second)
2456 exception_list.emplace_back(
2463 code =
code_blockt({ std::move(catch_push), code });
2483 auto next_opcode_it = std::find_if(
2484 working_set.begin(),
2487 if(next_opcode_it != working_set.end())
2490 std::set<std::size_t> start_positions;
2494 if(*next_opcode_it == exception_row.end_pc)
2495 start_positions.insert(exception_row.start_pc);
2497 for(std::size_t handler = 0; handler < start_positions.size(); ++handler)
2524 create.
add(assume_le_max_size);
2542 if(statement ==
"newarray")
2549 else if(
id == ID_char)
2551 else if(
id == ID_float)
2553 else if(
id == ID_double)
2555 else if(
id == ID_byte)
2557 else if(
id == ID_short)
2559 else if(
id == ID_int)
2561 else if(
id == ID_long)
2583 block.
add(std::move(assume_le_max_size));
2636 block.
add(clinit_call);
2639 "stack_static_field",
2662 const bool is_assertions_disabled_field,
2668 if(arg0.
type().
id() == ID_struct_tag)
2673 else if(arg0.
type().
id() == ID_pointer)
2682 else if(is_assertions_disabled_field)
2697 else if(is_assertions_disabled_field)
2709 const int nan_value(statement[4] ==
'l' ? -1 : 1);
2787 const exprt arg1_int_type =
2795 block.
add(std::move(code_assign));
2809 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2816 address_map.at(label_number).source->source_location;
2831 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2838 address_map.at(label_number).source->source_location;
2851 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2860 address_map.at(label_number).source->source_location;
2880 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2886 address_map.at(label_number).source->source_location;
2893 const std::vector<method_offsett> &jsr_ret_targets,
2899 auto retvar =
variable(arg0,
'a', address);
2900 for(
size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2905 if(idx == idxlim - 1)
2915 branch.cond().add_source_location() = location;
2916 branch.add_source_location() = location;
2931 const auto ref_type =
2932 type_try_dynamic_cast<java_reference_typet>(expr.
type());
2933 const bool typecast_not_needed =
2934 ref_type && ((type_char ==
'b' && ref_type->subtype().get_identifier() ==
2935 "java::array[boolean]") ||
2937 return typecast_not_needed ? expr
2946 const char type_char = statement[0];
2949 deref.
set(ID_java_member_access,
true);
2951 auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
2955 plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
2957 data_plus_offset.
set(ID_java_array_access,
true);
2967 if(type_char ==
'i')
2971 type_try_dynamic_cast<bitvector_typet>(var.
type())->get_width() <= 32,
2972 "iload can be used for boolean, byte, short, int and char");
2978 "Variable type must match [adflv]load return type");
3013 const char type_char = statement[0];
3016 deref.
set(ID_java_member_access,
true);
3018 auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
3022 plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
3024 data_plus_offset.
set(ID_java_array_access,
true);
3033 block.
add(std::move(array_put), location);
3039 std::size_t instruction_address,
3059 if(!value.has_value())
3062 error() <<
"failed to zero-initialize return type" <<
eom;
3086 arguments.insert(arguments.begin(), new_instance);
3093 result.add(constructor_call);
3100 result_code = std::move(
result);
3102 if(return_type.
id() == ID_empty)
3105 return new_instance;
3110 const std::vector<method_offsett> &jsr_ret_targets,
3112 std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
3113 &ret_instructions)
const
3116 for(
const auto &retinst : ret_instructions)
3118 auto &a_entry = address_map.at(retinst->address);
3119 a_entry.successors.insert(
3120 a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
3124 std::vector<java_bytecode_convert_methodt::method_offsett>
3130 std::vector<method_offsett>
result;
3131 for(
const auto &exception_row : exception_table)
3133 if(address >= exception_row.start_pc && address < exception_row.end_pc)
3134 result.push_back(exception_row.handler_pc);
3154 &local_variable_table,
3166 typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3167 std::map<std::size_t, base_name_and_identifiert> param_names;
3168 for(
const auto &v : local_variable_table)
3170 if(v.index < slots_for_parameters)
3171 param_names.emplace(
3178 std::size_t param_index = 0;
3179 for(
auto ¶m : parameters)
3188 if(param_index == 0 && param.get_this())
3191 base_name = ID_this;
3196 auto param_name = param_names.find(param_index);
3197 if(param_name != param_names.end())
3199 base_name = param_name->second.first;
3200 identifier = param_name->second.second;
3207 const typet &type = param.type();
3214 param.set_base_name(base_name);
3215 param.set_identifier(identifier);
3220 parameter_symbol.
mode = ID_java;
3221 parameter_symbol.
name = identifier;
3222 parameter_symbol.
type = param.type();
3223 symbol_table.
insert(parameter_symbol);
3234 size_t max_array_length,
3235 bool throw_assertion_error,
3239 bool threading_support,
3241 bool assert_no_exceptions_thrown)
3248 throw_assertion_error,
3249 needed_lazy_methods,
3253 assert_no_exceptions_thrown);
3265 const irep_idt &mangled_method_name)
const
3270 return inherited_method.has_value();
3280 const irep_idt &component_name)
const
3286 inherited_method.has_value(),
"static field should be in symbol table");
3288 return inherited_method->get_full_component_identifier();
3298 const std::string &tmp_var_prefix,
3303 const std::function<bool(
3304 const std::function<
tvt(
const exprt &expr)>,
const exprt &expr)>
3305 entry_matches = [&entry_matches](
3306 const std::function<
tvt(
const exprt &expr)> predicate,
3307 const exprt &expr) {
3308 const tvt &tvres = predicate(expr);
3314 [&predicate, &entry_matches](
const exprt &expr) {
3315 return entry_matches(predicate, expr);
3327 const std::function<
tvt(
const exprt &expr)> has_member_entry = [&identifier](
3328 const exprt &expr) {
3329 const auto member_expr = expr_try_dynamic_cast<member_exprt>(expr);
3331 :
tvt(member_expr->get_component_name() == identifier);
3337 const std::function<
tvt(
const exprt &expr)> is_symbol_entry =
3338 [&identifier](
const exprt &expr) {
3339 const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
3341 :
tvt(symbol_expr->get_identifier() == identifier);
3347 const std::function<
tvt(
const exprt &expr)> is_dereference_entry =
3348 [](
const exprt &expr) {
3349 const auto dereference_expr =
3350 expr_try_dynamic_cast<dereference_exprt>(expr);
3354 for(
auto &stack_entry :
stack)
3361 replace = entry_matches(is_symbol_entry, stack_entry);
3364 replace = entry_matches(is_dereference_entry, stack_entry);
3367 replace = entry_matches(has_member_entry, stack_entry);
3373 tmp_var_prefix, stack_entry.type(), block, stack_entry);
3380 const std::string &tmp_var_prefix,
3381 const typet &tmp_var_type,
3385 const exprt tmp_var=
3388 stack_entry=tmp_var;