# Copyright 2017 syzkaller project authors. All rights reserved.
# Use of this source code is governed by Apache 2 LICENSE that can be found in the LICENSE file.

# These descriptions rely on binderfs being enabled and creating at least binder0
# and binder1 devices right after a mount.
# "binder,hwbinder,vndbinder" devices are also supported; this is the kconfig default
# and it's what's used on real Android devices (the main user of binder).
# Description assumes CONFIG_ANDROID_BINDER_IPC_32BIT is not set.

include <linux/android/binder.h>
include <linux/fcntl.h>
include <linux/mman.h>
include <linux/net.h>
include <linux/socket.h>
include <uapi/linux/netlink.h>
include <uapi/linux/genetlink.h>

resource fd_binder[fd]
resource binder_ptr[int64]: 0
resource genl_binder_mcgrp_id[int32]

# What's the difference between these node and handle? Do they mean the same?
type binder_node int64[0:3]
type binder_handle int32[0:3]
# Cookies are mostly checked for equality, but in Rust binder they are also
# the keys of freeze listeners, so there should be a few distinct values.
type binder_cookie int64[0:3]

openat$binder(fd const[AT_FDCWD], file ptr[in, string["/dev/binder"]], flags flags[binder_open_flags], mode const[0]) fd_binder
openat$binderfs(fd const[AT_FDCWD], file ptr[in, string[binderfs_devpath]], flags flags[binder_open_flags], mode const[0]) fd_binder
openat$hwbinder(fd const[AT_FDCWD], file ptr[in, string["/dev/hwbinder"]], flags flags[binder_open_flags], mode const[0]) fd_binder
openat$vndbinder(fd const[AT_FDCWD], file ptr[in, string["/dev/vndbinder"]], flags flags[binder_open_flags], mode const[0]) fd_binder

mmap$binder(addr vma, len len[addr], prot const[PROT_READ], flags const[MAP_SHARED], fd fd_binder, offset fileoff) binder_ptr
munmap$binder(addr binder_ptr, len intptr)

ioctl$BINDER_SET_MAX_THREADS(fd fd_binder, cmd const[BINDER_SET_MAX_THREADS], arg ptr[in, int32])
ioctl$BINDER_SET_CONTEXT_MGR(fd fd_binder, cmd const[BINDER_SET_CONTEXT_MGR], arg const[0])
ioctl$BINDER_SET_CONTEXT_MGR_EXT(fd fd_binder, cmd const[BINDER_SET_CONTEXT_MGR_EXT], arg ptr[in, flat_binder_object_t[BINDER_TYPE_BINDER, binder_node]])
ioctl$BINDER_THREAD_EXIT(fd fd_binder, cmd const[BINDER_THREAD_EXIT], arg const[0])
ioctl$BINDER_GET_NODE_DEBUG_INFO(fd fd_binder, cmd const[BINDER_GET_NODE_DEBUG_INFO], arg ptr[inout, binder_node_debug_info])
ioctl$BINDER_WRITE_READ(fd fd_binder, cmd const[BINDER_WRITE_READ], arg ptr[in, binder_write_read])
ioctl$BINDER_GET_NODE_INFO_FOR_REF(fd fd_binder, cmd const[BINDER_GET_NODE_INFO_FOR_REF], arg ptr[inout, binder_node_info_for_ref])
ioctl$BINDER_FREEZE(fd fd_binder, cmd const[BINDER_FREEZE], arg ptr[in, binder_freeze_info])
ioctl$BINDER_GET_FROZEN_INFO(fd fd_binder, cmd const[BINDER_GET_FROZEN_INFO], arg ptr[inout, binder_frozen_status_info])
ioctl$BINDER_ENABLE_ONEWAY_SPAM_DETECTION(fd fd_binder, cmd const[BINDER_ENABLE_ONEWAY_SPAM_DETECTION], arg ptr[in, bool32])
ioctl$BINDER_GET_EXTENDED_ERROR(fd fd_binder, cmd const[BINDER_GET_EXTENDED_ERROR], arg ptr[out, binder_extended_error])
ioctl$BINDER_VERSION(fd fd_binder, cmd const[BINDER_VERSION], arg ptr[out, binder_version])

