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.

Author: tautschnig

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);
+}

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.

regression/cbmc-library/__asm_fstcw-01/main.c

@@ -1,9 +1,20 @@
 #include <assert.h>
-#include <x86_assembler.h>
+#include <fenv.h>
 
 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);
 }

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");
+}

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.

regression/cbmc-library/__asm_fstcw-01/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$

src/assembler/remove_asm.cpp

@@ -17,6 +17,8 @@ Date:   December 2014
 
 #include <util/c_types.h>
 #include <util/pointer_expr.h>
+#include <util/prefix.h>
+#include <util/range.h>
 #include <util/std_code.h>
 #include <util/string_constant.h>
 
@@ -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;