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