From 0e9db7a4d17d9679de1fa763a1a002ba216b4eea Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Mon, 11 Sep 2023 11:14:11 +0200 Subject: [PATCH 1/4] safe configuration --- NEWS.md | 5 +++++ VERSION | 2 +- configure | 15 ++++++++++++--- src/file.c | 6 +++++- 4 files changed, 23 insertions(+), 5 deletions(-) diff --git a/NEWS.md b/NEWS.md index bf1f86cf..5f25b8d3 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,3 +1,8 @@ +Version 3.1.1 +------------- + + - configuration option `--safe` disables writing through `popen` + Version 3.1.0 ------------- diff --git a/VERSION b/VERSION index fd2a0186..94ff29cc 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -3.1.0 +3.1.1 diff --git a/configure b/configure index dd62570b..15ce4903 100755 --- a/configure +++ b/configure @@ -25,6 +25,7 @@ pic=no profile=no proofs=yes quiet=no +safe=no sat=no shared=no static=no @@ -77,13 +78,18 @@ fi cat << EOF Options used to instrument the code for coverage and performance profiling. - --coverage include line coverage code (to be used with 'gcov') - --profile include profiling code (to be used with 'gprof') + --coverage include line coverage code (to be used with 'gcov') + --profile include profiling code (to be used with 'gprof') For coverage testing it might be useful to enforce different compiler optimization levels, i.e., lower than the default '-O3' (without '-g'). - -O[0|1|2|3] set the optimization level of the compiler explicitly + -O[0|1|2|3] set the optimization level of the compiler explicitly + +Writing through 'popen' can be considered harmful in certain library usage. + + --safe disable the use of writing through 'popen' + (and thus disables writing zipped files too) We have compile time options which save memory and speed up the solver by limiting the size of formulas that can be handled, fix the default @@ -216,6 +222,8 @@ do -O2) optimize=2;; -O3) optimize=3;; + --safe) safe=yes;; + --compact) compact=yes;; --no-options) options=no;; --quiet) quiet=yes;; @@ -595,6 +603,7 @@ fi [ $options = no ] && CFLAGS="$CFLAGS -DNOPTIONS" [ $proofs = no ] && CFLAGS="$CFLAGS -DNPROOFS" [ $quiet = yes ] && CFLAGS="$CFLAGS -DQUIET" +[ $safe = yes ] && CFLAGS="$CFLAGS -DSAFE" [ $sat = yes ] && CFLAGS="$CFLAGS -DSAT" [ $statistics = yes -a $metrics = no ] && CFLAGS="$CFLAGS -DSTATISTICS" [ $unsat = yes ] && CFLAGS="$CFLAGS -DUNSAT" diff --git a/src/file.c b/src/file.c index dafb170d..1d805054 100644 --- a/src/file.c +++ b/src/file.c @@ -174,12 +174,16 @@ static FILE *read_pipe (const char *fmt, const int *sig, const char *path) { return open_pipe (fmt, path, "r"); } +#ifndef SAFE + static FILE *write_pipe (const char *fmt, const char *path) { return open_pipe (fmt, path, "w"); } #endif +#endif + void kissat_read_already_open_file (file *file, FILE *f, const char *path) { file->file = f; file->close = false; @@ -253,7 +257,7 @@ bool kissat_open_to_read_file (file *file, const char *path) { } bool kissat_open_to_write_file (file *file, const char *path) { -#ifdef KISSAT_HAS_COMPRESSION +#if defined(KISSAT_HAS_COMPRESSION) && !defined(SAFE) #define WRITE_PIPE(SUFFIX, CMD) \ do { \ if (kissat_has_suffix (path, SUFFIX)) { \ From 547c3c66eb25166500da77b173335cb2e5237722 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Mon, 11 Sep 2023 11:21:38 +0200 Subject: [PATCH 2/4] added clang-format --- .clang-format | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 .clang-format diff --git a/.clang-format b/.clang-format new file mode 100644 index 00000000..300836e6 --- /dev/null +++ b/.clang-format @@ -0,0 +1,4 @@ +AlignEscapedNewlines: DontAlign +ColumnLimit: 76 +SpaceBeforeParens: Always +SpaceAfterCStyleCast: true From 0b4848dc1af2772bd87dbba572b956477b34107a Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Mon, 11 Sep 2023 11:26:00 +0200 Subject: [PATCH 3/4] removed stale endianess.h file --- src/endianness.h | 8 -------- 1 file changed, 8 deletions(-) delete mode 100644 src/endianness.h diff --git a/src/endianness.h b/src/endianness.h deleted file mode 100644 index 2877a356..00000000 --- a/src/endianness.h +++ /dev/null @@ -1,8 +0,0 @@ -#ifndef _endianness_h_INCLUDED -#define _endianness_h_INCLUDED - -#if __BYTE_ORDER__ == __ORDER_BIG_ENDIAN__ -#define KISSAT_IS_BIG_ENDIAN -#endif - -#endif From 71caafb4d182ced9f76cef45b00f37cc598f2a37 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Mon, 11 Sep 2023 11:32:48 +0200 Subject: [PATCH 4/4] removing src makefile link --- configure | 1 + 1 file changed, 1 insertion(+) diff --git a/configure b/configure index 15ce4903..7f26dbc1 100755 --- a/configure +++ b/configure @@ -329,6 +329,7 @@ tissat: \$(MAKE) -C "$BUILD" tissat clean: rm -f "$ROOT"/makefile + rm -f "$ROOT"/src/makefile -\$(MAKE) -C "$BUILD" clean rm -rf "$BUILD" coverage: