From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.0 (2014-02-07) on aws-us-west-2-korg-lkml-1.web.codeaurora.org X-Spam-Level: X-Spam-Status: No, score=-8.6 required=3.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,MENTIONS_GIT_HOSTING, SIGNED_OFF_BY,SPF_HELO_NONE,SPF_PASS autolearn=ham autolearn_force=no version=3.4.0 Received: from mail.kernel.org (mail.kernel.org [198.145.29.99]) by smtp.lore.kernel.org (Postfix) with ESMTP id 14FD1C43603 for ; Tue, 10 Dec 2019 05:32:58 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [209.132.180.67]) by mail.kernel.org (Postfix) with ESMTP id D80B32077B for ; Tue, 10 Dec 2019 05:32:57 +0000 (UTC) Authentication-Results: mail.kernel.org; dkim=pass (2048-bit key) header.d=gmail.com header.i=@gmail.com header.b="qo5TxFS7" Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S1726831AbfLJFc5 (ORCPT ); Tue, 10 Dec 2019 00:32:57 -0500 Received: from mail-qt1-f195.google.com ([209.85.160.195]:38556 "EHLO mail-qt1-f195.google.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S1726824AbfLJFc5 (ORCPT ); Tue, 10 Dec 2019 00:32:57 -0500 Received: by mail-qt1-f195.google.com with SMTP id z15so1698072qts.5; Mon, 09 Dec 2019 21:32:56 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=pARBlMYqvOprGNNaD4cEJATEpLkcbgueMuYWWsX5QXM=; b=qo5TxFS7WobJt6/HnO+0OYNxmZnhCYVjZrLKJQoSbO6lrnLMxe6KlfvBB8frB3mo7B oGW2M1VX04Z3YpVqCragD302lQgoQgJNiThPAXQEtDqn1zTrVBZaFVcEjjEKcATjLazG AFabANzyETfrDtYMzu/wljj1p+KGt9702LDCxXGqZGQT4bYkFENJMRm8JJ8URwWp4At1 KZWlwOq18kvX482nrd/PRv4UdnK0kowOVVVCHz89VcoG6G3n86NOQUYrukup60HbJJsf XoLT+xUpuOev5TEuAhnQvRion06QwWyacY86hI/JgaGhEwtgd6BUk1GboWUmg11dtxfA yNIw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc:content-transfer-encoding; bh=pARBlMYqvOprGNNaD4cEJATEpLkcbgueMuYWWsX5QXM=; b=Ju75RcmZRaTwCpH8hWTJSLF1CzzpvYRDpppzODS+6/weLWM6Rzp1baf8ylO51/O4cP afeu/Mz2kEMf6s5Gumq/KMWrdRHYVBTSJz40I9FYIp/DrXYI1IniKk/uaRbGm/RPBXpr T4W+pmEqPj5EpD+9xw2qxHfHPRY09U5lYF7PRrqeBEdlIu9NorDx4ivREg3t4rXZclFH XZzSWwPh7nFoVWkisIY0biSEchzmiy+2eq9wwzH9WtYH2KJiYo+byF/LWCVgtwfDPr35 n4KoHUVemcfj7VFWNodHUYFFch4Nz4iT38bteCiOFCNeKAEj222ES+80dYyB9pf3aEN7 aCHQ== X-Gm-Message-State: APjAAAXrXu1K5KcrTelzG9JLz9Qv347sPd2XZ5os2z8zXV8gXVutxTsR x9FXGER4PnJTZYyA+XRG4SQ53K7W3vk0QpHpeKK/VYcFcgo= X-Google-Smtp-Source: APXvYqydE5ONyFyL4aFxrLVjR7W3kXqSnLjySLRaNX/it6I4quzW8g9mDD+vUVD7IBAjUumwGv2vuVfqDbY8nSsKWso= X-Received: by 2002:ac8:34b5:: with SMTP id w50mr1645379qtb.107.1575955975988; Mon, 09 Dec 2019 21:32:55 -0800 (PST) MIME-Version: 1.0 References: <20191209173136.29615-1-bjorn.topel@gmail.com> <20191209173136.29615-3-bjorn.topel@gmail.com> In-Reply-To: From: =?UTF-8?B?QmrDtnJuIFTDtnBlbA==?= Date: Tue, 10 Dec 2019 06:32:45 +0100 Message-ID: Subject: Re: [PATCH bpf-next 2/8] riscv, bpf: add support for far branching To: Luke Nelson Cc: Daniel Borkmann , Alexei Starovoitov , Netdev , linux-riscv@lists.infradead.org, bpf , Xi Wang Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Sender: bpf-owner@vger.kernel.org Precedence: bulk List-ID: X-Mailing-List: bpf@vger.kernel.org On Mon, 9 Dec 2019 at 22:08, Luke Nelson wrote= : > > On Mon, Dec 9, 2019 at 9:32 AM Bj=C3=B6rn T=C3=B6pel wrote: > > > > This commit adds branch relaxation to the BPF JIT, and with that > > support for far (offset greater than 12b) branching. > > > > The branch relaxation requires more than two passes to converge. For > > most programs it is three passes, but for larger programs it can be > > more. > > > > Signed-off-by: Bj=C3=B6rn T=C3=B6pel > > We have been developing a formal verification tool for BPF JIT > compilers, which we have used in the past to find bugs in the RV64 > and x32 BPF JITs: > > https://unsat.cs.washington.edu/projects/serval/ > > Recently I added support for verifying the JIT for branch and jump > instructions, and thought it a good opportunity to verify these > patches that add support for far jumps and branching. > > I ported these patches to our tool and ran verification, which > didn't find any bugs according to our specification of BPF and > RISC-V. > > The tool and code are publicly available, and you can read a more > detailed writeup of the results here: > > https://github.com/uw-unsat/bpf-jit-verif/tree/far-jump-review > > Currently the tool works on a manually translated version of the > JIT from C to Rosette, but we are experimenting with ways of making > this process more automated. > > > Reviewed-by: Luke Nelson > Cc: Xi Wang Wow! Very cool! Thanks a bunch for this!