From patchwork Mon Apr 12 21:21:04 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: 12198861 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 62DABC433B4 for ; Mon, 12 Apr 2021 21:21:23 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 4395A6135C for ; Mon, 12 Apr 2021 21:21:23 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S242939AbhDLVVl (ORCPT ); Mon, 12 Apr 2021 17:21:41 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60838 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S238709AbhDLVVk (ORCPT ); Mon, 12 Apr 2021 17:21:40 -0400 Received: from mail-ej1-x62b.google.com (mail-ej1-x62b.google.com [IPv6:2a00:1450:4864:20::62b]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 22A60C061574 for ; Mon, 12 Apr 2021 14:21:22 -0700 (PDT) Received: by mail-ej1-x62b.google.com with SMTP id u21so22571932ejo.13 for ; Mon, 12 Apr 2021 14:21:22 -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=BzbNi0EnHya8fd592cvfB02nNIXKteBsa15WcAk09v1pqQKWeU/Yobe7HSFfn6g/xl 6PPwOT2BXgH878Bs5yjBOIIbNSOGPd9mN98OgT6iTxkWCWevICsIGddeVJiyrMWjaS5q vesaHdXQl9rZnOTDpqY15w9067h24tm7iLDVnOjaDnGZPwv+IrjGJDyGimc5hXrycs04 q+JlEUTZJ+ks/PN9SD98//4R7fdMjlGX5cuYojIEdH5XQRys71RKq4CeUS5s47KciycN m+EdQeH9DqoZUzos8L5fQQZc3TtGLB2LDWHU9skjM88KVH97QVn5ViwBRc411xOLJ/0c NbTQ== 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=M5mhU3qfnL7bzD2SdQDoHOzukNVEozKqjsZ16LLFS+Tbv4NdHaIow4z5GJUCEPrDZx jMydKcwy0nCQ/+ZrogZcb5+8NPqmhocZnd84a5D4h6e1t/VU4oMETiaUbXSFRPzR2/fq m4Hs8cberrauit5aNgjO9S0QmqdxaLrHVk91QKKDihK3Xmaiv9s3vKfH4vSX5CPsZcBq j4SZcsddisaxr1TaFBv7/v7uzMgklj4PHl7vO72Y4lqyXRouO1sr7xMg+O/3qdkbP99z Q+zV+TPtmiQCIA4mWi7io+qf5RdCZS6aNIgPady5jMZQzJJm06/FOfPXc4hOQ7ll37Nj VwAw== X-Gm-Message-State: AOAM530czNxu5CeM6yukp8wJPAqpySXMx1Rk6tz5Tnj7ECQJpp3YsUR8 o9kyng2Uw7lqtzVizQc1CG22rFGg+es= X-Google-Smtp-Source: ABdhPJzw9ZID3oW31o4aUAN5CF5sI3vSz4/L8yEaRPoxURg6STMcPLBYwz3HGiEUAVdZzhoQiUNNpw== X-Received: by 2002:a17:906:aad9:: with SMTP id kt25mr28461857ejb.364.1618262480939; Mon, 12 Apr 2021 14:21:20 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.20 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:20 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 1/8] export declare_builtins() Date: Mon, 12 Apr 2021 23:21:04 +0200 Message-Id: <20210412212111.29186-2-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 Mon Apr 12 21:21:05 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: 12198863 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 BC8CEC433ED for ; Mon, 12 Apr 2021 21:21:25 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 9F53E6135C for ; Mon, 12 Apr 2021 21:21:25 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S243730AbhDLVVn (ORCPT ); Mon, 12 Apr 2021 17:21:43 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60844 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S238709AbhDLVVl (ORCPT ); Mon, 12 Apr 2021 17:21:41 -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 13BCDC061574 for ; Mon, 12 Apr 2021 14:21:23 -0700 (PDT) Received: by mail-ej1-x62c.google.com with SMTP id v6so21322748ejo.6 for ; Mon, 12 Apr 2021 14:21:23 -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=6x5qFu2A5sg0AfaOENDQ6CDYdDY/tuVTs61SwYKy2Tg=; b=VjcsCTCiw1X8Lp5thqw3IScZMLOE8WFyaVHh6p0rRP6976N8+FVkdI7bgweaKGvOTi aPjl47V4ho6xgZyZ/x4HCI518oBL/Bkzt6bBsxrYJK5vzpg/HXjzMuig0HiDClU3u35U yOpCgP6MOgaJa/3YdIOA7aNfPlpFmN1ezAnJlTUjmd6RwJLQyhYRqAQ+NwenU+Z6Tg0q x5DWJqf1LlOwNjd39wDVWIGEgO/KP/Se2aPw3HW3aBrhBXRsb8Hn9KDO5uVMADYt5fNR DRMyEjGKDRBVEdvbA3bl7U1tQDoITu2kRQmr4i8e29zvc6M7plk+gKJPcj42JTK+qKuU XlVw== 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=6x5qFu2A5sg0AfaOENDQ6CDYdDY/tuVTs61SwYKy2Tg=; b=brcADKoaKHhNDiVwEPDwkoTsJqmjbBd7Koa9lt4NAQod875YlMzun0FSDEh6QrWFUd JuO4T3vHdjZ0GL5QZcd4iNmDxD8tTgU5+AqXc7gQ56D5RG21Glx6Q6AWRsKc1++oOc8w 3AFTmynznnVlE+0sFXOrCkHCu8tKmGvCuQebCWD3FhjBG/T4V7XwAfKYZTrDl4L9yJnu R4Cxed8kAmiZZWNdsXab5LDSfMMs9cjeI6RVUsSuhiZdSCuTUY/GdvC1bDP0OTTehOiB BGerZtw5yoKO3G3vhHlV6rFWz+/49+At3FC7mDJZIn2mxzXfx79aCjktCAREPIwurelK DUUw== X-Gm-Message-State: AOAM531euxweaecVW+0bOSYLNi+qTO3WFKKMgBT67D49Qui3ZE/GP5ss 81yBebH6NBOVOoFflxZpjNYP96QMYzE= X-Google-Smtp-Source: ABdhPJzEsD9dzSc79wsP2nI83gtMtIMujCviwqiLlT2DH8aYOLEAplZpY0oNlD2u8ORbpt/tui647g== X-Received: by 2002:a17:906:7795:: with SMTP id s21mr14350877ejm.309.1618262481775; Mon, 12 Apr 2021 14:21:21 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.21 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:21 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 2/8] builtin: define a symbol_op for a generic op acting on integer Date: Mon, 12 Apr 2021 23:21:05 +0200 Message-Id: <20210412212111.29186-3-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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: (int) (T, T) (int, T) (int, T, long, T, ... T) where T is some integer type which will be instantiated at each call. Signed-off-by: Luc Van Oostenryck --- builtin.c | 61 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ builtin.h | 2 ++ 2 files changed, 63 insertions(+) diff --git a/builtin.c b/builtin.c index ff03dbab9a06..928e03050375 100644 --- a/builtin.c +++ b/builtin.c @@ -390,6 +390,67 @@ static struct symbol_op overflow_p_op = { }; +/// +// Evaluate the arguments of 'generic' integer operators. +// +// Parameters with a complete type are used like in a normal prototype. +// The first parameter with a 'dynamic' type will be consider +// as polymorphic and for each calls will be instancied with the type +// of its effective argument. +// The next dynamic parameters will the use this polymorphic type. +// This allows to declare functions with some parameters having +// a type variably defined at call time: +// int foo(int, T, T); +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) { + if (!is_dynamic_type(t)) { + ; + } else if (!ctype) { + // fist 'dynamic' type, chat that it is an integer + t = arg->ctype; + if (!t) + return 0; + if (t->type == SYM_NODE) + t = t->ctype.base_type; + if (!t) + return 0; + if (t->ctype.base_type != &int_type) + goto err; + + // next 'dynamic' arguments will use this type + ctype = t; + } else { + // use the previous 'dynamic' type + 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 Mon Apr 12 21:21:06 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: 12198865 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 077CCC433B4 for ; Mon, 12 Apr 2021 21:21:26 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id DAA2361278 for ; Mon, 12 Apr 2021 21:21:25 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S238709AbhDLVVn (ORCPT ); Mon, 12 Apr 2021 17:21:43 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60846 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S243618AbhDLVVm (ORCPT ); Mon, 12 Apr 2021 17:21:42 -0400 Received: from mail-ej1-x62b.google.com (mail-ej1-x62b.google.com [IPv6:2a00:1450:4864:20::62b]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id BBE92C061756 for ; Mon, 12 Apr 2021 14:21:23 -0700 (PDT) Received: by mail-ej1-x62b.google.com with SMTP id n2so22572763ejy.7 for ; Mon, 12 Apr 2021 14:21:23 -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=KczJiMkGiocpfuw+96XRbWtvm2jq84y6uV1ArtpB85Fj0Mu8+3lttiBfR2eFVHMK7t ud8E6o+uwmNzT4JkOwloR2VsgZ3ztHGheWGiXnyn8Ogvo3CcVWrkWYfJ+/G/oJVyNs94 W9LhWOhhI24IawTiLL8ZFGSAoEz481cSxftv3bs+5eDQK/a+TTtiLkc0H4qz9H9t4HLu n1sbC6pbdS2/zMPyCHxVRPWclZ37rx8GmxHnU5H8VQ/tQxsxEGvmJ7kGsl++gnurJZs+ 7uUk7ykDioCdO+17Ubccxov3f5Q1hOKFoU1yOUkt6WgQZRbZUeFinjRv78epud85C8fR prvA== 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=j28WoOHwSOx7OKj7OlWY0QrL7aGSWKIHDxMWsewgFgC7nX2UPPNTJxO+2KPDADHUWG zibziH4in5NbUa+jd2llY+tqyfYvX8CFQ560+CQMYT1vVLRpffL5tL8uvbccH9W5b5fe Z8Pv2kgcjN69l/rCXsQLPJRU0FeFJuHlgmCn9QWsFTgHh4v0dmDgs9wueFmAES4VgL97 iWdyDXIhQ8kBpou5LncB9GVGEHire7n06hTadgQtDsUU+k5ir0Cz24z6qGZPYvLdLlxH avr0qM/G0hvrpygoqHDckuMQ5Ei7EYzIk2GV8PRcQC6gDqeFOc6FbEv+F5wJrtbAtNNv 6AgA== X-Gm-Message-State: AOAM530GmR5kIEpC0yPww0QRLmZXKH1LUshsqvxTx7K3BllTXc7LJv5y cTYSaGit20LwXeWVukxYz31Vp04NJZM= X-Google-Smtp-Source: ABdhPJwGR2wDcZI38gnksN1wxoQX/6CG75TDYVqos60WsYtFKc4P5WTyHKWdgk+gC6Pjt2dKKOpAjQ== X-Received: by 2002:a17:907:9611:: with SMTP id gb17mr29800501ejc.325.1618262482571; Mon, 12 Apr 2021 14:21:22 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.21 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:22 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 3/8] .gitignore is a bit too greedy Date: Mon, 12 Apr 2021 23:21:06 +0200 Message-Id: <20210412212111.29186-4-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 Mon Apr 12 21:21:07 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: 12198867 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 3DADDC43461 for ; Mon, 12 Apr 2021 21:21:26 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 19CBA6135C for ; Mon, 12 Apr 2021 21:21:26 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S238773AbhDLVVo (ORCPT ); Mon, 12 Apr 2021 17:21:44 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60850 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S241461AbhDLVVn (ORCPT ); Mon, 12 Apr 2021 17:21:43 -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 C27D1C06175F for ; Mon, 12 Apr 2021 14:21:24 -0700 (PDT) Received: by mail-ed1-x530.google.com with SMTP id w23so16788461edx.7 for ; Mon, 12 Apr 2021 14:21:24 -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=taQt/yFMvKqZ4LVHJAl/i1/n6B7Qei3ktjv6VoJda4U=; b=vDVohqS6Wx82l1k/Mz2gDf9KKdf9uQzlcRYCwEKivRFiDpxbsjagQ1QyyRseXBU6C8 qNU6BK0YO6CS605RiwbIvfJ/A1vWXm2DMKII6K0S7TMqzByIQXuli5FcQTAZKunCTNsO WF7PpHpk7aKc1waqz4dngdAQTL2wEu2jMWA4yqEsAyGvAtCO641SaCGzsX87D2zlKiGu qKeb5mGSOr5VeegVn/HLxZIHfWt2/cVcofD76i0Zdgtwd7eQ342pIC6H3gaiBM0qv0JM t2EcQPu6TwhsI545DqSjo3lNiqLjCKPfqRCpFJNCDDJCrbcUY1uftl6IHEve6guxNF+N Vmhw== 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=taQt/yFMvKqZ4LVHJAl/i1/n6B7Qei3ktjv6VoJda4U=; b=reqmikApNWw0KHjB0yaDjeorJnhjXhvLDFy+ns0dD+U7fX2WJy7+nyaiypNI6k0ToK DjcMsfNa4AnHlucLVeh8jndJ4yLjzfPnIFQkOOE1BFlVluGUMifkraKDdkrC/G4GlsXn 8cdaGBD7sLttguEmJ7/pp8KkyTNGCKG/ylFaQJz4BULhi7vuCt0AjpoL6cD2jUgewhOH 7lJ3VesUhUts6/AbkuTBwwTnwM1i6n2n8iZxrwhZ/Czmne4oyM+LpRFJpBpJ5YNByOut xtYK5TTLnt9yDr4rLUu3tXxJ+IdNAvd8hGs/8dn7OyyxzI8TYs8fBRZp43Hi5Y20pGGF G90A== X-Gm-Message-State: AOAM5335R25DV1m/3JpP/5X2DShCjvnMPCIZWCV9mAx6PkvUrxSjlsEz cCenoBnOAVNJbwN/BK+FY/9XaSGq5Ww= X-Google-Smtp-Source: ABdhPJwzK5IfXWgix58RDOvUlX3UNjc7VhSvLvR06auWXcTYZuMxyEf7QEFk+E8KiGYV0+Zhq3Q22w== X-Received: by 2002:a05:6402:22a6:: with SMTP id cx6mr31156552edb.55.1618262483538; Mon, 12 Apr 2021 14:21:23 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.22 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:23 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 4/8] scheck: add a symbolic checker Date: Mon, 12 Apr 2021 23:21:07 +0200 Message-Id: <20210412212111.29186-5-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 | 315 +++++++++++++++++++++++++++++++++++++++++ validation/scheck/ko.c | 10 ++ validation/scheck/ok.c | 14 ++ validation/test-suite | 6 + 7 files changed, 356 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..63cbfa2d3404 --- /dev/null +++ b/scheck.c @@ -0,0 +1,315 @@ +// 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 binary(Btor *btor, BoolectorSort s, struct instruction *insn) +{ + 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 binop(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + binary(btor, s, insn); +} + +static void icmp(Btor *btor, struct instruction *insn) +{ + BoolectorSort s = get_sort(btor, insn->itype, insn->pos); + binary(btor, s, insn); +} + +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: + binop(btor, insn); + break; + case OP_BINCMP ... OP_BINCMP_END: + icmp(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 Mon Apr 12 21:21:08 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: 12198869 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 020D9C433B4 for ; Mon, 12 Apr 2021 21:21:30 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id D944B61278 for ; Mon, 12 Apr 2021 21:21:29 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S244048AbhDLVVr (ORCPT ); Mon, 12 Apr 2021 17:21:47 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60860 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S238774AbhDLVVo (ORCPT ); Mon, 12 Apr 2021 17:21:44 -0400 Received: from mail-ej1-x634.google.com (mail-ej1-x634.google.com [IPv6:2a00:1450:4864:20::634]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 2F8FDC061574 for ; Mon, 12 Apr 2021 14:21:26 -0700 (PDT) Received: by mail-ej1-x634.google.com with SMTP id u21so22572132ejo.13 for ; Mon, 12 Apr 2021 14:21:26 -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=jFigMdQ4IIzSB3aVsxjFRTm7LBjV+V/rgt0UVSYJPDQ=; b=jHv63XmVvD2NsdTOQm7pd15ObmOHy9C8CihGhJUC+B8h/NC4Ap6jMhmewz+y1ABfrc 2+JXby8Uds0TCNnQaIOc5e7pefrZ1WhqV68AG8tn7uRdKify6DmoH9lQ1stckemZbd0R qGwdYfPzwSS82MThvvRlDFVsMuo6dfYSZnyHOe6/6wB/dAEKhbxnnr+6qgyK+y0LGZ6w 39DELIAEuPQKdxW6YG7OOHf1sA5vBkTDp5cWEXU+k5/oEmxsZNStileGwqsUh9KRUBEV PPHPH9Ty/+w5Pg+WZaZLwRxPa/vhOtxqEbcW3IYUHLTQ7RqPmYUaC832+VRUSU5ucypZ Vgfg== 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=jFigMdQ4IIzSB3aVsxjFRTm7LBjV+V/rgt0UVSYJPDQ=; b=IRbvBaRJEb5ER7QdJSULEvCArpmzeSjBqtgS75WlwK80PcAyLJ11mV3dUOiB71f2Bw RrbMwU0VWPpy7pElKZZO4WxUa03W2QyjvJ0FvmidDK2Bvm1414sANqmavWd7vJv8ikqM 9X5rK9USjRwdCqI1strYXwAcb1sbCzE08u1n1+8ggwZtf3Z7qZywbm/qD5Pg3V4LI8a4 9RHWTINmq5kystCqOA0nsnA4VMBZoYN+FY2if14A63elpv0qX5tglQuLHLw6AphKmmyZ RgWkU/vHryWc4L/5iEzKIfTynOiUBdzrdy1eC53/20elgbL51p0fjFm41Gfn9c7/HGF5 Yoew== X-Gm-Message-State: AOAM532A+phge7zeW6cqBvyewlw7f5Hg9RWyz38wGS+gTPIiExoxS0yK ivAYmCfkU6D902j8+ADOH6vAwzQXI0E= X-Google-Smtp-Source: ABdhPJzAYdeB/gR/lV8TPQ3vcjDDuCKko4EfElpP4OahrTMtZausJskssAl+k9xC44rhJJWMU14zpQ== X-Received: by 2002:a17:906:c143:: with SMTP id dp3mr27641629ejc.499.1618262484927; Mon, 12 Apr 2021 14:21:24 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.23 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:24 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 5/8] scheck: assert_eq() Date: Mon, 12 Apr 2021 23:21:08 +0200 Message-Id: <20210412212111.29186-6-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 63cbfa2d3404..c64e865136c5 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 }, {} }; @@ -224,6 +225,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; @@ -231,6 +240,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 Mon Apr 12 21:21:09 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: 12198871 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 6E201C433ED for ; Mon, 12 Apr 2021 21:21:30 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 502716135C for ; Mon, 12 Apr 2021 21:21:30 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S244790AbhDLVVs (ORCPT ); Mon, 12 Apr 2021 17:21:48 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60866 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S242321AbhDLVVq (ORCPT ); Mon, 12 Apr 2021 17:21:46 -0400 Received: from mail-ed1-x536.google.com (mail-ed1-x536.google.com [IPv6:2a00:1450:4864:20::536]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id 652A9C061756 for ; Mon, 12 Apr 2021 14:21:27 -0700 (PDT) Received: by mail-ed1-x536.google.com with SMTP id bx20so15631041edb.12 for ; Mon, 12 Apr 2021 14:21:27 -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=7viAuovfFnmrqFKiDenn6AEET5zy1s11tBohzUeWfCk=; b=icAnPDIYN1u4XLPGHYYFSQhfOWXUSlSwMHFkOrHWXV+v04MXGmgGdhCYPfvAvBn3Xj gOTgI0ggI7xunZ8aqFVogt2AFftNlPW6o5/0MzC6veKoowsmPF/D12eXOPdo93HubMNT NeezVsq9Vg9O33/Kp1vr96u60L8u2FemstwfMWWqGj6IBgno+GhkwX1aEsL85DwIO5el Af/V0B/yQ5jL/rACxX/0B8DrWyEK27iY6WS2/zreHLjhRs/zFa15ZQ6jJqSePO5lhGU4 lYifreWgRNaJHCEINd/dklXEM2SNjX+HkMYYI9mFNyyOVotKFPQUPBLDQ2YAPlgp11bo jXlA== 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=7viAuovfFnmrqFKiDenn6AEET5zy1s11tBohzUeWfCk=; b=ABGhciwRXwHLCWHyyJLPM4TMIz5SIKCJeNrVk27UJXyHR5936PYhBnlEPQ88jUHa9P iYlAsOGTXdTml97KBXWWBwNHmYHUUJJlNwsU57Iqenm033n8Zcet+NXUgpwLSkhRc5Bj 9Fk+1mqEk7YPGHOnr0uH6cj+S+QENP/xeVw0KSCwnqR9y9dl1X8i+/5f/+DU626BvD0u xbK5QjwpVcTI6tphrJ/pVGhZDoOqGPHio75Bu6VYdVeGK0qrdsli4xU/3Q7XCbv0pIg9 zZeVrw4R1Ztn3Iice+Y5RH7WsqTTPstFWTLyIgbU/v/HnXdOUwFjDOujCh/jjYaP8u79 m8Ww== X-Gm-Message-State: AOAM530yQ91i+vDOgChS5c9i/eAyUjWgQ3X0aDQLUJ6comeyBblLfmqm pqPvWMyoWJcxn1dhxi4Tv6dIydK+Hn4= X-Google-Smtp-Source: ABdhPJzX4QQalnrVO18slVdgZbpji7CJ8Y4OpLGZxr9okFXIR7QPdz72u+sjXSshyZtqnGCf7NANuQ== X-Received: by 2002:aa7:db9a:: with SMTP id u26mr30764537edt.292.1618262486189; Mon, 12 Apr 2021 14:21:26 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.24 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:25 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 6/8] scheck: allow multiple assertions Date: Mon, 12 Apr 2021 23:21:09 +0200 Message-Id: <20210412212111.29186-7-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 c64e865136c5..efa5c1c3247b 100644 --- a/scheck.c +++ b/scheck.c @@ -252,6 +252,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; @@ -274,8 +275,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 Mon Apr 12 21:21:10 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: 12198873 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 CA072C43460 for ; Mon, 12 Apr 2021 21:21:30 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id AFAA061278 for ; Mon, 12 Apr 2021 21:21:30 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S237777AbhDLVVs (ORCPT ); Mon, 12 Apr 2021 17:21:48 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60870 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S242786AbhDLVVq (ORCPT ); Mon, 12 Apr 2021 17:21:46 -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 0FE5CC06175F for ; Mon, 12 Apr 2021 14:21:28 -0700 (PDT) Received: by mail-ej1-x62c.google.com with SMTP id mh2so1042152ejb.8 for ; Mon, 12 Apr 2021 14:21:27 -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=a3Atag3Uhwbwc86Jz5JwLkrDGBV8Qf2M+gfpyGrCfvo=; b=sPLFFq8fzjhcuxnjwbrQ+zb9boNHeulDeLBsT3/zUq1avOml8HXpiTggj01GH58lbO CQUCUE3eXqaQjZs2fNCUHLAY4MeHv4JacZT+uE1AVouoQomOPHeffvdDf7GEHKbZYJUX vkMJ/vAIKU3hfO9OLuvCDklSeWZSvDNhTWcgtZEvUq1p2S3fbYuGkq2cU7CybElTx37g MY7vV1l0bhLsFsfOPnvJJT3rnz2IUWfRZrHNI+9nnbgbGSXf2/iBdY0bHqkwIt5GVCCK k3DDq0kL1t7IwTeScFq+57vPwfeoB4No6VYpYU1CAB6J/BYJP9DoGQG3ka+KCmBSb49n CoYw== 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=a3Atag3Uhwbwc86Jz5JwLkrDGBV8Qf2M+gfpyGrCfvo=; b=Gzg6CTiv5rB17iosqeY4T6xdQCZM7tssPACuJ+HJC0HOARFJ/fFq60fWQWlBXzhlYL w4PVJJglEXxmYQRYEEgL6FQCTBiASXZAhdB0kY0NlpVcPRmu9x5xv4Ka7hIN6eZr/Ksb CVar0ddPZeV3AHBqiOFUSayPaRX8jRUPnPCNUPK9ugE5KMTQgT8iSYzLxDjm3+96MdR9 vebRXVaHeosWfUkMttAMR0dx4/20G+/aGDDOlrMajQmMdshUwdXacDIv/1ae9l8ReOTm 0aHoRkg5Y8tQ6Ytsi9j+OCguSKyE+G3TfflxhFxiUPhl1PXtlxhQHs0+yg2RpRr9FtKf /6qQ== X-Gm-Message-State: AOAM532q5EVCco+2l6qVIdSZsWfpeaoditocv1Y/+OjRLAd7gt+Vfl9l k4bSZqg2DtrHsMNZ2rPslTh6JCKybsM= X-Google-Smtp-Source: ABdhPJyjQVhu0QByvdW74Amr/HdOTAnq4cplv+MGR40P/EiHogZCjm/hvJkUp+OF8hSd+X1SUmLCwg== X-Received: by 2002:a17:907:2137:: with SMTP id qo23mr29541216ejb.442.1618262486815; Mon, 12 Apr 2021 14:21:26 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.26 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:26 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 7/8] scheck: assert_const() Date: Mon, 12 Apr 2021 23:21:10 +0200 Message-Id: <20210412212111.29186-8-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 efa5c1c3247b..f5ea4cf11902 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 }, {} }; @@ -233,6 +234,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; @@ -242,6 +259,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 Mon Apr 12 21:21:11 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: 12198875 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 00C01C43461 for ; Mon, 12 Apr 2021 21:21:31 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id D4B7C6135C for ; Mon, 12 Apr 2021 21:21:30 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S238774AbhDLVVs (ORCPT ); Mon, 12 Apr 2021 17:21:48 -0400 Received: from lindbergh.monkeyblade.net ([23.128.96.19]:60872 "EHLO lindbergh.monkeyblade.net" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S243618AbhDLVVr (ORCPT ); Mon, 12 Apr 2021 17:21:47 -0400 Received: from mail-ed1-x533.google.com (mail-ed1-x533.google.com [IPv6:2a00:1450:4864:20::533]) by lindbergh.monkeyblade.net (Postfix) with ESMTPS id A970FC06138C for ; Mon, 12 Apr 2021 14:21:28 -0700 (PDT) Received: by mail-ed1-x533.google.com with SMTP id 18so16810096edx.3 for ; Mon, 12 Apr 2021 14:21:28 -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=j7vBxDcK+CbBXGC7650Q3+DnkkKcVHAG3Vshdvo4C5U=; b=Rm4sYU9kfkfxHWoKFO2oGYbNcmmEtWVVPkGUThaHAzF66IPyfIUZnJWVNukDBOVtj4 vpOtANeB3DDO8/qF1D9JhcyGXAhk/Om+EUvDnsZ9iJRtgjCcKumYlhMLKffI8vFSCgXx bkFCOXdgGZ++PywgUUdkD48nXf+8BKX5ats6elVQzsgBGSh/TxUVUDJ2QjPQIfS7tynB j+3fw4bE8qDTwI3tk/Ao7BH+U30F1lXypZkhjA104nWis0zqBguv3WyD6Ml7/p8GYHke Xpb4acDS36wAPko5PWfgpHckkMfkffoTBMwz9LY+tVx4yejFcG1JqAOddic6w+brNyo9 H9dg== 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=j7vBxDcK+CbBXGC7650Q3+DnkkKcVHAG3Vshdvo4C5U=; b=DCVWqkbycPcyX70s/W1B+yK96vC+r2t0mOViI/V2ShsV0zYVEPGMHToWVQ4UhHEvVL a9idhaRK+rV9Lag+SLsIsgpsOpQCtO5FHgRA3ii+QQaENmxjFO9Ef2NaYbk8szOpfBWW qpEQHbXO+o0Qn1fwkaFC9Xd8Zfp4FrZYDhyT1rdHCP3DMQZW3zcIjj86uEMWC3WOzbQz 7OhQ0/IPK12QqBTXzeuGgwGxRkwMUkry7U5GG2AfL0ZS7RVhEicUuyG5/h8PD0f9SH/U +ZQUzo9g5uZd3p5i2sknaBGQsXCvzHwXF7ccKwalOVbGmR6qVyAnVd+4pBrk0ievwc/6 alsw== X-Gm-Message-State: AOAM533DD8hyRypSu+C9UPQk327+IGi+K/gsHrYGZKigCanMVjAKyizA 4WW3ny//clEt3ppzTbE+us7NFQ6dVDw= X-Google-Smtp-Source: ABdhPJzYvN1g6sszemfIbobHnernHzcSsVEzHckrXunwGJDf/E7pJ1E3lVfO20xFH6sWxoHyQ1YmEA== X-Received: by 2002:aa7:d3da:: with SMTP id o26mr20950491edr.147.1618262487487; Mon, 12 Apr 2021 14:21:27 -0700 (PDT) Received: from localhost.localdomain ([2a02:a03f:b7fe:f700:6903:692b:54da:df0c]) by smtp.gmail.com with ESMTPSA id g11sm7744156edt.35.2021.04.12.14.21.26 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Apr 2021 14:21:27 -0700 (PDT) From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Ramsay Jones , Luc Van Oostenryck Subject: [PATCH v2 8/8] scheck: support pre-conditions via __assume() Date: Mon, 12 Apr 2021 23:21:11 +0200 Message-Id: <20210412212111.29186-9-luc.vanoostenryck@gmail.com> X-Mailer: git-send-email 2.31.1 In-Reply-To: <20210412212111.29186-1-luc.vanoostenryck@gmail.com> References: <20210412212111.29186-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 f5ea4cf11902..6752b9d9baaf 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 }, @@ -195,11 +196,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) { @@ -218,20 +230,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) @@ -250,15 +262,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; @@ -267,6 +281,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; @@ -294,7 +309,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