From 54fab5b502cb59e6a4d797314cd3563f464b8488 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 4 Aug 2016 10:45:54 +0100 Subject: [PATCH 1/2] Add Java locals to the symbol table and give them declarations This is required for SSA renaming to work on Java local symbols. --- .../java_bytecode_convert_method.cpp | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index cc4b91b5cb7..c1983f139c0 100644 --- a/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/src/java_bytecode/java_bytecode_convert_method.cpp @@ -82,11 +82,12 @@ 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 @@ -150,13 +151,16 @@ 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(do_cast==CAST_AS_NEEDED && t!=result.type()) result=typecast_exprt(result, t); + 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; } } @@ -379,6 +383,7 @@ void java_bytecode_convert_methodt::convert( variables[param_index][0].symbol_expr=parameter_symbol.symbol_expr(); variables[param_index][0].start_pc=0; variables[param_index][0].length = std::numeric_limits::max(); + variables[param_index][0].is_parameter=true; param_index+=slots; } @@ -1529,6 +1534,22 @@ 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) { From 55ef3ff0ae9e923e987555e8f60295b1b3fb96d4 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 14 Dec 2016 15:01:00 +0000 Subject: [PATCH 2/2] cpplint fixes for java_bytecode_convert_method.cpp --- .../java_bytecode_convert_method.cpp | 168 ++++++++++-------- 1 file changed, 89 insertions(+), 79 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp index c1983f139c0..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: @@ -92,7 +91,7 @@ class java_bytecode_convert_methodt:public messaget 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 @@ -103,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]; } @@ -137,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()) @@ -160,7 +160,7 @@ class java_bytecode_convert_methodt:public messaget 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); + if(do_cast==CAST_AS_NEEDED && t!=result.type()) result=typecast_exprt(result, t); return result; } } @@ -232,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); } /*******************************************************************\ @@ -282,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); @@ -324,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; } @@ -464,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)); @@ -498,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()); } -} /*******************************************************************\ @@ -557,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 @@ -716,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()); @@ -738,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) @@ -810,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") { @@ -861,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]; @@ -909,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; } @@ -922,7 +917,6 @@ codet java_bytecode_convert_methodt::convert_instructions( error() << "unexpected ldc argument" << eom; throw 0; } - } else if(statement=="goto" || statement=="goto_w") { @@ -938,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")) @@ -1005,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; @@ -1123,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] @@ -1140,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")) { @@ -1245,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. @@ -1542,7 +1551,8 @@ codet java_bytecode_convert_methodt::convert_instructions( 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.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;