54 #include <unordered_set>
77 for(std::size_t i=0; i<parameters.size(); ++i)
81 if(i==0 && parameters[i].get_this())
87 parameters[i].set_base_name(base_name);
88 parameters[i].set_identifier(identifier);
93 parameter_symbol.
mode=ID_java;
94 parameter_symbol.
name=identifier;
95 parameter_symbol.
type=parameters[i].type();
96 symbol_table.
add(parameter_symbol);
112 symbol.
name = identifier;
116 symbol.
type.
set(ID_access, ID_private);
119 symbol.
mode = ID_java;
124 log.
debug() <<
"Generating codet: new opaque symbol: method '" << symbol.
name
126 symbol_table.
add(symbol);
131 return id2string(method_name).find(
"<init>") != std::string::npos;
144 for(std::size_t i=0; i<n; i++)
154 std::size_t residue_size=std::min(n,
stack.size());
163 for(std::size_t i=0; i<o.size(); i++)
174 const std::string &prefix,
183 tmp_symbol.
mode=ID_java;
184 tmp_symbol.
name=identifier;
185 tmp_symbol.
type=type;
189 result.
set(ID_C_base_name, base_name);
211 const std::size_t number_int =
227 result.
set(ID_C_base_name, base_name);
229 return std::move(result);
240 const std::string &descriptor,
242 const std::string &class_name,
243 const std::string &method_name,
258 member_type_from_descriptor.has_value() &&
259 member_type_from_descriptor->id() == ID_code,
260 "Must be code type");
261 if(signature.has_value())
265 auto member_type_from_signature =
268 member_type_from_signature.has_value() &&
269 member_type_from_signature->id() == ID_code,
270 "Must be code type");
279 message.debug() <<
"Method: " << class_name <<
"." << method_name
280 <<
"\n signature: " << signature.value()
281 <<
"\n descriptor: " << descriptor
282 <<
"\n different number of parameters, reverting to "
289 message.debug() <<
"Method: " << class_name <<
"." << method_name
290 <<
"\n could not parse signature: " << signature.value()
291 <<
"\n " << e.what() <<
"\n"
292 <<
" reverting to descriptor: " << descriptor
325 method_symbol.
name=method_identifier;
327 method_symbol.
mode=ID_java;
341 member_type.
set(ID_is_synchronized,
true);
343 member_type.
set(ID_is_static,
true);
359 parameters.insert(parameters.begin(), this_p);
385 type_checked_cast<annotated_typet>(
static_cast<typet &
>(member_type))
389 method_symbol.
type=member_type;
398 method_symbol.
type.
set(ID_C_must_not_throw,
true);
408 m, method_identifier, parameters, slots_for_parameters);
410 symbol_table.
add(method_symbol);
415 new_method.set_base_name(method_symbol.
base_name);
416 new_method.set_pretty_name(method_symbol.
pretty_name);
422 .emplace_back(std::move(new_method));
447 if(v.index >= slots_for_parameters)
450 std::ostringstream id_oss;
451 id_oss << method_identifier <<
"::" << v.name;
454 result.
set(ID_C_base_name, v.name);
460 variables[v.index].emplace_back(result, v.start_pc, v.length);
467 std::size_t param_index = 0;
468 for(
const auto ¶m : parameters)
471 variables[param_index].size() <= 1,
472 "should have at most one entry per index");
476 param_index == slots_for_parameters,
477 "java_parameter_count and local computation must agree");
479 for(
auto ¶m : parameters)
488 if(param_index == 0 && param.get_this())
494 else if(!variables[param_index].empty())
497 base_name = variables[param_index][0].symbol_expr.get(ID_C_base_name);
498 identifier = variables[param_index][0].symbol_expr.get(ID_identifier);
509 param.set_base_name(base_name);
510 param.set_identifier(identifier);
516 param_index == slots_for_parameters,
517 "java_parameter_count and local computation must agree");
526 std::size_t param_index = 0;
527 for(
const auto ¶m : parameters)
530 parameter_symbol.
base_name = param.get_base_name();
531 parameter_symbol.
mode = ID_java;
532 parameter_symbol.
name = param.get_identifier();
533 parameter_symbol.
type = param.type();
534 symbol_table.
add(parameter_symbol);
537 variables[param_index].clear();
538 variables[param_index].emplace_back(
541 std::numeric_limits<size_t>::max(),
579 log.
debug() <<
"Generating codet: class " << class_symbol.
name <<
", method "
589 method_symbol.
name == method_identifier,
590 "Name of method symbol shouldn't change");
593 "Base name of method symbol shouldn't change");
596 "Method symbol shouldn't have module");
598 method_symbol.
mode=ID_java;
620 "Member type should have already been marked as a constructor");
628 method_symbol.
type = method_type;
634 if(!method_context || (*method_context)(
id2string(method_identifier)))
638 method_symbol.
value = std::move(code);
645 if(bytecode ==
patternt(
"if_?cmplt"))
647 if(bytecode ==
patternt(
"if_?cmple"))
649 if(bytecode ==
patternt(
"if_?cmpgt"))
651 if(bytecode ==
patternt(
"if_?cmpge"))
653 if(bytecode ==
patternt(
"if_?cmpeq"))
655 if(bytecode ==
patternt(
"if_?cmpne"))
658 throw "unhandled java comparison instruction";
670 const exprt &pointer,
676 const exprt typed_pointer =
682 const auto type_of = [&ns](
const exprt &object) {
688 while(type_of(accessed_object).get_component(component_name).is_nil())
690 const auto components = type_of(accessed_object).components();
692 components.size() != 0,
693 "infer_opaque_type_fields should guarantee that a member access has a "
694 "corresponding field");
697 accessed_object =
member_exprt(accessed_object, components.front());
700 accessed_object, type_of(accessed_object).get_component(component_name));
717 if(g.get_destination()==old_label)
718 g.set_destination(new_label);
755 next_block_start_address,
794 assert(!tree.
branch.empty());
797 const auto afterstart=
803 auto findstart=afterstart;
814 const auto findlim_block_start_address =
824 auto child_iter = this_block.
statements().begin();
827 while(child_iter != this_block.
statements().end() &&
828 child_iter->get_statement() == ID_decl)
830 assert(child_iter != this_block.
statements().end());
831 std::advance(child_iter, child_offset);
832 assert(child_iter != this_block.
statements().end());
836 bool single_child(afterstart==findlim);
841 tree.
branch[child_offset],
845 findlim_block_start_address,
863 auto checkit=amap.
find(*findstart);
864 assert(checkit!=amap.end());
867 checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
870 for(
auto p : checkit->second.predecessors)
872 if(p<(*findstart) || p>=findlim_block_start_address)
875 <<
"warning: refusing to create lexical block spanning "
876 << (*findstart) <<
"-" << findlim_block_start_address
877 <<
" due to incoming edge " << p <<
" -> " << checkit->first
888 const irep_idt child_label_name=child_label.get_label();
889 std::string new_label_str =
id2string(child_label_name);
891 irep_idt new_label_irep(new_label_str);
895 auto nblocks=std::distance(findstart, findlim);
897 log.
debug() <<
"Generating codet: combining "
898 << std::distance(findstart, findlim) <<
" blocks for addresses "
899 << (*findstart) <<
"-" << findlim_block_start_address
903 auto &this_block_children = this_block.
statements();
904 assert(tree.
branch.size()==this_block_children.size());
905 for(
auto blockidx=child_offset, blocklim=child_offset+nblocks;
908 newblock.
add(this_block_children[blockidx]);
916 auto delfirst=this_block_children.begin();
917 std::advance(delfirst, child_offset+1);
918 auto dellim=delfirst;
919 std::advance(dellim, nblocks-1);
920 this_block_children.erase(delfirst, dellim);
921 this_block_children[child_offset].swap(newlabel);
925 auto branchstart=tree.
branch.begin();
926 std::advance(branchstart, child_offset);
927 auto branchlim=branchstart;
928 std::advance(branchlim, nblocks);
929 for(
auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
930 newnode.
branch.push_back(std::move(*branchiter));
932 tree.
branch.erase(branchstart, branchlim);
934 assert(tree.
branch.size()==this_block_children.size());
937 std::advance(branchaddriter, child_offset);
938 auto branchaddrlim=branchaddriter;
939 std::advance(branchaddrlim, nblocks);
948 tree.
branch[child_offset]=std::move(newnode);
955 this_block_children[child_offset]).code());
961 std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
963 if(e.
id()==ID_symbol)
966 auto findit = result.emplace(
967 std::piecewise_construct,
968 std::forward_as_tuple(symexpr.get_identifier()),
969 std::forward_as_tuple(symexpr, pc, 1));
972 auto &var = findit.first->second;
976 var.length+=(var.start_pc-pc);
981 var.length=std::max(var.length, (pc-var.start_pc)+1);
1014 if(ty.
id()==ID_pointer)
1027 std::size_t param_index = method_type.
has_this() ? 1 : 0;
1030 "parameters and parameter annotations mismatch");
1036 param_annotations,
"java::javax.validation.constraints.NotNull") ||
1038 param_annotations,
"java::org.jetbrains.annotations.NotNull") ||
1040 param_annotations,
"org.eclipse.jdt.annotation.NonNull") ||
1042 param_annotations,
"java::edu.umd.cs.findbugs.annotations.NonNull"))
1045 parameters[param_index].get_identifier();
1047 const auto param_type =
1048 type_try_dynamic_cast<pointer_typet>(param_symbol.
type);
1054 check_loc.
set_comment(
"Not null annotation check");
1058 code.
add(std::move(code_assert));
1080 std::set<method_offsett> targets;
1082 std::vector<method_offsett> jsr_ret_targets;
1083 std::vector<instructionst::const_iterator> ret_instructions;
1085 for(
auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1088 std::pair<address_mapt::iterator, bool> a_entry=
1089 address_map.insert(std::make_pair(i_it->address, ins));
1090 assert(a_entry.second);
1093 assert(a_entry.first==--address_map.end());
1095 const auto bytecode = i_it->bytecode;
1108 instructionst::const_iterator next=i_it;
1109 if(++next!=instructions.end())
1110 a_entry.first->second.successors.push_back(next->address);
1134 const std::vector<method_offsett> handler =
1136 std::list<method_offsett> &successors = a_entry.first->second.successors;
1137 successors.insert(successors.end(), handler.begin(), handler.end());
1138 targets.insert(handler.begin(), handler.end());
1143 bytecode ==
patternt(
"if_?cmp??") ||
1154 targets.insert(target);
1156 a_entry.first->second.successors.push_back(target);
1160 auto next = std::next(i_it);
1162 next != instructions.end(),
"jsr should have valid return address");
1163 targets.insert(next->address);
1164 jsr_ret_targets.push_back(next->address);
1170 for(
const auto &arg : i_it->args)
1175 targets.insert(target);
1176 a_entry.first->second.successors.push_back(target);
1181 else if(bytecode ==
BC_ret)
1184 ret_instructions.push_back(i_it);
1189 for(
const auto &address : address_map)
1191 for(
auto s : address.second.successors)
1193 const auto a_it = address_map.find(s);
1195 a_it->second.predecessors.insert(address.first);
1209 std::set<method_offsett> working_set;
1211 if(!instructions.empty())
1212 working_set.insert(instructions.front().address);
1214 while(!working_set.empty())
1216 auto cur = working_set.begin();
1217 auto address_it = address_map.find(*cur);
1219 auto &instruction = address_it->second;
1221 working_set.erase(cur);
1223 if(instruction.done)
1226 instruction.successors.begin(), instruction.successors.end());
1228 instructionst::const_iterator i_it = instruction.source;
1229 stack.swap(instruction.stack);
1230 instruction.stack.clear();
1231 codet &c = instruction.code;
1234 stack.empty() || instruction.predecessors.size() <= 1 ||
1240 const auto bytecode = i_it->bytecode;
1242 const std::string statement = stmt_bytecode_info.
mnemonic;
1245 if(statement.size()>=2 &&
1246 statement[statement.size()-2]==
'_' &&
1247 isdigit(statement[statement.size()-1]))
1252 std::string(
id2string(statement), statement.size()-1, 1)),
1264 if(cur_pc==it->handler_pc)
1267 catch_type !=
typet() ||
1274 catch_type=it->catch_type;
1280 if(catch_type!=
typet())
1294 stack.push_back(catch_var);
1304 assert(results.size()==1);
1332 "java::org.cprover.CProver.assume:(Z)V")
1337 "function expected to have exactly one parameter");
1343 arg0.
get(ID_identifier) ==
"java::org.cprover.CProver.atomicBegin:()V")
1345 c =
codet(ID_atomic_begin);
1350 arg0.
get(ID_identifier) ==
"java::org.cprover.CProver.atomicEnd:()V")
1352 c =
codet(ID_atomic_end);
1359 expr_try_dynamic_cast<class_method_descriptor_exprt>(arg0);
1362 class_method_descriptor,
1363 "invokeinterface, invokespecial, invokevirtual and invokestatic should "
1364 "be called with a class method descriptor expression as arg0");
1367 i_it->source_location, statement, *class_method_descriptor, c, results);
1374 else if(bytecode ==
patternt(
"?return"))
1383 else if(bytecode ==
patternt(
"?astore"))
1388 else if(bytecode ==
patternt(
"?store") || bytecode ==
patternt(
"?store_?"))
1395 else if(bytecode ==
patternt(
"?aload"))
1403 results[0] =
convert_load(arg0, statement[0], i_it->address);
1411 "String and Class literals should have been lowered in "
1412 "generate_constant_global_variables");
1434 std::next(i_it)->address,
1438 else if(bytecode ==
BC_ret)
1444 assert(!jsr_ret_targets.empty());
1450 assert(results.size()==1);
1453 else if(bytecode ==
patternt(
"?const_?"))
1455 assert(results.size()==1);
1458 else if(bytecode ==
patternt(
"?ipush"))
1462 arg0.
id()==ID_constant,
1463 "ipush argument expected to be constant");
1466 else if(bytecode ==
patternt(
"if_?cmp??"))
1472 address_map, bytecode, op, number, i_it->source_location);
1474 else if(bytecode ==
patternt(
"if??"))
1478 bytecode ==
BC_ifeq ? ID_equal :
1479 bytecode ==
BC_ifne ? ID_notequal :
1487 INVARIANT(!
id.empty(),
"unexpected bytecode-if");
1491 c =
convert_if(address_map, op,
id, number, i_it->source_location);
1493 else if(bytecode ==
patternt(
"ifnonnull"))
1500 else if(bytecode ==
patternt(
"ifnull"))
1505 c =
convert_ifnull(address_map, op, number, i_it->source_location);
1511 else if(bytecode ==
patternt(
"?xor"))
1516 else if(bytecode ==
patternt(
"?or"))
1521 else if(bytecode ==
patternt(
"?and"))
1526 else if(bytecode ==
patternt(
"?shl"))
1531 else if(bytecode ==
patternt(
"?shr"))
1536 else if(bytecode ==
patternt(
"?ushr"))
1541 else if(bytecode ==
patternt(
"?add"))
1546 else if(bytecode ==
patternt(
"?sub"))
1551 else if(bytecode ==
patternt(
"?div"))
1556 else if(bytecode ==
patternt(
"?mul"))
1561 else if(bytecode ==
patternt(
"?neg"))
1566 else if(bytecode ==
patternt(
"?rem"))
1574 else if(bytecode ==
patternt(
"?cmp"))
1579 else if(bytecode ==
patternt(
"?cmp?"))
1584 else if(bytecode ==
patternt(
"?cmpl"))
1589 else if(bytecode ==
BC_dup)
1592 results[0]=results[1]=op[0];
1630 to_member(op[0], expr_dynamic_cast<fieldref_exprt>(arg0),
ns));
1635 const auto &field_name=arg0.
get_string(ID_component_name);
1636 const bool is_assertions_disabled_field=
1637 field_name.find(
"$assertionsDisabled")!=std::string::npos;
1647 i_it->source_location,
1650 is_assertions_disabled_field,
1662 const auto &field_name=arg0.
get_string(ID_component_name);
1688 exprt largest_as_dest =
1696 exprt largest_as_src =
1700 exprt smallest_as_dest =
1705 exprt smallest_as_src =
1716 else if(bytecode ==
patternt(
"?2?"))
1731 else if(bytecode ==
BC_new)
1735 convert_new(i_it->source_location, arg0, c, results);
1747 const std::size_t dimension =
1751 assert(results.size()==1);
1761 array.set(ID_java_member_access,
true);
1791 else if(bytecode ==
BC_nop)
1806 if(catch_instruction.has_value())
1813 if(!i_it->source_location.get_line().empty())
1818 instruction.done =
true;
1819 for(
const auto address : instruction.successors)
1821 address_mapt::iterator a_it2=address_map.find(address);
1827 if(address==exception_row.handler_pc)
1834 if(!
stack.empty() && a_it2->second.predecessors.size()>1)
1841 if(a_it2->second.stack.empty())
1843 for(stackt::iterator s_it=
stack.begin();
1857 a_it2->second.stack.size() ==
stack.size(),
1858 "Stack sizes should be the same.");
1859 stackt::const_iterator os_it=a_it2->second.stack.begin();
1860 for(
auto &expr :
stack)
1862 assert(
has_prefix(os_it->get_string(ID_C_base_name),
"$stack"));
1883 if(last_statement.get_statement()==ID_goto)
1886 if(last_statement.get_statement() != ID_block)
1890 last_statement.operands().begin(),
1898 a_it2->second.stack=
stack;
1908 new_symbol.
name=var.get_identifier();
1909 new_symbol.
type=var.type();
1910 new_symbol.
base_name=var.get(ID_C_base_name);
1912 new_symbol.
mode=ID_java;
1929 bool start_new_block=
true;
1930 bool has_seen_previous_address=
false;
1932 for(
const auto &address_pair : address_map)
1935 assert(address_pair.first==address_pair.second.source->address);
1936 const codet &c=address_pair.second.code;
1939 if(!start_new_block)
1940 start_new_block=targets.find(address)!=targets.end();
1943 if(!start_new_block)
1944 start_new_block=address_pair.second.predecessors.size()>1;
1949 if(!start_new_block && has_seen_previous_address)
1952 if(exception_row.start_pc==previous_address)
1954 start_new_block=
true;
1966 "Block addresses should be unique and increasing");
1974 add_to_block.add(c);
1976 start_new_block=address_pair.second.successors.size()>1;
1978 previous_address=address;
1979 has_seen_previous_address=
true;
1983 std::map<irep_idt, variablet> temporary_variable_live_ranges;
1984 for(
const auto &aentry : address_map)
1988 temporary_variable_live_ranges);
1990 std::vector<const variablet*> vars_to_process;
1992 for(
const auto &v : vlist)
1993 vars_to_process.push_back(&v);
1996 vars_to_process.push_back(
1997 &temporary_variable_live_ranges.at(v.get_identifier()));
2000 vars_to_process.push_back(
2001 &temporary_variable_live_ranges.at(v.get_identifier()));
2003 for(
const auto vp : vars_to_process)
2017 v.start_pc + v.length,
2018 std::numeric_limits<method_offsett>::max(),
2021 for(
const auto vp : vars_to_process)
2027 if(v.symbol_expr.get_identifier().empty())
2033 v.start_pc + v.length,
2034 std::numeric_limits<method_offsett>::max());
2036 block.statements().insert(block.statements().begin(), d);
2070 bool is_label =
true;
2071 for(
auto a_it = args.begin(); a_it != args.end();
2072 a_it++, is_label = !is_label)
2083 numeric_cast_v<method_offsett>(number);
2087 if(a_it == args.begin())
2092 code_block.
add(std::move(code_case), location);
2101 code_block.
add(std::move(code_case), location);
2106 code_switcht code_switch(op[0], std::move(code_block));
2116 const irep_idt descriptor = (statement ==
"monitorenter") ?
2117 "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" :
2118 "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V";
2131 return std::move(call);
2143 results.insert(results.end(), op.begin(), op.end());
2144 results.insert(results.end(), op.begin(), op.end());
2156 results.insert(results.end(), op.begin() + 1, op.end());
2157 results.insert(results.end(), op.begin(), op.end());
2176 results.insert(results.end(), op.begin(), op.end());
2177 results.insert(results.end(), op2.begin(), op2.end());
2178 results.insert(results.end(), op.begin(), op.end());
2186 const char type_char = statement[0];
2187 const bool is_double(
'd' == type_char);
2188 const bool is_float(
'f' == type_char);
2190 if(is_double || is_float)
2197 if(arg0.
type().
id() != ID_floatbv)
2199 const mp_integer number = numeric_cast_v<mp_integer>(arg0);
2209 const mp_integer value = numeric_cast_v<mp_integer>(arg0);
2225 parameters.size() == arguments.size(),
2226 "for each parameter there must be exactly one argument");
2227 for(std::size_t i = 0; i < parameters.size(); i++)
2229 const typet &type = parameters[i].type();
2233 type.
id() == ID_pointer)
2247 const bool use_this(statement !=
"invokestatic");
2248 const bool is_virtual(
2249 statement ==
"invokevirtual" || statement ==
"invokeinterface");
2253 !invoked_method_id.
empty(),
2254 "invoke statement arg0 must have an identifier");
2269 "Function return type must not change in kind");
2270 class_method_descriptor.
type() = method_symbol->second.type;
2284 if(parameters.empty() || !parameters[0].get_this())
2291 parameters.insert(parameters.begin(), this_p);
2296 if(statement ==
"invokespecial")
2305 method_type.
set(ID_java_super_method_call,
true);
2315 !use_this || arguments.front().type().id() == ID_pointer,
2316 "first argument must be a pointer");
2324 if(return_type.
id() != ID_empty)
2330 results[0] = promoted;
2348 class_method_descriptor.
class_id(),
2357 class_method_descriptor.
class_id(),
2368 function = class_method_descriptor;
2375 function =
symbol_exprt(invoked_method_id, method_type);
2385 std::move(lhs), std::move(
function), std::move(arguments));
2428 c = std::move(assert_class);
2441 "java::java.lang.AssertionError") &&
2450 assert_location.set(
"user-provided",
true);
2451 assert_location.set_property_class(ID_assertion);
2452 assert_code.add_source_location() = assert_location;
2456 assume_location.
set(
"user-provided",
true);
2457 assume_code.add_source_location() = assume_location;
2472 const std::set<method_offsett> &working_set,
2481 typedef std::vector<std::reference_wrapper<
2483 std::map<std::size_t, exceptionst> exceptions_by_end;
2488 exceptions_by_end[exception.
end_pc].push_back(exception);
2490 for(
const auto &exceptions : exceptions_by_end)
2498 : exceptions.second)
2500 exception_list.emplace_back(
2507 code =
code_blockt({ std::move(catch_push), code });
2527 auto next_opcode_it = std::find_if(
2528 working_set.begin(),
2531 if(next_opcode_it != working_set.end())
2534 std::set<std::size_t> start_positions;
2538 if(*next_opcode_it == exception_row.end_pc)
2539 start_positions.insert(exception_row.start_pc);
2541 for(std::size_t handler = 0; handler < start_positions.size(); ++handler)
2568 create.
add(assume_le_max_size);
2586 if(statement ==
"newarray")
2593 else if(
id == ID_char)
2595 else if(
id == ID_float)
2597 else if(
id == ID_double)
2599 else if(
id == ID_byte)
2601 else if(
id == ID_short)
2603 else if(
id == ID_int)
2605 else if(
id == ID_long)
2627 block.
add(std::move(assume_le_max_size));
2680 block.
add(clinit_call);
2683 "stack_static_field",
2706 const bool is_assertions_disabled_field,
2712 if(arg0.
type().
id() == ID_struct_tag)
2717 else if(arg0.
type().
id() == ID_pointer)
2726 else if(is_assertions_disabled_field)
2741 else if(is_assertions_disabled_field)
2753 const int nan_value(statement[4] ==
'l' ? -1 : 1);
2848 const exprt arg1_int_type =
2856 block.
add(std::move(code_assign));
2870 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2877 address_map.at(label_number).source->source_location;
2892 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2899 address_map.at(label_number).source->source_location;
2912 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2921 address_map.at(label_number).source->source_location;
2941 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2947 address_map.at(label_number).source->source_location;
2954 const std::vector<method_offsett> &jsr_ret_targets,
2960 auto retvar =
variable(arg0,
'a', address);
2961 for(
size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2966 if(idx == idxlim - 1)
2976 branch.cond().add_source_location() = location;
2977 branch.add_source_location() = location;
2992 const auto ref_type =
2993 type_try_dynamic_cast<java_reference_typet>(expr.
type());
2994 const bool typecast_not_needed =
2995 ref_type && ((type_char ==
'b' && ref_type->subtype().get_identifier() ==
2996 "java::array[boolean]") ||
2998 return typecast_not_needed ? expr
3007 const char type_char = statement[0];
3010 deref.
set(ID_java_member_access,
true);
3012 auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
3016 plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
3018 data_plus_offset.
set(ID_java_array_access,
true);
3028 if(type_char ==
'i')
3032 type_try_dynamic_cast<bitvector_typet>(var.
type())->get_width() <= 32,
3033 "iload can be used for boolean, byte, short, int and char");
3039 "Variable type must match [adflv]load return type");
3074 const char type_char = statement[0];
3077 deref.
set(ID_java_member_access,
true);
3079 auto java_array_type = type_try_dynamic_cast<struct_tag_typet>(deref.type());
3083 plus_exprt data_plus_offset{std::move(data_ptr), op[1]};
3085 data_plus_offset.
set(ID_java_array_access,
true);
3094 block.
add(std::move(array_put), location);
3100 std::size_t instruction_address,
3120 if(!value.has_value())
3147 arguments.insert(arguments.begin(), new_instance);
3154 result.
add(constructor_call);
3161 result_code = std::move(result);
3163 if(return_type.
id() == ID_empty)
3166 return new_instance;
3171 const std::vector<method_offsett> &jsr_ret_targets,
3173 std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
3174 &ret_instructions)
const
3177 for(
const auto &retinst : ret_instructions)
3179 auto &a_entry = address_map.at(retinst->address);
3180 a_entry.successors.insert(
3181 a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
3185 std::vector<java_bytecode_convert_methodt::method_offsett>
3191 std::vector<method_offsett> result;
3192 for(
const auto &exception_row : exception_table)
3194 if(address >= exception_row.start_pc && address < exception_row.end_pc)
3195 result.push_back(exception_row.handler_pc);
3215 &local_variable_table,
3227 typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3228 std::map<std::size_t, base_name_and_identifiert> param_names;
3229 for(
const auto &v : local_variable_table)
3231 if(v.index < slots_for_parameters)
3232 param_names.emplace(
3239 std::size_t param_index = 0;
3240 for(
auto ¶m : parameters)
3249 if(param_index == 0 && param.get_this())
3252 base_name = ID_this;
3257 auto param_name = param_names.find(param_index);
3258 if(param_name != param_names.end())
3260 base_name = param_name->second.first;
3261 identifier = param_name->second.second;
3268 const typet &type = param.type();
3275 param.set_base_name(base_name);
3276 param.set_identifier(identifier);
3281 parameter_symbol.
mode = ID_java;
3282 parameter_symbol.
name = identifier;
3283 parameter_symbol.
type = param.type();
3284 symbol_table.
insert(parameter_symbol);
3295 size_t max_array_length,
3296 bool throw_assertion_error,
3300 bool threading_support,
3302 bool assert_no_exceptions_thrown)
3309 throw_assertion_error,
3310 needed_lazy_methods,
3314 assert_no_exceptions_thrown);
3326 const irep_idt &mangled_method_name)
const
3331 return inherited_method.has_value();
3341 const irep_idt &component_name)
const
3347 inherited_method.has_value(),
"static field should be in symbol table");
3349 return inherited_method->get_full_component_identifier();
3359 const std::string &tmp_var_prefix,
3364 const std::function<bool(
3365 const std::function<
tvt(
const exprt &expr)>,
const exprt &expr)>
3366 entry_matches = [&entry_matches](
3367 const std::function<
tvt(
const exprt &expr)> predicate,
3368 const exprt &expr) {
3369 const tvt &tvres = predicate(expr);
3375 [&predicate, &entry_matches](
const exprt &expr) {
3376 return entry_matches(predicate, expr);
3388 const std::function<
tvt(
const exprt &expr)> has_member_entry = [&identifier](
3389 const exprt &expr) {
3390 const auto member_expr = expr_try_dynamic_cast<member_exprt>(expr);
3392 :
tvt(member_expr->get_component_name() == identifier);
3398 const std::function<
tvt(
const exprt &expr)> is_symbol_entry =
3399 [&identifier](
const exprt &expr) {
3400 const auto symbol_expr = expr_try_dynamic_cast<symbol_exprt>(expr);
3402 :
tvt(symbol_expr->get_identifier() == identifier);
3408 const std::function<
tvt(
const exprt &expr)> is_dereference_entry =
3409 [](
const exprt &expr) {
3410 const auto dereference_expr =
3411 expr_try_dynamic_cast<dereference_exprt>(expr);
3415 for(
auto &stack_entry :
stack)
3422 replace = entry_matches(is_symbol_entry, stack_entry);
3425 replace = entry_matches(is_dereference_entry, stack_entry);
3428 replace = entry_matches(has_member_entry, stack_entry);
3434 tmp_var_prefix, stack_entry.type(), block, stack_entry);
3441 const std::string &tmp_var_prefix,
3442 const typet &tmp_var_type,
3446 const exprt tmp_var=
3449 stack_entry=tmp_var;