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;
1555 symbol_expr.set_identifier(
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);
1575 symbol_expr.set_identifier(
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")
1622 PRECONDITION(pointer.type().subtype().id() == ID_struct_tag);
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;
2418 java_new_array.operands() = op;
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);
2503 java_new_expr.add_source_location() = location;
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);
2717 code_branch.then_case().add_source_location() =
2718 address_map.at(label_number).source->source_location;
2719 code_branch.add_source_location() = location;
2733 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2739 code_branch.then_case().add_source_location() =
2740 address_map.at(label_number).source->source_location;
2741 code_branch.add_source_location() = location;
2753 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2759 code_branch.cond().add_source_location() = location;
2761 code_branch.then_case().add_source_location() =
2762 address_map.at(label_number).source->source_location;
2763 code_branch.then_case().add_source_location().set_function(
method_id);
2764 code_branch.add_source_location() = location;
2782 const method_offsett label_number = numeric_cast_v<method_offsett>(number);
2787 code_branch.then_case().add_source_location() =
2788 address_map.at(label_number).source->source_location;
2789 code_branch.add_source_location() = 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) {
3183 :
tvt(member_expr->get_component_name() == identifier);
3189 const std::function<tvt(const exprt &expr)> is_symbol_entry =
3190 [&identifier](
const 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 =
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;
The void type, the same as empty_typet.
code_blockt convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
const irep_idt & get_statement() const
The type of an expression, extends irept.
irep_idt name
The unique identifier.
codet convert_pop(const irep_idt &statement, const exprt::operandst &op)
Fixed-width bit-vector with unsigned binary interpretation.
void set_function(const irep_idt &function)
void set_access(const irep_idt &access)
std::vector< exception_list_entryt > exception_listt
Semantic type conversion.
static bool is_constructor(const irep_idt &method_name)
void pop_residue(std::size_t n)
removes minimum(n, stack.size()) elements from the stack
JAVA Bytecode Language Conversion.
codet representing a switch statement.
A base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
void convert(const symbolt &class_symbol, const methodt &)
std::vector< parametert > parameterst
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
pointer_typet pointer_type(const typet &subtype)
dereference_exprt checked_dereference(const exprt &expr, const typet &type)
Dereference an expression and flag it for a null-pointer check.
Remove function exceptional returns.
static void gather_symbol_live_ranges(java_bytecode_convert_methodt::method_offsett pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
void convert_athrow(const source_locationt &location, const exprt::operandst &op, codet &c, exprt::operandst &results) const
Over-approximative uncaught exceptions analysis.
Symbol table entry of function parameterThis is a symbol generated as part of type checking...
const mp_integer string2integer(const std::string &n, unsigned base)
const std::string integer2string(const mp_integer &n, unsigned base)
void set_is_final(bool is_final)
exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns an expression indicating a local variable suitable to load/store from a bytecode at address a...
optionalt< std::string > signature
typet java_boolean_type()
irep_idt method_id
Fully qualified name of the method under translation.
void set_property_class(const irep_idt &property_class)
static bool operator==(const irep_idt &what, const patternt &pattern)
constant_exprt to_expr() const
codet & find_last_statement()
Non-graph-based representation of the class hierarchy.
optionalt< symbolt > get_lambda_method_symbol(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const size_t index)
Retrieves the symbol of the lambda method associated with the given lambda method handle (bootstrap m...
methodt::instructionst instructionst
const java_lambda_method_handlest & lambda_method_handles() const
code_ifthenelset convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
irep_idt mode
Language mode.
code_blockt convert_ret(const std::vector< method_offsett > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const method_offsett address)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void from_expr(const constant_exprt &expr)
bool is_method_inherited(const irep_idt &classname, const irep_idt &methodid) const
Returns true iff method methodid from class classname is a method inherited from a class (and not an ...
optionalt< ci_lazy_methods_neededt > needed_lazy_methods
reference_typet java_reference_type(const typet &subtype)
void set_comment(const irep_idt &comment)
const bool threading_support
signed int get_int(const irep_namet &name) const
static irep_idt label(const irep_idt &address)
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
const irep_idt & get_identifier() const
bool is_valid() const
Use to check if this inherited_componentt has been fully constructed.
code_operandst & statements()
std::string as_string() const
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
struct bytecode_infot const bytecode_info[]
The null pointer constant.
exprt value
Initial value of symbol.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
void setup_local_variables(const methodt &m, const address_mapt &amap)
See find_initializers_for_slot above for more detail.
The trinary if-then-else operator.
A struct tag type, i.e., struct_typet with an identifier.
irep_idt module
Name of module the symbol belongs to.
code_blockt convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, method_offsett address)
codet representation of a goto statement.
irep_idt pretty_name
Language-specific display name.
typet & type()
Return the type of the expression.
An exception that is raised for unsupported class signature.
Pops an exception handler from the stack of active handlers (i.e.
bool operator==(const irep_idt &what) const
A constant literal expression.
#define CHECK_RETURN(CONDITION)
void convert_new(const source_locationt &location, const exprt &arg0, codet &c, exprt::operandst &results)
bool get_is_constructor() const
bool is_parameter(const local_variablet &v)
Returns true iff the slot index of the local variable of a method (coming from the LVT) is a paramete...
reference_typet java_array_type(const char subtype)
Construct an array pointer type.
codet representation of an expression statement.
expanding_vectort< variablest > variables
A side_effect_exprt representation of a side effect that throws an exception.
code_ifthenelset convert_if_cmp(const java_bytecode_convert_methodt::address_mapt &address_map, const irep_idt &statement, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
irept::subt java_lambda_method_handlest
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const exprt & case_op() const
const class_hierarchyt & class_hierarchy
java_method_typet member_type_lazy(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name, const std::string &method_name, message_handlert &message_handler)
Returns the member type for a method, based on signature or descriptor.
code_blockt convert_instructions(const methodt &, const java_class_typet::java_lambda_method_handlest &)
void set_base_name(const irep_idt &name)
static ieee_float_spect double_precision()
Extract member of struct or union.
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
mstreamt & warning() const
irep_idt current_method
A copy of method_id :/.
void set_is_constructor()
Expression Initialization.
const irep_idt & id() const
Evaluates to true if the operand is NaN.
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
void set_native(bool is_native)
typet java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof...
void add(const codet &code)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
class code_blockt & make_block()
If this codet is a code_blockt (i.e. it represents a block of statements), return the unmodified inpu...
code_blockt convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, exprt::operandst &results)
void add_throws_exceptions(irep_idt exception)
static irep_idt get_if_cmp_operator(const irep_idt &stmt)
source_locationt source_location
Given a string of the format '?blah?', will return true when compared against a string that matches a...
std::vector< exceptiont > exception_tablet
const irep_idt & get_line() const
A codet representing the declaration of a local variable.
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const symbol_tablet &symbol_table, const class_hierarchyt &class_hierarchy, bool include_interfaces)
Finds an inherited component (method or field), taking component visibility into account.
exprt::operandst & convert_cmp2(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
Strip java:: prefix from given identifier.
std::vector< exprt > argst
source_locationt source_location
codet replace_character_call(code_function_callt call)
Operator to dereference a pointer.
static std::size_t get_bytecode_type_width(const typet &ty)
typet java_type_from_char(char t)
Constructs a type indicated by the given character:
nonstd::optional< T > optionalt
const code_gotot & to_code_goto(const codet &code)
exprt::operandst & convert_cmp(const exprt::operandst &op, exprt::operandst &results) const
API to expression classes.
exprt::operandst & convert_const(const irep_idt &statement, const exprt &arg0, exprt::operandst &results) const
irep_idt get_static_field(const irep_idt &class_identifier, const irep_idt &component_name) const
Get static field identifier referred to by class_identifier.component_name Note this may be inherited...
const irep_idt & get(const irep_namet &name) const
static irep_idt get_exception_type(const typet &type)
Returns the compile type of an exception.
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static ieee_float_spect single_precision()
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address)
'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
void java_bytecode_convert_method(const symbolt &class_symbol, const java_bytecode_parse_treet::methodt &method, symbol_table_baset &symbol_table, message_handlert &message_handler, size_t max_array_length, bool throw_assertion_error, optionalt< ci_lazy_methods_neededt > needed_lazy_methods, java_string_library_preprocesst &string_preprocess, const class_hierarchyt &class_hierarchy, bool threading_support)
codet representation of a label for branch targets.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
#define PRECONDITION(CONDITION)
Given a class and a component (either field or method), find the closest parent that defines that com...
std::string pretty_signature(const java_method_typet &method_type)
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Base class for tree-like data structures with sharing.
codet representation of a function call statement.
#define forall_operands(it, expr)
The plus expression Associativity is not specified.
code_blockt convert_putfield(const exprt &arg0, const exprt::operandst &op)
const std::unordered_set< std::string > cprover_methods_to_ignore
Methods belonging to the class org.cprover.CProver that should be ignored (not converted), leaving the driver program to stub them if it wishes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
std::vector< method_offsett > branch_addresses
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
code_ifthenelset convert_if(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const irep_idt &id, const mp_integer &number, const source_locationt &location) const
unsigned java_local_variable_slots(const typet &t)
Returns the number of JVM local variables (slots) taken by a local variable that, when translated to ...
Class that provides messages with a built-in verbosity 'level'.
const size_t max_array_length
code_ifthenelset convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
java_string_library_preprocesst & string_preprocess
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, method_offsett address_start, method_offsett address_limit, method_offsett next_block_start_address, const address_mapt &amap, bool allow_merge=true)
As above, but this version can additionally create a new branch in the block_tree-node and code_block...
codet get_clinit_call(const irep_idt &classname)
Each static access to classname should be prefixed with a check for necessary static init; this retur...
The unary minus expression.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
void convert_checkcast(const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results) const
typet method_return_type
Return type of the method under conversion.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
The Boolean constant false.
std::list< symbol_exprt > tmp_vars
const codet & body() const
typet java_type_from_string_with_exception(const std::string &descriptor, const optionalt< std::string > &signature, const std::string &class_name)
exprt::operandst pop(std::size_t n)
void java_bytecode_convert_method_lazy(const symbolt &class_symbol, const irep_idt &method_identifier, const java_bytecode_parse_treet::methodt &m, symbol_tablet &symbol_table, message_handlert &message_handler)
This creates a method symbol in the symtab, but doesn't actually perform method conversion just yet...
std::set< symbol_exprt > used_local_names
const bool throw_assertion_error
static exprt conditional_cast(const exprt &expr, const typet &type)
std::vector< exprt > operandst
Binary multiplication Associativity is not specified.
std::vector< block_tree_nodet > branch
A non-fatal assertion, which checks a condition then permits execution to continue.
An assumption, which must hold in subsequent code.
const exprt & value() const
code_switcht convert_switch(const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
method_offsett slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< method_offsett > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
code_blockt convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
code_blockt convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
const java_method_typet & to_java_method_type(const typet &type)
std::vector< variablet > variablest
const bytecode_infot & get_bytecode_info(const irep_idt &statement)
void create_stack_tmp_var(const std::string &, const typet &, code_blockt &, exprt &)
actually create a temporary variable to hold the value of a stack entry
void set_is_varargs(bool is_varargs)
codet convert_monitorenterexit(const irep_idt &statement, const exprt::operandst &op, const source_locationt &source_location)
mstreamt & result() const
void convert_dup2_x1(exprt::operandst &op, exprt::operandst &results)
symbol_exprt tmp_variable(const std::string &prefix, const typet &type)
void merge_source_location_rec(exprt &expr, const source_locationt &source_location)
Attaches a source location to an expression and all of its subexpressions.
void convert_getstatic(const exprt &arg0, const symbol_exprt &symbol_expr, bool is_assertions_disabled_field, codet &c, exprt::operandst &results)
instructionst instructions
Base class for all expressions.
void convert_annotations(const java_bytecode_parse_treet::annotationst &parsed_annotations, std::vector< java_annotationt > &java_annotations)
Convert parsed annotations into the symbol table.
const parameterst & parameters() const
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
const variablet & find_variable_for_slot(size_t address, variablest &var_list)
See above.
const exprt & assumption() const
const source_locationt & source_location() const
std::vector< local_variablet > local_variable_tablet
exception_tablet exception_table
unsigned java_method_parameter_slots(const java_method_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call...
irept & add(const irep_namet &name)
const std::string & get_string(const irep_namet &name) const
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
codet & replace_call_to_cprover_assume(source_locationt location, codet &c)
void from_integer(const mp_integer &i)
void push(const exprt::operandst &o)
source_locationt & add_source_location()
A codet representing sequential composition of program statements.
const codet & to_code(const exprt &expr)
codet & do_exception_handling(const methodt &method, const std::set< method_offsett > &working_set, method_offsett cur_pc, codet &c)
A codet representing a skip statement.
symbol_table_baset & symbol_table
codet representation of an if-then-else statement.
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
void convert_dup2_x2(exprt::operandst &op, exprt::operandst &results)
void convert_dup2(exprt::operandst &op, exprt::operandst &results)
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
codet representation of a switch-case, i.e. a case statement within a switch.
code_blockt convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const method_offsett address, const source_locationt &location)
Data structure for representing an arbitrary statement in a program.
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
codet representation of a "return from a function" statement.
std::map< method_offsett, converted_instructiont > address_mapt
const code_labelt & to_code_label(const codet &code)
JAVA Bytecode Language Conversion.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
An expression containing a side effect.
local_variable_tablet local_variable_table
Compute dominators for CFG of goto_function.
void java_bytecode_initialize_parameter_names(symbolt &method_symbol, const java_bytecode_parse_treet::methodt::local_variable_tablet &local_variable_table, symbol_table_baset &symbol_table)
This uses a cut-down version of the logic in java_bytecode_convert_methodt::convert to initialize sym...
std::vector< method_offsett > try_catch_handler(method_offsett address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
void push_back(const T &t)
static void replace_goto_target(codet &repl, const irep_idt &old_label, const irep_idt &new_label)
Find all goto statements in 'repl' that target 'old_label' and redirect them to 'new_label'.
std::size_t get_size_t(const irep_namet &name) const
exception_listt & exception_list()
optionalt< exprt > convert_invoke_dynamic(const java_class_typet::java_lambda_method_handlest &lambda_method_handles, const source_locationt &location, const exprt &arg0)
irep_idt clinit_wrapper_name(const irep_idt &class_name)
Get the Java static initializer wrapper name for a given class (the wrapper checks if static initiali...
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
const irept & find(const irep_namet &name) const
static member_exprt to_member(const exprt &pointer, const exprt &fieldref)
irep_idt get_full_component_identifier() const
Get the full name of this function.
const typet & return_type() const
const java_class_typet & to_java_class_type(const typet &type)
A codet representing an assignment in the program.
char java_char_from_type(const typet &type)
void set(const irep_namet &name, const irep_idt &value)
exprt convert_aload(const irep_idt &statement, const exprt::operandst &op) const
static void assign_parameter_names(java_method_typet &ftype, const irep_idt &name_prefix, symbol_table_baset &symbol_table)
Iterates through the parameters of the function type ftype, finds a new new name for each parameter a...
void save_stack_entries(const std::string &, code_blockt &, const bytecode_write_typet, const irep_idt &)
Create temporary variables if a write instruction can have undesired side- effects.
A statement that catches an exception, assigning the exception in flight to an expression (e...
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
void branch(goto_modelt &goto_model, const irep_idt &id)
const exprt & assertion() const
Produce code for simple implementation of String Java libraries.
static block_tree_nodet get_leaf()
IEEE-floating-point equality.
std::vector< irep_idt > throws_exception_table