Skip to content

cbmc: Switch to tautschnig/cbmc fix-8813-union-performance branch #1016

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
mkannwischer wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

cbmc: Switch to tautschnig/cbmc fix-8813-union-performance branch #1016

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion mldsa/mldsa_native.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -252,7 +252,6 @@
#undef MLD_NAMESPACE_KL
#undef MLD_NAMESPACE_PREFIX
#undef MLD_NAMESPACE_PREFIX_KL
#undef MLD_UNION_OR_STRUCT
#undef mld_memcpy
#undef mld_memset
/* mldsa/src/packing.h */
Expand Down
18 changes: 9 additions & 9 deletions mldsa/mldsa_native.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -913,20 +913,20 @@ int MLD_API_NAMESPACE(pk_from_sk)(
/* check-magic: off */
#if defined(MLD_API_LEGACY_CONFIG) || !defined(MLD_CONFIG_REDUCE_RAM)
#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 41216
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 56640
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 48448
#define MLD_TOTAL_ALLOC_44_PK_FROM_SK 45248
#define MLD_TOTAL_ALLOC_44_SIGN 52896
#define MLD_TOTAL_ALLOC_44_VERIFY 38816
#define MLD_TOTAL_ALLOC_44_SIGN 44704
#define MLD_TOTAL_ALLOC_44_VERIFY 34720
#define MLD_TOTAL_ALLOC_65_KEYPAIR_NO_PCT 65792
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 85856
#define MLD_TOTAL_ALLOC_65_KEYPAIR_PCT 75616
#define MLD_TOTAL_ALLOC_65_PK_FROM_SK 71872
#define MLD_TOTAL_ALLOC_65_SIGN 80576
#define MLD_TOTAL_ALLOC_65_VERIFY 62432
#define MLD_TOTAL_ALLOC_65_SIGN 70336
#define MLD_TOTAL_ALLOC_65_VERIFY 56288
#define MLD_TOTAL_ALLOC_87_KEYPAIR_NO_PCT 104704
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 130816
#define MLD_TOTAL_ALLOC_87_KEYPAIR_PCT 116480
#define MLD_TOTAL_ALLOC_87_PK_FROM_SK 112832
#define MLD_TOTAL_ALLOC_87_SIGN 123584
#define MLD_TOTAL_ALLOC_87_VERIFY 99552
#define MLD_TOTAL_ALLOC_87_SIGN 109248
#define MLD_TOTAL_ALLOC_87_VERIFY 91360
#else /* MLD_API_LEGACY_CONFIG || !MLD_CONFIG_REDUCE_RAM */
#define MLD_TOTAL_ALLOC_44_KEYPAIR_NO_PCT 28960
#define MLD_TOTAL_ALLOC_44_KEYPAIR_PCT 28960
Expand Down
1 change: 0 additions & 1 deletion mldsa/mldsa_native_asm.S
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -255,7 +255,6 @@
#undef MLD_NAMESPACE_KL
#undef MLD_NAMESPACE_PREFIX
#undef MLD_NAMESPACE_PREFIX_KL
#undef MLD_UNION_OR_STRUCT
#undef mld_memcpy
#undef mld_memset
/* mldsa/src/packing.h */
Expand Down
13 changes: 0 additions & 13 deletions mldsa/src/common.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -290,19 +290,6 @@

#endif /* MLD_CONFIG_CUSTOM_ALLOC_FREE */

/*
* We are facing severe CBMC performance issues when using unions.
* As a temporary workaround, we use unions only when MLD_CONFIG_REDUCE_RAM is
* set.
* TODO: Remove the workaround once
* https://github.com/diffblue/cbmc/issues/8813
* is resolved
*/
#if defined(MLD_CONFIG_REDUCE_RAM)
#define MLD_UNION_OR_STRUCT union
#else
#define MLD_UNION_OR_STRUCT struct
#endif

/****************************** Error codes ***********************************/

Expand Down
21 changes: 6 additions & 15 deletions mldsa/src/sign.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -681,25 +681,19 @@ __contract__(
unsigned int n;
uint32_t w0_invalid, h_invalid;
int ret;
/* TODO: Remove the following workaround for
* https://github.com/diffblue/cbmc/issues/8813 */
typedef MLD_UNION_OR_STRUCT
typedef union
{
mld_polyvecl y;
mld_polyveck h;
}
yh_u;
} yh_u;
mld_polyvecl *y;
mld_polyveck *h;

/* TODO: Remove the following workaround for
* https://github.com/diffblue/cbmc/issues/8813 */
typedef MLD_UNION_OR_STRUCT
typedef union
{
mld_polyveck w1;
mld_polyvecl tmp;
}
w1tmp_u;
} w1tmp_u;
mld_polyveck *w1;
mld_polyvecl *tmp;

