kconfig_parser rewritten and now supports revers dependency

Most of the kconfig_parser is changed.
Now dependency are not copied before transfer to CNF and CNF expression is direcly extracted from kconfíg parsed output structures.

9 files changed, 821 insertions, 110 deletions

diff --git a/programs/src/kconfig_parser/Makefile b/programs/src/kconfig_parser/Makefile
index d8babae..6aee15d 100644
--- a/programs/src/kconfig_parser/Makefile
+++ b/programs/src/kconfig_parser/Makefile
@@ -5,7 +5,7 @@ all: ../../kconfig_parser
 
 INPUT_FILES  = kconfig_parser.c
 INPUT_FILES += kconfig/zconf.tab.c \
-			   boolexp.c \
+			   cnfexpr.c \
 			   symlist.c \
 			   output.c
 CFLAGS = -O0 -w -ggdb
diff --git a/programs/src/kconfig_parser/boolexp.c b/programs/src/kconfig_parser/boolexp.c
index a41937a..c39b79c 100644
--- a/programs/src/kconfig_parser/boolexp.c
+++ b/programs/src/kconfig_parser/boolexp.c
@@ -54,6 +54,373 @@ struct boolexp *copy_kconfig_dep(struct symlist *sl, struct expr *expr) {
     }
 }
 
