From 6b7ae6f3e38a06223d0a44ff28f6ff5951703f6f Mon Sep 17 00:00:00 2001 From: Michal Sojka Date: Sun, 25 Oct 2015 17:50:23 +0100 Subject: [PATCH] kconfig2sat almost finished --- kconfig2sat/Makefile | 10 + kconfig2sat/kconfig2sat.cc | 635 +++++++++++++++++++++++++++++-------- kconfig2sat/lcp_data.h | 1 + 3 files changed, 515 insertions(+), 131 deletions(-) diff --git a/kconfig2sat/Makefile b/kconfig2sat/Makefile index 5e00510..bde7a03 100644 --- a/kconfig2sat/Makefile +++ b/kconfig2sat/Makefile @@ -36,3 +36,13 @@ kconfig/zconf.tab.c: $(addprefix kconfig/,zconf.lex.c zconf.hash.c util.c confda clean:: $(RM) kconfig2sat $(OBJ_C) $(OBJ_CC) $(RM) kconfig/zconf.tab.c kconfig/zconf.lex.c kconfig/zconf.hash.c + +.PHONY: test +test: all + grep -q bbb ../.target + ./kconfig2sat -k ../targets/bbb/linux/Kconfig --env ../.conf.mk --baseconf ../targets/bbb/build/.config --varfile ../dot_measure --cnf test.cnf --dot test.dot + dot -Tpdf test.dot > test.pdf + +test2: all + ./kconfig2sat -k Kconfig.test --cnf test.cnf --dot test.dot + dot -Tpdf test.dot > test.pdf diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc index 356de0f..fa65b8c 100644 --- a/kconfig2sat/kconfig2sat.cc +++ b/kconfig2sat/kconfig2sat.cc @@ -23,6 +23,7 @@ enum options { OPT__START = 256, OPT_BASECONFIG, OPT_CNF, + OPT_DOT, OPT_DUMP, OPT_ENV, OPT_HELP, @@ -48,9 +49,11 @@ void print_help() ); } -char *expr_to_string(struct expr *e); +typedef unique_ptr upchar; -char *sym_to_string(struct symbol *sym) +upchar expr_to_string(struct expr *e); + +upchar sym_to_string(struct symbol *sym) { char *ret; @@ -58,37 +61,32 @@ char *sym_to_string(struct symbol *sym) asprintf(&ret, sym->name); else asprintf(&ret, "NONAME%d", sym->lcp.id); - return ret; + return upchar(ret); } -char *expr_binop_to_string(struct expr *e, const char *op_str) +upchar expr_binop_to_string(struct expr *e, const char *op_str) { - char *l = expr_to_string(e->left.expr); - char *r = expr_to_string(e->right.expr); + upchar l = expr_to_string(e->left.expr); + upchar r = expr_to_string(e->right.expr); char *ret; - asprintf(&ret, "(%s %s %s)", l, op_str, r); - free(l); - free(r); - return ret; + asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get()); + return upchar(ret); } -char *expr_comp_to_string(struct expr *e, const char *op_str) +upchar expr_comp_to_string(struct expr *e, const char *op_str) { - char *l = sym_to_string(e->left.sym); - char *r = sym_to_string(e->right.sym); + upchar l = sym_to_string(e->left.sym); + upchar r = sym_to_string(e->right.sym); char *ret; - asprintf(&ret, "(%s %s %s)", l, op_str, r); - free(l); - free(r); - return ret; + asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get()); + return upchar(ret); } -char *expr_to_string(struct expr *e) +upchar expr_to_string(struct expr *e) { char *ret = NULL; - char *tmp; if (!e) return NULL; @@ -96,16 +94,14 @@ char *expr_to_string(struct expr *e) switch (e->type) { case E_NONE: asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr)); - return ret; + return upchar(ret); case E_OR: return expr_binop_to_string(e, "||"); case E_AND: return expr_binop_to_string(e, "&&"); case E_NOT: - tmp = expr_to_string(e->left.expr); - asprintf(&ret, "!%s", tmp); - free(tmp); - return ret; + asprintf(&ret, "!%s", expr_to_string(e->left.expr).get()); + break; case E_EQUAL: return expr_comp_to_string(e, "=="); case E_UNEQUAL: @@ -130,7 +126,7 @@ char *expr_to_string(struct expr *e) break; } - return ret; + return upchar(ret); } @@ -138,10 +134,9 @@ char *expr_to_string(struct expr *e) void dump_symbol(struct symbol *sym) { struct property *prop; - const char *name = sym_to_string(sym); + upchar name = sym_to_string(sym); const char *type = sym_type_name(sym->type); const char *prompt = NULL; - char *tmp; char flags[256] = "fl("; char val = '.'; @@ -177,21 +172,16 @@ void dump_symbol(struct symbol *sym) prompt = prop->text; } - printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt); + printf("%-40s %c %-8s %-50s %s\n", name.get(), val, type, flags, prompt); if (verbosity > 0) { - if (sym->dir_dep.expr) { - tmp = expr_to_string(sym->dir_dep.expr); - printf(" depends %s\n", tmp); - free(tmp); - } + if (sym->dir_dep.expr) + printf(" depends %s\n", expr_to_string(sym->dir_dep.expr).get()); for_all_properties(sym, prop, P_SELECT) { assert(prop->expr->type == E_SYMBOL); - tmp = expr_to_string(prop->visible.expr); - printf(" selects %s if %s\n", prop->expr->left.sym->name, tmp); - free(tmp); - + printf(" selects %s if %s\n", prop->expr->left.sym->name, + expr_to_string(prop->visible.expr).get()); } } } @@ -220,21 +210,23 @@ void read_varfile(const char *varfile) char *p = line; lineno++; + if (line[0] == '#') + continue; if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0) p += strlen(CONFIG_); const char *sym_name = strtok(p, " =\n"); struct symbol *sym = sym_find(sym_name); if (!sym) { - fprintf(stderr, "%s:%d: Invalid symbol: %s\n", varfile, lineno, sym_name); - exit(EXIT_FAILURE); - } - if (!(sym->flags & SYMBOL_WRITE)) { - fprintf(stderr, "%s:%d: Symbol %s not visible\n", varfile, lineno, sym_name); + fprintf(stderr, "%s:%d: Error: Invalid symbol: %s\n", varfile, lineno, sym_name); exit(EXIT_FAILURE); } +// if (!(sym->flags & SYMBOL_WRITE)) { +// fprintf(stderr, "%s:%d: Error: Symbol %s not visible\n", varfile, lineno, sym_name); +// exit(EXIT_FAILURE); +// } if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) { - fprintf(stderr, "%s:%d: Choice values not yet supported: %s", varfile, lineno, sym_name); + fprintf(stderr, "%s:%d: Error: Choice values not yet supported: %s", varfile, lineno, sym_name); exit(EXIT_FAILURE); } struct property *prop; @@ -250,37 +242,77 @@ void read_varfile(const char *varfile) fclose(f); } +void set_all_symbols_variable() +{ + int i; + struct symbol *sym; + + for_all_symbols(i, sym) { + if (!(sym->flags & (SYMBOL_CONST | SYMBOL_AUTO))) + sym->lcp.variable = 1; + } +} + struct SatLiteral { struct symbol *sym; struct expr *expr; + int dot_printed:1; - SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {} - SatLiteral(struct expr *e) : sym(nullptr), expr(e) {} - bool has_fixed_value() const { return sym && !sym->lcp.variable; } + SatLiteral(struct symbol *s) : sym(s), expr(nullptr) { assert(sym->lcp.variable && sym->lcp.id); } + SatLiteral(struct expr *e) : sym(nullptr), expr(e) { assert(expr->lcp.variable && expr->lcp.id); } sat_id id() const { return sym ? sym->lcp.id : expr->lcp.id; } - bool value() const { assert(sym); return sym->curr.tri == yes; } + upchar name() const { + char *ret; + if (sym) { + assert(sym->name); // TODO + asprintf(&ret, "%s", sym->name); + } else if (expr) { + asprintf(&ret, "expr%d", expr->lcp.id); + } + return upchar(ret); + } }; typedef vector SatClause; +struct Implication: public SatClause { + Implication(sat_id a, sat_id b) : SatClause{-a, b} {} +}; + struct SatExpr { sat_id left, right; enum expr_type op; - SatExpr(int l, enum expr_type o, int r) + SatExpr(sat_id l, enum expr_type o, sat_id r) : left(l), right(r), op(o) {} + //SatExpr(enum expr_type o) : left(0), right(0), op(o) { assert(o == E_NONE); } bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); } }; -class SatLiterals : public vector +class SatLiterals : protected vector { public: - int fixed = {0}; - SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); } - int count() const { return size() - 1; } + using vector::begin; + using vector::end; + using vector::push_back; + SatLiterals() { reserve(20000); } + int count() const { return size(); } + const SatLiteral &operator[](size_type i) const { return at(i-1); } + const SatLiteral &last() const { return *(--end()); } + bool test_set_dot_printed(struct symbol *sym) const { + auto l = (*this)[sym->lcp.id]; + bool ret = l.dot_printed; + l.dot_printed = 1; + return ret; + } + bool test_set_dot_printed(struct expr *e) const { + auto l = (*this)[e->lcp.id]; + bool ret = l.dot_printed; + l.dot_printed = 1; + return ret; + } }; - /* * bool FOO!=n => FOO * bool FOO!=y => !FOO @@ -336,51 +368,252 @@ struct expr *expr_eliminate_eq_yn(struct expr *e) return e; } +bool mark_variable_expressions(struct expr *e) +{ + if (!e) + return false; + + switch (e->type) { + case E_SYMBOL: + return (e->lcp.variable = e->left.sym->lcp.variable); + case E_NONE: + fprintf(stderr, "NONE not implemented\n"); + exit(EXIT_FAILURE); + break; + case E_NOT: + if (mark_variable_expressions(e->left.expr)) + return (e->lcp.variable = 1); + else + return false; + case E_OR: + case E_AND: { + mark_variable_expressions(e->left.expr); + mark_variable_expressions(e->right.expr); + + if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) { + return (e->lcp.variable = 1); + } else if (!e->left.expr->lcp.variable && !e->right.expr->lcp.variable) { + return (e->lcp.variable = 0); + } else { + tristate val; + + if (e->left.expr->lcp.variable) { + val = expr_calc_value(e->right.expr); + } else if (e->right.expr->lcp.variable) { + val = expr_calc_value(e->left.expr); + } + if ((e->type == E_OR && val == yes) || + (e->type == E_AND && val == no)) + return (e->lcp.variable = 0); + else + return (e->lcp.variable = 1); + } + __builtin_unreachable(); + } + case E_EQUAL: + case E_UNEQUAL: + if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) { + return (e->lcp.variable = 1); + } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) { + fprintf(stderr, "Comparison with fixed symbol not yet supported!\n"); + exit(EXIT_FAILURE); + } else + return false; + case E_LTH: + case E_LEQ: + case E_GTH: + case E_GEQ: + if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) { + fprintf(stderr, "Comparison of variable symbols not implemented\n"); + exit(EXIT_FAILURE); + } else + return false; + break; + case E_LIST: + fprintf(stderr, "LIST not implemented\n"); + exit(EXIT_FAILURE); + break; + case E_RANGE: + fprintf(stderr, "RANGE not implemented\n"); + exit(EXIT_FAILURE); + break; + } + fprintf(stderr, "Unexpected situation in mark_variable_expressions\n"); + exit(EXIT_FAILURE); +} + +void mark_variable_expressions() +{ + int i; + struct symbol *sym; + struct property *prop; + + for_all_symbols(i, sym) { + mark_variable_expressions(sym->dir_dep.expr); + mark_variable_expressions(sym->rev_dep.expr); + for_all_properties(sym, prop, P_SELECT) { + assert(prop->expr->type == E_SYMBOL); + mark_variable_expressions(prop->visible.expr); + } + } +} + +void check_dep_consistency() +{ + int i; + struct symbol *sym; + tristate val; + + for_all_symbols(i, sym) { + if (sym->lcp.variable && sym->dir_dep.expr && !sym->dir_dep.expr->lcp.variable) { + val = expr_calc_value(sym->dir_dep.expr); + if (val == no) { + fprintf(stderr, "Symbol %s cannot be variable because its dependency is always 'no': %s\n", + sym->name, expr_to_string(sym->dir_dep.expr).get()); + exit(EXIT_FAILURE); + } + } + if (sym->lcp.variable && sym->rev_dep.expr && !sym->rev_dep.expr->lcp.variable) { + val = expr_calc_value(sym->rev_dep.expr); + if (val == yes) { + fprintf(stderr, "Symbol %s cannot be variable because it is selected by expression that is always 'yes': %s\n", + sym->name, expr_to_string(sym->rev_dep.expr).get()); + exit(EXIT_FAILURE); + } + } + if (!sym->lcp.variable && (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) && + sym->curr.tri == no && sym->rev_dep.expr && sym->rev_dep.expr->lcp.variable) { + fprintf(stderr, "Symbol %s cannot be fixed to 'no', because it is selcted by variable expression '%s'\n", + sym->name, expr_to_string(sym->rev_dep.expr).get()); + exit(EXIT_FAILURE); + } + } +} + + +class DotWriter { + FILE *f; +public: + DotWriter(const char *file_name) { + f = fopen(file_name, "w"); + + if (!f) { + perror(file_name); + exit(EXIT_FAILURE); + } + + fprintf(f, "digraph conf {\n"); + //fprintf(f, "rankdir=LR;\n"); + } + ~DotWriter() { + fprintf(f, "}\n"); + fclose(f); + } + void symbol(struct symbol *sym) { +// if (sym->lcp.dot_printed) +// return; +// sym->lcp.dot_printed = 1; + + const char *opts = ""; + if (sym->lcp.variable) + opts = " [penwidth=3]"; + else + opts = " [color=gray]"; + fprintf(f, "\"%s\"%s;\n", sym->name, opts); + } + void expr(const SatLiteral &l) { + assert(l.expr); + const char *label = "???"; +// if (sym->lcp.dot_printed) +// return; +// sym->lcp.dot_printed = 1; + switch (l.expr->type) { + case E_OR: label = "|"; break; + case E_AND: label = "&"; break; + case E_EQUAL: label = "="; break; + case E_UNEQUAL: label = "!="; break; + case E_NOT: label = "!"; break; + case E_SYMBOL: + case E_NONE: + case E_RANGE: + case E_LTH: + case E_LEQ: + case E_GTH: + case E_GEQ: + case E_LIST: + default: + fprintf(stderr, "Expr %d not implemented\n", l.expr->type); + exit(EXIT_FAILURE); + break; + } + + fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", l.name().get(), label); + } + void depends_on(const SatLiteral &l1, const SatLiteral &l2) { + fprintf(f, "\"%s\" -> \"%s\" [style=bold,label=d];\n", l1.name().get(), l2.name().get()); + } + void selects(const SatLiteral &l1, const SatLiteral &l2) { + fprintf(f, "\"%s\" -> \"%s\" [style=bold,arrowhead=open,label=s];\n", l1.name().get(), l2.name().get()); + } + void edge(const SatLiteral &from, const SatLiteral &to) { + fprintf(f, "\"%s\" -> \"%s\" [arrowhead=empty];\n", from.name().get(), to.name().get()); + } +}; class SatData { SatLiterals literals = {}; vector clauses = {}; map expressions = {}; - + DotWriter *dot = nullptr; public: - SatData() { + SatData(const char *dot_fn) { + if (dot_fn) + dot = new DotWriter(dot_fn); symbols2literals(); expressions2literals(); - symbols2clauses(); expressions2clauses(); + if (dot) + delete dot; + } - void add_symbol_literal(struct symbol *sym) { + const SatLiteral &add_literal(struct symbol *sym) { + sym->lcp.id = literals.count() + 1; literals.push_back(SatLiteral(sym)); - sym->lcp.id = literals.count(); + if (dot) + dot->symbol(sym); + return literals.last(); + } + + const SatLiteral &add_literal(struct expr *e) { + e->lcp.id = literals.count() + 1; + literals.push_back(SatLiteral(e)); + if (dot) + dot->expr(literals.last()); + return literals.last(); } void symbols2literals() { int i; struct symbol *sym; - symbol_yes.type = S_TRISTATE; - symbol_no.type = S_TRISTATE; - symbol_mod.type = S_TRISTATE; - - add_symbol_literal(&symbol_yes); - add_symbol_literal(&symbol_no); - add_symbol_literal(&symbol_mod); - for_all_symbols(i, sym) { - if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE || sym->type == S_UNKNOWN) { - add_symbol_literal(sym); - } + if (sym->lcp.variable) + add_literal(sym); } } - void expr2literal(struct expr *e) { - if (!e || e->lcp.id) - return; + // Assign e->lcp.id to variable literals + sat_id expr2literal(struct expr *e) { + if (!e || !e->lcp.variable) + return 0; + if (e->lcp.id) + return e->lcp.id; switch (e->type) { case E_SYMBOL: + assert(e->left.sym->lcp.id); e->lcp.id = e->left.sym->lcp.id; break; case E_NONE: @@ -393,9 +626,10 @@ public: SatExpr se(e->left.expr->lcp.id, e->type, 0); auto it = expressions.find(se); if (it == expressions.end()) { - literals.push_back(SatLiteral(e)); - expressions.insert(pair(se, literals.count())); - e->lcp.id = literals.count(); + auto l = add_literal(e); + expressions.insert(pair(se, l.id())); + if (dot) + dot->edge(literals[e->left.expr->lcp.id], l); } else e->lcp.id = it->second; break; @@ -405,32 +639,56 @@ public: expr2literal(e->left.expr); expr2literal(e->right.expr); - SatExpr se(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id); - auto it = expressions.find(se); - if (it == expressions.end()) { - literals.push_back(SatLiteral(e)); - expressions.insert(pair(se, literals.count())); - e->lcp.id = literals.count(); - } else - e->lcp.id = it->second; + if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) { + SatExpr se = SatExpr(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id); + auto it = expressions.find(se); + if (it == expressions.end()) { + auto l = add_literal(e); + expressions.insert(pair(se, l.id())); + if (dot) { + dot->edge(literals[e->left.expr->lcp.id], l); + dot->edge(literals[e->right.expr->lcp.id], l); + } + } else + e->lcp.id = it->second; + } else { + if (e->left.expr->lcp.variable) { + e->lcp.id = e->left.expr->lcp.id; + } else if (e->right.expr->lcp.variable) { + e->lcp.id = e->right.expr->lcp.id; + } + } break; } case E_EQUAL: - case E_UNEQUAL: + case E_UNEQUAL: { + if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) { + SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id); + auto it = expressions.find(se); + if (it == expressions.end()) { + auto l = add_literal(e); + expressions.insert(pair(se, l.id())); + if (dot) { + dot->edge(literals[e->left.sym->lcp.id], l); + dot->edge(literals[e->right.sym->lcp.id], l); + } + } else + e->lcp.id = it->second; + } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) { + fprintf(stderr, "Comparison with fixed symbol not yet supported!\n"); + exit(EXIT_FAILURE); + } + break; + } case E_LTH: case E_LEQ: case E_GTH: - case E_GEQ: { - SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id); - auto it = expressions.find(se); - if (it == expressions.end()) { - literals.push_back(SatLiteral(e)); - expressions.insert(pair(se, literals.count())); - e->lcp.id = literals.count(); - } else - e->lcp.id = it->second; + case E_GEQ: + if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) { + fprintf(stderr, "Comparison of variable symbols not implemented\n"); + exit(EXIT_FAILURE); + } break; - } case E_LIST: fprintf(stderr, "LIST not implemented\n"); exit(EXIT_FAILURE); @@ -440,46 +698,53 @@ public: exit(EXIT_FAILURE); break; } + assert(e->lcp.id); + return e->lcp.id; } void expressions2literals() { int i; struct symbol *sym; - struct property *prop; + struct expr *e; + sat_id id; + const SatLiteral *syml; for_all_symbols(i, sym) { - if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) { - assert(sym->lcp.id); - if (sym->flags & SYMBOL_VALID && !sym->lcp.variable) - clauses.push_back(SatClause{ sym->curr.tri == yes ? sym->lcp.id : -sym->lcp.id }); - - sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr); - expr2literal(sym->dir_dep.expr); - - for_all_properties(sym, prop, P_SELECT) { - assert(prop->expr->type == E_SYMBOL); - prop->visible.expr = expr_eliminate_eq_yn(prop->visible.expr); - expr2literal(prop->visible.expr); + if (sym->lcp.variable && + (sym->type == S_BOOLEAN || sym->type == S_TRISTATE)) { + syml = &literals[sym->lcp.id]; + // Direct dependencies + //sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr); + e = sym->dir_dep.expr; + id = expr2literal(e); + if (id) { + clauses.push_back(Implication(sym->lcp.id, id)); + if (dot) + dot->depends_on(*syml, literals[id]); + } + + // Reverse dependecies + e = sym->rev_dep.expr; + id = expr2literal(e); + if (id) { + clauses.push_back(Implication(id, sym->lcp.id)); + if (dot) + dot->selects(literals[id], *syml); } } } } - void symbols2clauses() { - for (auto lit: literals) - if (lit.sym && lit.has_fixed_value()) - clauses.push_back(SatClause{ lit.value() ? lit.id() : -lit.id() }); - } - + // Tseitin Transformation - see + // https://en.wikipedia.org/wiki/Tseitin_transformation or + // http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27. void expressions2clauses() { - // Tseitin Transformation - see https://en.wikipedia.org/wiki/Tseitin_transformation - // or http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27. for (auto expr: expressions) { SatExpr e = expr.first; sat_id e_id = expr.second; assert(e_id); if (e.left == 0 || (e.right == 0 && e.op != E_NOT)) { - unique_ptr tmp(expr_to_string(literals[e_id].expr)); + upchar tmp(expr_to_string(literals[e_id].expr)); printf("Unexpected sat_id == 0 in %s\n", tmp.get()); //exit(1); } @@ -519,7 +784,7 @@ public: case E_GTH: case E_GEQ: { struct expr *e = literals[e_id].expr; - unique_ptr tmp(expr_to_string(e)); + upchar tmp(expr_to_string(e)); tristate val = expr_calc_value(e); //fprintf(stderr, "Comparison operators not implemented %s = %d\n", tmp.get(), val); //exit(EXIT_FAILURE); @@ -547,18 +812,13 @@ public: exit(EXIT_FAILURE); } - fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed); + fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size()); for (auto l: literals) { - if (l.sym) { - char val = l.has_fixed_value() ? (l.value() ? 'y' : 'n') : '?'; - fprintf(f, "c SYM %d %s = %c\n", l.sym->lcp.id, l.sym->name, val); - } - if (l.expr) { - char *tmp = expr_to_string(l.expr); - fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, tmp); - free(tmp); - } + if (l.sym) + fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name); + if (l.expr) + fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get()); } for (auto clause: clauses) { for (sat_id id: clause) { @@ -569,6 +829,110 @@ public: } fclose(f); } + +// void print_dot_oper(FILE *f, struct expr *e, const char *parent, const char *label) { +// char *expr_name; +// asprintf(&expr_name, "expr%d", e->lcp.id); +// fprintf(f, "\"%s\" -> \"%s\";\n", parent, expr_name); + +// fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", expr_name, label); +// print_dot_expr(f, e->left.expr, expr_name, "l", ""); +// print_dot_expr(f, e->right.expr, expr_name, "r", ""); +// free(expr_name); +// } + +// void print_dot_expr(FILE *f, struct expr *e, const char *parent, +// const char *suffix, const char *edge_opts) { +// if (e->lcp.dot_printed || +// !e->lcp.variable) +// return; +// e->lcp.dot_printed = 1; +// if (e) { +// switch (e->type) { +// case E_NONE: +// break; +// case E_OR: +// print_dot_oper(f, e, parent, "|"); +// break; +// case E_AND: +// print_dot_oper(f, e, parent, "&"); +// break; +// case E_NOT: +// print_dot_expr(f, e->left.expr, parent, suffix, "arrowhead=odot"); +// break; +// case E_EQUAL: +// print_dot_oper(f, e, parent, "="); +// break; +// case E_UNEQUAL: +// print_dot_oper(f, e, parent, "!="); +// break; +// case E_LIST: +// fprintf(stderr, "LIST not implemented\n"); +// exit(EXIT_FAILURE); +// break; +// case E_SYMBOL: { +// if (e->left.sym->name) { +// fprintf(f, "\"%s\" -> \"%s\" [%s];\n", parent, e->left.sym->name, edge_opts); +// print_dot_symbol(f, e->left.sym); +// } +// break; +// } +// case E_RANGE: +// fprintf(stderr, "RANGE not implemented\n"); +// exit(EXIT_FAILURE); +// break; +// case E_LTH: +// case E_LEQ: +// case E_GTH: +// case E_GEQ: +// break; +// } +// } +// } + +// void print_dot_symbol(FILE *f, struct symbol *sym) { +// if (!sym->lcp.variable || +// sym->lcp.dot_printed) +// return; +// sym->lcp.dot_printed = 1; + +// const char *opts = ""; +// if (sym->lcp.variable) +// opts = " [penwidth=3]"; +// else +// opts = " [color=gray]"; +// fprintf(f, "\"%s\"%s;\n", sym->name, opts); +// if (sym->dir_dep.expr) +// print_dot_expr(f, sym->dir_dep.expr, sym->name, "", ""); + +// struct property *prop; +// for_all_properties(sym, prop, P_SELECT) { +// assert(prop->expr->type == E_SYMBOL); +// print_dot_expr(f, prop->expr, sym->name, "", "label=\"selects\""); +// if (prop->visible.expr && prop->visible.expr->lcp.variable) { +// printf("Not implemented %s\n", expr_to_string(prop->visible.expr).get()); +// } +// } +// } + + +// void write_dot(const char *dot) { +// int i; +// FILE *f = fopen(dot, "w"); + +// if (!f) { +// perror(dot); +// exit(EXIT_FAILURE); +// } + +// fprintf(f, "digraph conf {\n"); + +// struct symbol *sym; +// for_all_symbols(i, sym) +// print_dot_symbol(f, sym); +// fprintf(f, "}\n"); +// fclose(f); +// } }; int main(int argc, char **argv) @@ -577,6 +941,7 @@ int main(int argc, char **argv) char *baseconf = NULL; char *cnf = NULL; + char *dot = NULL; char *kconfig = NULL; char *varfile = NULL; int dump = false; @@ -586,6 +951,7 @@ int main(int argc, char **argv) static struct option long_options[] = { {"baseconf", required_argument, 0, OPT_BASECONFIG }, {"cnf", required_argument, 0, OPT_CNF }, + {"dot", required_argument, 0, OPT_DOT }, {"env", required_argument, 0, OPT_ENV }, {"dump", no_argument, &dump, true }, {"help", no_argument, 0, OPT_HELP }, @@ -611,6 +977,9 @@ int main(int argc, char **argv) case OPT_CNF: cnf = optarg; break; + case OPT_DOT: + dot = optarg; + break; case OPT_ENV: set_missing_env(optarg); break; @@ -657,17 +1026,21 @@ int main(int argc, char **argv) if (baseconf) conf_read(baseconf); - SatData sat_data; - if (varfile) read_varfile(varfile); + else + set_all_symbols_variable(); + + mark_variable_expressions(); + check_dep_consistency(); + + SatData sat_data(dot); if (dump) do_dump(); - if (cnf) { + if (cnf) sat_data.write_dimacs_cnf(cnf); - } return EXIT_SUCCESS; } diff --git a/kconfig2sat/lcp_data.h b/kconfig2sat/lcp_data.h index 4953b3f..e3ea702 100644 --- a/kconfig2sat/lcp_data.h +++ b/kconfig2sat/lcp_data.h @@ -14,6 +14,7 @@ struct lcp_symbol { struct lcp_expr { sat_id id; + int variable:1; /* The value of the expression depends on variable symbol. */ }; -- 2.39.2