From 2d6ec056c8702c157e243b6ca6f98bb568f7d1ef Mon Sep 17 00:00:00 2001 From: Michal Sojka Date: Mon, 19 Oct 2015 22:55:50 +0200 Subject: [PATCH] kconfig2sat: More work --- kconfig2sat/Makefile | 4 +- kconfig2sat/kconfig/expr.h | 4 +- kconfig2sat/kconfig2sat.cc | 371 ++++++++++++++++++++++++++++++++++--- kconfig2sat/lcp_data.h | 8 +- 4 files changed, 354 insertions(+), 33 deletions(-) diff --git a/kconfig2sat/Makefile b/kconfig2sat/Makefile index 218dba6..5e00510 100644 --- a/kconfig2sat/Makefile +++ b/kconfig2sat/Makefile @@ -29,10 +29,10 @@ kconfig2sat: $(OBJ_CC) $(OBJ_C) %.lex.c: %.l flex -o $@ -L -P zconf $< -kconfig/zconf.tab.c: kconfig/zconf.lex.c kconfig/zconf.hash.c +kconfig/zconf.tab.c: $(addprefix kconfig/,zconf.lex.c zconf.hash.c util.c confdata.c expr.c symbol.c menu.c) %.tab.c: %.y bison -o $@ $< -p zconf -t -l clean:: - $(RM) kconfig2sat $(OBJ) + $(RM) kconfig2sat $(OBJ_C) $(OBJ_CC) $(RM) kconfig/zconf.tab.c kconfig/zconf.lex.c kconfig/zconf.hash.c diff --git a/kconfig2sat/kconfig/expr.h b/kconfig2sat/kconfig/expr.h index a8f8361..19a52b0 100644 --- a/kconfig2sat/kconfig/expr.h +++ b/kconfig2sat/kconfig/expr.h @@ -44,7 +44,7 @@ struct expr { enum expr_type type; union expr_data left, right; - struct lcp_expr *lcp; + struct lcp_expr lcp; }; #define EXPR_OR(dep1, dep2) (((dep1)>(dep2))?(dep1):(dep2)) @@ -89,7 +89,7 @@ struct symbol { struct expr_value dir_dep; struct expr_value rev_dep; - struct lcp_symbol *lcp; + struct lcp_symbol lcp; }; #define for_all_symbols(i, sym) for (i = 0; i < SYMBOL_HASHSIZE; i++) for (sym = symbol_hash[i]; sym; sym = sym->next) if (sym->type != S_OTHER) diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc index c47daac..1f4ea0d 100644 --- a/kconfig2sat/kconfig2sat.cc +++ b/kconfig2sat/kconfig2sat.cc @@ -6,11 +6,13 @@ #include #include #include +#include #include "kconfig/lkc.h" #include "lcp_utils.h" #include +#include using namespace std; @@ -45,12 +47,100 @@ void print_help() ); } +char *expr_to_string(struct expr *e); + +char *sym_to_string(struct symbol *sym) +{ + char *ret; + + if (sym->name) + asprintf(&ret, sym->name); + else + asprintf(&ret, "NONAME%d", sym->lcp.sat_id); + return ret; +} + +char *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); + char *ret; + + asprintf(&ret, "(%s %s %s)", l, op_str, r); + free(l); + free(r); + return ret; +} + +char *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); + char *ret; + + asprintf(&ret, "(%s %s %s)", l, op_str, r); + free(l); + free(r); + return ret; +} + +char *expr_to_string(struct expr *e) +{ + char *ret = NULL; + char *tmp; + + if (!e) + return NULL; + + switch (e->type) { + case E_NONE: + asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr)); + return 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; + case E_EQUAL: + return expr_comp_to_string(e, "=="); + case E_UNEQUAL: + return expr_comp_to_string(e, "!="); + case E_LTH: + return expr_comp_to_string(e, "<"); + case E_LEQ: + return expr_comp_to_string(e, "<="); + case E_GTH: + return expr_comp_to_string(e, ">"); + case E_GEQ: + return expr_comp_to_string(e, ">="); + case E_LIST: + fprintf(stderr, "LIST not implemented\n"); + exit(EXIT_FAILURE); + break; + case E_SYMBOL: + return sym_to_string(e->left.sym); + case E_RANGE: + fprintf(stderr, "RANGE not implemented\n"); + exit(EXIT_FAILURE); + break; + } + + return ret; +} + + + void dump_symbol(struct symbol *sym) { struct property *prop; - const char *name = sym->name; + const char *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 = '.'; @@ -87,6 +177,22 @@ void dump_symbol(struct symbol *sym) } printf("%-40s %c %-8s %-50s %s\n", name, 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); + } + + 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); + + } + } } void do_dump() @@ -138,23 +244,11 @@ void read_varfile(const char *varfile) if (!prompt) { fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name); } - sym->lcp->variable = 1; + sym->lcp.variable = 1; } fclose(f); } -void write_dimacs_cnf(const char *cnf) -{ - FILE *f = fopen(cnf, "w"); - - if (!f) { - perror(cnf); - exit(EXIT_FAILURE); - } - - fclose(f); -} - struct SatLiteral { struct symbol *sym; struct expr *expr; @@ -163,8 +257,15 @@ struct SatLiteral { SatLiteral(struct expr *e) : sym(nullptr), expr(e) {} }; -struct SatClause { - // TODO +typedef vector SatClause; + +struct SatExpr { + sat_id left, right; + enum expr_type op; + + SatExpr(int l, enum expr_type o, int r) + : left(l), right(r), op(o) {} + bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); } }; class SatLiterals : public vector @@ -175,25 +276,162 @@ public: int count() const { return size() - 1; } }; + +/* + * bool FOO!=n => FOO + * bool FOO!=y => !FOO + * bool FOO==n => !FOO + * bool FOO==y => FOO + */ +struct expr *expr_eliminate_eq_yn(struct expr *e) +{ + if (!e) + return NULL; + switch (e->type) { + case E_AND: + case E_OR: + case E_NOT: + e->left.expr = expr_eliminate_eq_yn(e->left.expr); + e->right.expr = expr_eliminate_eq_yn(e->right.expr); + break; + case E_UNEQUAL: + // UNKNOWN symbols sometimes occur in dependency - + // e.g. ACPI_VIDEO on arm (the symbol is only defined + // for ACPI platforms (x86) but some drivers refer to + // it. + if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) { + if (e->right.sym == &symbol_no) { + // FOO!=n -> FOO + e->type = E_SYMBOL; + e->right.sym = NULL; + } else if (e->right.sym == &symbol_yes) { + // FOO!=y -> !FOO + e->type = E_SYMBOL; + e->right.sym = NULL; + e = expr_alloc_one(E_NOT, e); + } + } + break; + case E_EQUAL: + if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) { + if (e->right.sym == &symbol_yes) { + // FOO==y -> FOO + e->type = E_SYMBOL; + e->right.sym = NULL; + } else if (e->right.sym == &symbol_no) { + // FOO==n -> !FOO + e->type = E_SYMBOL; + e->right.sym = NULL; + e = expr_alloc_one(E_NOT, e); + } + } + break; + default: + ; + } + return e; +} + + class SatData { SatLiterals literals = {}; vector clauses = {}; + map expressions = {}; + + void expr2literal(struct expr *e); + public: SatData() { + symbols2literals(); + expressions2literals(); + expressions2clauses(); + } + + void symbols2literals() { int i; struct symbol *sym; for_all_symbols(i, sym) { if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) { literals.push_back(SatLiteral(sym)); - sym->lcp = new lcp_symbol; - memset(sym->lcp, 0, sizeof(*sym->lcp)); - sym->lcp->sat_id = literals.count(); + sym->lcp.sat_id = literals.count(); } } } + void expressions2literals() { + int i; + struct symbol *sym; + struct property *prop; + + for_all_symbols(i, sym) { + if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) { + 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); + } + } + } + } + + 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; + switch (e.op) { + case E_SYMBOL: + case E_NONE: + assert(0); + break; + case E_NOT: + clauses.push_back(SatClause{ e_id, e.left }); + clauses.push_back(SatClause{ -e_id, -e.left }); + break; + case E_OR: + clauses.push_back(SatClause{ -e.left, e_id }); + clauses.push_back(SatClause{ -e.right, e_id }); + clauses.push_back(SatClause{ -e_id, e.left, e.right }); + break; + case E_AND: + clauses.push_back(SatClause{ -e_id, e.left }); + clauses.push_back(SatClause{ -e_id, e.right }); + clauses.push_back(SatClause{ -e.left, -e.right, e_id }); + break; + case E_EQUAL: + clauses.push_back(SatClause{ -e_id, -e.left, e.right }); + clauses.push_back(SatClause{ -e_id, -e.right, e.left }); + clauses.push_back(SatClause{ -e.left, -e.right, e_id }); + clauses.push_back(SatClause{ e.left, e.right, e_id }); + break; + case E_UNEQUAL: + case E_LTH: + case E_LEQ: + case E_GTH: + case E_GEQ: { + fprintf(stderr, "Comparison operators not implemented\n"); + //exit(EXIT_FAILURE); + 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; + } + } + + } + void write_dimacs_cnf(const char *cnf) { int i; FILE *f = fopen(cnf, "w"); @@ -207,15 +445,97 @@ public: for (i = 1; i <= literals.count(); i++) { SatLiteral &l = literals[i]; - if (l.sym) - fprintf(f, "c SYM %d %s\n", l.sym->lcp->sat_id, l.sym->name); - if (l.sym && l.sym->flags & SYMBOL_VALID && !l.sym->lcp->variable) - fprintf(f, "%d 0\n", l.sym->curr.tri != no ? l.sym->lcp->sat_id : -l.sym->lcp->sat_id); + if (l.sym) { + fprintf(f, "c SYM %d %s\n", l.sym->lcp.sat_id, l.sym->name); + if (l.sym->flags & SYMBOL_VALID && !l.sym->lcp.variable) + fprintf(f, "%d 0\n", l.sym->curr.tri != no ? l.sym->lcp.sat_id : -l.sym->lcp.sat_id); + } + if (l.expr) { + char *tmp = expr_to_string(l.expr); + fprintf(f, "c EXPR %d %s\n", l.expr->lcp.sat_id, tmp); + free(tmp); + } + } + for (auto clause: clauses) { + for (sat_id id: clause) + fprintf(f, "%d ", id); + fprintf(f, "0\n"); } fclose(f); } }; +void none(struct expr *e) +{ +} + +void SatData::expr2literal(struct expr *e) +{ + if (!e || e->lcp.sat_id) + return; + + switch (e->type) { + case E_SYMBOL: + e->lcp.sat_id = e->left.sym->lcp.sat_id; + break; + case E_NONE: + fprintf(stderr, "NONE not implemented\n"); + exit(EXIT_FAILURE); + break; + case E_NOT: { + expr2literal(e->left.expr); + + SatExpr se(e->left.expr->lcp.sat_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.sat_id = literals.count(); + } else + e->lcp.sat_id = it->second; + break; + } + case E_OR: + case E_AND: { + expr2literal(e->left.expr); + expr2literal(e->right.expr); + + SatExpr se(e->left.expr->lcp.sat_id, e->type, e->right.expr->lcp.sat_id); + auto it = expressions.find(se); + if (it == expressions.end()) { + literals.push_back(SatLiteral(e)); + expressions.insert(pair(se, literals.count())); + e->lcp.sat_id = literals.count(); + } else + e->lcp.sat_id = it->second; + break; + } + case E_EQUAL: + case E_UNEQUAL: + case E_LTH: + case E_LEQ: + case E_GTH: + case E_GEQ: { + SatExpr se(e->left.sym->lcp.sat_id, e->type, e->right.sym->lcp.sat_id); + auto it = expressions.find(se); + if (it == expressions.end()) { + literals.push_back(SatLiteral(e)); + expressions.insert(pair(se, literals.count())); + e->lcp.sat_id = literals.count(); + } else + e->lcp.sat_id = it->second; + 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; + } +} int main(int argc, char **argv) { @@ -300,18 +620,17 @@ int main(int argc, char **argv) textdomain(PACKAGE); conf_parse_path(kconfig); - SatData sat_data; - if (baseconf) conf_read(baseconf); + SatData sat_data; + if (varfile) read_varfile(varfile); if (dump) do_dump(); - if (cnf) { sat_data.write_dimacs_cnf(cnf); } diff --git a/kconfig2sat/lcp_data.h b/kconfig2sat/lcp_data.h index 251112a..eba47ab 100644 --- a/kconfig2sat/lcp_data.h +++ b/kconfig2sat/lcp_data.h @@ -5,13 +5,15 @@ /* linux-conf-perf data structures extensions */ +typedef int sat_id; /* Id of corresponding SAT literal */ + struct lcp_symbol { - int sat_id; - int variable:1; + sat_id sat_id; + int variable:1; /* SAT literal is variable (i.e. not fixed) */ }; struct lcp_expr { - int sat_id; + sat_id sat_id; }; -- 2.39.2