11 #include "kconfig/lkc.h"
12 #include "lcp_utils.h"
39 printf("Usage: kconfig2sat [options/actions]\n"
42 " -b, --baseconf <.config> Linux .config file with base configuration\n"
43 " --env <.conf.mk> Set env. variables such as ARCH from .conf.mk\n"
44 " -k, --kconfig <Kconfig> Kconfig file (with path)\n"
45 " --varfile <file> File listing variable options (one option per line)\n"
48 " --dump Dump internal data (for debugging)\n"
49 " --cnf <file> Generate CNF representation to <file>\n"
53 typedef unique_ptr<char> upchar;
55 upchar expr_to_string(struct expr *e);
57 upchar sym_to_string(struct symbol *sym)
62 asprintf(&ret, sym->name);
64 asprintf(&ret, "NONAME%d", sym->lcp.id);
68 upchar expr_binop_to_string(struct expr *e, const char *op_str)
70 upchar l = expr_to_string(e->left.expr);
71 upchar r = expr_to_string(e->right.expr);
74 asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
78 upchar expr_comp_to_string(struct expr *e, const char *op_str)
80 upchar l = sym_to_string(e->left.sym);
81 upchar r = sym_to_string(e->right.sym);
84 asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
88 upchar expr_to_string(struct expr *e)
97 asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr));
100 return expr_binop_to_string(e, "||");
102 return expr_binop_to_string(e, "&&");
104 asprintf(&ret, "!%s", expr_to_string(e->left.expr).get());
107 return expr_comp_to_string(e, "==");
109 return expr_comp_to_string(e, "!=");
111 return expr_comp_to_string(e, "<");
113 return expr_comp_to_string(e, "<=");
115 return expr_comp_to_string(e, ">");
117 return expr_comp_to_string(e, ">=");
119 fprintf(stderr, "LIST not implemented\n");
123 return sym_to_string(e->left.sym);
125 fprintf(stderr, "RANGE not implemented\n");
135 void dump_symbol(struct symbol *sym)
137 struct property *prop;
138 upchar name = sym_to_string(sym);
139 const char *type = sym_type_name(sym->type);
140 const char *prompt = NULL;
141 char flags[256] = "fl(";
144 if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
145 switch (sym->curr.tri) {
146 case no: val = 'n'; break;
147 case mod: val = 'm'; break;
148 case yes: val = 'y'; break;
152 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
169 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
172 for_all_properties(sym, prop, P_PROMPT) {
176 printf("%-40s %c %-8s %-50s %s\n", name.get(), val, type, flags, prompt);
179 if (sym->dir_dep.expr)
180 printf(" depends %s\n", expr_to_string(sym->dir_dep.expr).get());
182 for_all_properties(sym, prop, P_SELECT) {
183 assert(prop->expr->type == E_SYMBOL);
184 printf(" selects %s if %s\n", prop->expr->left.sym->name,
185 expr_to_string(prop->visible.expr).get());
194 for_all_symbols(i, sym) {
199 void mark_symbol_variable(const char *sym_name, const char *file, int lineno)
201 struct symbol *sym = sym_find(sym_name);
203 fprintf(stderr, "%s:%d: Error: Invalid symbol: %s\n", file, lineno, sym_name);
206 // if (!(sym->flags & SYMBOL_WRITE)) {
207 // fprintf(stderr, "%s:%d: Error: Symbol %s not visible\n", varfile, lineno, sym_name);
208 // exit(EXIT_FAILURE);
210 if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
211 fprintf(stderr, "%s:%d: Error: Choice values not yet supported: %s", file, lineno, sym_name);
214 struct property *prop;
215 const char *prompt = NULL;
216 for_all_properties(sym, prop, P_PROMPT) {
220 fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", file, lineno, sym_name);
222 sym->lcp.variable = 1;
225 void read_varfile(const char *varfile)
227 FILE *f = fopen(varfile, "r");
236 while (fgets(line, sizeof(line), f)) {
242 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
243 p += strlen(CONFIG_);
245 const char *sym_name = strtok(p, " =\n");
246 mark_symbol_variable(sym_name, varfile, lineno);
251 void set_all_symbols_variable()
256 for_all_symbols(i, sym) {
257 if (!(sym->flags & (SYMBOL_CONST | SYMBOL_AUTO)))
258 sym->lcp.variable = 1;
267 SatLiteral(struct symbol *s) : sym(s), expr(nullptr) { assert(sym->lcp.variable && sym->lcp.id); }
268 SatLiteral(struct expr *e) : sym(nullptr), expr(e) { assert(expr->lcp.variable && expr->lcp.id); }
269 sat_id id() const { return sym ? sym->lcp.id : expr->lcp.id; }
270 upchar name() const {
273 assert(sym->name); // TODO
274 asprintf(&ret, "%s", sym->name);
276 asprintf(&ret, "expr%d", expr->lcp.id);
282 typedef vector<sat_id> SatClause;
284 struct Implication: public SatClause {
285 Implication(sat_id a, sat_id b) : SatClause{-a, b} {}
292 SatExpr(sat_id l, enum expr_type o, sat_id r)
293 : left(l), right(r), op(o) {}
294 bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
297 class SatLiterals : protected vector<struct SatLiteral>
300 using vector<struct SatLiteral>::begin;
301 using vector<struct SatLiteral>::end;
302 using vector<struct SatLiteral>::push_back;
303 SatLiterals() { reserve(20000); }
304 int count() const { return size(); }
305 const SatLiteral &operator[](size_type i) const { return at(i-1); }
306 SatLiteral &last() { return *(--end()); }
307 bool test_set_dot_printed(struct symbol *sym) const {
308 auto l = (*this)[sym->lcp.id];
309 bool ret = l.dot_printed;
313 bool test_set_dot_printed(struct expr *e) const {
314 auto l = (*this)[e->lcp.id];
315 bool ret = l.dot_printed;
323 * bool FOO!=y => !FOO
324 * bool FOO==n => !FOO
327 struct expr *expr_eliminate_eq_yn(struct expr *e)
335 e->left.expr = expr_eliminate_eq_yn(e->left.expr);
336 e->right.expr = expr_eliminate_eq_yn(e->right.expr);
339 // UNKNOWN symbols sometimes occur in dependency -
340 // e.g. ACPI_VIDEO on arm (the symbol is only defined
341 // for ACPI platforms (x86) but some drivers refer to
343 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
344 if (e->right.sym == &symbol_no) {
348 } else if (e->right.sym == &symbol_yes) {
352 e = expr_alloc_one(E_NOT, e);
357 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
358 if (e->right.sym == &symbol_yes) {
362 } else if (e->right.sym == &symbol_no) {
366 e = expr_alloc_one(E_NOT, e);
376 bool mark_variable_expressions(struct expr *e)
383 return (e->lcp.variable = e->left.sym->lcp.variable);
385 fprintf(stderr, "NONE not implemented\n");
389 if (mark_variable_expressions(e->left.expr))
390 return (e->lcp.variable = 1);
395 mark_variable_expressions(e->left.expr);
396 mark_variable_expressions(e->right.expr);
398 if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
399 return (e->lcp.variable = 1);
400 } else if (!e->left.expr->lcp.variable && !e->right.expr->lcp.variable) {
401 return (e->lcp.variable = 0);
405 if (e->left.expr->lcp.variable) {
406 val = expr_calc_value(e->right.expr);
407 } else if (e->right.expr->lcp.variable) {
408 val = expr_calc_value(e->left.expr);
410 if ((e->type == E_OR && val == yes) ||
411 (e->type == E_AND && val == no))
412 return (e->lcp.variable = 0);
414 return (e->lcp.variable = 1);
416 __builtin_unreachable();
420 if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
421 return (e->lcp.variable = 1);
422 } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
423 fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
431 if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
432 fprintf(stderr, "Comparison of variable symbols not implemented\n");
438 fprintf(stderr, "LIST not implemented\n");
442 fprintf(stderr, "RANGE not implemented\n");
446 fprintf(stderr, "Unexpected situation in mark_variable_expressions\n");
450 void mark_variable_expressions()
454 struct property *prop;
456 for_all_symbols(i, sym) {
457 mark_variable_expressions(sym->dir_dep.expr);
458 mark_variable_expressions(sym->rev_dep.expr);
459 for_all_properties(sym, prop, P_SELECT) {
460 assert(prop->expr->type == E_SYMBOL);
461 mark_variable_expressions(prop->visible.expr);
466 void check_dep_consistency()
472 for_all_symbols(i, sym) {
473 if (sym->lcp.variable && sym->dir_dep.expr && !sym->dir_dep.expr->lcp.variable) {
474 val = expr_calc_value(sym->dir_dep.expr);
476 fprintf(stderr, "Symbol %s cannot be variable because its dependency is always 'no': %s\n",
477 sym->name, expr_to_string(sym->dir_dep.expr).get());
481 if (sym->lcp.variable && sym->rev_dep.expr && !sym->rev_dep.expr->lcp.variable) {
482 val = expr_calc_value(sym->rev_dep.expr);
484 fprintf(stderr, "Symbol %s cannot be variable because it is selected by expression that is always 'yes': %s\n",
485 sym->name, expr_to_string(sym->rev_dep.expr).get());
489 if (!sym->lcp.variable && (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) &&
490 sym->curr.tri == no && sym->rev_dep.expr && sym->rev_dep.expr->lcp.variable) {
491 fprintf(stderr, "Symbol %s cannot be fixed to 'no', because it is selcted by variable expression '%s'\n",
492 sym->name, expr_to_string(sym->rev_dep.expr).get());
501 void symbol(struct symbol *sym) {
502 const char *opts = "";
503 if (sym->lcp.variable)
504 opts = " [penwidth=3]";
506 opts = " [color=gray]";
507 fprintf(f, "\"%s\"%s;\n", sym->name, opts);
509 void expr(struct expr *e, upchar name) {
510 const char *label = "???";
512 case E_OR: label = "|"; break;
513 case E_AND: label = "&"; break;
514 case E_EQUAL: label = "="; break;
515 case E_UNEQUAL: label = "!="; break;
516 case E_NOT: label = "!"; break;
526 fprintf(stderr, "Expr %d not implemented\n", e->type);
531 fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", name.get(), label);
534 DotWriter(const char *file_name) {
535 f = fopen(file_name, "w");
542 fprintf(f, "digraph conf {\n");
543 //fprintf(f, "rankdir=LR;\n");
549 void literal(SatLiteral &l) {
556 expr(l.expr, l.name());
558 void depends_on(const SatLiteral &l1, const SatLiteral &l2) {
559 fprintf(f, "\"%s\" -> \"%s\" [style=bold,label=d];\n", l1.name().get(), l2.name().get());
561 void selects(const SatLiteral &l1, const SatLiteral &l2) {
562 fprintf(f, "\"%s\" -> \"%s\" [style=bold,arrowhead=open,label=s];\n", l1.name().get(), l2.name().get());
564 void edge(const SatLiteral &from, const SatLiteral &to) {
565 fprintf(f, "\"%s\" -> \"%s\" [arrowhead=empty];\n", from.name().get(), to.name().get());
570 SatLiterals literals = {};
571 vector<SatClause> clauses = {};
572 map<SatExpr, sat_id> expressions = {};
573 DotWriter *dot = nullptr;
576 SatData(const char *dot_fn) {
578 dot = new DotWriter(dot_fn);
580 expressions2literals();
581 expressions2clauses();
587 const SatLiteral &add_literal(struct symbol *sym) {
588 sym->lcp.id = literals.count() + 1;
589 literals.push_back(SatLiteral(sym));
591 dot->literal(literals.last());
592 return literals.last();
595 const SatLiteral &add_literal(struct expr *e) {
596 e->lcp.id = literals.count() + 1;
597 literals.push_back(SatLiteral(e));
599 dot->literal(literals.last());
600 return literals.last();
603 void symbols2literals() {
607 for_all_symbols(i, sym) {
608 if (sym->lcp.variable)
613 // Assign e->lcp.id to variable literals
614 sat_id expr2literal(struct expr *e) {
615 if (!e || !e->lcp.variable)
622 assert(e->left.sym->lcp.id);
623 e->lcp.id = e->left.sym->lcp.id;
626 fprintf(stderr, "NONE not implemented\n");
630 expr2literal(e->left.expr);
632 SatExpr se(e->left.expr->lcp.id, e->type, 0);
633 auto it = expressions.find(se);
634 if (it == expressions.end()) {
635 auto l = add_literal(e);
636 expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
638 dot->edge(literals[e->left.expr->lcp.id], l);
640 e->lcp.id = it->second;
645 expr2literal(e->left.expr);
646 expr2literal(e->right.expr);
648 if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
649 SatExpr se = SatExpr(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id);
650 auto it = expressions.find(se);
651 if (it == expressions.end()) {
652 auto l = add_literal(e);
653 expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
655 dot->edge(literals[e->left.expr->lcp.id], l);
656 dot->edge(literals[e->right.expr->lcp.id], l);
659 e->lcp.id = it->second;
661 if (e->left.expr->lcp.variable) {
662 e->lcp.id = e->left.expr->lcp.id;
663 } else if (e->right.expr->lcp.variable) {
664 e->lcp.id = e->right.expr->lcp.id;
671 if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
672 SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id);
673 auto it = expressions.find(se);
674 if (it == expressions.end()) {
675 auto l = add_literal(e);
676 expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
678 dot->edge(literals[e->left.sym->lcp.id], l);
679 dot->edge(literals[e->right.sym->lcp.id], l);
682 e->lcp.id = it->second;
683 } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
684 fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
693 if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
694 fprintf(stderr, "Comparison of variable symbols not implemented\n");
699 fprintf(stderr, "LIST not implemented\n");
703 fprintf(stderr, "RANGE not implemented\n");
711 void expressions2literals() {
716 const SatLiteral *syml;
718 for_all_symbols(i, sym) {
719 if (sym->lcp.variable &&
720 (sym->type == S_BOOLEAN || sym->type == S_TRISTATE)) {
721 syml = &literals[sym->lcp.id];
722 // Direct dependencies
723 //sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
724 e = sym->dir_dep.expr;
725 id = expr2literal(e);
727 clauses.push_back(Implication(sym->lcp.id, id));
729 dot->depends_on(*syml, literals[id]);
732 // Reverse dependecies
733 e = sym->rev_dep.expr;
734 id = expr2literal(e);
736 clauses.push_back(Implication(id, sym->lcp.id));
738 dot->selects(literals[id], *syml);
744 // Tseitin Transformation - see
745 // https://en.wikipedia.org/wiki/Tseitin_transformation or
746 // http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
747 void expressions2clauses() {
748 for (auto expr: expressions) {
749 SatExpr e = expr.first;
750 sat_id e_id = expr.second;
752 if (e.left == 0 || (e.right == 0 && e.op != E_NOT)) {
753 upchar tmp(expr_to_string(literals[e_id].expr));
754 printf("Unexpected sat_id == 0 in %s\n", tmp.get());
763 clauses.push_back(SatClause{ e_id, e.left });
764 clauses.push_back(SatClause{ -e_id, -e.left });
767 clauses.push_back(SatClause{ -e.left, e_id });
768 clauses.push_back(SatClause{ -e.right, e_id });
769 clauses.push_back(SatClause{ -e_id, e.left, e.right });
772 clauses.push_back(SatClause{ -e_id, e.left });
773 clauses.push_back(SatClause{ -e_id, e.right });
774 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
777 clauses.push_back(SatClause{ -e_id, -e.left, e.right });
778 clauses.push_back(SatClause{ -e_id, -e.right, e.left });
779 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
780 clauses.push_back(SatClause{ e.left, e.right, e_id });
783 clauses.push_back(SatClause{ -e_id, -e.left, -e.right });
784 clauses.push_back(SatClause{ -e_id, e.right, e.left });
785 clauses.push_back(SatClause{ -e.left, e.right, e_id });
786 clauses.push_back(SatClause{ e.left, -e.right, e_id });
792 struct expr *e = literals[e_id].expr;
793 upchar tmp(expr_to_string(e));
794 tristate val = expr_calc_value(e);
795 //fprintf(stderr, "Comparison operators not implemented %s = %d\n", tmp.get(), val);
796 //exit(EXIT_FAILURE);
797 clauses.push_back(SatClause{ val == yes ? e_id : -e_id });
801 fprintf(stderr, "LIST not implemented\n");
805 fprintf(stderr, "RANGE not implemented\n");
813 void write_dimacs_cnf(const char *cnf) {
814 FILE *f = fopen(cnf, "w");
821 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size());
823 for (auto l: literals) {
825 fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
827 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
829 for (auto clause: clauses) {
830 for (sat_id id: clause) {
832 fprintf(f, "%d ", id);
841 int main(int argc, char **argv)
845 char *baseconf = NULL;
848 char *kconfig = NULL;
849 char *varfile = NULL;
851 deque<string> varopts;
854 int option_index = 0;
855 static struct option long_options[] = {
856 {"baseconf", required_argument, 0, OPT_BASECONFIG },
857 {"cnf", required_argument, 0, OPT_CNF },
858 {"dot", required_argument, 0, OPT_DOT },
859 {"env", required_argument, 0, OPT_ENV },
860 {"dump", no_argument, &dump, true },
861 {"help", no_argument, 0, OPT_HELP },
862 {"kconfig", required_argument, 0, OPT_KCONFIG },
863 {"varfile", required_argument, 0, OPT_VARFILE },
864 {"varopt", required_argument, 0, OPT_VAROPTION },
865 {"verbose", no_argument, 0, OPT_VERBOSE },
869 c = getopt_long(argc, argv, "b:hk:v",
870 long_options, &option_index);
875 case 0: /* long option with flag != NULL */
888 set_missing_env(optarg);
906 varopts.push_back(string(optarg));
912 printf("?? getopt returned character code 0%o ??\n", c);
917 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
923 if (kconfig == NULL) {
924 fprintf(stderr, "--kconfig option missing\n");
928 setlocale(LC_ALL, "");
929 bindtextdomain(PACKAGE, LOCALEDIR);
932 conf_parse_path(kconfig);
936 if (!varfile && varopts.empty())
937 set_all_symbols_variable();
940 read_varfile(varfile);
941 if (!varopts.empty())
942 for (auto o: varopts)
943 mark_symbol_variable(o.c_str(), NULL, 0);
946 mark_variable_expressions();
947 check_dep_consistency();
949 SatData sat_data(dot);
955 sat_data.write_dimacs_cnf(cnf);