# HG changeset patch
# User Paul Boddie <paul@boddie.org.uk>
# Date 1663337308 -7200
# Node ID bd893bc43d7c1b10625b8c7f5585a3ad1ce2df0a
# Parent  fed02d483493d1ebda41f9aa92e2bd5b8024d1c4
Using opcode_type to work around L4Re dataspace IPC issues on 32-bit platforms.
This reserves a 64-bit area for the opcode, even though only the first message
word will be used to obtain the opcode, but it allows the operands to be found
at the appropriate place. On 64-bit platforms, there remains a risk of opcodes
being misinterpreted since the message word for the opcode will be interpreted
as a 64-bit quantity, but if the upper half of that word is not initialised
correctly, it will cause a bad opcode to be found.

diff -r fed02d483493 -r bd893bc43d7c libsystypes/idl/dataspace.idl
--- a/libsystypes/idl/dataspace.idl	Fri Sep 16 15:24:38 2022 +0200
+++ b/libsystypes/idl/dataspace.idl	Fri Sep 16 16:08:28 2022 +0200
@@ -6,9 +6,10 @@
 [protocol(L4RE_PROTO_DATASPACE)]
 interface Dataspace
 {
-  /* Map memory within a dataspace. */
+  /* Map memory within a dataspace.
+     NOTE: Using opcode_type to work around L4Re dataspace IPC issues. */
 
-  [opcode(0)] void map(in offset_t offset, in map_address_t hot_spot,
+  [opcode(0),opcode_type(l4_uint64_t)] void map(in offset_t offset, in map_address_t hot_spot,
                        in map_flags_t flags, out fpage region);
 
   /* Clear a dataspace. */