diff mbox series

[v5,01/11] kconfig: Add PicoSAT interface

Message ID 20240920085628.51863-2-ole0811sch@gmail.com (mailing list archive)
State New
Headers show
Series kbuild, kconfig: Add support for conflict resolution | expand

Commit Message

Ole Schuerks Sept. 20, 2024, 8:56 a.m. UTC 
PicoSAT (https://fmv.jku.at/picosat/) is the SAT solver used in this
project. It is used as a dynamically loaded library. This commit contains a
script that installs PicoSAT as a library on the host system, a source file
that provides a function for loading a subset of functions from the
library, and a header file that declares these functions.

Signed-off-by: Patrick Franz <deltaone@debian.org>
Signed-off-by: Ibrahim Fayaz <phayax@gmail.com>
Signed-off-by: Thorsten Berger <thorsten.berger@rub.de>
Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
---
 scripts/kconfig/install-picosat.sh  | 29 +++++++++++
 scripts/kconfig/picosat_functions.c | 74 +++++++++++++++++++++++++++++
 scripts/kconfig/picosat_functions.h | 35 ++++++++++++++
 3 files changed, 138 insertions(+)
 create mode 100755 scripts/kconfig/install-picosat.sh
 create mode 100644 scripts/kconfig/picosat_functions.c
 create mode 100644 scripts/kconfig/picosat_functions.h

Comments

Luis Chamberlain Sept. 20, 2024, 11:11 a.m. UTC | #1 
On Fri, Sep 20, 2024 at 10:56:18AM +0200, Ole Schuerks wrote:
> diff --git a/scripts/kconfig/install-picosat.sh b/scripts/kconfig/install-picosat.sh
> new file mode 100755
> index 000000000000..aadfa9582ecb
> --- /dev/null
> +++ b/scripts/kconfig/install-picosat.sh
> @@ -0,0 +1,29 @@
> +#!/bin/bash
> +# SPDX-License-Identifier: GPL-2.0
> +
> +psinstdir=$(mktemp -d)
> +if [ $? -ne 0 ]; then
> +	echo "mktemp failed"
> +	exit 1
> +fi
> +cd $psinstdir
> +wget "https://fmv.jku.at/picosat/picosat-965.tar.gz"
> +tar -xf picosat-965.tar.gz
> +cd picosat-965
> +cp makefile.in makefile.in2
> +# change soname to conform with packages for Debian and Fedora
> +sed -e "s,-soname -Xlinker libpicosat.so,-soname -Xlinker	\
> +	libpicosat-trace.so.0," makefile.in2 > makefile.in
> +./configure.sh -O -t --shared
> +make libpicosat.so

Imagine if the kernel did the same thing for all the libraries we use,
so this is just not scalable. Instead it would be better for you to
intent to package this onto something like debian as a library for
picosat, once and accepted then your tooling would just detect if its
present and if so use it.

  Luis
diff mbox series

Patch

diff --git a/scripts/kconfig/install-picosat.sh b/scripts/kconfig/install-picosat.sh
new file mode 100755
index 000000000000..aadfa9582ecb
--- /dev/null
+++ b/scripts/kconfig/install-picosat.sh
@@ -0,0 +1,29 @@ 
+#!/bin/bash
+# SPDX-License-Identifier: GPL-2.0
+
+psinstdir=$(mktemp -d)
+if [ $? -ne 0 ]; then
+	echo "mktemp failed"
+	exit 1
+fi
+cd $psinstdir
+wget "https://fmv.jku.at/picosat/picosat-965.tar.gz"
+tar -xf picosat-965.tar.gz
+cd picosat-965
+cp makefile.in makefile.in2
+# change soname to conform with packages for Debian and Fedora
+sed -e "s,-soname -Xlinker libpicosat.so,-soname -Xlinker	\
+	libpicosat-trace.so.0," makefile.in2 > makefile.in
+./configure.sh -O -t --shared
+make libpicosat.so
+install -m 0755 -p libpicosat.so /usr/local/lib/libpicosat-trace.so.0.0.965	\
+&& ln -s -f libpicosat-trace.so.0.0.965 /usr/local/lib/libpicosat-trace.so.0	\
+&& ln -s -f libpicosat-trace.so.0 /usr/local/lib/libpicosat-trace.so \
+&& ldconfig
+echo
+if [ $? -ne 0 ]; then
+	echo "Installation of PicoSAT failed, make sure you are running with root privileges."
+	exit 1
+else
+	echo "Installation of PicoSAT succeeded."
+fi
diff --git a/scripts/kconfig/picosat_functions.c b/scripts/kconfig/picosat_functions.c
new file mode 100644
index 000000000000..ada42abbc22b
--- /dev/null
+++ b/scripts/kconfig/picosat_functions.c
@@ -0,0 +1,74 @@ 
+// SPDX-License-Identifier: GPL-2.0
+
+#include <dlfcn.h>
+#include <unistd.h>
+
+#include "array_size.h"
+
+#include "cf_defs.h"
+#include "picosat_functions.h"
+
+const char *picosat_lib_names[] = { "libpicosat-trace.so",
+				    "libpicosat-trace.so.0",
+				    "libpicosat-trace.so.1" };
+
+PicoSAT *(*picosat_init)(void);
+int (*picosat_add)(PicoSAT *pico, int lit);
+int (*picosat_deref)(PicoSAT *pico, int lit);
+void (*picosat_assume)(PicoSAT *pico, int lit);
+int (*picosat_sat)(PicoSAT *pico, int decision_limit);
+const int *(*picosat_failed_assumptions)(PicoSAT *pico);
+int (*picosat_added_original_clauses)(PicoSAT *pico);
+int (*picosat_enable_trace_generation)(PicoSAT *pico);
+void (*picosat_print)(PicoSAT *pico, FILE *file);
+
+#define PICOSAT_FUNCTION_LIST             \
+	X(picosat_init)                   \
+	X(picosat_add)                    \
+	X(picosat_deref)                  \
+	X(picosat_assume)                 \
+	X(picosat_sat)                    \
+	X(picosat_failed_assumptions)     \
+	X(picosat_added_original_clauses) \
+	X(picosat_enable_trace_generation)\
+	X(picosat_print)
+
+static void load_function(const char *name, void **ptr, void *handle, bool *failed)
+{
+	if (*failed)
+		return;
+
+	*ptr = dlsym(handle, name);
+	if (!*ptr) {
+		printd("While loading %s: %s\n", name, dlerror());
+		*failed = true;
+	}
+}
+
+bool load_picosat(void)
+{
+	void *handle = NULL;
+	bool failed = false;
+
+	/*
+	 * Try different names for the .so library. This is necessary since
+	 * all packages don't use the same versioning.
+	 */
+	for (int i = 0; i < ARRAY_SIZE(picosat_lib_names) && !handle; ++i)
+		handle = dlopen(picosat_lib_names[i], RTLD_LAZY);
+	if (!handle) {
+		printd("%s\n", dlerror());
+		return false;
+	}
+
+#define X(name) load_function(#name, (void **) &name, handle, &failed);
+
+	PICOSAT_FUNCTION_LIST
+#undef X
+
+	if (failed) {
+		dlclose(handle);
+		return false;
+	} else
+		return true;
+}
diff --git a/scripts/kconfig/picosat_functions.h b/scripts/kconfig/picosat_functions.h
new file mode 100644
index 000000000000..5d8524afa844
--- /dev/null
+++ b/scripts/kconfig/picosat_functions.h
@@ -0,0 +1,35 @@ 
+/* SPDX-License-Identifier: GPL-2.0 */
+
+#ifndef PICOSAT_FUNCTIONS_H
+#define PICOSAT_FUNCTIONS_H
+
+#include <stdbool.h>
+#include <stdio.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#define PICOSAT_UNKNOWN         0
+#define PICOSAT_SATISFIABLE     10
+#define PICOSAT_UNSATISFIABLE   20
+
+typedef struct PicoSAT PicoSAT;
+
+extern PicoSAT *(*picosat_init)(void);
+extern int (*picosat_add)(PicoSAT *pico, int lit);
+extern int (*picosat_deref)(PicoSAT *pico, int lit);
+extern void (*picosat_assume)(PicoSAT *pico, int lit);
+extern int (*picosat_sat)(PicoSAT *pico, int decision_limit);
+extern const int *(*picosat_failed_assumptions)(PicoSAT *pico);
+extern int (*picosat_added_original_clauses)(PicoSAT *pico);
+extern int (*picosat_enable_trace_generation)(PicoSAT *pico);
+extern void (*picosat_print)(PicoSAT *pico, FILE *file);
+
+bool load_picosat(void);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // PICOSAT_FUNCTIONS_H