From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mp1.migadu.com ([2001:41d0:403:4876::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by ms8.migadu.com with LMTPS id mKL6Cz0ty2Vv0AAA62LTzQ:P1 (envelope-from ) for ; Tue, 13 Feb 2024 09:50:05 +0100 Received: from aspmx1.migadu.com ([2001:41d0:403:4876::]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits)) by mp1.migadu.com with LMTPS id mKL6Cz0ty2Vv0AAA62LTzQ (envelope-from ) for ; Tue, 13 Feb 2024 09:50:05 +0100 X-Envelope-To: larch@yhetil.org Authentication-Results: aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=OJkSlLLd; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); 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" ARC-Seal: i=1; s=key1; d=yhetil.org; t=1707814205; a=rsa-sha256; cv=none; b=RYs7soYdtyN1j2spq3yOa3PBDQFbKKi4zXBByFRhoPmuMl9+FCpgiQUfRXRNgjIQjCWx2e Aa/fWm43EwsYg9QvnlPO74OeqWUP3EuIiZhuULxS1NIAJiIc5Fi57maKzWXXN4Sf0K4nuy npd940lRFw5LqyCGVQ7TbPZFZpPZ2PPx6LqLKHSkJ4CRGdFBkr7EYva5awyTAvR+gXv0+R UZHcMgi+s4tD/4xHLIKcokBnHBFAobHubcl0A736T9UDqMnosXqT/1yvj8jRlGYQtmgJLW CtF4cHke+IUj6PfW80uM/HcrLDry5tFr6Bi8EJ+DHYmJaMTwejzOktHNr1/jfg== ARC-Authentication-Results: i=1; aspmx1.migadu.com; dkim=fail ("headers rsa verify failed") header.d=lepiller.eu header.s=dkim header.b=OJkSlLLd; dmarc=fail reason="SPF not aligned (relaxed)" header.from=lepiller.eu (policy=none); 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" ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=yhetil.org; s=key1; t=1707814205; h=from:from:sender:sender:reply-to:subject:subject:date:date: message-id:message-id:to:to: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=76CMCZIe4b6dai4Pr5zyxSdf90CdAyObmYt+l2eyCF8=; b=WAIH+y6ccuRh+jpURR/BH9ssq2G+ijkb0nOR/XfrEavSSOX9iZveamdPzDD7UCgSYvLdDV vuaKYNe3JsdQXfuHcWdm+NVvLy43rhzZ/2EhRekmhVxZebY+FiWwOhI8EmjWzO0a/ydQZk oUsd90v81082ucOUAuVef23g/6KCMkOUsJ3ghvznNtz/dBBlSnQbpcPpirGCo9rWKh52YA 0Gs4TmHUwlql0Orw1174sah8HPLXadvViQ9oFBfmQIZfRDne7k6vOUeR2NJkZNBlPd2qDO eV8H3Nm+OwvgPYGvxY8pyMAN0NJK3VvtZYR70G6bMNHcf6RbmRIAVKklFn9d5Q== 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 A69E471794 for ; Tue, 13 Feb 2024 09:50:04 +0100 (CET) Received: from localhost ([::1] helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1rZoUB-0006DC-MG; Tue, 13 Feb 2024 03:49:52 -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 1rZoU5-0006Cw-Mx for guix-patches@gnu.org; Tue, 13 Feb 2024 03:49:45 -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 1rZoU5-0007PQ-F2 for guix-patches@gnu.org; Tue, 13 Feb 2024 03:49:45 -0500 Received: from Debian-debbugs by debbugs.gnu.org with local (Exim 4.84_2) (envelope-from ) id 1rZoUM-0000q0-OH for guix-patches@gnu.org; Tue, 13 Feb 2024 03:50:02 -0500 X-Loop: help-debbugs@gnu.org Subject: [bug#68296] [PATCH] gnu: Add KLEE. Resent-From: Julien Lepiller Original-Sender: "Debbugs-submit" Resent-CC: guix-patches@gnu.org Resent-Date: Tue, 13 Feb 2024 08:50: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: 68296@debbugs.gnu.org, soeren@soeren-tempel.net X-Debbugs-Original-To: guix-patches@gnu.org, soeren@soeren-tempel.net, 68296@debbugs.gnu.org Received: via spool by 68296-submit@debbugs.gnu.org id=B68296.17078141793142 (code B ref 68296); Tue, 13 Feb 2024 08:50:02 +0000 Received: (at 68296) by debbugs.gnu.org; 13 Feb 2024 08:49:39 +0000 Received: from localhost ([127.0.0.1]:41306 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZoTy-0000oa-1b for submit@debbugs.gnu.org; Tue, 13 Feb 2024 03:49:39 -0500 Received: from lepiller.eu ([89.234.186.109]:39776) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZoTv-0000oL-59 for 68296@debbugs.gnu.org; Tue, 13 Feb 2024 03:49:36 -0500 Received: from lepiller.eu (localhost [127.0.0.1]) by lepiller.eu (OpenSMTPD) with ESMTP id ed9954df; Tue, 13 Feb 2024 08:49:15 +0000 (UTC) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed; d=lepiller.eu; h=date:from :to:subject:in-reply-to:references:message-id:mime-version :content-type:content-transfer-encoding; s=dkim; bh=zb/BciQq7mVb 5+SC1Ng6HvjPLOhllCu+xyh/5/M99g8=; b=OJkSlLLdwflD23UQRWL7K+06nA2P W3aWmBxbsm5jsEygkNu7V7pMPASSL7untauIwft7dK7JkTSaUPgevgdDOzRN3crZ keMSezAq3AHwMPuV0mfpuv0ph2xQ8WV83TepXwR4wn5s2sivloS9QkddbXctFw8a LdHSfLmFcMDoVHffdpA99TnNkW5ok/M4k2VZ6WDwYvVWI4QXP/8Eu4c7n/aPumNW ycmEy/KKEjgscLGlThYIieGGzZiQzJQVjQVNBThu+iSglivY29m7S0FAa2H2kHIo LFX2Wen66n6P33Uwg9Pn/BV4BSR9qOdx5AS+Yt1uy4ZCE2ap04iEvIVZsQ== Received: by lepiller.eu (OpenSMTPD) with ESMTPSA id 5d2061db (TLSv1.3:TLS_AES_256_GCM_SHA384:256:NO); Tue, 13 Feb 2024 08:49:14 +0000 (UTC) Date: Tue, 13 Feb 2024 09:49:12 +0100 From: Julien Lepiller User-Agent: K-9 Mail for Android In-Reply-To: <890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@soeren-tempel.net> References: <890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@soeren-tempel.net> Message-ID: 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-Scanner: mx10.migadu.com X-Spam-Score: -5.38 X-Migadu-Queue-Id: A69E471794 X-Migadu-Spam-Score: -5.38 X-TUID: aNWyOQSThYe7 Le 6 janvier 2024 21:40:41 GMT+01:00, soeren@soeren-tempel=2Enet a =C3=A9cr= it=C2=A0: >From: S=C3=B6ren Tempel > >* gnu/packages/check=2Escm (klee-uclibc): New variable=2E >* gnu/packages/check=2Escm (klee): New variable=2E > >Signed-off-by: S=C3=B6ren Tempel >--- >This is a new package for KLEE, a popular piece of academic software >in the software engineering domain=2E KLEE implements a technique called >symbolic execution >which allows for automated testing of software through SMT solving=2E >KLEE forms the basis for a lot of research in the symbolic execution >domain =2E Packaging KLEE and >other related tools, eases using Guix for conducting reproducible >research in this domain=2E I have Guix packages for other symbolic >execution tools which I also would like to upstream in the future, >I figured I would start with KLEE as it has little to no dependencies=2E > >I tested this package by conforming that the basic upstream tutorials >work as intended, e=2Eg=2E =2E > >This is my first Guix package, hence CC'ing the mentors=2E > > gnu/packages/check=2Escm | 107 +++++++++++++++++++++++++++++++++++++++++ > 1 file changed, 107 insertions(+) > >diff --git a/gnu/packages/check=2Escm b/gnu/packages/check=2Escm >index 5181d3a164=2E=2E7e97e59955 100644 >--- a/gnu/packages/check=2Escm >+++ b/gnu/packages/check=2Escm >@@ -71,6 +71,7 @@ (define-module (gnu packages check) > #:use-module (gnu packages bash) > #:use-module (gnu packages cmake) > #:use-module (gnu packages compression) >+ #:use-module (gnu packages cpp) > #:use-module (gnu packages linux) > #:use-module (gnu packages llvm) > #:use-module (gnu packages glib) >@@ -79,6 +80,8 @@ (define-module (gnu packages check) > #:use-module (gnu packages gtk) > #:use-module (gnu packages guile) > #:use-module (gnu packages guile-xyz) >+ #:use-module (gnu packages maths) >+ #:use-module (gnu packages ncurses) > #:use-module (gnu packages perl) > #:use-module (gnu packages pkg-config) > #:use-module (gnu packages python) >@@ -87,6 +90,7 @@ (define-module (gnu packages check) > #:use-module (gnu packages python-web) > #:use-module (gnu packages python-xyz) > #:use-module (gnu packages python-science) >+ #:use-module (gnu packages sqlite) > #:use-module (gnu packages texinfo) > #:use-module (gnu packages time) > #:use-module (gnu packages xml) >@@ -3648,3 +3652,106 @@ (define-public subunit > command line filters to process a subunit stream and language bindings f= or > Python, C, C++ and shell=2E Bindings are easy to write for other langua= ges=2E") > (license (list license:asl2=2E0 license:bsd-3)))) ;user can pick >+ >+(define-public klee-uclibc >+ (let ((commit "955d502cc1f0688e82348304b053ad787056c754")) >+ (package >+ (name "klee-uclibc") >+ (version (git-version "20230612" "0" commit)) >+ (source >+ (origin >+ (method git-fetch) >+ (uri (git-reference >+ (url "https://github=2Ecom/klee/klee-uclibc") >+ (commit commit))) >+ (file-name (git-file-name name version)) >+ (sha256 >+ (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j"= )))) >+ (build-system gnu-build-system) >+ (supported-systems '("x86_64-linux")) >+ (arguments >+ `(#:tests? #f ;upstream uClibc tests do not work in the fork >+ #:phases (modify-phases %standard-phases >+ ;; Disable locales as these would have to be downloa= ded and >+ ;; shouldn't really be needed for symbolic execution= either=2E >+ (add-after 'unpack 'patch-config >+ (lambda _ >+ (substitute* "klee-premade-configs/x86_64/config= " >+ (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=3D= y") >+ "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=3Dn= ") >+ (("UCLIBC_PREGENERATED_LOCALE_DATA=3Dy") >+ "UCLIBC_PREGENERATED_LOCALE_DATA=3Dn") >+ (("UCLIBC_HAS_LOCALE=3Dy") >+ "UCLIBC_HAS_LOCALE=3Dn") >+ (("UCLIBC_HAS_XLOCALE=3Dy") >+ "UCLIBC_HAS_XLOCALE=3Dn")))) >+ >+ ;; Upstream uses a custom non-GNU configure script w= ritten >+ ;; in Python, replace the default configure phase ac= cordingly=2E >+ (replace 'configure >+ (lambda _ >+ (invoke "=2E/configure" >+ "--make-llvm-lib" >+ "--enable-release"))) >+ >+ ;; Custom install phase to only install the libc=2Ea= file manually=2E >+ ;; This is the only file which is used/needed by KLE= E itself=2E >+ (replace 'install >+ (lambda* (#:key outputs #:allow-other-keys) >+ (install-file "lib/libc=2Ea" >+ (string-append (assoc-ref outputs = "out") >+ "/lib"))))))) >+ (inputs (list clang-toolchain-13 python ncurses)) >+ (synopsis "Variant of uClibc tailored to symbolic execution") >+ (description >+ "Modified version of uClibc for symbolic execution of >+Unix userland software=2E This library can only be used in conjunction >+with the @code{klee} package=2E") >+ (home-page "https://klee=2Egithub=2Eio/") >+ (license license:lgpl2=2E1)))) >+ >+(define-public klee >+ (package >+ (name "klee") >+ (version "3=2E0") >+ (source >+ (origin >+ (method git-fetch) >+ (uri (git-reference >+ (url "https://github=2Ecom/klee/klee") >+ (commit (string-append "v" version)))) >+ (sha256 >+ (base32 "0dj20nazkcq84ryr87dihvjznapsbl1n21sa8dhhnb0wsad5d6fb")) >+ (file-name (git-file-name name version)))) >+ (build-system cmake-build-system) >+ (supported-systems '("x86_64-linux")) >+ (arguments >+ `(#:test-target "systemtests" >+ #:strip-directories '("bin") >+ #:configure-flags ,#~(list "-DENABLE_KLEE_ASSERTS=3DOFF" >+ "-DENABLE_TCMALLOC=3DON" >+ "-DENABLE_POSIX_RUNTIME=3DON" >+ (string-append "-DKLEE_UCLIBC_PATH=3D" >+ #$klee-uclibc)) >+ #:phases (modify-phases %standard-phases >+ (add-after 'unpack 'patch-lit-config >+ (lambda _ >+ ;; Make sure that we retain the value of the GUIX_= PYTHONPATH >+ ;; environment variable in the test environmented = created by >+ ;; python-lit=2E Otherwise, the test scripts won't= be able to >+ ;; find the python-tabulate dependency, causing te= st failures=2E >+ (substitute* "test/lit=2Ecfg" >+ (("addEnv\\('PWD'\\)" env) >+ (string-append env "\n" "addEnv('GUIX_PYTHONPAT= H')")))))))) >+ (propagated-inputs (list klee-uclibc clang-toolchain-13 llvm-13 pyth= on >+ python-tabulate)) >+ (inputs (list python-lit z3 gperftools sqlite)) >+ (synopsis >+ "Symbolic execution engine built on top of the LLVM compiler infast= ructure") >+ (description >+ "Dynamic symbolic execution engine built on top of >+LLVM=2E Symbolic execution is an automated software testing technique, >+KLEE leverage this technique to automatically generate test cases for >+software compiled to LLVM IR=2E") >+ (home-page "https://klee=2Egithub=2Eio/") >+ (license (list license:expat license:bsd-4)))) > >base-commit: 29c94dd522833b2603a651c14a5b06120bcf1829 > > > Hi S=C3=B6ren, I'm sorry nobody looked at this before=2E Here are a few remarks=2E First, could you separate this in two patches, one per package? Is there a reason why this is limited to the x86_64 architecture? You have mixed native and normal inputs=2E In uclibc, since python is only= used for the build, it should be native=2E Does it make sense to propagate uclibc in klee, when it only contains a st= atic library? Some for clang and llvm=2E Isn't z3 used at runtime? Shouldn'= t it be propagated? Using #$klee-uclibc directly in the phase could be problematic I think, yo= u 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)=2E Otherwise, looks good for a first patch :)