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
  10 #include "kconfig/lkc.h"
  11 #include "lcp_utils.h"
  12
  13 #include <vector>
  14
  15 using namespace std;
  16
  17 int verbosity = 0;
  18
  19 enum options {
  20         OPT__START = 256,
  21         OPT_BASECONFIG,
  22         OPT_CNF,
  23         OPT_DUMP,
  24         OPT_ENV,
  25         OPT_HELP,
  26         OPT_KCONFIG,
  27         OPT_VARFILE,
  28         OPT_VAROPTION,
  29         OPT_VERBOSE,
  30 };
  31
  32 void print_help()
  33 {
  34         printf("Usage: kconfig2sat [options/actions]\n"
  35                "\n"
  36                "Options:\n"
  37                "  -b, --baseconf <.config>  Linux .config file with base configuration\n"
  38                "  --env <.conf.mk>          Set env. variables such as ARCH from .conf.mk\n"
  39                "  -k, --kconfig <Kconfig>   Kconfig file (with path)\n"
  40                "  --varfile <file>          File listing variable options (one option per line)\n"
  41                "\n"
  42                "Actions:\n"
  43                "  --dump                    Dump internal data (for debugging)\n"
  44                "  --cnf <file>              Generate CNF representation to <file>\n"
  45                 );
  46 }
  47
  48 void dump_symbol(struct symbol *sym)
  49 {
  50         struct property *prop;
  51         const char *name = sym->name;
  52         const char *type = sym_type_name(sym->type);
  53         const char *prompt = NULL;
  54         char flags[256] = "fl(";
  55         char val = '.';
  56
  57         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
  58                 switch (sym->curr.tri) {
  59                 case no:  val = 'n'; break;
  60                 case mod: val = 'm'; break;
  61                 case yes: val = 'y'; break;
  62                 }
  63         }
  64
  65 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
  66         FLAG(CONST);
  67         FLAG(CHECK);
  68         FLAG(CHOICE);
  69         FLAG(CHOICEVAL);
  70         FLAG(VALID);
  71         FLAG(OPTIONAL);
  72         FLAG(WRITE);
  73         FLAG(CHANGED);
  74         FLAG(AUTO);
  75         FLAG(CHECKED);
  76         FLAG(WARNED);
  77         FLAG(DEF_USER);
  78         FLAG(DEF_AUTO);
  79         FLAG(DEF3);
  80         FLAG(DEF4);
  81         if (flags[3])
  82                 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
  83 #undef FLAG
  84
  85         for_all_properties(sym, prop, P_PROMPT) {
  86                 prompt = prop->text;
  87         }
  88
  89         printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt);
  90 }
  91
  92 void do_dump()
  93 {
  94     int i;
  95     struct symbol *sym;
  96     for_all_symbols(i, sym) {
  97             dump_symbol(sym);
  98     }
  99 }
 100
 101 void read_varfile(const char *varfile)
 102 {
 103         FILE *f = fopen(varfile, "r");
 104         char line[1000];
 105
 106         if (!f) {
 107                 perror(varfile);
 108                 exit(EXIT_FAILURE);
 109         }
 110
 111         int lineno = 0;
 112         while (fgets(line, sizeof(line), f)) {
 113                 char *p = line;
 114                 lineno++;
 115
 116                 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
 117                         p += strlen(CONFIG_);
 118
 119                 const char *sym_name = strtok(p, " =\n");
 120                 struct symbol *sym = sym_find(sym_name);
 121                 if (!sym) {
 122                         fprintf(stderr, "%s:%d: Invalid symbol: %s\n", varfile, lineno, sym_name);
 123                         exit(EXIT_FAILURE);
 124                 }
 125                 if (!(sym->flags & SYMBOL_WRITE)) {
 126                         fprintf(stderr, "%s:%d: Symbol %s not visible\n", varfile, lineno, sym_name);
 127                         exit(EXIT_FAILURE);
 128                 }
 129                 if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
 130                         fprintf(stderr, "%s:%d: Choice values not yet supported: %s", varfile, lineno, sym_name);
 131                         exit(EXIT_FAILURE);
 132                 }
 133                 struct property *prop;
 134                 const char *prompt = NULL;
 135                 for_all_properties(sym, prop, P_PROMPT) {
 136                         prompt = prop->text;
 137                 }
 138                 if (!prompt) {
 139                         fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
 140                 }
 141                 sym->lcp->variable = 1;
 142         }
 143         fclose(f);
 144 }
 145
 146 void write_dimacs_cnf(const char *cnf)
 147 {
 148         FILE *f = fopen(cnf, "w");
 149
 150         if (!f) {
 151                 perror(cnf);
 152                 exit(EXIT_FAILURE);
 153         }
 154
 155         fclose(f);
 156 }
 157
 158 struct SatLiteral {
 159         struct symbol *sym;
 160         struct expr *expr;
 161
 162         SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
 163         SatLiteral(struct expr *e)   : sym(nullptr), expr(e) {}
 164 };
 165
 166 struct SatClause {
 167         // TODO
 168 };
 169
 170 class SatLiterals : public vector<struct SatLiteral>
 171 {
 172 public:
 173         int fixed = {0};
 174         SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
 175         int count() const { return size() - 1; }
 176 };
 177
 178 class SatData {
 179         SatLiterals literals = {};
 180         vector<SatClause> clauses = {};
 181 public:
 182
 183         SatData() {
 184                 int i;
 185                 struct symbol *sym;
 186
 187                 for_all_symbols(i, sym) {
 188                         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
 189                                 literals.push_back(SatLiteral(sym));
 190                                 sym->lcp = new lcp_symbol;
 191                                 memset(sym->lcp, 0, sizeof(*sym->lcp));
 192                                 sym->lcp->sat_id = literals.count();
 193                         }
 194                 }
 195         }
 196
 197         void write_dimacs_cnf(const char *cnf) {
 198                 int i;
 199                 FILE *f = fopen(cnf, "w");
 200
 201                 if (!f) {
 202                         perror(cnf);
 203                         exit(EXIT_FAILURE);
 204                 }
 205
 206                 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
 207
 208                 for (i = 1; i <= literals.count(); i++) {
 209                         SatLiteral &l = literals[i];
 210                         if (l.sym)
 211                                 fprintf(f, "c SYM %d %s\n", l.sym->lcp->sat_id, l.sym->name);
 212                         if (l.sym && l.sym->flags & SYMBOL_VALID && !l.sym->lcp->variable)
 213                                 fprintf(f, "%d 0\n", l.sym->curr.tri != no ? l.sym->lcp->sat_id : -l.sym->lcp->sat_id);
 214                 }
 215                 fclose(f);
 216         }
 217 };
 218
 219
 220 int main(int argc, char **argv)
 221 {
 222         int c;
 223
 224         char *baseconf = NULL;
 225         char *cnf = NULL;
 226         char *kconfig = NULL;
 227         char *varfile = NULL;
 228         int  dump = false;
 229
 230         while (1) {
 231                 int option_index = 0;
 232                 static struct option long_options[] = {
 233                         {"baseconf",    required_argument, 0,     OPT_BASECONFIG },
 234                         {"cnf",         required_argument, 0,     OPT_CNF },
 235                         {"env",         required_argument, 0,     OPT_ENV },
 236                         {"dump",        no_argument,       &dump, true },
 237                         {"help",        no_argument,       0,     OPT_HELP },
 238                         {"kconfig",     required_argument, 0,     OPT_KCONFIG },
 239                         {"varfile",     required_argument, 0,     OPT_VARFILE },
 240 //                      {"varopt",      required_argument, 0,     OPT_VAROPTION },
 241                         {"verbose",     no_argument,       0,     OPT_VERBOSE },
 242                         {0,             0,                 0,     0 }
 243                 };
 244
 245                 c = getopt_long(argc, argv, "b:hk:v",
 246                                 long_options, &option_index);
 247                 if (c == -1)
 248                         break;
 249
 250                 switch (c) {
 251                 case 0: /* long option with flag != NULL */
 252                         break;
 253                 case 'b':
 254                 case OPT_BASECONFIG:
 255                         baseconf = optarg;
 256                         break;
 257                 case OPT_CNF:
 258                         cnf = optarg;
 259                         break;
 260                 case OPT_ENV:
 261                         set_missing_env(optarg);
 262                         break;
 263                 case 'h':
 264                 case OPT_HELP:
 265                         print_help();
 266                         exit(EXIT_SUCCESS);
 267                 case 'k':
 268                 case OPT_KCONFIG:
 269                         kconfig = optarg;
 270                         break;
 271                 case 'v':
 272                 case OPT_VERBOSE:
 273                         verbosity++;
 274                         break;
 275                 case OPT_VARFILE:
 276                         varfile = optarg;
 277                         break;
 278                 case '?':
 279                 default:
 280                         print_help();
 281                         exit(EXIT_FAILURE);
 282                         printf("?? getopt returned character code 0%o ??\n", c);
 283                 }
 284         }
 285
 286         if (optind < argc) {
 287                 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
 288                 print_help();
 289                 exit(EXIT_FAILURE);
 290         }
 291
 292
 293         if (kconfig == NULL) {
 294                 fprintf(stderr, "--kconfig option missing\n");
 295                 exit(EXIT_FAILURE);
 296         }
 297
 298         setlocale(LC_ALL, "");
 299         bindtextdomain(PACKAGE, LOCALEDIR);
 300         textdomain(PACKAGE);
 301
 302         conf_parse_path(kconfig);
 303         SatData sat_data;
 304
 305         if (baseconf)
 306                 conf_read(baseconf);
 307
 308         if (varfile)
 309                 read_varfile(varfile);
 310
 311         if (dump)
 312                 do_dump();
 313
 314
 315         if (cnf) {
 316                 sat_data.write_dimacs_cnf(cnf);
 317         }
 318
 319         return EXIT_SUCCESS;
 320 }
 321
 322 #if 0
 323
 324 void build_symlist() {
 325     int i;
 326     struct symbol *sym;
 327     struct property *prop;
 328     for_all_symbols(i, sym) {
 329         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
 330             if (sym->name == NULL)
 331                 asprintf(&sym->name, "NONAMEGEN%d", noname_num++);
 332
 333             symlist_add(gsymlist, sym->name);
 334         }
 335     }
 336     symlist_closesym(gsymlist);
 337 }
 338
 339 /* TODO: Split to smaller functions with meaningful names */
 340 void cpy_dep() {
 341     int i;
 342     struct symbol *sym;
 343     struct property *prop;
 344     struct symlist_el *el;
 345     unsigned el_id;
 346     struct boolexpr *boolsym;
 347     for_all_symbols(i, sym) {
 348         if (sym->type != S_BOOLEAN && sym->type != S_TRISTATE)
 349             continue;
 350         el_id = symlist_id(gsymlist, sym->name);
 351         el = &(gsymlist->array[el_id - 1]);
 352         boolsym = boolexpr_sym(gsymlist, sym, false, NULL);
 353         Iprintf("Processing: %s\n", sym->name);
 354         // Visibility
 355         for_all_prompts(sym, prop) {
 356             Dprintf(" Prompt: %s\n", prop->text);
 357             if (prop->visible.expr != NULL) {
 358                 doutput_expr(prop->visible.expr);
 359                 struct boolexpr *vis =
 360                     boolexpr_kconfig(gsymlist, prop->visible.expr,
 361                                      false, NULL);
 362                 if (el->vis == NULL) {
 363                     el->vis = vis;
 364                 } else {
 365                     el->vis = boolexpr_or(el->vis, vis);
 366                 }
 367             } else if (el->vis == NULL) {
 368                 el->vis = boolexpr_true();
 369             }
 370         }
 371         if (el->vis == NULL)
 372             el->vis = boolexpr_false();
 373         // Symbol is choice.. special treatment required
 374         if (sym_is_choice(sym)) {
 375             Dprintf(" Is Choice\n");
 376             goto choice_exception;
 377         }
 378         // Default value
 379         struct boolexpr **defexpr = NULL;
 380         size_t defexpr_size = 0;
 381         int z;
 382         bool exitdef = false;
 383         for_all_defaults(sym, prop) {
 384             Dprintf(" Default value:\n");
 385             doutput_expr(prop->expr);
 386             struct boolexpr *def =
 387                 boolexpr_kconfig(gsymlist, prop->expr, true, NULL);
 388             struct boolexpr *vis;
 389             if (prop->visible.expr != NULL)
 390                 vis = boolexpr_kconfig(gsymlist, prop->visible.expr,
 391                                        false, NULL);
 392             else
 393                 vis = boolexpr_true();
 394             if (vis->type != BT_TRUE) {
 395                 defexpr = realloc(defexpr,
 396                                   ++defexpr_size * sizeof(struct boolexpr *));
 397                 defexpr[defexpr_size - 1] = boolexpr_copy(vis);
 398             } else {
 399                 ++defexpr_size;
 400                 exitdef = true;
 401             }
 402             def = boolexpr_and(def, vis);
 403             for (z = 0; z < ((int)defexpr_size - 1); z++) {
 404                 def = boolexpr_and(def, boolexpr_not(
 405                                        boolexpr_copy(defexpr[z])));
 406             }
 407             if (el->def == NULL)
 408                 el->def = def;
 409             else
 410                 el->def = boolexpr_or(el->def, def);
 411             if (exitdef)
 412                 break;
 413         }
 414         if (defexpr != NULL) {
 415             for (z = 0; z < defexpr_size - 1; z++) {
 416                 boolexpr_free(defexpr[z]);
 417             }
 418             free(defexpr);
 419         }
 420         if (el->def == NULL)
 421             el->def = boolexpr_false();
 422         // Dependency expression
 423         if (sym->dir_dep.expr != NULL) {
 424             Dprintf(" Dependency:\n");
 425             doutput_expr(sym->dir_dep.expr);
 426             el->dep =
 427                 boolexpr_kconfig(gsymlist, sym->dir_dep.expr, false, NULL);
 428         } else
 429             el->dep = boolexpr_true();
 430         // Reverse dependency expression
 431         if (sym->rev_dep.expr != NULL) {
 432             Dprintf(" Reverse dependency:\n");
 433             doutput_expr(sym->rev_dep.expr);
 434             el->rev_dep =
 435                 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, false, NULL);
 436         } else
 437             el->rev_dep = boolexpr_false();
 438
 439         if (el->dep->type != BT_FALSE && el->dep->type != BT_TRUE)
 440             cnf_boolexpr(gsymlist, el->dep);
 441         if (el->rev_dep->type != BT_FALSE
 442             && el->rev_dep->type != BT_TRUE)
 443             cnf_boolexpr(gsymlist, el->rev_dep);
 444         if (el->def->type != BT_FALSE && el->def->type != BT_TRUE)
 445             cnf_boolexpr(gsymlist, el->def);
 446         if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
 447             cnf_boolexpr(gsymlist, el->vis);
 448         // (!sym || dep) && (sym || !rev_dep) &&
 449         // && (sym || !dep || !def || vis) &&
 450         // (!sym || rev_dep || def || vis)
 451         if (el->dep->type != BT_TRUE) {
 452             output_rules_symbol(-1 * boolsym->id);
 453             if (el->dep->type != BT_FALSE) {
 454                 output_rules_symbol(el->dep->id);
 455             }
 456             output_rules_endterm();
 457         }
 458         if (el->rev_dep->type != BT_FALSE) {
 459             output_rules_symbol(boolsym->id);
 460             if (el->rev_dep->type != BT_TRUE) {
 461                 output_rules_symbol(-1 * el->rev_dep->id);
 462             }
 463             output_rules_endterm();
 464         }
 465         if (el->dep->type != BT_FALSE && el->def->type != BT_FALSE
 466             && el->vis->type != BT_TRUE) {
 467             output_rules_symbol(boolsym->id);
 468             if (el->dep->type != BT_TRUE) {
 469                 output_rules_symbol(-1 * el->dep->id);
 470             }
 471             if (el->def->type != BT_TRUE) {
 472                 output_rules_symbol(-1 * el->def->id);
 473             }
 474             if (el->vis->type != BT_FALSE) {
 475                 output_rules_symbol(el->vis->id);
 476             }
 477             output_rules_endterm();
 478         }
 479         if (el->rev_dep->type != BT_TRUE && el->def->type != BT_TRUE
 480             && el->vis->type != BT_TRUE) {
 481             output_rules_symbol(-1 * boolsym->id);
 482             if (el->rev_dep->type != BT_FALSE) {
 483                 output_rules_symbol(el->rev_dep->id);
 484             }
 485             if (el->def->type != BT_FALSE) {
 486                 output_rules_symbol(el->def->id);
 487             }
 488             if (el->vis->type != BT_FALSE) {
 489                 output_rules_symbol(el->vis->id);
 490             }
 491             output_rules_endterm();
 492         }
 493
 494         boolexpr_free(el->def);
 495         boolexpr_free(el->vis);
 496         boolexpr_free(el->dep);
 497         boolexpr_free(el->rev_dep);
 498
 499         continue;
 500
 501     choice_exception:
 502         // Add exclusive rules for choice symbol
 503         if (sym->rev_dep.expr != NULL) {
 504             Dprintf(" Dependency:\n");
 505             doutput_expr(sym->rev_dep.expr);
 506             el->rev_dep =
 507                 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, true, NULL);
 508         } else
 509             el->rev_dep = boolexpr_true();
 510         for_all_choices(sym, prop) {
 511             struct symbol *symw;
 512             struct expr *exprw;
 513             unsigned *symx = NULL;
 514             size_t symx_size = 0;
 515             int x, y;
 516             expr_list_for_each_sym(prop->expr, exprw, symw) {
 517                 symx_size++;
 518                 symx = realloc(symx, symx_size * sizeof(unsigned));
 519                 symx[symx_size - 1] = symlist_id(gsymlist, symw->name);
 520                 output_rules_symbol(symx[symx_size - 1]);
 521             }
 522             output_rules_symbol(-(int)
 523                                 el_id);
 524             output_rules_endterm();
 525             for (x = 0; x < symx_size - 1; x++) {
 526                 for (y = x + 1; y < symx_size; y++) {
 527                     output_rules_symbol(-(int)
 528                                         symx[x]);
 529                     output_rules_symbol(-(int)
 530                                         symx[y]);
 531                     output_rules_endterm();
 532                 }
 533             }
 534             free(symx);
 535             symx = NULL;
 536         }
 537         if (el->rev_dep->type != BT_FALSE && el->rev_dep->type != BT_TRUE)
 538             cnf_boolexpr(gsymlist, el->rev_dep);
 539         if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
 540             cnf_boolexpr(gsymlist, el->vis);
 541         // (!sym || rev_dep) && (!sym || !rev_dep || vis)
 542         // For nonoptional per list symbol add:
 543         // (sym || !rev_dep || !vis || !dir_dep_of_list))
 544         if (el->rev_dep->type != BT_TRUE) {
 545             output_rules_symbol(-1 * boolsym->id);
 546             if (el->rev_dep->type != BT_FALSE) {
 547                 output_rules_symbol(el->rev_dep->id);
 548             }
 549             output_rules_endterm();
 550         }
 551         if (el->rev_dep->type != BT_FALSE && el->vis->type != BT_TRUE) {
 552             output_rules_symbol(-1 * boolsym->id);
 553             if (el->rev_dep->type != BT_TRUE) {
 554                 output_rules_symbol(-1 * el->rev_dep->id);
 555             }
 556             if (el->vis != BT_FALSE) {
 557                 output_rules_symbol(el->vis->id);
 558             }
 559             output_rules_endterm();
 560         }
 561         if (!sym_is_optional(sym)) {
 562             for_all_choices(sym, prop) {
 563                 struct symbol *symw;
 564                 struct expr *exprw;
 565                 expr_list_for_each_sym(prop->expr, exprw, symw) {
 566                     struct boolexpr *wdep;
 567                     if (symw->dir_dep.expr != NULL) {
 568                         struct symbol *settrue[] = {sym, NULL};
 569                         wdep =
 570                             boolexpr_kconfig(gsymlist, symw->dir_dep.expr,
 571                                              false, settrue);
 572                     } else
 573                         wdep = boolexpr_true();
 574                     cnf_boolexpr(gsymlist, wdep);
 575                     if (el->rev_dep->type != BT_FALSE
 576                         && el->vis->type != BT_FALSE
 577                         && wdep->type != BT_FALSE) {
 578                         output_rules_symbol(boolsym->id);
 579                         if (el->rev_dep->type != BT_TRUE) {
 580                             output_rules_symbol(-1 * el->rev_dep->id);
 581                         }
 582                         if (el->vis->type != BT_TRUE) {
 583                             output_rules_symbol(-1 * el->vis->id);
 584                         }
 585                         if (wdep->type != BT_TRUE
 586                             && wdep->id != boolsym->id) {
 587                             output_rules_symbol(-1 * wdep->id);
 588                         }
 589                         output_rules_endterm();
 590                     }
 591                 }
 592             }
 593         }
 594     }
 595 }
 596
 597 #endif