From patchwork Thu Jul 29 21:20:50 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: 12409873 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=-19.7 required=3.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,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 46004C4338F for ; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 278CB604D7 for ; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233890AbhG2VVF (ORCPT ); Thu, 29 Jul 2021 17:21:05 -0400 Received: from mail.kernel.org ([198.145.29.99]:56262 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233798AbhG2VVE (ORCPT ); Thu, 29 Jul 2021 17:21:04 -0400 Received: by mail.kernel.org (Postfix) with ESMTPSA id 1EA86604D7; Thu, 29 Jul 2021 21:20:59 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1627593660; bh=AamUp6V6/GmSWDAe+QCv7NVD2ZVFZ8bVGB1rCgiixm0=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=GTtXY/ZPC0JNLT9aWqdujhF3npWwYzIpZU3hkYaTuloKC63dAi7nC3mlNb2PG6JFP SszxmX7yXJTOJEaVgcblsaYzpMTZf6N2r8kvA03WgRRUz7xFUnIaR7uNa34E66/amD /+rw7DNceUwBTYR/QJsdxQwvzr2BJJKS88wOS6/hzZ5sQSlmZupCmeU7nLfuitJAay F8OINbFChb5SsqSQZiUx5NPN8D4rF8twQfCkh6OjDLuwFjNnbzHmMeTx6VFdFLBvHM V5ZaqoTeQz60N9ca1F0BOEjb6YT8WStL4SQ+Opj3gIY7JoJlL0W11BUVL7HVc1XN94 5+YIxYEnfHnqw== From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 1/5] scheck: better diagnostic for unsupported instructions Date: Thu, 29 Jul 2021 23:20:50 +0200 Message-Id: <20210729212054.34327-2-lucvoo@kernel.org> X-Mailer: git-send-email 2.32.0 In-Reply-To: <20210729212054.34327-1-lucvoo@kernel.org> References: <20210729212054.34327-1-lucvoo@kernel.org> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org From: Luc Van Oostenryck When reporting an unsupported instruction, display the instruction together with the diagnostic message. Signed-off-by: Luc Van Oostenryck --- scheck.c | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/scheck.c b/scheck.c index 754fe76f986a..c830f56a0985 100644 --- a/scheck.c +++ b/scheck.c @@ -134,7 +134,7 @@ static void binary(Btor *btor, BoolectorSort s, struct instruction *insn) 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"); + fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn)); return; } insn->target->priv = t; @@ -167,7 +167,7 @@ static void unop(Btor *btor, struct instruction *insn) case OP_ZEXT: t = zext(btor, insn, a); break; case OP_TRUNC: t = slice(btor, insn, a); break; default: - fprintf(stderr, "unsupported insn\n"); + fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn)); return; } insn->target->priv = t; @@ -190,7 +190,7 @@ static void ternop(Btor *btor, struct instruction *insn) t = boolector_cond(btor, d, b, c); break; default: - fprintf(stderr, "unsupported insn\n"); + fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn)); return; } insn->target->priv = t; @@ -314,7 +314,7 @@ static bool check_function(struct entrypoint *ep) case OP_RET: goto out; default: - fprintf(stderr, "unsupported insn\n"); + fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn)); goto out; } } END_FOR_EACH_PTR(insn); From patchwork Thu Jul 29 21:20:51 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: 12409875 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=-19.7 required=3.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,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 8A0E5C4320A for ; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 67CD3604D7 for ; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233798AbhG2VVG (ORCPT ); Thu, 29 Jul 2021 17:21:06 -0400 Received: from mail.kernel.org ([198.145.29.99]:56282 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233875AbhG2VVF (ORCPT ); Thu, 29 Jul 2021 17:21:05 -0400 Received: by mail.kernel.org (Postfix) with ESMTPSA id 134F360C51; Thu, 29 Jul 2021 21:21:00 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1627593661; bh=lwAflT8ZAz82FXuGW5gsz56Te+TxRn5vvlU6pKuDLFk=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=mG74apM+1lglfFd7FQZ9zSsOowZ+/kgeXntTI6/DO/Pl3vw2APwD0bPC9qmINfEFC hJcXXYZ4KKitLl288I6eBM/9LFVq5BD7rtIjaAPJs67ZSL1fyLQ714R19kWXIySt7j AwXvpgPnY/fAOFOtwk3Xj+LmfmfhIqyWFcxwG1u9Mat3NciUP4KEsZiyRmQyqz2ZtS 61SpYTZdzZhhBc5K+eoq7jwCo+4CbMXh4UouJZ6/MkgwS2SQSeUEQtdArfdQX26sZ0 9tNMZ3dt+o1SszkQQl0F4CTijRKghaDU18+4/3tZ44w1PEbVE2BrbN+yoRzzZbvhx0 5daCIJeKw9Lcw== From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 2/5] scheck: ignore OP_NOP & friends Date: Thu, 29 Jul 2021 23:20:51 +0200 Message-Id: <20210729212054.34327-3-lucvoo@kernel.org> X-Mailer: git-send-email 2.32.0 In-Reply-To: <20210729212054.34327-1-lucvoo@kernel.org> References: <20210729212054.34327-1-lucvoo@kernel.org> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org From: Luc Van Oostenryck Some instructions have no effects and so can just be ignored here. Signed-off-by: Luc Van Oostenryck --- scheck.c | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/scheck.c b/scheck.c index c830f56a0985..d3ebddd6c2f5 100644 --- a/scheck.c +++ b/scheck.c @@ -313,6 +313,11 @@ static bool check_function(struct entrypoint *ep) break; case OP_RET: goto out; + case OP_INLINED_CALL: + case OP_DEATHNOTE: + case OP_NOP: + case OP_CONTEXT: + continue; default: fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn)); goto out; From patchwork Thu Jul 29 21:20:52 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: 12409877 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=-19.7 required=3.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,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 B3306C432BE for ; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 9D18960ED4 for ; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233871AbhG2VVG (ORCPT ); Thu, 29 Jul 2021 17:21:06 -0400 Received: from mail.kernel.org ([198.145.29.99]:56288 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233832AbhG2VVG (ORCPT ); Thu, 29 Jul 2021 17:21:06 -0400 Received: by mail.kernel.org (Postfix) with ESMTPSA id 081A8604D7; Thu, 29 Jul 2021 21:21:01 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1627593662; bh=MZlTmP/R5JDvGn92H3J1GaaR3ZvW/p9+EXCYZrx1zKk=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=TNAWh+vYQ4F/dFFu1RyihzQF1+WQ+pSX0wAjExf0Wix2gAqibpiesFXtZ+oFUG9iM 0Dc8gTVSBLnqGViG+7rrWXZQyx/QSuqN+7LVCTvQUvTIRfA1IbjqvAt1uUzl/W887c m0En16InMwfK1SU2eVKKsKaikesAHst1sGal5frA3k26keqyq0GtYYGOFl/gVIR8sO FBw/jT3GA5//YhSlf4anZKhViEnxN5sRfOyfVrZLxCO1v0zr32f00eFQ7BKdCI55+v 7eWTj3UEALp5g4iaW8kc2/MMgg143aWyVGaBXvOypyOGPsU95Ardq1zN5EP36q43HE qD2hyx9r46jHA== From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 3/5] scheck: constants are untyped Date: Thu, 29 Jul 2021 23:20:52 +0200 Message-Id: <20210729212054.34327-4-lucvoo@kernel.org> X-Mailer: git-send-email 2.32.0 In-Reply-To: <20210729212054.34327-1-lucvoo@kernel.org> References: <20210729212054.34327-1-lucvoo@kernel.org> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org From: Luc Van Oostenryck in sparse, constants (PSEUDO_VALs) are not typed, so the same pseudo can be used to represent 1-bit 0, 8-bit 0, 16-bit 0, ... That's incompatible with the bit vectors used here, so we can't associate a PSEUDO_VAL with its own bitvector like it's done for PSEUDO_REGs. A fresh one is needed for each occurrence (we could use a small table but won't bother). Signed-off-by: Luc Van Oostenryck --- scheck.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/scheck.c b/scheck.c index d3ebddd6c2f5..5e2b60abb163 100644 --- a/scheck.c +++ b/scheck.c @@ -53,15 +53,14 @@ 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: + if (pseudo->priv) + return pseudo->priv; n = boolector_var(btor, s, show_pseudo(pseudo)); break; default: From patchwork Thu Jul 29 21:20:53 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: 12409879 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=-19.7 required=3.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,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 8C039C4338F for ; Thu, 29 Jul 2021 21:21:05 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id 6555360C51 for ; Thu, 29 Jul 2021 21:21:05 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233908AbhG2VVI (ORCPT ); Thu, 29 Jul 2021 17:21:08 -0400 Received: from mail.kernel.org ([198.145.29.99]:56306 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233832AbhG2VVH (ORCPT ); Thu, 29 Jul 2021 17:21:07 -0400 Received: by mail.kernel.org (Postfix) with ESMTPSA id F13BE60C51; Thu, 29 Jul 2021 21:21:02 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1627593663; bh=z9yk+mOEGcbUExGsrG2j4qFwgJXi9bpw+n9fat1ixzE=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=kpXKpAlZkNv9OkGzsqZMUSFu4BVkRdlDi55zgnDq8XLDQtzQPvzbeKd2vqgyXHcSX liFO48zu4ogjxV1PO47GP/50IT7TCKZnIFyYpSsXYPC5koRwDIVtq+TPbvSTvI9te2 kIu6oINrG7Dv4TH+Q/mIsVN44cx8m5aOmaPoAMXqvKXr9jF3Gbx60zzqZ4l77rVi4p qNOW8U/8WpaNNCU4gOITsho5PheoxxpPgmacjeFmATBYAssWrounEOd5kfL4RJYlKQ q35OEV48ILoIbdHz4JHxB6y+zh24vhuyedc18QkM9ZlzlaZQCUtXpdjuAUMfWa18XG svLqKJFTPqEQA== From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 4/5] scheck: mkvar() with target or input type Date: Thu, 29 Jul 2021 23:20:53 +0200 Message-Id: <20210729212054.34327-5-lucvoo@kernel.org> X-Mailer: git-send-email 2.32.0 In-Reply-To: <20210729212054.34327-1-lucvoo@kernel.org> References: <20210729212054.34327-1-lucvoo@kernel.org> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org From: Luc Van Oostenryck Most instructions have one associated type, the 'target type'. Some, like compares, have another one too, the 'input type'. So, when creating a bitvector from an instruction, we need to specify the type in some way. So, create an helper for both cases: mktvar() and mkivar(). Signed-off-by: Luc Van Oostenryck --- scheck.c | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/scheck.c b/scheck.c index 5e2b60abb163..07b15a0600e3 100644 --- a/scheck.c +++ b/scheck.c @@ -70,6 +70,18 @@ static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo) return pseudo->priv = n; } +static BoolectorNode *mktvar(Btor *btor, struct instruction *insn, pseudo_t src) +{ + BoolectorSort s = get_sort(btor, insn->type, insn->pos); + return mkvar(btor, s, src); +} + +static BoolectorNode *mkivar(Btor *btor, struct instruction *insn, pseudo_t src) +{ + BoolectorSort s = get_sort(btor, insn->itype, insn->pos); + return mkvar(btor, s, src); +} + static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx) { pseudo_t arg = ptr_list_nth(insn->arguments, idx); From patchwork Thu Jul 29 21:20:54 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: 12409881 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=-19.7 required=3.0 tests=BAYES_00,DKIMWL_WL_HIGH, DKIM_SIGNED,DKIM_VALID,DKIM_VALID_AU,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 0CE74C43214 for ; Thu, 29 Jul 2021 21:21:06 +0000 (UTC) Received: from vger.kernel.org (vger.kernel.org [23.128.96.18]) by mail.kernel.org (Postfix) with ESMTP id E833960C51 for ; Thu, 29 Jul 2021 21:21:05 +0000 (UTC) Received: (majordomo@vger.kernel.org) by vger.kernel.org via listexpand id S233832AbhG2VVI (ORCPT ); Thu, 29 Jul 2021 17:21:08 -0400 Received: from mail.kernel.org ([198.145.29.99]:56322 "EHLO mail.kernel.org" rhost-flags-OK-OK-OK-OK) by vger.kernel.org with ESMTP id S233900AbhG2VVI (ORCPT ); Thu, 29 Jul 2021 17:21:08 -0400 Received: by mail.kernel.org (Postfix) with ESMTPSA id E60F1604D7; Thu, 29 Jul 2021 21:21:03 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=kernel.org; s=k20201202; t=1627593664; bh=nE32FZ8ab2v2n9Lf03BC/xIYv79pcx9aMJnX/IpA9Xw=; h=From:To:Cc:Subject:Date:In-Reply-To:References:From; b=RhC5xKDNlG6pgR2+de21UkMKSuqlIpV+ImPOkIHXttFNoCcV6+mWeFlJiYFLU83I2 vfAWu0U3GDTPVFNr31M+OfIC39t2tv1vJ9p/oETp015bGu2ZxB6m7WqRM6YISokdCI hiaLjyszAnehwUCp1PYBGqZKWsYHt13Rhwt7Ta0fxQxBPgKJHn1nxFwwyCVTsS/Aeq O6UKMM4bAjrcgAcpaZW2elamix7Mp6MQ1TUKSDniIvXYCu5WTCoEGpiTLO6/vaqTt9 NBtiwuTz6H54A0fEI/ge1US6rcxBjjr+vmYk1+G17sjAjOzfCS2rljnMr46pJ5sXRC SPbF+A23pH26g== From: Luc Van Oostenryck To: linux-sparse@vger.kernel.org Cc: Luc Van Oostenryck Subject: [PATCH 5/5] scheck: fix type of operands in casts Date: Thu, 29 Jul 2021 23:20:54 +0200 Message-Id: <20210729212054.34327-6-lucvoo@kernel.org> X-Mailer: git-send-email 2.32.0 In-Reply-To: <20210729212054.34327-1-lucvoo@kernel.org> References: <20210729212054.34327-1-lucvoo@kernel.org> MIME-Version: 1.0 Precedence: bulk List-ID: X-Mailing-List: linux-sparse@vger.kernel.org From: Luc Van Oostenryck Casts were using the target type for their operands. Fix this by using the new helper mkivar() for them. Signed-off-by: Luc Van Oostenryck --- scheck.c | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/scheck.c b/scheck.c index 07b15a0600e3..bb052d97996d 100644 --- a/scheck.c +++ b/scheck.c @@ -165,18 +165,16 @@ static void icmp(Btor *btor, struct instruction *insn) static void unop(Btor *btor, struct instruction *insn) { - BoolectorSort s = get_sort(btor, insn->type, insn->pos); - BoolectorNode *t, *a; + pseudo_t src = insn->src; + BoolectorNode *t; - 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; + case OP_SEXT: t = sext(btor, insn, mkivar(btor, insn, src)); break; + case OP_ZEXT: t = zext(btor, insn, mkivar(btor, insn, src)); break; + case OP_TRUNC: t = slice(btor, insn, mkivar(btor, insn, src)); break; + + case OP_NEG: t = boolector_neg(btor, mktvar(btor, insn, src)); break; + case OP_NOT: t = boolector_not(btor, mktvar(btor, insn, src)); break; default: fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn)); return;