[PATCH v4 10/12] kconfig: Add tools

[Ole Schuerks]

This commit contains the actual API to be used from a configurator.
Furthermore, it contains a tool to print all constraints into a file.

Co-developed-by: Patrick Franz <deltaone@xxxxxxxxxx>
Signed-off-by: Patrick Franz <deltaone@xxxxxxxxxx>
Co-developed-by: Ibrahim Fayaz <phayax@xxxxxxxxx>
Signed-off-by: Ibrahim Fayaz <phayax@xxxxxxxxx>
Reviewed-by: Luis Chamberlain <mcgrof@xxxxxxxxxx>
Tested-by: Evgeny Groshev <eugene.groshev@xxxxxxxxx>
Suggested-by: Sarah Nadi <nadi@xxxxxxxxxxx>
Suggested-by: Thorsten Berger <thorsten.berger@xxxxxx>
Signed-off-by: Thorsten Berger <thorsten.berger@xxxxxx>
Signed-off-by: Ole Schuerks <ole0811sch@xxxxxxxxx>
---
 scripts/kconfig/.gitignore    |   1 +
 scripts/kconfig/cfoutconfig.c | 142 ++++++++++++++
 scripts/kconfig/configfix.c   | 337 ++++++++++++++++++++++++++++++++++
 scripts/kconfig/configfix.h   |  40 ++++
 4 files changed, 520 insertions(+)
 create mode 100644 scripts/kconfig/cfoutconfig.c
 create mode 100644 scripts/kconfig/configfix.c
 create mode 100644 scripts/kconfig/configfix.h

diff --git a/scripts/kconfig/.gitignore b/scripts/kconfig/.gitignore
index 0b2ff775b2e3..23446f70083e 100644
--- a/scripts/kconfig/.gitignore
+++ b/scripts/kconfig/.gitignore
@@ -5,3 +5,4 @@
 /[gmnq]conf-cflags
 /[gmnq]conf-libs
 /qconf-moc.cc
