diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index cc4b91b5cb7..49b621aed89 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -26,7 +26,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -namespace { class patternt { public: @@ -82,16 +81,17 @@ class java_bytecode_convert_methodt:public messaget symbol_exprt symbol_expr; size_t start_pc; size_t length; + bool is_parameter; }; typedef std::vector variablest; expanding_vector variables; - + std::set used_local_names; bool method_has_this; typedef enum instruction_sizet { - INST_INDEX = 2, INST_INDEX_CONST = 3 + INST_INDEX=2, INST_INDEX_CONST=3 } instruction_sizet; // return corresponding reference of variable @@ -102,19 +102,20 @@ class java_bytecode_convert_methodt:public messaget { for(variablet &var : var_list) { - size_t start_pc = var.start_pc; - size_t length = var.length; - if (address + (size_t) inst_size >= start_pc && address < start_pc + length) + size_t start_pc=var.start_pc; + size_t length=var.length; + if(address+(size_t)inst_size>=start_pc && + address::max(); + size_t list_length=var_list.size(); + var_list.resize(list_length+1); + var_list[list_length].start_pc=0; + var_list[list_length].length=std::numeric_limits::max(); return var_list[list_length]; } @@ -136,10 +137,10 @@ class java_bytecode_convert_methodt:public messaget std::size_t number_int=safe_string2size_t(id2string(number)); typet t=java_type_from_char(type_char); - variablest &var_list = variables[number_int]; + variablest &var_list=variables[number_int]; // search variable in list for correct frame / address if necessary - variablet &var = + variablet &var= find_variable_for_slot(address, var_list, inst_size); if(var.symbol_expr.get_identifier().empty()) @@ -150,12 +151,15 @@ class java_bytecode_convert_methodt:public messaget symbol_exprt result(identifier, t); result.set(ID_C_base_name, base_name); + used_local_names.insert(result); return result; } else { exprt result=var.symbol_expr; + if(!var.is_parameter) + used_local_names.insert(to_symbol_expr(result)); if(do_cast==CAST_AS_NEEDED && t!=result.type()) result=typecast_exprt(result, t); return result; } @@ -228,38 +232,36 @@ class java_bytecode_convert_methodt:public messaget const bytecode_infot &get_bytecode_info(const irep_idt &statement); }; -} - -namespace { const size_t SLOTS_PER_INTEGER(1u); const size_t INTEGER_WIDTH(64u); -size_t count_slots(const size_t value, const code_typet::parametert ¶m) +static size_t count_slots( + const size_t value, + const code_typet::parametert ¶m) { const std::size_t width(param.type().get_unsigned_int(ID_width)); - return value + SLOTS_PER_INTEGER + width / INTEGER_WIDTH; + return value+SLOTS_PER_INTEGER+width/INTEGER_WIDTH; } -size_t get_variable_slots(const code_typet::parametert ¶m) +static size_t get_variable_slots(const code_typet::parametert ¶m) { return count_slots(0, param); } -bool is_constructor(const class_typet::methodt &method) +static bool is_constructor(const class_typet::methodt &method) { const std::string &name(id2string(method.get_name())); const std::string::size_type &npos(std::string::npos); - return npos != name.find("") || npos != name.find(""); + return npos!=name.find("") || npos!=name.find(""); } -void cast_if_necessary(binary_relation_exprt &condition) +static void cast_if_necessary(binary_relation_exprt &condition) { exprt &lhs(condition.lhs()); exprt &rhs(condition.rhs()); const typet &lhs_type(lhs.type()); - if(lhs_type == rhs.type()) return; - rhs = typecast_exprt(rhs, lhs_type); -} + if(lhs_type==rhs.type()) return; + rhs=typecast_exprt(rhs, lhs_type); } /*******************************************************************\ @@ -278,8 +280,6 @@ void java_bytecode_convert_methodt::convert( const symbolt &class_symbol, const methodt &m) { - //const class_typet &class_type=to_class_type(class_symbol.type); - typet member_type=java_type_from_string(m.signature); assert(member_type.id()==ID_code); @@ -320,16 +320,16 @@ void java_bytecode_convert_methodt::convert( irep_idt identifier(id_oss.str()); symbol_exprt result(identifier, t); result.set(ID_C_base_name, v.name); - size_t number_index_entries = variables[v.index].size(); - variables[v.index].resize(number_index_entries + 1); - variables[v.index][number_index_entries].symbol_expr = result; - variables[v.index][number_index_entries].start_pc = v.start_pc; - variables[v.index][number_index_entries].length = v.length; + size_t number_index_entries=variables[v.index].size(); + variables[v.index].resize(number_index_entries+1); + variables[v.index][number_index_entries].symbol_expr=result; + variables[v.index][number_index_entries].start_pc=v.start_pc; + variables[v.index][number_index_entries].length=v.length; } // set up variables array for(std::size_t i=0, param_index=0; - i < parameters.size(); ++i) + i::max(); + variables[param_index][0].length=std::numeric_limits::max(); + variables[param_index][0].is_parameter=true; param_index+=slots; } @@ -459,29 +460,27 @@ const bytecode_infot &java_bytecode_convert_methodt::get_bytecode_info( throw 0; } -namespace { - -irep_idt get_if_cmp_operator(const irep_idt &stmt) +static irep_idt get_if_cmp_operator(const irep_idt &stmt) { - if(stmt == patternt("if_?cmplt")) return ID_lt; - if(stmt == patternt("if_?cmple")) return ID_le; - if(stmt == patternt("if_?cmpgt")) return ID_gt; - if(stmt == patternt("if_?cmpge")) return ID_ge; - if(stmt == patternt("if_?cmpeq")) return ID_equal; - if(stmt == patternt("if_?cmpne")) return ID_notequal; + if(stmt==patternt("if_?cmplt")) return ID_lt; + if(stmt==patternt("if_?cmple")) return ID_le; + if(stmt==patternt("if_?cmpgt")) return ID_gt; + if(stmt==patternt("if_?cmpge")) return ID_ge; + if(stmt==patternt("if_?cmpeq")) return ID_equal; + if(stmt==patternt("if_?cmpne")) return ID_notequal; throw "Unhandled java comparison instruction"; } -constant_exprt as_number(const mp_integer value, const typet &type) +static constant_exprt as_number(const mp_integer value, const typet &type) { const std::size_t java_int_width(type.get_unsigned_int(ID_width)); const std::string significant_bits(integer2string(value, 2)); - std::string binary_width(java_int_width - significant_bits.length(), '0'); - return constant_exprt(binary_width += significant_bits, type); + std::string binary_width(java_int_width-significant_bits.length(), '0'); + return constant_exprt(binary_width+=significant_bits, type); } -member_exprt to_member(const exprt &pointer, const exprt &fieldref) +static member_exprt to_member(const exprt &pointer, const exprt &fieldref) { symbol_typet class_type(fieldref.get(ID_class)); @@ -493,7 +492,6 @@ member_exprt to_member(const exprt &pointer, const exprt &fieldref) return member_exprt( obj_deref, fieldref.get(ID_component_name), fieldref.type()); } -} /*******************************************************************\ @@ -552,8 +550,8 @@ codet java_bytecode_convert_methodt::convert_instructions( { std::pair a_entry= address_map.insert(std::make_pair( - i_it->address, - converted_instructiont(i_it, code_skipt()))); + i_it->address, + converted_instructiont(i_it, code_skipt()))); assert(a_entry.second); // addresses are strictly increasing, hence we must have inserted // a new maximal key @@ -711,9 +709,9 @@ codet java_bytecode_convert_methodt::convert_instructions( statement=="invokevirtual" || statement=="invokestatic") { - const bool use_this(statement != "invokestatic"); + const bool use_this(statement!="invokestatic"); const bool is_virtual( - statement == "invokevirtual" || statement == "invokeinterface"); + statement=="invokevirtual" || statement=="invokeinterface"); code_typet &code_type=to_code_type(arg0.type()); code_typet::parameterst ¶meters(code_type.parameters()); @@ -733,7 +731,7 @@ codet java_bytecode_convert_methodt::convert_instructions( code_function_callt call; call.add_source_location()=i_it->source_location; - call.arguments() = pop(parameters.size()); + call.arguments()=pop(parameters.size()); // double-check a bit if(use_this) @@ -805,7 +803,7 @@ codet java_bytecode_convert_methodt::convert_instructions( } call.function().add_source_location()=i_it->source_location; - c = call; + c=call; } else if(statement=="return") { @@ -856,7 +854,7 @@ codet java_bytecode_convert_methodt::convert_instructions( } else if(statement==patternt("?aload")) { - assert(op.size() == 2 && results.size() == 1); + assert(op.size()==2 && results.size()==1); char type_char=statement[0]; @@ -904,7 +902,9 @@ codet java_bytecode_convert_methodt::convert_instructions( { irep_idt class_id=arg0.type().get(ID_identifier); symbol_typet java_lang_Class("java::java.lang.Class"); - symbol_exprt symbol_expr(id2string(class_id)+"@class_model", java_lang_Class); + symbol_exprt symbol_expr( + id2string(class_id)+"@class_model", + java_lang_Class); address_of_exprt address_of_expr(symbol_expr); results[0]=address_of_expr; } @@ -917,7 +917,6 @@ codet java_bytecode_convert_methodt::convert_instructions( error() << "unexpected ldc argument" << eom; throw 0; } - } else if(statement=="goto" || statement=="goto_w") { @@ -933,33 +932,33 @@ codet java_bytecode_convert_methodt::convert_instructions( } else if(statement==patternt("?const")) { - assert(results.size() == 1); + assert(results.size()==1); const char type_char=statement[0]; - const bool is_double('d' == type_char); - const bool is_float('f' == type_char); + const bool is_double('d'==type_char); + const bool is_float('f'==type_char); if(is_double || is_float) { const ieee_float_spect spec( - is_float ? - ieee_float_spect::single_precision() : - ieee_float_spect::double_precision()); + is_float ? + ieee_float_spect::single_precision() : + ieee_float_spect::double_precision()); ieee_floatt value(spec); const typet &arg_type(arg0.type()); - if(ID_integer == arg_type.id()) + if(ID_integer==arg_type.id()) value.from_integer(arg0.get_int(ID_value)); else value.from_expr(to_constant_expr(arg0)); - results[0] = value.to_expr(); + results[0]=value.to_expr(); } else { const unsigned int value(arg0.get_unsigned_int(ID_value)); const typet type=java_type_from_char(statement[0]); - results[0] = as_number(value, type); + results[0]=as_number(value, type); } } else if(statement==patternt("?ipush")) @@ -1000,7 +999,8 @@ codet java_bytecode_convert_methodt::convert_instructions( assert(op.size()==1 && results.empty()); code_ifthenelset code_branch; - code_branch.cond()=binary_relation_exprt(op[0], id, gen_zero(op[0].type())); + code_branch.cond()= + binary_relation_exprt(op[0], id, gen_zero(op[0].type())); code_branch.cond().add_source_location()=i_it->source_location; code_branch.then_case()=code_gotot(label(number)); code_branch.then_case().add_source_location()=i_it->source_location; @@ -1118,7 +1118,7 @@ codet java_bytecode_convert_methodt::convert_instructions( } else if(statement==patternt("?cmp")) { - assert(op.size() == 2 && results.size() == 1); + assert(op.size()==2 && results.size()==1); // The integer result on the stack is: // 0 if op[0] equals op[1] @@ -1135,21 +1135,33 @@ codet java_bytecode_convert_methodt::convert_instructions( else if(statement==patternt("?cmp?")) { assert(op.size()==2 && results.size()==1); - const floatbv_typet type(to_floatbv_type(java_type_from_char(statement[0]))); + const floatbv_typet type( + to_floatbv_type(java_type_from_char(statement[0]))); const ieee_float_spect spec(type); const ieee_floatt nan(ieee_floatt::NaN(spec)); const constant_exprt nan_expr(nan.to_expr()); - const int nan_value(statement[4] == 'l' ? -1 : 1); + const int nan_value(statement[4]=='l' ? -1 : 1); const typet result_type(java_int_type()); const exprt nan_result(from_integer(nan_value, result_type)); - // (value1 == NaN || value2 == NaN) ? nan_value : value1 < value2 ? -1 : value2 < value1 1 ? 1 : 0; - // (value1 == NaN || value2 == NaN) ? nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0; + // (value1 == NaN || value2 == NaN) ? + // nan_value : value1 < value2 ? -1 : value2 < value1 1 ? 1 : 0; + // (value1 == NaN || value2 == NaN) ? + // nan_value : value1 == value2 ? 0 : value1 < value2 -1 ? 1 : 0; results[0]= - if_exprt(or_exprt(ieee_float_equal_exprt(nan_expr, op[0]), ieee_float_equal_exprt(nan_expr, op[1])), nan_result, - if_exprt(ieee_float_equal_exprt(op[0], op[1]), gen_zero(result_type), - if_exprt(binary_relation_exprt(op[0], ID_lt, op[1]), from_integer(-1, result_type), from_integer(1, result_type)))); + if_exprt( + or_exprt( + ieee_float_equal_exprt(nan_expr, op[0]), + ieee_float_equal_exprt(nan_expr, op[1])), + nan_result, + if_exprt( + ieee_float_equal_exprt(op[0], op[1]), + gen_zero(result_type), + if_exprt( + binary_relation_exprt(op[0], ID_lt, op[1]), + from_integer(-1, result_type), + from_integer(1, result_type)))); } else if(statement==patternt("?cmpl")) { @@ -1240,19 +1252,21 @@ codet java_bytecode_convert_methodt::convert_instructions( { assert(op.empty() && results.size()==1); symbol_exprt symbol_expr(arg0.type()); - symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+arg0.get_string(ID_component_name)); + symbol_expr.set_identifier( + arg0.get_string(ID_class)+"."+arg0.get_string(ID_component_name)); results[0]=java_bytecode_promotion(symbol_expr); } else if(statement=="putfield") { assert(op.size()==2 && results.size()==0); - c = code_assignt(to_member(op[0], arg0), op[1]); + c=code_assignt(to_member(op[0], arg0), op[1]); } else if(statement=="putstatic") { assert(op.size()==1 && results.empty()); symbol_exprt symbol_expr(arg0.type()); - symbol_expr.set_identifier(arg0.get_string(ID_class)+"."+arg0.get_string(ID_component_name)); + symbol_expr.set_identifier( + arg0.get_string(ID_class)+"."+arg0.get_string(ID_component_name)); c=code_assignt(symbol_expr, op[0]); } else if(statement==patternt("?2?")) // i2c etc. @@ -1529,6 +1543,23 @@ codet java_bytecode_convert_methodt::convert_instructions( // review successor computation of athrow! code_blockt code; + // locals + for(const auto & var : used_local_names) + { + code.add(code_declt(var)); + symbolt new_symbol; + new_symbol.name=var.get_identifier(); + new_symbol.type=var.type(); + new_symbol.base_name=var.get(ID_C_base_name); + new_symbol.pretty_name= + id2string(var.get_identifier()).substr(6, std::string::npos); + new_symbol.mode=ID_java; + new_symbol.is_type=false; + new_symbol.is_file_local=true; + new_symbol.is_thread_local=true; + new_symbol.is_lvalue=true; + symbol_table.add(new_symbol); + } // temporaries for(const auto & var : tmp_vars) {