| Message ID | 20240710065255.10338-8-ole0811sch@gmail.com (mailing list archive) |
|---|---|
| State | New |
| Headers | show |
| Series | kconfig: Add support for conflict resolution | expand |
On Wed, Jul 10, 2024 at 3:54 PM Ole Schuerks <ole0811sch@gmail.com> 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@debian.org> > Signed-off-by: Patrick Franz <deltaone@debian.org> > Co-developed-by: Ibrahim Fayaz <phayax@gmail.com> > Signed-off-by: Ibrahim Fayaz <phayax@gmail.com> > Reviewed-by: Luis Chamberlain <mcgrof@kernel.org> > Tested-by: Evgeny Groshev <eugene.groshev@gmail.com> > Suggested-by: Sarah Nadi <nadi@ualberta.ca> > Suggested-by: Thorsten Berger <thorsten.berger@rub.de> > Signed-off-by: Thorsten Berger <thorsten.berger@rub.de> > Signed-off-by: Ole Schuerks <ole0811sch@gmail.com> > --- > 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@debian.org> > + */ > + > +#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@debian.org> > + */ > + > +#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
On 8/12/24 10:46, Masahiro Yamada wrote: > On Wed, Jul 10, 2024 at 3:54 PM Ole Schuerks <ole0811sch@gmail.com> 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@debian.org> >> Signed-off-by: Patrick Franz <deltaone@debian.org> >> Co-developed-by: Ibrahim Fayaz <phayax@gmail.com> >> Signed-off-by: Ibrahim Fayaz <phayax@gmail.com> >> Reviewed-by: Luis Chamberlain <mcgrof@kernel.org> >> Tested-by: Evgeny Groshev <eugene.groshev@gmail.com> >> Suggested-by: Sarah Nadi <nadi@ualberta.ca> >> Suggested-by: Thorsten Berger <thorsten.berger@rub.de> >> Signed-off-by: Thorsten Berger <thorsten.berger@rub.de> >> Signed-off-by: Ole Schuerks <ole0811sch@gmail.com> >> --- >> 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 >> +/* >> + * 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. > > Could you give us one or two examples of what other functions have bad names? I didn't find anything as bad as pexf() so I'm not sure what the expectations are. Thank you, that would be helpful.
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@debian.org> + */ + +#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)); + + 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; +} + +/* + * 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; +} + +/* + * 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++; +} + +/* + * 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) +{ + 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; +} 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@debian.org> + */ + +#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) + +/* 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