47 #include <unordered_set> 63 for(std::size_t i=0; i<what.
size(); i++)
66 else if(
p[i]!=
'?' &&
p[i]!=what[i])
69 return p[what.
size()]==0;
97 for(std::size_t i=0; i<parameters.size(); ++i)
101 if(i==0 && parameters[i].get_this())
107 parameters[i].set_base_name(base_name);
108 parameters[i].set_identifier(identifier);
113 parameter_symbol.
mode=ID_java;
114 parameter_symbol.
name=identifier;
115 parameter_symbol.
type=parameters[i].type();
116 symbol_table.
add(parameter_symbol);
122 return pattern==what;
127 return id2string(method_name).find(
"<init>") != std::string::npos;
134 error() <<
"malformed bytecode (pop too high)" <<
eom;
140 for(std::size_t i=0; i<n; i++)
150 std::size_t residue_size=std::min(n,
stack.size());
159 for(std::size_t i=0; i<o.size(); i++)
170 const std::string &prefix,
179 tmp_symbol.
mode=ID_java;
180 tmp_symbol.
name=identifier;
181 tmp_symbol.
type=type;
185 result.set(ID_C_base_name, base_name);
231 result.set(ID_C_base_name, base_name);
258 const std::string &descriptor,
260 const std::string &class_name,
261 const std::string &method_name,
275 INVARIANT(member_type_from_descriptor.
id()==ID_code,
"Must be code type");
276 if(signature.has_value())
283 INVARIANT(member_type_from_signature.
id()==ID_code,
"Must be code type");
291 message.
warning() <<
"Method: " << class_name <<
"." << method_name
292 <<
"\n signature: " << signature.value()
293 <<
"\n descriptor: " << descriptor
294 <<
"\n different number of parameters, reverting to " 301 message.
warning() <<
"Method: " << class_name <<
"." << method_name
302 <<
"\n could not parse signature: " << signature.value()
303 <<
"\n " << e.what() <<
"\n" 304 <<
" reverting to descriptor: " << descriptor
321 const symbol_exprt &lambda_method_handle = lambda_method_handles.at(index);
354 method_symbol.
name=method_identifier;
356 method_symbol.
mode=ID_java;
376 this_p.
type()=object_ref_type;
378 parameters.insert(parameters.begin(), this_p);
404 type_checked_cast<annotated_typet>(static_cast<typet &>(member_type))
408 method_symbol.
type=member_type;
416 method_symbol.
type.
set(ID_C_must_not_throw,
true);
419 symbol_table.
add(method_symbol);
439 code_type.
set(ID_C_class, class_symbol.
name);
447 debug() <<
"Generating codet: class " 448 << class_symbol.
name <<
", method " 465 if(v.signature.has_value())
475 std::ostringstream id_oss;
479 result.set(ID_C_base_name, v.name);
488 newv.start_pc=v.start_pc;
489 newv.length=v.length;
496 std::size_t param_index=0;
497 for(
const auto ¶m : parameters)
504 "java_parameter_count and local computation must agree");
508 for(
auto ¶m : parameters)
517 if(param_index==0 && param.get_this())
526 base_name=
variables[param_index][0].symbol_expr.get(ID_C_base_name);
527 identifier=
variables[param_index][0].symbol_expr.get(ID_identifier);
530 if(base_name.
empty())
535 const typet &type=param.type();
541 param.set_base_name(base_name);
542 param.set_identifier(identifier);
547 parameter_symbol.
mode=ID_java;
548 parameter_symbol.
name=identifier;
549 parameter_symbol.
type=param.type();
554 variables[param_index][0].is_parameter=
true;
556 variables[param_index][0].length=std::numeric_limits<size_t>::max();
564 "java_parameter_count and local computation must agree");
568 method_symbol.
name == method_identifier,
569 "Name of method symbol shouldn't change");
572 "Base name of method symbol shouldn't change");
575 "Method symbol shouldn't have module");
577 method_symbol.
mode=ID_java;
596 "Member type should have already been marked as a constructor");
604 method_symbol.
type = code_type;
620 if(statement==p->mnemonic)
623 error() <<
"failed to find bytecode mnemonic `" 624 << statement <<
'\'' <<
eom;
643 throw "unhandled java comparison instruction";
656 fieldref.
get(ID_component_name),
677 if(g.get_destination()==old_label)
678 g.set_destination(new_label);
705 unsigned address_start,
706 unsigned address_limit,
707 unsigned next_block_start_address)
715 next_block_start_address,
737 unsigned address_start,
738 unsigned address_limit,
739 unsigned next_block_start_address,
749 assert(!tree.
branch.empty());
752 const auto afterstart=
758 auto findstart=afterstart;
769 unsigned findlim_block_start_address=
771 next_block_start_address :
780 auto child_iter=this_block.
operands().begin();
783 while(child_iter!=this_block.
operands().end() &&
786 assert(child_iter!=this_block.
operands().end());
787 std::advance(child_iter, child_offset);
788 assert(child_iter!=this_block.
operands().end());
792 bool single_child(afterstart==findlim);
797 tree.
branch[child_offset],
801 findlim_block_start_address,
819 auto checkit=amap.
find(*findstart);
820 assert(checkit!=amap.end());
823 checkit!=amap.end() && (checkit->first)<(findlim_block_start_address);
826 for(
auto p : checkit->second.predecessors)
828 if(p<(*findstart) || p>=findlim_block_start_address)
830 debug() <<
"Generating codet: " 831 <<
"warning: refusing to create lexical block spanning " 832 << (*findstart) <<
"-" << findlim_block_start_address
833 <<
" due to incoming edge " << p <<
" -> " 834 << checkit->first <<
eom;
844 const irep_idt child_label_name=child_label.get_label();
845 std::string new_label_str =
id2string(child_label_name);
847 irep_idt new_label_irep(new_label_str);
851 auto nblocks=std::distance(findstart, findlim);
853 debug() <<
"Generating codet: combining " 854 << std::distance(findstart, findlim)
855 <<
" blocks for addresses " << (*findstart) <<
"-" 856 << findlim_block_start_address <<
eom;
859 auto &this_block_children=this_block.
operands();
860 assert(tree.
branch.size()==this_block_children.size());
861 for(
auto blockidx=child_offset, blocklim=child_offset+nblocks;
872 auto delfirst=this_block_children.begin();
873 std::advance(delfirst, child_offset+1);
874 auto dellim=delfirst;
875 std::advance(dellim, nblocks-1);
876 this_block_children.erase(delfirst, dellim);
877 this_block_children[child_offset].swap(newlabel);
881 auto branchstart=tree.
branch.begin();
882 std::advance(branchstart, child_offset);
883 auto branchlim=branchstart;
884 std::advance(branchlim, nblocks);
885 for(
auto branchiter=branchstart; branchiter!=branchlim; ++branchiter)
886 newnode.
branch.push_back(std::move(*branchiter));
888 tree.
branch.erase(branchstart, branchlim);
890 assert(tree.
branch.size()==this_block_children.size());
893 std::advance(branchaddriter, child_offset);
894 auto branchaddrlim=branchaddriter;
895 std::advance(branchaddrlim, nblocks);
904 tree.
branch[child_offset]=std::move(newnode);
911 to_code(this_block_children[child_offset])).code());
917 std::map<irep_idt, java_bytecode_convert_methodt::variablet> &result)
919 if(e.
id()==ID_symbol)
922 auto findit = result.insert(
924 auto &var=findit.first->second;
927 var.symbol_expr=symexpr;
935 var.length+=(var.start_pc-pc);
940 var.length=std::max(var.length, (pc-var.start_pc)+1);
965 ret.
function() = findit->second.symbol_expr();
974 if(ty.
id()==ID_pointer)
995 std::set<unsigned> targets;
997 std::vector<unsigned> jsr_ret_targets;
998 std::vector<instructionst::const_iterator> ret_instructions;
1000 for(
auto i_it = instructions.begin(); i_it != instructions.end(); i_it++)
1003 std::pair<address_mapt::iterator, bool> a_entry=
1004 address_map.insert(std::make_pair(i_it->address, ins));
1005 assert(a_entry.second);
1008 assert(a_entry.first==--address_map.end());
1010 if(i_it->statement!=
"goto" &&
1011 i_it->statement!=
"return" &&
1012 !(i_it->statement==
patternt(
"?return")) &&
1013 i_it->statement!=
"athrow" &&
1014 i_it->statement!=
"jsr" &&
1015 i_it->statement!=
"jsr_w" &&
1016 i_it->statement!=
"ret")
1018 instructionst::const_iterator next=i_it;
1019 if(++next!=instructions.end())
1020 a_entry.first->second.successors.push_back(next->address);
1023 if(i_it->statement==
"athrow" ||
1024 i_it->statement==
"putfield" ||
1025 i_it->statement==
"getfield" ||
1026 i_it->statement==
"checkcast" ||
1027 i_it->statement==
"newarray" ||
1028 i_it->statement==
"anewarray" ||
1029 i_it->statement==
"idiv" ||
1030 i_it->statement==
"ldiv" ||
1031 i_it->statement==
"irem" ||
1032 i_it->statement==
"lrem" ||
1033 i_it->statement==
patternt(
"?astore") ||
1034 i_it->statement==
patternt(
"?aload") ||
1035 i_it->statement==
"invokestatic" ||
1036 i_it->statement==
"invokevirtual" ||
1037 i_it->statement==
"invokespecial" ||
1038 i_it->statement==
"invokeinterface")
1040 const std::vector<unsigned int> handler =
1042 std::list<unsigned int> &successors = a_entry.first->second.successors;
1043 successors.insert(successors.end(), handler.begin(), handler.end());
1044 targets.insert(handler.begin(), handler.end());
1047 if(i_it->statement==
"goto" ||
1048 i_it->statement==
patternt(
"if_?cmp??") ||
1049 i_it->statement==
patternt(
"if??") ||
1050 i_it->statement==
"ifnonnull" ||
1051 i_it->statement==
"ifnull" ||
1052 i_it->statement==
"jsr" ||
1053 i_it->statement==
"jsr_w")
1060 targets.insert(target);
1062 a_entry.first->second.successors.push_back(target);
1064 if(i_it->statement==
"jsr" ||
1065 i_it->statement==
"jsr_w")
1067 auto next = std::next(i_it);
1069 next != instructions.end(),
"jsr should have valid return address");
1070 targets.insert(next->address);
1071 jsr_ret_targets.push_back(next->address);
1074 else if(i_it->statement==
"tableswitch" ||
1075 i_it->statement==
"lookupswitch")
1078 for(
const auto &arg : i_it->args)
1085 targets.insert(target);
1086 a_entry.first->second.successors.push_back(target);
1091 else if(i_it->statement==
"ret")
1094 ret_instructions.push_back(i_it);
1099 for(
const auto &address : address_map)
1101 for(
unsigned s : address.second.successors)
1103 const auto a_it = address_map.find(s);
1105 a_it->second.predecessors.insert(address.first);
1119 std::set<unsigned> working_set;
1121 if(!instructions.empty())
1122 working_set.insert(instructions.front().address);
1124 while(!working_set.empty())
1126 auto cur = working_set.begin();
1127 auto address_it = address_map.find(*cur);
1129 auto &instruction = address_it->second;
1130 unsigned cur_pc=*cur;
1131 working_set.erase(cur);
1133 if(instruction.done)
1136 instruction.successors.begin(), instruction.successors.end());
1138 instructionst::const_iterator i_it = instruction.source;
1139 stack.swap(instruction.stack);
1140 instruction.stack.clear();
1141 codet &c = instruction.code;
1144 stack.empty() || instruction.predecessors.size() <= 1 ||
1147 irep_idt statement=i_it->statement;
1154 if(statement.
size()>=2 &&
1155 statement[statement.
size()-2]==
'_' &&
1156 isdigit(statement[statement.
size()-1]))
1163 statement=std::string(
id2string(statement), 0, statement.size()-2);
1174 if(cur_pc==it->handler_pc)
1182 catch_type=it->catch_type;
1186 codet catch_instruction;
1188 if(catch_type!=
typet())
1202 stack.push_back(catch_var);
1204 catch_instruction=catch_statement;
1211 if(statement==
"aconst_null")
1213 assert(results.size()==1);
1216 else if(statement==
"athrow")
1221 else if(statement==
"checkcast")
1229 else if(statement==
"invokedynamic")
1234 lambda_method_handles, i_it->source_location, arg0))
1240 else if(statement==
"invokestatic" &&
1242 "java::org.cprover.CProver.assume:(Z)V")
1246 "function expected to have exactly one parameter");
1249 else if(statement==
"invokeinterface" ||
1250 statement==
"invokespecial" ||
1251 statement==
"invokevirtual" ||
1252 statement==
"invokestatic")
1254 convert_invoke(i_it->source_location, statement, arg0, c, results);
1256 else if(statement==
"return")
1261 else if(statement==
patternt(
"?return"))
1271 else if(statement==
patternt(
"?astore"))
1273 assert(op.size()==3 && results.empty());
1276 else if(statement==
patternt(
"?store"))
1283 else if(statement==
patternt(
"?aload"))
1288 else if(statement==
patternt(
"?load"))
1294 else if(statement==
"ldc" || statement==
"ldc_w" ||
1295 statement==
"ldc2" || statement==
"ldc2_w")
1300 arg0.
id() != ID_java_string_literal && arg0.
id() != ID_type,
1301 "String and Class literals should have been lowered in " 1302 "generate_constant_global_variables");
1306 else if(statement==
"goto" || statement==
"goto_w")
1311 INVARIANT(!ret,
"goto argument should be an integer");
1315 else if(statement==
"jsr" || statement==
"jsr_w")
1321 INVARIANT(!ret,
"jsr argument should be an integer");
1326 std::next(i_it)->address,
1330 else if(statement==
"ret")
1336 assert(!jsr_ret_targets.empty());
1340 else if(statement==
"iconst_m1")
1342 assert(results.size()==1);
1345 else if(statement==
patternt(
"?const"))
1347 assert(results.size()==1);
1350 else if(statement==
patternt(
"?ipush"))
1354 arg0.
id()==ID_constant,
1355 "ipush argument expected to be constant");
1360 else if(statement==
patternt(
"if_?cmp??"))
1365 INVARIANT(!ret,
"if_?cmp?? argument should be an integer");
1367 address_map, statement, op, number, i_it->source_location);
1369 else if(statement==
patternt(
"if??"))
1372 statement==
"ifeq"?ID_equal:
1373 statement==
"ifne"?ID_notequal:
1374 statement==
"iflt"?ID_lt:
1375 statement==
"ifge"?ID_ge:
1376 statement==
"ifgt"?ID_gt:
1377 statement==
"ifle"?ID_le:
1380 INVARIANT(!
id.empty(),
"unexpected bytecode-if");
1384 INVARIANT(!ret,
"if?? argument should be an integer");
1385 c =
convert_if(address_map, op,
id, number, i_it->source_location);
1387 else if(statement==
patternt(
"ifnonnull"))
1392 INVARIANT(!ret,
"ifnonnull argument should be an integer");
1395 else if(statement==
patternt(
"ifnull"))
1400 INVARIANT(!ret,
"ifnull argument should be an integer");
1401 c =
convert_ifnull(address_map, op, number, i_it->source_location);
1403 else if(statement==
"iinc")
1407 else if(statement==
patternt(
"?xor"))
1412 else if(statement==
patternt(
"?or"))
1417 else if(statement==
patternt(
"?and"))
1422 else if(statement==
patternt(
"?shl"))
1427 else if(statement==
patternt(
"?shr"))
1432 else if(statement==
patternt(
"?ushr"))
1437 else if(statement==
patternt(
"?add"))
1442 else if(statement==
patternt(
"?sub"))
1447 else if(statement==
patternt(
"?div"))
1452 else if(statement==
patternt(
"?mul"))
1457 else if(statement==
patternt(
"?neg"))
1462 else if(statement==
patternt(
"?rem"))
1465 if(statement==
"frem" || statement==
"drem")
1470 else if(statement==
patternt(
"?cmp"))
1475 else if(statement==
patternt(
"?cmp?"))
1480 else if(statement==
patternt(
"?cmpl"))
1485 else if(statement==
"dup")
1488 results[0]=results[1]=op[0];
1490 else if(statement==
"dup_x1")
1497 else if(statement==
"dup_x2")
1507 else if(statement==
"dup2")
1512 else if(statement==
"dup2_x1")
1517 else if(statement==
"dup2_x2")
1522 else if(statement==
"dconst")
1526 else if(statement==
"fconst")
1530 else if(statement==
"getfield")
1535 else if(statement==
"getstatic")
1539 const auto &field_name=arg0.
get_string(ID_component_name);
1540 const bool is_assertions_disabled_field=
1541 field_name.find(
"$assertionsDisabled")!=std::string::npos;
1543 symbol_expr.set_identifier(
1548 "getstatic symbol should have been created before method conversion");
1551 arg0, symbol_expr, is_assertions_disabled_field, c, results);
1553 else if(statement==
"putfield")
1558 else if(statement==
"putstatic")
1562 const auto &field_name=arg0.
get_string(ID_component_name);
1563 symbol_expr.set_identifier(
1568 "putstatic symbol should have been created before method conversion");
1572 else if(statement==
patternt(
"?2?"))
1577 if(results[0].type()!=type)
1578 results[0].make_typecast(type);
1580 else if(statement==
"new")
1584 convert_new(i_it->source_location, arg0, c, results);
1586 else if(statement==
"newarray" ||
1587 statement==
"anewarray")
1593 else if(statement==
"multianewarray")
1599 INVARIANT(!ret,
"multianewarray argument should be an integer");
1603 assert(results.size()==1);
1606 else if(statement==
"arraylength")
1613 assert(pointer.type().subtype().id()==ID_symbol);
1614 array.
set(ID_java_member_access,
true);
1620 else if(statement==
"tableswitch" ||
1621 statement==
"lookupswitch")
1624 c =
convert_switch(address_map, op, i_it->args, i_it->source_location);
1626 else if(statement==
"pop" || statement==
"pop2")
1630 else if(statement==
"instanceof")
1637 else if(statement==
"monitorenter")
1641 else if(statement==
"monitorexit")
1645 else if(statement==
"swap")
1651 else if(statement==
"nop")
1666 if(catch_instruction!=
codet())
1672 if(!i_it->source_location.get_line().empty())
1677 instruction.done =
true;
1678 for(
const unsigned address : instruction.successors)
1680 address_mapt::iterator a_it2=address_map.find(address);
1686 if(address==exception_row.handler_pc)
1693 if(!
stack.empty() && a_it2->second.predecessors.size()>1)
1700 if(a_it2->second.stack.empty())
1702 for(stackt::iterator s_it=
stack.begin();
1716 a_it2->second.stack.size() ==
stack.size(),
1717 "Stack sizes should be the same.");
1718 stackt::const_iterator os_it=a_it2->second.stack.begin();
1719 for(
auto &expr :
stack)
1721 assert(
has_prefix(os_it->get_string(ID_C_base_name),
"$stack"));
1740 if(last_statement.get_statement()==ID_goto)
1745 last_statement.operands().begin(),
1754 a_it2->second.stack=
stack;
1764 new_symbol.
name=var.get_identifier();
1765 new_symbol.
type=var.type();
1766 new_symbol.
base_name=var.get(ID_C_base_name);
1768 new_symbol.
mode=ID_java;
1785 bool start_new_block=
true;
1786 bool has_seen_previous_address=
false;
1787 unsigned previous_address=0;
1788 for(
const auto &address_pair : address_map)
1790 const unsigned address=address_pair.first;
1791 assert(address_pair.first==address_pair.second.source->address);
1792 const codet &c=address_pair.second.code;
1795 if(!start_new_block)
1796 start_new_block=targets.find(address)!=targets.end();
1799 if(!start_new_block)
1800 start_new_block=address_pair.second.predecessors.size()>1;
1802 if(!start_new_block && has_seen_previous_address)
1805 if(exception_row.start_pc==previous_address)
1807 start_new_block=
true;
1819 "Block addresses should be unique and increasing");
1827 add_to_block.
add(c);
1829 start_new_block=address_pair.second.successors.size()>1;
1831 previous_address=address;
1832 has_seen_previous_address=
true;
1836 std::map<irep_idt, variablet> temporary_variable_live_ranges;
1837 for(
const auto &aentry : address_map)
1841 temporary_variable_live_ranges);
1843 std::vector<const variablet*> vars_to_process;
1845 for(
const auto &v : vlist)
1846 vars_to_process.push_back(&v);
1849 vars_to_process.push_back(
1850 &temporary_variable_live_ranges.at(v.get_identifier()));
1853 vars_to_process.push_back(
1854 &temporary_variable_live_ranges.at(v.get_identifier()));
1856 for(
const auto vp : vars_to_process)
1870 v.start_pc+v.length,
1871 std::numeric_limits<unsigned>::max(),
1874 for(
const auto vp : vars_to_process)
1880 if(v.symbol_expr.get_identifier().empty())
1886 v.start_pc+v.length,
1887 std::numeric_limits<unsigned>::max());
1889 block.operands().insert(block.operands().begin(), d);
1892 for(
auto &block : root_block.
operands())
1923 code_switch.
value() = op[0];
1927 bool is_label =
true;
1928 for(
auto a_it = args.begin(); a_it != args.end();
1929 a_it++, is_label = !is_label)
1943 if(a_it == args.begin())
1955 code_block.
add(code_case);
1959 code_switch.
body() = code_block;
1972 results.insert(results.end(), op.begin(), op.end());
1973 results.insert(results.end(), op.begin(), op.end());
1985 results.insert(results.end(), op.begin() + 1, op.end());
1986 results.insert(results.end(), op.begin(), op.end());
2005 results.insert(results.end(), op.begin(), op.end());
2006 results.insert(results.end(), op2.begin(), op2.end());
2007 results.insert(results.end(), op.begin(), op.end());
2015 const char type_char = statement[0];
2016 const bool is_double(
'd' == type_char);
2017 const bool is_float(
'f' == type_char);
2019 if(is_double || is_float)
2026 if(arg0.
type().
id() != ID_floatbv)
2056 const bool use_this(statement !=
"invokestatic");
2057 const bool is_virtual(
2058 statement ==
"invokevirtual" || statement ==
"invokeinterface");
2065 if(parameters.empty() || !parameters[0].get_this())
2071 if(statement ==
"invokespecial")
2080 code_type.
set(ID_java_super_method_call,
true);
2086 parameters.insert(parameters.begin(), this_p);
2101 this_arg.
type().
id() == ID_pointer,
"first argument must be a pointer");
2109 for(std::size_t i = 0; i < parameters.size(); i++)
2111 const typet &type = parameters[i].type();
2115 type.
id() == ID_pointer)
2119 call.
arguments()[i].make_typecast(type);
2127 if(return_type.
id() != ID_empty)
2133 results[0] = promoted;
2136 assert(arg0.
id() == ID_virtual_function);
2166 symbol.
type.
set(ID_access, ID_public);
2168 symbol.
mode = ID_java;
2172 debug() <<
"Generating codet: new opaque symbol: method '" << symbol.
name 2212 c = std::move(ret_block);
2244 c = std::move(assert_class);
2257 "java::java.lang.AssertionError")
2266 assert_location.
set(
"user-provided",
true);
2273 assume_location.
set(
"user-provided",
true);
2293 const std::set<unsigned int> &working_set,
2294 unsigned int cur_pc,
2297 std::vector<irep_idt> exception_ids;
2298 std::vector<irep_idt> handler_labels;
2305 std::size_t
pos = 0;
2306 std::size_t end_pc = 0;
2323 exception_ids.push_back(
2328 handler_labels.push_back(
2336 if(!exception_ids.empty())
2340 exception_ids.size() == handler_labels.size(),
2341 "Exception tags and handler labels should be 1-to-1");
2344 for(
size_t i = 0; i < exception_ids.size(); ++i)
2346 exception_list.push_back(
2348 exception_ids[i], handler_labels[i]));
2364 exception_ids.clear();
2365 handler_labels.clear();
2369 size_t start_pc = 0;
2372 bool first_handler =
false;
2378 cur_pc < exception_row.end_pc && !working_set.empty() &&
2379 *working_set.begin() == exception_row.end_pc)
2383 if(exception_row.start_pc != start_pc || !first_handler)
2386 first_handler =
true;
2389 start_pc = exception_row.start_pc;
2444 java_new_array.operands() = op;
2447 java_new_array.add_source_location() = location;
2461 c = std::move(create);
2475 if(statement ==
"newarray")
2481 else if(
id == ID_char)
2483 else if(
id == ID_float)
2485 else if(
id == ID_double)
2487 else if(
id == ID_byte)
2489 else if(
id == ID_short)
2491 else if(
id == ID_int)
2493 else if(
id == ID_long)
2533 java_new_expr.add_source_location() = location;
2545 c = std::move(ret_block);
2573 "stack_static_field",
2592 arg0.
get(ID_component_name));
2600 const bool is_assertions_disabled_field,
2606 if(arg0.
type().
id() == ID_symbol)
2611 else if(arg0.
type().
id() == ID_pointer)
2620 else if(is_assertions_disabled_field)
2633 else if(is_assertions_disabled_field)
2645 const int nan_value(statement[4] ==
'l' ? -1 : 1);
2695 const std::size_t width = type.
get_size_t(ID_width);
2699 if(lhs.
type() != target)
2702 if(rhs.
type() != target)
2706 if(results[0].type() != op[0].type())
2707 results[0].make_typecast(op[0].type());
2715 const unsigned address)
2730 exprt arg1_int_type = arg1;
2781 code_branch.
cond() =
2808 const typet &lhs_type(lhs.type());
2809 if(lhs_type != rhs.type())
2812 code_branch.
cond() = condition;
2823 const std::vector<unsigned int> &jsr_ret_targets,
2826 const unsigned address)
2830 for(
size_t idx = 0, idxlim = jsr_ret_targets.size(); idx != idxlim; ++idx)
2835 if(idx == idxlim - 1)
2844 branch.cond().add_source_location() = location;
2846 branch.add_source_location() = location;
2857 const char &type_char = statement[0];
2861 deref.
set(ID_java_member_access,
true);
2868 data_plus_offset.
set(ID_java_array_access,
true);
2878 const unsigned address,
2884 exprt toassign = op[0];
2885 if(
'a' == statement[0] && toassign.
type() != var.
type())
2897 assign.add_source_location() = location;
2907 const char type_char = statement[0];
2911 deref.
set(ID_java_member_access,
true);
2918 data_plus_offset.
set(ID_java_array_access,
true);
2930 block.
move(array_put);
2942 lambda_method_handles,
2943 code_type.
get_int(ID_java_lambda_method_handle_index));
2944 if(lambda_method_symbol.has_value())
2945 debug() <<
"Converting invokedynamic for lambda: " 2946 << lambda_method_symbol.value().name <<
eom;
2948 debug() <<
"Converting invokedynamic for lambda with unknown handle " 2954 pop(parameters.size());
2958 if(return_type.id() == ID_empty)
2967 const std::vector<unsigned int> &jsr_ret_targets,
2969 std::vector<java_bytecode_parse_treet::instructiont>::const_iterator>
2970 &ret_instructions)
const 2973 for(
const auto &retinst : ret_instructions)
2975 auto &a_entry = address_map.at(retinst->address);
2976 a_entry.successors.insert(
2977 a_entry.successors.end(), jsr_ret_targets.begin(), jsr_ret_targets.end());
2982 const unsigned int address,
2986 std::vector<unsigned>
result;
2987 for(
const auto &exception_row : exception_table)
2989 if(address >= exception_row.start_pc && address < exception_row.end_pc)
2990 result.push_back(exception_row.handler_pc);
3010 &local_variable_table,
3022 typedef std::pair<irep_idt, irep_idt> base_name_and_identifiert;
3023 std::map<std::size_t, base_name_and_identifiert> param_names;
3024 for(
const auto &v : local_variable_table)
3026 if(v.index < slots_for_parameters)
3027 param_names.emplace(
3034 std::size_t param_index = 0;
3035 for(
auto ¶m : parameters)
3044 if(param_index == 0 && param.get_this())
3052 auto param_name = param_names.find(param_index);
3053 if(param_name != param_names.end())
3055 base_name = param_name->second.first;
3056 identifier = param_name->second.second;
3063 const typet &type = param.type();
3070 param.set_base_name(base_name);
3071 param.set_identifier(identifier);
3076 parameter_symbol.
mode = ID_java;
3077 parameter_symbol.
name = identifier;
3078 parameter_symbol.
type = param.type();
3079 symbol_table.
insert(parameter_symbol);
3090 size_t max_array_length,
3091 bool throw_assertion_error,
3096 if(std::regex_match(
3098 std::regex(
".*org\\.cprover\\.CProver.*")) &&
3110 throw_assertion_error,
3111 needed_lazy_methods,
3135 return inherited_method.
is_valid();
3145 const irep_idt &component_name)
const 3157 inherited_method.
is_valid(),
"static field should be in symbol table");
3165 const std::string &tmp_var_prefix,
3166 const typet &tmp_var_type,
3171 for(
auto &stack_entry :
stack)
3174 while(stack_entry.id()==ID_typecast)
3180 stack_entry.id()==ID_symbol)
3189 stack_entry.id()==ID_dereference)
3194 stack_entry.id()==ID_member)
3198 if(entry_id==identifier)
3206 const std::string &tmp_var_prefix,
3207 const typet &tmp_var_type,
3211 const exprt tmp_var=
3214 stack_entry=tmp_var;
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
void draw_edges_from_ret_to_jsr(address_mapt &address_map, const std::vector< unsigned int > &jsr_ret_targets, const std::vector< std::vector< java_bytecode_parse_treet::instructiont >::const_iterator > &ret_instructions) const
const codet & then_case() const
codet convert_monitorenter(const source_locationt &location, const exprt::operandst &op) const
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
codet convert_monitorexit(const source_locationt &location, const exprt::operandst &op) const
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
static optionalt< annotationt > find_annotation(const annotationst &annotations, const irep_idt &annotation_type_name)
Find an annotation given its name.
JAVA Bytecode Language Conversion.
codet convert_putstatic(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, const symbol_exprt &symbol_expr)
A ‘switch’ instruction.
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
void convert(const symbolt &class_symbol, const methodt &)
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)
codet convert_ifnull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
std::vector< symbol_exprt > java_lambda_method_handlest
void set_label(const irep_idt &label)
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.
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)
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)
const exprt variable(const exprt &arg, char type_char, size_t address, variable_cast_argumentt do_cast)
Returns a symbol_exprt indicating a local variable suitable to load/store from a bytecode at address ...
static bool operator==(const irep_idt &what, const patternt &pattern)
constant_exprt to_expr() const
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...
static void gather_symbol_live_ranges(unsigned pc, const exprt &e, std::map< irep_idt, java_bytecode_convert_methodt::variablet > &result)
methodt::instructionst instructionst
const java_lambda_method_handlest & lambda_method_handles() const
irep_idt mode
Language mode.
code_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.
const exprt & cond() const
source_locationt source_location
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
code_blockt & get_or_create_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned 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...
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
reference_typet java_reference_type(const typet &subtype)
void set_comment(const irep_idt &comment)
signed int get_int(const irep_namet &name) const
static irep_idt label(const irep_idt &address)
exception_tablet exception_table
void copy_to_operands(const exprt &expr)
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.
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.
void move_to_operands(exprt &expr)
struct bytecode_infot const bytecode_info[]
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
std::vector< parametert > parameterst
exprt value
Initial value of symbol.
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.
irep_idt module
Name of module the symbol belongs to.
A ‘goto’ instruction.
irep_idt pretty_name
Language-specific display name.
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
codet convert_iinc(const exprt &arg0, const exprt &arg1, const source_locationt &location, unsigned address)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
std::vector< unsigned int > try_catch_handler(unsigned int address, const java_bytecode_parse_treet::methodt::exception_tablet &exception_table) const
A constant literal expression.
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
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...
std::map< unsigned, converted_instructiont > address_mapt
reference_typet java_array_type(const char subtype)
codet convert_switch(java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const java_bytecode_parse_treet::instructiont::argst &args, const source_locationt &location)
expanding_vectort< variablest > variables
A side effect that throws an exception.
codet convert_instructions(const methodt &, const code_typet &, const irep_idt &, const java_class_typet::java_lambda_method_handlest &)
#define INVARIANT(CONDITION, REASON)
const exprt & case_op() const
unsigned java_method_parameter_slots(const code_typet &t)
Returns the the number of JVM local variables (slots) used by the JVM to pass, upon call...
code_blockt & get_block_for_pcrange(block_tree_nodet &tree, code_blockt &this_block, unsigned address_start, unsigned address_limit, unsigned next_block_start_address)
'tree' describes a tree of code_blockt objects; this_block is the corresponding block (thus they are ...
void set_base_name(const irep_idt &name)
static ieee_float_spect double_precision()
Extract member of struct or union.
mstreamt & warning() const
codet convert_putfield(const exprt &arg0, const exprt::operandst &op)
irep_idt current_method
A copy of method_id :/.
instructionst instructions
void set_is_constructor()
Expression Initialization.
const irep_idt & id() const
Evaluates to true if the operand is NaN.
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()
static irep_idt get_if_cmp_operator(const irep_idt &stmt)
Given a string of the format '?blah?', will return true when compared against a string that matches a...
const irep_idt & get_line() const
division (integer and real)
A reference into the symbol table.
A declaration of a local variable.
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)
exprt::operandst & convert_ushr(const irep_idt &statement, const exprt::operandst &op, exprt::operandst &results) const
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.
codet replace_character_call(code_function_callt call)
Operator to dereference a pointer.
void convert_multianewarray(const source_locationt &location, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
typet java_type_from_char(char t)
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...
codet convert_store(const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, const unsigned address, const source_locationt &location)
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...
static ieee_float_spect single_precision()
class_hierarchyt class_hierarchy
A label for branch targets.
#define PRECONDITION(CONDITION)
static unsigned get_bytecode_type_width(const typet &ty)
Given a class and a component (either field or method), find the closest parent that defines that com...
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
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 a generic exprt to a symbol_exprt.
void convert_invoke(source_locationt location, const irep_idt &statement, exprt &arg0, codet &c, exprt::operandst &results)
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 ...
const size_t max_array_length
java_string_library_preprocesst & string_preprocess
codet & find_last_statement()
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 a generic 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
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
std::vector< block_tree_nodet > branch
unsigned integer2unsigned(const mp_integer &n)
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
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
static void assign_parameter_names(code_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...
message_handlert & get_message_handler()
std::vector< exceptiont > exception_tablet
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
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)
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
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const source_locationt & source_location() const
irep_idt get_component_name() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
std::vector< local_variablet > local_variable_tablet
void save_stack_entries(const std::string &, const typet &, code_blockt &, const bytecode_write_typet, const irep_idt &)
create temporary variables if a write instruction can have undesired side- effects ...
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)
unsigned int get_unsigned_int(const irep_namet &name) const
source_locationt & add_source_location()
std::vector< exprt > argst
const codet & to_code(const exprt &expr)
codet & do_exception_handling(const methodt &method, const std::set< unsigned int > &working_set, unsigned int cur_pc, codet &c)
symbol_table_baset & symbol_table
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)
local_variable_tablet local_variable_table
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 generic typet to a pointer_typet.
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
A generic base class for expressions that are predicates, i.e., boolean-typed, and that take exactly ...
unsigned slots_for_parameters
Number of local variable slots used by the JVM to pass parameters upon invocation of the method under...
std::size_t integer2size_t(const mp_integer &n)
codet convert_ifnonull(const java_bytecode_convert_methodt::address_mapt &address_map, const exprt::operandst &op, const mp_integer &number, const source_locationt &location) const
const code_labelt & to_code_label(const codet &code)
JAVA Bytecode Language Conversion.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
An expression containing a side effect.
Compute dominators for CFG of goto_function.
codet 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
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...
resolve_inherited_componentt::inherited_componentt get_inherited_component(const irep_idt &component_class_id, const irep_idt &component_name, const irep_idt &user_class_id, 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.
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)
void convert_newarray(const source_locationt &location, const irep_idt &statement, const exprt &arg0, const exprt::operandst &op, codet &c, exprt::operandst &results)
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...
codet convert_astore(const irep_idt &statement, const exprt::operandst &op, const source_locationt &location)
void make_typecast(const typet &_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.
optionalt< std::string > signature
codet 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
std::vector< unsigned > branch_addresses
const typet & return_type() const
const java_class_typet & to_java_class_type(const typet &type)
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
A statement that catches an exception, assigning the exception in flight to an expression (e...
void branch(goto_modelt &goto_model, const irep_idt &id)
const exprt & assertion() const
Produce code for simple implementation of String Java libraries.
code_blockt convert_ret(const std::vector< unsigned int > &jsr_ret_targets, const exprt &arg0, const source_locationt &location, const unsigned address)
static block_tree_nodet get_leaf()
IEEE-floating-point equality.
std::string pretty_signature(const code_typet &code_type)