11 #include "kconfig/lkc.h"
12 #include "lcp_utils.h"
36 printf("Usage: kconfig2sat [options/actions]\n"
39 " -b, --baseconf <.config> Linux .config file with base configuration\n"
40 " --env <.conf.mk> Set env. variables such as ARCH from .conf.mk\n"
41 " -k, --kconfig <Kconfig> Kconfig file (with path)\n"
42 " --varfile <file> File listing variable options (one option per line)\n"
45 " --dump Dump internal data (for debugging)\n"
46 " --cnf <file> Generate CNF representation to <file>\n"
50 char *expr_to_string(struct expr *e);
52 char *sym_to_string(struct symbol *sym)
57 asprintf(&ret, sym->name);
59 asprintf(&ret, "NONAME%d", sym->lcp.sat_id);
63 char *expr_binop_to_string(struct expr *e, const char *op_str)
65 char *l = expr_to_string(e->left.expr);
66 char *r = expr_to_string(e->right.expr);
69 asprintf(&ret, "(%s %s %s)", l, op_str, r);
75 char *expr_comp_to_string(struct expr *e, const char *op_str)
77 char *l = sym_to_string(e->left.sym);
78 char *r = sym_to_string(e->right.sym);
81 asprintf(&ret, "(%s %s %s)", l, op_str, r);
87 char *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 tmp = expr_to_string(e->left.expr);
105 asprintf(&ret, "!%s", tmp);
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 return expr_comp_to_string(e, ">=");
121 fprintf(stderr, "LIST not implemented\n");
125 return sym_to_string(e->left.sym);
127 fprintf(stderr, "RANGE not implemented\n");
137 void dump_symbol(struct symbol *sym)
139 struct property *prop;
140 const char *name = sym_to_string(sym);
141 const char *type = sym_type_name(sym->type);
142 const char *prompt = NULL;
144 char flags[256] = "fl(";
147 if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
148 switch (sym->curr.tri) {
149 case no: val = 'n'; break;
150 case mod: val = 'm'; break;
151 case yes: val = 'y'; break;
155 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
172 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
175 for_all_properties(sym, prop, P_PROMPT) {
179 printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt);
182 if (sym->dir_dep.expr) {
183 tmp = expr_to_string(sym->dir_dep.expr);
184 printf(" depends %s\n", tmp);
188 for_all_properties(sym, prop, P_SELECT) {
189 assert(prop->expr->type == E_SYMBOL);
190 tmp = expr_to_string(prop->visible.expr);
191 printf(" selects %s if %s\n", prop->expr->left.sym->name, tmp);
202 for_all_symbols(i, sym) {
207 void read_varfile(const char *varfile)
209 FILE *f = fopen(varfile, "r");
218 while (fgets(line, sizeof(line), f)) {
222 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
223 p += strlen(CONFIG_);
225 const char *sym_name = strtok(p, " =\n");
226 struct symbol *sym = sym_find(sym_name);
228 fprintf(stderr, "%s:%d: Invalid symbol: %s\n", varfile, lineno, sym_name);
231 if (!(sym->flags & SYMBOL_WRITE)) {
232 fprintf(stderr, "%s:%d: Symbol %s not visible\n", varfile, lineno, sym_name);
235 if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
236 fprintf(stderr, "%s:%d: Choice values not yet supported: %s", varfile, lineno, sym_name);
239 struct property *prop;
240 const char *prompt = NULL;
241 for_all_properties(sym, prop, P_PROMPT) {
245 fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
247 sym->lcp.variable = 1;
256 SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
257 SatLiteral(struct expr *e) : sym(nullptr), expr(e) {}
260 typedef vector<sat_id> SatClause;
266 SatExpr(int l, enum expr_type o, int r)
267 : left(l), right(r), op(o) {}
268 bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
271 class SatLiterals : public vector<struct SatLiteral>
275 SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
276 int count() const { return size() - 1; }
282 * bool FOO!=y => !FOO
283 * bool FOO==n => !FOO
286 struct expr *expr_eliminate_eq_yn(struct expr *e)
294 e->left.expr = expr_eliminate_eq_yn(e->left.expr);
295 e->right.expr = expr_eliminate_eq_yn(e->right.expr);
298 // UNKNOWN symbols sometimes occur in dependency -
299 // e.g. ACPI_VIDEO on arm (the symbol is only defined
300 // for ACPI platforms (x86) but some drivers refer to
302 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
303 if (e->right.sym == &symbol_no) {
307 } else if (e->right.sym == &symbol_yes) {
311 e = expr_alloc_one(E_NOT, e);
316 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
317 if (e->right.sym == &symbol_yes) {
321 } else if (e->right.sym == &symbol_no) {
325 e = expr_alloc_one(E_NOT, e);
337 SatLiterals literals = {};
338 vector<SatClause> clauses = {};
339 map<SatExpr, sat_id> expressions = {};
341 void expr2literal(struct expr *e);
347 expressions2literals();
348 expressions2clauses();
351 void symbols2literals() {
355 for_all_symbols(i, sym) {
356 if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
357 literals.push_back(SatLiteral(sym));
358 sym->lcp.sat_id = literals.count();
363 void expressions2literals() {
366 struct property *prop;
368 for_all_symbols(i, sym) {
369 if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
370 sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
371 expr2literal(sym->dir_dep.expr);
373 for_all_properties(sym, prop, P_SELECT) {
374 assert(prop->expr->type == E_SYMBOL);
375 prop->visible.expr = expr_eliminate_eq_yn(prop->visible.expr);
376 expr2literal(prop->visible.expr);
382 void expressions2clauses() {
383 // Tseitin Transformation - see https://en.wikipedia.org/wiki/Tseitin_transformation
384 // or http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
385 for (auto expr: expressions) {
386 SatExpr e = expr.first;
387 sat_id e_id = expr.second;
394 clauses.push_back(SatClause{ e_id, e.left });
395 clauses.push_back(SatClause{ -e_id, -e.left });
398 clauses.push_back(SatClause{ -e.left, e_id });
399 clauses.push_back(SatClause{ -e.right, e_id });
400 clauses.push_back(SatClause{ -e_id, e.left, e.right });
403 clauses.push_back(SatClause{ -e_id, e.left });
404 clauses.push_back(SatClause{ -e_id, e.right });
405 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
408 clauses.push_back(SatClause{ -e_id, -e.left, e.right });
409 clauses.push_back(SatClause{ -e_id, -e.right, e.left });
410 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
411 clauses.push_back(SatClause{ e.left, e.right, e_id });
418 fprintf(stderr, "Comparison operators not implemented\n");
419 //exit(EXIT_FAILURE);
423 fprintf(stderr, "LIST not implemented\n");
427 fprintf(stderr, "RANGE not implemented\n");
435 void write_dimacs_cnf(const char *cnf) {
437 FILE *f = fopen(cnf, "w");
444 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
446 for (i = 1; i <= literals.count(); i++) {
447 SatLiteral &l = literals[i];
449 fprintf(f, "c SYM %d %s\n", l.sym->lcp.sat_id, l.sym->name);
450 if (l.sym->flags & SYMBOL_VALID && !l.sym->lcp.variable)
451 fprintf(f, "%d 0\n", l.sym->curr.tri != no ? l.sym->lcp.sat_id : -l.sym->lcp.sat_id);
454 char *tmp = expr_to_string(l.expr);
455 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.sat_id, tmp);
459 for (auto clause: clauses) {
460 for (sat_id id: clause)
461 fprintf(f, "%d ", id);
468 void none(struct expr *e)
472 void SatData::expr2literal(struct expr *e)
474 if (!e || e->lcp.sat_id)
479 e->lcp.sat_id = e->left.sym->lcp.sat_id;
482 fprintf(stderr, "NONE not implemented\n");
486 expr2literal(e->left.expr);
488 SatExpr se(e->left.expr->lcp.sat_id, e->type, 0);
489 auto it = expressions.find(se);
490 if (it == expressions.end()) {
491 literals.push_back(SatLiteral(e));
492 expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
493 e->lcp.sat_id = literals.count();
495 e->lcp.sat_id = it->second;
500 expr2literal(e->left.expr);
501 expr2literal(e->right.expr);
503 SatExpr se(e->left.expr->lcp.sat_id, e->type, e->right.expr->lcp.sat_id);
504 auto it = expressions.find(se);
505 if (it == expressions.end()) {
506 literals.push_back(SatLiteral(e));
507 expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
508 e->lcp.sat_id = literals.count();
510 e->lcp.sat_id = it->second;
519 SatExpr se(e->left.sym->lcp.sat_id, e->type, e->right.sym->lcp.sat_id);
520 auto it = expressions.find(se);
521 if (it == expressions.end()) {
522 literals.push_back(SatLiteral(e));
523 expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
524 e->lcp.sat_id = literals.count();
526 e->lcp.sat_id = it->second;
530 fprintf(stderr, "LIST not implemented\n");
534 fprintf(stderr, "RANGE not implemented\n");
540 int main(int argc, char **argv)
544 char *baseconf = NULL;
546 char *kconfig = NULL;
547 char *varfile = NULL;
551 int option_index = 0;
552 static struct option long_options[] = {
553 {"baseconf", required_argument, 0, OPT_BASECONFIG },
554 {"cnf", required_argument, 0, OPT_CNF },
555 {"env", required_argument, 0, OPT_ENV },
556 {"dump", no_argument, &dump, true },
557 {"help", no_argument, 0, OPT_HELP },
558 {"kconfig", required_argument, 0, OPT_KCONFIG },
559 {"varfile", required_argument, 0, OPT_VARFILE },
560 // {"varopt", required_argument, 0, OPT_VAROPTION },
561 {"verbose", no_argument, 0, OPT_VERBOSE },
565 c = getopt_long(argc, argv, "b:hk:v",
566 long_options, &option_index);
571 case 0: /* long option with flag != NULL */
581 set_missing_env(optarg);
602 printf("?? getopt returned character code 0%o ??\n", c);
607 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
613 if (kconfig == NULL) {
614 fprintf(stderr, "--kconfig option missing\n");
618 setlocale(LC_ALL, "");
619 bindtextdomain(PACKAGE, LOCALEDIR);
622 conf_parse_path(kconfig);
629 read_varfile(varfile);
635 sat_data.write_dimacs_cnf(cnf);
643 void build_symlist() {
646 struct property *prop;
647 for_all_symbols(i, sym) {
648 if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
649 if (sym->name == NULL)
650 asprintf(&sym->name, "NONAMEGEN%d", noname_num++);
652 symlist_add(gsymlist, sym->name);
655 symlist_closesym(gsymlist);
658 /* TODO: Split to smaller functions with meaningful names */
662 struct property *prop;
663 struct symlist_el *el;
665 struct boolexpr *boolsym;
666 for_all_symbols(i, sym) {
667 if (sym->type != S_BOOLEAN && sym->type != S_TRISTATE)
669 el_id = symlist_id(gsymlist, sym->name);
670 el = &(gsymlist->array[el_id - 1]);
671 boolsym = boolexpr_sym(gsymlist, sym, false, NULL);
672 Iprintf("Processing: %s\n", sym->name);
674 for_all_prompts(sym, prop) {
675 Dprintf(" Prompt: %s\n", prop->text);
676 if (prop->visible.expr != NULL) {
677 doutput_expr(prop->visible.expr);
678 struct boolexpr *vis =
679 boolexpr_kconfig(gsymlist, prop->visible.expr,
681 if (el->vis == NULL) {
684 el->vis = boolexpr_or(el->vis, vis);
686 } else if (el->vis == NULL) {
687 el->vis = boolexpr_true();
691 el->vis = boolexpr_false();
692 // Symbol is choice.. special treatment required
693 if (sym_is_choice(sym)) {
694 Dprintf(" Is Choice\n");
695 goto choice_exception;
698 struct boolexpr **defexpr = NULL;
699 size_t defexpr_size = 0;
701 bool exitdef = false;
702 for_all_defaults(sym, prop) {
703 Dprintf(" Default value:\n");
704 doutput_expr(prop->expr);
705 struct boolexpr *def =
706 boolexpr_kconfig(gsymlist, prop->expr, true, NULL);
707 struct boolexpr *vis;
708 if (prop->visible.expr != NULL)
709 vis = boolexpr_kconfig(gsymlist, prop->visible.expr,
712 vis = boolexpr_true();
713 if (vis->type != BT_TRUE) {
714 defexpr = realloc(defexpr,
715 ++defexpr_size * sizeof(struct boolexpr *));
716 defexpr[defexpr_size - 1] = boolexpr_copy(vis);
721 def = boolexpr_and(def, vis);
722 for (z = 0; z < ((int)defexpr_size - 1); z++) {
723 def = boolexpr_and(def, boolexpr_not(
724 boolexpr_copy(defexpr[z])));
729 el->def = boolexpr_or(el->def, def);
733 if (defexpr != NULL) {
734 for (z = 0; z < defexpr_size - 1; z++) {
735 boolexpr_free(defexpr[z]);
740 el->def = boolexpr_false();
741 // Dependency expression
742 if (sym->dir_dep.expr != NULL) {
743 Dprintf(" Dependency:\n");
744 doutput_expr(sym->dir_dep.expr);
746 boolexpr_kconfig(gsymlist, sym->dir_dep.expr, false, NULL);
748 el->dep = boolexpr_true();
749 // Reverse dependency expression
750 if (sym->rev_dep.expr != NULL) {
751 Dprintf(" Reverse dependency:\n");
752 doutput_expr(sym->rev_dep.expr);
754 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, false, NULL);
756 el->rev_dep = boolexpr_false();
758 if (el->dep->type != BT_FALSE && el->dep->type != BT_TRUE)
759 cnf_boolexpr(gsymlist, el->dep);
760 if (el->rev_dep->type != BT_FALSE
761 && el->rev_dep->type != BT_TRUE)
762 cnf_boolexpr(gsymlist, el->rev_dep);
763 if (el->def->type != BT_FALSE && el->def->type != BT_TRUE)
764 cnf_boolexpr(gsymlist, el->def);
765 if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
766 cnf_boolexpr(gsymlist, el->vis);
767 // (!sym || dep) && (sym || !rev_dep) &&
768 // && (sym || !dep || !def || vis) &&
769 // (!sym || rev_dep || def || vis)
770 if (el->dep->type != BT_TRUE) {
771 output_rules_symbol(-1 * boolsym->id);
772 if (el->dep->type != BT_FALSE) {
773 output_rules_symbol(el->dep->id);
775 output_rules_endterm();
777 if (el->rev_dep->type != BT_FALSE) {
778 output_rules_symbol(boolsym->id);
779 if (el->rev_dep->type != BT_TRUE) {
780 output_rules_symbol(-1 * el->rev_dep->id);
782 output_rules_endterm();
784 if (el->dep->type != BT_FALSE && el->def->type != BT_FALSE
785 && el->vis->type != BT_TRUE) {
786 output_rules_symbol(boolsym->id);
787 if (el->dep->type != BT_TRUE) {
788 output_rules_symbol(-1 * el->dep->id);
790 if (el->def->type != BT_TRUE) {
791 output_rules_symbol(-1 * el->def->id);
793 if (el->vis->type != BT_FALSE) {
794 output_rules_symbol(el->vis->id);
796 output_rules_endterm();
798 if (el->rev_dep->type != BT_TRUE && el->def->type != BT_TRUE
799 && el->vis->type != BT_TRUE) {
800 output_rules_symbol(-1 * boolsym->id);
801 if (el->rev_dep->type != BT_FALSE) {
802 output_rules_symbol(el->rev_dep->id);
804 if (el->def->type != BT_FALSE) {
805 output_rules_symbol(el->def->id);
807 if (el->vis->type != BT_FALSE) {
808 output_rules_symbol(el->vis->id);
810 output_rules_endterm();
813 boolexpr_free(el->def);
814 boolexpr_free(el->vis);
815 boolexpr_free(el->dep);
816 boolexpr_free(el->rev_dep);
821 // Add exclusive rules for choice symbol
822 if (sym->rev_dep.expr != NULL) {
823 Dprintf(" Dependency:\n");
824 doutput_expr(sym->rev_dep.expr);
826 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, true, NULL);
828 el->rev_dep = boolexpr_true();
829 for_all_choices(sym, prop) {
832 unsigned *symx = NULL;
833 size_t symx_size = 0;
835 expr_list_for_each_sym(prop->expr, exprw, symw) {
837 symx = realloc(symx, symx_size * sizeof(unsigned));
838 symx[symx_size - 1] = symlist_id(gsymlist, symw->name);
839 output_rules_symbol(symx[symx_size - 1]);
841 output_rules_symbol(-(int)
843 output_rules_endterm();
844 for (x = 0; x < symx_size - 1; x++) {
845 for (y = x + 1; y < symx_size; y++) {
846 output_rules_symbol(-(int)
848 output_rules_symbol(-(int)
850 output_rules_endterm();
856 if (el->rev_dep->type != BT_FALSE && el->rev_dep->type != BT_TRUE)
857 cnf_boolexpr(gsymlist, el->rev_dep);
858 if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
859 cnf_boolexpr(gsymlist, el->vis);
860 // (!sym || rev_dep) && (!sym || !rev_dep || vis)
861 // For nonoptional per list symbol add:
862 // (sym || !rev_dep || !vis || !dir_dep_of_list))
863 if (el->rev_dep->type != BT_TRUE) {
864 output_rules_symbol(-1 * boolsym->id);
865 if (el->rev_dep->type != BT_FALSE) {
866 output_rules_symbol(el->rev_dep->id);
868 output_rules_endterm();
870 if (el->rev_dep->type != BT_FALSE && el->vis->type != BT_TRUE) {
871 output_rules_symbol(-1 * boolsym->id);
872 if (el->rev_dep->type != BT_TRUE) {
873 output_rules_symbol(-1 * el->rev_dep->id);
875 if (el->vis != BT_FALSE) {
876 output_rules_symbol(el->vis->id);
878 output_rules_endterm();
880 if (!sym_is_optional(sym)) {
881 for_all_choices(sym, prop) {
884 expr_list_for_each_sym(prop->expr, exprw, symw) {
885 struct boolexpr *wdep;
886 if (symw->dir_dep.expr != NULL) {
887 struct symbol *settrue[] = {sym, NULL};
889 boolexpr_kconfig(gsymlist, symw->dir_dep.expr,
892 wdep = boolexpr_true();
893 cnf_boolexpr(gsymlist, wdep);
894 if (el->rev_dep->type != BT_FALSE
895 && el->vis->type != BT_FALSE
896 && wdep->type != BT_FALSE) {
897 output_rules_symbol(boolsym->id);
898 if (el->rev_dep->type != BT_TRUE) {
899 output_rules_symbol(-1 * el->rev_dep->id);
901 if (el->vis->type != BT_TRUE) {
902 output_rules_symbol(-1 * el->vis->id);
904 if (wdep->type != BT_TRUE
905 && wdep->id != boolsym->id) {
906 output_rules_symbol(-1 * wdep->id);
908 output_rules_endterm();