From af79cb91a2b449460bc1ad1dc23b31dddde795c4 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 31 Jul 2018 12:40:49 +0100 Subject: [PATCH] add support for Visual Studio style inline assembler --- .../assembly_call_graph_test/main.c | 14 +- src/goto-programs/remove_asm.cpp | 462 ++++++++++++------ 2 files changed, 315 insertions(+), 161 deletions(-) diff --git a/regression/goto-instrument/assembly_call_graph_test/main.c b/regression/goto-instrument/assembly_call_graph_test/main.c index afc2bbc5c3c..6eeb26fcf95 100644 --- a/regression/goto-instrument/assembly_call_graph_test/main.c +++ b/regression/goto-instrument/assembly_call_graph_test/main.c @@ -1,16 +1,10 @@ -// This is a hack to make the test pass on windows. The way CBMC on -// windows handles assembly code needs to be fixed. -// CBMC doesn't recognise __asm mfence as a function. - -#ifndef __GNUC__ -void __asm_mfence(); -#endif - void* thr(void * arg) { #ifdef __GNUC__ -__asm__ __volatile__ ("mfence": : :"memory"); + // gcc/clang syntax + __asm__ __volatile__("mfence" : : : "memory"); #else -__asm_mfence(); + // this is Visual Studio syntax + __asm mfence; #endif } diff --git a/src/goto-programs/remove_asm.cpp b/src/goto-programs/remove_asm.cpp index 3774cf8489d..4e5d13a57e8 100644 --- a/src/goto-programs/remove_asm.cpp +++ b/src/goto-programs/remove_asm.cpp @@ -46,15 +46,24 @@ class remove_asmt goto_programt::instructiont &instruction, goto_programt &dest); + void process_instruction_gcc(const code_asmt &, goto_programt &dest); + + void process_instruction_msc(const code_asmt &, goto_programt &dest); + void gcc_asm_function_call( const irep_idt &function_base_name, - const codet &code, + const code_asmt &code, + goto_programt &dest); + + void msc_asm_function_call( + const irep_idt &function_base_name, + const code_asmt &code, goto_programt &dest); }; void remove_asmt::gcc_asm_function_call( const irep_idt &function_base_name, - const codet &code, + const code_asmt &code, goto_programt &dest) { irep_idt function_identifier=function_base_name; @@ -119,6 +128,52 @@ void remove_asmt::gcc_asm_function_call( } } +void remove_asmt::msc_asm_function_call( + const irep_idt &function_base_name, + const code_asmt &code, + goto_programt &dest) +{ + irep_idt function_identifier = function_base_name; + + code_function_callt function_call; + function_call.lhs().make_nil(); + + const typet void_pointer = pointer_type(void_typet()); + + code_typet fkt_type({}, void_typet()); + fkt_type.make_ellipsis(); + + symbol_exprt fkt(function_identifier, fkt_type); + + function_call.function() = fkt; + + goto_programt::targett call = dest.add_instruction(FUNCTION_CALL); + call->code = function_call; + call->source_location = code.source_location(); + + // do we have it? + if(!symbol_table.has_symbol(function_identifier)) + { + symbolt symbol; + + symbol.name = function_identifier; + symbol.type = fkt_type; + symbol.base_name = function_base_name; + symbol.value = nil_exprt(); + symbol.mode = ID_C; + + symbol_table.add(symbol); + } + + if( + goto_functions.function_map.find(function_identifier) == + goto_functions.function_map.end()) + { + auto &f = goto_functions.function_map[function_identifier]; + f.type = fkt_type; + } +} + /// removes assembler void remove_asmt::process_instruction( goto_programt::instructiont &instruction, @@ -129,167 +184,272 @@ void remove_asmt::process_instruction( const irep_idt &flavor=code.get_flavor(); if(flavor==ID_gcc) + process_instruction_gcc(code, dest); + else if(flavor == ID_msc) + process_instruction_msc(code, dest); + else + DATA_INVARIANT(false, "unexpected assembler flavor"); +} + +/// removes gcc assembler +void remove_asmt::process_instruction_gcc( + const code_asmt &code, + goto_programt &dest) +{ + const irep_idt &i_str = to_string_constant(code.op0()).get_value(); + + std::istringstream str(id2string(i_str)); + assembler_parser.clear(); + assembler_parser.in = &str; + assembler_parser.parse(); + + goto_programt tmp_dest; + bool unknown = false; + bool x86_32_locked_atomic = false; + + for(const auto &instruction : assembler_parser.instructions) { - const irep_idt &i_str= - to_string_constant(code.op0()).get_value(); + if(instruction.empty()) + continue; + +#if 0 + std::cout << "A ********************\n"; + for(const auto &ins : instruction) + { + std::cout << "XX: " << ins.pretty() << '\n'; + } + + std::cout << "B ********************\n"; +#endif - // std::cout << "DOING " << i_str << '\n'; + // deal with prefixes + irep_idt command; + unsigned pos = 0; - std::istringstream str(id2string(i_str)); - assembler_parser.clear(); - assembler_parser.in=&str; - assembler_parser.parse(); + if( + instruction.front().id() == ID_symbol && + instruction.front().get(ID_identifier) == "lock") + { + x86_32_locked_atomic = true; + pos++; + } - goto_programt tmp_dest; - bool unknown=false; - bool x86_32_locked_atomic=false; + // done? + if(pos == instruction.size()) + continue; - for(const auto &instruction : assembler_parser.instructions) + if(instruction[pos].id() == ID_symbol) { - if(instruction.empty()) - continue; - - #if 0 - std::cout << "A ********************\n"; - for(const auto &ins : instruction) - { - std::cout << "XX: " << ins.pretty() << '\n'; - } - - std::cout << "B ********************\n"; - #endif - - // deal with prefixes - irep_idt command; - unsigned pos=0; - - if(instruction.front().id()==ID_symbol && - instruction.front().get(ID_identifier)=="lock") - { - x86_32_locked_atomic=true; - pos++; - } - - // done? - if(pos==instruction.size()) - continue; - - if(instruction[pos].id()==ID_symbol) - { - command=instruction[pos].get(ID_identifier); - pos++; - } - - if(command=="xchg" || command=="xchgl") - x86_32_locked_atomic=true; - - if(x86_32_locked_atomic) - { - goto_programt::targett ab=tmp_dest.add_instruction(ATOMIC_BEGIN); - ab->source_location=code.source_location(); - - goto_programt::targett t=tmp_dest.add_instruction(OTHER); - t->source_location=code.source_location(); - t->code=codet(ID_fence); - t->code.add_source_location()=code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); - } - - if(command=="fstcw" || - command=="fnstcw" || - command=="fldcw") // x86 - { - gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest); - } - else if(command=="mfence" || - command=="lfence" || - command=="sfence") // x86 - { - gcc_asm_function_call("__asm_"+id2string(command), code, tmp_dest); - } - else if(command == ID_sync) // Power - { - goto_programt::targett t=tmp_dest.add_instruction(OTHER); - t->source_location=code.source_location(); - t->code=codet(ID_fence); - t->code.add_source_location()=code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); - t->code.set(ID_WWcumul, true); - t->code.set(ID_RWcumul, true); - t->code.set(ID_RRcumul, true); - t->code.set(ID_WRcumul, true); - } - else if(command == ID_lwsync) // Power - { - goto_programt::targett t=tmp_dest.add_instruction(OTHER); - t->source_location=code.source_location(); - t->code=codet(ID_fence); - t->code.add_source_location()=code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WWcumul, true); - t->code.set(ID_RWcumul, true); - t->code.set(ID_RRcumul, true); - } - else if(command == ID_isync) // Power - { - goto_programt::targett t=tmp_dest.add_instruction(OTHER); - t->source_location=code.source_location(); - t->code=codet(ID_fence); - t->code.add_source_location()=code.source_location(); - // doesn't do anything by itself, - // needs to be combined with branch - } - else if(command=="dmb" || command=="dsb") // ARM - { - goto_programt::targett t=tmp_dest.add_instruction(OTHER); - t->source_location=code.source_location(); - t->code=codet(ID_fence); - t->code.add_source_location()=code.source_location(); - t->code.set(ID_WWfence, true); - t->code.set(ID_RRfence, true); - t->code.set(ID_RWfence, true); - t->code.set(ID_WRfence, true); - t->code.set(ID_WWcumul, true); - t->code.set(ID_RWcumul, true); - t->code.set(ID_RRcumul, true); - t->code.set(ID_WRcumul, true); - } - else if(command=="isb") // ARM - { - goto_programt::targett t=tmp_dest.add_instruction(OTHER); - t->source_location=code.source_location(); - t->code=codet(ID_fence); - t->code.add_source_location()=code.source_location(); - // doesn't do anything by itself, - // needs to be combined with branch - } - else - unknown=true; // give up - - if(x86_32_locked_atomic) - { - goto_programt::targett ae=tmp_dest.add_instruction(ATOMIC_END); - ae->source_location=code.source_location(); - - x86_32_locked_atomic=false; - } + command = instruction[pos].get(ID_identifier); + pos++; } - if(unknown) + if(command == "xchg" || command == "xchgl") + x86_32_locked_atomic = true; + + if(x86_32_locked_atomic) { - // we give up; we should perhaps print a warning + goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN); + ab->source_location = code.source_location(); + + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + t->code.set(ID_WWfence, true); + t->code.set(ID_RRfence, true); + t->code.set(ID_RWfence, true); + t->code.set(ID_WRfence, true); + } + + if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86 + { + gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest); + } + else if( + command == "mfence" || command == "lfence" || command == "sfence") // x86 + { + gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest); + } + else if(command == ID_sync) // Power + { + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + t->code.set(ID_WWfence, true); + t->code.set(ID_RRfence, true); + t->code.set(ID_RWfence, true); + t->code.set(ID_WRfence, true); + t->code.set(ID_WWcumul, true); + t->code.set(ID_RWcumul, true); + t->code.set(ID_RRcumul, true); + t->code.set(ID_WRcumul, true); + } + else if(command == ID_lwsync) // Power + { + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + t->code.set(ID_WWfence, true); + t->code.set(ID_RRfence, true); + t->code.set(ID_RWfence, true); + t->code.set(ID_WWcumul, true); + t->code.set(ID_RWcumul, true); + t->code.set(ID_RRcumul, true); + } + else if(command == ID_isync) // Power + { + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + // doesn't do anything by itself, + // needs to be combined with branch + } + else if(command == "dmb" || command == "dsb") // ARM + { + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + t->code.set(ID_WWfence, true); + t->code.set(ID_RRfence, true); + t->code.set(ID_RWfence, true); + t->code.set(ID_WRfence, true); + t->code.set(ID_WWcumul, true); + t->code.set(ID_RWcumul, true); + t->code.set(ID_RRcumul, true); + t->code.set(ID_WRcumul, true); + } + else if(command == "isb") // ARM + { + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + // doesn't do anything by itself, + // needs to be combined with branch + } + else + unknown = true; // give up + + if(x86_32_locked_atomic) + { + goto_programt::targett ae = tmp_dest.add_instruction(ATOMIC_END); + ae->source_location = code.source_location(); + + x86_32_locked_atomic = false; + } + } + + if(unknown) + { + // we give up; we should perhaps print a warning + } + else + dest.destructive_append(tmp_dest); +} + +/// removes msc assembler +void remove_asmt::process_instruction_msc( + const code_asmt &code, + goto_programt &dest) +{ + const irep_idt &i_str = to_string_constant(code.op0()).get_value(); + + std::istringstream str(id2string(i_str)); + assembler_parser.clear(); + assembler_parser.in = &str; + assembler_parser.parse(); + + goto_programt tmp_dest; + bool unknown = false; + bool x86_32_locked_atomic = false; + + for(const auto &instruction : assembler_parser.instructions) + { + if(instruction.empty()) + continue; + +#if 0 + std::cout << "A ********************\n"; + for(const auto &ins : instruction) + { + std::cout << "XX: " << ins.pretty() << '\n'; + } + + std::cout << "B ********************\n"; +#endif + + // deal with prefixes + irep_idt command; + unsigned pos = 0; + + if( + instruction.front().id() == ID_symbol && + instruction.front().get(ID_identifier) == "lock") + { + x86_32_locked_atomic = true; + pos++; + } + + // done? + if(pos == instruction.size()) + continue; + + if(instruction[pos].id() == ID_symbol) + { + command = instruction[pos].get(ID_identifier); + pos++; + } + + if(command == "xchg" || command == "xchgl") + x86_32_locked_atomic = true; + + if(x86_32_locked_atomic) + { + goto_programt::targett ab = tmp_dest.add_instruction(ATOMIC_BEGIN); + ab->source_location = code.source_location(); + + goto_programt::targett t = tmp_dest.add_instruction(OTHER); + t->source_location = code.source_location(); + t->code = codet(ID_fence); + t->code.add_source_location() = code.source_location(); + t->code.set(ID_WWfence, true); + t->code.set(ID_RRfence, true); + t->code.set(ID_RWfence, true); + t->code.set(ID_WRfence, true); + } + + if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86 + { + msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest); + } + else if( + command == "mfence" || command == "lfence" || command == "sfence") // x86 + { + msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest); } else - dest.destructive_append(tmp_dest); + unknown = true; // give up + + if(x86_32_locked_atomic) + { + goto_programt::targett ae = tmp_dest.add_instruction(ATOMIC_END); + ae->source_location = code.source_location(); + + x86_32_locked_atomic = false; + } + } + + if(unknown) + { + // we give up; we should perhaps print a warning } + else + dest.destructive_append(tmp_dest); } /// removes assembler