From 3fc6fd5492d86c6ceb7e2adca2b2724a9ffdefbd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 Sep 2022 08:43:17 +0000 Subject: [PATCH] Fix parameter handling in remove_asmt::{gcc,msc}_asm_function_call We did not have any tests that exercised the parameter-requiring cases of inline assembler. Enabling these uncovered that we failed to construct the correct types. In the MSVC case we did not have any support for parameters at all. --- .../cbmc-concurrency/memory_barrier2/msvc.c | 32 +++++++++ .../memory_barrier2/msvc.desc | 11 +++ regression/cbmc-library/__asm_fstcw-01/main.c | 19 +++-- regression/cbmc-library/__asm_fstcw-01/msvc.c | 10 +++ .../cbmc-library/__asm_fstcw-01/msvc.desc | 11 +++ .../cbmc-library/__asm_fstcw-01/test.desc | 2 +- src/assembler/remove_asm.cpp | 69 ++++++++++++++++--- 7 files changed, 139 insertions(+), 15 deletions(-) create mode 100644 regression/cbmc-concurrency/memory_barrier2/msvc.c create mode 100644 regression/cbmc-concurrency/memory_barrier2/msvc.desc create mode 100644 regression/cbmc-library/__asm_fstcw-01/msvc.c create mode 100644 regression/cbmc-library/__asm_fstcw-01/msvc.desc diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.c b/regression/cbmc-concurrency/memory_barrier2/msvc.c new file mode 100644 index 00000000000..b36e9a1be00 --- /dev/null +++ b/regression/cbmc-concurrency/memory_barrier2/msvc.c @@ -0,0 +1,32 @@ +volatile int turn; +int x; +volatile int flag1 = 0, flag2 = 0; + +void *thr1(void *arg) +{ + flag1 = 1; + turn = 1; + __asm { mfence; } + __CPROVER_assume(!(flag2 == 1 && turn == 1)); + x = 0; + __CPROVER_assert(x <= 0, ""); + flag1 = 0; +} + +void *thr2(void *arg) +{ + flag2 = 1; + turn = 0; + __asm { mfence; } + __CPROVER_assume(!(flag1 == 1 && turn == 0)); + x = 1; + __CPROVER_assert(x >= 1, ""); + flag2 = 0; +} + +int main() +{ +__CPROVER_ASYNC_1: + thr1(0); + thr2(0); +} diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.desc b/regression/cbmc-concurrency/memory_barrier2/msvc.desc new file mode 100644 index 00000000000..9327f8de9a5 --- /dev/null +++ b/regression/cbmc-concurrency/memory_barrier2/msvc.desc @@ -0,0 +1,11 @@ +CORE +msvc.c +--mm tso --winx64 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This is the same test as main.c/test.desc, but now using Visual Studio inline +ASM syntax. diff --git a/regression/cbmc-library/__asm_fstcw-01/main.c b/regression/cbmc-library/__asm_fstcw-01/main.c index df3a96dac6a..cc18111668a 100644 --- a/regression/cbmc-library/__asm_fstcw-01/main.c +++ b/regression/cbmc-library/__asm_fstcw-01/main.c @@ -1,9 +1,20 @@ #include -#include +#include int main() { - __asm_fstcw(); - assert(0); - return 0; + unsigned short cw; +#ifdef __GNUC__ + __asm__("fstcw %0" : "=m"(cw)); +#else + __asm { fstcw cw; } +#endif + assert((cw & 0xc00) == 0); + fesetround(FE_UPWARD); +#ifdef __GNUC__ + __asm__("fstcw %0" : "=m"(cw)); +#else + __asm { fstcw cw; } +#endif + assert((cw & 0xc00) == 0x800); } diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.c b/regression/cbmc-library/__asm_fstcw-01/msvc.c new file mode 100644 index 00000000000..11c1cf19932 --- /dev/null +++ b/regression/cbmc-library/__asm_fstcw-01/msvc.c @@ -0,0 +1,10 @@ +int main() +{ + unsigned short cw; + __asm { fstcw cw; } + __CPROVER_assert((cw & 0xc00) == 0, "default rounding mode"); + // fesetround(FE_UPWARD); + __CPROVER_rounding_mode = 2; + __asm { fstcw cw; } + __CPROVER_assert((cw & 0xc00) == 0x800, "round upwards"); +} diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.desc b/regression/cbmc-library/__asm_fstcw-01/msvc.desc new file mode 100644 index 00000000000..0275139a2df --- /dev/null +++ b/regression/cbmc-library/__asm_fstcw-01/msvc.desc @@ -0,0 +1,11 @@ +CORE +msvc.c +--pointer-check --bounds-check --winx64 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This is the same test as main.c/test.desc, but now using Visual Studio inline +ASM syntax. diff --git a/regression/cbmc-library/__asm_fstcw-01/test.desc b/regression/cbmc-library/__asm_fstcw-01/test.desc index 9542d988e8d..96c9b4bcd7b 100644 --- a/regression/cbmc-library/__asm_fstcw-01/test.desc +++ b/regression/cbmc-library/__asm_fstcw-01/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --bounds-check ^EXIT=0$ diff --git a/src/assembler/remove_asm.cpp b/src/assembler/remove_asm.cpp index 6b626d2a646..0d2bab1473c 100644 --- a/src/assembler/remove_asm.cpp +++ b/src/assembler/remove_asm.cpp @@ -17,6 +17,8 @@ Date: December 2014 #include #include +#include +#include #include #include @@ -36,22 +38,26 @@ class remove_asmt void operator()() { for(auto &f : goto_functions.function_map) - process_function(f.second); + process_function(f.first, f.second); } protected: symbol_tablet &symbol_table; goto_functionst &goto_functions; - void process_function(goto_functionst::goto_functiont &); + void process_function(const irep_idt &, goto_functionst::goto_functiont &); void process_instruction( + const irep_idt &function_id, goto_programt::instructiont &instruction, goto_programt &dest); void process_instruction_gcc(const code_asm_gcct &, goto_programt &dest); - void process_instruction_msc(const code_asmt &, goto_programt &dest); + void process_instruction_msc( + const irep_idt &, + const code_asmt &, + goto_programt &dest); void gcc_asm_function_call( const irep_idt &function_base_name, @@ -60,6 +66,7 @@ class remove_asmt void msc_asm_function_call( const irep_idt &function_base_name, + const exprt::operandst &operands, const code_asmt &code, goto_programt &dest); }; @@ -102,7 +109,10 @@ void remove_asmt::gcc_asm_function_call( } } - code_typet fkt_type({}, empty_typet()); + code_typet fkt_type{ + code_typet::parameterst{ + arguments.size(), code_typet::parametert{void_pointer}}, + empty_typet()}; symbol_exprt fkt(function_identifier, fkt_type); @@ -138,23 +148,33 @@ void remove_asmt::gcc_asm_function_call( /// assembly statement /// /// \param function_base_name: Name of the function to call +/// \param operands: Arguments to be passed to function /// \param code: msc-style inline assembly statement to translate to function /// call /// \param dest: Goto program to append the function call to void remove_asmt::msc_asm_function_call( const irep_idt &function_base_name, + const exprt::operandst &operands, const code_asmt &code, goto_programt &dest) { irep_idt function_identifier = function_base_name; + code_function_callt::argumentst arguments; + const typet void_pointer = pointer_type(empty_typet()); - code_typet fkt_type({}, empty_typet()); + for(const auto &op : operands) + arguments.push_back(typecast_exprt::conditional_cast(op, void_pointer)); + + code_typet fkt_type{ + code_typet::parameterst{ + arguments.size(), code_typet::parametert{void_pointer}}, + empty_typet()}; symbol_exprt fkt(function_identifier, fkt_type); - code_function_callt function_call(fkt); + code_function_callt function_call(std::move(fkt), std::move(arguments)); dest.add( goto_programt::make_function_call(function_call, code.source_location())); @@ -185,10 +205,12 @@ void remove_asmt::msc_asm_function_call( /// Translates the given inline assembly code (which must be in either gcc or /// msc style) to non-assembly goto program instructions /// +/// \param function_id: Name of function being processed /// \param instruction: The goto program instruction containing the inline /// assembly statements /// \param dest: The goto program to append the new instructions to void remove_asmt::process_instruction( + const irep_idt &function_id, goto_programt::instructiont &instruction, goto_programt &dest) { @@ -199,7 +221,7 @@ void remove_asmt::process_instruction( if(flavor == ID_gcc) process_instruction_gcc(to_code_asm_gcc(code), dest); else if(flavor == ID_msc) - process_instruction_msc(code, dest); + process_instruction_msc(function_id, code, dest); else DATA_INVARIANT(false, "unexpected assembler flavor"); } @@ -376,9 +398,11 @@ void remove_asmt::process_instruction_gcc( /// Translates the given inline assembly code (in msc style) to non-assembly /// goto program instructions /// +/// \param function_id: Name of function being processed /// \param code: The inline assembly code statement to translate /// \param dest: The goto program to append the new instructions to void remove_asmt::process_instruction_msc( + const irep_idt &function_id, const code_asmt &code, goto_programt &dest) { @@ -450,12 +474,35 @@ void remove_asmt::process_instruction_msc( if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86 { - msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest); + exprt::operandst args{null_pointer_exprt{pointer_type(empty_typet{})}}; + // try to typecheck the argument + if(pos != instruction.size() && instruction[pos].id() == ID_symbol) + { + const irep_idt &name = instruction[pos].get(ID_identifier); + for(const auto &entry : equal_range(symbol_table.symbol_base_map, name)) + { + // global scope symbol, don't replace a local one + if(entry.second == name && args[0].id() != ID_address_of) + { + args[0] = + address_of_exprt{symbol_table.lookup_ref(name).symbol_expr()}; + } + // parameter or symbol in local scope + else if(has_prefix( + id2string(entry.second), id2string(function_id) + "::")) + { + args[0] = address_of_exprt{ + symbol_table.lookup_ref(entry.second).symbol_expr()}; + } + } + } + msc_asm_function_call( + "__asm_" + id2string(command), args, code, tmp_dest); } else if( command == "mfence" || command == "lfence" || command == "sfence") // x86 { - msc_asm_function_call("__asm_" + id2string(command), code, tmp_dest); + msc_asm_function_call("__asm_" + id2string(command), {}, code, tmp_dest); } else unknown = true; // give up @@ -479,8 +526,10 @@ void remove_asmt::process_instruction_msc( /// Replaces inline assembly instructions in the goto function by non-assembly /// goto program instructions /// +/// \param function_id: Name of function being processed /// \param goto_function: The goto function void remove_asmt::process_function( + const irep_idt &function_id, goto_functionst::goto_functiont &goto_function) { bool did_something = false; @@ -490,7 +539,7 @@ void remove_asmt::process_function( if(it->is_other() && it->get_other().get_statement() == ID_asm) { goto_programt tmp_dest; - process_instruction(*it, tmp_dest); + process_instruction(function_id, *it, tmp_dest); it->turn_into_skip(); did_something = true;