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/picosat_functions.c | 74 +++++++++++++++++++++++++++++
 scripts/kconfig/picosat_functions.h | 35 ++++++++++++++
 2 files changed, 109 insertions(+)
 create mode 100644 scripts/kconfig/picosat_functions.c
 create mode 100644 scripts/kconfig/picosat_functions.h

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
-- 
2.39.5

On Mon, Oct 28, 2024 at 04:49:39AM +0100, Ole Schuerks wrote:
> PicoSAT (https://fmv.jku.at/picosat/) is the SAT solver used in this

PicoSAT [0] ... etc etc..

Then at the bottom you use the tag:

Link: https://fmv.jku.at/picosat/ # [0]

> project. It is used as a dynamically loaded library. 

OK

> This commit contains a

Obviously this commit exits... be more imperative...

> 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.

Just say something like:

Add PicoSAT dynamic library support to kconfig. Support for this will be
used subsequent patches.

> +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) {

This just deals with the first error and there is no unwinding, is that OK?

Other than that, did you run this through checkpatch.pl?

 Luis

Thanks for all the feedback.

> This just deals with the first error and there is no unwinding, is that OK?

This should be OK. dlsym() only retrieves the address of a symbol from an
already loaded object. The calls to dlsym() thus should not need to be
unwound, it's sufficient to unload the object via dlclose().

> Other than that, did you run this through checkpatch.pl?

I ran all patches through checkpath.pl. The only reported issues with this
patch are the ones related to the use of the X-macro and one about the
typedef for the PicoSAT type. Is the use of X-macros discouraged?
Refactoring it wouldn't be a problem. (I think it makes most sense to keep
the typedef, though, in order to keep the declarations compatible with
those from the original header file.)

Best regards,
Ole Schuerks

On Mon, Dec 09, 2024 at 01:57:13AM +0100, Ole Schuerks wrote:
> Thanks for all the feedback.
> 
> > This just deals with the first error and there is no unwinding, is that OK?
> 
> This should be OK. dlsym() only retrieves the address of a symbol from an
> already loaded object. The calls to dlsym() thus should not need to be
> unwound, it's sufficient to unload the object via dlclose().

OK thanks, maybe add a comment about it.

> > Other than that, did you run this through checkpatch.pl?
> 
> I ran all patches through checkpath.pl. The only reported issues with this
> patch are the ones related to the use of the X-macro and one about the
> typedef for the PicoSAT type. 

I don't know what x-macro is so I don't have any clear opinion on that.

  Luis