sendmsg$binder_nlctrl_getfamily(fd sock_nl_generic_init, msg ptr[in, msghdr_netlink[binder_nlctrl_getfamily_msg]], f flags[send_flags])
recvfrom$binder_nlctrl_getfamily(fd sock_nl_generic_init, buf ptr[out, binder_nlctrl_reply], len len[buf], f flags[recv_flags], addr const[0], addrlen const[0])
setsockopt$binder_NETLINK_ADD_MEMBERSHIP(fd sock_nl_generic_init, level const[SOL_NETLINK], opt const[NETLINK_ADD_MEMBERSHIP], arg ptr[in, genl_binder_mcgrp_id], arglen len[arg])
recvfrom$binder_report(fd sock_nl_generic_init, buf ptr[out, binder_report_msg], len len[buf], f flags[recv_flags], addr const[0], addrlen const[0])

openat$binder_debug(fd const[AT_FDCWD], file ptr[in, string[binder_debug_file]], flags const[O_RDONLY], mode const[0]) fd

binder_debug_file = "/sys/kernel/debug/binder/failed_transaction_log", "/sys/kernel/debug/binder/state", "/sys/kernel/debug/binder/stats", "/sys/kernel/debug/binder/transaction_log", "/sys/kernel/debug/binder/transactions"

binder_open_flags = O_RDWR, O_NONBLOCK
_ = __NR_mmap2

binder_freeze_info {
	pid		pid
	enable		bool32
	timeout_ms	int32
}

binder_frozen_status_info {
	pid		pid	(in)
	sync_recv	int32	(out)
	async_recv	int32	(out)
}

binder_node_debug_info {
	ptr		binder_node
	cookie		const[0, int64]
	has_strong_ref	const[0, int32]
	has_weak_ref	const[0, int32]
}

binder_node_info_for_ref {
	handle		binder_handle
	strong_count	const[0, int32]
	weak_count	const[0, int32]
	reserved1	const[0, int32]
	reserved2	const[0, int32]
	reserved3	const[0, int32]
}

binder_write_read {
	write_size	bytesize[write_buffer, int64]
	write_consumed	const[0, int64]
	write_buffer	ptr64[in, array[binder_write_cmd]]
	read_size	bytesize[read_buffer, int64]
	read_consumed	const[0, int64]
# The buffer must be large enough to receive at least BR_TRANSACTION/BR_REPLY.
	read_buffer	ptr64[out, binder_read_buffer, opt]
}

binder_read_buffer [
	transaction		binder_read_tr
	reply			binder_read_reply
	tr_acquire		binder_read_tr_acquire
	tr_increfs_acquire	binder_read_tr_increfs_acquire
]

binder_read_tr {
	noop	const[0, int32]
	cmd	const[0, int32]
	tr	binder_transaction_data_out
	rest	array[int8, 184]
} [packed]

binder_read_reply {
	noop		const[0, int32]
	complete	const[0, int32]
	cmd		const[0, int32]
	tr		binder_transaction_data_out
	rest		array[int8, 180]
} [packed]

binder_read_tr_acquire {
	noop	const[0, int32]
	acquire	array[int8, 20]
	cmd	const[0, int32]
	tr	binder_transaction_data_out
	rest	array[int8, 164]
} [packed]

binder_read_tr_increfs_acquire {
	noop	const[0, int32]
	refs	array[int8, 40]
	cmd	const[0, int32]
	tr	binder_transaction_data_out
	rest	array[int8, 144]
} [packed]

binder_transaction_data_out {
	target		const[0, int64]
	cookie		const[0, int64]
	code		const[0, int32]
	flags		const[0, int32]
	sender_pid	const[0, int32]
	sender_euid	const[0, int32]
	data_size	const[0, int64]
	offsets_size	const[0, int64]
	buffer		binder_ptr
	offsets		const[0, int64]
} [packed]

binder_write_cmd [
	transaction		binder_cmd_transaction
	reply			binder_cmd_reply
	transaction_sg		binder_cmd_transaction_sg
	reply_sg		binder_cmd_reply_sg
	free_buffer		binder_cmd_free_buffer
	increfs			binder_cmd_increfs
	acquire			binder_cmd_acquire
	release			binder_cmd_release
	decrefs			binder_cmd_decrefs
	increfs_done		binder_cmd_increfs_done
	acquire_done		binder_cmd_acquire_done
	register_looper		binder_cmd_register_looper
	enter_looper		binder_cmd_enter_looper
	exit_looper		binder_cmd_exit_looper
	request_death		binder_cmd_request_death
	clear_death		binder_cmd_clear_death
	dead_binder_done	binder_cmd_dead_binder_done
	request_freeze		binder_cmd_request_freeze
	clear_freeze		binder_cmd_clear_freeze
	freeze_done		binder_cmd_freeze_done
] [varlen]

