kconfig2sat/kconfig2sat.cc

   1 #include <stdio.h>
   2 #include <stdlib.h>
   3 #include <string.h>
   4 #include <locale.h>
   5 #include <stdbool.h>
   6 #include <libintl.h>
   7 #include <unistd.h>
   8 #include <getopt.h>
   9 #include <inttypes.h>
  10
  11 #include "kconfig/lkc.h"
  12 #include "lcp_utils.h"
  13
  14 #include <vector>
  15 #include <map>
  16
  17 using namespace std;
  18
  19 int verbosity = 0;
  20
  21 enum options {
  22         OPT__START = 256,
  23         OPT_BASECONFIG,
  24         OPT_CNF,
  25         OPT_DUMP,
  26         OPT_ENV,
  27         OPT_HELP,
  28         OPT_KCONFIG,
  29         OPT_VARFILE,
  30         OPT_VAROPTION,
  31         OPT_VERBOSE,
  32 };
  33
  34 void print_help()
  35 {
  36         printf("Usage: kconfig2sat [options/actions]\n"
  37                "\n"
  38                "Options:\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"
  43                "\n"
  44                "Actions:\n"
  45                "  --dump                    Dump internal data (for debugging)\n"
  46                "  --cnf <file>              Generate CNF representation to <file>\n"
  47                 );
  48 }
  49
  50 char *expr_to_string(struct expr *e);
  51
  52 char *sym_to_string(struct symbol *sym)
  53 {
  54         char *ret;
  55
  56         if (sym->name)
  57                 asprintf(&ret, sym->name);
  58         else
  59                 asprintf(&ret, "NONAME%d", sym->lcp.sat_id);
  60         return ret;
  61 }
  62
  63 char *expr_binop_to_string(struct expr *e, const char *op_str)
  64 {
  65         char *l = expr_to_string(e->left.expr);
  66         char *r = expr_to_string(e->right.expr);
  67         char *ret;
  68
  69         asprintf(&ret, "(%s %s %s)", l, op_str, r);
  70         free(l);
  71         free(r);
  72         return ret;
  73 }
  74
  75 char *expr_comp_to_string(struct expr *e, const char *op_str)
  76 {
  77         char *l = sym_to_string(e->left.sym);
  78         char *r = sym_to_string(e->right.sym);
  79         char *ret;
  80
  81         asprintf(&ret, "(%s %s %s)", l, op_str, r);
  82         free(l);
  83         free(r);
  84         return ret;
  85 }
  86
  87 char *expr_to_string(struct expr *e)
  88 {
  89         char *ret = NULL;
  90         char *tmp;
  91
  92         if (!e)
  93                 return NULL;
  94
  95         switch (e->type) {
  96         case E_NONE:
  97                 asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr));
  98                 return ret;
  99         case E_OR:
 100                 return expr_binop_to_string(e, "||");
 101         case E_AND:
 102                 return expr_binop_to_string(e, "&&");
 103         case E_NOT:
 104                 tmp = expr_to_string(e->left.expr);
 105                 asprintf(&ret, "!%s", tmp);
 106                 free(tmp);
 107                 return ret;
 108         case E_EQUAL:
 109                 return expr_comp_to_string(e, "==");
 110         case E_UNEQUAL:
 111                 return expr_comp_to_string(e, "!=");
 112         case E_LTH:
 113                 return expr_comp_to_string(e, "<");
 114         case E_LEQ:
 115                 return expr_comp_to_string(e, "<=");
 116         case E_GTH:
 117                 return expr_comp_to_string(e, ">");
 118         case E_GEQ:
 119                 return expr_comp_to_string(e, ">=");
 120         case E_LIST:
 121                 fprintf(stderr, "LIST not implemented\n");
 122                 exit(EXIT_FAILURE);
 123                 break;
 124         case E_SYMBOL:
 125                 return sym_to_string(e->left.sym);
 126         case E_RANGE:
 127                 fprintf(stderr, "RANGE not implemented\n");
 128                 exit(EXIT_FAILURE);
 129                 break;
 130         }
 131
 132         return ret;
 133 }
 134
 135
 136
 137 void dump_symbol(struct symbol *sym)
 138 {
 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;
 143         char *tmp;
 144         char flags[256] = "fl(";
 145         char val = '.';
 146
 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;
 152                 }
 153         }
 154
 155 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
 156         FLAG(CONST);
 157         FLAG(CHECK);
 158         FLAG(CHOICE);
 159         FLAG(CHOICEVAL);
 160         FLAG(VALID);
 161         FLAG(OPTIONAL);
 162         FLAG(WRITE);
 163         FLAG(CHANGED);
 164         FLAG(AUTO);
 165         FLAG(CHECKED);
 166         FLAG(WARNED);
 167         FLAG(DEF_USER);
 168         FLAG(DEF_AUTO);
 169         FLAG(DEF3);
 170         FLAG(DEF4);
 171         if (flags[3])
 172                 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
 173 #undef FLAG
 174
 175         for_all_properties(sym, prop, P_PROMPT) {
 176                 prompt = prop->text;
 177         }
 178
 179         printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt);
 180
 181         if (verbosity > 0) {
 182                 if (sym->dir_dep.expr) {
 183                         tmp = expr_to_string(sym->dir_dep.expr);
 184                         printf("    depends %s\n", tmp);
 185                         free(tmp);
 186                 }
 187
 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);
 192                         free(tmp);
 193
 194                 }
 195         }
 196 }
 197
 198 void do_dump()
 199 {
 200     int i;
 201     struct symbol *sym;
 202     for_all_symbols(i, sym) {
 203             dump_symbol(sym);
 204     }
 205 }
 206
 207 void read_varfile(const char *varfile)
 208 {
 209         FILE *f = fopen(varfile, "r");
 210         char line[1000];
 211
 212         if (!f) {
 213                 perror(varfile);
 214                 exit(EXIT_FAILURE);
 215         }
 216
 217         int lineno = 0;
 218         while (fgets(line, sizeof(line), f)) {
 219                 char *p = line;
 220                 lineno++;
 221
 222                 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
 223                         p += strlen(CONFIG_);
 224
 225                 const char *sym_name = strtok(p, " =\n");
 226                 struct symbol *sym = sym_find(sym_name);
 227                 if (!sym) {
 228                         fprintf(stderr, "%s:%d: Invalid symbol: %s\n", varfile, lineno, sym_name);
 229                         exit(EXIT_FAILURE);
 230                 }
 231                 if (!(sym->flags & SYMBOL_WRITE)) {
 232                         fprintf(stderr, "%s:%d: Symbol %s not visible\n", varfile, lineno, sym_name);
 233                         exit(EXIT_FAILURE);
 234                 }
 235                 if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
 236                         fprintf(stderr, "%s:%d: Choice values not yet supported: %s", varfile, lineno, sym_name);
 237                         exit(EXIT_FAILURE);
 238                 }
 239                 struct property *prop;
 240                 const char *prompt = NULL;
 241                 for_all_properties(sym, prop, P_PROMPT) {
 242                         prompt = prop->text;
 243                 }
 244                 if (!prompt) {
 245                         fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
 246                 }
 247                 sym->lcp.variable = 1;
 248         }
 249         fclose(f);
 250 }
 251
 252 struct SatLiteral {
 253         struct symbol *sym;
 254         struct expr *expr;
 255
 256         SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
 257         SatLiteral(struct expr *e)   : sym(nullptr), expr(e) {}
 258 };
 259
 260 typedef vector<sat_id> SatClause;
 261
 262 struct SatExpr {
 263         sat_id left, right;
 264         enum expr_type op;
 265
 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); }
 269 };
 270
 271 class SatLiterals : public vector<struct SatLiteral>
 272 {
 273 public:
 274         int fixed = {0};
 275         SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
 276         int count() const { return size() - 1; }
 277 };
 278
 279
 280 /*
 281  * bool FOO!=n => FOO
 282  * bool FOO!=y => !FOO
 283  * bool FOO==n => !FOO
 284  * bool FOO==y => FOO
 285  */
 286 struct expr *expr_eliminate_eq_yn(struct expr *e)
 287 {
 288         if (!e)
 289                 return NULL;
 290         switch (e->type) {
 291         case E_AND:
 292         case E_OR:
 293         case E_NOT:
 294                 e->left.expr = expr_eliminate_eq_yn(e->left.expr);
 295                 e->right.expr = expr_eliminate_eq_yn(e->right.expr);
 296                 break;
 297         case E_UNEQUAL:
 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
 301                 // it.
 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) {
 304                                 // FOO!=n -> FOO
 305                                 e->type = E_SYMBOL;
 306                                 e->right.sym = NULL;
 307                         } else if (e->right.sym == &symbol_yes) {
 308                                 // FOO!=y -> !FOO
 309                                 e->type = E_SYMBOL;
 310                                 e->right.sym = NULL;
 311                                 e = expr_alloc_one(E_NOT, e);
 312                         }
 313                 }
 314                 break;
 315         case E_EQUAL:
 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) {
 318                                 // FOO==y -> FOO
 319                                 e->type = E_SYMBOL;
 320                                 e->right.sym = NULL;
 321                         } else if (e->right.sym == &symbol_no) {
 322                                 // FOO==n -> !FOO
 323                                 e->type = E_SYMBOL;
 324                                 e->right.sym = NULL;
 325                                 e = expr_alloc_one(E_NOT, e);
 326                         }
 327                 }
 328                 break;
 329         default:
 330                 ;
 331         }
 332         return e;
 333 }
 334
 335
 336 class SatData {
 337         SatLiterals literals = {};
 338         vector<SatClause> clauses = {};
 339         map<SatExpr, sat_id> expressions = {};
 340
 341         void expr2literal(struct expr *e);
 342
 343 public:
 344
 345         SatData() {
 346                 symbols2literals();
 347                 expressions2literals();
 348                 expressions2clauses();
 349         }
 350
 351         void symbols2literals() {
 352                 int i;
 353                 struct symbol *sym;
 354
 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();
 359                         }
 360                 }
 361         }
 362
 363         void expressions2literals() {
 364                 int i;
 365                 struct symbol *sym;
 366                 struct property *prop;
 367
 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);
 372
 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);
 377                                 }
 378                         }
 379                 }
 380         }
 381
 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;
 388                         switch (e.op) {
 389                         case E_SYMBOL:
 390                         case E_NONE:
 391                                 assert(0);
 392                                 break;
 393                         case E_NOT:
 394                                 clauses.push_back(SatClause{  e_id,  e.left });
 395                                 clauses.push_back(SatClause{ -e_id, -e.left });
 396                                 break;
 397                         case E_OR:
 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 });
 401                                 break;
 402                         case E_AND:
 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 });
 406                                 break;
 407                         case E_EQUAL:
 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 });
 412                                 break;
 413                         case E_UNEQUAL:
 414                         case E_LTH:
 415                         case E_LEQ:
 416                         case E_GTH:
 417                         case E_GEQ: {
 418                                 fprintf(stderr, "Comparison operators not implemented\n");
 419                                 //exit(EXIT_FAILURE);
 420                                 break;
 421                         }
 422                         case E_LIST:
 423                                 fprintf(stderr, "LIST not implemented\n");
 424                                 exit(EXIT_FAILURE);
 425                                 break;
 426                         case E_RANGE:
 427                                 fprintf(stderr, "RANGE not implemented\n");
 428                                 exit(EXIT_FAILURE);
 429                                 break;
 430                         }
 431                 }
 432
 433         }
 434
 435         void write_dimacs_cnf(const char *cnf) {
 436                 int i;
 437                 FILE *f = fopen(cnf, "w");
 438
 439                 if (!f) {
 440                         perror(cnf);
 441                         exit(EXIT_FAILURE);
 442                 }
 443
 444                 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
 445
 446                 for (i = 1; i <= literals.count(); i++) {
 447                         SatLiteral &l = literals[i];
 448                         if (l.sym) {
 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);
 452                         }
 453                         if (l.expr) {
 454                                 char *tmp = expr_to_string(l.expr);
 455                                 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.sat_id, tmp);
 456                                 free(tmp);
 457                         }
 458                 }
 459                 for (auto clause: clauses) {
 460                         for (sat_id id: clause)
 461                                 fprintf(f, "%d ", id);
 462                         fprintf(f, "0\n");
 463                 }
 464                 fclose(f);
 465         }
 466 };
 467
 468 void none(struct expr *e)
 469 {
 470 }
 471
 472 void SatData::expr2literal(struct expr *e)
 473 {
 474         if (!e || e->lcp.sat_id)
 475                 return;
 476
 477         switch (e->type) {
 478         case E_SYMBOL:
 479                 e->lcp.sat_id = e->left.sym->lcp.sat_id;
 480                 break;
 481         case E_NONE:
 482                 fprintf(stderr, "NONE not implemented\n");
 483                 exit(EXIT_FAILURE);
 484                 break;
 485         case E_NOT: {
 486                 expr2literal(e->left.expr);
 487
 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();
 494                 } else
 495                         e->lcp.sat_id = it->second;
 496                 break;
 497         }
 498         case E_OR:
 499         case E_AND: {
 500                 expr2literal(e->left.expr);
 501                 expr2literal(e->right.expr);
 502
 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();
 509                 } else
 510                         e->lcp.sat_id = it->second;
 511                 break;
 512         }
 513         case E_EQUAL:
 514         case E_UNEQUAL:
 515         case E_LTH:
 516         case E_LEQ:
 517         case E_GTH:
 518         case E_GEQ: {
 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();
 525                 } else
 526                         e->lcp.sat_id = it->second;
 527                 break;
 528         }
 529         case E_LIST:
 530                 fprintf(stderr, "LIST not implemented\n");
 531                 exit(EXIT_FAILURE);
 532                 break;
 533         case E_RANGE:
 534                 fprintf(stderr, "RANGE not implemented\n");
 535                 exit(EXIT_FAILURE);
 536                 break;
 537         }
 538 }
 539
 540 int main(int argc, char **argv)
 541 {
 542         int c;
 543
 544         char *baseconf = NULL;
 545         char *cnf = NULL;
 546         char *kconfig = NULL;
 547         char *varfile = NULL;
 548         int  dump = false;
 549
 550         while (1) {
 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 },
 562                         {0,             0,                 0,     0 }
 563                 };
 564
 565                 c = getopt_long(argc, argv, "b:hk:v",
 566                                 long_options, &option_index);
 567                 if (c == -1)
 568                         break;
 569
 570                 switch (c) {
 571                 case 0: /* long option with flag != NULL */
 572                         break;
 573                 case 'b':
 574                 case OPT_BASECONFIG:
 575                         baseconf = optarg;
 576                         break;
 577                 case OPT_CNF:
 578                         cnf = optarg;
 579                         break;
 580                 case OPT_ENV:
 581                         set_missing_env(optarg);
 582                         break;
 583                 case 'h':
 584                 case OPT_HELP:
 585                         print_help();
 586                         exit(EXIT_SUCCESS);
 587                 case 'k':
 588                 case OPT_KCONFIG:
 589                         kconfig = optarg;
 590                         break;
 591                 case 'v':
 592                 case OPT_VERBOSE:
 593                         verbosity++;
 594                         break;
 595                 case OPT_VARFILE:
 596                         varfile = optarg;
 597                         break;
 598                 case '?':
 599                 default:
 600                         print_help();
 601                         exit(EXIT_FAILURE);
 602                         printf("?? getopt returned character code 0%o ??\n", c);
 603                 }
 604         }
 605
 606         if (optind < argc) {
 607                 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
 608                 print_help();
 609                 exit(EXIT_FAILURE);
 610         }
 611
 612
 613         if (kconfig == NULL) {
 614                 fprintf(stderr, "--kconfig option missing\n");
 615                 exit(EXIT_FAILURE);
 616         }
 617
 618         setlocale(LC_ALL, "");
 619         bindtextdomain(PACKAGE, LOCALEDIR);
 620         textdomain(PACKAGE);
 621
 622         conf_parse_path(kconfig);
 623         if (baseconf)
 624                 conf_read(baseconf);
 625
 626         SatData sat_data;
 627
 628         if (varfile)
 629                 read_varfile(varfile);
 630
 631         if (dump)
 632                 do_dump();
 633
 634         if (cnf) {
 635                 sat_data.write_dimacs_cnf(cnf);
 636         }
 637
 638         return EXIT_SUCCESS;
 639 }
 640
 641 #if 0
 642
 643 void build_symlist() {
 644     int i;
 645     struct symbol *sym;
 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++);
 651
 652             symlist_add(gsymlist, sym->name);
 653         }
 654     }
 655     symlist_closesym(gsymlist);
 656 }
 657
 658 /* TODO: Split to smaller functions with meaningful names */
 659 void cpy_dep() {
 660     int i;
 661     struct symbol *sym;
 662     struct property *prop;
 663     struct symlist_el *el;
 664     unsigned el_id;
 665     struct boolexpr *boolsym;
 666     for_all_symbols(i, sym) {
 667         if (sym->type != S_BOOLEAN && sym->type != S_TRISTATE)
 668             continue;
 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);
 673         // Visibility
 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,
 680                                      false, NULL);
 681                 if (el->vis == NULL) {
 682                     el->vis = vis;
 683                 } else {
 684                     el->vis = boolexpr_or(el->vis, vis);
 685                 }
 686             } else if (el->vis == NULL) {
 687                 el->vis = boolexpr_true();
 688             }
 689         }
 690         if (el->vis == NULL)
 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;
 696         }
 697         // Default value
 698         struct boolexpr **defexpr = NULL;
 699         size_t defexpr_size = 0;
 700         int z;
 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,
 710                                        false, NULL);
 711             else
 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);
 717             } else {
 718                 ++defexpr_size;
 719                 exitdef = true;
 720             }
 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])));
 725             }
 726             if (el->def == NULL)
 727                 el->def = def;
 728             else
 729                 el->def = boolexpr_or(el->def, def);
 730             if (exitdef)
 731                 break;
 732         }
 733         if (defexpr != NULL) {
 734             for (z = 0; z < defexpr_size - 1; z++) {
 735                 boolexpr_free(defexpr[z]);
 736             }
 737             free(defexpr);
 738         }
 739         if (el->def == NULL)
 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);
 745             el->dep =
 746                 boolexpr_kconfig(gsymlist, sym->dir_dep.expr, false, NULL);
 747         } else
 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);
 753             el->rev_dep =
 754                 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, false, NULL);
 755         } else
 756             el->rev_dep = boolexpr_false();
 757
 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);
 774             }
 775             output_rules_endterm();
 776         }
 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);
 781             }
 782             output_rules_endterm();
 783         }
 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);
 789             }
 790             if (el->def->type != BT_TRUE) {
 791                 output_rules_symbol(-1 * el->def->id);
 792             }
 793             if (el->vis->type != BT_FALSE) {
 794                 output_rules_symbol(el->vis->id);
 795             }
 796             output_rules_endterm();
 797         }
 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);
 803             }
 804             if (el->def->type != BT_FALSE) {
 805                 output_rules_symbol(el->def->id);
 806             }
 807             if (el->vis->type != BT_FALSE) {
 808                 output_rules_symbol(el->vis->id);
 809             }
 810             output_rules_endterm();
 811         }
 812
 813         boolexpr_free(el->def);
 814         boolexpr_free(el->vis);
 815         boolexpr_free(el->dep);
 816         boolexpr_free(el->rev_dep);
 817
 818         continue;
 819
 820     choice_exception:
 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);
 825             el->rev_dep =
 826                 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, true, NULL);
 827         } else
 828             el->rev_dep = boolexpr_true();
 829         for_all_choices(sym, prop) {
 830             struct symbol *symw;
 831             struct expr *exprw;
 832             unsigned *symx = NULL;
 833             size_t symx_size = 0;
 834             int x, y;
 835             expr_list_for_each_sym(prop->expr, exprw, symw) {
 836                 symx_size++;
 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]);
 840             }
 841             output_rules_symbol(-(int)
 842                                 el_id);
 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)
 847                                         symx[x]);
 848                     output_rules_symbol(-(int)
 849                                         symx[y]);
 850                     output_rules_endterm();
 851                 }
 852             }
 853             free(symx);
 854             symx = NULL;
 855         }
 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);
 867             }
 868             output_rules_endterm();
 869         }
 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);
 874             }
 875             if (el->vis != BT_FALSE) {
 876                 output_rules_symbol(el->vis->id);
 877             }
 878             output_rules_endterm();
 879         }
 880         if (!sym_is_optional(sym)) {
 881             for_all_choices(sym, prop) {
 882                 struct symbol *symw;
 883                 struct expr *exprw;
 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};
 888                         wdep =
 889                             boolexpr_kconfig(gsymlist, symw->dir_dep.expr,
 890                                              false, settrue);
 891                     } else
 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);
 900                         }
 901                         if (el->vis->type != BT_TRUE) {
 902                             output_rules_symbol(-1 * el->vis->id);
 903                         }
 904                         if (wdep->type != BT_TRUE
 905                             && wdep->id != boolsym->id) {
 906                             output_rules_symbol(-1 * wdep->id);
 907                         }
 908                         output_rules_endterm();
 909                     }
 910                 }
 911             }
 912         }
 913     }
 914 }
 915
 916 #endif