From unknown Sat Sep 20 18:58:07 2025 Content-Disposition: inline Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-Mailer: MIME-tools 5.509 (Entity 5.509) Content-Type: text/plain; charset=utf-8 From: bug#68296 <68296@debbugs.gnu.org> To: bug#68296 <68296@debbugs.gnu.org> Subject: Status: [PATCH] gnu: Add KLEE. Reply-To: bug#68296 <68296@debbugs.gnu.org> Date: Sun, 21 Sep 2025 01:58:07 +0000 retitle 68296 [PATCH] gnu: Add KLEE. reassign 68296 guix-patches submitter 68296 soeren@soeren-tempel.net severity 68296 normal tag 68296 patch thanks From debbugs-submit-bounces@debbugs.gnu.org Sat Jan 06 15:49:15 2024 Received: (at submit) by debbugs.gnu.org; 6 Jan 2024 20:49:15 +0000 Received: from localhost ([127.0.0.1]:60329 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rMDbW-00052z-R4 for submit@debbugs.gnu.org; Sat, 06 Jan 2024 15:49:15 -0500 Received: from lists.gnu.org ([2001:470:142::17]:51408) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rMDbV-00052n-AH for submit@debbugs.gnu.org; Sat, 06 Jan 2024 15:49:14 -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 1rMDbK-0003rL-IQ for guix-patches@gnu.org; Sat, 06 Jan 2024 15:49:02 -0500 Received: from magnesium.8pit.net ([45.76.88.171]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1rMDbI-0006AJ-79; Sat, 06 Jan 2024 15:49:02 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=Rp8vwAS+Ii gH1BWSEwmr55Dc/5d04LLRYmPUyC+DEu4=; h=date:subject:to:from; d=soeren-tempel.net; b=nPwsls4aCgPKk2SDYAWFnohzoimDmxQFBHZpn8jM7C190k2 OmczvEsvjQqmO0ZipdKFim2Ps1Pyhf13shwF5do4EP5jAAK7lfNoUUrvrZ33DG0I+JNoEJ A6mezbFJDLv/cp2RaZR8gz3AVZGspIoY1FoDj2d2gViVXMZcprkeV8= Received: from localhost (dynamic-2a02-3102-49da-001b-e576-f39c-a415-1e23.310.pool.telefonica.de [2a02:3102:49da:1b:e576:f39c:a415:1e23]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 0b1cbe9f (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Sat, 6 Jan 2024 21:48:55 +0100 (CET) From: soeren@soeren-tempel.net To: guix-patches@gnu.org Subject: [PATCH] gnu: Add KLEE. Date: Sat, 6 Jan 2024 21:40:41 +0100 Message-ID: <890dc6595ccef88cb60ff0a380be9d323df479aa.1704573641.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.43.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Received-SPF: pass client-ip=45.76.88.171; envelope-from=soeren@soeren-tempel.net; helo=magnesium.8pit.net X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: 0.9 (/) X-Debbugs-Envelope-To: submit X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.1 (/) From: Sören Tempel * gnu/packages/check.scm (klee-uclibc): New variable. * gnu/packages/check.scm (klee): New variable. Signed-off-by: Sören Tempel --- This is a new package for KLEE, a popular piece of academic software in the software engineering domain. KLEE implements a technique called symbolic execution which allows for automated testing of software through SMT solving. KLEE forms the basis for a lot of research in the symbolic execution domain . Packaging KLEE and other related tools, eases using Guix for conducting reproducible research in this domain. 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. I tested this package by conforming that the basic upstream tutorials work as intended, e.g. . This is my first Guix package, hence CC'ing the mentors. gnu/packages/check.scm | 107 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index 5181d3a164..7e97e59955 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -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 for Python, C, C++ and shell. Bindings are easy to write for other languages.") (license (list license:asl2.0 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.com/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 downloaded and + ;; shouldn't really be needed for symbolic execution either. + (add-after 'unpack 'patch-config + (lambda _ + (substitute* "klee-premade-configs/x86_64/config" + (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_HAS_LOCALE=y") + "UCLIBC_HAS_LOCALE=n") + (("UCLIBC_HAS_XLOCALE=y") + "UCLIBC_HAS_XLOCALE=n")))) + + ;; Upstream uses a custom non-GNU configure script written + ;; in Python, replace the default configure phase accordingly. + (replace 'configure + (lambda _ + (invoke "./configure" + "--make-llvm-lib" + "--enable-release"))) + + ;; Custom install phase to only install the libc.a file manually. + ;; This is the only file which is used/needed by KLEE itself. + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (install-file "lib/libc.a" + (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. This library can only be used in conjunction +with the @code{klee} package.") + (home-page "https://klee.github.io/") + (license license:lgpl2.1)))) + +(define-public klee + (package + (name "klee") + (version "3.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/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=OFF" + "-DENABLE_TCMALLOC=ON" + "-DENABLE_POSIX_RUNTIME=ON" + (string-append "-DKLEE_UCLIBC_PATH=" + #$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. Otherwise, the test scripts won't be able to + ;; find the python-tabulate dependency, causing test failures. + (substitute* "test/lit.cfg" + (("addEnv\\('PWD'\\)" env) + (string-append env "\n" "addEnv('GUIX_PYTHONPATH')")))))))) + (propagated-inputs (list klee-uclibc clang-toolchain-13 llvm-13 python + python-tabulate)) + (inputs (list python-lit z3 gperftools sqlite)) + (synopsis + "Symbolic execution engine built on top of the LLVM compiler infastructure") + (description + "Dynamic symbolic execution engine built on top of +LLVM. Symbolic execution is an automated software testing technique, +KLEE leverage this technique to automatically generate test cases for +software compiled to LLVM IR.") + (home-page "https://klee.github.io/") + (license (list license:expat license:bsd-4)))) base-commit: 29c94dd522833b2603a651c14a5b06120bcf1829 From debbugs-submit-bounces@debbugs.gnu.org Tue Feb 13 03:49:39 2024 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 To: guix-patches@gnu.org, soeren@soeren-tempel.net, 68296@debbugs.gnu.org Subject: Re: [bug#68296] [PATCH] gnu: Add KLEE. 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-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: 68296 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.3 (/) 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 :) From debbugs-submit-bounces@debbugs.gnu.org Tue Feb 13 09:09:28 2024 Received: (at 68296) by debbugs.gnu.org; 13 Feb 2024 14:09:28 +0000 Received: from localhost ([127.0.0.1]:43411 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtTT-0007V9-Eo for submit@debbugs.gnu.org; Tue, 13 Feb 2024 09:09:28 -0500 Received: from magnesium.8pit.net ([45.76.88.171]:24699) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtTQ-0007Uv-6z; Tue, 13 Feb 2024 09:09:25 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=pngbtM32y6 fF+mUesk3yhGISnVUe/HVOK1IST0UHWGk=; h=date:subject:to:from; d=soeren-tempel.net; b=E+ZstjjUTRqTF1eezGbNxh+QliCnADz8/DqSHmatsMdn4ke Pn2VoRjHAh7oIvBKAXTl2fI0L6tXU0DHkdi46CEcVk4NejPp98ze3KSC7pJkTxf+pcSmTq wEaJWxyIAww14wbKuXBKl5NGbykDGSMsXqxntfUjAjD2luQ2j5TZ48= Received: from localhost (dynamic-2a02-3102-49da-001b-df49-33b7-2af2-ff52.310.pool.telefonica.de [2a02:3102:49da:1b:df49:33b7:2af2:ff52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id b01068d1 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Tue, 13 Feb 2024 15:09:03 +0100 (CET) From: soeren@soeren-tempel.net To: 68296@debbugs.gnu.org Subject: [PATCH v2 1/2] gnu: Add klee-uclibc. Date: Tue, 13 Feb 2024 15:08:51 +0100 Message-ID: <168e4aa2bfe10a6b15190c93bd3453d665cebd33.1707833332.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.43.1 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: 68296 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.3 (/) From: Sören Tempel * gnu/packages/check.scm (klee-uclibc): New variable. Signed-off-by: Sören Tempel --- gnu/packages/check.scm | 62 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index 4f593cde8d..ecf48ab121 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -48,6 +48,7 @@ ;;; Copyright © 2023 Reza Housseini ;;; Copyright © 2023 Hilton Chain ;;; Copyright © 2023 Troy Figiel +;;; Copyright © 2024 Sören Tempel ;;; ;;; This file is part of GNU Guix. ;;; @@ -80,6 +81,7 @@ (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 ncurses) #:use-module (gnu packages perl) #:use-module (gnu packages pkg-config) #:use-module (gnu packages python) @@ -3610,3 +3612,63 @@ (define-public subunit command line filters to process a subunit stream and language bindings for Python, C, C++ and shell. Bindings are easy to write for other languages.") (license (list license:asl2.0 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.com/klee/klee-uclibc") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j")))) + (build-system gnu-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (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 downloaded and + ;; shouldn't really be needed for symbolic execution either. + (add-after 'unpack 'patch-config + (lambda _ + (substitute* "klee-premade-configs/x86_64/config" + (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_HAS_LOCALE=y") + "UCLIBC_HAS_LOCALE=n") + (("UCLIBC_HAS_XLOCALE=y") + "UCLIBC_HAS_XLOCALE=n")))) + + ;; Upstream uses a custom non-GNU configure script written + ;; in Python, replace the default configure phase accordingly. + (replace 'configure + (lambda _ + (invoke "./configure" + "--make-llvm-lib" + "--enable-release"))) + + ;; Custom install phase to only install the libc.a file manually. + ;; This is the only file which is used/needed by KLEE itself. + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (install-file "lib/libc.a" + (string-append (assoc-ref outputs "out") + "/lib"))))))) + (inputs (list clang-toolchain-13)) + ;; ncurses is only needed for the `make menuconfig` interface. + (native-inputs (list python ncurses)) + (synopsis "Variant of uClibc tailored to symbolic execution") + (description + "Modified version of uClibc for symbolic execution of +Unix userland software. This library can only be used in conjunction +with the @code{klee} package.") + (home-page "https://klee.github.io/") + (license license:lgpl2.1)))) base-commit: 85e67f7feac14a1290022b9500c333c51c7f3ca3 From debbugs-submit-bounces@debbugs.gnu.org Tue Feb 13 09:09:36 2024 Received: (at 68296) by debbugs.gnu.org; 13 Feb 2024 14:09:36 +0000 Received: from localhost ([127.0.0.1]:43415 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtTc-0007Vi-4V for submit@debbugs.gnu.org; Tue, 13 Feb 2024 09:09:36 -0500 Received: from magnesium.8pit.net ([45.76.88.171]:1987) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtTZ-0007VS-WD; Tue, 13 Feb 2024 09:09:34 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=rOG/zgRWk/ DZoyG+E2MHrbdVWrSre/kTQKEtmB+4TUg=; h=references:in-reply-to:date: subject:to:from; d=soeren-tempel.net; b=ejQ03dDIY6ztY0aJiCM8dlMTUXklgS SWpd62QiyG6QkVyN0Tx8mKTfXq0XPtvHPoieWxFfq4ILobrGlSqA7AM/P0gs6zrtDEnd7j MNOAecE05ayQieN1keHlOEV99nPSLO8WLkfZNWWJAqYuNGCgcdmaChdqNkiYjgqYwpxcey 8= Received: from localhost (dynamic-2a02-3102-49da-001b-df49-33b7-2af2-ff52.310.pool.telefonica.de [2a02:3102:49da:1b:df49:33b7:2af2:ff52]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id f5096164 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Tue, 13 Feb 2024 15:09:12 +0100 (CET) From: soeren@soeren-tempel.net To: 68296@debbugs.gnu.org Subject: [PATCH v2 2/2] gnu: Add klee. Date: Tue, 13 Feb 2024 15:08:52 +0100 Message-ID: X-Mailer: git-send-email 2.43.1 In-Reply-To: <168e4aa2bfe10a6b15190c93bd3453d665cebd33.1707833332.git.soeren@soeren-tempel.net> References: <168e4aa2bfe10a6b15190c93bd3453d665cebd33.1707833332.git.soeren@soeren-tempel.net> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.7 (/) X-Debbugs-Envelope-To: 68296 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -0.3 (/) From: Sören Tempel * gnu/packages/check.scm (klee): New variable. Signed-off-by: Sören Tempel --- gnu/packages/check.scm | 52 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 52 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index ecf48ab121..82c40b63b1 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -73,6 +73,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) @@ -81,6 +82,7 @@ (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) @@ -90,6 +92,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) @@ -3672,3 +3675,52 @@ (define-public klee-uclibc with the @code{klee} package.") (home-page "https://klee.github.io/") (license license:lgpl2.1)))) + +(define-public klee + (package + (name "klee") + (version "3.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/klee/klee") + (commit (string-append "v" version)))) + (sha256 + (base32 "0dj20nazkcq84ryr87dihvjznapsbl1n21sa8dhhnb0wsad5d6fb")) + (file-name (git-file-name name version)))) + (build-system cmake-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (supported-systems '("x86_64-linux")) + (arguments + `(#:test-target "systemtests" + #:strip-directories '("bin") + #:configure-flags ,#~(list "-DENABLE_KLEE_ASSERTS=OFF" + "-DENABLE_TCMALLOC=ON" + "-DENABLE_POSIX_RUNTIME=ON" + (string-append "-DKLEE_UCLIBC_PATH=" + #$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. Otherwise, the test scripts won't be able to + ;; find the python-tabulate dependency, causing test failures. + (substitute* "test/lit.cfg" + (("addEnv\\('PWD'\\)" env) + (string-append env "\n" "addEnv('GUIX_PYTHONPATH')")))))))) + ;; KLEE operates on LLVM IR generated by a specific toolchain version. + ;; Propergate the toolchain to allow users to transform code to this version. + (propagated-inputs (list clang-toolchain-13 llvm-13 python python-tabulate)) + (inputs (list z3 gperftools sqlite)) + (native-inputs (list python-lit)) + (synopsis + "Symbolic execution engine built on top of the LLVM compiler infastructure") + (description + "Dynamic symbolic execution engine built on top of +LLVM. Symbolic execution is an automated software testing technique, +KLEE leverage this technique to automatically generate test cases for +software compiled to LLVM IR.") + (home-page "https://klee.github.io/") + (license (list license:expat license:bsd-4)))) From debbugs-submit-bounces@debbugs.gnu.org Tue Feb 13 09:10:56 2024 Received: (at submit) by debbugs.gnu.org; 13 Feb 2024 14:10:56 +0000 Received: from localhost ([127.0.0.1]:43442 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtUt-0007Zi-Ob for submit@debbugs.gnu.org; Tue, 13 Feb 2024 09:10:56 -0500 Received: from lists.gnu.org ([209.51.188.17]:45602) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rZtUr-0007Za-UT for submit@debbugs.gnu.org; Tue, 13 Feb 2024 09:10:54 -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 1rZtUa-0007bA-6b for guix-patches@gnu.org; Tue, 13 Feb 2024 09:10:36 -0500 Received: from magnesium.8pit.net ([45.76.88.171]) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1rZtUY-0002py-7w for guix-patches@gnu.org; Tue, 13 Feb 2024 09:10:35 -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 To: Julien Lepiller Subject: Re: [bug#68296] [PATCH] gnu: Add KLEE. 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 Received-SPF: pass client-ip=45.76.88.171; envelope-from=soeren@soeren-tempel.net; helo=magnesium.8pit.net X-Spam_score_int: -20 X-Spam_score: -2.1 X-Spam_bar: -- X-Spam_report: (-2.1 / 5.0 requ) BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, SPF_HELO_NONE=0.001, SPF_PASS=-0.001, T_SCC_BODY_TEXT_LINE=-0.01 autolearn=ham autolearn_force=no X-Spam_action: no action X-Spam-Score: -0.6 (/) X-Debbugs-Envelope-To: submit Cc: 68296@debbugs.gnu.org, guix-patches@gnu.org X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.6 (-) 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 From debbugs-submit-bounces@debbugs.gnu.org Wed Feb 28 12:40:23 2024 Received: (at 68296) by debbugs.gnu.org; 28 Feb 2024 17:40:23 +0000 Received: from localhost ([127.0.0.1]:56923 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rfNuo-0007b9-5L for submit@debbugs.gnu.org; Wed, 28 Feb 2024 12:40:23 -0500 Received: from magnesium.8pit.net ([45.76.88.171]:45015) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rfNPs-00062k-2p; Wed, 28 Feb 2024 12:08:27 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=dBZcFcOWKA 7HHKM4gY/KZOQRed0KohARWQaTBXGblMM=; h=date:subject:to:from; d=soeren-tempel.net; b=qxmy3mSC9rmXLNXPnIfuU/0TH0KMfKZ+6Kwc1mjXmIPYomf 7MGpKReRkik6s8b/tnB/ZNMwVIynzS0V+vc2qGZwsaQ9eztv+z8zhpPHmpXt3EzhqdL80b rz+fFz7MTi1Rz6Lpp5fZsK8+8+D9KSMhxFBjjFHdnVx0ixkOcV2x28= Received: from localhost (dynamic-2a02-3102-49da-001b-77ea-c25c-fe03-c73c.310.pool.telefonica.de [2a02:3102:49da:1b:77ea:c25c:fe03:c73c]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 581ad21b (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Wed, 28 Feb 2024 18:06:39 +0100 (CET) From: soeren@soeren-tempel.net To: 68296@debbugs.gnu.org Subject: [PATCH v3 1/2] gnu: Add klee-uclibc. Date: Wed, 28 Feb 2024 18:04:45 +0100 Message-ID: <99fdb88daa1db94c659f2c79b42b39c704fd8bde.1709139885.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.44.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 68296 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/check.scm (klee-uclibc): New variable. Signed-off-by: Sören Tempel --- Changes since v2: Rebase against the current master branch, this resolves a merge conflict in the copyright comment section. No functional changes. gnu/packages/check.scm | 62 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index 5428098c15..50fd105b2c 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -49,6 +49,7 @@ ;;; Copyright © 2023 Hilton Chain ;;; Copyright © 2023 Troy Figiel ;;; Copyright © 2024 Giacomo Leidi +;;; Copyright © 2024 Sören Tempel ;;; ;;; This file is part of GNU Guix. ;;; @@ -82,6 +83,7 @@ (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 ncurses) #:use-module (gnu packages perl) #:use-module (gnu packages pkg-config) #:use-module (gnu packages python) @@ -3635,3 +3637,63 @@ (define-public subunit command line filters to process a subunit stream and language bindings for Python, C, C++ and shell. Bindings are easy to write for other languages.") (license (list license:asl2.0 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.com/klee/klee-uclibc") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j")))) + (build-system gnu-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (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 downloaded and + ;; shouldn't really be needed for symbolic execution either. + (add-after 'unpack 'patch-config + (lambda _ + (substitute* "klee-premade-configs/x86_64/config" + (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_HAS_LOCALE=y") + "UCLIBC_HAS_LOCALE=n") + (("UCLIBC_HAS_XLOCALE=y") + "UCLIBC_HAS_XLOCALE=n")))) + + ;; Upstream uses a custom non-GNU configure script written + ;; in Python, replace the default configure phase accordingly. + (replace 'configure + (lambda _ + (invoke "./configure" + "--make-llvm-lib" + "--enable-release"))) + + ;; Custom install phase to only install the libc.a file manually. + ;; This is the only file which is used/needed by KLEE itself. + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (install-file "lib/libc.a" + (string-append (assoc-ref outputs "out") + "/lib"))))))) + (inputs (list clang-toolchain-13)) + ;; ncurses is only needed for the `make menuconfig` interface. + (native-inputs (list python ncurses)) + (synopsis "Variant of uClibc tailored to symbolic execution") + (description + "Modified version of uClibc for symbolic execution of +Unix userland software. This library can only be used in conjunction +with the @code{klee} package.") + (home-page "https://klee.github.io/") + (license license:lgpl2.1)))) base-commit: bc6840316c665e5959469e5c857819142cc4a47b From debbugs-submit-bounces@debbugs.gnu.org Wed Feb 28 12:40:24 2024 Received: (at 68296) by debbugs.gnu.org; 28 Feb 2024 17:40:24 +0000 Received: from localhost ([127.0.0.1]:56927 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rfNup-0007bI-8i for submit@debbugs.gnu.org; Wed, 28 Feb 2024 12:40:24 -0500 Received: from magnesium.8pit.net ([45.76.88.171]:45015) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rfNPw-00062k-AC; Wed, 28 Feb 2024 12:08:32 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=simple/simple; s=opensmtpd; bh=DC/tywyrx2 ZkwZyVFOIgi33ienDylxvLpZfID3OkgUM=; h=references:in-reply-to:date: subject:to:from; d=soeren-tempel.net; b=H8s8geFvYzZGN6cyNFBxyJDTaoR0ec hBNoExqzHNfgph2ED2w6E2sZu88z1Sx1NZzeDUvvBHdJLSlD2bRgbtndKz18s83d1IBDMa b9NB4JJOAA0dKmaU87Dk1+JB08BiF6tpnfnC5Veq+RMSksN6JtwYsPpHgz1zzNFs0uS4Zh Y= Received: from localhost (dynamic-2a02-3102-49da-001b-77ea-c25c-fe03-c73c.310.pool.telefonica.de [2a02:3102:49da:1b:77ea:c25c:fe03:c73c]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 25a623a0 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Wed, 28 Feb 2024 18:06:58 +0100 (CET) From: soeren@soeren-tempel.net To: 68296@debbugs.gnu.org Subject: [PATCH v3 2/2] gnu: Add klee. Date: Wed, 28 Feb 2024 18:04:48 +0100 Message-ID: <262a52af77537ec120f0ac58a5d8c76d73a7aa92.1709139885.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.44.0 In-Reply-To: <99fdb88daa1db94c659f2c79b42b39c704fd8bde.1709139885.git.soeren@soeren-tempel.net> References: <99fdb88daa1db94c659f2c79b42b39c704fd8bde.1709139885.git.soeren@soeren-tempel.net> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 68296 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/check.scm (klee): New variable. Signed-off-by: Sören Tempel --- Changes since v2: Switch to a non-debug build-type to workaround an internal error being triggered in clang while building KLEE with it. gnu/packages/check.scm | 55 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index 50fd105b2c..534852f029 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -74,6 +74,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) @@ -83,6 +84,7 @@ (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) @@ -92,6 +94,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) @@ -3697,3 +3700,55 @@ (define-public klee-uclibc with the @code{klee} package.") (home-page "https://klee.github.io/") (license license:lgpl2.1)))) + +(define-public klee + (package + (name "klee") + (version "3.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/klee/klee") + (commit (string-append "v" version)))) + (sha256 + (base32 "0dj20nazkcq84ryr87dihvjznapsbl1n21sa8dhhnb0wsad5d6fb")) + (file-name (git-file-name name version)))) + (build-system cmake-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (supported-systems '("x86_64-linux")) + (arguments + `(#:test-target "systemtests" + ;; Default build type (RelWithDebInfo) causes an internal error + ;; in clang while compiling KLEE, hence use a different build type. + #:build-type "Release" + #:strip-directories '("bin") + #:configure-flags ,#~(list "-DENABLE_KLEE_ASSERTS=OFF" + "-DENABLE_TCMALLOC=ON" + "-DENABLE_POSIX_RUNTIME=ON" + (string-append "-DKLEE_UCLIBC_PATH=" + #$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. Otherwise, the test scripts won't be able to + ;; find the python-tabulate dependency, causing test failures. + (substitute* "test/lit.cfg" + (("addEnv\\('PWD'\\)" env) + (string-append env "\n" "addEnv('GUIX_PYTHONPATH')")))))))) + ;; KLEE operates on LLVM IR generated by a specific toolchain version. + ;; Propergate the toolchain to allow users to transform code to this version. + (propagated-inputs (list clang-toolchain-13 llvm-13 python python-tabulate)) + (inputs (list z3 gperftools sqlite)) + (native-inputs (list python-lit)) + (synopsis + "Symbolic execution engine built on top of the LLVM compiler infastructure") + (description + "Dynamic symbolic execution engine built on top of +LLVM. Symbolic execution is an automated software testing technique, +KLEE leverage this technique to automatically generate test cases for +software compiled to LLVM IR.") + (home-page "https://klee.github.io/") + (license (list license:expat license:bsd-4)))) From debbugs-submit-bounces@debbugs.gnu.org Mon Mar 11 05:54:43 2024 Received: (at 68296) by debbugs.gnu.org; 11 Mar 2024 09:54:44 +0000 Received: from localhost ([127.0.0.1]:38880 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rjcMl-0000VF-Md for submit@debbugs.gnu.org; Mon, 11 Mar 2024 05:54:43 -0400 Received: from magnesium.8pit.net ([45.76.88.171]:20090) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rjcMi-0000V5-G3 for 68296@debbugs.gnu.org; Mon, 11 Mar 2024 05:54:41 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=ZPB3glxr htKXVaOSrQrGklZpD+9abT6IXcHu5+55CZU=; h=from:subject:to:date; d=soeren-tempel.net; b=TrmnnFE29qdtkju1ICOvdQb8KQfe9QNKVlP9dXuciFgvsCX qvZTCH8XqceV/G7TksY/vuwmrLfBFin0wcCXT6nSOieXc4gB3kO2eJxEn+OkK+XoutO6Zv nXk7DVTlfgeF5Wp4FIw9uIRSb3tOd59AbkvTpl0EYp13nfSfnsnKBw= Received: from localhost (dynamic-2a02-3102-49da-001b-64ba-7ea6-b5d2-00d0.310.pool.telefonica.de [2a02:3102:49da:1b:64ba:7ea6:b5d2:d0]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id d096d53e (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES) for <68296@debbugs.gnu.org>; Mon, 11 Mar 2024 10:54:04 +0100 (CET) Date: Mon, 11 Mar 2024 10:54:03 +0100 To: 68296@debbugs.gnu.org Subject: Re: gnu: Add KLEE. From: =?UTF-8?Q?S=C3=B6ren?= Tempel Message-Id: <3209APKM19WGZ.39BXJ12FGTBCL@8pit.net> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 68296 X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hi, What does "QA: Investigate" mean? The build should be fixed now with the v3 revision. I don't see any build failures on the QA. Is there anything I need to do on my end in order to have the build restarted? Greetings S=C3=B6ren From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 28 15:21:02 2024 Received: (at 68296) by debbugs.gnu.org; 28 Mar 2024 19:21:02 +0000 Received: from localhost ([127.0.0.1]:41176 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rpvJ7-0007zo-Mk for submit@debbugs.gnu.org; Thu, 28 Mar 2024 15:21:02 -0400 Received: from magnesium.8pit.net ([45.76.88.171]:35282) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rpvJ3-0007zL-QU; Thu, 28 Mar 2024 15:21:00 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=kmjPTAzh 5tGvtj+vgxow9t787ukGifhJBvwBBxP93V4=; h=date:subject:cc:to:from; d=soeren-tempel.net; b=zsBKF5rvtoipfStWyhbiwCEz0eU8a9WlkFWvWWhq3nrorfq OD13PcU5PTPD4oPYRR9uki1Xl3duqkFN+MP1XLdUUTTCH0fzLfbOWm3XrgfowXPQh08Q1v YifkDi/jyzIlY0IxnPDHgol8LSWT5hL5czgMIOU1huZ+T+y7FkgAhY= Received: from localhost (dynamic-2a02-3102-49da-001b-e01a-5b4b-a2ca-2e2f.310.pool.telefonica.de [2a02:3102:49da:1b:e01a:5b4b:a2ca:2e2f]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 6c6d7a50 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Thu, 28 Mar 2024 20:20:54 +0100 (CET) From: soeren@soeren-tempel.net To: 68296@debbugs.gnu.org Subject: [PATCH v4 1/2] gnu: Add klee-uclibc. Date: Thu, 28 Mar 2024 20:20:18 +0100 Message-ID: X-Mailer: git-send-email 2.44.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 68296 Cc: julien@lepiller.eu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/check.scm (klee-uclibc): New variable. Signed-off-by: Sören Tempel --- Change since v3: Resolve merge conflict, update KLEE website. gnu/packages/check.scm | 62 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index 7fd28c3ac7..9beba88788 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -51,6 +51,7 @@ ;;; Copyright © 2024 Giacomo Leidi ;;; Copyright © 2024 Zheng Junjie <873216071@qq.com> ;;; Copyright © 2024 Navid Afkhami +;;; Copyright © 2024 Sören Tempel ;;; ;;; This file is part of GNU Guix. ;;; @@ -84,6 +85,7 @@ (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 ncurses) #:use-module (gnu packages perl) #:use-module (gnu packages pkg-config) #:use-module (gnu packages python) @@ -3705,3 +3707,63 @@ (define-public subunit command line filters to process a subunit stream and language bindings for Python, C, C++ and shell. Bindings are easy to write for other languages.") (license (list license:asl2.0 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.com/klee/klee-uclibc") + (commit commit))) + (file-name (git-file-name name version)) + (sha256 + (base32 "12fnr5mq80cxwvv09gi844mi31jgi8067swagxnlxlhxj4mi125j")))) + (build-system gnu-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (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 downloaded and + ;; shouldn't really be needed for symbolic execution either. + (add-after 'unpack 'patch-config + (lambda _ + (substitute* "klee-premade-configs/x86_64/config" + (("UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_DOWNLOAD_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_PREGENERATED_LOCALE_DATA=y") + "UCLIBC_PREGENERATED_LOCALE_DATA=n") + (("UCLIBC_HAS_LOCALE=y") + "UCLIBC_HAS_LOCALE=n") + (("UCLIBC_HAS_XLOCALE=y") + "UCLIBC_HAS_XLOCALE=n")))) + + ;; Upstream uses a custom non-GNU configure script written + ;; in Python, replace the default configure phase accordingly. + (replace 'configure + (lambda _ + (invoke "./configure" + "--make-llvm-lib" + "--enable-release"))) + + ;; Custom install phase to only install the libc.a file manually. + ;; This is the only file which is used/needed by KLEE itself. + (replace 'install + (lambda* (#:key outputs #:allow-other-keys) + (install-file "lib/libc.a" + (string-append (assoc-ref outputs "out") + "/lib"))))))) + (inputs (list clang-toolchain-13)) + ;; ncurses is only needed for the `make menuconfig` interface. + (native-inputs (list python ncurses)) + (synopsis "Variant of uClibc tailored to symbolic execution") + (description + "Modified version of uClibc for symbolic execution of +Unix userland software. This library can only be used in conjunction +with the @code{klee} package.") + (home-page "https://klee-se.org/") + (license license:lgpl2.1)))) base-commit: daab3da5042a5803ffa13ee759b3f8895dd92de4 From debbugs-submit-bounces@debbugs.gnu.org Thu Mar 28 15:21:06 2024 Received: (at 68296) by debbugs.gnu.org; 28 Mar 2024 19:21:06 +0000 Received: from localhost ([127.0.0.1]:41178 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rpvJB-00080T-J4 for submit@debbugs.gnu.org; Thu, 28 Mar 2024 15:21:06 -0400 Received: from magnesium.8pit.net ([45.76.88.171]:35282) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1rpvJ6-0007zL-Cx; Thu, 28 Mar 2024 15:21:01 -0400 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=lDJEY/6A /R/B2hU2deaRrysHaPiLkwJLkvnWLxmFJnw=; h=references:in-reply-to:date: subject:cc:to:from; d=soeren-tempel.net; b=vNsZk1PWa7pTolUgmy8wT8sQD4/ 7qj7ir5F1nOn5x8DU+2TNsLUQ8CSWjiNNxVd2IB9PxEO14WQEZTFIgPfzGE5B9LSOha+Zp ErqeX8J673tKn+3g14M3c+zEUcOjW/6zLkE0SEc799f8e3SMx4hw5uG7cQekOe42O62Uip ++l8= Received: from localhost (dynamic-2a02-3102-49da-001b-e01a-5b4b-a2ca-2e2f.310.pool.telefonica.de [2a02:3102:49da:1b:e01a:5b4b:a2ca:2e2f]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 66014ca0 (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES); Thu, 28 Mar 2024 20:20:58 +0100 (CET) From: soeren@soeren-tempel.net To: 68296@debbugs.gnu.org Subject: [PATCH v4 2/2] gnu: Add klee. Date: Thu, 28 Mar 2024 20:20:19 +0100 Message-ID: <375eabc4693b9416e53c58fead36e0b8d4dde25d.1711653619.git.soeren@soeren-tempel.net> X-Mailer: git-send-email 2.44.0 In-Reply-To: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 68296 Cc: julien@lepiller.eu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) From: Sören Tempel * gnu/packages/check.scm (klee): New variable. Signed-off-by: Sören Tempel --- Change since v3: Update KLEE website. gnu/packages/check.scm | 55 ++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) diff --git a/gnu/packages/check.scm b/gnu/packages/check.scm index 9beba88788..f936bb12c1 100644 --- a/gnu/packages/check.scm +++ b/gnu/packages/check.scm @@ -76,6 +76,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) @@ -85,6 +86,7 @@ (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) @@ -94,6 +96,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) @@ -3767,3 +3770,55 @@ (define-public klee-uclibc with the @code{klee} package.") (home-page "https://klee-se.org/") (license license:lgpl2.1)))) + +(define-public klee + (package + (name "klee") + (version "3.0") + (source + (origin + (method git-fetch) + (uri (git-reference + (url "https://github.com/klee/klee") + (commit (string-append "v" version)))) + (sha256 + (base32 "0dj20nazkcq84ryr87dihvjznapsbl1n21sa8dhhnb0wsad5d6fb")) + (file-name (git-file-name name version)))) + (build-system cmake-build-system) + ;; Only x86_64 is presently supported by KLEE upstream. + (supported-systems '("x86_64-linux")) + (arguments + `(#:test-target "systemtests" + ;; Default build type (RelWithDebInfo) causes an internal error + ;; in clang while compiling KLEE, hence use a different build type. + #:build-type "Release" + #:strip-directories '("bin") + #:configure-flags ,#~(list "-DENABLE_KLEE_ASSERTS=OFF" + "-DENABLE_TCMALLOC=ON" + "-DENABLE_POSIX_RUNTIME=ON" + (string-append "-DKLEE_UCLIBC_PATH=" + #$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. Otherwise, the test scripts won't be able to + ;; find the python-tabulate dependency, causing test failures. + (substitute* "test/lit.cfg" + (("addEnv\\('PWD'\\)" env) + (string-append env "\n" "addEnv('GUIX_PYTHONPATH')")))))))) + ;; KLEE operates on LLVM IR generated by a specific toolchain version. + ;; Propergate the toolchain to allow users to transform code to this version. + (propagated-inputs (list clang-toolchain-13 llvm-13 python python-tabulate)) + (inputs (list z3 gperftools sqlite)) + (native-inputs (list python-lit)) + (synopsis + "Symbolic execution engine built on top of the LLVM compiler infastructure") + (description + "Dynamic symbolic execution engine built on top of +LLVM. Symbolic execution is an automated software testing technique, +KLEE leverage this technique to automatically generate test cases for +software compiled to LLVM IR.") + (home-page "https://klee-se.org/") + (license (list license:expat license:bsd-4)))) From debbugs-submit-bounces@debbugs.gnu.org Sun Jun 23 09:47:22 2024 Received: (at 68296) by debbugs.gnu.org; 23 Jun 2024 13:47:22 +0000 Received: from localhost ([127.0.0.1]:59929 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sLNYw-00043p-3t for submit@debbugs.gnu.org; Sun, 23 Jun 2024 09:47:22 -0400 Received: from mail-wm1-f68.google.com ([209.85.128.68]:44391) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1sLNYt-00043E-4q; Sun, 23 Jun 2024 09:47:20 -0400 Received: by mail-wm1-f68.google.com with SMTP id 5b1f17b1804b1-4217a96de38so25680835e9.1; Sun, 23 Jun 2024 06:47:18 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20230601; t=1719150373; x=1719755173; darn=debbugs.gnu.org; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:from:to:cc:subject :date:message-id:reply-to; bh=SQ8raIDnK2xbh6Y2Gc9wnEUqyRugL+lkrlmTKlmluoA=; b=GXJCH1wJeC4tay9K4McYoryjnrGp/HmTjNXoHQfMXZJfPfkhrVbimlMvYNYk7BK2I3 amqQd9XgtoF7pnz7//Ps4PgapoiwvFXZ2nWRDKs0Ch2Lmcl956Crd9PMhzoeLdHFh3EW OaRjKMBRvC1Ybm4EaIrcWVx8at7AbZBhPlXO/CMkrObTlZ9VcqBx4UZ74HxkFAckzZ2S ru4OuCWg6QRHSsX49bggG25WI2tHfHncgjVPzJGQA78a/niPjN2yniHtOQSPp7ZNVLaV ibiGLFI09QpT7FZ/2CABQNEh1j2ipO8xqykvX4K9EWnF6rgP8MgK4etcWTGW7LthksQ6 yo0A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1719150373; x=1719755173; h=mime-version:user-agent:content-transfer-encoding:references :in-reply-to:date:cc:to:from:subject:message-id:x-gm-message-state :from:to:cc:subject:date:message-id:reply-to; bh=SQ8raIDnK2xbh6Y2Gc9wnEUqyRugL+lkrlmTKlmluoA=; b=rb25dFtp3qcYzAkVwJIYGFc9ObP1AzQeTXbQlr+ZW1qiGDwAloifqg+e5daFehK1LC FhUrNqWOMcx2FluDVriUQKvTKLDnHQA6duKoQHe7M8F38BML4vw0+5MN6Q8wHDnYUCRn Bsf117ZqLx46Tun5n1etm9zDXoMj2k+1FlPZAmx45f0xISDUViGXCkJAPP5a3BmKj1ah yRcPxCLdtT/QsPprJ9GzsKE0AYPZ6tJACbMzPrvsWugE3V55x82zNFJUMGCoXpQ8kq4k sNdKsrqT+PmrPoNB6stKvprGMCpjEGy2f1WZXNw9EBKSEUxO3YEWmfjzEivqqYyM/xN4 JbUw== X-Forwarded-Encrypted: i=1; AJvYcCWcTUvalf9ZH2N02AsO5fHPjpOIvcGdHMxqYoUsEj/m8+z2VhC2jVR6CmL7HrXqs8BTA9X+wGLqDgAtHle3LQo0r0OjXKjjgr7dtuLjplYQsco3kBMMsa1p8i7nCCprAfrW X-Gm-Message-State: AOJu0Yyscs1apec6gJy9tZ4Psd0fGgInqC9CyzjPfNuW7svJLR/0Hq6M w0QnHt07D1XKXHMFhDI+JsdfIFFfQZd4pQlnDFPiqWiuQPVF9V74aeVLT1q/ X-Google-Smtp-Source: AGHT+IEGQHi3pqSiG3CSLDAx5LICfs/HApoHl5lAYh8A6aWAYryzNJ1tfniVBufbyNyr871Vm5dlRw== X-Received: by 2002:adf:f512:0:b0:362:3526:4ebb with SMTP id ffacd0b85a97d-366e4ede448mr2154607f8f.37.1719150372648; Sun, 23 Jun 2024 06:46:12 -0700 (PDT) Received: from lumine.fritz.box (85-127-52-93.dsl.dynamic.surfer.at. [85.127.52.93]) by smtp.gmail.com with ESMTPSA id ffacd0b85a97d-366387cf523sm7368981f8f.25.2024.06.23.06.46.11 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Sun, 23 Jun 2024 06:46:12 -0700 (PDT) Message-ID: Subject: Re: [PATCH v4 2/2] gnu: Add klee. From: Liliana Marie Prikler To: soeren@soeren-tempel.net, 68296@debbugs.gnu.org Date: Sun, 23 Jun 2024 15:46:11 +0200 In-Reply-To: <375eabc4693b9416e53c58fead36e0b8d4dde25d.1711653619.git.soeren@soeren-tempel.net> References: <375eabc4693b9416e53c58fead36e0b8d4dde25d.1711653619.git.soeren@soeren-tempel.net> Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable User-Agent: Evolution 3.48.4 MIME-Version: 1.0 X-Spam-Score: -0.0 (/) X-Debbugs-Envelope-To: 68296 Cc: julien@lepiller.eu X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hi S=C3=B6ren, hi Julien Am Donnerstag, dem 28.03.2024 um 20:20 +0100 schrieb soeren@soeren-tempel.net: > From: S=C3=B6ren Tempel >=20 > * gnu/packages/check.scm (klee): New variable. I pushed 71634 earlier today, which adds klee, but not klee-uclibc =E2=80= =93 would you mind taking a look at it and adding any missing bits? Cheers From debbugs-submit-bounces@debbugs.gnu.org Mon Jan 13 12:52:21 2025 Received: (at 68296-done) by debbugs.gnu.org; 13 Jan 2025 17:52:21 +0000 Received: from localhost ([127.0.0.1]:52763 helo=debbugs.gnu.org) by debbugs.gnu.org with esmtp (Exim 4.84_2) (envelope-from ) id 1tXObt-0002Nb-ID for submit@debbugs.gnu.org; Mon, 13 Jan 2025 12:52:21 -0500 Received: from magnesium.8pit.net ([2001:19f0:6c01:4ae:5400:ff:fe66:af9d]:3042) by debbugs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.84_2) (envelope-from ) id 1tXObq-0002NO-UY for 68296-done@debbugs.gnu.org; Mon, 13 Jan 2025 12:52:19 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; s=opensmtpd; bh=OrLSrYP9 poECmioPq+5Cax+uLoX2L1StFC0GDndlyNY=; h=from:subject:to:date; d=soeren-tempel.net; b=JURurOMPYvJxcAmtlAbfspLiZvkM+c/a+Fw5b9mlgYD1F8Z DlgqAGsfWz7StgJDzQIf5Ow5A5xURrPvJP0aIA+seqttYhvKoWIahoUivzznj39MT5hn0n bQv0MPgZzcQVzVR3v7sm7L1dekXh5VA2hjyAs8wlrFyXnfblghlYng= Received: from localhost ( [2a02:560:4d3d:df00:4fe7:d7be:f3b3:38d3]) by magnesium.8pit.net (OpenSMTPD) with ESMTPSA id 13a7965a (TLSv1.3:TLS_AES_256_GCM_SHA384:256:YES) for <68296-done@debbugs.gnu.org>; Mon, 13 Jan 2025 18:52:13 +0100 (CET) Date: Mon, 13 Jan 2025 18:52:06 +0100 To: 68296-done@debbugs.gnu.org Subject: Re: [PATCH] gnu: Add KLEE. From: =?UTF-8?Q?S=C3=B6ren?= Tempel Message-Id: <2C8JOOUL2GHJR.32GXTU4IR3YKE@8pit.net> MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Spam-Score: 0.0 (/) X-Debbugs-Envelope-To: 68296-done X-BeenThere: debbugs-submit@debbugs.gnu.org X-Mailman-Version: 2.1.18 Precedence: list List-Id: List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: debbugs-submit-bounces@debbugs.gnu.org Sender: "Debbugs-submit" X-Spam-Score: -1.0 (-) Hi, klee has been added in fe7c898750e3fdad586ab3929c67b4b4643ffece, klee-uclibc has been added as well in a follow-up commit, namely 3bdaa223b363b6986baa4bfa11f629f6ba974bba. Hence, this can be closed. From unknown Sat Sep 20 18:58:07 2025 Received: (at fakecontrol) by fakecontrolmessage; To: internal_control@debbugs.gnu.org From: Debbugs Internal Request Subject: Internal Control Message-Id: bug archived. Date: Tue, 11 Feb 2025 12:24:11 +0000 User-Agent: Fakemail v42.6.9 # This is a fake control message. # # The action: # bug archived. thanks # This fakemail brought to you by your local debbugs # administrator