aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-01-27 16:57:20 +0100
committerXavier Leroy <xavier.leroy@inria.fr>2015-01-27 16:57:20 +0100
commite096fa7aa6161e1f5a74001185eb3873a684c48d (patch)
treeca928bcb3f7b6b2237a626fbb1dbc1ce62b2e5d1 /ia32
parentf00b70b6a17fdfb4e8606df891f6becc8102ef12 (diff)
downloadcompcert-e096fa7aa6161e1f5a74001185eb3873a684c48d.tar.gz
compcert-e096fa7aa6161e1f5a74001185eb3873a684c48d.zip
ABI compatibility for struct/union function arguments passed by value.
The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
Diffstat (limited to 'ia32')
-rw-r--r--ia32/PrintAsm.ml17
1 files changed, 14 insertions, 3 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index b0ef0180..2ffd5600 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -844,8 +844,10 @@ let print_instruction oc = function
| Pjmp_l(l) ->
fprintf oc " jmp %a\n" label (transl_label l)
| Pjmp_s(f, sg) ->
+ assert (not sg.sig_cc.cc_structret);
fprintf oc " jmp %a\n" symbol f
| Pjmp_r(r, sg) ->
+ assert (not sg.sig_cc.cc_structret);
fprintf oc " jmp *%a\n" ireg r
| Pjcc(c, l) ->
let l = transl_label l in
@@ -861,11 +863,20 @@ let print_instruction oc = function
fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r;
jumptables := (l, tbl) :: !jumptables
| Pcall_s(f, sg) ->
- fprintf oc " call %a\n" symbol f
+ fprintf oc " call %a\n" symbol f;
+ if sg.sig_cc.cc_structret then
+ fprintf oc " pushl %%eax\n"
| Pcall_r(r, sg) ->
- fprintf oc " call *%a\n" ireg r
+ fprintf oc " call *%a\n" ireg r;
+ if sg.sig_cc.cc_structret then
+ fprintf oc " pushl %%eax\n"
| Pret ->
- fprintf oc " ret\n"
+ if (!current_function_sig).sig_cc.cc_structret then begin
+ fprintf oc " movl 0(%%esp), %%eax\n";
+ fprintf oc " ret $4\n"
+ end else begin
+ fprintf oc " ret\n"
+ end
(** Pseudo-instructions *)
| Plabel(l) ->
fprintf oc "%a:\n" label (transl_label l)