This patch adds include/uapi/linux/bcf.h with: - Expression node format: struct bcf_expr { u8 code; u8 vlen; u16 params; u32 args[]; } * code encodes (operation(5 bits)| type (3 bits)). The op first reuses all the bpf encoding, e.g., BPF_ADD/BPF_SUB, and then, extends it with bitvector specific ops, e.g., extract. * args[] holds u32 indices into the same arena (DAG by backwards indices); BV VAL is the only op whose args carry immediates. * params packs op-specific fields; helpers are provided to access bit widths, extract ranges, extension sizes, boolean literal bits. - Proof buffer layout and rule ids: * struct bcf_proof_header { magic=BCF_MAGIC, expr_cnt, step_cnt }. * struct bcf_proof_step { u16 rule; u8 premise_cnt; u8 param_cnt; u32 args[] }; args[] is (premise ids followed by parameters). * Rule classes are ORed into rule (BCF_RULE_CORE/BOOL/BV). This patch is UAPI-only; no kernel behavior change. Signed-off-by: Hao Sun --- include/uapi/linux/bcf.h | 197 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 197 insertions(+) create mode 100644 include/uapi/linux/bcf.h diff --git a/include/uapi/linux/bcf.h b/include/uapi/linux/bcf.h new file mode 100644 index 000000000000..459ad3ed5c6f --- /dev/null +++ b/include/uapi/linux/bcf.h @@ -0,0 +1,197 @@ +/* SPDX-License-Identifier: GPL-2.0 WITH Linux-syscall-note */ +#ifndef _UAPI__LINUX_BCF_H__ +#define _UAPI__LINUX_BCF_H__ + +#include +#include + +/* Expression Types */ +#define BCF_TYPE(code) ((code) & 0x07) +#define BCF_BV 0x00 /* Bitvector */ +#define BCF_BOOL 0x01 /* Boolean */ +#define BCF_LIST 0x02 /* List of vals */ +#define __MAX_BCF_TYPE 0x03 + +#define BCF_OP(code) ((code) & 0xf8) +/* Common Operations */ +#define BCF_VAL 0x08 /* Value/Constant */ +#define BCF_VAR 0x18 /* Variable */ +#define BCF_ITE 0x28 /* If-Then-Else */ + +/* Bitvector Operations */ +#define BCF_SDIV 0xb0 +#define BCF_SMOD 0xd0 +#define BCF_EXTRACT 0x38 /* Bitvector extraction */ +#define BCF_SIGN_EXTEND 0x48 /* Sign extension */ +#define BCF_ZERO_EXTEND 0x58 /* Zero extension */ +#define BCF_BVSIZE 0x68 /* Bitvector size */ +#define BCF_BVNOT 0x78 /* Bitvector not */ +#define BCF_FROM_BOOL 0x88 /* Bool list to Bitvector */ +#define BCF_CONCAT 0x98 /* Concatenation */ +#define BCF_REPEAT 0xa8 /* Bitvector repeat */ + +/* Boolean Operations */ +#define BCF_CONJ 0x00 /* Conjunction (AND) */ +#define BCF_DISJ 0x40 /* Disjunction (OR) */ +#define BCF_NOT 0x80 /* Negation */ +#define BCF_IMPLIES 0x90 /* Implication */ +#define BCF_XOR 0x38 /* Exclusive OR */ +#define BCF_BITOF 0x48 /* Bitvector to Boolean */ + +/* Boolean Literals/Vals */ +#define BCF_FALSE 0x00 +#define BCF_TRUE 0x01 + +/** + * struct bcf_expr - BCF expression structure + * @code: Operation code (operation | type) + * @vlen: Argument count + * @params: Operation parameters + * @args: Argument indices + * + * Parameter encoding by type: + * - Bitvector: [7:0] bit width, except: + * - [15:8] and [7:0] extract `start` and `end` for EXTRACT; + * - [15:8] repeat count for REPEAT; + * - [15:8] extension size for SIGN/ZERO_EXTEND + * - Boolean: + * - [0] literal value for constants; + * - [7:0] bit index for BITOF. + * - List: element type encoding: + * - [7:0] for types; + * - [15:8] for type parameters, e.g., bit width. + */ +struct bcf_expr { + __u8 code; + __u8 vlen; + __u16 params; + __u32 args[]; +}; + +#define BCF_PARAM_LOW(p) ((p) & 0xff) +#define BCF_PARAM_HIGH(p) (((p) >> 8) & 0xff) + +/* Operation-specific parameter meanings */ +#define BCF_BV_WIDTH(p) BCF_PARAM_LOW(p) +#define BCF_EXT_LEN(p) BCF_PARAM_HIGH(p) +#define BCF_EXTRACT_START(p) BCF_PARAM_HIGH(p) +#define BCF_EXTRACT_END(p) BCF_PARAM_LOW(p) +#define BCF_REPEAT_N(p) BCF_PARAM_HIGH(p) +#define BCF_BOOL_LITERAL(p) ((p) & 1) +#define BCF_BITOF_BIT(p) BCF_PARAM_LOW(p) +#define BCF_LIST_TYPE(p) BCF_PARAM_LOW(p) +#define BCF_LIST_TYPE_PARAM(p) BCF_PARAM_HIGH(p) + +/* BCF proof definitions */ +#define BCF_MAGIC 0x0BCF + +struct bcf_proof_header { + __u32 magic; + __u32 expr_cnt; + __u32 step_cnt; +}; + +/** + * struct bcf_proof_step - Proof step + * @rule: Rule identifier (class | rule) + * @premise_cnt: Number of premises + * @param_cnt: Number of parameters + * @args: Arguments (premises followed by parameters) + */ +struct bcf_proof_step { + __u16 rule; + __u8 premise_cnt; + __u8 param_cnt; + __u32 args[]; +}; + +/* Rule Class */ +#define BCF_RULE_CLASS(r) ((r) & 0xe000) +#define BCF_RULE_CORE 0x0000 +#define BCF_RULE_BOOL 0x2000 +#define BCF_RULE_BV 0x4000 + +#define BCF_STEP_RULE(r) ((r) & 0x1fff) + +/* Core proof rules */ +#define BCF_CORE_RULES(FN) \ + FN(ASSUME) \ + FN(EVALUATE) \ + FN(DISTINCT_VALUES) \ + FN(ACI_NORM) \ + FN(ABSORB) \ + FN(REWRITE) \ + FN(REFL) \ + FN(SYMM) \ + FN(TRANS) \ + FN(CONG) \ + FN(TRUE_INTRO) \ + FN(TRUE_ELIM) \ + FN(FALSE_INTRO) \ + FN(FALSE_ELIM) + +#define BCF_RULE_NAME(x) BCF_RULE_##x +#define BCF_RULE_ENUM_VARIANT(x) BCF_RULE_NAME(x), + +enum bcf_core_rule { + BCF_RULE_CORE_UNSPEC = 0, + BCF_CORE_RULES(BCF_RULE_ENUM_VARIANT) + __MAX_BCF_CORE_RULES, +}; + +/* Boolean proof rules */ +#define BCF_BOOL_RULES(FN) \ + FN(RESOLUTION) \ + FN(FACTORING) \ + FN(REORDERING) \ + FN(SPLIT) \ + FN(EQ_RESOLVE) \ + FN(MODUS_PONENS) \ + FN(NOT_NOT_ELIM) \ + FN(CONTRA) \ + FN(AND_ELIM) \ + FN(AND_INTRO) \ + FN(NOT_OR_ELIM) \ + FN(IMPLIES_ELIM) \ + FN(NOT_IMPLIES_ELIM) \ + FN(EQUIV_ELIM) \ + FN(NOT_EQUIV_ELIM) \ + FN(XOR_ELIM) \ + FN(NOT_XOR_ELIM) \ + FN(ITE_ELIM) \ + FN(NOT_ITE_ELIM) \ + FN(NOT_AND) \ + FN(CNF_AND_POS) \ + FN(CNF_AND_NEG) \ + FN(CNF_OR_POS) \ + FN(CNF_OR_NEG) \ + FN(CNF_IMPLIES_POS) \ + FN(CNF_IMPLIES_NEG) \ + FN(CNF_EQUIV_POS) \ + FN(CNF_EQUIV_NEG) \ + FN(CNF_XOR_POS) \ + FN(CNF_XOR_NEG) \ + FN(CNF_ITE_POS) \ + FN(CNF_ITE_NEG) \ + FN(ITE_EQ) + +enum bcf_bool_rule { + BCF_RULE_BOOL_UNSPEC = 0, + BCF_BOOL_RULES(BCF_RULE_ENUM_VARIANT) + __MAX_BCF_BOOL_RULES, +}; + +/* Bitvector proof rules */ +#define BCF_BV_RULES(FN) \ + FN(BITBLAST) \ + FN(POLY_NORM) \ + FN(POLY_NORM_EQ) + +enum bcf_bv_rule { + BCF_RULE_BV_UNSPEC = 0, + BCF_BV_RULES(BCF_RULE_ENUM_VARIANT) + __MAX_BCF_BV_RULES, +}; +#undef BCF_RULE_ENUM_VARIANT + +#endif /* _UAPI__LINUX_BCF_H__ */ -- 2.34.1