mirror of
https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux.git
synced 2026-06-21 15:43:21 +02:00
Eduard Zingerman
256f0071f9
This commit adds basic definitions for cnum32/cnum64.
This is a unified numeric range representation for signed and unsigned
domains. Inspired by an old post from Shung-Hsi Yu [1] and paper [2].
Operations correctness is verified using cbmc model checker,
tests source code can be found in a separate repo [3].
The cnum64_cnum32_intersect() function is notable, because it handled
several cases verifier.c:deduce_bounds_64_from_32() does not.
Given:
- a is a 64-bit range
- b is a 32-bit range
- t is a refined 64-bit range, such that ∀ v ∈ a, (u32)v ∈ b: v ∈ t.
cnum64_cnum32_intersect() makes the following deductions:
(A): 'b' is a sub-range of the first or the last 32-bit
sub-range of 'a':
64-bit number axis --->
N*2^32 (N+1)*2^32 (N+2)*2^32 (N+3)*2^32
||------|---|=====|-------||----------|=====|-------||----------|=====|----|--||
| |< b >| |< b >| |< b >| |
| | | |
|<--+--------------------------- a ---------------------------+--->|
| |
|<-------------------------- t -------------------------->|
(B) 'b' does not intersect with the first of the last 32-bit
sub-range of 'a':
N*2^32 (N+1)*2^32 (N+2)*2^32 (N+3)*2^32
||--|=====|----|----------||--|=====|---------------||--|=====|------------|--||
|< b >| | |< b >| |< b >| |
| | | |
|<-------------+--------- a -------------------|----------->|
| |
|<-------- t ------------------>|
(C) 'b' crosses 0/U32_MAX boundary:
N*2^32 (N+1)*2^32 (N+2)*2^32 (N+3)*2^32
||===|---------|------|===||===|----------------|===||===|---------|------|===||
|b >| | |< b||b >| |< b||b >| | |< b|
| | | |
|<-----+----------------- a --------------+-------->|
| |
|<---------------- t ------------->|
Current implementation of deduce_bounds_64_from_32() only handles
case (A).
[1] https://lore.kernel.org/all/ZTZxoDJJbX9mrQ9w@u94a/
[2] https://jorgenavas.github.io/papers/ACM-TOPLAS-wrapped.pdf
[3] https://github.com/eddyz87/cnum-verif/tree/master
Signed-off-by: Eduard Zingerman <eddyz87@gmail.com>
Link: https://lore.kernel.org/r/20260424-cnums-everywhere-rfc-v1-v3-1-ca434b39a486@gmail.com
Signed-off-by: Alexei Starovoitov <ast@kernel.org>
77 lines
3.1 KiB
Makefile
77 lines
3.1 KiB
Makefile
# SPDX-License-Identifier: GPL-2.0
|
|
obj-y := core.o
|
|
ifneq ($(CONFIG_BPF_JIT_ALWAYS_ON),y)
|
|
# ___bpf_prog_run() needs GCSE disabled on x86; see 3193c0836f203 for details
|
|
cflags-nogcse-$(CONFIG_X86)$(CONFIG_CC_IS_GCC) := -fno-gcse
|
|
endif
|
|
CFLAGS_core.o += -Wno-override-init $(cflags-nogcse-yy)
|
|
|
|
obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o cnum.o log.o token.o liveness.o const_fold.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += bpf_iter.o map_iter.o task_iter.o prog_iter.o link_iter.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += hashtab.o arraymap.o percpu_freelist.o bpf_lru_list.o lpm_trie.o map_in_map.o bloom_filter.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += local_storage.o queue_stack_maps.o ringbuf.o bpf_insn_array.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += bpf_local_storage.o bpf_task_storage.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += fixups.o cfg.o states.o backtrack.o check_btf.o
|
|
obj-${CONFIG_BPF_LSM} += bpf_inode_storage.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += disasm.o mprog.o
|
|
obj-$(CONFIG_BPF_JIT) += trampoline.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += btf.o memalloc.o rqspinlock.o stream.o
|
|
ifeq ($(CONFIG_MMU)$(CONFIG_64BIT),yy)
|
|
obj-$(CONFIG_BPF_SYSCALL) += arena.o range_tree.o
|
|
endif
|
|
obj-$(CONFIG_BPF_JIT) += dispatcher.o
|
|
ifeq ($(CONFIG_NET),y)
|
|
obj-$(CONFIG_BPF_SYSCALL) += devmap.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += cpumap.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += offload.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += net_namespace.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += tcx.o
|
|
endif
|
|
ifeq ($(CONFIG_PERF_EVENTS),y)
|
|
obj-$(CONFIG_BPF_SYSCALL) += stackmap.o
|
|
endif
|
|
ifeq ($(CONFIG_CGROUPS),y)
|
|
obj-$(CONFIG_BPF_SYSCALL) += cgroup_iter.o bpf_cgrp_storage.o
|
|
endif
|
|
obj-$(CONFIG_CGROUP_BPF) += cgroup.o
|
|
ifeq ($(CONFIG_INET),y)
|
|
obj-$(CONFIG_BPF_SYSCALL) += reuseport_array.o
|
|
endif
|
|
ifeq ($(CONFIG_SYSFS),y)
|
|
obj-$(CONFIG_DEBUG_INFO_BTF) += sysfs_btf.o
|
|
endif
|
|
ifeq ($(CONFIG_BPF_JIT),y)
|
|
obj-$(CONFIG_BPF_SYSCALL) += bpf_struct_ops.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += cpumask.o
|
|
# bpf_lsm_proto.o must precede bpf_lsm.o. The current pahole logic
|
|
# deduplicates function prototypes within
|
|
# btf_encoder__add_saved_func() by keeping the first instance seen. We
|
|
# need the function prototype(s) in bpf_lsm_proto.o to take precedence
|
|
# over those within bpf_lsm.o. Having bpf_lsm_proto.o precede
|
|
# bpf_lsm.o ensures its DWARF CU is processed early, forcing the
|
|
# generated BTF to contain the overrides.
|
|
#
|
|
# Notably, this is a temporary workaround whilst the deduplication
|
|
# semantics within pahole are revisited accordingly.
|
|
obj-${CONFIG_BPF_LSM} += bpf_lsm_proto.o bpf_lsm.o
|
|
endif
|
|
ifneq ($(CONFIG_CRYPTO),)
|
|
obj-$(CONFIG_BPF_SYSCALL) += crypto.o
|
|
endif
|
|
obj-$(CONFIG_BPF_PRELOAD) += preload/
|
|
|
|
obj-$(CONFIG_BPF_SYSCALL) += relo_core.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += btf_iter.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += btf_relocate.o
|
|
obj-$(CONFIG_BPF_SYSCALL) += kmem_cache_iter.o
|
|
ifeq ($(CONFIG_DMA_SHARED_BUFFER),y)
|
|
obj-$(CONFIG_BPF_SYSCALL) += dmabuf_iter.o
|
|
endif
|
|
|
|
CFLAGS_REMOVE_percpu_freelist.o = $(CC_FLAGS_FTRACE)
|
|
CFLAGS_REMOVE_bpf_lru_list.o = $(CC_FLAGS_FTRACE)
|
|
CFLAGS_REMOVE_queue_stack_maps.o = $(CC_FLAGS_FTRACE)
|
|
CFLAGS_REMOVE_lpm_trie.o = $(CC_FLAGS_FTRACE)
|
|
CFLAGS_REMOVE_ringbuf.o = $(CC_FLAGS_FTRACE)
|
|
CFLAGS_REMOVE_rqspinlock.o = $(CC_FLAGS_FTRACE)
|