+/cfoutconfig
diff --git a/scripts/kconfig/cfoutconfig.c b/scripts/kconfig/cfoutconfig.c
new file mode 100644
index 000000000000..c0879e6ebaa1
--- /dev/null
+++ b/scripts/kconfig/cfoutconfig.c
@@ -0,0 +1,142 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@xxxxxxxxxx>
+ */
+
+#define _GNU_SOURCE
+#include <assert.h>
+#include <locale.h>
+#include <stdarg.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+#include <unistd.h>
+
+#include "configfix.h"
+#include "internal.h"
+
+#define OUTFILE_CONSTRAINTS "./scripts/kconfig/cfout_constraints.txt"
+#define OUTFILE_DIMACS "./scripts/kconfig/cfout_constraints.dimacs"
+
+static void write_constraints_to_file(struct cfdata *data);
+static void write_dimacs_to_file(PicoSAT *pico, struct cfdata *data);
+
+/* -------------------------------------- */
+
+int main(int argc, char *argv[])
+{
+	clock_t start, end;
+	double time;
+	PicoSAT *pico;
+
+	static struct constants constants = {NULL, NULL, NULL, NULL, NULL};
+	static struct cfdata data = {
+		1,    // unsigned int sat_variable_nr
+		1,    // unsigned int tmp_variable_nr
+		NULL, // struct fexpr *satmap
+		0,    // size_t satmap_size
+		&constants // struct constants *constants
+	};
+
+	printf("\nCreating constraints and CNF clauses...");
+	/* measure time for constructing constraints and clauses */
+	start = clock();
+
+	/* parse Kconfig-file and read .config */
+	init_config(argv[1]);
+
+	/* initialize satmap and cnf_clauses */
+	init_data(&data);
+
+	/* creating constants */
+	create_constants(&data);
+
+	/* assign SAT variables & create sat_map */
+	create_sat_variables(&data);
+
+	/* get the constraints */
+	get_constraints(&data);
+
+	end = clock();
+	time = ((double) (end - start)) / CLOCKS_PER_SEC;
+
+	printd("done. (%.6f secs.)\n", time);
+
+	/* start PicoSAT */
+	pico = picosat_init();
+	picosat_enable_trace_generation(pico);
+	printd("Building CNF-clauses...");
+	start = clock();
+
+	/* construct the CNF clauses */
+	construct_cnf_clauses(pico, &data);
+
+	end = clock();
+	time = ((double) (end - start)) / CLOCKS_PER_SEC;
+	printf("done. (%.6f secs.)\n", time);
+
+	printf("\n");
+
+	/* write constraints into file */
+	start = clock();
+	printf("Writing constraints...");
+	write_constraints_to_file(&data);
+	end = clock();
+	time = ((double) (end - start)) / CLOCKS_PER_SEC;
+	printf("done. (%.6f secs.)\n", time);
+
+	/* write SAT problem in DIMACS into file */
+	start = clock();
+	printf("Writing SAT problem in DIMACS...");
+	write_dimacs_to_file(pico, &data);
+	end = clock();
+	time = ((double) (end - start)) / CLOCKS_PER_SEC;
+	printf("done. (%.6f secs.)\n", time);
+
+	printf("\nConstraints have been written into %s\n", OUTFILE_CONSTRAINTS);
+	printf("DIMACS-output has been written into %s\n", OUTFILE_DIMACS);
+
+	return 0;
+}
+
+static void write_constraints_to_file(struct cfdata *data)
+{
+	FILE *fd = fopen(OUTFILE_CONSTRAINTS, "w");
+	struct symbol *sym;
+
+	for_all_symbols(sym) {
+		struct pexpr_node *node;
+
+		if (sym->type == S_UNKNOWN)
+			continue;
+
+		pexpr_list_for_each(node, sym->constraints) {
+			struct gstr s = str_new();
+
+			pexpr_as_char(node->elem, &s, 0, data);
+			fprintf(fd, "%s\n", str_get(&s));
+			str_free(&s);
+		}
+	}
+	fclose(fd);
+}
+
+static void add_comment(FILE *fd, struct fexpr *e)
+{
+	fprintf(fd, "c %d %s\n", e->satval, str_get(&e->name));
+}
+
+static void write_dimacs_to_file(PicoSAT *pico, struct cfdata *data)
+{
+	FILE *fd = fopen(OUTFILE_DIMACS, "w");
+
+	unsigned int i;
+
+	for (i = 1; i < data->sat_variable_nr; i++)
+		add_comment(fd, data->satmap[i]);
+
+	picosat_print(pico, fd);
+	fclose(fd);
+}
diff --git a/scripts/kconfig/configfix.c b/scripts/kconfig/configfix.c
new file mode 100644
index 000000000000..e161424149c4
--- /dev/null
+++ b/scripts/kconfig/configfix.c
@@ -0,0 +1,337 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@xxxxxxxxxx>
+ */
+
+#define _GNU_SOURCE
+#include <assert.h>
+#include <locale.h>
+#include <stdarg.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+#include <unistd.h>
+
+#include "configfix.h"
+#include "internal.h"
+#include "cf_expr.h"
+
+bool CFDEBUG;
+bool stop_rangefix;
+
+static PicoSAT *pico;
+static bool init_done;
+static struct sym_list *conflict_syms;
+
+static bool sdv_within_range(struct sdv_list *symbols);
+
+/* -------------------------------------- */
+
+
+struct sfl_list *run_satconf(struct sdv_list *symbols)
+{
+	clock_t start, end;
+	double time;
+	struct symbol *sym;
+	struct sdv_node *node;
+	int res;
+	struct sfl_list *ret;
+
+	static struct constants constants = {NULL, NULL, NULL, NULL, NULL};
+	static struct cfdata data = {
+		1,    // unsigned int sat_variable_nr
+		1,    // unsigned int tmp_variable_nr
+		NULL, // struct fexpr *satmap
+		0,    // size_t satmap_size
+		&constants, // struct constants *constants
+		NULL // array with conflict-symbols
+	};
+
+
+	/* check whether all values can be applied -> no need to run */
+	if (sdv_within_range(symbols)) {
+		printd("\nAll symbols are already within range.\n\n");
+		return sfl_list_init();
+	}
+
+	if (!init_done) {
+		printd("\n");
+		printd("Init...");
+
+		/* measure time for constructing constraints and clauses */
+		start = clock();
+
+		/* initialize satmap and cnf_clauses */
+		init_data(&data);
+
+		/* creating constants */
+		create_constants(&data);
+
+		/* assign SAT variables & create sat_map */
+		create_sat_variables(&data);
+
+		/* get the constraints */
+		get_constraints(&data);
+
+		end = clock();
+		time = ((double)(end - start)) / CLOCKS_PER_SEC;
+
+		printd("done. (%.6f secs.)\n", time);
+
+		/* start PicoSAT */
+		pico = initialize_picosat();
+		printd("Building CNF-clauses...");
+		start = clock();
+
+		/* construct the CNF clauses */
+		construct_cnf_clauses(pico, &data);
+
+		end = clock();
+		time = ((double)(end - start)) / CLOCKS_PER_SEC;
+
+		printd("done. (%.6f secs.)\n", time);
+
+		printd("CNF-clauses added: %d\n",
+		       picosat_added_original_clauses(pico));
+
+		init_done = true;
+	}
+
+	/* copy array with symbols to change */
+	data.sdv_symbols = sdv_list_copy(symbols);
+
+	/* add assumptions for conflict-symbols */
+	sym_add_assumption_sdv(pico, data.sdv_symbols);
+
+	/* add assumptions for all other symbols */
+	for_all_symbols(sym) {
+		if (sym->type == S_UNKNOWN)
+			continue;
+
+		if (!sym_is_sdv(data.sdv_symbols, sym))
+			sym_add_assumption(pico, sym);
+	}
+
+	/* store the conflict symbols */
+	conflict_syms = sym_list_init();
+	sdv_list_for_each(node, data.sdv_symbols)
+		sym_list_add(conflict_syms, node->elem->sym);
+
+	printd("Solving SAT-problem...");
+	start = clock();
+
+	res = picosat_sat(pico, -1);
+
+	end = clock();
+	time = ((double)(end - start)) / CLOCKS_PER_SEC;
+	printd("done. (%.6f secs.)\n\n", time);
+
+	if (res == PICOSAT_SATISFIABLE) {
+		printd("===> PROBLEM IS SATISFIABLE <===\n");
+
+		ret = sfl_list_init();
+
+	} else if (res == PICOSAT_UNSATISFIABLE) {
+		printd("===> PROBLEM IS UNSATISFIABLE <===\n");
+		printd("\n");
+
+		ret = rangefix_run(pico, &data);
+	} else {
+		printd("Unknown if satisfiable.\n");
+
+		ret = sfl_list_init();
+	}
+
+	sdv_list_free(data.sdv_symbols);
+	return ret;
+}
+
+/*
+ * check whether a symbol is a conflict symbol
+ */
+static bool sym_is_conflict_sym(struct symbol *sym)
+{
+	struct sym_node *node;
+
+	sym_list_for_each(node, conflict_syms)
+		if (sym == node->elem)
+			return true;
+
+	return false;
+}
+
+/*
+ * check whether all conflict symbols are set to their target values
+ */
+static bool syms_have_target_value(struct sfix_list *list)
+{
+	struct symbol_fix *fix;
+	struct sfix_node *node;
+
+	sfix_list_for_each(node, list) {
+		fix = node->elem;
+
+		if (!sym_is_conflict_sym(fix->sym))
+			continue;
+
+		sym_calc_value(fix->sym);
+
+		if (sym_is_boolean(fix->sym)) {
+			if (fix->tri != sym_get_tristate_value(fix->sym))
+				return false;
+		} else {
+			if (strcmp(str_get(&fix->nb_val),
+				   sym_get_string_value(fix->sym)) != 0)
+				return false;
+		}
+	}
+
+	return true;
+}
+
+/*
+ *
+ * apply the fixes from a diagnosis
+ */
+int apply_fix(struct sfix_list *fix)
+{
+	struct symbol_fix *sfix;
+	struct sfix_node *node, *next;
+	unsigned int no_symbols_set = 0, iterations = 0, manually_changed = 0;
+
+	struct sfix_list *tmp = sfix_list_copy(fix);
+
+	printd("Trying to apply fixes now...\n");
+
+	while (no_symbols_set < fix->size && !syms_have_target_value(fix)) {
+		if (iterations > fix->size * 2) {
+			printd("\nCould not apply all values :-(.\n");
+			return manually_changed;
+		}
+
+		for (node = tmp->head; node != NULL;) {
+			sfix = node->elem;
+
+			/* update symbol's current value */
+			sym_calc_value(sfix->sym);
+
+			/* value already set? */
+			if (sfix->type == SF_BOOLEAN) {
+				if (sfix->tri == sym_get_tristate_value(sfix->sym)) {
+					next = node->next;
+					sfix_list_delete(tmp, node);
+					node = next;
+					no_symbols_set++;
+					continue;
+				}
+			} else if (sfix->type == SF_NONBOOLEAN) {
+				if (strcmp(str_get(&sfix->nb_val),
+					   sym_get_string_value(sfix->sym)) == 0) {
+					next = node->next;
+					sfix_list_delete(tmp, node);
+					node = next;
+					no_symbols_set++;
+					continue;
+				}
+			} else {
+				perror("Error applying fix. Value set for disallowed.");
+			}
+
+			/* could not set value, try next */
+			if (sfix->type == SF_BOOLEAN) {
+				if (!sym_set_tristate_value(sfix->sym,
+							    sfix->tri)) {
+					node = node->next;
+					continue;
+				}
+			} else if (sfix->type == SF_NONBOOLEAN) {
+				if (!sym_set_string_value(
+					    sfix->sym,
+					    str_get(&sfix->nb_val))) {
+					node = node->next;
+					continue;
+				}
+			} else {
+				perror("Error applying fix. Value set for disallowed.");
+			}
+
+			/* could set value, remove from tmp */
+			manually_changed++;
+			if (sfix->type == SF_BOOLEAN) {
+				printd("%s set to %s.\n",
+				       sym_get_name(sfix->sym),
+				       tristate_get_char(sfix->tri));
+			} else if (sfix->type == SF_NONBOOLEAN) {
+				printd("%s set to %s.\n",
+				       sym_get_name(sfix->sym),
+				       str_get(&sfix->nb_val));
+			}
+
+			next = node->next;
+			sfix_list_delete(tmp, node);
+			node = next;
+			no_symbols_set++;
+		}
+
+		iterations++;
+	}
+
+	printd("Fixes successfully applied.\n");
+
+	return manually_changed;
+}
+
+/*
+ * stop RangeFix after the next iteration
+ */
+void interrupt_rangefix(void)
+{
+	stop_rangefix = true;
+}
+
+/*
+ * check whether all symbols are already within range
+ */
+static bool sdv_within_range(struct sdv_list *symbols)
+{
+	struct symbol_dvalue *sdv;
+	struct sdv_node *node;
+
+	sdv_list_for_each(node, symbols) {
+		sdv = node->elem;
+
+		assert(sym_is_boolean(sdv->sym));
+
+		if (sdv->tri == sym_get_tristate_value(sdv->sym))
+			continue;
+
+		if (!sym_tristate_within_range(sdv->sym, sdv->tri))
+			return false;
+	}
+
+	return true;
+}
+
+struct sfix_list *select_solution(struct sfl_list *solutions, int index)
+{
+	struct sfl_node *node = solutions->head;
+	unsigned int counter;
+
+	for (counter = 0; counter < index; counter++)
+		node = node->next;
+
+	return node->elem;
+}
+
+struct symbol_fix *select_symbol(struct sfix_list *solution, int index)
+{
+	struct sfix_node *node = solution->head;
+	unsigned int counter;
+
+	for (counter = 0; counter < index; counter++)
+		node = node->next;
+
+	return node->elem;
+}
diff --git a/scripts/kconfig/configfix.h b/scripts/kconfig/configfix.h
new file mode 100644
index 000000000000..8ebcc807da9d
--- /dev/null
+++ b/scripts/kconfig/configfix.h
@@ -0,0 +1,40 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@xxxxxxxxxx>
+ */
+
+#ifndef CONFIGFIX_H
+#define CONFIGFIX_H
+
+/* make functions accessible from xconfig */
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/* include internal definitions */
+#define LKC_DIRECT_LINK
+#include "lkc.h"
+
+/* include own definitions */
+#include "cf_defs.h"
+
+/* include other header files needed */
+#include "picosat.h"
+#include "cf_constraints.h"
+#include "cf_expr.h"
+#include "cf_rangefix.h"
+#include "cf_utils.h"
+
+/* external functions */
+struct sfl_list *run_satconf(struct sdv_list *symbols);
+int apply_fix(struct sfix_list *fix);
+int run_satconf_cli(const char *Kconfig_file);
+void interrupt_rangefix(void);
+struct sfix_list *select_solution(struct sfl_list *solutions, int index);
+struct symbol_fix *select_symbol(struct sfix_list *solution, int index);
+
+/* make functions accessible from xconfig */
+#ifdef __cplusplus
+}
+#endif
+#endif
-- 
2.39.2