On Wed, Jul 10, 2024 at 3:54 PM Ole Schuerks <ole0811sch@xxxxxxxxx> wrote:
>
> To translate the Kconfig-model into propositional logic and resolve
> conflicts, we need to handle propostional formulas.
> These files contain many functions and macros to deal with
> propositional formulas.
>
> 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/cf_expr.c | 2594 +++++++++++++++++++++++++++++++++++++
> scripts/kconfig/cf_expr.h | 296 +++++
> 2 files changed, 2890 insertions(+)
> create mode 100644 scripts/kconfig/cf_expr.c
> create mode 100644 scripts/kconfig/cf_expr.h
>
> diff --git a/scripts/kconfig/cf_expr.c b/scripts/kconfig/cf_expr.c
> new file mode 100644
> index 000000000000..f015f91ec8c6
> --- /dev/null
> +++ b/scripts/kconfig/cf_expr.c
> @@ -0,0 +1,2594 @@
> +// 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 "cf_expr.h"
> +#include "cf_defs.h"
> +#include "cf_utils.h"
> +
> +static void create_fexpr_bool(struct symbol *sym, struct cfdata *data);
> +static void create_fexpr_nonbool(struct symbol *sym, struct cfdata *data);
> +static void create_fexpr_unknown(struct symbol *sym, struct cfdata *data);
> +static void create_fexpr_choice(struct symbol *sym, struct cfdata *data);
> +
> +static void pexpr_print_util(struct pexpr *e, int prevtoken);
> +static void pexpr_shallow_copy(struct pexpr *dest, struct pexpr *org, unsigned int ref_count);
> +
> +static struct pexpr *pexpr_move_wrapper(
> + struct pexpr *a, struct pexpr *b, struct cfdata *data,
> + enum pexpr_move move,
> + struct pexpr *(*func)(struct pexpr *, struct pexpr *, struct cfdata *));
> +
> +static int trans_count;
> +
> +
> +/*
> + * create a fexpr
> + */
> +struct fexpr *fexpr_create(int satval, enum fexpr_type type, char *name)
> +{
> + struct fexpr *e = xcalloc(1, sizeof(*e));
Why xcalloc() instead of xmalloc()?
(same for all other places)
> +
> + e->satval = satval;
> + e->type = type;
> + e->name = str_new();
> + e->assumption = false;
> + str_append(&e->name, name);
> +
> + return e;
> +}
> +
> +/*
> + * create the fexpr for a symbol
> + */
> +void sym_create_fexpr(struct symbol *sym, struct cfdata *data)
> +{
> + if (sym_is_choice(sym))
> + create_fexpr_choice(sym, data);
> + else if (sym_is_boolean(sym))
> + create_fexpr_bool(sym, data);
> + else if (sym_is_nonboolean(sym))
> + create_fexpr_nonbool(sym, data);
> + else
> + create_fexpr_unknown(sym, data);
> +}
> +
> +/*
> + * create the fexpr for symbols with reverse dependencies
> + */
> +static void create_fexpr_selected(struct symbol *sym, struct cfdata *data)
> +{
> + struct fexpr *fexpr_sel_y;
> + struct fexpr *fexpr_sel_m;
> +
> + /* fexpr_sel_y */
> + fexpr_sel_y = fexpr_create(data->sat_variable_nr++, FE_SELECT, sym->name);
> + str_append(&fexpr_sel_y->name, "_sel_y");
> + fexpr_sel_y->sym = sym;
> + fexpr_add_to_satmap(fexpr_sel_y, data);
> +
> + sym->fexpr_sel_y = fexpr_sel_y;
> +
> + /* fexpr_sel_m */
> + if (sym->type == S_BOOLEAN)
> + return;
> +
> + fexpr_sel_m = fexpr_create(data->sat_variable_nr++, FE_SELECT, sym->name);
> + str_append(&fexpr_sel_m->name, "_sel_m");
> + fexpr_sel_m->sym = sym;
> + fexpr_add_to_satmap(fexpr_sel_m, data);
> +
> + sym->fexpr_sel_m = fexpr_sel_m;
> +}
> +
> +/*
> + * create the fexpr for a boolean/tristate symbol
> + */
> +static void create_fexpr_bool(struct symbol *sym, struct cfdata *data)
> +{
> + struct fexpr *fexpr_y;
> + struct fexpr *fexpr_m;
> +
> + fexpr_y = fexpr_create(data->sat_variable_nr++, FE_SYMBOL, sym->name);
> + fexpr_y->sym = sym;
> + fexpr_y->tri = yes;
> + fexpr_add_to_satmap(fexpr_y, data);
> +
> + sym->fexpr_y = fexpr_y;
> +
> +
> + if (sym->type == S_TRISTATE) {
> + fexpr_m = fexpr_create(data->sat_variable_nr++, FE_SYMBOL, sym->name);
> + str_append(&fexpr_m->name, "_MODULE");
> + fexpr_m->sym = sym;
> + fexpr_m->tri = mod;
> + fexpr_add_to_satmap(fexpr_m, data);
> + } else {
> + fexpr_m = data->constants->const_false;
> + }
> +
> + sym->fexpr_m = fexpr_m;
> +
> + if (sym->rev_dep.expr)
> + create_fexpr_selected(sym, data);
> +}
> +
> +/*
> + * create the fexpr for a non-boolean symbol
> + */
> +static void create_fexpr_nonbool(struct symbol *sym, struct cfdata *data)
> +{
> + /* default values */
> + char int_values[][2] = {"n", "0", "1"};
> + char hex_values[][4] = {"n", "0x0", "0x1"};
> + char string_values[][9] = {"n", "", "nonempty"};
> +
> + sym->fexpr_y = data->constants->const_false;
> + sym->fexpr_m = data->constants->const_false;
> + sym->nb_vals = fexpr_list_init();
> +
> + for (int i = 0; i < 3; i++) {
> + struct fexpr *e = fexpr_create(data->sat_variable_nr++, FE_NONBOOL, sym->name);
> +
> + e->sym = sym;
> + str_append(&e->name, "=");
> + e->nb_val = str_new();
> +
> + switch (sym->type) {
> + case S_INT:
> + str_append(&e->name, int_values[i]);
> + str_append(&e->nb_val, int_values[i]);
> + break;
> + case S_HEX:
> + str_append(&e->name, hex_values[i]);
> + str_append(&e->nb_val, hex_values[i]);
> + break;
> + case S_STRING:
> + str_append(&e->name, string_values[i]);
> + str_append(&e->nb_val, string_values[i]);
> + break;
> + default:
> + break;
> + }
> +
> + fexpr_list_add(sym->nb_vals, e);
> + fexpr_add_to_satmap(e, data);
> + }
> +}
> +
> +/*
> + * set fexpr_y and fexpr_m simply to False
> + */
> +static void create_fexpr_unknown(struct symbol *sym, struct cfdata *data)
> +{
> + sym->fexpr_y = data->constants->const_false;
> + sym->fexpr_m = data->constants->const_false;
> +}
> +
> +/*
> + * create the fexpr for a choice symbol
> + */
> +static void create_fexpr_choice(struct symbol *sym, struct cfdata *data)
> +{
> + struct property *prompt;
> + char *name, *write, *read;
> + struct fexpr *fexpr_y;
> + struct fexpr *fexpr_m;
> +
> + if (!sym_is_boolean(sym))
> + return;
> +
> + prompt = sym_get_prompt(sym);
> + if (prompt == NULL) {
> + perror("Choice symbol should have a prompt.");
> + return;
> + }
> +
> + name = strdup(prompt->text);
> +
> + /* remove spaces */
> + write = name;
> + read = name;
> + do {
> + if (*read != ' ')
> + *write++ = *read;
> + } while (*read++);
> +
> + fexpr_y = fexpr_create(data->sat_variable_nr++, FE_CHOICE, "Choice_");
> + str_append(&fexpr_y->name, name);
> + fexpr_y->sym = sym;
> + fexpr_y->tri = yes;
> + fexpr_add_to_satmap(fexpr_y, data);
> +
> + sym->fexpr_y = fexpr_y;
> +
> + if (sym->type == S_TRISTATE) {
> + fexpr_m = fexpr_create(data->sat_variable_nr++, FE_CHOICE, "Choice_");
> + str_append(&fexpr_m->name, name);
> + str_append(&fexpr_m->name, "_MODULE");
> + fexpr_m->sym = sym;
> + fexpr_m->tri = mod;
> + fexpr_add_to_satmap(fexpr_m, data);
> + } else {
> + fexpr_m = data->constants->const_false;
> + }
> + sym->fexpr_m = fexpr_m;
> + free(name);
> +}
> +
> +/*
> + * evaluate an unequality between a non-Boolean symbol and a constant
> + */
> +static struct pexpr *expr_eval_unequal_nonbool_const(struct symbol *sym, struct symbol *compval,
> + enum expr_type type, struct cfdata *data)
> +{
> + int base;
> + struct pexpr *c;
> + long val;
> + struct fexpr_node *node;
> + struct fexpr *fe;
> +
> + if (!sym || !compval)
> + return pexf(data->constants->const_false);
> +
> + base = 0;
> + switch (sym->type) {
> + case S_INT:
> + base = 10;
> + break;
> + case S_HEX:
> + base = 16;
> + break;
> + default:
> + break;
> + }
> +
> + c = pexf(data->constants->const_false);
> + val = strtol(compval->name, NULL, base);
> + for (node = sym->nb_vals->head->next; node != NULL; node = node->next) {
> + long symval;
> +
> + fe = node->elem;
> + symval = strtol(str_get(&fe->nb_val), NULL, base);
> +
> + switch (type) {
> + case E_LTH:
> + if (symval < val)
> + c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
> + break;
> + case E_LEQ:
> + if (symval <= val)
> + c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
> + break;
> + case E_GTH:
> + if (symval > val)
> + c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
> + break;
> + case E_GEQ:
> + if (symval >= val)
> + c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
> + break;
> + default:
> + perror("Illegal unequal.");
> + }
> + }
> +
> + return c;
> +}
> +
> +/*
> + * evaluate an unequality between 2 Boolean symbols
> + */
> +static struct pexpr *expr_eval_unequal_bool(struct symbol *left, struct symbol *right,
> + enum expr_type type, struct cfdata *data)
> +{
> + struct pexpr *c;
> +
> + if (!left || !right)
> + return pexf(data->constants->const_false);
> +
> + if (!sym_is_boolean(left) || !sym_is_boolean(right)) {
> + perror("Comparing 2 symbols that should be boolean.");
> + return pexf(data->constants->const_false);
> + }
> +
> + switch (type) {
> + case E_LTH:
> + c = pexpr_and(pexpr_not(sym_get_fexpr_both(left, data), data),
> + sym_get_fexpr_both(right, data), data,
> + PEXPR_ARGX);
> + if (left->type == S_TRISTATE)
> + c = pexpr_or(c,
> + pexpr_and(pexf(left->fexpr_m),
> + pexf(right->fexpr_y), data,
> + PEXPR_ARGX),
> + data, PEXPR_ARGX);
> + break;
> + case E_LEQ:
> + c = pexpr_and(pexf(left->fexpr_y), pexf(right->fexpr_y), data,
> + PEXPR_ARGX);
> + if (left->type == S_TRISTATE)
> + c = pexpr_or(c,
> + pexpr_and(pexf(left->fexpr_m),
> + sym_get_fexpr_both(right, data),
> + data, PEXPR_ARGX),
> + data, PEXPR_ARGX);
> + c = pexpr_or(c, pexpr_not(sym_get_fexpr_both(left, data), data),
> + data, PEXPR_ARGX);
> + break;
> + case E_GTH:
> + c = pexpr_and(sym_get_fexpr_both(left, data),
> + pexpr_not(sym_get_fexpr_both(right, data), data),
> + data, PEXPR_ARGX);
> + if (right->type == S_TRISTATE)
> + c = pexpr_or(c,
> + pexpr_and(pexf(left->fexpr_y),
> + pexf(right->fexpr_m), data,
> + PEXPR_ARGX),
> + data, PEXPR_ARGX);
> + break;
> + case E_GEQ:
> + c = pexpr_and(pexf(left->fexpr_y), pexf(right->fexpr_y), data,
> + PEXPR_ARGX);
> + if (right->type == S_TRISTATE)
> + c = pexpr_or(c,
> + pexpr_and(sym_get_fexpr_both(left, data),
> + pexf(right->fexpr_m), data,
> + PEXPR_ARGX),
> + data, PEXPR_ARGX);
> + c = pexpr_or(c,
> + pexpr_not(sym_get_fexpr_both(right, data), data),
> + data, PEXPR_ARGX);
> + break;
> + default:
> + fprintf(stderr, "Wrong type - %s", __func__);
> + c = pexf(data->constants->const_false);
> + }
> +
> + return c;
> +}
> +/*
> + * calculate, when expr will evaluate to yes or mod
> + */
> +struct pexpr *expr_calculate_pexpr_both(struct expr *e, struct cfdata *data)
> +{
> + if (!e)
> + return pexf(data->constants->const_false);
> +
> + if (!expr_can_evaluate_to_mod(e))
> + return expr_calculate_pexpr_y(e, data);
> +
> + switch (e->type) {
> + case E_SYMBOL:
> + return pexpr_or(expr_calculate_pexpr_m(e, data), expr_calculate_pexpr_y(e, data),
> + data, PEXPR_ARGX);
> + case E_AND:
> + return expr_calculate_pexpr_both_and(e->left.expr, e->right.expr, data);
> + case E_OR:
> + return expr_calculate_pexpr_both_or(e->left.expr, e->right.expr, data);
> + case E_NOT:
> + return pexpr_or(expr_calculate_pexpr_m(e, data), expr_calculate_pexpr_y(e, data),
> + data, PEXPR_ARGX);
> + case E_EQUAL:
> + return expr_calculate_pexpr_y_equals(e, data);
> + case E_UNEQUAL:
> + return expr_calculate_pexpr_y_unequals(e, data);
> + case E_LTH:
> + case E_LEQ:
> + case E_GTH:
> + case E_GEQ:
> + return expr_calculate_pexpr_y_comp(e, data);
> + default:
> + // TODO
> + fprintf(stderr, "Unhandled type - %s", __func__);
> + return NULL;
> + }
> +}
> +
> +/*
> + * calculate, when expr will evaluate to yes
> + */
> +struct pexpr *expr_calculate_pexpr_y(struct expr *e, struct cfdata *data)
> +{
> + if (!e)
> + return NULL;
> +
> + switch (e->type) {
> + case E_SYMBOL:
> + return pexf(e->left.sym->fexpr_y);
> + case E_AND:
> + return expr_calculate_pexpr_y_and(e->left.expr, e->right.expr, data);
> + case E_OR:
> + return expr_calculate_pexpr_y_or(e->left.expr, e->right.expr, data);
> + case E_NOT:
> + return expr_calculate_pexpr_y_not(e->left.expr, data);
> + case E_EQUAL:
> + return expr_calculate_pexpr_y_equals(e, data);
> + case E_UNEQUAL:
> + return expr_calculate_pexpr_y_unequals(e, data);
> + case E_LTH:
> + case E_LEQ:
> + case E_GTH:
> + case E_GEQ:
> + return expr_calculate_pexpr_y_comp(e, data);
> + default:
> + fprintf(stderr, "Unhandled type - %s", __func__);
> + return NULL;
> + }
> +}
> +
> +/*
> + * calculate, when expr will evaluate to mod
> + */
> +struct pexpr *expr_calculate_pexpr_m(struct expr *e, struct cfdata *data)
> +{
> + if (!e)
> + return NULL;
> +
> + if (!expr_can_evaluate_to_mod(e))
> + return pexf(data->constants->const_false);
> +
> + switch (e->type) {
> + case E_SYMBOL:
> + return pexf(e->left.sym->fexpr_m);
> + case E_AND:
> + return expr_calculate_pexpr_m_and(e->left.expr, e->right.expr, data);
> + case E_OR:
> + return expr_calculate_pexpr_m_or(e->left.expr, e->right.expr, data);
> + case E_NOT:
> + return expr_calculate_pexpr_m_not(e->left.expr, data);
> + default:
> + perror("Trying to evaluate to mod.");
> + return NULL;
> + }
> +}
> +
> +/*
> + * calculate, when expr of type AND will evaluate to yes
> + * A && B
> + */
> +struct pexpr *expr_calculate_pexpr_y_and(struct expr *a, struct expr *b, struct cfdata *data)
> +{
> + return pexpr_and(expr_calculate_pexpr_y(a, data),
> + expr_calculate_pexpr_y(b, data), data,
> + PEXPR_ARGX);
> +}
> +
> +/*
> + * calculate, when expr of type AND will evaluate to mod
> + * (A || A_m) && (B || B_m) && !(A && B)
> + */
> +struct pexpr *expr_calculate_pexpr_m_and(struct expr *a, struct expr *b,
> + struct cfdata *data)
> +{
> + struct pexpr *topright =
> + pexpr_not(pexpr_and(expr_calculate_pexpr_y(a, data),
> + expr_calculate_pexpr_y(b, data),
> + data, PEXPR_ARGX),
> + data);
> + struct pexpr *ll_left = pexpr_or(expr_calculate_pexpr_y(a, data),
> + expr_calculate_pexpr_m(a, data), data,
> + PEXPR_ARGX);
> + struct pexpr *ll_right = pexpr_or(expr_calculate_pexpr_y(b, data),
> + expr_calculate_pexpr_m(b, data), data,
> + PEXPR_ARGX);
> + struct pexpr *topleft = pexpr_and(ll_left, ll_right, data, PEXPR_ARGX);
> +
> + return pexpr_and(topleft, topright, data, PEXPR_ARGX);
> +}
> +
> +/*
> + * calculate, when expr of type AND will evaluate to mod or yes
> + * (A || A_m) && (B || B_m)
> + */
> +struct pexpr *expr_calculate_pexpr_both_and(struct expr *a, struct expr *b,
> + struct cfdata *data)
> +{
> + struct pexpr *left = pexpr_or(expr_calculate_pexpr_y(a, data),
> + expr_calculate_pexpr_m(a, data), data,
> + PEXPR_ARGX);
> + struct pexpr *right = pexpr_or(expr_calculate_pexpr_y(b, data),
> + expr_calculate_pexpr_m(b, data), data,
> + PEXPR_ARGX);
> +
> + return pexpr_and(left, right, data, PEXPR_ARGX);
> +}
> +
> +/*
> + * calculate, when expr of type OR will evaluate to yes
> + * A || B
> + */
> +struct pexpr *expr_calculate_pexpr_y_or(struct expr *a, struct expr *b,
> + struct cfdata *data)
> +{
> + return pexpr_or(expr_calculate_pexpr_y(a, data),
> + expr_calculate_pexpr_y(b, data), data, PEXPR_ARGX);
> +}
> +
> +/*
> + * calculate, when expr of type OR will evaluate to mod
> + * (A_m || B_m) && !A && !B
> + */
> +struct pexpr *expr_calculate_pexpr_m_or(struct expr *a, struct expr *b,
> + struct cfdata *data)
> +{
> + struct pexpr *topright =
> + pexpr_not(expr_calculate_pexpr_y(b, data), data);
> + struct pexpr *lowerleft = pexpr_or(expr_calculate_pexpr_m(a, data),
> + expr_calculate_pexpr_m(b, data),
> + data, PEXPR_ARGX);
> + struct pexpr *topleft = pexpr_and(
> + lowerleft,
> + pexpr_not(expr_calculate_pexpr_y(a, data), data), data,
> + PEXPR_ARGX);
> +
> + return pexpr_and(topleft, topright, data, PEXPR_ARGX);
> +}
> +
> +/*
> + * calculate, when expr of type OR will evaluate to mod or yes
> + * (A_m || A || B_m || B)
> + */
> +struct pexpr *expr_calculate_pexpr_both_or(struct expr *a, struct expr *b,
> + struct cfdata *data)
> +{
> + struct pexpr *left = pexpr_or(expr_calculate_pexpr_y(a, data),
> + expr_calculate_pexpr_m(a, data), data,
> + PEXPR_ARGX);
> + struct pexpr *right = pexpr_or(expr_calculate_pexpr_y(b, data),
> + expr_calculate_pexpr_m(b, data), data,
> + PEXPR_ARGX);
> +
> + return pexpr_or(left, right, data, PEXPR_ARGX);
> +}
> +
> +/*
> + * calculate, when expr of type NOT will evaluate to yes
> + * !(A || A_m)
> + */
> +struct pexpr *expr_calculate_pexpr_y_not(struct expr *e, struct cfdata *data)
> +{
> + return pexpr_not(pexpr_or(expr_calculate_pexpr_y(e, data),
> + expr_calculate_pexpr_m(e, data),
> + data, PEXPR_ARGX),
> + data);
> +}
> +
> +/*
> + * calculate, when expr of type NOT will evaluate to mod
> + * A_m
> + */
> +struct pexpr *expr_calculate_pexpr_m_not(struct expr *e, struct cfdata *data)
> +{
> + return expr_calculate_pexpr_m(e, data);
> +}
> +
> +static struct pexpr *equiv_pexpr_share(struct pexpr *a, struct pexpr *b,
> + struct cfdata *data)
> +{
> + struct pexpr *yes = pexpr_and_share(a, b, data);
> + struct pexpr *not = pexpr_and(pexpr_not_share(a, data),
> + pexpr_not_share(b, data), data,
> + PEXPR_ARGX);
> +
> + return pexpr_or(yes, not, data, PEXPR_ARGX);
> +}
> +
> +static struct pexpr *equiv_pexpr_move(struct pexpr *a, struct pexpr *b,
> + struct cfdata *data,
> + enum pexpr_move move)
> +{
> + return pexpr_move_wrapper(a, b, data, move, equiv_pexpr_share);
> +}
> +
> +/*
> + * create the fexpr of a non-boolean symbol for a specific value
> + */
> +struct fexpr *sym_create_nonbool_fexpr(struct symbol *sym, char *value,
> + struct cfdata *data)
> +{
> + struct fexpr *e;
> + char *s;
> +
> + if (!strcmp(value, "")) {
> + if (sym->type == S_STRING)
> + return sym->nb_vals->head->next->elem;
> + else
> + return sym->nb_vals->head->elem;
> + }
> +
> + e = sym_get_nonbool_fexpr(sym, value);
> +
> + /* fexpr already exists */
> + if (e != NULL)
> + return e;
> +
> + s = value;
> + if (sym->type == S_INT && !string_is_number(value)) {
> + struct symbol *tmp = sym_find(value);
> +
> + if (tmp != NULL)
> + s = (char *) tmp->curr.val;
> + } else if (sym->type == S_HEX && !string_is_hex(value)) {
> + struct symbol *tmp = sym_find(value);
> +
> + if (tmp != NULL)
> + s = (char *) tmp->curr.val;
> + } else if (sym->type == S_STRING) {
> + struct symbol *tmp = sym_find(value);
> +
> + if (tmp != NULL)
> + s = (char *) tmp->curr.val;
> + }
> +
> + if (!strcmp(s, "")) {
> + if (sym->type == S_STRING)
> + return sym->nb_vals->head->next->elem;
> + else
> + return sym->nb_vals->head->elem;
> + }
> +
> + e = sym_get_nonbool_fexpr(sym, s);
> + if (e != NULL)
> + return e;
> +
> + e = fexpr_create(data->sat_variable_nr++, FE_NONBOOL, sym->name);
> + e->sym = sym;
> + str_append(&e->name, "=");
> + str_append(&e->name, s);
> + e->nb_val = str_new();
> + str_append(&e->nb_val, s);
> +
> + fexpr_list_add(sym->nb_vals, e);
> + fexpr_add_to_satmap(e, data);
> +
> + return e;
> +}
> +
> +/*
> + * return the fexpr of a non-boolean symbol for a specific value, NULL if
> + * non-existent
> + */
> +struct fexpr *sym_get_nonbool_fexpr(struct symbol *sym, char *value)
> +{
> + struct fexpr_node *e;
> +
> + fexpr_list_for_each(e, sym->nb_vals) {
> + if (strcmp(str_get(&e->elem->nb_val), value) == 0)
> + return e->elem;
> + }
> +
> + return NULL;
> +}
> +
> +/*
> + * return the fexpr of a non-boolean symbol for a specific value, if it exists
> + * otherwise create it
> + */
> +struct fexpr *sym_get_or_create_nonbool_fexpr(struct symbol *sym, char *value,
> + struct cfdata *data)
> +{
> + struct fexpr *e = sym_get_nonbool_fexpr(sym, value);
> +
> + if (e != NULL)
> + return e;
> + else
> + return sym_create_nonbool_fexpr(sym, value, data);
> +}
> +
> +/*
> + * calculate, when expr of type EQUAL will evaluate to yes
> + * Side effect: May create certain values in e->{left,right}.sym.nb_vals
> + */
> +struct pexpr *expr_calculate_pexpr_y_equals(struct expr *e, struct cfdata *data)
> +{
> + /* comparing 2 tristate constants */
> + if (sym_is_tristate_constant(e->left.sym) &&
> + sym_is_tristate_constant(e->right.sym))
> + return e->left.sym == e->right.sym ?
> + pexf(data->constants->const_true) :
> + pexf(data->constants->const_false);
> +
> + /* comparing 2 nonboolean constants */
> + if (sym_is_nonbool_constant(e->left.sym) &&
> + sym_is_nonbool_constant(e->right.sym))
> + return strcmp(e->left.sym->name, e->right.sym->name) == 0 ?
> + pexf(data->constants->const_true) :
> + pexf(data->constants->const_false);
> +
> + /* comparing 2 boolean/tristate incl. yes/mod/no constants */
> + if (sym_is_bool_or_triconst(e->left.sym) &&
> + sym_is_bool_or_triconst(e->right.sym)) {
> + struct pexpr *yes = equiv_pexpr_move(
> + pexf(e->left.sym->fexpr_y), pexf(e->right.sym->fexpr_y),
> + data, PEXPR_ARGX);
> + struct pexpr *mod = equiv_pexpr_move(
> + pexf(e->left.sym->fexpr_m), pexf(e->right.sym->fexpr_m),
> + data, PEXPR_ARGX);
> +
> + return pexpr_and(yes, mod, data, PEXPR_ARGX);
> + }
> +
> + /* comparing nonboolean with a constant */
> + if (sym_is_nonboolean(e->left.sym) &&
> + sym_is_nonbool_constant(e->right.sym))
> + return pexf(sym_get_or_create_nonbool_fexpr(
> + e->left.sym, e->right.sym->name, data));
> +
> + if (sym_is_nonbool_constant(e->left.sym) &&
> + sym_is_nonboolean(e->right.sym))
> + return pexf(sym_get_or_create_nonbool_fexpr(
> + e->right.sym, e->left.sym->name, data));
> +
> + /* comparing nonboolean with tristate constant, will never be true */
> + if (sym_is_nonboolean(e->left.sym) &&
> + sym_is_tristate_constant(e->right.sym))
> + return pexf(data->constants->const_false);
> + if (sym_is_tristate_constant(e->left.sym) &&
> + sym_is_nonboolean(e->right.sym))
> + return pexf(data->constants->const_false);
> +
> + /* comparing 2 nonboolean symbols */
> + if (sym_is_nonboolean(e->left.sym) && sym_is_nonboolean(e->right.sym)) {
> + struct pexpr *c = pexf(data->constants->const_false);
> + struct fexpr *e1, *e2;
> +
> + for (struct fexpr_node *node1 =
> + e->left.sym->nb_vals->head->next;
> + node1 != NULL; node1 = node1->next) {
> + e1 = node1->elem;
> + for (struct fexpr_node *node2 =
> + e->right.sym->nb_vals->head->next;
> + node2 != NULL; node2 = node2->next) {
> + e2 = node2->elem;
> + if (!strcmp(str_get(&e1->nb_val),
> + str_get(&e2->nb_val))) {
> + c = pexpr_or(
> + c,
> + pexpr_and(pexf(e1),
> + pexf(e2), data,
> + PEXPR_ARGX),
> + data, PEXPR_ARGX);
> + break;
> + }
> + }
> + }
> + return c;
> + }
> +
> + /* comparing boolean item with nonboolean constant, will never be true */
> + if (sym_is_tristate_constant(e->left.sym) &&
> + sym_is_nonbool_constant(e->right.sym))
> + return pexf(data->constants->const_false);
> + if (sym_is_nonbool_constant(e->left.sym) &&
> + sym_is_tristate_constant(e->right.sym))
> + return pexf(data->constants->const_false);
> +
> + /* comparing symbol of type unknown with tristate constant */
> + if (e->left.sym->type == S_UNKNOWN &&
> + sym_is_tristate_constant(e->right.sym))
> + return pexf(data->constants->const_false);
> + if (sym_is_tristate_constant(e->left.sym) &&
> + e->right.sym->type == S_UNKNOWN)
> + return pexf(data->constants->const_false);
> +
> + /* any other comparison is not supported and should not be executed */
> + fprintf(stderr, "Unsupported equality.");
> + print_expr(":", e, 0);
> +
> + return pexf(data->constants->const_false);
> +}
> +
> +/*
> + * transform an UNEQUAL into a Not(EQUAL)
> + */
> +struct pexpr *expr_calculate_pexpr_y_unequals(struct expr *e, struct cfdata *data)
> +{
> + return pexpr_not(expr_calculate_pexpr_y_equals(e, data), data);
> +}
> +
> +struct pexpr *expr_calculate_pexpr_y_comp(struct expr *e, struct cfdata *data)
> +{
> + if (!e)
> + return NULL;
> +
> + switch (e->type) {
> + case E_LTH:
> + case E_LEQ:
> + case E_GTH:
> + case E_GEQ:
> + /* compare non-Boolean symbol with constant */
> + if (sym_is_nonboolean(e->left.sym) &&
> + e->right.sym->type == S_UNKNOWN &&
> + string_is_number(e->right.sym->name)
> + ) {
> + return expr_eval_unequal_nonbool_const(e->left.sym, e->right.sym, e->type,
> + data);
> + }
> + if (sym_is_nonboolean(e->right.sym) &&
> + e->left.sym->type == S_UNKNOWN &&
> + string_is_number(e->left.sym->name)
> + ) {
> + return expr_eval_unequal_nonbool_const(e->right.sym, e->left.sym, e->type,
> + data);
> + }
> +
> + /* compare 2 Boolean symbols */
> + if (sym_is_boolean(e->left.sym) && sym_is_boolean(e->right.sym))
> + return expr_eval_unequal_bool(e->left.sym, e->right.sym, e->type, data);
> +
> + return pexf(data->constants->const_false);
> + default:
> + fprintf(stderr, "Unhandled type - %s", __func__);
> + return NULL;
> + }
> +}
> +
> +static struct pexpr *pexpr_move_wrapper(
> + struct pexpr *a, struct pexpr *b, struct cfdata *data,
> + enum pexpr_move move,
> + struct pexpr *(*func)(struct pexpr *, struct pexpr *, struct cfdata *))
> +{
> + struct pexpr *retval = func(a, b, data);
> +
> + switch (move) {
> + case PEXPR_ARG1:
> + pexpr_put(a);
> + break;
> + case PEXPR_ARG2:
> + pexpr_put(b);
> + break;
> + case PEXPR_ARGX:
> + pexpr_put(a);
> + pexpr_put(b);
> + break;
> + default:
> + fprintf(stderr, "%s: invalid value for @move - %d\n", __func__,
> + move);
> + }
> + return retval;
> +}
> +
> +struct pexpr *pexpr_and(struct pexpr *a, struct pexpr *b, struct cfdata *data, enum pexpr_move move)
> +{
> + return pexpr_move_wrapper(a, b, data, move, pexpr_and_share);
> +}
> +
> +/*
> + * macro to create a pexpr of type AND
> + */
> +struct pexpr *pexpr_and_share(struct pexpr *a, struct pexpr *b, struct cfdata *data)
> +{
> + struct pexpr *e;
> +
> + /* A && A -> A */
> + if (a == b || pexpr_eq(a, b, data)) {
> + pexpr_get(a);
> + return a;
> + }
> +
> + /* simplifications:
> + * expr && False -> False
> + * expr && True -> expr
> + */
> + if ((a->type == PE_SYMBOL &&
> + a->left.fexpr == data->constants->const_false) ||
> + (b->type == PE_SYMBOL &&
> + b->left.fexpr == data->constants->const_true)) {
> + pexpr_get(a);
> + return a;
> + }
> +
> + if ((b->type == PE_SYMBOL &&
> + b->left.fexpr == data->constants->const_false) ||
> + (a->type == PE_SYMBOL &&
> + a->left.fexpr == data->constants->const_true)) {
> + pexpr_get(b);
> + return b;
> + }
> +
> + /* (A && B) && C -> A && B if B == C */
> + if (a->type == PE_AND && pexpr_eq(a->right.pexpr, b, data)) {
> + pexpr_get(a);
> + return a;
> + }
> +
> + /* A && (B && C) -> B && C if A == B */
> + if (b->type == PE_AND && pexpr_eq(a, b->left.pexpr, data)) {
> + pexpr_get(b);
> + return b;
> + }
> +
> + if (a->type == PE_OR && b->type == PE_OR) {
> + e = NULL;
> + /* (A || B) && (C || D) -> A || (B && D) if A == C */
> + if (pexpr_eq(a->left.pexpr, b->left.pexpr, data)) {
> + e = pexpr_or(a->left.pexpr,
> + pexpr_and_share(a->right.pexpr,
> + b->right.pexpr, data),
> + data, PEXPR_ARG2);
> + }
> + /* (A || B) && (C || D) -> B || (A && C) if B == D */
> + else if (pexpr_eq(a->right.pexpr, b->right.pexpr, data)) {
> + e = pexpr_or(a->right.pexpr,
> + pexpr_and_share(a->left.pexpr,
> + b->left.pexpr, data),
> + data, PEXPR_ARG2);
> + }
> + /* (A || B) && (C || D) -> A || (B && C) if A == D */
> + else if (pexpr_eq(a->left.pexpr, b->right.pexpr, data)) {
> + e = pexpr_or(a->left.pexpr,
> + pexpr_and_share(a->right.pexpr,
> + b->left.pexpr, data),
> + data, PEXPR_ARG2);
> + }
> + /* (A || B) && (C || D) -> B || (A && D) if B == C */
> + else if (pexpr_eq(a->right.pexpr, b->left.pexpr, data)) {
> + e = pexpr_or(a->right.pexpr,
> + pexpr_and_share(a->left.pexpr,
> + b->right.pexpr, data),
> + data, PEXPR_ARG2);
> + }
> + if (e)
> + return e;
> + }
> +
> + /* general case */
> + e = xcalloc(1, sizeof(*e));
> + pexpr_get(a);
> + pexpr_get(b);
> + pexpr_construct_and(e, a, b, 1);
> + return e;
> +}
> +
> +struct pexpr *pexpr_or(struct pexpr *a, struct pexpr *b, struct cfdata *data, enum pexpr_move move)
> +{
> + return pexpr_move_wrapper(a, b, data, move, pexpr_or_share);
> +}
> +
> +/*
> + * macro to create a pexpr of type OR
> + */
> +struct pexpr *pexpr_or_share(struct pexpr *a, struct pexpr *b, struct cfdata *data)
> +{
> + struct pexpr *e;
> + bool cond1, cond2;
> +
> + /* A || A -> A */
> + if (a == b || pexpr_eq(a, b, data)) {
> + pexpr_get(a);
> + return a;
> + }
> +
> + /* simplifications:
> + * A || False -> A
> + * A || True -> True
> + */
> + cond1 = a->type == PE_SYMBOL && a->left.fexpr == data->constants->const_false;
> + cond2 = b->type == PE_SYMBOL && b->left.fexpr == data->constants->const_true;
> + if (cond1 || cond2) {
> + pexpr_get(b);
> + return b;
> + }
> + cond1 = b->type == PE_SYMBOL && b->left.fexpr == data->constants->const_false;
> + cond2 = a->type == PE_SYMBOL && a->left.fexpr == data->constants->const_true;
> + if (cond1 || cond2) {
> + pexpr_get(a);
> + return a;
> + }
> +
> + /* A || (B && C) -> A if (A == B || A == C) */
> + if (b->type == PE_AND && (
> + pexpr_eq(a, b->left.pexpr, data) || pexpr_eq(a, b->right.pexpr, data)
> + )) {
> + pexpr_get(a);
> + return a;
> + }
> + /* (A && B) || C -> C if (A == C || B == C) */
> + if (a->type == PE_AND && (
> + pexpr_eq(a->left.pexpr, b, data) || pexpr_eq(a->right.pexpr, b, data)
> + )) {
> + pexpr_get(b);
> + return b;
> + }
> +
> + /* -A || B -> True if A == B
> + * A || -B -> True if A == B
> + */
> + cond1 = a->type == PE_NOT && pexpr_eq(a->left.pexpr, b, data);
> + cond2 = b->type == PE_NOT && pexpr_eq(a, b->left.pexpr, data);
> + if (cond1 || cond2)
> + return pexf(data->constants->const_true);
> +
> + if (a->type == PE_AND && b->type == PE_AND) {
> + e = NULL;
> + /* (A && B) || (C && D) -> A && (B || D) if (A == C) */
> + if (pexpr_eq(a->left.pexpr, b->left.pexpr, data)) {
> + e = pexpr_and(a->left.pexpr,
> + pexpr_or_share(a->right.pexpr, b->right.pexpr, data), data,
> + PEXPR_ARG2);
> + }
> + /* (A && B) || (C && D) -> B && (A || C) if (B == D) */
> + if (pexpr_eq(a->right.pexpr, b->right.pexpr, data)) {
> + e = pexpr_and(a->right.pexpr,
> + pexpr_or_share(a->left.pexpr, b->left.pexpr, data), data,
> + PEXPR_ARG2);
> + }
> + /* (A && B) || (C && D) -> A && (B || C) if (A == D) */
> + if (pexpr_eq(a->left.pexpr, b->right.pexpr, data)) {
> + e = pexpr_and(a->left.pexpr,
> + pexpr_or_share(a->right.pexpr, b->left.pexpr, data), data,
> + PEXPR_ARG2);
> + }
> + /* (A && B) || (C && D) -> B && (A || D) if (B == C) */
> + if (pexpr_eq(a->right.pexpr, b->left.pexpr, data)) {
> + e = pexpr_and(a->right.pexpr,
> + pexpr_or_share(a->left.pexpr, b->right.pexpr, data), data,
> + PEXPR_ARG2);
> + }
> + if (e)
> + return e;
> + }
> +
> + /* (A && B) || (C || D) -> C || D if
> + * A == C || A == D || B == C || B == D
> + */
> + if (a->type == PE_AND && b->type == PE_OR && (
> + pexpr_eq(a->left.pexpr, b->left.pexpr, data) ||
> + pexpr_eq(a->left.pexpr, b->right.pexpr, data) ||
> + pexpr_eq(a->right.pexpr, b->left.pexpr, data) ||
> + pexpr_eq(a->right.pexpr, b->right.pexpr, data)
> + )) {
> + pexpr_get(b);
> + return b;
> + }
> + /* (C || D) || (A && B) -> C || D if
> + * A == C || A == D || B == C || B == D
> + */
> + if (a->type == PE_OR && b->type == PE_AND && (
> + pexpr_eq(a->left.pexpr, b->left.pexpr, data) ||
> + pexpr_eq(a->left.pexpr, b->right.pexpr, data) ||
> + pexpr_eq(a->right.pexpr, b->left.pexpr, data) ||
> + pexpr_eq(a->right.pexpr, b->right.pexpr, data)
> + )) {
> + pexpr_get(a);
> + return a;
> + }
> +
> + /* general case */
> + e = xcalloc(1, sizeof(*e));
> + pexpr_get(a);
> + pexpr_get(b);
> + pexpr_construct_or(e, a, b, 1);
> +
> + return e;
> +}
> +
> +struct pexpr *pexpr_not(struct pexpr *a, struct cfdata *data)
> +{
> + struct pexpr *retval = pexpr_not_share(a, data);
> +
> + pexpr_put(a);
> + return retval;
> +}
> +
> +/*
> + * Builds NOT(@a)
> + */
> +struct pexpr *pexpr_not_share(struct pexpr *a, struct cfdata *data)
> +{
> + struct pexpr *ret_val;
> +
> + if (a->type == PE_SYMBOL &&
> + a->left.fexpr == data->constants->const_false)
> + ret_val = pexf(data->constants->const_true);
> + else if (a->type == PE_SYMBOL &&
> + a->left.fexpr == data->constants->const_true)
> + ret_val = pexf(data->constants->const_false);
> + /* eliminate double negation */
> + else if (a->type == PE_NOT) {
> + ret_val = a->left.pexpr;
> + pexpr_get(ret_val);
> + }
> + /* De Morgan */
> + else if (a->type == PE_AND) {
> + ret_val = xmalloc(sizeof(*ret_val));
> + pexpr_construct_or(ret_val,
> + pexpr_not_share(a->left.pexpr, data),
> + pexpr_not_share(a->right.pexpr, data), 1);
> + } else if (a->type == PE_OR) {
> + ret_val = xmalloc(sizeof(*ret_val));
> + pexpr_construct_and(ret_val,
> + pexpr_not_share(a->left.pexpr, data),
> + pexpr_not_share(a->right.pexpr, data), 1);
> + } else {
> + ret_val = xmalloc(sizeof(*ret_val));
> + pexpr_get(a);
> + pexpr_construct_not(ret_val, a, 1);
> + }
> +
> + return ret_val;
> +}
> +
> +struct pexpr *pexpr_implies(struct pexpr *a, struct pexpr *b, struct cfdata *data,
> + enum pexpr_move move)
> +{
> + return pexpr_move_wrapper(a, b, data, move, pexpr_implies_share);
> +}
> +
> +/*
> + * macro to construct a pexpr for "A implies B"
> + */
> +struct pexpr *pexpr_implies_share(struct pexpr *a, struct pexpr *b, struct cfdata *data)
> +{
> + /* A => B -> True if A == B */
> + if (a == b || pexpr_eq(a, b, data))
> + return pexf(data->constants->const_true);
> +
> + /* (A => B && C) -> (A => C) if A == B */
> + if (b->type == PE_AND && pexpr_eq(a, b->left.pexpr, data))
> + return pexpr_implies_share(a, b->right.pexpr, data);
> + /* (A => B && C) -> (A => B) if A == C */
> + if (b->type == PE_AND && pexpr_eq(a, b->right.pexpr, data))
> + return pexpr_implies_share(a, b->left.pexpr, data);
> +
> + /* (A => B || C) -> True if (A == B || A == C) */
> + if (b->type == PE_OR && (
> + pexpr_eq(a, b->left.pexpr, data) || pexpr_eq(a, b->right.pexpr, data)
> + ))
> + return pexf(data->constants->const_true);
> +
> + /* (A && B => C) -> True if (A == C || B == C) */
> + if (a->type == PE_AND && (
> + pexpr_eq(a->left.pexpr, b, data) || pexpr_eq(a->right.pexpr, b, data)
> + ))
> + return pexf(data->constants->const_true);
> +
> + return pexpr_or(pexpr_not_share(a, data), b, data, PEXPR_ARG1);
> +}
> +
> +/*
> + * check whether a pexpr is in CNF
> + */
> +bool pexpr_is_cnf(struct pexpr *e)
> +{
> + if (!e)
> + return false;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + return true;
> + case PE_AND:
> + return false;
> + case PE_OR:
> + return pexpr_is_cnf(e->left.pexpr) &&
> + pexpr_is_cnf(e->right.pexpr);
> + case PE_NOT:
> + return e->left.pexpr->type == PE_SYMBOL;
> + }
> +
> + return false;
> +}
> +
> +/*
> + * check whether a pexpr is in NNF
> + */
> +bool pexpr_is_nnf(struct pexpr *e)
> +{
> + if (!e)
> + return false;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + return true;
> + case PE_AND:
> + case PE_OR:
> + return pexpr_is_nnf(e->left.pexpr) && pexpr_is_nnf(e->right.pexpr);
> + case PE_NOT:
> + return e->left.pexpr->type == PE_SYMBOL;
> + }
> +
> + return false;
> +}
> +
> +/*
> + * return fexpr_both for a symbol
> + */
> +struct pexpr *sym_get_fexpr_both(struct symbol *sym, struct cfdata *data)
> +{
> + return sym->type == S_TRISTATE ?
> + pexpr_or(pexf(sym->fexpr_m), pexf(sym->fexpr_y),
> + data, PEXPR_ARGX) :
> + pexf(sym->fexpr_y);
> +}
> +
> +/*
> + * return fexpr_sel_both for a symbol
> + */
> +struct pexpr *sym_get_fexpr_sel_both(struct symbol *sym, struct cfdata *data)
> +{
> + if (!sym->rev_dep.expr)
> + return pexf(data->constants->const_false);
> +
> + return sym->type == S_TRISTATE ?
> + pexpr_or(pexf(sym->fexpr_sel_m),
> + pexf(sym->fexpr_sel_y), data, PEXPR_ARGX) :
> + pexf(sym->fexpr_sel_y);
> +}
> +
> +/*
> + * check, if the fexpr is a symbol, a True/False-constant, a literal symbolizing a non-boolean or
> + * a choice symbol
> + */
> +bool fexpr_is_symbol(struct fexpr *e)
> +{
> + return e->type == FE_SYMBOL || e->type == FE_FALSE || e->type == FE_TRUE ||
> + e->type == FE_NONBOOL || e->type == FE_CHOICE || e->type == FE_SELECT ||
> + e->type == FE_NPC;
> +}
> +
> +/*
> + * check whether a pexpr is a symbol or a negated symbol
> + */
> +bool pexpr_is_symbol(struct pexpr *e)
> +{
> + return e->type == PE_SYMBOL || (e->type == PE_NOT && e->left.pexpr->type == PE_SYMBOL);
> +}
> +
> +/*
> + * check whether the fexpr is a constant (true/false)
> + */
> +bool fexpr_is_constant(struct fexpr *e, struct cfdata *data)
> +{
> + return e == data->constants->const_true || e == data->constants->const_false;
> +}
> +
> +/*
> + * add a fexpr to the satmap
> + */
> +void fexpr_add_to_satmap(struct fexpr *e, struct cfdata *data)
> +{
> + if (e->satval >= data->satmap_size) {
> + data->satmap =
> + xrealloc(data->satmap, data->satmap_size * 2 * sizeof(**data->satmap));
> + data->satmap_size *= 2;
> + }
> +
> + data->satmap[e->satval] = e;
I see a bug here.
Size mismatch for memory allocation.
(much bigger than used)
> +}
> +
> +/*
> + * print a fexpr
> + */
> +void fexpr_print(char *tag, struct fexpr *e)
> +{
> + if (!e)
> + return;
> +
> + printf("%s: %s\n", tag, str_get(&e->name));
> +}
> +
> +/*
> + * write an fexpr into a string (format needed for testing)
> + */
> +void fexpr_as_char(struct fexpr *e, struct gstr *s)
> +{
> + if (!e)
> + return;
> +
> + switch (e->type) {
> + case FE_SYMBOL:
> + case FE_CHOICE:
> + case FE_SELECT:
> + case FE_NPC:
> + case FE_NONBOOL:
> + str_append(s, "definedEx(");
> + str_append(s, str_get(&e->name));
> + str_append(s, ")");
> + return;
> + case FE_FALSE:
> + str_append(s, "0");
> + return;
> + case FE_TRUE:
> + str_append(s, "1");
> + return;
> + default:
> + return;
> + }
> +}
> +
> +/*
> + * write a pexpr into a string
> + */
> +void pexpr_as_char(struct pexpr *e, struct gstr *s, int parent, struct cfdata *data)
> +{
> + if (!e)
> + return;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + if (e->left.fexpr == data->constants->const_false) {
> + str_append(s, "0");
> + return;
> + }
> + if (e->left.fexpr == data->constants->const_true) {
> + str_append(s, "1");
> + return;
> + }
> + str_append(s, "definedEx(");
> + str_append(s, str_get(&e->left.fexpr->name));
> + str_append(s, ")");
> + return;
> + case PE_AND:
> + if (parent != PE_AND)
> + str_append(s, "(");
> + pexpr_as_char(e->left.pexpr, s, PE_AND, data);
> + str_append(s, " && ");
> + pexpr_as_char(e->right.pexpr, s, PE_AND, data);
> + if (parent != PE_AND)
> + str_append(s, ")");
> + return;
> + case PE_OR:
> + if (parent != PE_OR)
> + str_append(s, "(");
> + pexpr_as_char(e->left.pexpr, s, PE_OR, data);
> + str_append(s, " || ");
> + pexpr_as_char(e->right.pexpr, s, PE_OR, data);
> + if (parent != PE_OR)
> + str_append(s, ")");
> + return;
> + case PE_NOT:
> + str_append(s, "!");
> + pexpr_as_char(e->left.pexpr, s, PE_NOT, data);
> + return;
> + }
> +}
> +
> +/*
> + * write a pexpr into a string
> + */
> +void pexpr_as_char_short(struct pexpr *e, struct gstr *s, int parent)
> +{
> + if (!e)
> + return;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + str_append(s, str_get(&e->left.fexpr->name));
> + return;
> + case PE_AND:
> + if (parent != PE_AND)
> + str_append(s, "(");
> + pexpr_as_char_short(e->left.pexpr, s, PE_AND);
> + str_append(s, " && ");
> + pexpr_as_char_short(e->right.pexpr, s, PE_AND);
> + if (parent != PE_AND)
> + str_append(s, ")");
> + return;
> + case PE_OR:
> + if (parent != PE_OR)
> + str_append(s, "(");
> + pexpr_as_char_short(e->left.pexpr, s, PE_OR);
> + str_append(s, " || ");
> + pexpr_as_char_short(e->right.pexpr, s, PE_OR);
> + if (parent != PE_OR)
> + str_append(s, ")");
> + return;
> + case PE_NOT:
> + str_append(s, "!");
> + pexpr_as_char_short(e->left.pexpr, s, PE_NOT);
> + return;
> + }
> +}
> +
> +/*
> + * check whether a pexpr contains a specific fexpr
> + */
> +bool pexpr_contains_fexpr(struct pexpr *e, struct fexpr *fe)
> +{
> + if (!e)
> + return false;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + return e->left.fexpr->satval == fe->satval;
> + case PE_AND:
> + case PE_OR:
> + return pexpr_contains_fexpr(e->left.pexpr, fe) ||
> + pexpr_contains_fexpr(e->right.pexpr, fe);
> + case PE_NOT:
> + return e->left.pexpr->left.fexpr->satval == fe->satval;
> + }
> +
> + return false;
> +}
> +
> +/*
> + * init list of fexpr
> + */
> +struct fexpr_list *fexpr_list_init(void)
> +{
> + struct fexpr_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of fexpr_list
> + */
> +struct fexl_list *fexl_list_init(void)
> +{
> + struct fexl_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of pexpr
> + */
> +struct pexpr_list *pexpr_list_init(void)
> +{
> + struct pexpr_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of symbol_fix
> + */
> +struct sfix_list *sfix_list_init(void)
> +{
> + struct sfix_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of symbol_fix
> + */
> +struct sfl_list *sfl_list_init(void)
> +{
> + struct sfl_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of symbol_dvalue
> + */
> +struct sdv_list *sdv_list_init(void)
> +{
> + struct sdv_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of symbols
> + */
> +struct sym_list *sym_list_init(void)
> +{
> + struct sym_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of default_maps
> + */
> +struct defm_list *defm_list_init(void)
> +{
> + struct defm_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
> +
> +/*
> + * init list of properties
> + */
> +struct prop_list *prop_list_init(void)
> +{
> + struct prop_list *list = xcalloc(1, sizeof(*list));
> +
> + list->head = NULL;
> + list->tail = NULL;
> + list->size = 0;
> +
> + return list;
> +}
A bunch of similar *_list_init() functions.
Do not do this.
Kconfig uses the similar liss.h to the kernel space.
Remove all the duplications.
> +/*
> + * add element to tail of a fexpr_list
> + */
> +void fexpr_list_add(struct fexpr_list *list, struct fexpr *fe)
> +{
> + struct fexpr_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = fe;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a fexl_list
> + */
> +void fexl_list_add(struct fexl_list *list, struct fexpr_list *elem)
> +{
> + struct fexl_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = elem;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a pexpr_list
> + */
> +void pexpr_list_add(struct pexpr_list *list, struct pexpr *e)
> +{
> + struct pexpr_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = e;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a sfix_list
> + */
> +void sfix_list_add(struct sfix_list *list, struct symbol_fix *fix)
> +{
> + struct sfix_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = fix;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a sfl_list
> + */
> +void sfl_list_add(struct sfl_list *list, struct sfix_list *elem)
> +{
> + struct sfl_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = elem;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a sdv_list
> + */
> +void sdv_list_add(struct sdv_list *list, struct symbol_dvalue *sdv)
> +{
> + struct sdv_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = sdv;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a sym_list
> + */
> +void sym_list_add(struct sym_list *list, struct symbol *sym)
> +{
> + struct sym_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = sym;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a defm_list
> + */
> +void defm_list_add(struct defm_list *list, struct default_map *map)
> +{
> + struct defm_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = map;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
> +
> +/*
> + * add element to tail of a prop_list
> + */
> +void prop_list_add(struct prop_list *list, struct property *prop)
> +{
> + struct prop_node *node = xcalloc(1, sizeof(*node));
> +
> + node->elem = prop;
> +
> + if (list->size == 0) {
> + list->head = node;
> + list->tail = node;
> + } else {
> + node->prev = list->tail;
> + list->tail = node;
> + node->prev->next = node;
> + }
> +
> + list->size++;
> +}
Again. A bunch of *_list_add().
> +/*
> + * delete an element from a fexpr_list
> + */
> +void fexpr_list_delete(struct fexpr_list *list, struct fexpr_node *node)
> +{
> + if (list->size == 0 || node == NULL)
> + return;
> +
> + if (node == list->head)
> + list->head = node->next;
> + else
> + node->prev->next = node->next;
> +
> + if (node == list->tail)
> + list->tail = node->prev;
> + else
> + node->next->prev = node->prev;
> +
> + list->size--;
> + free(node);
> +}
> +
> +/*
> + * delete an element from a fexpr_list
> + */
> +void sfix_list_delete(struct sfix_list *list, struct sfix_node *node)
> +{
> + if (list->size == 0 || node == NULL)
> + return;
> +
> + if (node == list->head)
> + list->head = node->next;
> + else
> + node->prev->next = node->next;
> +
> + if (node == list->tail)
> + list->tail = node->prev;
> + else
> + node->next->prev = node->prev;
> +
> + list->size--;
> + free(node);
> +}
> +
> +/*
> + * delete an element from a fexpr_list
> + */
> +void pexpr_list_delete(struct pexpr_list *list, struct pexpr_node *node)
> +{
> + if (list->size == 0 || node == NULL)
> + return;
> +
> + if (node == list->head)
> + list->head = node->next;
> + else
> + node->prev->next = node->next;
> +
> + if (node == list->tail)
> + list->tail = node->prev;
> + else
> + node->next->prev = node->prev;
> +
> + list->size--;
> + free(node);
> +}
> +
> +/*
> + * delete an element from a fexl_list
> + */
> +void fexl_list_delete(struct fexl_list *list, struct fexl_node *node)
> +{
> + if (list->size == 0 || node == NULL)
> + return;
> +
> + if (node == list->head)
> + list->head = node->next;
> + else
> + node->prev->next = node->next;
> +
> + if (node == list->tail)
> + list->tail = node->prev;
> + else
> + node->next->prev = node->prev;
> +
> + list->size--;
> + free(node);
> +}
> +
> +/*
> + * delete the first occurrence of elem in an fexl_list
> + */
> +void fexl_list_delete_elem(struct fexl_list *list, struct fexpr_list *elem)
> +{
> + struct fexl_node *node, *to_delete = NULL;
> +
> + fexl_list_for_each(node, list) {
> + if (node->elem == elem) {
> + to_delete = node;
> + break;
> + }
> + }
> +
> + if (to_delete != NULL)
> + fexl_list_delete(list, to_delete);
> +}
> +
> +/*
> + * make a shallow copy of a fexpr_list
> + */
> +struct fexpr_list *fexpr_list_copy(struct fexpr_list *list)
> +{
> + struct fexpr_list *ret = fexpr_list_init();
> + struct fexpr_node *node;
> +
> + fexpr_list_for_each(node, list)
> + fexpr_list_add(ret, node->elem);
> +
> + return ret;
> +}
> +
> +/*
> + * make a shallow copy of a fexl_list
> + */
> +struct fexl_list *fexl_list_copy(struct fexl_list *list)
> +{
> + struct fexl_list *ret = fexl_list_init();
> + struct fexl_node *node;
> +
> + fexl_list_for_each(node, list)
> + fexl_list_add(ret, node->elem);
> +
> + return ret;
> +}
> +
> +/*
> + * make a shallow copy of a sdv_list
> + */
> +struct sdv_list *sdv_list_copy(struct sdv_list *list)
> +{
> + struct sdv_list *ret = sdv_list_init();
> + struct sdv_node *node;
> +
> + sdv_list_for_each(node, list)
> + sdv_list_add(ret, node->elem);
> +
> +
> + return ret;
> +}
> +
> +/*
> + * make a shallow copy of a sfix_list
> + */
> +struct sfix_list *sfix_list_copy(struct sfix_list *list)
> +{
> + struct sfix_list *ret = sfix_list_init();
> + struct sfix_node *node;
> +
> + sfix_list_for_each(node, list)
> + sfix_list_add(ret, node->elem);
> +
> + return ret;
> +}
> +
> +/*
> + * print a fexpr_list
> + */
> +void fexpr_list_print(char *title, struct fexpr_list *list)
> +{
> + struct fexpr_node *node;
> +
> + printf("%s: [", title);
> +
> + fexpr_list_for_each(node, list) {
> + printf("%s", str_get(&node->elem->name));
> + if (node->next != NULL)
> + printf(", ");
> + }
> +
> + printf("]\n");
> +}
> +
> +/*
> + * print a fexl_list
> + */
> +void fexl_list_print(char *title, struct fexl_list *list)
> +{
> + struct fexl_node *node;
> +
> + printf("%s:\n", title);
> +
> + fexl_list_for_each(node, list)
> + fexpr_list_print(":", node->elem);
> +}
> +
> +/*
> + * print a pexpr_list
> + */
> +void pexpr_list_print(char *title, struct pexpr_list *list)
> +{
> + struct pexpr_node *node;
> +
> + printf("%s: [", title);
> +
> + pexpr_list_for_each(node, list) {
> + pexpr_print_util(node->elem, -1);
> + if (node->next != NULL)
> + printf(", ");
> + }
> +
> + printf("]\n");
> +}
> +
> +/*
> + * free an fexpr_list
> + */
> +void fexpr_list_free(struct fexpr_list *list)
> +{
> + struct fexpr_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * free an defm_list (and pexpr_put the conditions of the maps and free the
> + * node->element's)
> + */
> +void defm_list_destruct(struct defm_list *list)
> +{
> + struct defm_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + pexpr_put(node->elem->e);
> + free(node->elem);
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * free an fexl_list
> + */
> +void fexl_list_free(struct fexl_list *list)
> +{
> + struct fexl_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * free a sdv_list
> + */
> +void sdv_list_free(struct sdv_list *list)
> +{
> + struct sdv_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * free a pexpr_list (and pexpr_put the elements)
> + */
> +void pexpr_list_free_put(struct pexpr_list *list)
> +{
> + struct pexpr_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + pexpr_put(node->elem);
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * free a prop_list
> + */
> +void prop_list_free(struct prop_list *list)
> +{
> + struct prop_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * free a sym_list
> + */
> +void sym_list_free(struct sym_list *list)
> +{
> + struct sym_node *node = list->head, *tmp;
> +
> + while (node != NULL) {
> + tmp = node->next;
> + free(node);
> + node = tmp;
> + }
> +
> + free(list);
> +}
> +
> +/*
> + * simplify a pexpr in-place
> + * pexpr && False -> False
> + * pexpr && True -> pexpr
> + * pexpr || False -> pexpr
> + * pexpr || True -> True
> + */
> +static void pexpr_eliminate_yn(struct pexpr *e, struct cfdata *data)
> +{
> + struct pexpr *tmp;
> + unsigned int ref_count;
> +
> + if (!e)
> + return;
> +
> + switch (e->type) {
> + case PE_AND:
> + pexpr_eliminate_yn(e->left.pexpr, data);
> + pexpr_eliminate_yn(e->right.pexpr, data);
> + if (e->left.pexpr->type == PE_SYMBOL) {
> + if (e->left.pexpr->left.fexpr == data->constants->const_false) {
> + pexpr_put(e->left.pexpr);
> + pexpr_put(e->right.pexpr);
> + ref_count = e->ref_count;
> + pexpr_construct_sym(
> + e, data->constants->const_false,
> + ref_count);
> + return;
> + } else if (e->left.pexpr->left.fexpr == data->constants->const_true) {
> + pexpr_put(e->left.pexpr);
> + tmp = e->right.pexpr;
> + ref_count = e->ref_count;
> + pexpr_shallow_copy(e, tmp, ref_count);
> + pexpr_put(tmp);
> + return;
> + }
> + }
> + if (e->right.pexpr->type == PE_SYMBOL) {
> + if (e->right.pexpr->left.fexpr == data->constants->const_false) {
> + pexpr_put(e->left.pexpr);
> + pexpr_put(e->right.pexpr);
> + ref_count = e->ref_count;
> + pexpr_construct_sym(
> + e, data->constants->const_false,
> + ref_count);
> + return;
> + } else if (e->right.pexpr->left.fexpr == data->constants->const_true) {
> + pexpr_put(e->right.pexpr);
> + tmp = e->left.pexpr;
> + ref_count = e->ref_count;
> + pexpr_shallow_copy(e, tmp, ref_count);
> + pexpr_put(tmp);
> + return;
> + }
> + }
> + break;
> + case PE_OR:
> + pexpr_eliminate_yn(e->left.pexpr, data);
> + pexpr_eliminate_yn(e->right.pexpr, data);
> + if (e->left.pexpr->type == PE_SYMBOL) {
> + if (e->left.pexpr->left.fexpr == data->constants->const_false) {
> + pexpr_put(e->left.pexpr);
> + tmp = e->right.pexpr;
> + ref_count = e->ref_count;
> + pexpr_shallow_copy(e, tmp, ref_count);
> + pexpr_put(tmp);
> + return;
> + } else if (e->left.pexpr->left.fexpr == data->constants->const_true) {
> + pexpr_put(e->left.pexpr);
> + pexpr_put(e->right.pexpr);
> + ref_count = e->ref_count;
> + pexpr_construct_sym(
> + e, data->constants->const_true,
> + ref_count);
> + return;
> + }
> + }
> + if (e->right.pexpr->type == PE_SYMBOL) {
> + if (e->right.pexpr->left.fexpr == data->constants->const_false) {
> + pexpr_put(e->right.pexpr);
> + tmp = e->left.pexpr;
> + ref_count = e->ref_count;
> + pexpr_shallow_copy(e, tmp, ref_count);
> + pexpr_put(tmp);
> + return;
> + } else if (e->right.pexpr->left.fexpr == data->constants->const_true) {
> + pexpr_put(e->left.pexpr);
> + pexpr_put(e->right.pexpr);
> + ref_count = e->ref_count;
> + pexpr_construct_sym(e,
> + data->constants->const_true,
> + ref_count);
> + return;
> + }
> + }
> + default:
> + break;
> + }
> +}
> +
> +static void pexpr_shallow_copy(struct pexpr *dest, struct pexpr *org, unsigned int ref_count)
> +{
> + struct pexpr inter;
> +
> + inter.type = org->type;
> + inter.left = org->left;
> + inter.right = org->right;
> + if (org->type == PE_OR || org->type == PE_AND) {
> + pexpr_get(org->left.pexpr);
> + pexpr_get(org->right.pexpr);
> + } else if (org->type == PE_NOT) {
> + pexpr_get(org->left.pexpr);
> + }
> + inter.ref_count = ref_count;
> + *dest = inter;
> +}
> +
> +/*
> + * copy a pexpr
> + */
> +struct pexpr *pexpr_deep_copy(const struct pexpr *org)
> +{
> + struct pexpr *e;
> +
> + if (!org)
> + return NULL;
> +
> + e = xmalloc(sizeof(*org));
> + memcpy(e, org, sizeof(*org));
> + e->ref_count = 1;
> + switch (org->type) {
> + case PE_SYMBOL:
> + e->left = org->left;
> + break;
> + case PE_AND:
> + case PE_OR:
> + e->left.pexpr = pexpr_deep_copy(org->left.pexpr);
> + e->right.pexpr = pexpr_deep_copy(org->right.pexpr);
> + break;
> + case PE_NOT:
> + e->left.pexpr = pexpr_deep_copy(org->left.pexpr);
> + break;
> + }
> +
> + return e;
> +}
> +
> +/*
> + * free a pexpr
> + */
> +void pexpr_free_depr(struct pexpr *e)
> +{
> + if (!e)
> + return;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + break;
> + case PE_AND:
> + case PE_OR:
> + pexpr_free_depr(e->left.pexpr);
> + pexpr_free_depr(e->right.pexpr);
> + break;
> + case PE_NOT:
> + pexpr_free_depr(e->left.pexpr);
> + break;
> + }
> +
> + free(e);
> +}
> +
> +/*
> + * Increments ref_count and returns @e
> + */
> +struct pexpr *pexpr_get(struct pexpr *e)
> +{
> + ++e->ref_count;
> + return e;
> +}
> +
> +/*
> + * Decrements ref_count and if it becomes 0, it recursively puts the references
> + * to its children and calls ``free(e)``. If @e == NULL, it does nothing.
> + */
> +void pexpr_put(struct pexpr *e)
> +{
> + if (!e)
> + return;
> +
> + if (e->ref_count == 0) {
> + printd("Invalid call to %s - ref_count is zero\n", __func__);
> + return;
> + }
> +
> + --e->ref_count;
> + if (e->ref_count > 0)
> + return;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + break;
> + case PE_AND:
> + case PE_OR:
> + pexpr_put(e->left.pexpr);
> + pexpr_put(e->right.pexpr);
> + break;
> + case PE_NOT:
> + pexpr_put(e->left.pexpr);
> + break;
> + }
> +
> + free(e);
> +}
> +
> +/*
> + * calls pexpr_put for a NULL-terminated array of struct pexpr *
> + */
> +void _pexpr_put_list(struct pexpr **es)
> +{
> + for (; *es != NULL; es++)
> + pexpr_put(*es);
> +}
> +
> +#define e1 (*ep1)
> +#define e2 (*ep2)
> +/*
> + * pexpr_eliminate_eq() helper
> + */
> +static void __pexpr_eliminate_eq(enum pexpr_type type, struct pexpr **ep1, struct pexpr **ep2,
> + struct cfdata *data)
> +{
> + /* recurse down to the leaves */
> + if (e1->type == type) {
> + __pexpr_eliminate_eq(type, &e1->left.pexpr, &e2, data);
> + __pexpr_eliminate_eq(type, &e1->right.pexpr, &e2, data);
> + return;
> + }
> + if (e2->type == type) {
> + __pexpr_eliminate_eq(type, &e1, &e2->left.pexpr, data);
> + __pexpr_eliminate_eq(type, &e1, &e2->right.pexpr, data);
> + return;
> + }
> +
> + /* e1 and e2 are leaves. Compare them. */
> + if (e1->type == PE_SYMBOL && e2->type == PE_SYMBOL &&
> + e1->left.fexpr->satval == e2->left.fexpr->satval &&
> + (e1->left.fexpr == data->constants->const_true ||
> + e2->left.fexpr == data->constants->const_false))
> + return;
> + if (!pexpr_eq(e1, e2, data))
> + return;
> +
> + /* e1 and e2 are equal leaves. Prepare them for elimination. */
> + trans_count++;
> + pexpr_put(e1);
> + pexpr_put(e2);
> + switch (type) {
> + case PE_AND:
> + e1 = pexf(data->constants->const_true);
> + e2 = pexf(data->constants->const_true);
> + break;
> + case PE_OR:
> + e1 = pexf(data->constants->const_false);
> + e2 = pexf(data->constants->const_false);
> + break;
> + default:
> + break;
> + }
> +}
> +
> +/*
> + * rewrite pexpr ep1 and ep2 to remove operands common to both
> + */
> +static void pexpr_eliminate_eq(struct pexpr **ep1, struct pexpr **ep2, struct cfdata *data)
> +{
> + if (!e1 || !e2)
> + return;
> +
> + switch (e1->type) {
> + case PE_AND:
> + case PE_OR:
> + __pexpr_eliminate_eq(e1->type, ep1, ep2, data);
> + default:
> + break;
> + }
> + if (e1->type != e2->type)
> + switch (e2->type) {
> + case PE_AND:
> + case PE_OR:
> + __pexpr_eliminate_eq(e2->type, ep1, ep2, data);
> + default:
> + break;
> + }
> + pexpr_eliminate_yn(e1, data);
> + pexpr_eliminate_yn(e2, data);
> +}
> +#undef e1
> +#undef e2
> +
> +/*
> + * check whether 2 pexpr are equal
> + */
> +bool pexpr_eq(struct pexpr *e1, struct pexpr *e2, struct cfdata *data)
> +{
> + bool res;
> + int old_count;
> +
> + if (!e1 || !e2)
> + return false;
> +
> + if (e1->type != e2->type)
> + return false;
> +
> + switch (e1->type) {
> + case PE_SYMBOL:
> + return e1->left.fexpr->satval == e2->left.fexpr->satval;
> + case PE_AND:
> + case PE_OR:
> + e1 = pexpr_deep_copy(e1);
> + e2 = pexpr_deep_copy(e2);
> + old_count = trans_count;
> + pexpr_eliminate_eq(&e1, &e2, data);
> + res = (e1->type == PE_SYMBOL && e2->type == PE_SYMBOL &&
> + e1->left.fexpr->satval == e2->left.fexpr->satval);
> + pexpr_put(e1);
> + pexpr_put(e2);
> + trans_count = old_count;
> + return res;
> + case PE_NOT:
> + return pexpr_eq(e1->left.pexpr, e2->left.pexpr, data);
> + }
> +
> + return false;
> +}
> +
> +/*
> + * print a pexpr
> + */
> +static void pexpr_print_util(struct pexpr *e, int prevtoken)
> +{
> + if (!e)
> + return;
> +
> + switch (e->type) {
> + case PE_SYMBOL:
> + printf("%s", str_get(&e->left.fexpr->name));
> + break;
> + case PE_AND:
> + if (prevtoken != PE_AND && prevtoken != -1)
> + printf("(");
> + pexpr_print_util(e->left.pexpr, PE_AND);
> + printf(" && ");
> + pexpr_print_util(e->right.pexpr, PE_AND);
> + if (prevtoken != PE_AND && prevtoken != -1)
> + printf(")");
> + break;
> + case PE_OR:
> + if (prevtoken != PE_OR && prevtoken != -1)
> + printf("(");
> + pexpr_print_util(e->left.pexpr, PE_OR);
> + printf(" || ");
> + pexpr_print_util(e->right.pexpr, PE_OR);
> + if (prevtoken != PE_OR && prevtoken != -1)
> + printf(")");
> + break;
> + case PE_NOT:
> + printf("!");
> + pexpr_print_util(e->left.pexpr, PE_NOT);
> + break;
> + }
> +}
> +void pexpr_print(char *tag, struct pexpr *e, int prevtoken)
> +{
> + printf("%s: ", tag);
> + pexpr_print_util(e, prevtoken);
> + printf("\n");
> +}
> +
> +/*
> + * convert a fexpr to a pexpr
> + */
> +struct pexpr *pexf(struct fexpr *fe)
Not only this one, but more descriptive function name please.
"pexf", so what?
I do not understand what it is doing from the name.
> +{
> + struct pexpr *pe = xcalloc(1, sizeof(*pe));
> +
> + pexpr_construct_sym(pe, fe, 1);
> + return pe;
> +}
> +
> +void pexpr_construct_or(struct pexpr *e, struct pexpr *left,
> + struct pexpr *right, unsigned int ref_count)
> +{
> + e->type = PE_OR;
> + e->left.pexpr = left;
> + e->right.pexpr = right;
> + e->ref_count = ref_count;
> +}
> +
> +void pexpr_construct_and(struct pexpr *e, struct pexpr *left,
> + struct pexpr *right, unsigned int ref_count)
> +{
> + e->type = PE_AND;
> + e->left.pexpr = left;
> + e->right.pexpr = right;
> + e->ref_count = ref_count;
> +}
> +
> +void pexpr_construct_not(struct pexpr *e, struct pexpr *left,
> + unsigned int ref_count)
> +{
> + e->type = PE_NOT;
> + e->left.pexpr = left;
> + e->right.pexpr = NULL;
> + e->ref_count = ref_count;
> +}
> +
> +void pexpr_construct_sym(struct pexpr *e, struct fexpr *left,
> + unsigned int ref_count)
> +{
> + e->type = PE_SYMBOL;
> + e->left.fexpr = left;
> + e->right.pexpr = NULL;
> + e->ref_count = ref_count;
> +}
> +
> +static struct pexpr *pexpr_join_or(struct pexpr *e1, struct pexpr *e2, struct cfdata *data)
> +{
> + if (pexpr_eq(e1, e2, data))
> + return pexpr_deep_copy(e1);
> + else
> + return NULL;
> +}
> +
> +static struct pexpr *pexpr_join_and(struct pexpr *e1, struct pexpr *e2, struct cfdata *data)
> +{
> + if (pexpr_eq(e1, e2, data))
> + return pexpr_deep_copy(e1);
> + else
> + return NULL;
> +}
> +
> +/*
> + * pexpr_eliminate_dups() helper.
> + */
> +static void pexpr_eliminate_dups1(enum pexpr_type type, struct pexpr **ep1, struct pexpr **ep2,
> + struct cfdata *data)
> +{
> +#define e1 (*ep1)
> +#define e2 (*ep2)
> +
> + struct pexpr *tmp;
> +
> + /* recurse down to leaves */
> + if (e1->type == type) {
> + pexpr_eliminate_dups1(type, &e1->left.pexpr, &e2, data);
> + pexpr_eliminate_dups1(type, &e1->right.pexpr, &e2, data);
> + return;
> + }
> + if (e2->type == type) {
> + pexpr_eliminate_dups1(type, &e1, &e2->left.pexpr, data);
> + pexpr_eliminate_dups1(type, &e1, &e2->right.pexpr, data);
> + return;
> + }
> +
> + /* e1 and e2 are leaves. Compare them. */
> +
> + if (e1 == e2)
> + return;
> +
> + switch (e1->type) {
> + case PE_AND:
> + case PE_OR:
> + pexpr_eliminate_dups1(e1->type, &e1, &e1, data);
> + default:
> + break;
> + }
> +
> + switch (type) {
> + case PE_AND:
> + tmp = pexpr_join_and(e1, e2, data);
> + if (tmp) {
> + pexpr_put(e1);
> + pexpr_put(e2);
> + e1 = pexf(data->constants->const_true);
> + e2 = tmp;
> + trans_count++;
> + }
> + break;
> + case PE_OR:
> + tmp = pexpr_join_or(e1, e2, data);
> + if (tmp) {
> + pexpr_put(e1);
> + pexpr_put(e2);
> + e1 = pexf(data->constants->const_false);
> + e2 = tmp;
> + trans_count++;
> + }
> + break;
> + default:
> + break;
> + }
> +
> +#undef e1
> +#undef e2
> +}
> +
> +/*
> + * eliminate duplicate and redundant operands
> + */
> +struct pexpr *pexpr_eliminate_dups(struct pexpr *e, struct cfdata *data)
> +{
> + int oldcount;
> +
> + if (!e)
> + return e;
> +
> + oldcount = trans_count;
> + while (true) {
> + trans_count = 0;
> + switch (e->type) {
> + case PE_AND:
> + case PE_OR:
> + pexpr_eliminate_dups1(e->type, &e, &e, data);
> + default:
> + break;
> + }
> + if (!trans_count)
> + /* no simplification done in this pass. We're done. */
> + break;
> + pexpr_eliminate_yn(e, data);
> + }
> + trans_count = oldcount;
> + return e;
> +}
This is a full copy-paste of scripts/kconfig/expr.c
If you need all of these, please referector
to avoid code duplication.
> diff --git a/scripts/kconfig/cf_expr.h b/scripts/kconfig/cf_expr.h
> new file mode 100644
> index 000000000000..07435ae381e6
> --- /dev/null
> +++ b/scripts/kconfig/cf_expr.h
> @@ -0,0 +1,296 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Copyright (C) 2023 Patrick Franz <deltaone@xxxxxxxxxx>
> + */
> +
> +#ifndef CF_EXPR_H
> +#define CF_EXPR_H
> +
> +#include <stdbool.h>
> +
> +#include "cf_defs.h"(
> +
> +#define fexpr_list_for_each(node, list) \
> + for (node = list->head; node != NULL; node = node->next)
> +
> +#define fexl_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define pexpr_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define sdv_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define sfix_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define sfl_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define sym_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define defm_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
> +
> +#define prop_list_for_each(node, list) \
> + fexpr_list_for_each(node, list)
All of these are the same as fexpr_list_for_each(),
which is the same as list_for_each().
kconfig already use list.h
Please do not proliferate similar code.
> +
> +/* call pexpr_put for a list of pexpr's */
> +#define PEXPR_PUT(...) _pexpr_put_list((struct pexpr *[]){ __VA_ARGS__, NULL })
> +
> +/* create a fexpr */
> +struct fexpr *fexpr_create(int satval, enum fexpr_type type, char *name);
> +
> +/* create the fexpr for a symbol */
> +void sym_create_fexpr(struct symbol *sym, struct cfdata *data);
> +
> +struct pexpr *expr_calculate_pexpr_both(struct expr *e, struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y(struct expr *e, struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_m(struct expr *e, struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y_and(struct expr *a, struct expr *b,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_m_and(struct expr *a, struct expr *b,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_both_and(struct expr *a, struct expr *b,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y_or(struct expr *a, struct expr *b,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_m_or(struct expr *a, struct expr *b,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_both_or(struct expr *a, struct expr *b,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y_not(struct expr *e, struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_m_not(struct expr *e, struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y_equals(struct expr *e,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y_unequals(struct expr *e,
> + struct cfdata *data);
> +struct pexpr *expr_calculate_pexpr_y_comp(struct expr *e, struct cfdata *data);
> +
> +/* macro to create a pexpr of type AND */
> +struct pexpr *pexpr_and_share(struct pexpr *a, struct pexpr *b,
> + struct cfdata *data);
> +struct pexpr *pexpr_and(struct pexpr *a, struct pexpr *b, struct cfdata *data,
> + enum pexpr_move move);
> +
> +/* macro to create a pexpr of type OR */
> +struct pexpr *pexpr_or_share(struct pexpr *a, struct pexpr *b,
> + struct cfdata *data);
> +struct pexpr *pexpr_or(struct pexpr *a, struct pexpr *b, struct cfdata *data,
> + enum pexpr_move move);
> +
> +/* macro to create a pexpr of type NOT */
> +struct pexpr *pexpr_not_share(struct pexpr *a, struct cfdata *data);
> +struct pexpr *pexpr_not(struct pexpr *a, struct cfdata *data);
> +
> +/* check whether a pexpr is in CNF */
> +bool pexpr_is_cnf(struct pexpr *e);
> +
> +/* check whether a pexpr is in NNF */
> +bool pexpr_is_nnf(struct pexpr *e);
> +
> +/* return fexpr_both for a symbol */
> +struct pexpr *sym_get_fexpr_both(struct symbol *sym, struct cfdata *data);
> +
> +/* return fexpr_sel_both for a symbol */
> +struct pexpr *sym_get_fexpr_sel_both(struct symbol *sym, struct cfdata *data);
> +
> +/* create the fexpr of a non-boolean symbol for a specific value */
> +struct fexpr *sym_create_nonbool_fexpr(struct symbol *sym, char *value,
> + struct cfdata *data);
> +
> +/*
> + * return the fexpr of a non-boolean symbol for a specific value, NULL if
> + * non-existent
> + */
> +struct fexpr *sym_get_nonbool_fexpr(struct symbol *sym, char *value);
> +
> +/*
> + * return the fexpr of a non-boolean symbol for a specific value, if it exists
> + * otherwise create it
> + */
> +struct fexpr *sym_get_or_create_nonbool_fexpr(struct symbol *sym, char *value, struct cfdata *data);
> +
> +/* macro to construct a pexpr for "A implies B" */
> +struct pexpr *pexpr_implies_share(struct pexpr *a, struct pexpr *b, struct cfdata *data);
> +struct pexpr *pexpr_implies(struct pexpr *a, struct pexpr *b, struct cfdata *data,
> + enum pexpr_move move);
> +
> +/* check, if the fexpr is a symbol, a True/False-constant, a literal symbolising a non-boolean or
> + * a choice symbol
> + */
> +bool fexpr_is_symbol(struct fexpr *e);
> +
> +/* check whether a pexpr is a symbol or a negated symbol */
> +bool pexpr_is_symbol(struct pexpr *e);
> +
> +/* check whether the fexpr is a constant (true/false) */
> +bool fexpr_is_constant(struct fexpr *e, struct cfdata *data);
> +
> +/* add a fexpr to the satmap */
> +void fexpr_add_to_satmap(struct fexpr *e, struct cfdata *data);
> +
> +/* print an fexpr */
> +void fexpr_print(char *tag, struct fexpr *e);
> +
> +/* write an fexpr into a string (format needed for testing) */
> +void fexpr_as_char(struct fexpr *e, struct gstr *s);
> +
> +/* write pn pexpr into a string */
> +void pexpr_as_char_short(struct pexpr *e, struct gstr *s, int parent);
> +
> +/* write an fexpr into a string (format needed for testing) */
> +void pexpr_as_char(struct pexpr *e, struct gstr *s, int parent, struct cfdata *data);
> +
> +/* check whether a pexpr contains a specific fexpr */
> +bool pexpr_contains_fexpr(struct pexpr *e, struct fexpr *fe);
> +
> +/* init list of fexpr */
> +struct fexpr_list *fexpr_list_init(void);
> +
> +/* init list of fexpr_list */
> +struct fexl_list *fexl_list_init(void);
> +
> +/* init list of pexpr */
> +struct pexpr_list *pexpr_list_init(void);
> +
> +/* init list of symbol_fix */
> +struct sfix_list *sfix_list_init(void);
> +
> +/* init list of sfix_list */
> +struct sfl_list *sfl_list_init(void);
> +
> +/* init list of symbol_dvalue */
> +struct sdv_list *sdv_list_init(void);
> +
> +/* init list of symbols */
> +struct sym_list *sym_list_init(void);
> +
> +/* init list of default_maps */
> +struct defm_list *defm_list_init(void);
> +
> +/* init list of properties */
> +struct prop_list *prop_list_init(void);
> +
> +/* add element to tail of a fexpr_list */
> +void fexpr_list_add(struct fexpr_list *list, struct fexpr *fe);
> +
> +/* add element to tail of a fexl_list */
> +void fexl_list_add(struct fexl_list *list, struct fexpr_list *elem);
> +
> +/* add element to tail of a pexpr_list */
> +void pexpr_list_add(struct pexpr_list *list, struct pexpr *e);
> +
> +/* add element to tail of a sfix_list */
> +void sfix_list_add(struct sfix_list *list, struct symbol_fix *fix);
> +
> +/* add element to tail of a sfl_list */
> +void sfl_list_add(struct sfl_list *list, struct sfix_list *elem);
> +
> +/* add element to tail of a sdv_list */
> +void sdv_list_add(struct sdv_list *list, struct symbol_dvalue *sdv);
> +
> +/* add element to tail of a sym_list */
> +void sym_list_add(struct sym_list *list, struct symbol *sym);
> +
> +/* add element to tail of a defm_list */
> +void defm_list_add(struct defm_list *list, struct default_map *map);
> +
> +/* add element to tail of a prop_list */
> +void prop_list_add(struct prop_list *list, struct property *prop);
> +
> +/* delete an element from a fexpr_list */
> +void fexpr_list_delete(struct fexpr_list *list, struct fexpr_node *node);
> +
> +/* delete an element from a fexpr_list */
> +void fexl_list_delete(struct fexl_list *list, struct fexl_node *node);
> +
> +/* delete the first occurrence of elem in an fexl_list */
> +void fexl_list_delete_elem(struct fexl_list *list, struct fexpr_list *elem);
> +
> +/* delete an element from a pexpr_list */
> +void pexpr_list_delete(struct pexpr_list *list, struct pexpr_node *node);
> +
> +/* delete an element from a sfix_list */
> +void sfix_list_delete(struct sfix_list *list, struct sfix_node *node);
> +
> +/* make a shallow copy of a fexpr_list */
> +struct fexpr_list *fexpr_list_copy(struct fexpr_list *list);
> +
> +/* make a shallow copy of a fexpr_list */
> +struct fexl_list *fexl_list_copy(struct fexl_list *list);
> +
> +/* make a shallow copy of a sdv_list */
> +struct sdv_list *sdv_list_copy(struct sdv_list *list);
> +
> +/* make a shallow copy of a sfix_list */
> +struct sfix_list *sfix_list_copy(struct sfix_list *list);
> +
> +/* print a fexpr_list */
> +void fexpr_list_print(char *title, struct fexpr_list *list);
> +
> +/* print a fexl_list */
> +void fexl_list_print(char *title, struct fexl_list *list);
> +
> +/* print a pexpr_list */
> +void pexpr_list_print(char *title, struct pexpr_list *list);
> +
> +/* free an fexpr_list */
> +void fexpr_list_free(struct fexpr_list *list);
> +
> +/* free an pexpr_list (and pexpr_put the elements) */
> +void pexpr_list_free_put(struct pexpr_list *list);
> +
> +/* free an fexl_list */
> +void fexl_list_free(struct fexl_list *list);
> +
> +/* free a sdv_list */
> +void sdv_list_free(struct sdv_list *list);
> +
> +/* free a prop_list */
> +void prop_list_free(struct prop_list *list);
> +
> +/* free a defm_list (and pexpr_put the conditions of the maps) */
> +void defm_list_destruct(struct defm_list *list);
> +
> +/* free a sym_list */
> +void sym_list_free(struct sym_list *list);
> +
> +/* check whether 2 pexpr are equal */
> +bool pexpr_eq(struct pexpr *e1, struct pexpr *e2, struct cfdata *data);
> +
> +/* copy a pexpr */
> +struct pexpr *pexpr_deep_copy(const struct pexpr *org);
> +
> +void pexpr_construct_sym(struct pexpr *e, struct fexpr *left,
> + unsigned int ref_count);
> +void pexpr_construct_not(struct pexpr *e, struct pexpr *left,
> + unsigned int ref_count);
> +void pexpr_construct_and(struct pexpr *e, struct pexpr *left,
> + struct pexpr *right, unsigned int ref_count);
> +void pexpr_construct_or(struct pexpr *e, struct pexpr *left,
> + struct pexpr *right, unsigned int ref_count);
> +
> +/* free a pexpr */
> +void pexpr_free_depr(struct pexpr *e);
> +
> +/* give up a reference to e. Also see struct pexpr. */
> +void pexpr_put(struct pexpr *e);
> +/* Used by PEXPR_PUT(). Not to be used directly. */
> +void _pexpr_put_list(struct pexpr **es);
> +
> +/* acquire a reference to e. Also see struct pexpr. */
> +struct pexpr *pexpr_get(struct pexpr *e);
> +
> +/* print a pexpr */
> +void pexpr_print(char *tag, struct pexpr *e, int prevtoken);
> +
> +/* convert a fexpr to a pexpr */
> +struct pexpr *pexf(struct fexpr *fe);
> +
> +/* eliminate duplicate and redundant operands */
> +struct pexpr *pexpr_eliminate_dups(struct pexpr *e, struct cfdata *data);
> +
> +#endif
> --
> 2.39.2
>
--
Best Regards
Masahiro Yamada
