From patchwork Wed Nov 8 05:46:05 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449558 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 70B0DCA53 for ; Wed, 8 Nov 2023 05:46:36 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="g3fSb1U5" Received: from EUR01-VE1-obe.outbound.protection.outlook.com (mail-ve1eur01on2058.outbound.protection.outlook.com [40.107.14.58]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 9E4AE1705 for ; Tue, 7 Nov 2023 21:46:35 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=BAecFQFqxqq5d5D4U5IMcWEN74UQd4Cea0ufDyrrVIQq+pqKymEY496WBomS5hdCH8pzNuhiN/vS7N1isZggd2YfVP+dIY8Asx8QOIxTrOtfnyeLF2Kqe6+/sLAyHTysFgkpsA9NAbz5SmiBDOXYHCX4yvE4YLz7s4sXE+Pm6UJF0dbrwh0FyQBEmnznqKosw2i0Jg4G/SvUHzuJECYYyZ8/uO2/V9VswYzjRmwWzW8cKFhym9zQNyVc2rDi5OxyvxWmncH1fOGaQ1kPd8rYpmqGfwuS+j9LvleBRPiEG+u+Zvo3Iu/8WRz4whrkHAjNzIfwIRXlgaUgwoVd3p0S9w== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=GgaCkVBn3tbc1sqI3PQQfarsGRTX0VDCdSUjPFEIu0A=; b=FIROwvQpgK/AG0JTVaACVZxxIKZNEeGfL2Qj1nYahfwbsKzj2Az6pea1qUM6Cx8zInl/VOKF+d1XU9ExsjuEA1vccDQAaWxtuhJfVscBb2cIFLL3UtIgGISxqBlo7CFlwQUoej3mk9ntIvkJWRmu/g5EkGSD+woE6eSPl9lfYFUQxRmrlGQzTJ+K9zHFXoOxkeokiYIFLuST68IR0wU5sWIMbxbXOhehWkqb/DbCew8ftkDHvPjdOC2HFWf8uRG1FQasLao38qPKzFg/DHQYVyM3QIzPHgYiH96RfgYMPc24N5vvTGPmWDlYyTwC++jDWsr3aK/P2PyZmVEszyRxxQ== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=GgaCkVBn3tbc1sqI3PQQfarsGRTX0VDCdSUjPFEIu0A=; b=g3fSb1U5658K30tW5fzONZ7D33K2iE1sfO1hO5JvdRX4/LfI/yqHl2vEmQIiT+FDfbZjkIqPsvQ7S/mBi7Ebdj0PTxyJ1OuPwZLdNVH++drdN4wApbi99Td8Ww40531unABQBjZnwabDms4pfEqBluLf9wu7v6NEWneKN8ZtShrAPnpNSa6KYrOoSTWXl/gbxQfBdp+9VF6NH+/pA4/CB8xgXHrPIJMXTvuRo3HuTe2gmAUo4dZD6ByC4A6liDo6IC8k2IGgUbHIAnvTsMpVd9d6bSyVeryPLg6FgYivYhpfM83o595oe0e7xfRKPkDqRD+pKpAv0EZmT8BsrjGWjw== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by PA4PR04MB9568.eurprd04.prod.outlook.com (2603:10a6:102:26e::6) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.18; Wed, 8 Nov 2023 05:46:32 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:46:30 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 1/7] Add inital wrange32 definition along with checks for umin/umax Date: Wed, 8 Nov 2023 13:46:05 +0800 Message-ID: <20231108054611.19531-2-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0275.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:3c9::17) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|PA4PR04MB9568:EE_ X-MS-Office365-Filtering-Correlation-Id: 79cba5e4-e019-4a88-3a1b-08dbe01e0e75 X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: eCVSR+aGd0hO6QUHngRxePgMNJPQ8QGJeuWBjGCwUqDwh/ye98Wae1KZnMvCPK6XSFraM+EZziUO2JiEw0/8UBimzMLtLK5hH7xuxJk0aFZryiX7FXKkvbi1uq+AW11wkchPdZzFu+yf04r5+hPKAbWcqrU0yyCFNlyIyLBgQbSKwt3M5sVpbQHvcTXlR8eR2pMKpBX9a0h4jnZfQS5SQf5+N64jnckon4yR1XLjoXmuYv+q03KJR7ilcJ8BXbE4AbzAxRfsOakS5j51Aj8Hofl/T3M7zTdocfqukBu4r7DZrKRd85gKqXJ6wEFamFEjQDsVNe1fwwLCRKLQYXWxHDTi4YevqGFI1jbczPaJvwFSvO4T9RzOTwCZeRj2hHpsa05WMwVtSOxe8RSKrlI+6JI2bz/BvItGIuvy+Dbt4Qn8A2Q6jOCJ2FmguitRQqpoy7zDXX78YlYLGPp42Otfz+GzVQ60e6YIZ7MFl/Z6uIrQo9EbEknL+oCfWqL8cQYiqFiYVZtUjPU8C/wHpw1zSMv32wueyCFzn4bepso4BrkPco0loqhLggYZX2gTZceB X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(136003)(346002)(376002)(39860400002)(396003)(366004)(230922051799003)(64100799003)(186009)(451199024)(1800799009)(6916009)(316002)(54906003)(66476007)(66946007)(66556008)(478600001)(6486002)(6666004)(86362001)(5660300002)(41300700001)(36756003)(2906002)(8936002)(4326008)(8676002)(2616005)(1076003)(6506007)(6512007)(38100700002);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: 6Nkw+sSsIo9XUm34ZLSn2o2UJI/0JPCoL3cIvmgtxhya9tGzLc4psLA4EtGdh5G1pt35Wc6hR+45/3OXixMCNJ8Wj/XKiJ0ZfOVq7aS5S0cUa1wXgC+X/gPSCVYHS6Z3c2xBO6B8OXmXbFrF01afj85FbE7kg6nlsSJno2EU9jhbwxYL6aan8ou1QR1CqXhcHb1HmQEwNjBEUsKJ9nj10mLobDPSXB0aNidaBf+/AB6PUE4N2PANcLX625Q/X4hK66MYskINDoK+oaEI4G8ndZNrgFNonqlJiQ4BzHeVcIz5a5z1l7Tx2vpUjHXqicZXA7VA5YLpIydJhqBuzMKi//xB0JUxMf5YQl0zt2OqP6OQzAVQHY+9CoXFyT3hFYRjJSBeSImtknEceumPvEuAvet0y9+7I3bjOyVPg/L3T6OZoKvGougmuIjA7f1aWPvT0WznPfHi96EXZgIdbfJvf9roZfwyRKk4Fx4CLV5HRryOQv40Jo/cEfLL2Fqo9GVtMrrHhcbO8wnLaRwXu6pWUr1vG8hSz4MMxo5eOCf/MTdpvdHepwLoE9qlOerrSAQ2OFtOP3OR/rB+HpVXg+VviLAlVNSkEMmEOZwuDj7XjAunnBGgU87sJ8xjWCPFoqexv862S4cv4OCBwWw1osVOdMPbC07y1xEUOX/KLFritGoQEWKcgZ8sFDzBAOUWyarrp6q9y4L6LV+d+uKUKdxUWRc10EMxSnVpsW2EduOdkFu7LmhhPCyl/YtCEXuspb2El4BKOT8FjOgadMI7mo0gOC/bKajzDx/V/lm5RCS2zam6M1Suy5Vdv/0+rHeovJMESIie/+8Nae1kvH6mkgsL/gJqSwuBTiCekKlT7GYlqMWvaUf0uLpxXLKj7ExeBjO4y2s35VKfC6rjAqTRQKHzU8wJbF9k7NBoCnyMZtfFsk4XfmIiNpFT9lity9WtQJ988PWEp55BIguOfwTvQXSDAwk2tYEsaKX6ge1dIzTbz4c8IKsH0sKn/hNzhteG0nxLxsK7lmbmaEs+zEhVSlrwkuyBuNxHTM+HDCRSFuDAAmlVRo3Mp2lLLGYqL+PvQbPVq8SoI2xIjBeDQ4NInN1I5O3DnxtXkjaX60iq9Ir1FPw1yHGZ3Ptl+P0+Q/klJUzDIIyano/2C7L5QD8E9l8KGEqbBD/RW6QuPTmJicZWMv9WpgISxRFJ716xNHoVCIfTeFISrDB+XKhoyEHkjAxWmLDKgDtwgvhlo1shKvHOwKb44s/v3R6ZRGUc3wc4Zlm5+6sY/Tg14yx/e1Gir4O8gaUCZ4ZSy2KLvQY6F04GTO6sgqcmO+z8wrtFKLMkjxesePwaIhuERJniJ6e4SBLRpuTdAIHL2FvkzJJrdPH8Ku1A/s6lFUxH8X2O0UULwc5H1Bxef4OMpOxBShml0cR2a/G9TFx/2rpiuGyVW3pWBELFWe0/b8BBHmZ/ef4gMrTlRtDrPDcE8dE4El6MeC9hE4gyHb3o1ocpIoah7CmwUMYGxvMjtpS0S5m9nfpajTMpVdkMzfNRHvRY4xjAOUeuvLunSgptr1lJeathHgw+seMxwH/rvLceJ8BrYPpHf+ZYGDdMyJPBamP8s8Yyh02RQ68inpi4UdgsU9kgVc3SfNUFKBLg5KROe08DgCx8zj99/1MNYfHjyBxI36gHgk9diw== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: 79cba5e4-e019-4a88-3a1b-08dbe01e0e75 X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:46:30.2412 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: eWxT4eecBsTK/s0ccXiu1eretsRk5cc1IW9D95xZgKqrEz/knai3UzdyiH3gtm6DvnEdB1kvg2AEIYwUWSAnjg== X-MS-Exchange-Transport-CrossTenantHeadersStamped: PA4PR04MB9568 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC Add struct wrange32 (short for "32-bit wrapped range") and umin/umax helpers, the latter simply return start/end at the moment. We call the fields start and end instead of umin and umax, because later patch will lift the umin <= umax requirement, so we can have cases where umax < umin; and continuing to call them umin/umax would be confusing. A struct wrange32 modeled with z3Py is also attached to show that wrange32 in its current form work as intended. Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 26 ++++ tools/testing/selftests/bpf/formal/wrange.py | 150 +++++++++++++++++++ 2 files changed, 176 insertions(+) create mode 100644 include/linux/wrange.h create mode 100755 tools/testing/selftests/bpf/formal/wrange.py diff --git a/include/linux/wrange.h b/include/linux/wrange.h new file mode 100644 index 000000000000..e2316c7bbb2d --- /dev/null +++ b/include/linux/wrange.h @@ -0,0 +1,26 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +#ifndef _LINUX_WRANGE_H +#define _LINUX_WRANGE_H + +#include + +struct wrange32 { + /* Start with a usual u32 min/max. + * + * Requiring umin/start <= umax/end, and cannot be use to track s32 + * range. + */ + u32 start; /* umin */ + u32 end; /* umax */ +}; + +/* Helper functions that will be required later */ +static inline u32 wrange32_umin(struct wrange32 a) { + return a.start; +} + +static inline u32 wrange32_umax(struct wrange32 a) { + return a.end; +} + +#endif /* _LINUX_WRANGE_H */ diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py new file mode 100755 index 000000000000..8836f4cbbedb --- /dev/null +++ b/tools/testing/selftests/bpf/formal/wrange.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +import abc +from z3 import * + + +# Helpers +BitVec32 = lambda n: BitVec(n, bv=32) +BitVecVal32 = lambda v: BitVecVal(v, bv=32) + +class Wrange(abc.ABC): + SIZE = None # Bitwidth, this will be defined in the subclass + name: str + start: BitVecRef + end: BitVecRef + + def __init__(self, name, start=None, end=None): + self.name = name + self.start = BitVec(f'Wrange32-{name}-start', bv=self.SIZE) if start is None else start + assert(self.start.size() == self.SIZE) + self.end = BitVec(f'Wrange32-{name}-end', bv=self.SIZE) if end is None else end + assert(self.end.size() == self.SIZE) + + def wellformed(self): + # start <= end + return ULE(self.start, self.end) + + @property + def umin(self): + return self.start + + @property + def umax(self): + return self.end + + # Not used in wrange.c, but helps with checking later + def contains(self, val: BitVecRef): + assert(val.size() == self.SIZE) + # umin <= val <= umax + return And(ULE(self.umin, val), ULE(val, self.umax)) + + +class Wrange32(Wrange): + SIZE = 32 # Working with 32-bit integers + + +__all__ = [ + 'Wrange', + 'Wrange32', + 'BitVec32', + 'BitVecVal32', +] + + +def main(): + # A random 32-bit integer called x, that can be of any possible value + # unless constrained + x = BitVec32('x') + + w1 = Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(1)) + print(f'Given w1 start={w1.start} end={w1.end}') + print('\nChecking w1 is wellformed') + prove( + w1.wellformed(), + ) + print('\nChecking w1.umin is 1') + prove( + w1.umin == BitVecVal32(1), + ) + print('\nChecking w1.umax is 1') + prove( + w1.umax == BitVecVal32(1), + ) + print('\nChecking that w1 contains 1') + prove( + w1.contains(BitVecVal32(1)), + ) + print('\nChecking that w1 is a set of {1}, with only one element') + prove( + w1.contains(x) == (x == BitVecVal32(1)), + ) + + w2 = Wrange32('w2', start=BitVecVal32(2), end=BitVecVal32(2**32 - 1)) + print(f'\nGiven w2 start={w2.start} end={w2.end}') + print('\nChecking w2 is wellformed') + prove( + w2.wellformed(), + ) + print('\nChecking w2.umin is 2') + prove( + w2.umin == BitVecVal32(2), + ) + print('\nChecking w2.umax is 2**32-1') + prove( + w2.umax == BitVecVal32(2**32 - 1), + ) + print('\nChecking that w2 contains 2**32 - 1') + prove( + w2.contains(BitVecVal32(2**32 - 1)), + ) + print('\nChecking that w2 does NOT contains 1') + prove( + Not(w2.contains(BitVecVal32(1))), + ) + print('\nChecking that w2 is a set of {2..2**32-1}') + prove( + # Contrain x such that 2 <= x <= 2**32-1 and check that if x between 2 + # and 2**32-1 (inclusive), then w2.contains(x) will return true. + # + # In addition to that, check that the reverse is also true. That is if + # x it _not_ a value between 2 and 2**32-1, then w2.contains(x) will + # return false. + w2.contains(x) == And(ULE(BitVecVal32(2), x), ULE(x, BitVecVal32(2**32-1))), + ) + + # Right now our semantic doesn't allow umax/end < umin/start + w3 = Wrange32('w3', start=BitVecVal32(2), end=BitVecVal32(0)) + print(f'\nGiven w3 start={w3.start} end={w3.end}') + print('\nChecking w3 is NOT wellformed') + prove( + Not(w3.wellformed()), + ) + + # General checks that does not assum the value of start/end, except that it + # meets the requirement that start <= end. + w = Wrange32('w') # Given a Wrange32 called w + x = BitVec32('x') # And an 32-bit integer x (redeclared for clarity) + print(f'\nGiven any possible Wrange32 called w, and any possible 32-bit integer called x') + print('\nChecking if w.contains(x) == True, then w.umin <= (u32)x is also true') + prove( + Implies( + And( + w.wellformed(), + w.contains(x), + ), + ULE(w.umin, x), + ) + ) + print('\nChecking if w.contains(x) == True, then (u32)x <= w.umax is also true') + prove( + Implies( + And( + w.wellformed(), + w.contains(x), + ), + ULE(x, w.umax), + ) + ) + +if __name__ == '__main__': + main() From patchwork Wed Nov 8 05:46:06 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449559 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 28948CA60 for ; Wed, 8 Nov 2023 05:46:41 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="eh2Pfb0+" Received: from EUR01-VE1-obe.outbound.protection.outlook.com (mail-ve1eur01on2052.outbound.protection.outlook.com [40.107.14.52]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 8FD561705 for ; Tue, 7 Nov 2023 21:46:40 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=iAurLDoUG3s7uaAcTtVZgfaKFEtwUSsR2IRSuSlD++7vjq32oqOcrygNPLT5NcdAfocmeDAX8dXxTv/dDtng0ZnAu84ypi3ASD0dFO6k7Je6o0VUDXVA0zqNDPBcNDvP49tmDfdrmEoWSYaYfG57geOd1cuPPlTycvr+/aW/rwuwSYKSi3MXwrRn95S68a98DzUHNpCunWC4rHw3G3/Nm//0IdrWA3gGjnxiWiLWxFvX5VP1D0s2zcmvRaj+Fvu/sAG6VUET7WlYkbV4FtrtV38GXfZEqAFzPl51UqyrWN4ugF0MZCS+8ESybifmDVLXeL/jKzJaBrWdOziF8Ub5JA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=DZcDmYTio3JzCp/LgxrHZ77IPmzXRlwzqLj39Rq+ISs=; b=gPPehk2rmSUqN1qsrjVEAVeBuykaGbNV9blnN8Fr03nbT0RsFNn+iOCCKF5pI9M99B8BCHNI1Cj0xe2xnTsk1iBFVVOJrKdomr7IXk6Lu8obhX+5zYOcPKrBxZQGy/kZhWVOdpQNAcekfRW4coO/aPWASG9B6EG4w02wSb7rrBlYsJwJmLnMadjAIvyxhLpSASPRqhOwLkvUSd4ea6haHr8xxvwJjY4ar4QA+W927wc36J43HAEYIYVty3dpClcyMXG2n+OZpKbi4Etay+f4ZmBRF9FJknNzKkLFzjQa6dsTdR9cpCrHrb0nOQOzhFW2CYkhxtg+/78oFAaV5O8vBw== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=DZcDmYTio3JzCp/LgxrHZ77IPmzXRlwzqLj39Rq+ISs=; b=eh2Pfb0+KpPYnQ5tJDw63k1tW5G+sWj/qtMVgT5nNOUcH8UjELOysEfqoiUO56fjik3T9sQCW4LErPHgDPxC8kIxbi49/HsYcxwskjwCgMve8tawUQnMvJ/5sntpcqJeWN6TMsy7GsaiSW3YT0ONY58dDVmtn6Ymm2/TUYetN5lWc8RohXYHICbIBzpoaRqamd1X08KqWi0JoU8aGROr4GsshRLGDnW0W1R9l6zR6BrnSFfiP5l0fAO/C2JduxnGCtfOPATCMl6ZdCVOMhXZUzOawdICy6d0D1ooSYbdqJGXzk9KAd3nP2es94f7APUg1cL8gDHL/45p5x5VQx99iw== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by PA4PR04MB9568.eurprd04.prod.outlook.com (2603:10a6:102:26e::6) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.18; Wed, 8 Nov 2023 05:46:38 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:46:38 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 2/7] Lift the contrain requiring start <= end Date: Wed, 8 Nov 2023 13:46:06 +0800 Message-ID: <20231108054611.19531-3-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0283.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:3c9::11) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|PA4PR04MB9568:EE_ X-MS-Office365-Filtering-Correlation-Id: c6ba97a5-9c08-4672-e1bd-08dbe01e12e8 X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: XRvyOZAyKn5jsFVHQuct1PhsEu5JWQV74n/V4UB9EnIlw7+0nv/0bqMU3DjmWzjuC8nT41fy/SV/WtWeLHCQLBrsi58Z8iqsmuYc1xQhKuwVFWTFMX6X9+rtNQHBhImdhWY+dbVJZY9MiKAUjZHd197pPx5MhNJe9ItXazAwDGLpWtaI1Ywf0+9PwkFUDTOa2Nv0fvps5+5EIz0rZkwmwRGeLpfdNvmO2R4n593BqEzbh2z2T04Lp4vklgOsndN8FnbY1dpzBzE/NfdERDc2nPkeR1ENuNXs2iJVFmHy1vt48NgpulKqwlWxXWGCOndW0dx1AuiQ/xM3F2XrQTyd+LSXvWs3RgvN0Uq+D8NFmcDzIu3kit7yOs1HYW8Ku+k8v6QTtzepvjoOHu812++NwVj79JRMHgBiJsgwUaROXUVKq4YWuwo28XOwIRw0negxrHUjE/oagP4TSN6lRRaAA50l6+29lQAH74vP9i4SpbJfnU4ibDMIhkfRmzWYBpBJ+JIipNzjVDJdJ+mcMmghyjxChQZJlWQ3BjHkrDclD+izDbisev/G6phbkikg3t8F X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(136003)(346002)(376002)(39860400002)(396003)(366004)(230922051799003)(64100799003)(186009)(451199024)(1800799009)(6916009)(316002)(54906003)(66476007)(66946007)(66556008)(478600001)(6486002)(6666004)(86362001)(5660300002)(41300700001)(36756003)(2906002)(8936002)(4326008)(8676002)(2616005)(83380400001)(1076003)(6506007)(6512007)(38100700002);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: 66twX95e//Hi8lLhaJzU5hsxNYFdcLS+m/14hZy2Q76Csa4T5SEoo1oWuVNAY3ayVOlePmFVCrXZOuSNG+s40EXWCB8HCUUtcmVJddKeBIa1nQRE+zjMGx5g+/Midna5+izpLI+n26b5MjCxPEcZayF61Y5IbBd5ZjVXmeIHVy+x50x51APiaACcDj7dqH8gvZgzwVyiHBt+dhFgO+eJlZyqxpa33K0UiMkRcvWEpLnFvvecHuy8XFmyPNjY2atgthdQURW4g1LsgTuu2BgydVtMKmceDF3heF10TqyPO1MKmvR2j0Hb98cc3cxkL6DV16Nb723zy/FjyS7PgOqqsMJvwWc92Rgb2tHYjJ0N+v1/UJTrSD+iXOIwzzRBVBdAqQsTgbVsoI9nNv5JjVlny/mr5Sizr8D9Ilr6Nk6FDcXdhgh/8V1HMCCJDfonjB/sjMchh5OLhF7lcxAH0Vnb15uYhkUOJT56RDa64qQ+/XQYZ0kMQAmOLbDb7Y9dvmzqkSxk0tU5NhmrkO+IUjjGO9/AvrfrsViS6zdbZ6zEbWUJfW5knIoxfAHxZYCaayMIakHPaqu0L6f95ubVwnlZEJGMiyQaq2r14SXjl0HLFugAFr3s9aMlmxsAwevxIafYBZK7Zj2wHX71vA5U7v0u9BB0F6eCDf5IzLE9oNoll/cMsR0UXcpQNa8pTNGvznCuymC2BeDk1Z+CquO2FqxTNhddEoEZULLe/XGiTJWYQ5BLt/kMBU1uDvll7tojRHDiKmFCHvFnTK73+4pg049h+Bf1HY9dL+PmnnExukIoYHoIFhtoq4hay9kVd3ZLJpULF9+W67MokhsmsRTgMJBqPDOHw/7cu1P82dagzyqQ1b/oVSglFFoXWuN0/QsVatkGPr9bHARCkQwqdwIm0QBKXeJ5WBXfBY1bWxQlGa9wrgveUoRt4mDlvOwf9mTxT7fwEbx3DMqR6EDHPK9ohiKe6Bij2qGoIdYYkQATjO+qkolpKHYXGibeYrew0JfUHAPrPyK84+VYk8E0RSsEkoy0YBouomJS2CUw24ZSQiEKEt2/Tmd8gEkZE+j96jJ541kxIF3BsjBcz4+RMYdicSVpHqM+AWqfH3ElX0Vsg2HJ6ATw22v8hicvi4fsYxX+nATUKphiTqgahWuiaqO1G6ehL+JKkkjRBH1G0Rm6VFCDnLEB/mL6Lc/3Ab18Ah1RTtDO1AJp/s0TquPPvj2V05SMEaCudFJ9W9BHvOuWrRuWoDKypX6Vk4IpAQqlFz4AMgxQOXIy5nZ+StnfzZ+6xfzqzqj2dAjBfDVZFAPrk2ZUYIrE/FhUsN/ZWu/5uX74oEnw0lZ7aYiF/1g9nph4hDG7hsnsmtDl1RIxpJ1Li4QiN7IKC/k8qmOPwjtQ4nwEEwrDBSYNXHauhgZ/a73orPgTtxz3PEuH/aXi6vfjfuN+aojJhLBaNy64K4znnWqKsXX2FGalh0ogD2lxRRNWUHAgWopnq/uzLO5vFI16OXvyIr90LyfxEj3QPai75hOkbUBOSTypaehs9asXQTcGKcy2D4ILNGgjllXFrWYrXRJYhMp4PE1Ha3asTI/XRJsMUmAMDUWuID4T2BmAu/7WabyOlOhQA4mDtQkd7qN1K7/CDWsOTeBea0OvUxJDH4f99WYP+wKDNjmlvNq0V6Q5r9cmgQ== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: c6ba97a5-9c08-4672-e1bd-08dbe01e12e8 X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:46:38.0705 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: CK9kpB2UsKgrMCwAEnQTZB/bb4Q3pmv2UHf+I7bVi9TPUBlmRDxxSBLuqSH+ZNMifIZE8a8snyGvROIFKnPyFw== X-MS-Exchange-Transport-CrossTenantHeadersStamped: PA4PR04MB9568 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC Lifting the restriction that requires start/umin <= end/umax can allow us to track range that wraps around in the u32 range, e.g. {0xffffffff, 0, 1} can be tracked with start=0xffffffff and end=1. This makes retrieving umin/umax slightly more complicated, and requires checking whether wrapping occurs in the u32 range; wrange32_uwrapping() helper is introduced to simplify the check. Additional z3Py checks are added to make sure the new reasoning around umin/umax for the u32 wrapping case is correct. Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 26 ++++--- tools/testing/selftests/bpf/formal/wrange.py | 77 +++++++++++++++++--- 2 files changed, 82 insertions(+), 21 deletions(-) diff --git a/include/linux/wrange.h b/include/linux/wrange.h index e2316c7bbb2d..f51e674d1f18 100644 --- a/include/linux/wrange.h +++ b/include/linux/wrange.h @@ -3,24 +3,30 @@ #define _LINUX_WRANGE_H #include +#include struct wrange32 { - /* Start with a usual u32 min/max. - * - * Requiring umin/start <= umax/end, and cannot be use to track s32 - * range. - */ - u32 start; /* umin */ - u32 end; /* umax */ + /* Allow end < start */ + u32 start; + u32 end; }; -/* Helper functions that will be required later */ +static inline bool wrange32_uwrapping(struct wrange32 a) { + return a.end < a.start; +} + static inline u32 wrange32_umin(struct wrange32 a) { - return a.start; + if (wrange32_uwrapping(a)) + return U32_MIN; + else + return a.start; } static inline u32 wrange32_umax(struct wrange32 a) { - return a.end; + if (wrange32_uwrapping(a)) + return U32_MAX; + else + return a.end; } #endif /* _LINUX_WRANGE_H */ diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py index 8836f4cbbedb..a2b1b083d291 100755 --- a/tools/testing/selftests/bpf/formal/wrange.py +++ b/tools/testing/selftests/bpf/formal/wrange.py @@ -21,22 +21,31 @@ class Wrange(abc.ABC): assert(self.end.size() == self.SIZE) def wellformed(self): - # start <= end - return ULE(self.start, self.end) + # allow end < start, so any start/end combination is valid + return BoolVal(True) + + @property + def uwrapping(self): + # unsigned comparison, (u32)end < (u32)start + return ULT(self.end, self.start) @property def umin(self): - return self.start + return If(self.uwrapping, BitVecVal(0, bv=self.SIZE), self.start) @property def umax(self): - return self.end + return If(self.uwrapping, BitVecVal(2**self.SIZE - 1, bv=self.SIZE), self.end) # Not used in wrange.c, but helps with checking later def contains(self, val: BitVecRef): assert(val.size() == self.SIZE) - # umin <= val <= umax - return And(ULE(self.umin, val), ULE(val, self.umax)) + # start <= val <= end + nonwrapping_cond = And(ULE(self.start, val), ULE(val, self.end)) + # 0 <= val <= end or start <= val <= 2**32-1 + # (omit checking 0 <= val and val <= 2**32-1 since they're always true) + wrapping_cond = Or(ULE(val, self.end), ULE(self.start, val)) + return If(self.uwrapping, wrapping_cond, nonwrapping_cond) class Wrange32(Wrange): @@ -115,13 +124,59 @@ def main(): # Right now our semantic doesn't allow umax/end < umin/start w3 = Wrange32('w3', start=BitVecVal32(2), end=BitVecVal32(0)) print(f'\nGiven w3 start={w3.start} end={w3.end}') - print('\nChecking w3 is NOT wellformed') + print('\nChecking w3 is also wellformed') prove( - Not(w3.wellformed()), + w3.wellformed(), + ) + print('\nChecking w3.umin is 0') + prove( + w3.umin == BitVecVal32(0), + ) + print('\nChecking w3.umax is 2**32-1') + prove( + w3.umax == BitVecVal32(2**32 - 1), + ) + print('\nChecking that w3 contains 0') + prove( + w3.contains(BitVecVal32(0)), + ) + print('\nChecking that w3 does NOT contain 1') + prove( + Not(w3.contains(BitVecVal32(1))), + ) + print('\nChecking that w3 is a union set of ({0} U {2..2**32-1})') + prove( + w3.contains(x) == Or(x == BitVecVal32(0), And(ULE(2, x), ULE(x, 2**32-1))), ) - # General checks that does not assum the value of start/end, except that it - # meets the requirement that start <= end. + w4 = Wrange32('w4', start=BitVecVal32(2**32 - 1), end=BitVecVal32(1)) + print(f'\nGiven w4 start={w4.start} end={w4.end}') + print('\nChecking w4 is also wellformed') + prove( + w4.wellformed(), + ) + print('\nChecking w4.umin is 0') + prove( + w4.umin == BitVecVal32(0), + ) + print('\nChecking w4.umax is 2**32-1') + prove( + w4.umax == BitVecVal32(2**32 - 1), + ) + print('\nChecking that w4 contains 0') + prove( + w4.contains(BitVecVal32(0)), + ) + print('\nChecking that w4 does contain 2**32-1') + prove( + w4.contains(BitVecVal32(2**32-1)), + ) + print('\nChecking that w4 is a union set of ({2**32-1} U {0..1})') + prove( + w4.contains(x) == Or(x == BitVecVal32(2**32-1), x == BitVecVal32(0), x == BitVecVal32(1)), + ) + + # General checks for umin/umax w = Wrange32('w') # Given a Wrange32 called w x = BitVec32('x') # And an 32-bit integer x (redeclared for clarity) print(f'\nGiven any possible Wrange32 called w, and any possible 32-bit integer called x') @@ -129,7 +184,7 @@ def main(): prove( Implies( And( - w.wellformed(), + w.wellformed(), # Always true, but keeping it for now w.contains(x), ), ULE(w.umin, x), From patchwork Wed Nov 8 05:46:07 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449560 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id A58C5C8D2 for ; Wed, 8 Nov 2023 05:46:50 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="JQXkn5YU" Received: from EUR01-VE1-obe.outbound.protection.outlook.com (mail-ve1eur01on2048.outbound.protection.outlook.com [40.107.14.48]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id C2382170F for ; Tue, 7 Nov 2023 21:46:49 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=ilk5gYRszXv/w/BLKcK5aZVXadcMXrfoDPdQr3NmXS/BQKYqCvYFPNbul4lb6s0pXGfySCaTiZnmNe0thzH0NtxHM9ivsFCnl21k0jhwhwyREMD4VrNWvrYOGc+GYA7p0a4olKTvg8KIoEb+sgiagBYQksrgF7j8wR6Ae5Skzr8XtTJHIV8wIBdjQ6PYQ+oCt4DHwCYzfTiXV/L/oum61DdsYFviBuuJAbxAE8xYVzG6SyVsIuqf0zkl7+YF8+GERSrS3DIUdnrgfi9qlibgogJmKosFXaY3Z2xTQWKiiNaNh3reYZtfgGAT7G7tm4WU/so3iO+GIN2fLKOmndOLPQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=EIE0tNHu51H+i91nM9FbSd1pHFQxtReFDljXtYIpyDM=; b=gISfdkECCvMAFCzwSXkkrvgBc/w0aVf/Usqd+zaZUF75SDSU+2nG6UAHdxdvIgfwKclm9OfCROTM3sJ+AYP167SGeetik8jXyn2KJoYQ9RACsAv7J4B1jSzK7dJhH0RD7F7YwTU1cGO6uLTeQup0La3lbh85yU2Boj7DTyZHxvBBthI2Orp+0DEA7FB8D17jQjmFBUNs8WgmbgOv/Tssc728q3UsliE3Hd+Z6Sf2BxKg6rvY+X15CRTzct4jWWxDElxuUbcO2kEYBF1DkgfDJ1l3m+S/XbqKhmqzt51ywR/JKz4lGddbPn6g4OL/WsEBS5qbew0AGYYLfianR0ueoA== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=EIE0tNHu51H+i91nM9FbSd1pHFQxtReFDljXtYIpyDM=; b=JQXkn5YUQyYtO1SmqkKdW+Pcjf7iwludVQ+Ahk7kqmNbRJXcyXTK8FVdZQuJhb5yQhvDGpBhOxaXTZuBuwjCCuaSpJfXQs04fHIoDwsC/MHlkTieCW26XSNbHsOEed1u6ahDWsDJiDrzj0grQlMN56gktVDewuOyHR11lgVVJ7GSfVWdWIkoqZ96uVVJF5m8WS4ItEc03HVvX4jFdpFDpib/iK6dBMhnYYJPqBMOR9Ly1btUWcz5ubOpygG0x3lP5NPaXoFLGXE/HDlDj1jcP8RC7lu19mEqdhibZYiHTSB9wqukNwuP5MLL+rEsJ3s7qM0qkO2gbQxbYDA7Rtjzog== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by PA4PR04MB9568.eurprd04.prod.outlook.com (2603:10a6:102:26e::6) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.18; Wed, 8 Nov 2023 05:46:47 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:46:47 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 3/7] Support tracking signed min/max Date: Wed, 8 Nov 2023 13:46:07 +0800 Message-ID: <20231108054611.19531-4-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0081.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:2b3::7) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|PA4PR04MB9568:EE_ X-MS-Office365-Filtering-Correlation-Id: 9e1e875a-f0db-4153-8eb4-08dbe01e18a5 X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: pxNztqCaS3YxudSW6q1jPkihJEqQXRjB9QRIWYF0fMBfHRV3TfTlsmY4DFveDfTOfBmQwry/oAxjaUzZORkkLhNetz0RXUF0Zl0hF2oo98Jfijkp+fA3gh52WXmVZY/cy2SnO5RwM8x+NpX1p55+sbV73ZOdRcWyCKsF7F3muhwMfcK9fu/DgNSC++k1aTqQyvq8vK1TvBJ3k5z39fCDeQhUfsvxfuGanBVPnqgZ+S56vXV3UHOPlPESRm9l9JmqO50+aKBHinzpLXh8pqTk6+05TFfLM0yyWe4bSJQnNaDXKpyGWSxZh4TvcjYdiId53hCV2J8M6viAJz9nI5Y6jSwO7Fgs6Rcohdj4ZiZB60Y6u8JJv0fYmJhS3TbmTc9jJZptVZGQei46WknLgcm4nOk6m3eKtW/gXnr2OVLf8uh5MtgF01SlEJeUaubiUCFrLX3ThT5FV+y6taGjwJj935lGaTaE/yuUNe6qsrEq6zmpxYXyYelzxhkj4CbsqYsD5QN7MBNrPguIqynaCvp9luXZcOrvCyU/r4dWcOyU+zcUu9pbSK85YlugoOgbJpFe X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(136003)(346002)(376002)(39860400002)(396003)(366004)(230922051799003)(64100799003)(186009)(451199024)(1800799009)(6916009)(316002)(54906003)(66476007)(66946007)(66556008)(478600001)(6486002)(6666004)(86362001)(5660300002)(41300700001)(36756003)(2906002)(8936002)(4326008)(8676002)(2616005)(83380400001)(1076003)(6506007)(6512007)(38100700002);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: /hbJ+zPUKlTkOzHUJ39nWsizK25u27c/NftYoJpamf5K4B7yx3yQNLJ4X4T+jmh9XCpy7khkHpo3wXZWENxpbDRJsbvNxLfnWMpyyMm2Ic3En1S4A/H/5cLzY2HoB41vde9bJS9nKY1mkjlCeRDslYk4WOX+B25HprJEuo2p6itY+1IZ0GMBu0PugDDSagj6GudKZZX9dzkGFKEksMOKkL0yPt6pXQYZ/IooJerrkPwHEyTjoGcDCV9X8KLrjdxD3hCvW7NJWL9roVoHNX6qS+GBVBF5XP02qrCOwwzHgILXiYQaN2Ea7Rs829EnYs85UsEZIrzrtIGG+OaWGo10XZcPXB/plNU2y2joJbfEoVJ6SOwfJXMpmOtyH2uq/CWLPZQXdwOlAcvZEvojaSaRa7Wh9XEmHTqdlWy0Iat3QxUm7bZ2+5SRU6/SOWI1OKNIkbgbt6oVGWuXoqnw+yA/r9Hu7fKY0QSv9zSzs9eX/zK5bujd4qIwJbLdQug96GIYWO15K1pJamiiBaljTzeX73fs8G/4/An8IAJy2dx6IkvWj2WIXiFC8e5lwS1INOiGsqrP9N7c57oKQ5FVPo+EDk6PFKHYRlq40tUy7KCj7ammiVd48lok9eHezluP/gFAvZlQQ3H3Pq12hwcUtXAfEHB+kAj589d8kkEJJDpjRSYNhw5y9WpSwarLjHt/s2uYXNDGYw2xasgO0r8diDi/OUPSf03Ap5X1p3NXE6WZvTGezSrEh4amsDTVRkQ8wazU0NQFJxR24qwXHFKUvDuyPDT9UgUzCrndXXuOL6ukMXRwarR/YwEKHXv87GsocczrZw+dQySchavNmT1xuDAs09RnRTY6QIaSMsRW4vO5QA9JajVmBH9RtMMvOUO/Ig8xDRxf+KiKWxSTAHCLiDuXpJoG58+V+VxtAACRu61NDH/YPrzb4Afr9PlS5lhjpdqX0nZPFr26Hes6Rc4O+3JohlqDwnZFXU7oe49shX+fwMEFgDaEYPaWUbx0rrg3sZT5P4WYMnbOMQmCk43BvQbP1t4wHdIAegU5BviHpQ+925SOrWCqlarFpBSWlQql5JljdbXoPfIf+CnUxqXhx5cZK2r1Xn0M34p2nlky7lpTJm1gzC4j1zTZENuCBN1K0ALXC8XY+EvX5o+NOm11Lg6SmGyn9nJplCPLDVHwsdkia31vZGRN2Q/ff6gPxZvZedy4Vz0ixqQaKq/il8N1OlDbLPVFTXRBhthfXkF785v1tiuJUQiqPNcam26sSXRUJ+A7MtT7VxO6o5lPfmsLzHFud/b/1AclETNKa5J9dTDW7vYShmLeLpNqDSDGuNFIsB0Fwp0sCkgatQs8C03dFfWagYknY3Hqe3UrgogtbxR5mAvYbfB947dI8+ouLBMjKMIojqsBR2Di11T+AJR5bVn4fU7ZVuzLaOaO14w7uTShhT43YUSMKr5VvnRhT0t+btGPIyB4OJY0WYVhNpLDT6z5VdbbF/yWnXCLhCB5TFwpJwADW8j+j2kQjblLrRq3iVf1sQB+OhN2Lv1Xg53/faLMb7gIajZ+/UXciwz210scF3M0gId3AYARiEAPppH5cL7rKAyIgMjxkyyxG80cxZ8tvPacrbhBBG+NoaKnTR0IT9hm2Wx92dTkjP49sNm8X18UhFzcJZ0mng1RM0g2NVzMGw== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: 9e1e875a-f0db-4153-8eb4-08dbe01e18a5 X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:46:47.3473 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: gQWudJvukl695YmXWEtQbqMlQtpdSKvNHSpzGO6cG06Bme+g2mOrqPPNCZgu88AMVi5eGe7FchZg3uRpTZFe9g== X-MS-Exchange-Transport-CrossTenantHeadersStamped: PA4PR04MB9568 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC With the start <= end restriction lifted, wrange32 gains the ability to track the s32 range as well. The example provided in previous patch shows that wrange32 can now track {0xffffffff, 0, 1}, which is in fact just a plain s32 range {-1, 0, 1}. This patch add helpers to extract the smin and smax from wrange32 along with wrange32_swrapping() helper that checks whether this wrange32 wraps in the s32 range. Additional z3Py checks are added to make sure that the smin/smax reasoning is correct as well. Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 19 ++++++ tools/testing/selftests/bpf/formal/wrange.py | 67 +++++++++++++++++++- 2 files changed, 85 insertions(+), 1 deletion(-) diff --git a/include/linux/wrange.h b/include/linux/wrange.h index f51e674d1f18..876e260017fe 100644 --- a/include/linux/wrange.h +++ b/include/linux/wrange.h @@ -29,4 +29,23 @@ static inline u32 wrange32_umax(struct wrange32 a) { return a.end; } +static inline bool wrange32_swrapping(struct wrange32 a) { + return (s32)a.end < (s32)a.start; +} + +/* Helper functions that will be required later */ +static inline s32 wrange32_smin(struct wrange32 a) { + if (wrange32_swrapping(a)) + return S32_MIN; + else + return a.start; +} + +static inline s32 wrange32_smax(struct wrange32 a) { + if (wrange32_swrapping(a)) + return S32_MAX; + else + return a.end; +} + #endif /* _LINUX_WRANGE_H */ diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py index a2b1b083d291..825d79c6570f 100755 --- a/tools/testing/selftests/bpf/formal/wrange.py +++ b/tools/testing/selftests/bpf/formal/wrange.py @@ -37,6 +37,19 @@ class Wrange(abc.ABC): def umax(self): return If(self.uwrapping, BitVecVal(2**self.SIZE - 1, bv=self.SIZE), self.end) + @property + def swrapping(self): + # signed comparison, (s32)end < (s32)start + return self.end < self.start + + @property + def smin(self): + return If(self.swrapping, BitVecVal(1 << (self.SIZE - 1), bv=self.SIZE), self.start) + + @property + def smax(self): + return If(self.swrapping, BitVecVal((2**self.SIZE - 1) >> 1, bv=self.SIZE), self.end) + # Not used in wrange.c, but helps with checking later def contains(self, val: BitVecRef): assert(val.size() == self.SIZE) @@ -79,6 +92,14 @@ def main(): prove( w1.umax == BitVecVal32(1), ) + print('\nChecking w1.smin is 1') + prove( + w1.smin == BitVecVal32(1), + ) + print('\nChecking w1.smax is 1') + prove( + w1.smax == BitVecVal32(1), + ) print('\nChecking that w1 contains 1') prove( w1.contains(BitVecVal32(1)), @@ -102,6 +123,14 @@ def main(): prove( w2.umax == BitVecVal32(2**32 - 1), ) + print('\nChecking w2.smin is -2147483648/0x80000000') + prove( + w2.smin == BitVecVal32(0x80000000), + ) + print('\nChecking w2.smax is 2147483647/0x7fffffff') + prove( + w2.smax == BitVecVal32(0x7fffffff), + ) print('\nChecking that w2 contains 2**32 - 1') prove( w2.contains(BitVecVal32(2**32 - 1)), @@ -136,6 +165,14 @@ def main(): prove( w3.umax == BitVecVal32(2**32 - 1), ) + print('\nChecking w3.smin is -2147483648/0x80000000') + prove( + w3.smin == BitVecVal32(0x80000000), + ) + print('\nChecking w3.smax is 2147483647/0x7fffffff') + prove( + w3.smax == BitVecVal32(0x7fffffff), + ) print('\nChecking that w3 contains 0') prove( w3.contains(BitVecVal32(0)), @@ -163,6 +200,14 @@ def main(): prove( w4.umax == BitVecVal32(2**32 - 1), ) + print('\nChecking w4.smin is -1') + prove( + w4.smin == BitVecVal32(-1), + ) + print('\nChecking w4.smax is 1') + prove( + w4.smax == BitVecVal32(1), + ) print('\nChecking that w4 contains 0') prove( w4.contains(BitVecVal32(0)), @@ -176,7 +221,7 @@ def main(): w4.contains(x) == Or(x == BitVecVal32(2**32-1), x == BitVecVal32(0), x == BitVecVal32(1)), ) - # General checks for umin/umax + # General checks for umin/umax/smin/smax w = Wrange32('w') # Given a Wrange32 called w x = BitVec32('x') # And an 32-bit integer x (redeclared for clarity) print(f'\nGiven any possible Wrange32 called w, and any possible 32-bit integer called x') @@ -200,6 +245,26 @@ def main(): ULE(x, w.umax), ) ) + print('\nChecking if w.contains(x) == True, then w.smin <= (s32)x is also true') + prove( + Implies( + And( + w.wellformed(), + w.contains(x), + ), + w.smin <= x, + ) + ) + print('\nChecking if w.contains(x) == True, then (s32)x <= w.smax is also true') + prove( + Implies( + And( + w.wellformed(), + w.contains(x), + ), + x <= w.smax, + ) + ) if __name__ == '__main__': main() From patchwork Wed Nov 8 05:46:08 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449561 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 04A0BC8D2 for ; Wed, 8 Nov 2023 05:46:57 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="fObMEZ08" Received: from EUR01-VE1-obe.outbound.protection.outlook.com (mail-ve1eur01on2080.outbound.protection.outlook.com [40.107.14.80]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 084641707 for ; Tue, 7 Nov 2023 21:46:57 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=XLOm2Et58SLocA2cDad4kysqVzCmoUQamz+YJhxKDycQARZ2cn2nbcPdA/8NxDeD1/ZEPPya3uHAs6aHExo4UrVeMwi9wHxpFIErYbeHQAa5E4dn15waRZpTlUGCX9CvSX4jqtXW1IZ6hSwzjQssG0ujcGNpmqJ8lrW0R7yMb48xur7Zpbp2HsEoyrmehX9trzfQ+2PwukAy6bf0rBY5HRwR03kOx1P38cXJoIfnPf3kOP27San343B3VoPwKHeBYdH+ltXSJD9M3goNKefUdkx219gxqoPuDei7AondkuF77enJ07whOwnAdWVmV+ngVjowbDcMJL24pUARhj5Wng== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=1L7s4F+1u69iqXSVHKHqh3zPlevFxs9mQa312W8D2aE=; b=NnxyVttbWhiLHV5H77lmeqQr084vuxI2e3qE9aXkWE7WFMdtWz+Lun87HVCDDYgAwRiBYpKtDFoFdILC0xb/NCSaG+1lbikyQe3u7UwUB3O01n5zM7M+/mnkgmkazZYeHc+7JMccLjBmq6sOsZVYVKnI9oWJ04i9IAiFMU/M09/9ESvCuhyh5CKG8El7KjqYzFGegCGVN09LReJ8OZbxninTf+Fggjzfin1Hsc19JFLAM0i/VFMdgoyBCx2fhA7XRSgb+/crLZq0RURFllacY+FxYrsKOy2IBpVqE2ApnjzoC7QmE6+6I2XCJv2YPEKvxnZFdaRXJfZr9OMkyuY/YQ== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=1L7s4F+1u69iqXSVHKHqh3zPlevFxs9mQa312W8D2aE=; b=fObMEZ08LQysKxa4FLeT9GZEBB/aVSZCz91VqtDu4coG4bnCDHbp1RjWqcbaYxEOhmMPyrBWNVI4IiSsgPWTaqt5vycq5Hv6GVGcTe5k7m7iayc5SHC84/uC6qiTtHMHkjEsgZDEsRsxStpt1SDUHzYqOpU48c91l/htcuMXe1adpnGFh6fYTyaOF/mzTbZULPTsPmnG9foQSA8pckEACrK8YMnW7w0AFjuf47w7WMsOO/65zqMtO1iZiGsJuO6O8MQeg0A6DHwhrkeDPBjYBQixMjFa+7bTxsSV99q9d8HPyw1tA+2r26/nj4P38UsV+f0Muz9NqQcDiKXx6HueOA== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by PA4PR04MB9568.eurprd04.prod.outlook.com (2603:10a6:102:26e::6) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.18; Wed, 8 Nov 2023 05:46:54 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:46:54 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 4/7] Implement wrange32_add() Date: Wed, 8 Nov 2023 13:46:08 +0800 Message-ID: <20231108054611.19531-5-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0080.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:2b3::10) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|PA4PR04MB9568:EE_ X-MS-Office365-Filtering-Correlation-Id: ba96e02a-f7c6-4329-e81e-08dbe01e1d0a X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: kpn0yHc+fzN4+7oefdyvBdskcq0XZAgu6T5H/6+jCnwWHyDXvfuJMO7a6i1Lo08EJOMCpmnP6yG3I8N5VQadLH8AHatM7wRc27L1w1zBMUdYmkz3pm+RNTnm3I1TFkM/fztiPLLaRMVUmInI7WEdHhO/TkCSoVJ1Ugidj+hVq/5hm8Bn+tNXCtQAhwoG7vFMU2S5DKJygZN/24DhTCth2UlliyhrnR8gqRtYwwhajv3uhOGP9JKyUb5kkz8NS9Sk1MBio4eT0jXv0c5S3wmuwSDrLGCNmI6idCmDKQzRHU3EQESoGTCA1MlO1PK+9d8mmjVDtYGq0LnCpr2dR4uSGtGubt1ASI7rD6O6P+rAhjHb4V3JQLYnw98VPO4Ci5WcsCFFAxpg46L3yJh39g9FH9m0eDEA4BWRDpU8/aYnhZs6hqiM9lm9R0H5wPLvxsAH145HUyHC+/bm6IcALXGISq5B2pn9kOBnCxoW37Lv4MdMelmf/+ZkLkUooibo5RXpN/hWQ5TwBvYpYWJey/j+xv5GUgqJ4TUcUk+kEIlPTEjOWiw+NlmC5fUQPK6IeAbqKxLGEcFCelXDk0LnPcBBjQjVZaf+pw9XI90+NX6mvvsBt8My8f39iOAVHgZob0Tk X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(136003)(346002)(376002)(39860400002)(396003)(366004)(230273577357003)(230922051799003)(230173577357003)(64100799003)(186009)(451199024)(1800799009)(6916009)(316002)(54906003)(66476007)(66946007)(66556008)(478600001)(6486002)(6666004)(86362001)(5660300002)(41300700001)(36756003)(2906002)(8936002)(4326008)(8676002)(2616005)(83380400001)(1076003)(6506007)(6512007)(38100700002);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: fKFMyRKbjfEutOcj6Dz1uecPAzUv2hJzazElqucPwTietmNdtPgPp+bQIIn9YKMa3TtKAnPY7lh8wkBUoHwpMHHOeRkvwh/gR/z9pkS+PyTekYrHYg/yz49dTZ3e/DJ2GWOhAr/U8RO6GFe39AMRpwjASOBraxXLFrPKDA6oiq7t456vmqLb6VDmXHCJGo72GtjRty7GwOB7grccqcA0kaNS1nXrtI9Ly7qXvOwBhorgB+FXOfDJ8H8MkkB4D1EGQFm5g48pDSvZa+mAuWFqG+Mhyz9iyhJ2BV4VpbF5EsSTvd9AM0tQBYMmd9flWYrnf0aQ+E+b6t8F8hsx89Fq8OgODlsRaywza/Vr/H1XQbNXFyj/EG5D/Dn5BEgV8OFB0qDdffg764NwfmCHO6HRhCVKbbie50g00j4zdg1Uf4wltIqVRU3K+o/QP/5wsGT1/QtuVzojdV2slmBj4Jw3LkFMbpqgR74bvkL9hQ85/i1ZHdF58lT7M6OLjQKgYKv1lvWyp09Bu0w0az3bYLfD4rDnp+71sgVKM6OjTxdzx8sMKJoiOxvYkOd1NUivVaXZlskddnfGi0yjMjaq9LzehoPnQppRufpnP43G9QjRrHKfF7y1I5Ytw6RvSL3eyNAHfW5bwjVbchlalf9gIKN2lky1/dg6G+JijF+j2iq98vYATLC7cFwUzyWsoe8CJREbma3keNUjKQQ+6cb3MAelAkFCkOZxCToea4uos0ddJgeZUNGO/kTAMG+Xy43nnHAwFPI+uE4OL9c7Jx/IVTVEhqk4OqMVY6rkZ9cvCn5d19VRi9JnJcBzVF2hVIp/KyyPYqnPvfcTh31rlgLzaN1Agn03MD7iRFHA8NTBa9aHoUyG94KJHiwdmNlOCf7ObeOfTgtkqD899NYpSVyv9GADMiO2yuva9LxbSrCGkOq6JNeD8VwBTsXB0P4X2zuutSmqiivAKfGQCGL8S+5XcFi4vDFiROqWRO1m7k6fzhZCLE5rzWjDkb4bq1grI10uwt7O+XfeDWanyiRa2VOq4hGd3oRinXwb+6hZBkd68qOyvimP5ChWk6t5RbkrdtdlZ637V4Ut0VtEgQG6t3sPuYycky+oUda+Q2ooI5w1vQ2h9v1AT5seGUaAt2uxkmqW62YQRA8Sah3c9llAXKHTJ9Y9dxxLT7NaAGPJv/vn5GjkFasu3gSupsQbLc26Ok9dB67p8pfueYIVPe5zvjsEQDN8W68XkpJK8PxbAC19jFvNOPe8CjGPR7B4uQM26jzFrkvnhJnY62QzjQDsFqp9JVYQLvbalXH9y25xFud/KCKh/f7sdJjwG0wBcjLz0DfThbufo/ZnwAZ7sZD+7aX+fOrkmzua+qUKpwys0D+/E0GrB9glCWMIgoCfREtBWaex3UszUyTHANPmGsifYz9sxKhsrW4InrRl3npans+YRMB1opsTBsRReXG+Tc1QCvTmFZRGLqR/mDERPnwcxiJfvhqfAljuLt4dMEXZhKS8EkYpIPjYwoIwHsn64h7ulMRz6pQvQdmGYIMbpeXsvziCLm0QBgqM0Noj5jYSGzE9pFPn5+iBCGwgdngwE3BI32MSxMAhwlx1lz/yN3CvCVqISSWtL3/+PpGkC5VYh480RTEAXrCWctzgX7o/dkf9bjxWt94MwJHRrglRTt4728atomdQAA== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: ba96e02a-f7c6-4329-e81e-08dbe01e1d0a X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:46:54.7044 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: MNxKOGn8cZ1Z34lSEGQFiN/5prC9zELpymteq2GqNwkd0AOaCYOCsuDUL4Asn28Ln4oiQEwTvwBLS4Xv+/6kMA== X-MS-Exchange-Transport-CrossTenantHeadersStamped: PA4PR04MB9568 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC Implement wrange32_add() that takes two wrange32 and compute a new wrange32 that contains all possible combinations of sums produced by adding values in the two wrange32. This is done by adding start and end of both wrange32 for the majority of cases, and works even when the addition overflows. However, there still exist cases where the addition of two wrange32 result in a range that is too large to track, this happens when the combined length is too large. When this happens we fallback to start=U32_MIN and end=U32_MAX. (Calling end-minus-start as "length" because one can visual wrange32 as a number line, and thus end point minus starting point would naturally be the length of such line) Additionally, make sure wrange.c gets compilation checked, and add wrange_add.py that models and check wrange32_add(). Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 2 + kernel/bpf/Makefile | 3 +- kernel/bpf/wrange.c | 17 +++++ tools/testing/selftests/bpf/formal/wrange.py | 4 + .../selftests/bpf/formal/wrange_add.py | 73 +++++++++++++++++++ 5 files changed, 98 insertions(+), 1 deletion(-) create mode 100644 kernel/bpf/wrange.c create mode 100755 tools/testing/selftests/bpf/formal/wrange_add.py diff --git a/include/linux/wrange.h b/include/linux/wrange.h index 876e260017fe..0c4a8affd877 100644 --- a/include/linux/wrange.h +++ b/include/linux/wrange.h @@ -11,6 +11,8 @@ struct wrange32 { u32 end; }; +struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b); + static inline bool wrange32_uwrapping(struct wrange32 a) { return a.end < a.start; } diff --git a/kernel/bpf/Makefile b/kernel/bpf/Makefile index f526b7573e97..f0a4ce21e2ff 100644 --- a/kernel/bpf/Makefile +++ b/kernel/bpf/Makefile @@ -6,7 +6,8 @@ cflags-nogcse-$(CONFIG_X86)$(CONFIG_CC_IS_GCC) := -fno-gcse endif CFLAGS_core.o += $(call cc-disable-warning, override-init) $(cflags-nogcse-yy) -obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o log.o +# At least make sure wrange.c compiles +obj-$(CONFIG_BPF_SYSCALL) += syscall.o verifier.o inode.o helpers.o tnum.o log.o wrange.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 diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c new file mode 100644 index 000000000000..8cdbc21a51f2 --- /dev/null +++ b/kernel/bpf/wrange.c @@ -0,0 +1,17 @@ +/* SPDX-License-Identifier: GPL-2.0-only */ +#include + +#define WRANGE32(_s, _e) ((struct wrange32) {.start = _s, .end = _e}) + +struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b) +{ + u32 a_len = a.end - a.start; + u32 b_len = b.end - b.start; + u32 new_len = a_len + b_len; + + /* the new start/end pair goes full circle, so any value is possible */ + if (new_len < a_len || new_len < b_len) + return WRANGE32(U32_MIN, U32_MAX); + else + return WRANGE32(a.start + b.start, a.end + b.end); +} diff --git a/tools/testing/selftests/bpf/formal/wrange.py b/tools/testing/selftests/bpf/formal/wrange.py index 825d79c6570f..c659cfd3a52c 100755 --- a/tools/testing/selftests/bpf/formal/wrange.py +++ b/tools/testing/selftests/bpf/formal/wrange.py @@ -24,6 +24,10 @@ class Wrange(abc.ABC): # allow end < start, so any start/end combination is valid return BoolVal(True) + @property + def length(self): + return self.end - self.start + @property def uwrapping(self): # unsigned comparison, (u32)end < (u32)start diff --git a/tools/testing/selftests/bpf/formal/wrange_add.py b/tools/testing/selftests/bpf/formal/wrange_add.py new file mode 100755 index 000000000000..43d035383fe4 --- /dev/null +++ b/tools/testing/selftests/bpf/formal/wrange_add.py @@ -0,0 +1,73 @@ +#!/usr/bin/env python3 +from z3 import * +from wrange import * + + +def wrange_add(a: Wrange, b: Wrange): + wrange_class = type(a) + assert(a.SIZE == b.SIZE) + + new_length = a.length + b.length + too_wide = Or(ULT(new_length, a.length), ULT(new_length, b.length)) + new_start = If(too_wide, BitVecVal(0, a.SIZE), a.start + b.start) + new_end = If(too_wide, BitVecVal(2**a.SIZE-1, a.SIZE), a.end + b.end) + return wrange_class(f'{a.name} + {b.name}', new_start, new_end) + + +def main(): + x = BitVec32('x') + w = wrange_add( + # {1, 2, 3} + Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(3)), + # + {0} + Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(0)), + ) # = {1, 2, 3} + print('Checking {1, 2, 3} + {0} = {1, 2, 3}') + prove( # 1 <= x <= 3 + w.contains(x) == And(BitVecVal32(1) <= x, x <= BitVecVal32(3)), + ) + + w = wrange_add( + # {-1} + Wrange32('w1', start=BitVecVal32(-1), end=BitVecVal32(-1)), + # + {0, 1, 2} + Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(2)), + ) # = {-1, 0, 1} + print('\nChecking {-1} + {0, 1, 2} = {-1, 0, 1}') + prove( # -1 <= x <= 1 + w.contains(x) == And(BitVecVal32(-1) <= x, x <= BitVecVal32(1)), + ) + + # A general check to make sure wrange_add() is sound + x = BitVec32('x') + y = BitVec32('y') + w1 = Wrange32('w1') + w2 = Wrange32('w2') + w = wrange_add(w1, w2) + premise = And( + w1.wellformed(), + w2.wellformed(), + w1.contains(x), + w2.contains(y), + ) + # Suppose we have a wrange32 called w1 that contains the 32-bit integer x + # (where x can be any possible value contained inside w1), and another + # wrange32 called w2 that similarly contains 32-bit integer y. + # + # The sum of w1 and w2 calculated from wrange_add(w1, w2), called w, should + # _always_ contains the sum of x and y, no matter what. + print('\nChecking that if w1.contains(x) and w2.contains(y), then wrange32_add(w1, w2).contains(x+y)') + print('(note: this may take awhile)') + prove( + Implies( + premise, + And( + w.contains(x + y), + w.wellformed(), + ), + ) + ) + + +if __name__ == '__main__': + main() From patchwork Wed Nov 8 05:46:09 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449562 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 7EE1FC8C4 for ; Wed, 8 Nov 2023 05:47:05 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="OMKoHYEi" Received: from EUR03-DBA-obe.outbound.protection.outlook.com (mail-dbaeur03on2081.outbound.protection.outlook.com [40.107.104.81]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id BEAF21706 for ; Tue, 7 Nov 2023 21:47:04 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=i2B37/zN4W810wIeKSsKQbAMqMiaRkf6g+upv7DDIup+1PPg/zZz0cBlTwJsy1Ss3OKiCFOPJGkwgI+dSZ9N17KHGfTY9UIdTr/hGqStzwMoaMJmO7WmR9F1XCDW4TtALzcEl5R0QudP5R/hcKDNH8aNIr2UJrj/W9LDyCNBIu1lEN87N824HgcKDtN42C12LOM3687FBxPw3A+LaHswje+plLHzjfAWMMdz+3tHoGVmGT7VRxuh/8VM9WDr8ObzIKVytds3ex6sLydpxFFpKfQzkwcfCKecc+furCbs+TTQWcG6aIchG5yKPZdk/dsP+MGlbHfqk2ro43VL3L+Byw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=Lsfco474x3kUiChppMI9jct3gpEcWVJg9mU/CsFJUCI=; b=IS+USkuZKh+x7QTERKrrxWxlahAYJkp+WB2WlzC394uViAiaNDvQ9gsOpzoJk4hB6U85PwLqgIdIl1kYduTQQPcItDaHJeHrjKAi9lgF+INM/FgD6br/AYiVOdqRnAYAz3xVL5nxJeZvcleBv90Xc9q4xMqc6YC8gH9j4gHyPzkvMt4QM7YibsvEeKC+ImUCf4TAu3nvzwqeRVKYqgxCzUTewjafGHzT9PGUA3xA8Lb+T/du9k3UOigaDSCx12Ov8mv1RyArX40xg49Ekri4Pcm5yHmuoPDImS6MKmk/cRVov+2ftHsQlF4pgGNUsOleghjzRk/+iKyk2ijir3wgGA== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=Lsfco474x3kUiChppMI9jct3gpEcWVJg9mU/CsFJUCI=; b=OMKoHYEiQ/aGxtQUaX9VtUnAjxzAs905gnAuolD1LMeHTxs941bIeGu0MHg8BUlrZe43aLIU7YQWT47A7MZoqcS/wxGLUkbjXkEr01BdByvTfK6AAZmOcv/Xu0l16xDr6ErVwutmXVYtY2AHRHoUGCKBWTjTruTCiIj23+HhjmZqIWxtIAsTXBBTyWqGSc45kw/lB73sKtda67BFjlO9MRyVzpc+S7pruAGYDxAKuTgaXGf6SjlPI03yNQY0Xq9WRqTrkz+xwJxiOPCvaMx7blRE/y77x1fu8BzoxuUIFHZQ2ySj/Lj07CoWvVMLPz6jk6M486Or161ptw/97A+hFg== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by AS8PR04MB7816.eurprd04.prod.outlook.com (2603:10a6:20b:2a3::5) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.17; Wed, 8 Nov 2023 05:47:02 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:47:01 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 5/7] Implement wrange32_sub() Date: Wed, 8 Nov 2023 13:46:09 +0800 Message-ID: <20231108054611.19531-6-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0326.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:3b7::10) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|AS8PR04MB7816:EE_ X-MS-Office365-Filtering-Correlation-Id: f5c9fdfd-0452-4d6a-e0f3-08dbe01e214e X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: h8D8MrxeaPpq0sWmmVYZ97Q0PYVqbQBnOpO9/K+8Nj/KHRCdQ5IF1zVKOB70az0Xy9d98sv+f1y86icC7UsO7LHpA8BurY6tuTFkHCiE3a+CIcRvPlWdxghbL9IBVpY/Gw66Py9DBGTI+RmWdLcBwv6e8htqWGKq9bOFfqYEztCsQDgNdjOXdooMNbD4xeC92+iZdQCz2aya0f/1ecmqTHDRVUYCw6j142Wx7KTS+3gv8B4rlKVtjOeHc1XBvmVcwVxqRQ9oXfeO0EGa/8bG8Ao5q71DFI9vepBPnrcqrgZUUcOw6mxH22Eg+Edu4oshkQcPLo8eKQPDNMWr2DDWAJFrJsxlVBBuUlcHEySmfWbNBqmkm6gVMXMCnRLdgFYxzZplHatf1zMHtKCLvkDlUxtTYPiM8zItIgH7wAVOQcBRi8ZTH3Uuf6nAgHIeXBAQBE3tPdfnEI2CqCi1walBdrbBh7bj8vMKaRVj3HIMDfixgca0qLhUHu7IvEB70p1ZQZmSlTzrnFjleJTqfBA5/b3hh6kiSYkMDsvdPdCRnUP4fWMEFIUGqyihhX/Ga1LT X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(376002)(366004)(136003)(39860400002)(396003)(346002)(230922051799003)(1800799009)(451199024)(186009)(64100799003)(5660300002)(8936002)(6916009)(4326008)(8676002)(6486002)(6506007)(316002)(54906003)(66556008)(66476007)(36756003)(38100700002)(41300700001)(2906002)(86362001)(66946007)(2616005)(1076003)(6512007)(478600001);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: XEYbaUTpU2H7gwBPrwDeY0R02xjZqOzN9KkZlYDFARjkUP9Wp90TaZoP8ia3zWauKwci8z28CrYVyRI0Rlcsn/9mUPi1Xcx0wIXRuOc7LvmKuYlUnyt+tI/sixyv0tQZBYiv9ocqsLzSAEppTvpzuUrR2/w9fXCqaRPgbvyy8xgzLqFl7vrmNBN0MTFPV+855R+LV+Ks8RkLkDqDKpJG5rDR858PYMdY6Aafsj75CwlQVPnySPYO2TC6DzOU4rx9CkYMOcNsKAyvGYWpc+wlZw5b5MA8XX0soHwIrumiYhV6QqVf/ye3Cu5GHGG+qtI1yuyZXbwUXfAN/7Zde3RrSrxdxj9bMmU/6DUbrvsMJ7q+JZoif0EZOmycoMKVumQFMjO5XNXEJMXcBp7gdIZlRw2Hpw1eQlY8vRY9wr5cc5qFRI/JcItts1xSTRhJDz3dYqs30T/zzmfGkH/M9pTnyE6Qe4wt3Gj+2mnIMmGVxlR8eUUlRmQgvh7fKoGbI6yeHFKhBBCuUfjCEeT3X1FiYaalN0Y1bsm4Tmgd5Ozi+lWZhKvoL1o4QaVddLUFcsRy2wlWrYZc/zMu2CQrURWWhx36k4LeYNqJVwp5euaUDB+W0pZz0666EZeBz9IUxw/e9yKl7HtwvBCZ2pwjQqK2pe7fbtpWrucZoCH7+qNZ/eGE3CVpHskVHOcbMc98TxWR11GnwG+D45tKm0qP/nX6Vseh4H88KBzWSVr8Ncm/v9Nwicaz5YeZlXP2Xt4V1crCdjaRlmIodV490sm9Ye3NBj40vv3MszWTYqlRDL4OELiuQl4BEKG/x20byWGFzVw9CbqEHtX5wjbDMk/qAr0CdLl7+iSotw1tm2EtsYrYKFVoh0W20GIRyXhVh/7mKPzWr7eW7Y4UMyzmfEmboniH8g5RkwCGe5ORfSilIJGaT3SfDLohIZ90SjpS+wVUIZRdCaJgzQT+Hc+YJnmX0+a8Y5Qw8QliPOo2qzQOW/eq2sv5Tuqu+WLAzbx99q64Tdsw5OmOzJ4/xQtt2EvlzfbEI22zPTj+kL6f/dcm5EVQSqHGO7ANLK60BuHg7l4+PDUaFjjBbbEcpvx52mZB7BZbA68bj9u0Ww97Jk14i5kO6ewp1r4FJ5cNxQqE3Uu9VF0pDiIuFCfbkR6/GrsNL5qmllO+7ckoQYzO5JUOm9uFIUJd1QG5tgNzut7m3f0gcRhowKMJHt7xx16uKajDRdOsZJbSNVgnG81ENd8oaoQ3YLh7Mlg9nbXG+4ZRCCM/IsRUflzF5O/VDoV6/39G20vNe6KVh7XjFtv9N15JnaQmUnWH/RZ/hCnuQXJAWZE5cEPKJw3nPlnE5+Xe7WIE13rWOlE0RwpfxdRSZ4iBs4oBs5lNT7s1MfascI3C8L21Z7dQDjB4dWYuZEMNSJodh1+3ypPg2jtf7QMxtz6GxxFWyhNksvCn3/VD3UxrMly9jkcQxpXsP8R6oQifdYLzuqhHb1+8Kv1JKU5jZ1dYZ93qCUXZ+INCTmTKJ2LndEGrNk2iK+vbJsmYYHMxBdAijdBBgd8ydYYoS/p4Jf8QbvZFTjVZ6ALWtNU8xlT/1WZYoM9UsGvGHGRSCOst2aqbO3KqAXfyz1g8w8kcLZYWZD48He0p01lueQZ9j5ybe32oAjJyN0gw1kUqJanSDyjBCClCTQ== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: f5c9fdfd-0452-4d6a-e0f3-08dbe01e214e X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:47:01.8453 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: 5mPa9wms9J41LG5XHCeAusvdjgLugQysjazxtGMFsgi5oqGNbQ72Mjp6nCtul9Y4KU+5h9KKz+IN54rBirJVXA== X-MS-Exchange-Transport-CrossTenantHeadersStamped: AS8PR04MB7816 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC Implement wrange32_sub() that takes two wrange32 and compute a new wrange32 that contains all possible combinations of difference produced by subtracting values in the two wrange32. Simliar to wrange32_add(), the implementation can work even when underflow occurs, but when the resulting length is too large to track we again fallback to start=U32_MIN and end=U32_MAX. Also add wrange_sub.py that models and check wrange32_sub(). Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 1 + kernel/bpf/wrange.c | 13 ++++ .../selftests/bpf/formal/wrange_sub.py | 72 +++++++++++++++++++ 3 files changed, 86 insertions(+) create mode 100755 tools/testing/selftests/bpf/formal/wrange_sub.py diff --git a/include/linux/wrange.h b/include/linux/wrange.h index 0c4a8affd877..ef02f5b06705 100644 --- a/include/linux/wrange.h +++ b/include/linux/wrange.h @@ -12,6 +12,7 @@ struct wrange32 { }; struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b); +struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b); static inline bool wrange32_uwrapping(struct wrange32 a) { return a.end < a.start; diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c index 8cdbc21a51f2..08bb7e129d7f 100644 --- a/kernel/bpf/wrange.c +++ b/kernel/bpf/wrange.c @@ -15,3 +15,16 @@ struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b) else return WRANGE32(a.start + b.start, a.end + b.end); } + +struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b) +{ + u32 a_len = a.end - a.start; + u32 b_len = b.end - b.start; + u32 new_len = a_len + b_len; + + /* the new start/end pair goes full circle, so any value is possible */ + if (new_len < a_len || new_len < b_len) + return WRANGE32(U32_MIN, U32_MAX); + else + return WRANGE32(a.start - b.end, a.end - b.start); +} diff --git a/tools/testing/selftests/bpf/formal/wrange_sub.py b/tools/testing/selftests/bpf/formal/wrange_sub.py new file mode 100755 index 000000000000..63abf4d2d978 --- /dev/null +++ b/tools/testing/selftests/bpf/formal/wrange_sub.py @@ -0,0 +1,72 @@ +#!/usr/bin/env python3 +from z3 import * +from wrange import * + + +def wrange_sub(a: Wrange, b: Wrange): + wrange_class = type(a) + assert(a.SIZE == b.SIZE) + + new_length = a.length + b.length + too_wide = Or(ULT(new_length, a.length), ULT(new_length, b.length)) + new_start = If(too_wide, BitVecVal(0, a.SIZE), a.start - b.end) + new_end = If(too_wide, BitVecVal(2**a.SIZE-1, a.SIZE), a.end - b.start) + return wrange_class(f'{a.name} - {b.name}', new_start, new_end) + + +def main(): + x = BitVec32('x') + w = wrange_sub( + # {1, 2, 3} + Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(3)), + # - {0} + Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(0)), + ) # = {1, 2, 3} + print('Checking {1, 2, 3} - {0} = {1, 2, 3}') + prove( # 1 <= x <= 3 + w.contains(x) == And(1 <= x, x <= 3) + ) + + w = wrange_sub( + # {-1} + Wrange32('w1', start=BitVecVal32(-1), end=BitVecVal32(-1)), + # - {0, 1, 2} + Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(2)), + ) # = {-3, -2, -1} + print('\nChecking {-1} - {0, 1, 2} = {-3, -2, -1}') + prove( # -3 <= x <= -1 + w.contains(x) == And(-3 <= x, x <= -1), + ) + + # A general check to make sure wrange_sub() is sound + w1 = Wrange32('w1') + w2 = Wrange32('w2') + w = wrange_sub(w1, w2) + x = BitVec32('x') + y = BitVec32('y') + premise = And( + w1.wellformed(), + w2.wellformed(), + w1.contains(x), + w2.contains(y), + ) + # Suppose we have a wrange32 called w1 that contains the 32-bit integer x + # (where x can be any possible value contained inside w1), and another + # wrange32 called w2 that similarly contains 32-bit integer y. + # + # The difference of w1 and w2 calculated from wrange_sub(w1, w2), called w, + # should _always_ contains the difference of x and y, no matter what. + print('\nChecking that if w1.contains(x) and w2.contains(y), then wrange32_sub(w1, w2).contains(x-y)') + print('(note: this may take awhile)') + prove( + Implies( + premise, + And( + w.contains(x - y), + w.wellformed(), + ), + ) + ) + +if __name__ == '__main__': + main() From patchwork Wed Nov 8 05:46:10 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449563 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 41152C8C4 for ; Wed, 8 Nov 2023 05:47:13 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="tm3iYhoj" Received: from EUR05-VI1-obe.outbound.protection.outlook.com (mail-vi1eur05on2057.outbound.protection.outlook.com [40.107.21.57]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 72D9A1705 for ; Tue, 7 Nov 2023 21:47:12 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=JBJgpAu9TblZkZm0xmyfDPdhWwuWzn+2fvSMkeq5CawV4gfuvZe2Q+ox8o63cVcZfj7upR4jjHpEqnPOAdJDG0jDSxyJnsXgrO2YlawBIX0N7OsCNZ14A1X5QrKRt0KFPT/CWFmkfJmv1fqz6n5QPGJf08618HrvtPQ+agZZR2rKetuiyxUFQ54Dh3KBXme0POvr29iNnLnYDWOjLr/ADwbuWIprMeU8mAxRUCHUXlXVyeDY+/nFKIrkerY3ZXIEktpk4WKvsP+CjDuD8edDcWxRlNRHHsTWNMOCyZI/grVOVYp+ILra1+Pdp4dsEuX74vW1iBmSfJnGsIq43VNT4A== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=KEKVkmo0HtSvymnUIurAsIDgeD6uS36PG7052MbNEiM=; b=C+afbIeffNTsHpniNdUT5vspuPXVjyU7RLs4MgpfVx9ahFHCYY2RRA++wWWjdwsOfEKLgb1F/3NvZ3+yAGinAWEG78qbqgTfHInuhUyzPfmKmu2jMmUIcKFEJfC7dM4QVS0OF2Z4aaZcz+iyPRucelqJgZQeIvpo2sTyO5E7slr6U3qyP6Hmtrvyn7CieC5eQ3Ujo4h07irZghf2fVAY4fv6ZnjWa40Usaen9PIFX3+VQKpCRD7z78dwb/7og3BklJwe38qMJkK0N78Kh3lKz1LPP7xUaP38wlaY3wCKG56WsaK8lyltTAmut2iNCaqkl1SPwfGix275T9PS4csDvQ== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=KEKVkmo0HtSvymnUIurAsIDgeD6uS36PG7052MbNEiM=; b=tm3iYhojjv5vlJZL/HkV7h3+6g9QPabA1vzb9JoxVI/WG0r1h1yR6WsewZoLxUBf310U+LXM7HQW5Ml/30lQ+JyRb1209LOST44nlHGnG6myseImuV4FrmXjr5jHeqdYP/9l5VR0eIOyvrlGgSMkbfnf8dekD+7YKOqU9ye/SdLxl4aDf0bx1CyBZ4nLGWojMtlXlxmuiLF9hsDlQ0LEVR4vNRdIGQ+SPUYqERiYxKvxAv22+5fCEjqDgLkOe5gecBHl5I8e+AwovipRtAPSzMuC7g131G9BKP8rMlWXEaQJ0sCXeGRaixn+GDGsQUG16nFJakmvSzlPJ66RNwaMcg== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by AS8PR04MB7816.eurprd04.prod.outlook.com (2603:10a6:20b:2a3::5) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.17; Wed, 8 Nov 2023 05:47:10 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:47:10 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 6/7] Implement wrange32_mul() Date: Wed, 8 Nov 2023 13:46:10 +0800 Message-ID: <20231108054611.19531-7-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0328.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:3b7::17) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|AS8PR04MB7816:EE_ X-MS-Office365-Filtering-Correlation-Id: 8f5c92c1-b7a6-4aac-47db-08dbe01e2643 X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: Q8ZXsG8w9uOyMU161dfkDmuV6MMqM9TkxT2JOH70j7424C0wuoEHmvCrIkJa65/sx/NNdHp8b+JDRnv+h78qZn78YoaZGxezcauC/Rkej8Ha5oBrMSovKgPjjnpK8SMj2V6KUVRM/8fC1YUesMDePGlxzpo61kjbc4aLnAQ/OOuSdZqXbm3/401GPfu1sbbueBApSDX9y5c7OCTA86ZEBHKpR0wvyGaU390CTnXjsPm4mnmq/Dz9/JUS1KpishJ/oCYK6NeOoZeXU31ajvYMJWGdSBKXSfRtrTlP0LyrRbNGi+xe+umH18XShyGQBq/1Fbpwsfc8vH1wvOuCiL43g7YOE37oceZ7ySEUsKE2BqQF9Sp7HW0arB1uexWYpzzri+/9wpmGje12F4WFaQby6Po8TRz0Xsn/vKEbmmJzXViRl30j+GxBgxY5p6rjPXm22F7UEuVT2Kn0i/zJChXS6e9qgnwWebHGKcs/b9pR2qvUOkWR7JfIk3l7xYR3WCyZdmuzoqAWmDkoRMvu/iGG18XAfX70Oit5NeHw4MZ8ICnxiWeRCFcE130ezRTqlU3m X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(376002)(366004)(136003)(39860400002)(396003)(346002)(230922051799003)(1800799009)(451199024)(186009)(64100799003)(5660300002)(8936002)(6916009)(4326008)(8676002)(6486002)(6506007)(316002)(54906003)(66556008)(66476007)(36756003)(38100700002)(41300700001)(2906002)(86362001)(66946007)(66899024)(2616005)(1076003)(6512007)(478600001);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: ySOzL4kTawpznIOVad7eoEHmZK6UZpAKbmXzzP1wz5o79UaDiKd9yvH+S/nmeq2KT0nHQ/3FLaQzX12fYrZPzW7tmR+CQxrOcMQt0BB9QZ1jZcQOeXT/RJOd46s9Xo2VV5phHMFB1Eo4eHSmwjWUUq6DRBNeZJWO8B1qSyRbD9i5Ly9mlxyb4FWqn0ACrsSr5Ybc8MGQ88igp70tks5IanQ+gkYCLcG54Wj2Z2FFFh+OZff2ZOw+y+vNp5yYb+HrROEf6C+0TBA4NHqgzA5bB2NNjQaOt016XTHQosLF1bvnzf4Cq9d4mTsjDttZxGwKiXRrNyZ8UStajmEhzsvdqY30AzJHXYuC4Do3+JamwRkyVHvKI4G7ocZ1eEP4JvBHtoP/dMe6ECtwl1y3Ljt6u3m4oDRWezuWudMCrMABw4NSNq8LANmXaoHAJNvk2pjy5y5RwPgMjjiecM/kkDLRaV26X+qD/xXxKpmfVC00NXu+cyUlZ8fm5rdn1GWAHDlYynbbSjymRJGwojruLOEajI4lw+fBjete26K1z0b9MdcwTmQV81qqggcj52PYwkI730wIN8BrfnJ8fFi9P/HzmQY85h7ymq0rZ8YGC3R///5Nzv9m8xA1dgK9XWrrOLNrUlEkTrQDoywAEMe9dKzqo44fN1vWdC1BBG/lduQn60MIx+pMCXfOc4B9kSTLryP0UyMZkphyzwPb+vWicu/X6aJ0ovQRcFjrvfkNxhMQRuFmzTBmQi/wE2dFj7VZC3DgYScueGgzPdcSuJjYibkqp/czdmut9pwYcYEFuQTQ4MFZ00Qvqr5O7MJdm4eeWwz900rmu2k6ihHd4w6P9DEB3oc4INgbmyfM27KgqMJyZ7n+oD+JjfZhZNTgcoeADpUtdH4HLy8FO4kFIOAsdWxaEU822EE8UIRmN3UQJcDyUjOaensGVm5eknVbjKPpbRelxZ7PNRGXGh5EFF7K0zxMgz3qiG3fFciljkTmMevMBrK2AcjiRv4xXGI4jI5T7Ne/40jjP+SJpZBD2mScHD5hvc9dnNUxqppUsWDWnsddtoYAaFeFbPU23wCLuFpcZhWyw8fYDv46t90w1d/c/0xUAwOnM2VIKcFLnJcZ36npmguPk636b1O8gxCeq5Q/9NJpqJ90DBdsuisbVEgitHDPxyIfiyB3NpkdL7cgu9RJnrrOYX53bCEDjdT3rN2OXR1tbT4aq7aAGLWtWfQGFmgF+EmnDR2vrBDsiIAaS3i/QdXyTdf7tiSlCtQplVvvaHYIgGK8OQQOo4V47A1GtdQHSjHc0ESXAk4xxjMmaOcHWaO+QplMnqdEt30ABGVCO2MX45viApDZLb7txpGgi51w2nWp23JlJ9EsLt4d9jcf+afoWEjZmLaFTt0Lsf5wS7jHJj93IH0F1aQlQllAYknZAKKie25fAKPQMzSrupOpdrGnqY38Tmy5gvNrZjG7uPXw7Zca47gL2jxD7j+2LzH3Pdkhx84XfDOLgfwT/jR/UJi/wSK0pykAVcc1NOvz7Va9N2AnTQKv4gblQy9/OmaYl8QVEAwlmdlmGDdQMjU/z/RidAcwNVRcfMIGGUV8PhadZgAyl3mnRaqL0tQ7J0UeoTvtRMUk7AsS8gyxlWvXwywutByN0qriuLB/0ecaPWJgaND5IPfxfsYsBD4g1QHEdQ== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: 8f5c92c1-b7a6-4aac-47db-08dbe01e2643 X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:47:10.1502 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: DnygnIVuLGS1LiPKF1lLb6D4PWkyCLwtQUE5EOcZI4Pb4O7THUArNF2BDM5urjI0wauqb2aH+nM811VOC+Hsow== X-MS-Exchange-Transport-CrossTenantHeadersStamped: AS8PR04MB7816 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC Implement wrange32_mul() that takes two wrange32 and compute a new wrange32 that contains all possible combinations of product produced by multiplying values in the two wrange32. This implementation is pretty much the unsigned version of scalar32_min_max_mul(), and does not take full advantage of unification. This can be further improved if needed. Also add wrange_mul.py that models and check wrange32_mul(). However at the time of writing this model checking for wrange32_mul is still on-going. Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 1 + kernel/bpf/wrange.c | 15 ++++ .../selftests/bpf/formal/wrange_mul.py | 87 +++++++++++++++++++ 3 files changed, 103 insertions(+) create mode 100755 tools/testing/selftests/bpf/formal/wrange_mul.py diff --git a/include/linux/wrange.h b/include/linux/wrange.h index ef02f5b06705..45d3db3f518b 100644 --- a/include/linux/wrange.h +++ b/include/linux/wrange.h @@ -13,6 +13,7 @@ struct wrange32 { struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b); struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b); +struct wrange32 wrange32_mul(struct wrange32 a, struct wrange32 b); static inline bool wrange32_uwrapping(struct wrange32 a) { return a.end < a.start; diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c index 08bb7e129d7f..4ca253e55743 100644 --- a/kernel/bpf/wrange.c +++ b/kernel/bpf/wrange.c @@ -28,3 +28,18 @@ struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b) else return WRANGE32(a.start - b.end, a.end - b.start); } + +/* Model checking is still on-going for wrange32_mul() */ +struct wrange32 wrange32_mul(struct wrange32 a, struct wrange32 b) +{ + /* Be lazy and don't deal with wrange that contains large value that + * may overflow as well as wrange32 with negative number. This can be + * improved if needed. + */ + if (a.end > U16_MAX || b.end > U16_MAX) + return WRANGE32(U32_MIN, U32_MAX); + else if (wrange32_smin(a) < 0 || wrange32_smin(b) < 0) + return WRANGE32(U32_MIN, U32_MAX); + else + return WRANGE32(a.start - b.end, a.end - b.start); +} diff --git a/tools/testing/selftests/bpf/formal/wrange_mul.py b/tools/testing/selftests/bpf/formal/wrange_mul.py new file mode 100755 index 000000000000..bd95fc6367b2 --- /dev/null +++ b/tools/testing/selftests/bpf/formal/wrange_mul.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +from z3 import * +from wrange import * + + +# This could be further improved if needed +def wrange_mul(a: Wrange, b: Wrange): + wrange_class = type(a) + assert(a.SIZE == b.SIZE) + + too_large = Or(UGT(a.end, BitVecVal(2**(a.SIZE/2)-1, bv=a.SIZE)), UGT(b.end, BitVecVal(2**(b.SIZE/2)-1, bv=b.SIZE))) + negative = Or(a.smin < 0, b.smin < 0) + giveup = Or(too_large, negative) + new_start = If(giveup, BitVecVal(0, a.SIZE), a.start * b.start) + new_end = If(giveup, BitVecVal(-1, a.SIZE), a.end * b.end) + return wrange_class(f'{a.name} * {b.name}', new_start, new_end) + + +def main(): + x = BitVec32('x') + w = wrange_mul( + # {1, 2, 3} + Wrange32('w1', start=BitVecVal32(1), end=BitVecVal32(3)), + # - {0} + Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(0)), + ) # = {0} + print('Checking {1, 2, 3} * {0} = {0}') + prove( #x can only be 0 + w.contains(x) == (x == BitVecVal32(0)) + ) + + w = wrange_mul( + # {0xfff0..0xffff} + Wrange32('w1', start=BitVecVal32(0xff0), end=BitVecVal32(0xfff)), + # - {0xf0..0xff} + Wrange32('w2', start=BitVecVal32(0xf0), end=BitVecVal32(0xff)), + ) # = {0xeff100..0xfeff01} + print('Checking {0xff0..0xfff} * {0xf0..0xff} = {0xef100..0xfef01}') + prove( # 0xef100 <= x <= 0xfef01 + w.contains(x) == And(ULE(BitVecVal32(0xef100), x), ULE(x, BitVecVal32(0xfef01))) + ) + + # Multiplication is not implemented when there's negative number, but it + # could be made to work + w = wrange_mul( + # {-1} + Wrange32('w1', start=BitVecVal32(-1), end=BitVecVal32(-1)), + # * {0, 1, 2} + Wrange32('w2', start=BitVecVal32(0), end=BitVecVal32(2)), + ) # = {-2, -1, 0} + print('\nChecking {-1} * {0, 1, 2} = {S32_MIN..S32_MAX}') + prove( + w.contains(x) == BoolVal(True), + ) + + # A general check to make sure wrange_mul() is sound + w1 = Wrange32('w1') + w2 = Wrange32('w2') + w = wrange_mul(w1, w2) + x = BitVec32('x') + y = BitVec32('y') + premise = And( + w1.wellformed(), + w2.wellformed(), + w1.contains(x), + w2.contains(y), + ) + # Suppose we have a wrange32 called w1 that contains the 32-bit integer x + # (where x can be any possible value contained inside w1), and another + # wrange32 called w2 that similarly contains 32-bit integer y. + # + # The product of w1 and w2 calculated from wrange32_mul(w1, w2), called w, + # should _always_ contains the product of x and y, no matter what. + print('\nChecking that if w1.contains(x) and w2.contains(y), then wrange32_mul(w1, w2).contains(x*y)') + print('(note: this takes a very, very, long time to run)') + prove( + Implies( + premise, + And( + w.contains(x * y), + w.wellformed(), + ), + ) + ) + +if __name__ == '__main__': + main() From patchwork Wed Nov 8 05:46:11 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Shung-Hsi Yu X-Patchwork-Id: 13449564 X-Patchwork-Delegate: bpf@iogearbox.net Received: from lindbergh.monkeyblade.net (lindbergh.monkeyblade.net [23.128.96.19]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by smtp.subspace.kernel.org (Postfix) with ESMTPS id 64320C8FD for ; Wed, 8 Nov 2023 05:47:20 +0000 (UTC) Authentication-Results: smtp.subspace.kernel.org; dkim=pass (2048-bit key) header.d=suse.com header.i=@suse.com header.b="IAy8GGxI" Received: from EUR03-DBA-obe.outbound.protection.outlook.com (mail-dbaeur03on2089.outbound.protection.outlook.com [40.107.104.89]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 91D551709 for ; Tue, 7 Nov 2023 21:47:19 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=T3/ys56EfBg/0GmRHCpsLin0uzvcOHDf7utF8N+In4D4TudFCHVWwtoVjYWeTJFdgACLbD5gtMHTnHY0Z53ZAb5FQOltNox99AY1/qS4TF214GDqj97ZPh9FCZeUmmnPe/coY7czxTXSx4bMuSRa1qNK6ICHEuDT2t4Nxm7uuSJVrI1obLvzBy2GO2j88GtJVUUPEstndGRAvxSGoLc4hkwSVk3Tk6h7pRgZcIKvH6pK2vyPhlvCg/WKI+w07IJ4TYs/J2VwG6PkKnP4vSDNZNNIP9MDroKduLbEB6ht24cicAfOWLdreogKBYmwwdvZrFKVPYdCtKSUPJRu/FzwWg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=+jKmUCG8VbuXO7u32x/KWAKrtykMsgwTAgsIJtzwysY=; b=P0cpI75fwNRdPMcd8xnw0zPoRc3oHR2SbTYfuArN58QCYEr9wGvuWnK4g7fXcbdbqbIfZetd5EkWW3m9gmF6ob6vNYltE1N+M13qhga4D13AxXhulxEJAF/1uyg9/81PdTiuwclfKCUaPf1gpMYfU//8wSNWe5miGxvR65FaxGenHNKDSA1uQTQeiCO3S5UC8cOeVBxsCTkAkfQpcY/2FfaaboutXLs2WlxxIsBitxhoafkCa3oB1lO31einfqIt9S9WJz5cBwpe91eURkz2HQch4b68lR/q6+Goo4YjEz4n1wGpbD8RaO/xM4tK2VgP9WX2H22HBvZ8Hg736fxwOQ== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=suse.com; dmarc=pass action=none header.from=suse.com; dkim=pass header.d=suse.com; arc=none DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=suse.com; s=selector1; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=+jKmUCG8VbuXO7u32x/KWAKrtykMsgwTAgsIJtzwysY=; b=IAy8GGxIrh/rolKBuoNmI6mx4wGPvoRX4zvwgAjp7afOj9TZO+k7++k4e5nnqQE8D5SlKOmV3jLqLPCt/3qI5URi9E/BFMTDEnktp4NCUWLmL6jGq0jTBiSHvi9FuBxmdTHCWbAEA1K4aMhufVpFl8Ghmy3MasLZObMOUWtYKRVpQ+xWaueYtiUA6SsSoIal2N/hrRdoDmR5cIe1AfJQoTEY5ek/9nbh+3zwjCDAiTASoW/0A7+okzbw7NI3kYSfLMzYctVE1z/Vqj+XaVMZP0X5Brq/SAdM6/aLkTzGGHR4g7/xyLrF4z6OdaTfxcsyoYVcUxqOwt8GABr0ZZxQrg== Authentication-Results: dkim=none (message not signed) header.d=none;dmarc=none action=none header.from=suse.com; Received: from AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) by AS8PR04MB7816.eurprd04.prod.outlook.com (2603:10a6:20b:2a3::5) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.6977.17; Wed, 8 Nov 2023 05:47:17 +0000 Received: from AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1]) by AS8PR04MB9510.eurprd04.prod.outlook.com ([fe80::24f2:1041:ddd8:39f1%6]) with mapi id 15.20.6977.018; Wed, 8 Nov 2023 05:47:17 +0000 From: Shung-Hsi Yu To: bpf@vger.kernel.org Cc: Shung-Hsi Yu , Andrii Nakryiko , Eduard Zingerman , Yonghong Song , Alexei Starovoitov , Daniel Borkmann , John Fastabend , Paul Chaignon Subject: [RFC bpf-next v0 7/7] (WIP) Add helper functions that transform wrange32 to and from smin/smax/umin/umax Date: Wed, 8 Nov 2023 13:46:11 +0800 Message-ID: <20231108054611.19531-8-shung-hsi.yu@suse.com> X-Mailer: git-send-email 2.42.0 In-Reply-To: <20231108054611.19531-1-shung-hsi.yu@suse.com> References: <20231108054611.19531-1-shung-hsi.yu@suse.com> X-ClientProxiedBy: TYCP286CA0329.JPNP286.PROD.OUTLOOK.COM (2603:1096:400:3b7::13) To AS8PR04MB9510.eurprd04.prod.outlook.com (2603:10a6:20b:44a::11) Precedence: bulk X-Mailing-List: bpf@vger.kernel.org List-Id: List-Subscribe: List-Unsubscribe: MIME-Version: 1.0 X-MS-PublicTrafficType: Email X-MS-TrafficTypeDiagnostic: AS8PR04MB9510:EE_|AS8PR04MB7816:EE_ X-MS-Office365-Filtering-Correlation-Id: a0a8bd74-878b-4f74-db11-08dbe01e2ac2 X-MS-Exchange-SenderADCheck: 1 X-MS-Exchange-AntiSpam-Relay: 0 X-Microsoft-Antispam: BCL:0; X-Microsoft-Antispam-Message-Info: 7hkFf3kRD6WlIeX9IIjffSkw+d3D8xnnMEfrudh8l2L0Su+1T5pYI1TmKGroYq5t/iKJ+dVFSUdlf88lahixIrWG12Q7y7xce4tkjEEhmQQORJIHfcJ2g66lP48eyg+9xZmh8O7JH7kCjGfcUTXsAwQ8o7rRzdso50w9iIF93oFfL7qFqduDN4xXb3jd8QiRovNdMNh/EL5xWeTsJy4OulqgdeJXPxhXGeQuE225h5IyO6gjKPKLDMp921bwKj7LOTE1QuXG1mgI3vJ9WCotSDaDbwtUdqZrrJnNZxNpxWIZ1sSnbpvmuriLX1rN+HWXTHQg9FfYt8yvwTdU1MZISG4xTVi6bF4EntCAoNSLnYfFXYPg7dzNn6uQ7ZgRg88yz2LilGz7fW/lOqJaRaj3tQMPhW8yyvzhd4gXgEgHVRHQ9kGdxsOGrwazMQL1SBSJkO67pMGZjq6NzonJNRhfnsWlsf17BfAVJfxIva9yTCK9m+jLNWKRqK4kdDZKhFoieDeMwv7LqjVBWT6AnyIJof2Z1BuJJ+dYVMv4OAJHnV11GV1zTa85jf7GuVo/vxxF X-Forefront-Antispam-Report: CIP:255.255.255.255;CTRY:;LANG:en;SCL:1;SRV:;IPV:NLI;SFV:NSPM;H:AS8PR04MB9510.eurprd04.prod.outlook.com;PTR:;CAT:NONE;SFS:(13230031)(376002)(366004)(136003)(39860400002)(396003)(346002)(230922051799003)(1800799009)(451199024)(186009)(64100799003)(5660300002)(8936002)(6916009)(4326008)(8676002)(6486002)(6506007)(316002)(54906003)(83380400001)(66556008)(66476007)(36756003)(38100700002)(41300700001)(2906002)(86362001)(66946007)(2616005)(1076003)(6666004)(6512007)(478600001);DIR:OUT;SFP:1101; X-MS-Exchange-AntiSpam-MessageData-ChunkCount: 1 X-MS-Exchange-AntiSpam-MessageData-0: 2CgkDNIfbYczwZacKxy3+bQ3/IDNm2mC2Vcaufh9/Csv2y9hqJd04wvsWj7tm86IWGF9B90dLl/rPKlOaMEUCu/9lXdHW9iyRrcUC0yvPZoBtCvw2TFq1tslBLdqxTodtZ8CDgww9SGBPSHJv0G2++NqvzCmetuXL9ENBvEkWbf5YNc7iV9cFjXtL5AeTWF4LMlivso5NCwEYwCjYtecFliDY+g1SGwNxF2nxojdL9fCZr/cYu0FZfd2cPDxw9bJxJ+Sn6Fa0DPpG+fyO0xc0/ks+i0XuNySJPwOimhWlrgAI3B4BQCyEcYtW+ePhY+oMu9220Lh4GwaSkPTdUrQJeYcQVhuq3YF2iN6vNiuhAkZ/y6Y5n2BH4RxjBX3wGjbNyiOY6Zv1OlSdAT+spMOV+QTD0d8vLMmtqXq2RoCphrzilb5I6Vo60Ey1LjbbE9l1281be43xOQxHiIlx/E+aSEZwd2wQ5KMHphwXoxZmJvP8NiSOJANIXjEFwuLsZAJ5g03aXXAxAPNcEleJIo0VMoEBB2JxQF53OTFJN9kA5xLF3+X7gMFDPGkVOmKJ4tPgYXL6kODcofu4TBNnbkewZA64loAdAJJBNFXb3THEG5zJ7qDK8cSRk0dQFoZLhWTQizkLG3VmpM8l2IK/0O5sJRqFBqFMHa82hx5SMfZHt76cNRpMIZfkkVwlKhJcN+0p5u5R2M+8xI/2SnA7GL0kVd6PDrV/v8gtfVyiHkIku/wVsz9fUgIyzFGtdCn19Ihas8ExTkHaCe6SfDTRSP30OD+6qSmJYU02M1r1iOcvaaPjS0D8oSlSpHO95uSw0z8FuiHaDpX9dZexnNnRd9gA/iIRYNd3Bk6AjDhB3Alyh3FSz2y71wbeAXcyCDr/lCwtM7dE/4mJmS+Y3PDOwYUr9WIvnzorlwPliZ4l0lqeK6IiFZZFmXFPd74XEkRane8wwB5tPr8bd/CUd5AgK4Ns1S5sn1LqEGhNgiM7ZAgxSOv1pmHcYzyks2+EjqI/irgT5czYkxCtxWEM1WbMHLWhOHA4fkqt2EcTgrNkafxK53zGYEyM3h7mdcUuFUODW3ikGYZyQP0y2S1Ax17dN8fDcDM0fURf89jiUlUzj4nZg25XJX3+KTWmGwGN5igzRhdncNxGxf2WjZWNHKLR6qtQ1RWTG7dBOWzzF2Vb+B6jSs7sxwTQ0WpneUFU1onJoNvbt9D83ipQNnqtFQ1AgtalvyCzMBGEmIEZqRNgQ60C9vjp+ezpSHD1HN382T4Fpoe5AD7Em5nZCIk/I8e0ePTWmy0zQizOa0NqE5p3C7baMvU0g5N4dULFGZDba/Az5SEFr3N4LetpzAVgiLBRofcZlHsLQOzEmx6rfmNreXO2XVcY4ivu1hBhTKOA8sDSvIOmfMh+JrjJxCA0WtzCK7eVqU64n+J4IGg+4OEwZyrjfXDXmQmM61rZsmkeRWmM1mHIiJbuWWtErAaXgBuVgxd6DAkW+xOJ3EUA1D5mnPqw+kptHTvwxI9xk6GHrR/wYvIru7TLUpJqM3VQDXG1sXPrwSEOjMPPkrO3owbh4OMATUtOI/bKvODeC9m8vhC6EjYvjCeQEpHC3Kyp/0w5/IvkHlN1jTD6iXOXo5ZsN0gG0C3VbxZ76YVmZmxsykIVCfmtpTLD1KyTJ6pr/W8axmkrw== X-OriginatorOrg: suse.com X-MS-Exchange-CrossTenant-Network-Message-Id: a0a8bd74-878b-4f74-db11-08dbe01e2ac2 X-MS-Exchange-CrossTenant-AuthSource: AS8PR04MB9510.eurprd04.prod.outlook.com X-MS-Exchange-CrossTenant-AuthAs: Internal X-MS-Exchange-CrossTenant-OriginalArrivalTime: 08 Nov 2023 05:47:17.5557 (UTC) X-MS-Exchange-CrossTenant-FromEntityHeader: Hosted X-MS-Exchange-CrossTenant-Id: f7a17af6-1c5c-4a36-aa8b-f5be247aa4ba X-MS-Exchange-CrossTenant-MailboxType: HOSTED X-MS-Exchange-CrossTenant-UserPrincipalName: rulMWPYkQ1N/c91RVwfDo3PMZgjTM4JFNNyFmLJg/eNpvvJ99TTsNPw4uZKWlciaIrBTL005XKze+gHQe50W7g== X-MS-Exchange-Transport-CrossTenantHeadersStamped: AS8PR04MB7816 X-Patchwork-Delegate: bpf@iogearbox.net X-Patchwork-State: RFC To check how wrange32 logic interacts with current verifier codebase, it is necessary to try integrating it as soon as possible in order to take advantange of the selftests we have. One way for this to be done is by adding a helper function that takes smin/smax/umin/umax from bpf_reg_state and turn them into wrange32, then do calculation in wrange32_{add,sub,mul} instead of scalar32_min_max_{add,sub,mul}, and turn the resulting wrange32 back into smin/smax/umin/umax with another helper function. wrange32_to_min_max() is easy and readily available, however I'm still working on wrange32_from_min_max(), which is trickier. Signed-off-by: Shung-Hsi Yu --- include/linux/wrange.h | 6 ++++++ kernel/bpf/wrange.c | 16 ++++++++++++++++ 2 files changed, 22 insertions(+) diff --git a/include/linux/wrange.h b/include/linux/wrange.h index 45d3db3f518b..cecdecefab53 100644 --- a/include/linux/wrange.h +++ b/include/linux/wrange.h @@ -11,6 +11,12 @@ struct wrange32 { u32 end; }; +/* Create wrange32 from bpf_reg_state's s32_min/s32_max/u32_min/u32_max */ +struct wrange32 wrange32_from_min_max(s32 s32_min, s32 s32_max, + u32 u32_min, u32 u32_max); +/* Turn wrange32 back into s32_min/s32_max/u32_min/u32_max */ +void wrange32_to_min_max(struct wrange32 w, s32 *s32_min, s32 *s32_max, + u32 *u32_min, u32 *u32_max); struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b); struct wrange32 wrange32_sub(struct wrange32 a, struct wrange32 b); struct wrange32 wrange32_mul(struct wrange32 a, struct wrange32 b); diff --git a/kernel/bpf/wrange.c b/kernel/bpf/wrange.c index 4ca253e55743..c150efb42cd2 100644 --- a/kernel/bpf/wrange.c +++ b/kernel/bpf/wrange.c @@ -3,6 +3,22 @@ #define WRANGE32(_s, _e) ((struct wrange32) {.start = _s, .end = _e}) +struct wrange32 wrange32_from_min_max(s32 s32_min, s32 s32_max, + u32 u32_min, u32 u32_max) +{ + /* To be implemented */ + return WRANGE32(U32_MIN, U32_MAX); +} + +void wrange32_to_min_max(struct wrange32 w, s32 *s32_min, s32 *s32_max, + u32 *u32_min, u32 *u32_max) +{ + *s32_min = wrange32_smin(w); + *s32_max = wrange32_smax(w); + *u32_min = wrange32_umin(w); + *u32_max = wrange32_umax(w); +} + struct wrange32 wrange32_add(struct wrange32 a, struct wrange32 b) { u32 a_len = a.end - a.start;