binder_cmd_transaction {
	cmd	const[BC_TRANSACTION, int32]
	data	binder_transaction_data
} [packed]

binder_cmd_reply {
	cmd	const[BC_REPLY, int32]
	data	binder_transaction_data
} [packed]

binder_cmd_transaction_sg {
	cmd		const[BC_TRANSACTION_SG, int32]
	data		binder_transaction_data
	buffers_size	flags[binder_sg_size, int64]
} [packed]

binder_cmd_reply_sg {
	cmd		const[BC_REPLY_SG, int32]
	data		binder_transaction_data
	buffers_size	flags[binder_sg_size, int64]
} [packed]

# NEED: buffers_size should be multiple of 8 and must be no less than size of all BINDER_TYPE_PTR buffers.
binder_sg_size = 0, 64, 1024, 4096, 8192, 16384

binder_transaction_data {
	handle		binder_handle
# there is a union of handle with binder_uintptr_t
	pad		const[0, int32]
	cookie		binder_cookie
	code		int32[0:2]
	flags		flags[binder_transaction_flags, int32]
	sender_pid	const[0, int32]
	sender_euid	const[0, int32]
	data_size	bytesize[buffer, int64]
	offsets_size	bytesize[offsets, int64]
	buffer		ptr64[in, binder_objects]
	offsets		ptr64[in, binder_offsets, opt]
}

binder_objects {
	obj0	binder_root_object
	obj1	binder_object
	obj2	binder_object
} [packed, align[8]]

binder_offsets {
	off0	offsetof[binder_transaction_data:buffer:obj0, int64]
	off1	offsetof[binder_transaction_data:buffer:obj1, int64]
	off2	offsetof[binder_transaction_data:buffer:obj2, int64]
}

binder_transaction_flags = TF_ONE_WAY, TF_ROOT_OBJECT, TF_STATUS_CODE, TF_ACCEPT_FDS, TF_CLEAR_BUF, TF_UPDATE_TXN, TF_DEFER_COMPLETE

binder_root_object [
	flat	flat_binder_object
	fd	binder_fd_object
	ptr	binder_root_buffer_object
	raw_ptr	binder_raw_buffer_object
] [varlen]

binder_object [
	flat		flat_binder_object
	fd		binder_fd_object
	fda		binder_fd_array_object
	ptr		binder_root_buffer_object
	child_ptr	binder_child_buffer_object
	raw_ptr		binder_raw_buffer_object
] [varlen]

flat_binder_object [
	binder		flat_binder_object_t[BINDER_TYPE_BINDER, binder_node]
	weak_binder	flat_binder_object_t[BINDER_TYPE_WEAK_BINDER, binder_node]
	handle		flat_binder_object_t[BINDER_TYPE_HANDLE, binder_handle]
	weak_handle	flat_binder_object_t[BINDER_TYPE_WEAK_HANDLE, binder_handle]
]

type flat_binder_object_t[TYP, DATA] {
	type	const[TYP, int32]
	flags	flags[binder_flat_flags, int32]
	binder	DATA
	cookie	binder_cookie
}

binder_flat_flags = 1, 10, FLAT_BINDER_FLAG_ACCEPTS_FDS, FLAT_BINDER_FLAG_TXN_SECURITY_CTX

binder_fd_object {
	type	const[BINDER_TYPE_FD, int32]
	pad	const[0, int32]
	fd	fd
	pad2	const[0, int32]
	cookie	binder_cookie
}

binder_fd_array_object {
	type		const[BINDER_TYPE_FDA, int32]
	pad		const[0, int32]
	num_fds		int64[1:4]
	parnt		int64[0:1]
	parent_offset	flags[binder_parent_offset, int64]
}

binder_root_buffer_object {
	type		const[BINDER_TYPE_PTR, int32]
	flags		const[0, int32]
	buffer		ptr64[in, array[fd, 2:10]]
	length		bytesize[buffer, int64]
	parnt		const[0, int64]
	parent_offset	const[0, int64]
}