Expand Down Expand Up @@ -1078,14 +1072,11 @@ int mld_sign_verify_internal(const uint8_t *sig, size_t siglen,
{
int ret, cmp;

/* TODO: Remove the following workaround for
* https://github.com/diffblue/cbmc/issues/8813 */
typedef MLD_UNION_OR_STRUCT
typedef union
{
mld_polyveck t1;
mld_polyveck w1;
}
t1w1_u;
} t1w1_u;
mld_polyveck *t1;
mld_polyveck *w1;

Expand Down
53 changes: 53 additions & 0 deletions nix/cbmc/0002-Do-not-download-sources-in-cmake.patch
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,53 @@
# SPDX-License-Identifier: Apache-2.0 OR ISC OR MIT
From c6b6438d3c87ce000b4e80b2eda2389e9473d24c Mon Sep 17 00:00:00 2001
From: wxt <3264117476@qq.com>
Date: Mon, 11 Nov 2024 11:35:03 +0800
Subject: [PATCH] Do not download sources in cmake

---
src/solvers/CMakeLists.txt | 9 +++------
1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt
index ab8d111..d7165e2 100644
--- a/src/solvers/CMakeLists.txt
+++ b/src/solvers/CMakeLists.txt
@@ -102,10 +102,9 @@ foreach(SOLVER ${sat_impl})
message(STATUS "Building solvers with glucose")

download_project(PROJ glucose
- URL https://github.com/BrunoDutertre/glucose-syrup/archive/0bb2afd3b9baace6981cbb8b4a1c7683c44968b7.tar.gz
+ SOURCE_DIR @srcglucose@
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/glucose-syrup-patch
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/glucose_CMakeLists.txt CMakeLists.txt
- URL_MD5 7c539c62c248b74210aef7414787323a
)

add_subdirectory(${glucose_SOURCE_DIR} ${glucose_BINARY_DIR})
@@ -121,11 +120,10 @@ foreach(SOLVER ${sat_impl})
message(STATUS "Building solvers with cadical")

download_project(PROJ cadical
- URL https://github.com/arminbiere/cadical/archive/rel-3.0.0.tar.gz
+ SOURCE_DIR @srccadical@
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-3.0.0-patch
COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
COMMAND ./configure
- URL_HASH SHA256=282b1c9422fde8631cb721b86450ae94df4e8de0545c17a69a301aaa4bf92fcf
)

add_subdirectory(${cadical_SOURCE_DIR} ${cadical_BINARY_DIR})
@@ -144,10 +142,9 @@ foreach(SOLVER ${sat_impl})
message(STATUS "Building with IPASIR solver linking against: CaDiCaL")

download_project(PROJ cadical
- URL https://github.com/arminbiere/cadical/archive/rel-3.0.0.tar.gz
+ SOURCE_DIR @srccadical@
PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-3.0.0-patch
COMMAND ./configure
- URL_HASH SHA256=282b1c9422fde8631cb721b86450ae94df4e8de0545c17a69a301aaa4bf92fcf
)

message(STATUS "Building CaDiCaL")
--
2.47.0
16 changes: 12 additions & 4 deletions nix/cbmc/default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,18 @@ buildEnv {
cbmc = cbmc.overrideAttrs (old: rec {
version = "6.8.0";
src = fetchFromGitHub {
owner = "diffblue";
owner = "tautschnig";
repo = "cbmc";
hash = "sha256-PT6AYiwkplCeyMREZnGZA0BKl4ZESRC02/9ibKg7mYU=";
tag = "cbmc-6.8.0";
hash = "sha256-8ou+8ucabQy+IAfW/WeCU7Zv4u1uZknrMwtecY9UDcs=";
rev = "f2244fd6ea6068ba0493280942538bad9c0f2367";
};
srccadical = cadical.src; # 3.0.0 from nixpkgs-unstable
patches = [
(builtins.elemAt old.patches 0) # cudd patch from nixpkgs
./0002-Do-not-download-sources-in-cmake.patch # cadical 3.0.0
];
env = old.env // {
NIX_CFLAGS_COMPILE = (old.env.NIX_CFLAGS_COMPILE or "") + " -Wno-error=switch-enum";
};
});
litani = callPackage ./litani.nix { }; # 1.29.0
Expand All @@ -40,7 +48,7 @@ buildEnv {
});

inherit
cadical# 2.2.0
cadical# 3.0.0
bitwuzla# 0.8.2
ninja; # 1.13.2
};
Expand Down
Loading