Merge pull request #7932 from tautschnig/cleanup/asm-library

C library: ASM functions take void* pointers

Author: tautschnig

Diff for: .github/workflows/build-and-test-Xen.yaml

@@ -62,3 +62,9 @@ jobs:
 
       - name: Check for goto-cc section in xen-syms binary
         run: objdump -h xen_4_13/xen/xen-syms | grep "goto-cc"
+
+      - name: Show goto-cc properties
+        run:  $(pwd)/src/cbmc/cbmc --show-properties xen_4_13/xen/xen-syms
+
+      - name: Show some goto-cc functions
+        run:  $(pwd)/src/cbmc/cbmc --list-goto-functions xen_4_13/xen/xen-syms | grep "arch"

Diff for: src/ansi-c/library/x86_assembler.c

@@ -3,30 +3,30 @@
 
 extern int __CPROVER_rounding_mode;
 
-void __asm_fnstcw(unsigned short *dest)
+void __asm_fnstcw(void *dest)
 {
   // the rounding mode is bits 10 and 11 in the control word
-  *dest=__CPROVER_rounding_mode<<10;
+  *(unsigned short *)dest = __CPROVER_rounding_mode << 10;
 }
 
 /* FUNCTION: __asm_fstcw */
 
 extern int __CPROVER_rounding_mode;
 
-void __asm_fstcw(unsigned short *dest)
+void __asm_fstcw(void *dest)
 {
   // the rounding mode is bits 10 and 11 in the control word
-  *dest=__CPROVER_rounding_mode<<10;
+  *(unsigned short *)dest = __CPROVER_rounding_mode << 10;
 }
 
 /* FUNCTION: __asm_fldcw */
 
 extern int __CPROVER_rounding_mode;
 
-void __asm_fldcw(const unsigned short *src)
+void __asm_fldcw(void *src)
 {
   // the rounding mode is bits 10 and 11 in the control word
-  __CPROVER_rounding_mode=((*src)>>10)&3;
+  __CPROVER_rounding_mode = ((*(const unsigned short *)src) >> 10) & 3;
 }
 
 /* FUNCTION: __asm_mfence */

Diff for: src/assembler/remove_asm.cpp

@@ -68,6 +68,7 @@ class remove_asmt
   void gcc_asm_function_call(
     const irep_idt &function_base_name,
     const code_asm_gcct &code,
+    std::size_t n_args,
     goto_programt &dest);
 
   void msc_asm_function_call(
@@ -83,10 +84,12 @@ class remove_asmt
 /// \param function_base_name: Name of the function to call
 /// \param code: gcc-style inline assembly statement to translate to function
 ///   call
+/// \param n_args: Number of arguments required by \p function_base_name
 /// \param dest: Goto program to append the function call to
 void remove_asmt::gcc_asm_function_call(
   const irep_idt &function_base_name,
   const code_asm_gcct &code,
+  std::size_t n_args,
   goto_programt &dest)
 {
   irep_idt function_identifier = function_base_name;
@@ -115,6 +118,16 @@ void remove_asmt::gcc_asm_function_call(
     }
   }
 
+  // An inline asm statement may consist of multiple commands, not all of which
+  // use all of the inputs/outputs of the inline asm statement.
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    arguments.size() >= n_args,
+    "insufficient number of arguments for calling " +
+      id2string(function_identifier),
+    "required arguments: " + std::to_string(n_args),
+    code.pretty());
+  arguments.resize(n_args);
+
   code_typet fkt_type{
     code_typet::parameterst{
       arguments.size(), code_typet::parametert{void_pointer}},
@@ -139,9 +152,12 @@ void remove_asmt::gcc_asm_function_call(
   }
   else
   {
-    DATA_INVARIANT(
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
       symbol_table.lookup_ref(function_identifier).type == fkt_type,
-      "function types should match");
+      "types of function " + id2string(function_identifier) + " should match",
+      code.pretty(),
+      symbol_table.lookup_ref(function_identifier).type.pretty(),
+      fkt_type.pretty());
   }
 }
 
@@ -299,12 +315,12 @@ void remove_asmt::process_instruction_gcc(
 
     if(command == "fstcw" || command == "fnstcw" || command == "fldcw") // x86
     {
-      gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
+      gcc_asm_function_call("__asm_" + id2string(command), code, 1, tmp_dest);
     }
     else if(
       command == "mfence" || command == "lfence" || command == "sfence") // x86
     {
-      gcc_asm_function_call("__asm_" + id2string(command), code, tmp_dest);
+      gcc_asm_function_call("__asm_" + id2string(command), code, 0, tmp_dest);
     }
     else if(command == ID_sync) // Power
     {