binder_raw_buffer_object {
	type		const[BINDER_TYPE_PTR, int32]
	flags		const[0, int32]
	buffer		ptr64[in, array[int8]]
	length		bytesize[buffer, int64]
	parnt		const[0, int64]
	parent_offset	const[0, int64]
}

binder_child_buffer_object {
	type		const[BINDER_TYPE_PTR, int32]
	flags		const[BINDER_BUFFER_FLAG_HAS_PARENT, int32]
	buffer		ptr64[in, array[fd, 2:10]]
	length		bytesize[buffer, int64]
	parnt		int64[0:1]
	parent_offset	flags[binder_parent_offset, int64]
}

binder_parent_offset = 0, 8, 16, 24

binder_cmd_free_buffer {
	cmd	const[BC_FREE_BUFFER, int32]
	ptr	binder_ptr
} [packed]

binder_cmd_increfs {
	cmd	const[BC_INCREFS, int32]
	ref	binder_handle
} [packed]

binder_cmd_acquire {
	cmd	const[BC_ACQUIRE, int32]
	ref	binder_handle
} [packed]

binder_cmd_release {
	cmd	const[BC_RELEASE, int32]
	ref	binder_handle
} [packed]

binder_cmd_decrefs {
	cmd	const[BC_DECREFS, int32]
	ref	binder_handle
} [packed]

binder_cmd_increfs_done {
	cmd	const[BC_INCREFS_DONE, int32]
	ptr	binder_node
	cookie	binder_cookie
} [packed]

binder_cmd_acquire_done {
	cmd	const[BC_ACQUIRE_DONE, int32]
	ptr	binder_node
	cookie	binder_cookie
} [packed]

binder_cmd_register_looper {
	cmd	const[BC_REGISTER_LOOPER, int32]
} [packed]

binder_cmd_enter_looper {
	cmd	const[BC_ENTER_LOOPER, int32]
} [packed]

binder_cmd_exit_looper {
	cmd	const[BC_EXIT_LOOPER, int32]
} [packed]

binder_cmd_request_death {
	cmd	const[BC_REQUEST_DEATH_NOTIFICATION, int32]
	handle	binder_handle
	cookie	binder_cookie
} [packed]

binder_cmd_clear_death {
	cmd	const[BC_CLEAR_DEATH_NOTIFICATION, int32]
	handle	binder_handle
	cookie	binder_cookie
} [packed]

binder_cmd_dead_binder_done {
	cmd	const[BC_DEAD_BINDER_DONE, int32]
	cookie	binder_cookie
} [packed]

binder_cmd_request_freeze {
	cmd	const[BC_REQUEST_FREEZE_NOTIFICATION, int32]
	handle	binder_handle
	cookie	binder_cookie
} [packed]

binder_cmd_clear_freeze {
	cmd	const[BC_CLEAR_FREEZE_NOTIFICATION, int32]
	handle	binder_handle
	cookie	binder_cookie
} [packed]

binder_cmd_freeze_done {
	cmd	const[BC_FREEZE_NOTIFICATION_DONE, int32]
	cookie	binder_cookie
} [packed]

binder_version {
	protocol_version	int32
}

binder_extended_error {
	id	int32
	command	int32
	param	int32
}

binder_nlctrl_getfamily_msg {
	len	len[parent, int32]
	type	const[GENL_ID_CTRL, int16]
	flags	const[NLM_F_REQUEST, int16]
	seq	const[0, int32]
	pid	const[0, int32]
	hdr	genlmsghdr_t[CTRL_CMD_GETFAMILY]
	attr	nlattr[CTRL_ATTR_FAMILY_NAME, string["binder"]]
} [packed, align[4]]

binder_nlctrl_reply {
	hdr		array[int8, 76]
	mcgrp_id	genl_binder_mcgrp_id
	rest		array[int8, 48]
} [packed]

# Offsets assume a 4-7 char context name (e.g. "binder", "binder0", "custom0");
# to_pid is present at offset 60 when the failed transaction had a target proc.
binder_report_msg {
	hdr		array[int8, 44]
	from_pid	pid
	mid		array[int8, 12]
	to_pid		pid
	rest		array[int8, 64]
} [packed]
