From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp0.migadu.com ([2001:41d0:403:58f0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms8.migadu.com with LMTPS id ELI3Lnd4y2WCHwAAqHPOHw:P1 (envelope-from ) for ; Tue, 13 Feb 2024 15:11:03 +0100 Received: from aspmx1.migadu.com ([2001:41d0:403:58f0::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp0.migadu.com with LMTPS id ELI3Lnd4y2WCHwAAqHPOHw (envelope-from ) for ; Tue, 13 Feb 2024 15:11:03 +0100 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=soeren-tempel.net header.s=opensmtpd header.b="znt04q/7"; spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=soeren-tempel.net (policy=none) ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1707833463; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to:cc:cc:mime-version:mime-version: content-type:content-type: content-transfer-encoding:content-transfer-encoding:resent-cc: resent-from:resent-sender:resent-message-id:in-reply-to:in-reply-to: references:references:list-id:list-help:list-unsubscribe: list-subscribe:list-post:dkim-signature; bh=TZY7ulg/adcwRQxaSFDNNve8KgVHCLns3zCvl/LpARE=; b=tKC+ftBMEYVT7jzp3kFQwL6TvJ1A95Ys8wbzaUzHIC6JRuLtVxqyzNoP9AkCyBtldk+dJu /aWBT9V4P8thpK/bYkUl9v/RrZfBwfFi9vUwElPwykZf45ZM64FqFj6MINNndnON4jM4ba FvXngjBzsTldTdW6vPfw2B5VgKgCUwXo73DQ2qBPytDWuM8qiAt1yn2HJH9r7f/sF3usYe fcJjCu8KFIFQw2fnRnOc+AfbJfEw5Nh+CbpYiRn3ZuWuhn9Rti4J2cED1lK6VUE/KYCQU7 RiSa2b4O+4XXYuXyila1ABT+GLB6GQ13GhoMKc2J/opfQaFvRw/S5fj7IXBkoA== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=soeren-tempel.net header.s=opensmtpd header.b="znt04q/7"; spf=pass (aspmx1.migadu.com: domain of "guix-patches-bounces+larch=yhetil.org@gnu.org" designates 209.51.188.17 as permitted sender) smtp.mailfrom="guix-patches-bounces+larch=yhetil.org@gnu.org"; dmarc=fail reason="SPF not aligned (relaxed)" header.from=soeren-tempel.net (policy=none) ARC-Seal: i=1; s=key1; d=yhetil.org; t=1707833463; a=rsa-sha256; cv=none; b=pP8D4D5KYw5mjPike5mezRvG8eHUfYT6QIB6qlQjZFM95rhIQgTxWwcUL4s9MMAhFzEI3e 4Cm10yr9bWUXkkPikGOTZm0Bz09s/uEF+hHE1n5lWIs1pURNCIVhYgrl7vBu7yvtP/M+Ba qneEiELtTUFBEuvJxO8Z1884KI4miWhwfWCLF7KtFO1q7ewnxlL5iwxZe0B60TOrFoz6oR 20Mikv/SuyaX3AoiR8VFi8eZWDZwiRgaxc0wSpT0jUOHaLe7eWImEai7f2haTD/2f0KmOr B8mSpWXCwxHdez9k+GMiV+/wkYuJeHBeWFf8zsMLOt1rqfbLWUgptXl0DyDzdQ== Received: from lists.gnu.org (lists.gnu.org [209.51.188.17]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by aspmx1.migadu.com (Postfix) with ESMTPS id 886295F92A for ; Tue, 13 Feb 2024 15:11:03 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rZtUk-0007c9-Vu; Tue, 13 Feb 2024 09:10:47 -0500 Received: from eggs.gnu.org ([2001:470:142:3::10]) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1rZtUi-0007bf-Ss for guix-patches@gnu.org; Tue, 13 Feb 2024 09:10:44 -0500 Received: from debbugs.gnu.org ([2001:470:142:5::43]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_128_GCM_SHA256:128) (Exim 4.90_1) (envelope-from ) id 1rZtUi-0002sL-Kf for guix-patches@gnu.org; Tue, 13 Feb 2024 09:10:44 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1rZtV0-0007aF-1v for guix-patches@gnu.org; Tue, 13 Feb 2024 09:11:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#68296] [PATCH] gnu: Add KLEE. Resent-From: =?UTF-8?Q?S=C3=B6ren?= Tempel Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 13 Feb 2024 14:11:02 +0000 Resent-Message-ID: Resent-Sender: help-debbugs@gnu.org X-GNU-PR-Message: followup 68296 X-GNU-PR-Package: guix-patches X-GNU-PR-Keywords: patch To: Julien Lepiller Cc: 68296@debbugs.gnu.org X-Debbugs-Original-Cc: 68296@debbugs.gnu.org, guix-patches@gnu.org Received: via spool by 68296-submit@debbugs.gnu.org id=B68296.170783344929107 (code B ref 68296); Tue, 13 Feb 2024 14:11:02 +0000 Received: (at 68296) by debbugs.gnu.org; 13 Feb 2024 14:10:49 +0000 Received: from localhost ([127.0.0.1]:43439 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtUn-0007ZP-8F for submit@debbugs.gnu.org; Tue, 13 Feb 2024 09:10:49 -0500 Received: from magnesium.8pit.net ([45.76.88.171]:9409) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtUk-0007ZA-0j for 68296@debbugs.gnu.org; Tue, 13 Feb 2024 09:10:47 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=TZY7ulg/ad cwRQxaSFDNNve8KgVHCLns3zCvl/LpARE=; h=in-reply-to:references:from: subject:cc:to:date; d=soeren-tempel.net; b=znt04q/79dPi0ONLPuZdU/QMWlj R+fv5EfYOA3uUY6M7yBUoa/sDDKqyqL23bU42toPBYiReCTFcIZzSPdnVISA89fH1pPsLP eEDvuMBA4QqxKPZcAwE7G+dZuLHNSq1xBQwQp8L2LLDMD7e8fDFGZWRPCKyMHpGmhA13DI H4+0= Received: from localhost (dynamic-2a02-3102-49da-001b-2b04-5c0d-7bef-ac8d.310.pool.telefonica.de [2a02:3102:49da:1b:2b04:5c0d:7bef:ac8d]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 9b18339f (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Tue, 13 Feb 2024 15:10:27 +0100 (CET) Date: Tue, 13 Feb 2024 15:09:12 +0100 From: =?UTF-8?Q?S=C3=B6ren?= Tempel References: <890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@soeren-tempel.net> In-Reply-To: Message-Id: <3TGIYFPTVHXE1.3QGMCQNGUI376@8pit.net> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list X-BeenThere: guix-patches@gnu.org List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: guix-patches-bounces+larch=yhetil.org@gnu.org Sender: guix-patches-bounces+larch=yhetil.org@gnu.org X-Migadu-Flow: FLOW_IN X-Migadu-Country: US X-Migadu-Spam-Score: 2.53 X-Migadu-Queue-Id: 886295F92A X-Spam-Score: 2.53 X-Migadu-Scanner: mx11.migadu.com X-TUID: sVZdzOX3gTPg Hi Julien, Thanks a lot for your feedback! I send an updated revision of the patchset based on your feedback. More information on changes below. Julien Lepiller wrote: > First, could you separate this in two patches, one per package? Sorry, oversight on my part. Fixed! > Is there a reason why this is limited to the x86_64 architecture? Yes, despite operating on LLVM IR abstraction, KLEE is tightly integrated with the host architecture. Therefore, upstream currently only support x86_64. Packages for other package manager (e.g. Nix) also only support KLEE on x86_64 [1]. I added a comment explaining this. > You have mixed native and normal inputs. In uclibc, since python is > only used for the build, it should be native. Fixed, ncurses should also be native as it is only used for menuconfig. > Does it make sense to propagate uclibc in klee, when it only contains > a static library? Some for clang and llvm. Isn't z3 used at runtime? > Shouldn't it be propagated? Sorry, I should have done a better job at explaining this: KLEE is a symbolic analyzer for LLVM IR. Users of KLEE will need to translate their C/C++ source to LLVM IR in order to analyze it with KLEE [2]. Furthermore, as KLEE is tightly integrated with a specific LLVM version, it makes (at least from my point of view) sense to propagate a specific clang toolchain so users can just run `guix shell klee` and get started with it. However, if preferred I can also remove the propagation. z3 isn't used at runtime, KLEE just uses the Z3 library interface and links against z3. AFAIK, it doesn't use any binaries from z3. Does z3 still need to be propagated in this case? uclibc does not need to be a propagated input since the KLEE build systems generates LLVM IR from the .a archive [3]. I fixed this. > Using #$klee-uclibc directly in the phase could be problematic I > think, you should use this-package-inputs or similar (can't remember > the exact name or syntax right now, you can leave it to me if you > don't find it). Sorry, I am new to Guix so I am not sure what you mean. Let me know if you have more information on this but also feel free to just adjust this as you wish :) Greetings S=C3=B6ren [1]: https://github.com/NixOS/nixpkgs/blob/40a7b182e0a00245d69f6b8c1dfd3ea4= bfc6257c/pkgs/applications/science/logic/klee/default.nix [2]: https://klee.github.io/tutorials/testing-function/#compiling-to-llvm-b= itcode [3]: https://github.com/klee/klee/blob/v3.0/CMakeLists.txt#L473-L487