+struct boolexp *copy_kconfig_f_dep(struct symlist *sl, struct expr *expr) {
+    switch (expr->type) {
+    case E_OR:
+        printf("OR\n");
+        copy_kconfig_f_dep(sl, expr->left.expr);
+        copy_kconfig_f_dep(sl, expr->right.expr);
+        break;
+    case E_AND:
+        printf("AND\n");
+        copy_kconfig_f_dep(sl, expr->left.expr);
+        copy_kconfig_f_dep(sl, expr->right.expr);
+        break;
+    case E_NOT:
+        printf("NOT\n");
+        copy_kconfig_f_dep(sl, expr->left.expr);
+        break;
+    case E_EQUAL:
+        printf("= ");
+        printf("%s ", expr->left.sym->name);
+        if (!strcmp("y", expr->right.sym->name))
+            printf("YES\n");
+        else if (!strcmp("n", expr->right.sym->name))
+            printf("NO\n");
+        else
+            printf("PROBLEM\n");
+        break;
+    case E_UNEQUAL:
+        printf("!= ");
+        printf("%s ", expr->left.sym->name);
+        if (!strcmp("y", expr->right.sym->name))
+            printf("YES\n");
+        else if (!strcmp("n", expr->right.sym->name))
+            printf("NO\n");
+        else
+            printf("OTHER %s\n", expr->right.sym->name);
+        break;
+    case E_LIST:
+        printf("list\n");
+        break;
+    case E_SYMBOL:
+        printf("symbol\n");
+        break;
+    case E_RANGE:
+        printf("range\n");
+        break;
+    case E_NONE:
+        printf("none\n");
+        break;
+    default:
+        printf("ERROR\n");
+        break;
+    }
+
+}
+
+/*struct cnfexpr *kconfig_dep(struct symlist *sl, struct expr *expr) {
+    struct nd {
+        struct cnfexpr *cnfe;
+        struct expr *expr;
+    };
+    struct cnfexpr *ret = NULL;
+    struct nd *wlist;
+    int wlist_size = 2, wlist_pos = -1;
+    struct expr **backstack;
+    int backstack_size = 2, backstack_pos = -1;
+    bool neg = false;
+    int ng;
+
+    wlist = malloc((unsigned) wlist_size * sizeof(struct nd));
+    backstack = malloc((unsigned) backstack_size * sizeof(struct expr *));
+
+    while (expr != NULL) {
+        if (neg)
+            ng = -1;
+        else
+            ng = 1;
+        if ((backstack_pos >= 0 && backstack[backstack_pos] != expr)
+            || backstack_pos < 0) { // left
+            if (++backstack_pos >= backstack_size) {
+                backstack_size *= 2;
+                backstack =
+                    realloc(backstack,
+                            (unsigned) backstack_size *
+                            sizeof(struct expr *));
+            }
+            backstack[backstack_pos] = expr;
+            switch (expr->type) {
+            case E_SYMBOL:
+                ret = malloc(sizeof(struct cnfexpr));
+                ret->size = 1;
+                ret->sizes = malloc(sizeof(int));
+                ret->sizes[0] = 1;
+                ret->exprs = malloc(sizeof(int *));
+                ret->exprs[0] = malloc(sizeof(int));
+                ret->exprs[0][0] = ng * (int)
+                    symlist_find(sl, expr->left.sym->name)->id;
+                goto back;
+            case E_OR:
+            case E_AND:
+                if (expr->left.expr->type != E_SYMBOL)
+                    expr = expr->left.expr;
+                break;
+            case E_NOT:
+                neg = !neg;     // Is it working?
+                expr = expr->left.expr;
+                break;
+            case E_EQUAL:
+            case E_UNEQUAL:
+                ng = 1;
+                if (expr->type == E_UNEQUAL)
+                    ng *= -1;
+                if (!strcmp("y", expr->right.sym->name)) {
+                    // pass
+                } else if (!strcmp("n", expr->right.sym->name)) {
+                    ng *= -1;
+                } else if (!strcmp("m", expr->right.sym->name)) {
+                    ret = NULL;
+                    goto back;
+                } else {
+                    fprintf(stderr, "ERROR: kconfig_dep unknown equal\n");
+                    exit(1);
+                }
+                ret = malloc(sizeof(struct cnfexpr));
+                ret->size = 1;
+                ret->sizes = malloc(sizeof(unsigned));
+                ret->sizes[0] = 1;
+                ret->exprs = malloc(sizeof(int *));
+                ret->exprs[0] = malloc(sizeof(int));
+                ret->exprs[0][0] = ng *
+                    (int) symlist_find(sl, expr->left.sym->name)->id;
+                goto back;
+            default:
+                fprintf(stderr, "ERROR: kconfig_dep unknown left state\n");
+                exit(1);
+            }
+        } else {                // right
+            switch (expr->type) {
+            case E_OR:
+            case E_AND:
+                if (wlist_pos >= 0 && wlist[wlist_pos].expr == expr) {
+                    // navrat z prave strany v ret prava strana
+                    if (ret == NULL) {
+                        if ((!neg && expr->type == E_OR)
+                            || (neg && expr->type == E_AND)) {
+                            ret = wlist[wlist_pos--].cnfe;
+                        } else {
+                            struct cnfexpr *wcnf = wlist[wlist_pos--].cnfe;
+                            unsigned i;
+                            for (i = 0; i < wcnf->size; i++) {
+                                free(wcnf->exprs[i]);
+                            }
+                            free(wcnf->sizes);
+                            free(wcnf->exprs);
+                            free(wcnf);
+                        }
+                        goto back;
+                    }
+                    if ((!neg && expr->type == E_OR)
+                        || (neg && expr->type == E_AND)) {
+                        struct cnfexpr *wcnf = wlist[wlist_pos--].cnfe;
+                        unsigned oldsize = ret->size;
+                        ret->size *= wcnf->size;
+                        ret->sizes =
+                            realloc(ret->sizes, ret->size * sizeof(int));
+                        ret->exprs =
+                            realloc(ret->exprs, ret->size * sizeof(int *));
+                        unsigned i1, i2;
+                        for (i1 = 1; i1 < wcnf->size; i1++) {
+                            for (i2 = 0; i2 < oldsize; i2++) {
+                                ret->sizes[(i1 * oldsize) + i2] =
+                                    ret->sizes[i2];
+                                ret->exprs[(i1 * oldsize) + i2] =
+                                    malloc(ret->sizes[i2] * sizeof(int));
+                                memcpy(ret->exprs[(i1 * oldsize) + i2],
+                                       ret->exprs[i2],
+                                       ret->sizes[i2] * sizeof(int));
+                            }
+                        }
+                        for (i1 = 0; i1 < wcnf->size; i1++) {
+                            for (i2 = 0; i2 < oldsize; i2++) {
+                                unsigned offset =
+                                    ret->sizes[(i1 * oldsize) + i2];
+                                ret->sizes[(i1 * oldsize) + i2] +=
+                                    wcnf->sizes[i1];
+                                ret->exprs[(i1 * oldsize) + i2] =
+                                    realloc(ret->exprs
+                                            [(i1 * oldsize) + i2],
+                                            ret->sizes[(i1 * oldsize) +
+                                                       i2] * sizeof(int));
+                                memcpy(ret->exprs[(i1 * oldsize) + i2] +
+                                       offset, wcnf->exprs[i1],
+                                       wcnf->sizes[i1] * sizeof(int));
+                            }
+                        }
+                        for (i1 = 0; i1 < wcnf->size; i1++)
+                            free(wcnf->exprs[i1]);
+                        free(wcnf->sizes);
+                        free(wcnf->exprs);
+                        free(wcnf);
+                    } else {
+                        struct cnfexpr *wcnf = wlist[wlist_pos--].cnfe;
+                        unsigned oldsize = ret->size;
+                        ret->size += wcnf->size;
+                        ret->sizes =
+                            realloc(ret->sizes, ret->size * sizeof(int));
+                        ret->exprs =
+                            realloc(ret->exprs, ret->size * sizeof(int *));
+                        memcpy(ret->sizes + oldsize, wcnf->sizes,
+                               wcnf->size * sizeof(int));
+                        memcpy(ret->exprs + oldsize, wcnf->exprs,
+                               wcnf->size * sizeof(int *));
+                        free(wcnf->sizes);
+                        free(wcnf->exprs);
+                        free(wcnf);
+                    }
+                    goto back;
+                } else if (expr->left.expr->type == E_SYMBOL) {
+                    if (expr->right.expr->type != E_SYMBOL) {
+                        if (++wlist_pos >= wlist_size) {
+                            wlist_size *= 2;
+                            wlist =
+                                realloc(wlist,
+                                        (unsigned) wlist_size *
+                                        sizeof(struct nd));
+                        }
+                        wlist[wlist_pos].expr = expr;
+                        struct cnfexpr *w = malloc(sizeof(struct cnfexpr));
+                        w->size = 1;
+                        w->sizes = malloc(sizeof(int));
+                        w->sizes[0] = 1;
+                        w->exprs = malloc(sizeof(int *));
+                        w->exprs[0] = malloc(sizeof(int));
+                        w->exprs[0][0] = ng * (int)
+                            symlist_find(sl,
+                                         expr->left.expr->left.sym->
+                                         name)->id;
+                        wlist[wlist_pos].cnfe = w;
+                        expr = expr->right.expr;
+                    } else {
+                        ret = malloc(sizeof(struct cnfexpr));
+                        if ((!neg && expr->type == E_OR)
+                            || (neg && expr->type == E_AND)) {
+                            ret->size = 1;
+                            ret->sizes = malloc(sizeof(int));
+                            ret->sizes[0] = 2;
+                            ret->exprs = malloc(sizeof(int *));
+                            ret->exprs[0] = malloc(2 * sizeof(int));
+                            ret->exprs[0][0] = ng * (int)
+                                symlist_find(sl,
+                                             expr->left.expr->left.
+                                             sym->name)->id;
+                            ret->exprs[0][1] = ng * (int)
+                                symlist_find(sl,
+                                             expr->right.expr->left.
+                                             sym->name)->id;
+                        } else {
+                            ret->size = 2;
+                            ret->sizes = malloc(2 * sizeof(int));
+                            ret->sizes[0] = 1;
+                            ret->sizes[1] = 1;
+                            ret->exprs = malloc(2 * sizeof(int *));
+                            ret->exprs[0] = malloc(sizeof(int));
+                            ret->exprs[1] = malloc(sizeof(int));
+                            ret->exprs[0][0] =
+                                ng * (int) symlist_find(sl,
+                                                        expr->left.expr->
+                                                        left.sym->name)->
+                                id;
+                            ret->exprs[1][0] =
+                                ng * (int) symlist_find(sl,
+                                                        expr->right.expr->
+                                                        left.sym->name)->
+                                id;
+                        }
+                        goto back;
+                    }
+                } else if (ret != NULL) {
+                    if (expr->right.expr->type == E_SYMBOL) {
+                        if ((!neg && expr->type == E_OR)
+                            || (neg && expr->type == E_AND)) {
+                            unsigned i;
+                            for (i = 0; i < ret->size; i++) {
+                                ret->sizes[i]++;
+                                ret->exprs[i] =
+                                    realloc(ret->exprs[i],
+                                            ret->sizes[i] * sizeof(int));
+                                ret->exprs[i][ret->sizes[i] - 1] =
+                                    ng * (int)
+                                    symlist_find(sl,
+                                                 expr->right.expr->
+                                                 left.sym->name)->id;
+                            }
+                        } else {
+                            ret->size++;
+                            ret->exprs =
+                                realloc(ret->exprs,
+                                        ret->size * sizeof(int *));
+                            ret->exprs[ret->size - 1] =
+                                malloc(sizeof(int));
+                            ret->sizes =
+                                realloc(ret->sizes,
+                                        ret->size * sizeof(int));
+                            ret->sizes[ret->size - 1] = 1;
+                            ret->exprs[ret->size - 1][0] =
+                                ng * (int) symlist_find(sl,
+                                                        expr->right.
+                                                        expr->left.sym->
+                                                        name)->id;
+                        }
+                        goto back;
+                    } else {
+                        if (++wlist_pos >= wlist_size) {
+                            wlist_size *= 2;
+                            wlist =
+                                realloc(wlist,
+                                        (unsigned) wlist_size *
+                                        sizeof(struct nd));
+                        }
+                        wlist[wlist_pos].cnfe = ret;
+                        wlist[wlist_pos].expr = expr;
+                        expr = expr->right.expr;
+                    }
+                } else {
+                    // navrat z leva, v lefo je false
+                    if (expr->right.expr->type == E_SYMBOL) {
+                        if ((!neg && expr->type == E_OR)
+                            || (neg && expr->type == E_AND)) {
+                        } else
+                            goto back;
+                    } else {
+                        if ((!neg && expr->type == E_OR)
+                            || (neg && expr->type == E_AND)) {
+                        } else {
+                        }
+                    }
+                }
+                break;
+            case E_NOT:
+                neg = !neg;
+                goto back;
+            default:
+                fprintf(stderr,
+                        "ERROR: kconfig_dep unknown right state\n");
+            }
+        }
+        continue;
+      back:
+        if (backstack_pos > 0) {
+            expr = backstack[--backstack_pos];
+        } else
+            expr = NULL;
+    }
+
+    return ret;
+}
+
+void cnfprint(struct cnfexpr *wcnf) {
+    unsigned i, r;
+    for (i = 0; i < wcnf->size; i++) {
+        for (r = 0; r < wcnf->sizes[i]; r++) {
+            printf("%d ", wcnf->exprs[i][r]);
+        }
+        printf("x ");
+    }
+    printf("\n");
+}*/
+
 // This function is leaking memory! TODO
 struct boolexp *boolexp_cnf(struct boolexp *be) {
     if (be->type == BE_NOT) {
@@ -64,7 +431,7 @@ struct boolexp *boolexp_cnf(struct boolexp *be) {
             nright = malloc(sizeof(struct boolexp));
             if (be->left.be->type == BE_OR)
                 root->type = BE_AND;
-            else if (be->left.be->type == BE_AND)
+            else
                 root->type = BE_OR;
             nleft->type = BE_NOT;
             nright->type = BE_NOT;
@@ -74,7 +441,7 @@ struct boolexp *boolexp_cnf(struct boolexp *be) {
             nright->left.be = be->right.be;
             be = root;
         }
-    } else if (be->type == BE_OR)
+    } else if (be->type == BE_OR) {
         if (be->left.be->type == BE_AND) {
             struct boolexp *root, *nleft, *nright;
             root = malloc(sizeof(struct boolexp));
@@ -106,6 +473,7 @@ struct boolexp *boolexp_cnf(struct boolexp *be) {
             nright->right.be = be->right.be->right.be;
             be = root;
         }
+    }
     if (be->type == BE_OR || be->type == BE_AND || be->type == BE_NOT)
         be->left.be = boolexp_cnf(be->left.be);
     if (be->type == BE_OR || be->type == BE_AND)
diff --git a/programs/src/kconfig_parser/boolexp.h b/programs/src/kconfig_parser/boolexp.h
index 2a73374..7f3aed6 100644
--- a/programs/src/kconfig_parser/boolexp.h
+++ b/programs/src/kconfig_parser/boolexp.h
@@ -21,7 +21,17 @@ struct boolexp {
     union boolexp_data left, right;
 };
 
+/*struct cnfexpr {
+    int **exprs;
+    unsigned *sizes;
+    unsigned size;
+};*/
+
+struct cnfexpr *kconfig_dep(struct symlist *sl, struct expr *expr);
+void cnfprint(struct cnfexpr *);
+
 struct boolexp *copy_kconfig_dep(struct symlist *sl, struct expr *expr);
+struct boolexp *copy_kconfig_f_dep(struct symlist *sl, struct expr *expr);
 struct boolexp *boolexp_cnf(struct boolexp *be);
 void boolexp_print(struct boolexp *be);
 
diff --git a/programs/src/kconfig_parser/cnfexpr.c b/programs/src/kconfig_parser/cnfexpr.c
new file mode 100644
index 0000000..50f0929
--- /dev/null
+++ b/programs/src/kconfig_parser/cnfexpr.c
@@ -0,0 +1,338 @@
+#include "cnfexpr.h"
+
+struct cnfexpr *cnf_sym(struct symlist *sl, bool not, struct symbol *sym);
+struct cnfexpr *cnf_eql(struct symlist *sl, bool not, struct symbol *sym1,
+                        struct symbol *sym2);
+struct cnfexpr *cnf_or(struct cnfexpr *e1, struct cnfexpr *e2);
+struct cnfexpr *cnf_and(struct cnfexpr *e1, struct cnfexpr *e2);
+void free_cnf(struct cnfexpr *e);
+
+struct cnfexpr *kconfig_cnfexpr(struct symlist *sl, struct expr *expr) {
+    struct stck {
+        struct expr *expr;
+        struct cnfexpr *cnf;
+    };
+    struct expr **back;
+    int back_size = 2, back_pos = -1;
+    back = malloc((unsigned) back_size * sizeof(struct expr *));
+    struct stck *stack;
+    int stack_size = 2, stack_pos = -1;
+    stack = malloc((unsigned) stack_size * sizeof(struct stck));
+    struct cnfexpr *rtrn = NULL;
+    bool nt = false;
+
+    while (expr != NULL) {
+        if ((back_pos >= 0 && back[back_pos] != expr) || back_pos < 0) {
+            if (++back_pos == back_size) {
+                back_size *= 2;
+                back =
+                    realloc(back,
+                            (unsigned) back_size * sizeof(struct expr *));
+            }
+            back[back_pos] = expr;
+        }
+        switch (expr->type) {
+        case E_SYMBOL:
+            rtrn = cnf_sym(sl, nt, expr->left.sym);
+            goto go_up;
+        case E_NOT:
+            nt = !nt;
+            if (rtrn == NULL)
+                expr = expr->left.expr;
+            else
+                goto go_up;
+            break;
+        case E_OR:
+        case E_AND:
+            if (stack_pos < 0 || stack[stack_pos].expr != expr) {
+                if (rtrn == NULL) {
+                    expr = expr->left.expr;
+                } else {
+                    if (stack_size == ++stack_pos) {
+                        stack_size *= 2;
+                        stack =
+                            realloc(stack,
+                                    (unsigned) stack_size *
+                                    sizeof(struct stck));
+                    }
+                    stack[stack_pos].expr = expr;
+                    stack[stack_pos].cnf = rtrn;
+                    expr = expr->right.expr;
+                    rtrn = NULL;
+                }
+            } else {
+                if ((!nt && expr->type == E_OR)
+                    || (nt && expr->type == E_AND))
+                    rtrn = cnf_or(stack[stack_pos].cnf, rtrn);
+                else
+                    rtrn = cnf_and(stack[stack_pos].cnf, rtrn);
+                stack_pos--;
+                goto go_up;
+            }
+            break;
+        case E_EQUAL:
+            rtrn = cnf_eql(sl, nt, expr->left.sym, expr->right.sym);
+            goto go_up;
+        case E_UNEQUAL:
+            rtrn = cnf_eql(sl, !nt, expr->left.sym, expr->right.sym);
+            goto go_up;
+        default:
+            fprintf(stderr, "ERROR: Unknown expression type.\n");
+        }
+        continue;
+
+      go_up:
+        if (--back_pos >= 0)
+            expr = back[back_pos];
+        else
+            expr = NULL;
+    }
+
+    free(back);
+    free(stack);
+    return rtrn;
+}
+
+void cnf_printf(struct cnfexpr *wcnf) {
+    if (wcnf == NULL) {
+        printf("hey NULL\n");
+        return;
+    }
+    switch (wcnf->type) {
+    case CT_TRUE:
+        printf("True\n");
+        return;
+    case CT_FALSE:
+        printf("False\n");
+        return;
+    case CT_EXPR:
+        break;
+    }
+    unsigned i, r;
+    for (i = 0; i < wcnf->size; i++) {
+        for (r = 0; r < wcnf->sizes[i]; r++) {
+            printf("%d ", wcnf->exprs[i][r]);
+        }
+        if (i < wcnf->size - 1)
+            printf("x ");
+    }
+    printf("\n");
+}
+
+struct cnfexpr *cnf_sym(struct symlist *sl, bool not, struct symbol *sym) {
+    struct cnfexpr *w = malloc(sizeof(struct cnfexpr));
+    struct symlist_el *se = symlist_find(sl, sym->name);
+    if (se == NULL) {
+        if (!not)
+            w->type = CT_FALSE;
+        else
+            w->type = CT_TRUE;
+    } else {
+        w->type = CT_EXPR;
+        w->size = 1;
+        w->sizes = malloc(sizeof(int));
+        w->sizes[0] = 1;
+        w->exprs = malloc(sizeof(int *));
+        w->exprs[0] = malloc(sizeof(int));
+        w->exprs[0][0] = (int) se->id;
+        if (not)
+            w->exprs[0][0] *= -1;
+    }
+    return w;
+}
+
+struct cnfexpr *cnf_eql(struct symlist *sl, bool not, struct symbol *sym1,
+                        struct symbol *sym2) {
+    if (!strcmp(sym2->name, "m")) {
+        struct cnfexpr *fls = malloc(sizeof(struct cnfexpr));
+        if (!not)
+            fls->type = CT_FALSE;
+        else
+            fls->type = CT_TRUE;
+        return fls;
+    }
+    if (!strcmp(sym2->name, "n")) {
+        struct cnfexpr *w = cnf_sym(sl, not, sym1);
+        w->exprs[0][0] *= -1;
+        return w;
+    }
+    if (!strcmp(sym2->name, "y")) {
+        return cnf_sym(sl, not, sym1);
+    }
+
+    struct cnfexpr *w1 = cnf_sym(sl, not, sym1);
+    struct cnfexpr *w2 = cnf_sym(sl, not, sym2);
+    struct cnfexpr *w3 = cnf_sym(sl, !not, sym1);
+    struct cnfexpr *w4 = cnf_sym(sl, !not, sym2);
+    struct cnfexpr *wa = cnf_or(w1, w2);
+    struct cnfexpr *wb = cnf_or(w3, w4);
+    struct cnfexpr *w = cnf_and(wa, wb);
+    return w;
+}
+
+struct cnfexpr *cnf_or(struct cnfexpr *e1, struct cnfexpr *e2) {
+    switch (e1->type) {
+    case CT_TRUE:
+        free_cnf(e2);
+        return e1;
+    case CT_FALSE:
+        free_cnf(e1);
+        return e2;
+    case CT_EXPR:
+        switch (e2->type) {
+        case CT_TRUE:
+            free_cnf(e1);
+            return e2;
+        case CT_FALSE:
+            free_cnf(e2);
+            return e1;
+        case CT_EXPR:
+            break;
+        }
+        break;
+    }
+
+    unsigned oldsize = e1->size;
+    e1->size *= e2->size;
+    e1->sizes = realloc(e1->sizes, e1->size * sizeof(int));
+    e1->exprs = realloc(e1->exprs, e1->size * sizeof(int *));
+    unsigned i1, i2;
+    // Duplicate e2->size times e1
+    for (i2 = 1; i2 < e2->size; i2++) {
+        memcpy(e1->sizes + (i2 * oldsize), e1->sizes,
+               oldsize * sizeof(int));
+        for (i1 = 0; i1 < oldsize; i1++) {
+            e1->exprs[(i2 * oldsize) + i1] =
+                malloc(e1->sizes[i1] * sizeof(int));
+            memcpy(e1->exprs[(i2 * oldsize) + i1], e1->exprs[i1],
+                   e1->sizes[i1] * sizeof(int));
+        }
+    }
+    unsigned oldsizes;
+    // Append e2->exprs to e1->exprs
+    for (i2 = 0; i2 < e2->size; i2++) {
+        for (i1 = 0; i1 < oldsize; i1++) {
+            oldsizes = e1->sizes[(i2 * oldsize) + i1];
+            e1->sizes[(i2 * oldsize) + i1] += e2->sizes[i2];
+            e1->exprs[(i2 * oldsize) + i1] =
+                realloc(e1->exprs[(i2 * oldsize) + i1],
+                        e1->sizes[(i2 * oldsize) + i1] * sizeof(int));
+            memcpy(e1->exprs[(i2 * oldsize) + i1] + oldsizes,
+                   e2->exprs[i2], e2->sizes[i2] * sizeof(int));
+        }
+    }
+    free_cnf(e2);
+    return e1;
+}
+
+struct cnfexpr *cnf_and(struct cnfexpr *e1, struct cnfexpr *e2) {
+    switch (e1->type) {
+    case CT_FALSE:
+        free_cnf(e2);
+        return e1;
+    case CT_TRUE:
+        free_cnf(e1);
+        return e2;
+    case CT_EXPR:
+        switch (e2->type) {
+        case CT_FALSE:
+            free_cnf(e1);
+            return e2;
+        case CT_TRUE:
+            free_cnf(e2);
+            return e1;
+        case CT_EXPR:
+            break;
+        }
+        break;
+    }
+
+    unsigned oldsize = e1->size;
+    e1->size += e2->size;
+    e1->sizes = realloc(e1->sizes, e1->size * sizeof(int));
+    e1->exprs = realloc(e1->exprs, e1->size * sizeof(int *));
+    memcpy(e1->sizes + oldsize, e2->sizes, e2->size * sizeof(int));
+    unsigned i;
+    for (i = 0; i < e2->size; i++) {
+        e1->exprs[oldsize + i] = malloc(e2->sizes[i] * sizeof(int));
+        memcpy(e1->exprs[oldsize + i], e2->exprs[i],
+               e2->sizes[i] * sizeof(int));
+    }
+    free_cnf(e2);
+    return e1;
+}
+
+void free_cnf(struct cnfexpr *e) {
+    if (e->type != CT_EXPR) {
+        free(e);
+        return;
+    }
+    unsigned i;
+    for (i = 0; i < e->size; i++) {
+        free(e->exprs[i]);
+    }
+    free(e->exprs);
+    free(e->sizes);
+    free(e);
+}
+
+
+struct boolexp *printf_original(struct symlist *sl, struct expr *expr) {
+    switch (expr->type) {
+    case E_OR:
+        printf("  OR\n");
+        printf_original(sl, expr->left.expr);
+        printf_original(sl, expr->right.expr);
+        break;
+    case E_AND:
+        printf("  AND\n");
+        printf_original(sl, expr->left.expr);
+        printf_original(sl, expr->right.expr);
+        break;
+    case E_NOT:
+        printf("  NOT\n");
+        printf_original(sl, expr->left.expr);
+        break;
+    case E_EQUAL:
+        printf("  = ");
+        printf("%s ", expr->left.sym->name);
+        if (!strcmp("y", expr->right.sym->name))
+            printf("YES\n");
+        else if (!strcmp("n", expr->right.sym->name))
+            printf("NO\n");
+        else if (!strcmp("m", expr->right.sym->name))
+            printf("MODULE\n");
+        else
+            printf("%s\n", expr->left.sym->name);
+        break;
+    case E_UNEQUAL:
+        printf("  != ");
+        printf("%s ", expr->left.sym->name);
+        if (!strcmp("y", expr->right.sym->name))
+            printf("YES\n");
+        else if (!strcmp("n", expr->right.sym->name))
+            printf("NO\n");
+        else
+            printf("OTHER %s\n", expr->right.sym->name);
+        break;
+    case E_LIST:
+        printf("  list\n");
+        break;
+    case E_SYMBOL:
+        printf("  symbol");
+        if (expr->left.sym->name != NULL)
+                printf(": %s", expr->left.sym->name);
+        printf("\n");
+        break;
+    case E_RANGE:
+        printf("  range\n");
+        break;
+    case E_NONE:
+        printf("  none\n");
+        break;
+    default:
+        printf("  ERROR\n");
+        break;
+    }
+
+}
diff --git a/programs/src/kconfig_parser/cnfexpr.h b/programs/src/kconfig_parser/cnfexpr.h
new file mode 100644
index 0000000..ed5c2fb
--- /dev/null
+++ b/programs/src/kconfig_parser/cnfexpr.h
@@ -0,0 +1,26 @@
+#ifndef _CNFEXPR_H_
+#define _CNFEXPR_H_
+
+#include <stdlib.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include "symlist.h"
+#include "kconfig/lkc.h"
+
+enum cnfexpr_type {
+    CT_EXPR, CT_FALSE, CT_TRUE
+};
+
+struct cnfexpr {
+    enum cnfexpr_type type; 
+    int **exprs;
+    unsigned *sizes;
+    unsigned size;
+};
+
+struct cnfexpr *kconfig_cnfexpr(struct symlist *sl, struct expr *expr);
+void cnf_printf(struct cnfexpr *);
+
+struct boolexp *printf_original(struct symlist *sl, struct expr *expr);
+
+#endif /* _CNFEXPR_H_ */
diff --git a/programs/src/kconfig_parser/kconfig_parser.c b/programs/src/kconfig_parser/kconfig_parser.c
index d936f48..c4ee358 100644
--- a/programs/src/kconfig_parser/kconfig_parser.c
+++ b/programs/src/kconfig_parser/kconfig_parser.c
@@ -12,20 +12,15 @@
 #include <stdbool.h>
 #include "kconfig/lkc.h"
 #include "symlist.h"
-#include "boolexp.h"
 #include "output.h"
 
-void kconfig_menu_walker(void (*solve)
-                          (struct symbol * sym));
-
-void solve_names(struct symbol *sym);
-void solve_dep(struct symbol *sym);
-
 struct symlist *gsymlist;
 int noname_num;
 
-int main(int argc, char **argv) {
+void build_symlist();
+void cpy_dep();
 
+int main(int argc, char **argv) {
     if (argc < 2) {
         printf("No input file specified\n");
         exit(1);
@@ -44,8 +39,8 @@ int main(int argc, char **argv) {
 
     gsymlist = symlist_create();
 
-    kconfig_menu_walker(solve_names);
-    kconfig_menu_walker(solve_dep);
+    build_symlist();
+    cpy_dep();
 
     char *rules_file, *symbol_map_file;
     asprintf(&rules_file, "%s/%s", argv[2], DEFAULT_RULES_FILE);
@@ -55,53 +50,47 @@ int main(int argc, char **argv) {
     return 0;
 }
 
-void kconfig_menu_walker(void (*solve) (struct symbol * sym)) {
-    struct menu *menu;
+void build_symlist() {
+    int i;
     struct symbol *sym;
-    menu = rootmenu.list;
-
-    while (menu != NULL) {
-        sym = menu->sym;
-        if (sym != NULL) {
-            do {
-                if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
-                    solve(sym);
-                }
-            } while ((sym = sym->next) != NULL);
-        }
-        // switch to menu
-        if (menu->list != NULL) {
-            menu = menu->list;
-        } else if (menu->next != NULL) {
-            menu = menu->next;
-        } else {
-            while ((menu = menu->parent) != NULL) {
-                if (menu->next != NULL) {
-                    menu = menu->next;
-                    break;
-                }
+    for_all_symbols(i, sym) {
+        if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
+            if (sym->name != NULL) {
+                symlist_add(gsymlist, sym->name);
+            } else {
+                sym->name = malloc((9 + 7) * sizeof(char));
+                sprintf(sym->name, "NONAMEGEN%d", noname_num++);
+                symlist_add(gsymlist, sym->name);
             }
         }
     }
 }
 
-void solve_names(struct symbol *sym) {
-    if (sym->name != NULL) {
-        if (symlist_find(gsymlist, sym->name) == NULL)
-            symlist_add(gsymlist, sym->name);
-    } else {
-        sym->name = malloc((9 + 7) * sizeof(char));
-        sprintf(sym->name, "NONAMEGEN%d", noname_num++);
-        symlist_add(gsymlist, sym->name);
-    }
-}
+void cpy_dep() {
+    int i;
+    struct symbol *sym;
+    struct symlist_el *el;
+    for_all_symbols(i, sym) {
+        if ((sym->type == S_BOOLEAN || sym->type == S_TRISTATE)
+            && strstr(sym->name, "NONAMEGEN") == NULL) {
+            printf("working: %s\n", sym->name);
 
-void solve_dep(struct symbol *sym) {
-    if (sym->dir_dep.expr != NULL) {
-        struct symlist_el *el;
-        el = symlist_find(gsymlist, sym->name);
-        el->be = copy_kconfig_dep(gsymlist, sym->dir_dep.expr);
-        if (el->be != NULL)
-            el->be = boolexp_cnf(el->be);
+            el = symlist_find(gsymlist, sym->name);
+            if (sym->dir_dep.expr != NULL) {
+                printf_original(gsymlist, sym->dir_dep.expr);
+                printf("Direct:\n");
+                el->be = kconfig_cnfexpr(gsymlist, sym->dir_dep.expr);
+                cnf_printf(el->be);
+            }
+            if (sym->rev_dep.expr != NULL) {
+                if (!strcmp(sym->name, "CRC32"))
+                        continue;
+                printf_original(gsymlist, sym->rev_dep.expr);
+                printf("Revers:\n");
+                el->re_be = kconfig_cnfexpr(gsymlist, sym->rev_dep.expr);
+                cnf_printf(el->re_be);
+                el->re_be = kconfig_cnfexpr(gsymlist, sym->rev_dep.expr);
+            }
+        }
     }
 }
diff --git a/programs/src/kconfig_parser/output.c b/programs/src/kconfig_parser/output.c
index 5f8bbd6..942693b 100644
--- a/programs/src/kconfig_parser/output.c
+++ b/programs/src/kconfig_parser/output.c
@@ -1,80 +1,59 @@
 #include "output.h"
 
-void fprint_rules(struct symlist *sl, char* output) {
+void fprint_rules_cnf(FILE * f, unsigned id, struct cnfexpr *cnf) {
+    unsigned i, y;
+    switch (cnf->type) {
+    case CT_FALSE:
+        // Never satisfiable
+        fprintf(f, "-%d\n", id);
+        break;
+    case CT_TRUE:
+        // Always satisfiable
+        break;
+    case CT_EXPR:
+        for (i = 0; i < cnf->size; i++) {
+            fprintf(f, "-%d ", id);
+            for (y = 0; y < cnf->sizes[i] - 1; y++) {
+                fprintf(f, "%d ", cnf->exprs[i][y]);
+            }
+            fprintf(f, "%d ", cnf->exprs[i][cnf->sizes[i] - 1]);
+            fprintf(f, "\n");
+        }
+        break;
+    }
+}
+
+void fprint_rules(struct symlist *sl, char *output) {
     FILE *f;
     f = fopen(output, "w");
     if (f == NULL) {
         fprintf(stderr, "Can't create file: %s\n", output);
         return;
     }
-    int i;
+    size_t i;
     struct symlist_el *el;
-    struct boolexp *be;
-    struct boolexp **stack;
-    size_t stack_size = 2, stack_pos = 0;
-    int count_or, count_and;
-    stack = malloc(stack_size * sizeof(struct boolexp *));
     for (i = 0; i < sl->pos; i++) {
         if (sl->array[i].be != NULL) {
             el = sl->array + i;
-            be = el->be;
-            stack_pos = 0;
-            count_or = 0;
-            count_and = 0;
-            fprintf(f, "-%d ", el->id);
-            while (be != NULL) {
-                if (stack_pos >= stack_size) {
-                    stack_size *= 2;
-                    stack =
-                        realloc(stack,
-                                stack_size * sizeof(struct boolexp *));
-                }
-                switch (be->type) {
-                case BE_NOT:
-                    fprintf(f, "-");
-                    be = be->left.be;
-                    break;
-                case BE_AND:
-                    count_and++;
-                    stack[stack_pos++] = be->right.be;
-                    be = be->left.be;
-                    break;
-                case BE_OR:
-                    count_or++;
-                    stack[stack_pos++] = be->right.be;
-                    be = be->left.be;
-                    break;
-                case BE_LEAF:
-                    fprintf(f, "%d", be->left.id);
-                    if (count_or > 0) {
-                        fprintf(f, " ");
-                        count_or--;
-                    } else if (count_and > 0) {
-                        fprintf(f, "\n-%d ", el->id);
-                        count_and--;
-                    }
-                    if (stack_pos > 0)
-                        be = stack[--stack_pos];
-                    else
-                        be = NULL;
-                    break;
-                }
+            if (el->be != NULL) {
+                fprint_rules_cnf(f, el->id, el->be);
+            }
+            if (el->re_be != NULL) {
+                fprint_rules_cnf(f, el->id, el->be);
             }
-            fprintf(f, "\n");
         }
     }
-    free(stack);
     fclose(f);
 }
 
-void fprint_symbol_map(struct symlist *sl, char* output) {
+void fprint_symbol_map(struct symlist *sl, char *output) {
     FILE *f;
     f = fopen(output, "w");
     if (f == NULL) {
         fprintf(stderr, "Can't create file: %s\n", output);
         return;
     }
-    int i;
+    size_t i;
     for (i = 0; i < sl->pos; i++) {
         fprintf(f, "%d:%s\n", sl->array[i].id, sl->array[i].name);
     }
diff --git a/programs/src/kconfig_parser/symlist.c b/programs/src/kconfig_parser/symlist.c
index 7dcd2c6..5423163 100644
--- a/programs/src/kconfig_parser/symlist.c
+++ b/programs/src/kconfig_parser/symlist.c
@@ -37,7 +37,7 @@ void symlist_print(struct symlist *sl) {
         printf("%d:%s\n", sl->array[i].id, sl->array[i].name);
         if (sl->array[i].be != NULL) {
             printf("  ");
-            boolexp_print(sl->array[i].be);
+            cnf_printf(sl->array[i].be);
             printf("\n");
         }
     }
diff --git a/programs/src/kconfig_parser/symlist.h b/programs/src/kconfig_parser/symlist.h
index caa827a..88bf4b0 100644
--- a/programs/src/kconfig_parser/symlist.h
+++ b/programs/src/kconfig_parser/symlist.h
@@ -3,12 +3,13 @@
 
 #include <stdbool.h>
 #include <string.h>
-#include "boolexp.h"
+#include "cnfexpr.h"
 
 struct symlist_el {
     unsigned int id;
     char *name;
-    struct boolexp *be;
+    struct cnfexpr *be;
+    struct cnfexpr *re_be; // forward dependency
 };
 struct symlist {
     struct symlist_el *array;