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 #include <memory>
  17 #include <deque>
  18
  19 using namespace std;
  20
  21 int verbosity = 0;
  22
  23 enum options {
  24         OPT__START = 256,
  25         OPT_BASECONFIG,
  26         OPT_CNF,
  27         OPT_DOT,
  28         OPT_DUMP,
  29         OPT_ENV,
  30         OPT_HELP,
  31         OPT_KCONFIG,
  32         OPT_VARFILE,
  33         OPT_VAROPTION,
  34         OPT_VERBOSE,
  35 };
  36
  37 void print_help()
  38 {
  39         printf("Usage: kconfig2sat [options/actions]\n"
  40                "\n"
  41                "Options:\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"
  46                "\n"
  47                "Actions:\n"
  48                "  --dump                    Dump internal data (for debugging)\n"
  49                "  --cnf <file>              Generate CNF representation to <file>\n"
  50                 );
  51 }
  52
  53 typedef unique_ptr<char> upchar;
  54
  55 upchar expr_to_string(struct expr *e);
  56
  57 upchar sym_to_string(struct symbol *sym)
  58 {
  59         char *ret;
  60
  61         if (sym->name)
  62                 asprintf(&ret, sym->name);
  63         else
  64                 asprintf(&ret, "NONAME%d", sym->lcp.id);
  65         return upchar(ret);
  66 }
  67
  68 upchar expr_binop_to_string(struct expr *e, const char *op_str)
  69 {
  70         upchar l = expr_to_string(e->left.expr);
  71         upchar r = expr_to_string(e->right.expr);
  72         char *ret;
  73
  74         asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
  75         return upchar(ret);
  76 }
  77
  78 upchar expr_comp_to_string(struct expr *e, const char *op_str)
  79 {
  80         upchar l = sym_to_string(e->left.sym);
  81         upchar r = sym_to_string(e->right.sym);
  82         char *ret;
  83
  84         asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
  85         return upchar(ret);
  86 }
  87
  88 upchar expr_to_string(struct expr *e)
  89 {
  90         char *ret = NULL;
  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 upchar(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                 asprintf(&ret, "!%s", expr_to_string(e->left.expr).get());
 105                 break;
 106         case E_EQUAL:
 107                 return expr_comp_to_string(e, "==");
 108         case E_UNEQUAL:
 109                 return expr_comp_to_string(e, "!=");
 110         case E_LTH:
 111                 return expr_comp_to_string(e, "<");
 112         case E_LEQ:
 113                 return expr_comp_to_string(e, "<=");
 114         case E_GTH:
 115                 return expr_comp_to_string(e, ">");
 116         case E_GEQ:
 117                 return expr_comp_to_string(e, ">=");
 118         case E_LIST:
 119                 fprintf(stderr, "LIST not implemented\n");
 120                 exit(EXIT_FAILURE);
 121                 break;
 122         case E_SYMBOL:
 123                 return sym_to_string(e->left.sym);
 124         case E_RANGE:
 125                 fprintf(stderr, "RANGE not implemented\n");
 126                 exit(EXIT_FAILURE);
 127                 break;
 128         }
 129
 130         return upchar(ret);
 131 }
 132
 133
 134
 135 void dump_symbol(struct symbol *sym)
 136 {
 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(";
 142         char val = '.';
 143
 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;
 149                 }
 150         }
 151
 152 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
 153         FLAG(CONST);
 154         FLAG(CHECK);
 155         FLAG(CHOICE);
 156         FLAG(CHOICEVAL);
 157         FLAG(VALID);
 158         FLAG(OPTIONAL);
 159         FLAG(WRITE);
 160         FLAG(CHANGED);
 161         FLAG(AUTO);
 162         FLAG(CHECKED);
 163         FLAG(WARNED);
 164         FLAG(DEF_USER);
 165         FLAG(DEF_AUTO);
 166         FLAG(DEF3);
 167         FLAG(DEF4);
 168         if (flags[3])
 169                 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
 170 #undef FLAG
 171
 172         for_all_properties(sym, prop, P_PROMPT) {
 173                 prompt = prop->text;
 174         }
 175
 176         printf("%-40s %c %-8s %-50s %s\n", name.get(), val, type, flags, prompt);
 177
 178         if (verbosity > 0) {
 179                 if (sym->dir_dep.expr)
 180                         printf("    depends %s\n", expr_to_string(sym->dir_dep.expr).get());
 181
 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());
 186                 }
 187         }
 188 }
 189
 190 void do_dump()
 191 {
 192     int i;
 193     struct symbol *sym;
 194     for_all_symbols(i, sym) {
 195             dump_symbol(sym);
 196     }
 197 }
 198
 199 void mark_symbol_variable(const char *sym_name, const char *file, int lineno)
 200 {
 201         struct symbol *sym = sym_find(sym_name);
 202         if (!sym) {
 203                 fprintf(stderr, "%s:%d: Error: Invalid symbol: %s\n", file, lineno, sym_name);
 204                 exit(EXIT_FAILURE);
 205         }
 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);
 209 //      }
 210         if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
 211                 fprintf(stderr, "%s:%d: Error: Choice values not yet supported: %s", file, lineno, sym_name);
 212                 exit(EXIT_FAILURE);
 213         }
 214         struct property *prop;
 215         const char *prompt = NULL;
 216         for_all_properties(sym, prop, P_PROMPT) {
 217                 prompt = prop->text;
 218         }
 219         if (!prompt) {
 220                 fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", file, lineno, sym_name);
 221         }
 222         sym->lcp.variable = 1;
 223 }
 224
 225 void read_varfile(const char *varfile)
 226 {
 227         FILE *f = fopen(varfile, "r");
 228         char line[1000];
 229
 230         if (!f) {
 231                 perror(varfile);
 232                 exit(EXIT_FAILURE);
 233         }
 234
 235         int lineno = 0;
 236         while (fgets(line, sizeof(line), f)) {
 237                 char *p = line;
 238                 lineno++;
 239
 240                 if (line[0] == '#')
 241                         continue;
 242                 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
 243                         p += strlen(CONFIG_);
 244
 245                 const char *sym_name = strtok(p, " =\n");
 246                 mark_symbol_variable(sym_name, varfile, lineno);
 247         }
 248         fclose(f);
 249 }
 250
 251 void set_all_symbols_variable()
 252 {
 253         int i;
 254         struct symbol *sym;
 255
 256         for_all_symbols(i, sym) {
 257                 if (!(sym->flags & (SYMBOL_CONST | SYMBOL_AUTO)))
 258                         sym->lcp.variable = 1;
 259         }
 260 }
 261
 262 struct SatLiteral {
 263         struct symbol *sym;
 264         struct expr *expr;
 265         int dot_printed:1;
 266
 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 {
 271                 char *ret;
 272                 if (sym) {
 273                         assert(sym->name); // TODO
 274                         asprintf(&ret, "%s", sym->name);
 275                 } else if (expr) {
 276                         asprintf(&ret, "expr%d", expr->lcp.id);
 277                 }
 278                 return upchar(ret);
 279         }
 280 };
 281
 282 typedef vector<sat_id> SatClause;
 283
 284 struct Implication: public SatClause {
 285         Implication(sat_id a, sat_id b) : SatClause{-a, b} {}
 286 };
 287
 288 struct SatExpr {
 289         sat_id left, right;
 290         enum expr_type op;
 291
 292         SatExpr(sat_id l, enum expr_type o, sat_id r)
 293                 : left(l), right(r), op(o) {}
 294         //SatExpr(enum expr_type o) : left(0), right(0), op(o) { assert(o == E_NONE); }
 295         bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
 296 };
 297
 298 class SatLiterals : protected vector<struct SatLiteral>
 299 {
 300 public:
 301         using vector<struct SatLiteral>::begin;
 302         using vector<struct SatLiteral>::end;
 303         using vector<struct SatLiteral>::push_back;
 304         SatLiterals() { reserve(20000); }
 305         int count() const { return size(); }
 306         const SatLiteral &operator[](size_type i) const { return at(i-1); }
 307         const SatLiteral &last() const { return *(--end()); }
 308         bool test_set_dot_printed(struct symbol *sym) const {
 309                 auto l = (*this)[sym->lcp.id];
 310                 bool ret = l.dot_printed;
 311                 l.dot_printed = 1;
 312                 return ret;
 313         }
 314         bool test_set_dot_printed(struct expr *e) const {
 315                 auto l = (*this)[e->lcp.id];
 316                 bool ret = l.dot_printed;
 317                 l.dot_printed = 1;
 318                 return ret;
 319         }
 320 };
 321
 322 /*
 323  * bool FOO!=n => FOO
 324  * bool FOO!=y => !FOO
 325  * bool FOO==n => !FOO
 326  * bool FOO==y => FOO
 327  */
 328 struct expr *expr_eliminate_eq_yn(struct expr *e)
 329 {
 330         if (!e)
 331                 return NULL;
 332         switch (e->type) {
 333         case E_AND:
 334         case E_OR:
 335         case E_NOT:
 336                 e->left.expr = expr_eliminate_eq_yn(e->left.expr);
 337                 e->right.expr = expr_eliminate_eq_yn(e->right.expr);
 338                 break;
 339         case E_UNEQUAL:
 340                 // UNKNOWN symbols sometimes occur in dependency -
 341                 // e.g. ACPI_VIDEO on arm (the symbol is only defined
 342                 // for ACPI platforms (x86) but some drivers refer to
 343                 // it.
 344                 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
 345                         if (e->right.sym == &symbol_no) {
 346                                 // FOO!=n -> FOO
 347                                 e->type = E_SYMBOL;
 348                                 e->right.sym = NULL;
 349                         } else if (e->right.sym == &symbol_yes) {
 350                                 // FOO!=y -> !FOO
 351                                 e->type = E_SYMBOL;
 352                                 e->right.sym = NULL;
 353                                 e = expr_alloc_one(E_NOT, e);
 354                         }
 355                 }
 356                 break;
 357         case E_EQUAL:
 358                 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
 359                         if (e->right.sym == &symbol_yes) {
 360                                 // FOO==y -> FOO
 361                                 e->type = E_SYMBOL;
 362                                 e->right.sym = NULL;
 363                         } else if (e->right.sym == &symbol_no) {
 364                                 // FOO==n -> !FOO
 365                                 e->type = E_SYMBOL;
 366                                 e->right.sym = NULL;
 367                                 e = expr_alloc_one(E_NOT, e);
 368                         }
 369                 }
 370                 break;
 371         default:
 372                 ;
 373         }
 374         return e;
 375 }
 376
 377 bool mark_variable_expressions(struct expr *e)
 378 {
 379         if (!e)
 380                 return false;
 381
 382         switch (e->type) {
 383         case E_SYMBOL:
 384                 return (e->lcp.variable = e->left.sym->lcp.variable);
 385         case E_NONE:
 386                 fprintf(stderr, "NONE not implemented\n");
 387                 exit(EXIT_FAILURE);
 388                 break;
 389         case E_NOT:
 390                 if (mark_variable_expressions(e->left.expr))
 391                         return (e->lcp.variable = 1);
 392                 else
 393                         return false;
 394         case E_OR:
 395         case E_AND: {
 396                 mark_variable_expressions(e->left.expr);
 397                 mark_variable_expressions(e->right.expr);
 398
 399                 if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
 400                         return (e->lcp.variable = 1);
 401                 } else if (!e->left.expr->lcp.variable && !e->right.expr->lcp.variable) {
 402                         return (e->lcp.variable = 0);
 403                 } else {
 404                         tristate val;
 405
 406                         if (e->left.expr->lcp.variable) {
 407                                 val = expr_calc_value(e->right.expr);
 408                         } else if (e->right.expr->lcp.variable) {
 409                                 val = expr_calc_value(e->left.expr);
 410                         }
 411                         if ((e->type == E_OR && val == yes) ||
 412                             (e->type == E_AND && val == no))
 413                                 return (e->lcp.variable = 0);
 414                         else
 415                                 return (e->lcp.variable = 1);
 416                 }
 417                 __builtin_unreachable();
 418         }
 419         case E_EQUAL:
 420         case E_UNEQUAL:
 421                 if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
 422                         return (e->lcp.variable = 1);
 423                 } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 424                         fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
 425                         exit(EXIT_FAILURE);
 426                 } else
 427                         return false;
 428         case E_LTH:
 429         case E_LEQ:
 430         case E_GTH:
 431         case E_GEQ:
 432                 if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 433                         fprintf(stderr, "Comparison of variable symbols not implemented\n");
 434                         exit(EXIT_FAILURE);
 435                 } else
 436                         return false;
 437                 break;
 438         case E_LIST:
 439                 fprintf(stderr, "LIST not implemented\n");
 440                 exit(EXIT_FAILURE);
 441                 break;
 442         case E_RANGE:
 443                 fprintf(stderr, "RANGE not implemented\n");
 444                 exit(EXIT_FAILURE);
 445                 break;
 446         }
 447         fprintf(stderr, "Unexpected situation in mark_variable_expressions\n");
 448         exit(EXIT_FAILURE);
 449 }
 450
 451 void mark_variable_expressions()
 452 {
 453         int i;
 454         struct symbol *sym;
 455         struct property *prop;
 456
 457         for_all_symbols(i, sym) {
 458                 mark_variable_expressions(sym->dir_dep.expr);
 459                 mark_variable_expressions(sym->rev_dep.expr);
 460                 for_all_properties(sym, prop, P_SELECT) {
 461                         assert(prop->expr->type == E_SYMBOL);
 462                         mark_variable_expressions(prop->visible.expr);
 463                 }
 464         }
 465 }
 466
 467 void check_dep_consistency()
 468 {
 469         int i;
 470         struct symbol *sym;
 471         tristate val;
 472
 473         for_all_symbols(i, sym) {
 474                 if (sym->lcp.variable && sym->dir_dep.expr && !sym->dir_dep.expr->lcp.variable) {
 475                         val = expr_calc_value(sym->dir_dep.expr);
 476                         if (val == no) {
 477                                 fprintf(stderr, "Symbol %s cannot be variable because its dependency is always 'no': %s\n",
 478                                         sym->name, expr_to_string(sym->dir_dep.expr).get());
 479                                 exit(EXIT_FAILURE);
 480                         }
 481                 }
 482                 if (sym->lcp.variable && sym->rev_dep.expr && !sym->rev_dep.expr->lcp.variable) {
 483                         val = expr_calc_value(sym->rev_dep.expr);
 484                         if (val == yes) {
 485                                 fprintf(stderr, "Symbol %s cannot be variable because it is selected by expression that is always 'yes': %s\n",
 486                                         sym->name, expr_to_string(sym->rev_dep.expr).get());
 487                                 exit(EXIT_FAILURE);
 488                         }
 489                 }
 490                 if (!sym->lcp.variable && (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) &&
 491                     sym->curr.tri == no && sym->rev_dep.expr && sym->rev_dep.expr->lcp.variable) {
 492                         fprintf(stderr, "Symbol %s cannot be fixed to 'no', because it is selcted by variable expression '%s'\n",
 493                                 sym->name, expr_to_string(sym->rev_dep.expr).get());
 494                         exit(EXIT_FAILURE);
 495                 }
 496         }
 497 }
 498
 499
 500 class DotWriter {
 501         FILE *f;
 502 public:
 503         DotWriter(const char *file_name) {
 504                 f = fopen(file_name, "w");
 505
 506                 if (!f) {
 507                         perror(file_name);
 508                         exit(EXIT_FAILURE);
 509                 }
 510
 511                 fprintf(f, "digraph conf {\n");
 512                 //fprintf(f, "rankdir=LR;\n");
 513         }
 514         ~DotWriter() {
 515                 fprintf(f, "}\n");
 516                 fclose(f);
 517         }
 518         void symbol(struct symbol *sym) {
 519 //              if (sym->lcp.dot_printed)
 520 //                      return;
 521 //              sym->lcp.dot_printed = 1;
 522
 523                 const char *opts = "";
 524                 if (sym->lcp.variable)
 525                         opts = " [penwidth=3]";
 526                 else
 527                         opts = " [color=gray]";
 528                 fprintf(f, "\"%s\"%s;\n", sym->name, opts);
 529         }
 530         void expr(const SatLiteral &l) {
 531                 assert(l.expr);
 532                 const char *label = "???";
 533 //              if (sym->lcp.dot_printed)
 534 //                      return;
 535 //              sym->lcp.dot_printed = 1;
 536                 switch (l.expr->type) {
 537                 case E_OR:  label = "|"; break;
 538                 case E_AND: label = "&"; break;
 539                 case E_EQUAL: label = "="; break;
 540                 case E_UNEQUAL: label = "!="; break;
 541                 case E_NOT: label = "!"; break;
 542                 case E_SYMBOL:
 543                 case E_NONE:
 544                 case E_RANGE:
 545                 case E_LTH:
 546                 case E_LEQ:
 547                 case E_GTH:
 548                 case E_GEQ:
 549                 case E_LIST:
 550                 default:
 551                         fprintf(stderr, "Expr %d not implemented\n", l.expr->type);
 552                         exit(EXIT_FAILURE);
 553                         break;
 554                 }
 555
 556                 fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", l.name().get(), label);
 557         }
 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());
 560         }
 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());
 563         }
 564         void edge(const SatLiteral &from, const SatLiteral &to) {
 565                 fprintf(f, "\"%s\" -> \"%s\" [arrowhead=empty];\n", from.name().get(), to.name().get());
 566         }
 567 };
 568
 569 class SatData {
 570         SatLiterals literals = {};
 571         vector<SatClause> clauses = {};
 572         map<SatExpr, sat_id> expressions = {};
 573         DotWriter *dot = nullptr;
 574 public:
 575
 576         SatData(const char *dot_fn) {
 577                 if (dot_fn)
 578                         dot = new DotWriter(dot_fn);
 579                 symbols2literals();
 580                 expressions2literals();
 581                 expressions2clauses();
 582                 if (dot)
 583                         delete dot;
 584
 585         }
 586
 587         const SatLiteral &add_literal(struct symbol *sym) {
 588                 sym->lcp.id = literals.count() + 1;
 589                 literals.push_back(SatLiteral(sym));
 590                 if (dot)
 591                         dot->symbol(sym);
 592                 return literals.last();
 593         }
 594
 595         const SatLiteral &add_literal(struct expr *e) {
 596                 e->lcp.id = literals.count() + 1;
 597                 literals.push_back(SatLiteral(e));
 598                 if (dot)
 599                         dot->expr(literals.last());
 600                 return literals.last();
 601         }
 602
 603         void symbols2literals() {
 604                 int i;
 605                 struct symbol *sym;
 606
 607                 for_all_symbols(i, sym) {
 608                         if (sym->lcp.variable)
 609                                 add_literal(sym);
 610                 }
 611         }
 612
 613         // Assign e->lcp.id to variable literals
 614         sat_id expr2literal(struct expr *e) {
 615                 if (!e || !e->lcp.variable)
 616                         return 0;
 617                 if (e->lcp.id)
 618                         return e->lcp.id;
 619
 620                 switch (e->type) {
 621                 case E_SYMBOL:
 622                         assert(e->left.sym->lcp.id);
 623                         e->lcp.id = e->left.sym->lcp.id;
 624                         break;
 625                 case E_NONE:
 626                         fprintf(stderr, "NONE not implemented\n");
 627                         exit(EXIT_FAILURE);
 628                         break;
 629                 case E_NOT: {
 630                         expr2literal(e->left.expr);
 631
 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()));
 637                                 if (dot)
 638                                         dot->edge(literals[e->left.expr->lcp.id], l);
 639                         } else
 640                                 e->lcp.id = it->second;
 641                         break;
 642                 }
 643                 case E_OR:
 644                 case E_AND: {
 645                         expr2literal(e->left.expr);
 646                         expr2literal(e->right.expr);
 647
 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()));
 654                                         if (dot) {
 655                                                 dot->edge(literals[e->left.expr->lcp.id], l);
 656                                                 dot->edge(literals[e->right.expr->lcp.id], l);
 657                                         }
 658                                 } else
 659                                         e->lcp.id = it->second;
 660                         } else {
 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;
 665                                 }
 666                         }
 667                         break;
 668                 }
 669                 case E_EQUAL:
 670                 case E_UNEQUAL: {
 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()));
 677                                         if (dot) {
 678                                                 dot->edge(literals[e->left.sym->lcp.id], l);
 679                                                 dot->edge(literals[e->right.sym->lcp.id], l);
 680                                         }
 681                                 } else
 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");
 685                                 exit(EXIT_FAILURE);
 686                         }
 687                         break;
 688                 }
 689                 case E_LTH:
 690                 case E_LEQ:
 691                 case E_GTH:
 692                 case E_GEQ:
 693                         if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 694                                 fprintf(stderr, "Comparison of variable symbols not implemented\n");
 695                                 exit(EXIT_FAILURE);
 696                         }
 697                         break;
 698                 case E_LIST:
 699                         fprintf(stderr, "LIST not implemented\n");
 700                         exit(EXIT_FAILURE);
 701                         break;
 702                 case E_RANGE:
 703                         fprintf(stderr, "RANGE not implemented\n");
 704                         exit(EXIT_FAILURE);
 705                         break;
 706                 }
 707                 assert(e->lcp.id);
 708                 return e->lcp.id;
 709         }
 710
 711         void expressions2literals() {
 712                 int i;
 713                 struct symbol *sym;
 714                 struct expr *e;
 715                 sat_id id;
 716                 const SatLiteral *syml;
 717
 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);
 726                                 if (id) {
 727                                         clauses.push_back(Implication(sym->lcp.id, id));
 728                                         if (dot)
 729                                                 dot->depends_on(*syml, literals[id]);
 730                                 }
 731
 732                                 // Reverse dependecies
 733                                 e = sym->rev_dep.expr;
 734                                 id = expr2literal(e);
 735                                 if (id) {
 736                                         clauses.push_back(Implication(id, sym->lcp.id));
 737                                         if (dot)
 738                                                 dot->selects(literals[id], *syml);
 739                                 }
 740                         }
 741                 }
 742         }
 743
 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;
 751                         assert(e_id);
 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());
 755                                 //exit(1);
 756                         }
 757                         switch (e.op) {
 758                         case E_SYMBOL:
 759                         case E_NONE:
 760                                 assert(0);
 761                                 break;
 762                         case E_NOT:
 763                                 clauses.push_back(SatClause{  e_id,  e.left });
 764                                 clauses.push_back(SatClause{ -e_id, -e.left });
 765                                 break;
 766                         case E_OR:
 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 });
 770                                 break;
 771                         case E_AND:
 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 });
 775                                 break;
 776                         case E_EQUAL:
 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 });
 781                                 break;
 782                         case E_UNEQUAL:
 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 });
 787                                 break;
 788                         case E_LTH:
 789                         case E_LEQ:
 790                         case E_GTH:
 791                         case E_GEQ: {
 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 });
 798                                 break;
 799                         }
 800                         case E_LIST:
 801                                 fprintf(stderr, "LIST not implemented\n");
 802                                 exit(EXIT_FAILURE);
 803                                 break;
 804                         case E_RANGE:
 805                                 fprintf(stderr, "RANGE not implemented\n");
 806                                 exit(EXIT_FAILURE);
 807                                 break;
 808                         }
 809                 }
 810
 811         }
 812
 813         void write_dimacs_cnf(const char *cnf) {
 814                 FILE *f = fopen(cnf, "w");
 815
 816                 if (!f) {
 817                         perror(cnf);
 818                         exit(EXIT_FAILURE);
 819                 }
 820
 821                 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size());
 822
 823                 for (auto l: literals) {
 824                         if (l.sym)
 825                                 fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
 826                         if (l.expr)
 827                                 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
 828                 }
 829                 for (auto clause: clauses) {
 830                         for (sat_id id: clause) {
 831                                 assert(id != 0);
 832                                 fprintf(f, "%d ", id);
 833                         }
 834                         fprintf(f, "0\n");
 835                 }
 836                 fclose(f);
 837         }
 838
 839 //      void print_dot_oper(FILE *f, struct expr *e, const char *parent, const char *label) {
 840 //              char *expr_name;
 841 //              asprintf(&expr_name, "expr%d", e->lcp.id);
 842 //              fprintf(f, "\"%s\" -> \"%s\";\n", parent, expr_name);
 843
 844 //              fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", expr_name, label);
 845 //              print_dot_expr(f, e->left.expr, expr_name, "l", "");
 846 //              print_dot_expr(f, e->right.expr, expr_name, "r", "");
 847 //              free(expr_name);
 848 //      }
 849
 850 //      void print_dot_expr(FILE *f, struct expr *e, const char *parent,
 851 //                          const char *suffix, const char *edge_opts) {
 852 //              if (e->lcp.dot_printed ||
 853 //                  !e->lcp.variable)
 854 //                      return;
 855 //              e->lcp.dot_printed = 1;
 856 //              if (e) {
 857 //                      switch (e->type) {
 858 //                      case E_NONE:
 859 //                              break;
 860 //                      case E_OR:
 861 //                              print_dot_oper(f, e, parent, "|");
 862 //                              break;
 863 //                      case E_AND:
 864 //                              print_dot_oper(f, e, parent, "&");
 865 //                              break;
 866 //                      case E_NOT:
 867 //                              print_dot_expr(f, e->left.expr, parent, suffix, "arrowhead=odot");
 868 //                              break;
 869 //                      case E_EQUAL:
 870 //                              print_dot_oper(f, e, parent, "=");
 871 //                              break;
 872 //                      case E_UNEQUAL:
 873 //                              print_dot_oper(f, e, parent, "!=");
 874 //                              break;
 875 //                      case E_LIST:
 876 //                              fprintf(stderr, "LIST not implemented\n");
 877 //                              exit(EXIT_FAILURE);
 878 //                              break;
 879 //                      case E_SYMBOL: {
 880 //                              if (e->left.sym->name) {
 881 //                                      fprintf(f, "\"%s\" -> \"%s\" [%s];\n", parent, e->left.sym->name, edge_opts);
 882 //                                      print_dot_symbol(f, e->left.sym);
 883 //                              }
 884 //                              break;
 885 //                      }
 886 //                      case E_RANGE:
 887 //                              fprintf(stderr, "RANGE not implemented\n");
 888 //                              exit(EXIT_FAILURE);
 889 //                              break;
 890 //                      case E_LTH:
 891 //                      case E_LEQ:
 892 //                      case E_GTH:
 893 //                      case E_GEQ:
 894 //                              break;
 895 //                      }
 896 //              }
 897 //      }
 898
 899 //      void print_dot_symbol(FILE *f, struct symbol *sym) {
 900 //              if (!sym->lcp.variable ||
 901 //                  sym->lcp.dot_printed)
 902 //                      return;
 903 //              sym->lcp.dot_printed = 1;
 904
 905 //              const char *opts = "";
 906 //              if (sym->lcp.variable)
 907 //                      opts = " [penwidth=3]";
 908 //              else
 909 //                      opts = " [color=gray]";
 910 //              fprintf(f, "\"%s\"%s;\n", sym->name, opts);
 911 //              if (sym->dir_dep.expr)
 912 //                      print_dot_expr(f, sym->dir_dep.expr, sym->name, "", "");
 913
 914 //              struct property *prop;
 915 //              for_all_properties(sym, prop, P_SELECT) {
 916 //                      assert(prop->expr->type == E_SYMBOL);
 917 //                      print_dot_expr(f, prop->expr, sym->name, "", "label=\"selects\"");
 918 //                      if (prop->visible.expr && prop->visible.expr->lcp.variable) {
 919 //                              printf("Not implemented %s\n", expr_to_string(prop->visible.expr).get());
 920 //                      }
 921 //              }
 922 //      }
 923
 924
 925 //      void write_dot(const char *dot) {
 926 //              int i;
 927 //              FILE *f = fopen(dot, "w");
 928
 929 //              if (!f) {
 930 //                      perror(dot);
 931 //                      exit(EXIT_FAILURE);
 932 //              }
 933
 934 //              fprintf(f, "digraph conf {\n");
 935
 936 //              struct symbol *sym;
 937 //              for_all_symbols(i, sym)
 938 //                      print_dot_symbol(f, sym);
 939 //              fprintf(f, "}\n");
 940 //              fclose(f);
 941 //      }
 942 };
 943
 944 int main(int argc, char **argv)
 945 {
 946         int c;
 947
 948         char *baseconf = NULL;
 949         char *cnf = NULL;
 950         char *dot = NULL;
 951         char *kconfig = NULL;
 952         char *varfile = NULL;
 953         int  dump = false;
 954         deque<string> varopts;
 955
 956         while (1) {
 957                 int option_index = 0;
 958                 static struct option long_options[] = {
 959                         {"baseconf",    required_argument, 0,     OPT_BASECONFIG },
 960                         {"cnf",         required_argument, 0,     OPT_CNF },
 961                         {"dot",         required_argument, 0,     OPT_DOT },
 962                         {"env",         required_argument, 0,     OPT_ENV },
 963                         {"dump",        no_argument,       &dump, true },
 964                         {"help",        no_argument,       0,     OPT_HELP },
 965                         {"kconfig",     required_argument, 0,     OPT_KCONFIG },
 966                         {"varfile",     required_argument, 0,     OPT_VARFILE },
 967                         {"varopt",      required_argument, 0,     OPT_VAROPTION },
 968                         {"verbose",     no_argument,       0,     OPT_VERBOSE },
 969                         {0,             0,                 0,     0 }
 970                 };
 971
 972                 c = getopt_long(argc, argv, "b:hk:v",
 973                                 long_options, &option_index);
 974                 if (c == -1)
 975                         break;
 976
 977                 switch (c) {
 978                 case 0: /* long option with flag != NULL */
 979                         break;
 980                 case 'b':
 981                 case OPT_BASECONFIG:
 982                         baseconf = optarg;
 983                         break;
 984                 case OPT_CNF:
 985                         cnf = optarg;
 986                         break;
 987                 case OPT_DOT:
 988                         dot = optarg;
 989                         break;
 990                 case OPT_ENV:
 991                         set_missing_env(optarg);
 992                         break;
 993                 case 'h':
 994                 case OPT_HELP:
 995                         print_help();
 996                         exit(EXIT_SUCCESS);
 997                 case 'k':
 998                 case OPT_KCONFIG:
 999                         kconfig = optarg;
1000                         break;
1001                 case 'v':
1002                 case OPT_VERBOSE:
1003                         verbosity++;
1004                         break;
1005                 case OPT_VARFILE:
1006                         varfile = optarg;
1007                         break;
1008                 case OPT_VAROPTION:
1009                         varopts.push_back(string(optarg));
1010                         break;
1011                 case '?':
1012                 default:
1013                         print_help();
1014                         exit(EXIT_FAILURE);
1015                         printf("?? getopt returned character code 0%o ??\n", c);
1016                 }
1017         }
1018
1019         if (optind < argc) {
1020                 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
1021                 print_help();
1022                 exit(EXIT_FAILURE);
1023         }
1024
1025
1026         if (kconfig == NULL) {
1027                 fprintf(stderr, "--kconfig option missing\n");
1028                 exit(EXIT_FAILURE);
1029         }
1030
1031         setlocale(LC_ALL, "");
1032         bindtextdomain(PACKAGE, LOCALEDIR);
1033         textdomain(PACKAGE);
1034
1035         conf_parse_path(kconfig);
1036         if (baseconf)
1037                 conf_read(baseconf);
1038
1039         if (!varfile && varopts.empty())
1040                 set_all_symbols_variable();
1041         else {
1042                 if (varfile)
1043                         read_varfile(varfile);
1044                 if (!varopts.empty())
1045                         for (auto o: varopts)
1046                                 mark_symbol_variable(o.c_str(), NULL, 0);
1047         }
1048
1049         mark_variable_expressions();
1050         check_dep_consistency();
1051
1052         SatData sat_data(dot);
1053
1054         if (dump)
1055                 do_dump();
1056
1057         if (cnf)
1058                 sat_data.write_dimacs_cnf(cnf);
1059
1060         return EXIT_SUCCESS;
1061 }