From patchwork Sat Apr 10 13:30:38 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195595 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 06A4EC433B4 for ; Sat, 10 Apr 2021 13:30:56 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id D63AE61028 for ; Sat, 10 Apr 2021 13:30:55 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234804AbhDJNbI (ORCPT ); Sat, 10 Apr 2021 09:31:08 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43916 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234787AbhDJNbI (ORCPT ); Sat, 10 Apr 2021 09:31:08 -0400 Received: from mail-ej1-x62c.google.com (mail-ej1-x62c.google.com [IPv6:2a00:1450:4864:20::62c]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 814E3C061762 for ; Sat, 10 Apr 2021 06:30:53 -0700 (PDT) Received: by mail-ej1-x62c.google.com with SMTP id hq27so12888270ejc.9 for ; Sat, 10 Apr 2021 06:30:53 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=E1CyvQ3rcA3EwKZ3tbg1dtAI0Np9tyHVPkeNJqPwGVU=; b=B9fF6SOWTLKc84Pzhcld1RK8KvZI/Ie7L6KJto5RiV/qAKsWH/Q31CqHNeP30OQBw3 Gv4JU9Hf7zvZ/oGlYhU/rpzyzkLGJvZFegV2PNnpdtsRbxlO7h9BdtFqhZPVw4Pw0Fid tYKqXt5i7MoMz71TwUZthtAJzqzagDVGwy9q2DdQ2FcKAQEB7JOTrHEKVS9uoksdoWCL JXu0FtYtN1GX9fbXY2A5avAUU3dPlFlK3tAOmJNon2OgUBOV+1K/iLiUH79ufsOnsiRT evolouEDKfz5kf8F7nNr2tItHBAhndmMo3m46jE9TdRheRO2RoJxGw2RajXr/cmtJ1qK 6ASg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=E1CyvQ3rcA3EwKZ3tbg1dtAI0Np9tyHVPkeNJqPwGVU=; b=bJf30xQ4UPeZgKmlDDWwwd6sT39dODl0iesYPutKYrO5TE6GGESzpkcfJqGi5AIjN8 aR+Zn4WOy3+z2RGYggaa2Cq6qQXjfeqPuiyQNKttXUKlv7RuFjrTHFRy/kP5Z6P1MgGG ZsL21Z2tndhq4Q+n0zBhNGqorSIIVyAixyltVP0gulxt0+cUMZPkrK1C+cNxr/VN+c33 j6wuDbOlSe0bQP8IjIOlfs2UbQJvyc6p1AvpDbaoOpbnsW0xl6F5etQ7GMqP690hZqQS OZ9313hOhqD/weSVymHyknfuf1+8cBNjUuv3X39S3JWmUYI7VfD+AvnQHtBuPaB4/Wix zjbA== X-Gm-Message-State: AOAM530HOiQq4aq3B7tLQvjD+xXDVwcw08eT6OZ6+0N4a7YkSHKfARMd gLrSMIe1L+srY95b8ZAkC9MAIeYRlBs= X-Google-Smtp-Source: ABdhPJzYAEDvz1aEOxqJsylExaEFAAlheQzj7LE9rz7mmv/cZ1MuCj/fieh64qa5g9fvlDw3xo8Hfw== X-Received: by 2002:a17:906:6683:: with SMTP id z3mr20289630ejo.390.1618061452244; Sat, 10 Apr 2021 06:30:52 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.51 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:51 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 1/8] export declare_builtins() Date: Sat, 10 Apr 2021 15:30:38 +0200 Message-Id: <20210410133045.53189-2-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org Make declare_builtins() extern so that it can be used from other files. Signed-off-by: Luc Van Oostenryck --- builtin.c | 2 +- builtin.h | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/builtin.c b/builtin.c index c7e7da3b1b7b..ff03dbab9a06 100644 --- a/builtin.c +++ b/builtin.c @@ -559,7 +559,7 @@ static void declare_builtin(int stream, const struct builtin_fn *entry) } } -static void declare_builtins(int stream, const struct builtin_fn tbl[]) +void declare_builtins(int stream, const struct builtin_fn tbl[]) { if (!tbl) return; diff --git a/builtin.h b/builtin.h index d0d3fd2ccf87..9cb6728444fe 100644 --- a/builtin.h +++ b/builtin.h @@ -12,4 +12,6 @@ struct builtin_fn { struct symbol_op *op; }; +void declare_builtins(int stream, const struct builtin_fn tbl[]); + #endif From patchwork Sat Apr 10 13:30:39 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195597 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 ADD20C433B4 for ; Sat, 10 Apr 2021 13:30:58 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 8D4C561028 for ; Sat, 10 Apr 2021 13:30:58 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234808AbhDJNbM (ORCPT ); Sat, 10 Apr 2021 09:31:12 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43920 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234805AbhDJNbJ (ORCPT ); Sat, 10 Apr 2021 09:31:09 -0400 Received: from mail-ej1-x636.google.com (mail-ej1-x636.google.com [IPv6:2a00:1450:4864:20::636]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 73D45C061762 for ; Sat, 10 Apr 2021 06:30:54 -0700 (PDT) Received: by mail-ej1-x636.google.com with SMTP id sd23so4252977ejb.12 for ; Sat, 10 Apr 2021 06:30:54 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=oXBP0BK4rvrYi98UKOMLaLbLxhBUv2Q9UXrRM1XKjNs=; b=O3naIuZ0RD+d3n5ncJ0CSATT/IrGXqm02hnx8RU2KxKZaq+Huh1wgCIG+zUMZkX16d qPzhfEn6O1IlApqV7hyKMu+VKvhvaQfLLo0Me8wvJ6SXPwfSZ50OSAHwgE/8E4IRq3rc i580TS/B153LPK1CiHYUjX2k7/UtCfNz075wzscipGb5GNbnbM7RAMhk3+OFmhe04Is6 k247osq6NkfPzSwEUCznBJTjPY6hel+xy/tmsvWcvHSvC8NBi2CVvaSpnSO1TE6Vfqn6 kMrFz5KvGKbC+qvLZ9nK5393dzqSo4ntJrGxvXpgIbVOtwmjOTp9lO+rkcP4HwbahH8Y iG5g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=oXBP0BK4rvrYi98UKOMLaLbLxhBUv2Q9UXrRM1XKjNs=; b=dAXtkLqF5RS+bbTHiogLbVnk+Ju3VXLXWA9u/1iTbpb7W9cm6bwZStaQd7bRRymIh9 J2hg2i/f2WNdJpRXopEyyBSSHAVR/9dQizm9zPi7IA3lRfXhFApnRYXbC30PLB6S4MfY QSJosMC+JAFYKtzBBWBfsZlLV7U2UM7h4d9KJ6oUrYzlhwLM0fSDejX0pZxL7HQwsXvh d+oLoddJazgwOg690n+StCI1n+eo55zxH0gkZIvdYR0AQGsxbBBk0Iku0vVTihS3Y5XW l/68UGnYGd0txpqCC6scenvhb5yE8CBc0RlIX3qPJRvFJE9cOKPKfx7KHQUoeATprrjy tziA== X-Gm-Message-State: AOAM532BjKat4qfvg1DB9Wiutjuu4cFYAmmeT5lD8Hf0QQdcnWA7K8xs o+FQ9dvS+sSSpad/JBO7jsSRkEgL/9o= X-Google-Smtp-Source: ABdhPJxG9dYt9AZJDtXD8nR822k9VqYmWjHqYq+iDyXBjXtTmqaHnUS6RpYRBFI0MiWX2GR162sKFA== X-Received: by 2002:a17:906:37da:: with SMTP id o26mr672788ejc.413.1618061453306; Sat, 10 Apr 2021 06:30:53 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.52 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:52 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 2/8] builtin: define a symbol_op for a generic op acting on integer Date: Sat, 10 Apr 2021 15:30:39 +0200 Message-Id: <20210410133045.53189-3-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org This can be used to define some generic (polymorphic) builtin with a signature like: op(T) op(T, T) op(T,T, ... T) where T is some integer type. Signed-off-by: Luc Van Oostenryck --- builtin.c | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++ builtin.h | 2 ++ 2 files changed, 52 insertions(+) diff --git a/builtin.c b/builtin.c index ff03dbab9a06..f03bf109c818 100644 --- a/builtin.c +++ b/builtin.c @@ -390,6 +390,56 @@ static struct symbol_op overflow_p_op = { }; +/// +// Evaluate the arguments of 'generic' integer operators. +// +// All arguments must be the same basic integer type and +// their number comes from the prototype and is already checked. +static int evaluate_generic_int_op(struct expression *expr) +{ + struct symbol *fntype = expr->fn->ctype->ctype.base_type; + struct symbol_list *types = NULL; + struct symbol *ctype = NULL; + struct expression *arg; + struct symbol *t; + int n = 0; + + PREPARE_PTR_LIST(fntype->arguments, t); + FOR_EACH_PTR(expr->args, arg) { + struct symbol *type; + + if (++n == 1) { + t = arg->ctype; + if (!arg || !(type = arg->ctype)) + return 0; + if (type->type == SYM_NODE) + type = type->ctype.base_type; + if (!type) + return 0; + if (type->ctype.base_type != &int_type || type == &bool_ctype) + goto err; + } else { + t = ctype; + } + add_ptr_list(&types, t); + NEXT_PTR_LIST(t); + } END_FOR_EACH_PTR(arg); + FINISH_PTR_LIST(t); + return evaluate_arguments(types, expr->args); + +err: + sparse_error(arg->pos, "non-integer type for argument %d:", n); + info(arg->pos, " %s", show_typename(arg->ctype)); + expr->ctype = &bad_ctype; + return 0; +} + +struct symbol_op generic_int_op = { + .args = args_prototype, + .evaluate = evaluate_generic_int_op, +}; + + static int eval_atomic_common(struct expression *expr) { struct symbol *fntype = expr->fn->ctype->ctype.base_type; diff --git a/builtin.h b/builtin.h index 9cb6728444fe..5fe77c926244 100644 --- a/builtin.h +++ b/builtin.h @@ -14,4 +14,6 @@ struct builtin_fn { void declare_builtins(int stream, const struct builtin_fn tbl[]); +extern struct symbol_op generic_int_op; + #endif From patchwork Sat Apr 10 13:30:40 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195599 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 4F0B0C43460 for ; Sat, 10 Apr 2021 13:30:59 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 285E261028 for ; Sat, 10 Apr 2021 13:30:59 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234787AbhDJNbM (ORCPT ); Sat, 10 Apr 2021 09:31:12 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43928 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234799AbhDJNbK (ORCPT ); Sat, 10 Apr 2021 09:31:10 -0400 Received: from mail-ej1-x632.google.com (mail-ej1-x632.google.com [IPv6:2a00:1450:4864:20::632]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 62E89C061764 for ; Sat, 10 Apr 2021 06:30:55 -0700 (PDT) Received: by mail-ej1-x632.google.com with SMTP id hq27so12888349ejc.9 for ; Sat, 10 Apr 2021 06:30:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=MtBnJvpqiIeBmNYe9hP4F4mtkSRnyV2MSG0yXiMSTMw=; b=fZLbQ3nKarEli+tC2P6Y0GA6gSJV68AC2Br6N3m+qyjkyWO5mZ872uRc0OdR4Hz6fD zaw+PsHAca5wn6SuXlNK8S2wwEBO2e5NHxUBwyX64QTKa9ok6/jXnXU3Jkf4psbL2RfV gbmEGntRjaLqXcPOY+l8ldncKv2jiT2AAd15eeTYa803NvwJQ5M5BVNNXVRA6GykVQG8 9lJZ6ZJcqGlszQnIpTqLPg16u2rWO8Zu3ZF65M7jZXH3ofSkWNgc7+O1GIO3lY9nY8rb TGjf7PPzV4phd+qpMVa3K/eZhMzvLFZAsylGBRknyehASm0qdlxbZqReb9gEHCtufc7V 1shQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=MtBnJvpqiIeBmNYe9hP4F4mtkSRnyV2MSG0yXiMSTMw=; b=tvbNS1Xq3n4GmVnGXqMR1BTcMj8XShCv7i3tF8XyxrhQmcdEntIg708z4HO6srwRXf iE764oAwLLF5h8uYaZkULeoDngyY3A33gXW+XHyaKLp2hDUxzXi2szmcVaGFTjrTQAco flO82YmbdeQ24qJ/W1JL7w3/uo2Wq7rMt5vNlbYe88O9/FKoRTfY4fGAT/SenP1Bik4S bvee9hz1L9w+T6JUORhq//uL51P1kldscsF4ff0Nv1zSXb/JN/LWciGYyrCkaX5lCrHP G8AfYf7CGTXSfJ9NI1ptfZtx7qXXWtr3xwAGAbrp8J4hwhnDSgDBqGCAc23uFIeyTlp9 +Nfw== X-Gm-Message-State: AOAM530jgcSIHqGaxy+Lf+X5A2sOaVouGxKnGQQUNj+R2NuiR323FbVE vCf3aC32HmOzFT85fPYjHWXhc8yH4rY= X-Google-Smtp-Source: ABdhPJwUXcFoLNjEvY40Lsyd9LiXTG4FyZj26U1w2PBCvXW3VyHP7zuFkoNY5s9rGt8nPLSeoc9/ZA== X-Received: by 2002:a17:906:1749:: with SMTP id d9mr19579006eje.12.1618061454195; Sat, 10 Apr 2021 06:30:54 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.53 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:53 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 3/8] .gitignore is a bit too greedy Date: Sat, 10 Apr 2021 15:30:40 +0200 Message-Id: <20210410133045.53189-4-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org The current .gitignore specifies that the generated programs must be ignored. Good. However, this is done by just specifying the name of the program which has the effect of having any files or directories with the same name to be ignored too. This is not intended. Fix this using the pattern '/' instead so that they match in the root folder. Signed-off-by: Luc Van Oostenryck --- .gitignore | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/.gitignore b/.gitignore index 63c74afdb156..6a28fa50f8bb 100644 --- a/.gitignore +++ b/.gitignore @@ -8,25 +8,25 @@ .*.swp # generated -version.h +/version.h # programs -c2xml -compile -ctags -example -graph -obfuscate -sparse -sparse-llvm -semind -test-dissect -test-inspect -test-lexing -test-linearize -test-parsing -test-show-type -test-unssa +/c2xml +/compile +/ctags +/example +/graph +/obfuscate +/semind +/sparse +/sparse-llvm +/test-dissect +/test-inspect +/test-lexing +/test-linearize +/test-parsing +/test-show-type +/test-unssa # tags tags From patchwork Sat Apr 10 13:30:41 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195605 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 344A4C433ED for ; Sat, 10 Apr 2021 13:31:00 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 0C43961028 for ; Sat, 10 Apr 2021 13:31:00 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234786AbhDJNbN (ORCPT ); Sat, 10 Apr 2021 09:31:13 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43936 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234091AbhDJNbM (ORCPT ); Sat, 10 Apr 2021 09:31:12 -0400 Received: from mail-ej1-x635.google.com (mail-ej1-x635.google.com [IPv6:2a00:1450:4864:20::635]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 813AAC061762 for ; Sat, 10 Apr 2021 06:30:57 -0700 (PDT) Received: by mail-ej1-x635.google.com with SMTP id r12so12928559ejr.5 for ; Sat, 10 Apr 2021 06:30:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=//RpLQUnrXKDd0qIHIFVdT2RzkfNuaPo446jPakCDEs=; b=KNKTrs+g9jVnyYS/d8TrEyNRN+eJbfc5wtNDtN0m2VA6vIXL4I4vS+uA4nftB5s32r sKJH3/JGc2PTLdJ9fOZyxds1/Sy98DC/XzpTOnNBIQzOo6XibYVHOc3F0oUSFxlPw76f y8JSKhjlqae84rH7+q7HHjkG2E6T4GCS0C6JpiAG12nkldqHf2nV76vB+1qJCZ5YyFwV 871SIPOuEjpF/QbcGmlXnjdG0R51OAahh1BkRrmLakBpSYP1lhPdWftKTpY9lS2wqsji DRAj395GJu/GK7jM1lmzmoSx3xxMqtTxC5ch4EjgvH1pC/lmmAZByydm1TEnzBXS3BzH 4zHA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=//RpLQUnrXKDd0qIHIFVdT2RzkfNuaPo446jPakCDEs=; b=YgE6pxazT1lckHgdTEGF22FdDf7IfcLBySnh2MbsSsuNOiNgkd1jDazs/MVFwQxi+k wPV/Sl3zzxc+z2GWkzYPvVWyUo9LEmHWkKcyxb8QXDPCeSfaAHZ4PLGJoOtaosPKjIKd Ej8GdVSeOCcYQbrkwMzXvxAYcHuaAv8lKOlI1OmbMcPTt55fvrv+gLOLmp6NMyts6XdD zAdulDQSiCSHf4lC6R89DNUvUU++vXVzIbQZ9gb8EVcmxH4lAQd62uOBn/aZsi65Kh/e 1KVCF3ccOwlFtVCWMHiUnPSRq1Kyhe5R5V9+pB1tuIBBp8dsLbIz2akUdeerU0JlYv3+ 3rLg== X-Gm-Message-State: AOAM533yBjg66TMm1flVQh2lw9buDikOTwnSoOO4TGjGarNylPUxi3lm msJuC37rFfzZAyoQGcObiEBx0sTYtJE= X-Google-Smtp-Source: ABdhPJw455EoDrDf7wRfC8n9BU/brhB6Snr9ltQNH1+tl808thYb2sOhRhsqTSKJUNCHXqgS6eWM+A== X-Received: by 2002:a17:906:4801:: with SMTP id w1mr20174125ejq.475.1618061456228; Sat, 10 Apr 2021 06:30:56 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.55 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:55 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 4/8] scheck: add a symbolic checker Date: Sat, 10 Apr 2021 15:30:41 +0200 Message-Id: <20210410133045.53189-5-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org Some instruction simplifications can be quite tricky and thus easy to get wrong. Often, they also are hard to test (for example, you can test it with a few input values but of course not all combinations). I'm used to validate some of these with an independent tool (Alive cfr. [1], [2]) which is quite neat but has some issues: 1) This tool doesn't work with Sparse's IR or C source but it needs to have the tests written in its own language (very close to LLVM's IR). So it can be used to test if the logic of a simplification but not if implemented correctly. 2) This tool isn't maintained anymore (has some bugs too) and it's successor (Alive2 [3]) is not quite as handy to me (I miss the pre-conditions a lot). So, this patch implement the same idea but fully integrated with Sparse. This mean that you can write a test in C, let Sparse process and simplify it and then directly validate it and not only for a few values but symbolically, for all possible values. Note: Of course, this is not totally stand-alone and depends on an external library for the solver (Boolector, see [4], [5]). Note: Currently, it's just a proof of concept and, except the included tests, it's only very slightly tested (and untested with anything more complex than a few instructions). [1] https://blog.regehr.org/archives/1170 [2] https://www.cs.utah.edu/~regehr/papers/pldi15.pdf [3] https://blog.regehr.org/archives/1722 [4] https://boolector.github.io/ [5] https://boolector.github.io/papers/BrummayerBiere-TACAS09.pdf Signed-off-by: Luc Van Oostenryck --- .gitignore | 1 + Makefile | 7 + ident-list.h | 3 + scheck.c | 302 +++++++++++++++++++++++++++++++++++++++++ validation/scheck/ko.c | 10 ++ validation/scheck/ok.c | 14 ++ validation/test-suite | 6 + 7 files changed, 343 insertions(+) create mode 100644 scheck.c create mode 100644 validation/scheck/ko.c create mode 100644 validation/scheck/ok.c diff --git a/.gitignore b/.gitignore index 6a28fa50f8bb..b22f86b1ddfb 100644 --- a/.gitignore +++ b/.gitignore @@ -17,6 +17,7 @@ /example /graph /obfuscate +/scheck /semind /sparse /sparse-llvm diff --git a/Makefile b/Makefile index f9883da101c7..a0178a65a11a 100644 --- a/Makefile +++ b/Makefile @@ -227,6 +227,13 @@ else $(warning Your system does not have llvm, disabling sparse-llvm) endif +ifeq ($(HAVE_BOOLECTOR),yes) +PROGRAMS += scheck +scheck-cflags := -I${BOOLECTORDIR}/include/boolector +scheck-ldflags := -L${BOOLECTORDIR}/lib +scheck-ldlibs := -lboolector -llgl -lbtor2parser +endif + ######################################################################## LIBS := libsparse.a OBJS := $(LIB_OBJS) $(EXTRA_OBJS) $(PROGRAMS:%=%.o) diff --git a/ident-list.h b/ident-list.h index 8049b6940745..918f54d75fc4 100644 --- a/ident-list.h +++ b/ident-list.h @@ -78,6 +78,9 @@ IDENT(memset); IDENT(memcpy); IDENT(copy_to_user); IDENT(copy_from_user); IDENT(main); +/* used by the symbolic checker */ +IDENT(__assert); + #undef __IDENT #undef IDENT #undef IDENT_RESERVED diff --git a/scheck.c b/scheck.c new file mode 100644 index 000000000000..719aeea84e7c --- /dev/null +++ b/scheck.c @@ -0,0 +1,302 @@ +// SPDX-License-Identifier: MIT +// Copyright (C) 2021 Luc Van Oostenryck + +/// +// Symbolic checker for Sparse's IR +// -------------------------------- +// +// This is an example client program with a dual purpose: +// # It shows how to translate Sparse's IR into the language +// of SMT solvers (only the part concerning integers, +// floating-point and memory is ignored). +// # It's used as a simple symbolic checker for the IR. +// The idea is to create a mini-language that allows to +// express some assertions with some pre-conditions. + +#include +#include +#include +#include +#include +#include +#include + +#include +#include "lib.h" +#include "expression.h" +#include "linearize.h" +#include "symbol.h" +#include "builtin.h" + + +#define dyntype incomplete_ctype +static const struct builtin_fn builtins_scheck[] = { + { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op }, + {} +}; + + +static BoolectorSort get_sort(Btor *btor, struct symbol *type, struct position pos) +{ + if (!is_int_type(type)) { + sparse_error(pos, "invalid type"); + return NULL; + } + return boolector_bitvec_sort(btor, type->bit_size); +} + +static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo) +{ + static char buff[33]; + BoolectorNode *n; + + if (pseudo->priv) + return pseudo->priv; + + switch (pseudo->type) { + case PSEUDO_VAL: + sprintf(buff, "%llx", pseudo->value); + return boolector_consth(btor, s, buff); + case PSEUDO_ARG: + case PSEUDO_REG: + n = boolector_var(btor, s, show_pseudo(pseudo)); + break; + default: + fprintf(stderr, "invalid pseudo: %s\n", show_pseudo(pseudo)); + return NULL; + } + return pseudo->priv = n; +} + +static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx) +{ + pseudo_t arg = ptr_list_nth(insn->arguments, idx); + struct symbol *type = ptr_list_nth(insn->fntypes, idx + 1); + BoolectorSort s = get_sort(btor, type, insn->pos); + + return mkvar(btor, s, arg); +} + +static BoolectorNode *zext(Btor *btor, struct instruction *insn, BoolectorNode *s) +{ + int old = boolector_get_width(btor, s); + int new = insn->type->bit_size; + return boolector_uext(btor, s, new - old); +} + +static BoolectorNode *sext(Btor *btor, struct instruction *insn, BoolectorNode *s) +{ + int old = boolector_get_width(btor, s); + int new = insn->type->bit_size; + return boolector_sext(btor, s, new - old); +} + +static BoolectorNode *slice(Btor *btor, struct instruction *insn, BoolectorNode *s) +{ + int old = boolector_get_width(btor, s); + int new = insn->type->bit_size; + return boolector_slice(btor, s, old - new - 1, 0); +} + +static void binop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + BoolectorNode *t, *a, *b; + + a = mkvar(btor, s, insn->src1); + b = mkvar(btor, s, insn->src2); + if (!a || !b) + return; + switch (insn->opcode) { + case OP_ADD: t = boolector_add(btor, a, b); break; + case OP_SUB: t = boolector_sub(btor, a, b); break; + case OP_MUL: t = boolector_mul(btor, a, b); break; + case OP_AND: t = boolector_and(btor, a, b); break; + case OP_OR: t = boolector_or (btor, a, b); break; + case OP_XOR: t = boolector_xor(btor, a, b); break; + case OP_SHL: t = boolector_sll(btor, a, b); break; + case OP_LSR: t = boolector_srl(btor, a, b); break; + case OP_ASR: t = boolector_sra(btor, a, b); break; + case OP_DIVS: t = boolector_sdiv(btor, a, b); break; + case OP_DIVU: t = boolector_udiv(btor, a, b); break; + case OP_MODS: t = boolector_srem(btor, a, b); break; + case OP_MODU: t = boolector_urem(btor, a, b); break; + case OP_SET_EQ: t = zext(btor, insn, boolector_eq(btor, a, b)); break; + case OP_SET_NE: t = zext(btor, insn, boolector_ne(btor, a, b)); break; + case OP_SET_LT: t = zext(btor, insn, boolector_slt(btor, a, b)); break; + case OP_SET_LE: t = zext(btor, insn, boolector_slte(btor, a, b)); break; + case OP_SET_GE: t = zext(btor, insn, boolector_sgte(btor, a, b)); break; + case OP_SET_GT: t = zext(btor, insn, boolector_sgt(btor, a, b)); break; + case OP_SET_B: t = zext(btor, insn, boolector_ult(btor, a, b)); break; + case OP_SET_BE: t = zext(btor, insn, boolector_ulte(btor, a, b)); break; + case OP_SET_AE: t = zext(btor, insn, boolector_ugte(btor, a, b)); break; + case OP_SET_A: t = zext(btor, insn, boolector_ugt(btor, a, b)); break; + default: + fprintf(stderr, "unsupported insn\n"); + return; + } + insn->target->priv = t; +} + +static void unop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + BoolectorNode *t, *a; + + a = mkvar(btor, s, insn->src1); + if (!a) + return; + switch (insn->opcode) { + case OP_NEG: t = boolector_neg(btor, a); break; + case OP_NOT: t = boolector_not(btor, a); break; + case OP_SEXT: t = sext(btor, insn, a); break; + case OP_ZEXT: t = zext(btor, insn, a); break; + case OP_TRUNC: t = slice(btor, insn, a); break; + default: + fprintf(stderr, "unsupported insn\n"); + return; + } + insn->target->priv = t; +} + +static void ternop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + BoolectorNode *t, *a, *b, *c, *z, *d; + + a = mkvar(btor, s, insn->src1); + b = mkvar(btor, s, insn->src2); + c = mkvar(btor, s, insn->src3); + if (!a || !b || !c) + return; + switch (insn->opcode) { + case OP_SEL: + z = boolector_zero(btor, s); + d = boolector_ne(btor, a, z); + t = boolector_cond(btor, d, b, c); + break; + default: + fprintf(stderr, "unsupported insn\n"); + return; + } + insn->target->priv = t; +} + +static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn) +{ + char model_format[] = "btor"; + int res; + + boolector_assert(btor, boolector_not(btor, n)); + res = boolector_sat(btor); + switch (res) { + case BOOLECTOR_UNSAT: + return 1; + case BOOLECTOR_SAT: + sparse_error(insn->pos, "assertion failed"); + show_entry(insn->bb->ep); + boolector_dump_btor(btor, stdout); + boolector_print_model(btor, model_format, stdout); + break; + default: + sparse_error(insn->pos, "SMT failure"); + break; + } + return 0; +} + +static bool check_assert(Btor *btor, struct instruction *insn) +{ + BoolectorNode *a = get_arg(btor, insn, 0); + BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a)); + BoolectorNode *n = boolector_ne(btor, a, z); + return check_btor(btor, n, insn); +} + +static bool check_call(Btor *btor, struct instruction *insn) +{ + pseudo_t func = insn->func; + struct ident *ident = func->ident; + + if (ident == &__assert_ident) + return check_assert(btor, insn); + return 0; +} + +static bool check_function(struct entrypoint *ep) +{ + Btor *btor = boolector_new(); + struct basic_block *bb; + int rc = 0; + + boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1); + + FOR_EACH_PTR(ep->bbs, bb) { + struct instruction *insn; + FOR_EACH_PTR(bb->insns, insn) { + if (!insn->bb) + continue; + switch (insn->opcode) { + case OP_ENTRY: + continue; + case OP_BINARY ... OP_BINARY_END: + case OP_BINCMP ... OP_BINCMP_END: + binop(btor, insn); + break; + case OP_UNOP ... OP_UNOP_END: + unop(btor, insn); + break; + case OP_SEL: + ternop(btor, insn); + break; + case OP_CALL: + rc = check_call(btor, insn); + goto out; + case OP_RET: + goto out; + default: + fprintf(stderr, "unsupported insn\n"); + goto out; + } + } END_FOR_EACH_PTR(insn); + } END_FOR_EACH_PTR(bb); + fprintf(stderr, "unterminated function\n"); + +out: + boolector_release_all(btor); + boolector_delete(btor); + return rc; +} + +static void check_functions(struct symbol_list *list) +{ + struct symbol *sym; + + FOR_EACH_PTR(list, sym) { + struct entrypoint *ep; + + expand_symbol(sym); + ep = linearize_symbol(sym); + if (!ep || !ep->entry) + continue; + check_function(ep); + } END_FOR_EACH_PTR(sym); +} + +int main(int argc, char **argv) +{ + struct string_list *filelist = NULL; + char *file; + + Wdecl = 0; + + sparse_initialize(argc, argv, &filelist); + + declare_builtins(0, builtins_scheck); + + // Expand, linearize and check. + FOR_EACH_PTR(filelist, file) { + check_functions(sparse(file)); + } END_FOR_EACH_PTR(file); + return 0; +} diff --git a/validation/scheck/ko.c b/validation/scheck/ko.c new file mode 100644 index 000000000000..dbd861ea17fd --- /dev/null +++ b/validation/scheck/ko.c @@ -0,0 +1,10 @@ +static void ko(int x) +{ + __assert((~x) == (~0 + x)); +} + +/* + * check-name: scheck-ko + * check-command: scheck $file + * check-known-to-fail + */ diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c new file mode 100644 index 000000000000..113912e01aad --- /dev/null +++ b/validation/scheck/ok.c @@ -0,0 +1,14 @@ +static void ok(int x) +{ + __assert((~x) == (~0 - x)); // true but not simplified yet +} + +static void always(int x) +{ + __assert((x - x) == 0); // true and simplified +} + +/* + * check-name: scheck-ok + * check-command: scheck $file + */ diff --git a/validation/test-suite b/validation/test-suite index 1b05c75e9f74..2f7950ef50a4 100755 --- a/validation/test-suite +++ b/validation/test-suite @@ -13,6 +13,9 @@ prog_name=`basename $0` if [ ! -x "$default_path/sparse-llvm" ]; then disabled_cmds="sparsec sparsei sparse-llvm sparse-llvm-dis" fi +if [ ! -x "$default_path/scheck" ]; then + disabled_cmds="$disabled_cmds scheck" +fi # flags: # - some tests gave an unexpected result @@ -513,6 +516,7 @@ echo " -a append the created test to the input file" echo " -f write a test known to fail" echo " -l write a test for linearized code" echo " -p write a test for pre-processing" +echo " -s write a test for symbolic checking" echo echo "argument(s):" echo " file file containing the test case(s)" @@ -540,6 +544,8 @@ do_format() linear=1 ;; -p) def_cmd='sparse -E $file' ;; + -s) + def_cmd='scheck $file' ;; help|-*) do_format_help From patchwork Sat Apr 10 13:30:42 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195601 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 6853BC43462 for ; Sat, 10 Apr 2021 13:31:00 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 4947C61028 for ; Sat, 10 Apr 2021 13:31:00 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234805AbhDJNbO (ORCPT ); Sat, 10 Apr 2021 09:31:14 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43940 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234799AbhDJNbN (ORCPT ); Sat, 10 Apr 2021 09:31:13 -0400 Received: from mail-ed1-x530.google.com (mail-ed1-x530.google.com [IPv6:2a00:1450:4864:20::530]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 62CAEC061764 for ; Sat, 10 Apr 2021 06:30:58 -0700 (PDT) Received: by mail-ed1-x530.google.com with SMTP id w23so9685681edx.7 for ; Sat, 10 Apr 2021 06:30:58 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=HY2EdAJWzfL+nIACLIGy1wBD3wzDe0ETwULS8QDsTl4=; b=X/FCLJNHoDw8Nked6JYEoBO9Aug/z1Z6GiruU+JDkuWllKTrtST6eeld5b96mjpbDr jB9ZCdyqYYNDYdd1DSvc8qMKDSTmMSklbGJA/imxRx4Qfe3+Zm4cKRAcD/cJfNGi0exZ jEo19icF+3e/9PzaqsQoTRP9W5tbCgcujnbXBpIqPVKb8RVqVv85HvkFQI+m7k6psmBW 70eiXCjpYV1HgNopRz4xyj1YT76oY759EW+FsGsygoYBoPhiV7d+ZTEFT+DsxU9EYw35 4xOWdJZMxscHsuOIfRjwgA23e7WakAovuD5YTFak7rFbNYi2O8vDqUojBIrDcakZT/pn PeMQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=HY2EdAJWzfL+nIACLIGy1wBD3wzDe0ETwULS8QDsTl4=; b=UHefssHz96eV4aWQbpM7Hqm+JpoZyqxmOIlJsiGtBjkyvMfZL6EPKRfPuMx2MvDcBo IwkHplPnU/whqHK/OhWhu1Ju+NTThcu5zszNW9fCaUF7Lb6gXJDZRtOi5j0oj+yYZbUW XqGf7OlJDXErg0Peo0dLTR7S1YuZOTiAboZT288Ufq9dkyQ0YMFAigXNSjZbJePVGX+F U1SVPt2Y1FzMR227GKrupew34hQlGlLy3VUcAkxX4dJJCJHnWfstisoqkJcbJSF9TK4O g2yk4hi8Rok1WO6OrjlyzvVbqWWDZbYesNr5OZx6PxzFrUDAF5XGdgurfNUuVcVZSQW6 z0xw== X-Gm-Message-State: AOAM532xvCf/seGRQlqD+7vcRM+9eXEfrwQxHwJZPu/X9eSKCCMvN3ww OtHch/Mksu7tl5jC+PfK06pjADq8/wc= X-Google-Smtp-Source: ABdhPJwk2TKKTwA3G343YNHe13nKilYArXuFbSzofemMFCBpYDEdIqK+e4V4FB7WRkEXlghObEQZPQ== X-Received: by 2002:aa7:df13:: with SMTP id c19mr21754954edy.370.1618061457206; Sat, 10 Apr 2021 06:30:57 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.56 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:56 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 5/8] scheck: assert_eq() Date: Sat, 10 Apr 2021 15:30:42 +0200 Message-Id: <20210410133045.53189-6-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org Testing the equivalence of two sub-expressions can be done with with a single assertion like __assert(A == B). However, in some cases, Sparse can use the equality to simplify the whole expression although it's unable to simplify one of the two sub-expressions into the other. So, add a new assertion, __assert_eq(), testing the equality of the two expressions given in argument independently of each other. Signed-off-by: Luc Van Oostenryck --- ident-list.h | 1 + scheck.c | 11 +++++++++++ validation/scheck/ok.c | 5 +++++ 3 files changed, 17 insertions(+) diff --git a/ident-list.h b/ident-list.h index 918f54d75fc4..ab5bc5f52e01 100644 --- a/ident-list.h +++ b/ident-list.h @@ -80,6 +80,7 @@ IDENT(main); /* used by the symbolic checker */ IDENT(__assert); +IDENT(__assert_eq); #undef __IDENT #undef IDENT diff --git a/scheck.c b/scheck.c index 719aeea84e7c..ff91328f681a 100644 --- a/scheck.c +++ b/scheck.c @@ -32,6 +32,7 @@ #define dyntype incomplete_ctype static const struct builtin_fn builtins_scheck[] = { { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op }, + { "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, {} }; @@ -213,6 +214,14 @@ static bool check_assert(Btor *btor, struct instruction *insn) return check_btor(btor, n, insn); } +static bool check_equal(Btor *btor, struct instruction *insn) +{ + BoolectorNode *a = get_arg(btor, insn, 0); + BoolectorNode *b = get_arg(btor, insn, 1); + BoolectorNode *n = boolector_eq(btor, a, b); + return check_btor(btor, n, insn); +} + static bool check_call(Btor *btor, struct instruction *insn) { pseudo_t func = insn->func; @@ -220,6 +229,8 @@ static bool check_call(Btor *btor, struct instruction *insn) if (ident == &__assert_ident) return check_assert(btor, insn); + if (ident == &__assert_eq_ident) + return check_equal(btor, insn); return 0; } diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 113912e01aad..76c04c4f6870 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -3,6 +3,11 @@ static void ok(int x) __assert((~x) == (~0 - x)); // true but not simplified yet } +static void also_ok(int x) +{ + __assert_eq(~x, ~0 - x); +} + static void always(int x) { __assert((x - x) == 0); // true and simplified From patchwork Sat Apr 10 13:30:43 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195603 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 B8D17C43461 for ; Sat, 10 Apr 2021 13:31:00 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 9177361028 for ; Sat, 10 Apr 2021 13:31:00 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234799AbhDJNbO (ORCPT ); Sat, 10 Apr 2021 09:31:14 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43948 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234091AbhDJNbN (ORCPT ); Sat, 10 Apr 2021 09:31:13 -0400 Received: from mail-ej1-x629.google.com (mail-ej1-x629.google.com [IPv6:2a00:1450:4864:20::629]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 4ED68C061762 for ; Sat, 10 Apr 2021 06:30:59 -0700 (PDT) Received: by mail-ej1-x629.google.com with SMTP id r12so12928627ejr.5 for ; Sat, 10 Apr 2021 06:30:59 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=Ut6UAGUaiFV9b9kVlyDir9c4hl23I/6Etf5cntioMcw=; b=erKRyqQZFDOzY/wF2FLHtYFGN367gRNdh7o0Lmz59briF8ipXVTye2g1Ot4vw2BacO rgm6r6qgVIdNP487vFs6znKOKaIVWjtFtzJ0i96ZTkeCPBDswduIC7ws8OSbFjfpj80C BGutz7AHpf6eDecPq1DJa31cVyLAhiofs9zYLvtFN7RIPHMsZGwpLI/2SbBFxQ0JiTs9 qgQKy+gfkg2YtuCGgd+WpoZTAqQiXh1COpYlJyZ0UURbN4ecn6tW/jfuLt3eftF7RzlY BNpW+LjEYhCPgpFvmPVAnFuLJwgpDaM7oxXyrqAL5+LWqTUn4szyADwtICVvVJjsh084 UTcQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=Ut6UAGUaiFV9b9kVlyDir9c4hl23I/6Etf5cntioMcw=; b=nqQsafd2L7Yl7Uwm4zxC2PrQufPZu0H+YLpmnaabqlC+EwG+xveUbQ7Y9stqDqNJS4 BBFt48584hkHunBk+jJXC/dUSD2gcGA4ufCwo99LpXbn+dNBWS/Ocq49sIxD95kDYr2z MOzcwPz/KkvphbKdOdkhsdP1UfVcEgfwPFGTEhp0AGe8jKKrYQqZp0vYcB+KgeYvzTq9 qKFO5am0VxTKke8MOZrQlLnovvVcKDNhGy7GNTt6JyhXUSgv8OtV/fHu7dddKguIIyRd O+3OwDtt4HYs4hvmnYqNIZz2ufjyS6KxfZeB7rH9HrHwu9ZMzSpD+DcrJxxcXf+7z80x MoTQ== X-Gm-Message-State: AOAM532B/N5wza097+iuUSIYDxUILHF7nPMcwiMHl0b/GSlPbXmX+McL 3f4yiDtw7hkK6VGazMIYpItPPUMXFVY= X-Google-Smtp-Source: ABdhPJwONesIwZU8q/3CvDSE6Onhps1eX+t00IGWz6or0YCIhACaLKrypU0I7jhAlKdZp5MQ8iu1IQ== X-Received: by 2002:a17:907:6004:: with SMTP id fs4mr19618711ejc.479.1618061458126; Sat, 10 Apr 2021 06:30:58 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.57 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:57 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 6/8] scheck: allow multiple assertions Date: Sat, 10 Apr 2021 15:30:43 +0200 Message-Id: <20210410133045.53189-7-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org With the SMT solver used here, by default, once an expression is checked it's kinda consumed by the process and can't be reused anymore for another check. So, enable the incremental mode: it allows to call boolecter_sat() several times. Note: Another would be, of course, to just AND together all assertions and just check this but then we would lost the finer grained diagnostic in case of failure. Signed-off-by: Luc Van Oostenryck --- scheck.c | 5 +++-- validation/scheck/ok.c | 4 ---- 2 files changed, 3 insertions(+), 6 deletions(-) diff --git a/scheck.c b/scheck.c index ff91328f681a..26f88a4a028e 100644 --- a/scheck.c +++ b/scheck.c @@ -241,6 +241,7 @@ static bool check_function(struct entrypoint *ep) int rc = 0; boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1); + boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1); FOR_EACH_PTR(ep->bbs, bb) { struct instruction *insn; @@ -261,8 +262,8 @@ static bool check_function(struct entrypoint *ep) ternop(btor, insn); break; case OP_CALL: - rc = check_call(btor, insn); - goto out; + rc &= check_call(btor, insn); + break; case OP_RET: goto out; default: diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 76c04c4f6870..f4a0daabfe9a 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -1,10 +1,6 @@ static void ok(int x) { __assert((~x) == (~0 - x)); // true but not simplified yet -} - -static void also_ok(int x) -{ __assert_eq(~x, ~0 - x); } From patchwork Sat Apr 10 13:30:44 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195607 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 C4B09C433B4 for ; Sat, 10 Apr 2021 13:31:03 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 946FE61028 for ; Sat, 10 Apr 2021 13:31:03 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234807AbhDJNbQ (ORCPT ); Sat, 10 Apr 2021 09:31:16 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43952 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234091AbhDJNbP (ORCPT ); Sat, 10 Apr 2021 09:31:15 -0400 Received: from mail-ej1-x62c.google.com (mail-ej1-x62c.google.com [IPv6:2a00:1450:4864:20::62c]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 51D8CC061762 for ; Sat, 10 Apr 2021 06:31:00 -0700 (PDT) Received: by mail-ej1-x62c.google.com with SMTP id hq27so12888596ejc.9 for ; Sat, 10 Apr 2021 06:31:00 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=XGPFV+OYP7ikzGx0Wa0qXJJq6+m5hh+0ZKKsoGUXT48=; b=R+hCm/RtuSoyUFjCj01kbdDCzPWkfrDue3l3Zj/o+oTHfj/QgdCSZp5XgLi9fbRlYe keFH9rmNbW7yVIT5Kip4jWT9Qe5xzNGWHsDO0FoNfLRwiQn5tW/AX3G3OBRy+GKpUQsX JgKq7vnMHMW7N0mCnIADP2BOpESctzitwOPtCWn6N3IN7UoZpSXLq/7OD9v+X1rzLdIC UqK5ocyQBsLgqW+N9UgOtmXA3Celdjd3C354Rt69H5CzYz5tuMTNgRQfAaAeRbLLkk4O gpF00KkTgFeOUhGT/93G1J8LNJHHoHVRN7DPpSu0fEtuIkmF7SFKvg+XInR0Pera3obu s0uw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=XGPFV+OYP7ikzGx0Wa0qXJJq6+m5hh+0ZKKsoGUXT48=; b=bHxsYHLLEpQz78Uh3U+NFfXrATfMy3UoLm62g8ghyqexdEOuGXYWKVJBZYmVaJOaG6 s3+c8CFlPbQupC4Ns4uKkiqw7TrOSGH8INFeP3eU6klSOaVMHKOREWg1Lk71W6qRqEZn K9U68rkritL1fsmPEmxjO4ignQa7zFV+v2Kv3qkZNp/mEqSdeKxYHGLpY+RHVCNKoOgc XHGwBWjQCk+ijycQTdhYzt/so15B/b48dkDvTASVyTM2PKz4MNuui3OjCpVc8//axC6s +78/9SAHo3v/wicWX9d/17wOsWEEHPsrMINqj96DlMiZwTS22LEbHVDtVg2p/ctLM6vX xe0g== X-Gm-Message-State: AOAM533qlj9TEyM8yqh9MmGRJygMyS0WlDsqclLovRWxQLpS81wBqzBC vsCxD9avOgMtA9z9WJ+5y/kTYpNtnm8= X-Google-Smtp-Source: ABdhPJx2N/divIMkb99/YYKWFMi1nzbG/tW/oOsirLK6zfff9g3pptUUUxAt3pcKn5ECov0kOERP9A== X-Received: by 2002:a17:907:16a8:: with SMTP id hc40mr19915401ejc.40.1618061459095; Sat, 10 Apr 2021 06:30:59 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.58 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:58 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 7/8] scheck: assert_const() Date: Sat, 10 Apr 2021 15:30:44 +0200 Message-Id: <20210410133045.53189-8-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org Since, the symbolic checker check expressions at the ... symbolic level, this can be used to check if two expressions are equivalent but not if this equivalence is effectively used. So, add a new assertion (this time not at the symbolic level) to check if an expression which is expected to simplify to a constant is effectively simplified to this constant. Signed-off-by: Luc Van Oostenryck --- ident-list.h | 1 + scheck.c | 19 +++++++++++++++++++ validation/scheck/ok.c | 1 + 3 files changed, 21 insertions(+) diff --git a/ident-list.h b/ident-list.h index ab5bc5f52e01..6264fd062534 100644 --- a/ident-list.h +++ b/ident-list.h @@ -81,6 +81,7 @@ IDENT(main); /* used by the symbolic checker */ IDENT(__assert); IDENT(__assert_eq); +IDENT(__assert_const); #undef __IDENT #undef IDENT diff --git a/scheck.c b/scheck.c index 26f88a4a028e..ff140aaa1e95 100644 --- a/scheck.c +++ b/scheck.c @@ -33,6 +33,7 @@ static const struct builtin_fn builtins_scheck[] = { { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op }, { "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, + { "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, {} }; @@ -222,6 +223,22 @@ static bool check_equal(Btor *btor, struct instruction *insn) return check_btor(btor, n, insn); } +static bool check_const(Btor *ctxt, struct instruction *insn) +{ + pseudo_t src1 = ptr_list_nth(insn->arguments, 0); + pseudo_t src2 = ptr_list_nth(insn->arguments, 1); + + if (src2->type != PSEUDO_VAL) + sparse_error(insn->pos, "should be a constant: %s", show_pseudo(src2)); + if (src1 == src2) + return 1; + if (src1->type != PSEUDO_VAL) + sparse_error(insn->pos, "not a constant: %s", show_pseudo(src1)); + else + sparse_error(insn->pos, "invalid value: %s != %s", show_pseudo(src1), show_pseudo(src2)); + return 0; +} + static bool check_call(Btor *btor, struct instruction *insn) { pseudo_t func = insn->func; @@ -231,6 +248,8 @@ static bool check_call(Btor *btor, struct instruction *insn) return check_assert(btor, insn); if (ident == &__assert_eq_ident) return check_equal(btor, insn); + if (ident == &__assert_const_ident) + return check_const(btor, insn); return 0; } diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index f4a0daabfe9a..8f65013e1618 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -2,6 +2,7 @@ static void ok(int x) { __assert((~x) == (~0 - x)); // true but not simplified yet __assert_eq(~x, ~0 - x); + __assert_const(x & 0, 0); } static void always(int x) From patchwork Sat Apr 10 13:30:45 2021 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Luc Van Oostenryck X-Patchwork-Id: 12195609 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=-15.7 required=3.0 tests=BAYES_00,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,INCLUDES_CR_TRAILER,INCLUDES_PATCH, MAILING_LIST_MULTI,SPF_HELO_NONE,SPF_PASS,USER_AGENT_GIT 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 640B6C433ED for ; Sat, 10 Apr 2021 13:31:04 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 379D361028 for ; Sat, 10 Apr 2021 13:31:04 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S234091AbhDJNbR (ORCPT ); Sat, 10 Apr 2021 09:31:17 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:43954 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S234806AbhDJNbP (ORCPT ); Sat, 10 Apr 2021 09:31:15 -0400 Received: from mail-ed1-x52d.google.com (mail-ed1-x52d.google.com [IPv6:2a00:1450:4864:20::52d]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 1BEF1C061764 for ; Sat, 10 Apr 2021 06:31:01 -0700 (PDT) Received: by mail-ed1-x52d.google.com with SMTP id x4so9722617edd.2 for ; Sat, 10 Apr 2021 06:31:01 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:to:cc:subject:date:message-id:in-reply-to:references :mime-version:content-transfer-encoding; bh=7GyhyKuCGDerdGuoNjbX1b5UU6r+UUpK9bAjsPh002U=; b=Lfov4o0wSsKkgCwmT00i//X0LmRgtQNOPv8TcIHRS6o4BLlGXDQhMvCnHKCG/CjTBd BW8LTLNoXeP8+vqpdMVbT1G8NdUZH+jtJl72iIJvxosDxXOcP9XlaS38IIpPbbdicrsE uLUCJefWdsbKJTNGzp9Nd9UaWgHwxFrPP6QPTHyWVzW9WsqK8idBz2MYCtKwX5RpVLA8 X04hrdlGGCEsyBzXUVmicD0Ikf2EE0l/94bG6pi1AD6N03jydxHrKhiyUtjOdGcYI53F 6Fe+2l5V5Ngok686brxZ/kgw/FVS9a/A6Ij6mWNjMyGbe5ue/dosELf+WLub4XwRk6ao Op0Q== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:to:cc:subject:date:message-id:in-reply-to :references:mime-version:content-transfer-encoding; bh=7GyhyKuCGDerdGuoNjbX1b5UU6r+UUpK9bAjsPh002U=; b=cAadWSb+Yx864AZAJ0injWnxOZbJxU7GdCYkW+8ozJReW31JZCy0As8S/cfXOio5gb y6XtvlaMBkf8Mhxh+2wxlwu6exsiuF4tTZX80ObKk1hMPM7U2tNBleZn8pATXDU3gy+c cbBIfysFVqFWa1KhtRBTfpfoPjoyrysBvt+ElDrO5oQ+yTnvpm7p/XMR4KhUTOV5WWvc lZi9+YXiFhdytpYh0NpYG4+oicoVTDppOPhQSfIQnF06SSSt9bAqu5ep55HK0jvr98S3 q3RCVz2nZp2DXXP7zDjTDoZo4mNRRFjr5wfSY3vNGUpt9JF3i+8SC/M7tX9yiIuzE0Kd RQNw== X-Gm-Message-State: AOAM53125rYBeK8xt1R4smDnt25ttBEeEC00ZphkIvc81UgqyAgjyMux uaBqG5aflrcIbASRSDokO8dGbgM6h+8= X-Google-Smtp-Source: ABdhPJxz5c34O3QoJqQn0esRVm8ihzJD7Cd135ks7yNNyKAfmhgFz6bQK9Ck63Ak+2bzlsa85/CYYQ== X-Received: by 2002:a50:85cd:: with SMTP id q13mr22115272edh.114.1618061459901; Sat, 10 Apr 2021 06:30:59 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:f96a:804d:4fe5:372f]) by smtp.gmail.com with ESMTPSA id g26sm2594910ejz.70.2021.04.10.06.30.59 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sat, 10 Apr 2021 06:30:59 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 8/8] scheck: support pre-conditions via __assume() Date: Sat, 10 Apr 2021 15:30:45 +0200 Message-Id: <20210410133045.53189-9-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> References: <20210410133045.53189-1-luc.vanoostenryck@gmail.com> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org A lot of simplifications are only valid when their variables satisfy to some conditions (like "is within a given range" or "is a power of two"). So, allow to add such pre-conditions via new _assume() statements. Internally, all such preconditions are ANDed together and what is checked is they imply the assertions: AND(pre-condition) implies assertion 1 ... Note: IIUC, it seems that boolector has a native mechanism for such things but I'm not sure if t can be used here. Signed-off-by: Luc Van Oostenryck --- ident-list.h | 1 + scheck.c | 33 ++++++++++++++++++++++++--------- validation/scheck/ok.c | 6 ++++++ 3 files changed, 31 insertions(+), 9 deletions(-) diff --git a/ident-list.h b/ident-list.h index 6264fd062534..3c08e8ca9aa4 100644 --- a/ident-list.h +++ b/ident-list.h @@ -79,6 +79,7 @@ IDENT(copy_to_user); IDENT(copy_from_user); IDENT(main); /* used by the symbolic checker */ +IDENT(__assume); IDENT(__assert); IDENT(__assert_eq); IDENT(__assert_const); diff --git a/scheck.c b/scheck.c index ff140aaa1e95..b8bc9bb28498 100644 --- a/scheck.c +++ b/scheck.c @@ -31,6 +31,7 @@ #define dyntype incomplete_ctype static const struct builtin_fn builtins_scheck[] = { + { "__assume", &void_ctype, 0, { &dyntype }, .op = &generic_int_op }, { "__assert", &void_ctype, 0, { &bool_ctype }, .op = &generic_int_op }, { "__assert_eq", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, { "__assert_const", &void_ctype, 0, { &dyntype, &dyntype }, .op = &generic_int_op }, @@ -184,11 +185,22 @@ static void ternop(Btor *btor, struct instruction *insn) insn->target->priv = t; } -static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn) +static bool add_precondition(Btor *btor, BoolectorNode **pre, struct instruction *insn) +{ + BoolectorNode *a = get_arg(btor, insn, 0); + BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a)); + BoolectorNode *n = boolector_ne(btor, a, z); + BoolectorNode *p = boolector_and(btor, *pre, n); + *pre = p; + return true; +} + +static bool check_btor(Btor *btor, BoolectorNode *p, BoolectorNode *n, struct instruction *insn) { char model_format[] = "btor"; int res; + n = boolector_implies(btor, p, n); boolector_assert(btor, boolector_not(btor, n)); res = boolector_sat(btor); switch (res) { @@ -207,20 +219,20 @@ static bool check_btor(Btor *btor, BoolectorNode *n, struct instruction *insn) return 0; } -static bool check_assert(Btor *btor, struct instruction *insn) +static bool check_assert(Btor *btor, BoolectorNode *pre, struct instruction *insn) { BoolectorNode *a = get_arg(btor, insn, 0); BoolectorNode *z = boolector_zero(btor, boolector_get_sort(btor, a)); BoolectorNode *n = boolector_ne(btor, a, z); - return check_btor(btor, n, insn); + return check_btor(btor, pre, n, insn); } -static bool check_equal(Btor *btor, struct instruction *insn) +static bool check_equal(Btor *btor, BoolectorNode *pre, struct instruction *insn) { BoolectorNode *a = get_arg(btor, insn, 0); BoolectorNode *b = get_arg(btor, insn, 1); BoolectorNode *n = boolector_eq(btor, a, b); - return check_btor(btor, n, insn); + return check_btor(btor, pre, n, insn); } static bool check_const(Btor *ctxt, struct instruction *insn) @@ -239,15 +251,17 @@ static bool check_const(Btor *ctxt, struct instruction *insn) return 0; } -static bool check_call(Btor *btor, struct instruction *insn) +static bool check_call(Btor *btor, BoolectorNode **pre, struct instruction *insn) { pseudo_t func = insn->func; struct ident *ident = func->ident; + if (ident == &__assume_ident) + return add_precondition(btor, pre, insn); if (ident == &__assert_ident) - return check_assert(btor, insn); + return check_assert(btor, *pre, insn); if (ident == &__assert_eq_ident) - return check_equal(btor, insn); + return check_equal(btor, *pre, insn); if (ident == &__assert_const_ident) return check_const(btor, insn); return 0; @@ -256,6 +270,7 @@ static bool check_call(Btor *btor, struct instruction *insn) static bool check_function(struct entrypoint *ep) { Btor *btor = boolector_new(); + BoolectorNode *pre = boolector_true(btor); struct basic_block *bb; int rc = 0; @@ -281,7 +296,7 @@ static bool check_function(struct entrypoint *ep) ternop(btor, insn); break; case OP_CALL: - rc &= check_call(btor, insn); + rc &= check_call(btor, &pre, insn); break; case OP_RET: goto out; diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c index 8f65013e1618..1e5314f24ded 100644 --- a/validation/scheck/ok.c +++ b/validation/scheck/ok.c @@ -10,6 +10,12 @@ static void always(int x) __assert((x - x) == 0); // true and simplified } +static void assumed(int x, int a, int b) +{ + __assume((a & ~b) == 0); + __assert_eq((x ^ a) | b, x | b); +} + /* * check-name: scheck-ok * check-command: scheck $file