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 int verbosity = 0;
  14
  15 enum options {
  16         OPT__START = 256,
  17         OPT_BASECONFIG,
  18         OPT_CNF,
  19         OPT_ENV,
  20         OPT_HELP,
  21         OPT_KCONFIG,
  22         OPT_VARFILE,
  23         OPT_VAROPTION,
  24         OPT_VERBOSE,
  25 };
  26
  27 void print_help()
  28 {
  29         printf("kconfig2sat [ options ]\n"
  30                "\n"
  31                "Options:\n"
  32                "-b, --baseconf <.config>  Linux .config file with base configuration\n"
  33                "--env <.conf.mk>          .conf.mk file for setting variables such as ARCH\n"
  34                "-k, --kconfig <Kconfig>   Kconfig file (with path)\n"
  35                "--varfile <file>          File listing variable options (one option per line)\n"
  36                "--cnf <file>              Generate CNF representation to <file>\n"
  37                 );
  38 }
  39
  40 int main(int argc, char **argv)
  41 {
  42         int c;
  43
  44         char *baseconf = NULL;
  45         char *cnf = NULL;
  46         char *kconfig = NULL;
  47         char *varfile = NULL;
  48
  49         while (1) {
  50                 int option_index = 0;
  51                 static struct option long_options[] = {
  52                         {"baseconf",    required_argument, 0,  OPT_BASECONFIG },
  53                         {"cnf",         required_argument, 0,  OPT_CNF },
  54                         {"env",         required_argument, 0,  OPT_ENV },
  55                         {"help",        no_argument,       0,  OPT_HELP },
  56                         {"kconfig",     required_argument, 0,  OPT_KCONFIG },
  57                         {"varfile",     required_argument, 0,  OPT_VARFILE },
  58 //                      {"varopt",      required_argument, 0,  OPT_VAROPTION },
  59                         {"verbose",     no_argument,       0,  OPT_VERBOSE },
  60                         {0,             0,                 0,  0 }
  61                 };
  62
  63                 c = getopt_long(argc, argv, "b:hk:v",
  64                                 long_options, &option_index);
  65                 if (c == -1)
  66                         break;
  67
  68                 switch (c) {
  69                 case 'b':
  70                 case OPT_BASECONFIG:
  71                         baseconf = optarg;
  72                         break;
  73                 case OPT_CNF:
  74                         cnf = optarg;
  75                         break;
  76                 case OPT_ENV:
  77                         set_missing_env(optarg);
  78                         break;
  79                 case 'h':
  80                 case OPT_HELP:
  81                         print_help();
  82                         exit(EXIT_SUCCESS);
  83                 case 'k':
  84                 case OPT_KCONFIG:
  85                         kconfig = optarg;
  86                         break;
  87                 case 'v':
  88                 case OPT_VERBOSE:
  89                         verbosity++;
  90                         break;
  91                 case OPT_VARFILE:
  92                         varfile = optarg;
  93                         break;
  94                 case '?':
  95                 default:
  96                         print_help();
  97                         exit(EXIT_FAILURE);
  98                         printf("?? getopt returned character code 0%o ??\n", c);
  99                 }
 100         }
 101
 102         if (optind < argc) {
 103                 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
 104                 print_help();
 105                 exit(EXIT_FAILURE);
 106         }
 107
 108
 109         if (kconfig == NULL) {
 110                 fprintf(stderr, "--kconfig option missing\n");
 111                 exit(EXIT_FAILURE);
 112         }
 113
 114         setlocale(LC_ALL, "");
 115         bindtextdomain(PACKAGE, LOCALEDIR);
 116         textdomain(PACKAGE);
 117
 118         conf_parse_path(kconfig);
 119
 120 //      char *rules_file, *symbol_map_file, *variable_count_file;
 121 //      asprintf(&rules_file, "%s/%s", folder, DEFAULT_RULES_FILE);
 122 //      asprintf(&symbol_map_file, "%s/%s", folder, DEFAULT_SYMBOL_MAP_FILE);
 123 //      asprintf(&variable_count_file, "%s/%s", folder,
 124 //               DEFAULT_VARIABLE_COUNT_FILE);
 125 //      output_init(rules_file, symbol_map_file);
 126
 127 //      build_symlist();
 128 //      cpy_dep();
 129
 130 //      output_write_variable_count(variable_count_file,
 131 //                                  gsymlist->lastsym - 1, gsymlist->pos);
 132
 133 //      output_finish();
 134         return EXIT_SUCCESS;
 135 }
 136
 137 #if 0
 138
 139 void build_symlist() {
 140     int i;
 141     struct symbol *sym;
 142     struct property *prop;
 143     for_all_symbols(i, sym) {
 144         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
 145             if (sym->name == NULL)
 146                 asprintf(&sym->name, "NONAMEGEN%d", noname_num++);
 147
 148             symlist_add(gsymlist, sym->name);
 149         }
 150     }
 151     symlist_closesym(gsymlist);
 152 }
 153
 154 /* TODO: Split to smaller functions with meaningful names */
 155 void cpy_dep() {
 156     int i;
 157     struct symbol *sym;
 158     struct property *prop;
 159     struct symlist_el *el;
 160     unsigned el_id;
 161     struct boolexpr *boolsym;
 162     for_all_symbols(i, sym) {
 163         if (sym->type != S_BOOLEAN && sym->type != S_TRISTATE)
 164             continue;
 165         el_id = symlist_id(gsymlist, sym->name);
 166         el = &(gsymlist->array[el_id - 1]);
 167         boolsym = boolexpr_sym(gsymlist, sym, false, NULL);
 168         Iprintf("Processing: %s\n", sym->name);
 169         // Visibility
 170         for_all_prompts(sym, prop) {
 171             Dprintf(" Prompt: %s\n", prop->text);
 172             if (prop->visible.expr != NULL) {
 173                 doutput_expr(prop->visible.expr);
 174                 struct boolexpr *vis =
 175                     boolexpr_kconfig(gsymlist, prop->visible.expr,
 176                                      false, NULL);
 177                 if (el->vis == NULL) {
 178                     el->vis = vis;
 179                 } else {
 180                     el->vis = boolexpr_or(el->vis, vis);
 181                 }
 182             } else if (el->vis == NULL) {
 183                 el->vis = boolexpr_true();
 184             }
 185         }
 186         if (el->vis == NULL)
 187             el->vis = boolexpr_false();
 188         // Symbol is choice.. special treatment required
 189         if (sym_is_choice(sym)) {
 190             Dprintf(" Is Choice\n");
 191             goto choice_exception;
 192         }
 193         // Default value
 194         struct boolexpr **defexpr = NULL;
 195         size_t defexpr_size = 0;
 196         int z;
 197         bool exitdef = false;
 198         for_all_defaults(sym, prop) {
 199             Dprintf(" Default value:\n");
 200             doutput_expr(prop->expr);
 201             struct boolexpr *def =
 202                 boolexpr_kconfig(gsymlist, prop->expr, true, NULL);
 203             struct boolexpr *vis;
 204             if (prop->visible.expr != NULL)
 205                 vis = boolexpr_kconfig(gsymlist, prop->visible.expr,
 206                                        false, NULL);
 207             else
 208                 vis = boolexpr_true();
 209             if (vis->type != BT_TRUE) {
 210                 defexpr = realloc(defexpr,
 211                                   ++defexpr_size * sizeof(struct boolexpr *));
 212                 defexpr[defexpr_size - 1] = boolexpr_copy(vis);
 213             } else {
 214                 ++defexpr_size;
 215                 exitdef = true;
 216             }
 217             def = boolexpr_and(def, vis);
 218             for (z = 0; z < ((int)defexpr_size - 1); z++) {
 219                 def = boolexpr_and(def, boolexpr_not(
 220                                        boolexpr_copy(defexpr[z])));
 221             }
 222             if (el->def == NULL)
 223                 el->def = def;
 224             else
 225                 el->def = boolexpr_or(el->def, def);
 226             if (exitdef)
 227                 break;
 228         }
 229         if (defexpr != NULL) {
 230             for (z = 0; z < defexpr_size - 1; z++) {
 231                 boolexpr_free(defexpr[z]);
 232             }
 233             free(defexpr);
 234         }
 235         if (el->def == NULL)
 236             el->def = boolexpr_false();
 237         // Dependency expression
 238         if (sym->dir_dep.expr != NULL) {
 239             Dprintf(" Dependency:\n");
 240             doutput_expr(sym->dir_dep.expr);
 241             el->dep =
 242                 boolexpr_kconfig(gsymlist, sym->dir_dep.expr, false, NULL);
 243         } else
 244             el->dep = boolexpr_true();
 245         // Reverse dependency expression
 246         if (sym->rev_dep.expr != NULL) {
 247             Dprintf(" Reverse dependency:\n");
 248             doutput_expr(sym->rev_dep.expr);
 249             el->rev_dep =
 250                 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, false, NULL);
 251         } else
 252             el->rev_dep = boolexpr_false();
 253
 254         if (el->dep->type != BT_FALSE && el->dep->type != BT_TRUE)
 255             cnf_boolexpr(gsymlist, el->dep);
 256         if (el->rev_dep->type != BT_FALSE
 257             && el->rev_dep->type != BT_TRUE)
 258             cnf_boolexpr(gsymlist, el->rev_dep);
 259         if (el->def->type != BT_FALSE && el->def->type != BT_TRUE)
 260             cnf_boolexpr(gsymlist, el->def);
 261         if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
 262             cnf_boolexpr(gsymlist, el->vis);
 263         // (!sym || dep) && (sym || !rev_dep) &&
 264         // && (sym || !dep || !def || vis) &&
 265         // (!sym || rev_dep || def || vis)
 266         if (el->dep->type != BT_TRUE) {
 267             output_rules_symbol(-1 * boolsym->id);
 268             if (el->dep->type != BT_FALSE) {
 269                 output_rules_symbol(el->dep->id);
 270             }
 271             output_rules_endterm();
 272         }
 273         if (el->rev_dep->type != BT_FALSE) {
 274             output_rules_symbol(boolsym->id);
 275             if (el->rev_dep->type != BT_TRUE) {
 276                 output_rules_symbol(-1 * el->rev_dep->id);
 277             }
 278             output_rules_endterm();
 279         }
 280         if (el->dep->type != BT_FALSE && el->def->type != BT_FALSE
 281             && el->vis->type != BT_TRUE) {
 282             output_rules_symbol(boolsym->id);
 283             if (el->dep->type != BT_TRUE) {
 284                 output_rules_symbol(-1 * el->dep->id);
 285             }
 286             if (el->def->type != BT_TRUE) {
 287                 output_rules_symbol(-1 * el->def->id);
 288             }
 289             if (el->vis->type != BT_FALSE) {
 290                 output_rules_symbol(el->vis->id);
 291             }
 292             output_rules_endterm();
 293         }
 294         if (el->rev_dep->type != BT_TRUE && el->def->type != BT_TRUE
 295             && el->vis->type != BT_TRUE) {
 296             output_rules_symbol(-1 * boolsym->id);
 297             if (el->rev_dep->type != BT_FALSE) {
 298                 output_rules_symbol(el->rev_dep->id);
 299             }
 300             if (el->def->type != BT_FALSE) {
 301                 output_rules_symbol(el->def->id);
 302             }
 303             if (el->vis->type != BT_FALSE) {
 304                 output_rules_symbol(el->vis->id);
 305             }
 306             output_rules_endterm();
 307         }
 308
 309         boolexpr_free(el->def);
 310         boolexpr_free(el->vis);
 311         boolexpr_free(el->dep);
 312         boolexpr_free(el->rev_dep);
 313
 314         continue;
 315
 316     choice_exception:
 317         // Add exclusive rules for choice symbol
 318         if (sym->rev_dep.expr != NULL) {
 319             Dprintf(" Dependency:\n");
 320             doutput_expr(sym->rev_dep.expr);
 321             el->rev_dep =
 322                 boolexpr_kconfig(gsymlist, sym->rev_dep.expr, true, NULL);
 323         } else
 324             el->rev_dep = boolexpr_true();
 325         for_all_choices(sym, prop) {
 326             struct symbol *symw;
 327             struct expr *exprw;
 328             unsigned *symx = NULL;
 329             size_t symx_size = 0;
 330             int x, y;
 331             expr_list_for_each_sym(prop->expr, exprw, symw) {
 332                 symx_size++;
 333                 symx = realloc(symx, symx_size * sizeof(unsigned));
 334                 symx[symx_size - 1] = symlist_id(gsymlist, symw->name);
 335                 output_rules_symbol(symx[symx_size - 1]);
 336             }
 337             output_rules_symbol(-(int)
 338                                 el_id);
 339             output_rules_endterm();
 340             for (x = 0; x < symx_size - 1; x++) {
 341                 for (y = x + 1; y < symx_size; y++) {
 342                     output_rules_symbol(-(int)
 343                                         symx[x]);
 344                     output_rules_symbol(-(int)
 345                                         symx[y]);
 346                     output_rules_endterm();
 347                 }
 348             }
 349             free(symx);
 350             symx = NULL;
 351         }
 352         if (el->rev_dep->type != BT_FALSE && el->rev_dep->type != BT_TRUE)
 353             cnf_boolexpr(gsymlist, el->rev_dep);
 354         if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
 355             cnf_boolexpr(gsymlist, el->vis);
 356         // (!sym || rev_dep) && (!sym || !rev_dep || vis)
 357         // For nonoptional per list symbol add:
 358         // (sym || !rev_dep || !vis || !dir_dep_of_list))
 359         if (el->rev_dep->type != BT_TRUE) {
 360             output_rules_symbol(-1 * boolsym->id);
 361             if (el->rev_dep->type != BT_FALSE) {
 362                 output_rules_symbol(el->rev_dep->id);
 363             }
 364             output_rules_endterm();
 365         }
 366         if (el->rev_dep->type != BT_FALSE && el->vis->type != BT_TRUE) {
 367             output_rules_symbol(-1 * boolsym->id);
 368             if (el->rev_dep->type != BT_TRUE) {
 369                 output_rules_symbol(-1 * el->rev_dep->id);
 370             }
 371             if (el->vis != BT_FALSE) {
 372                 output_rules_symbol(el->vis->id);
 373             }
 374             output_rules_endterm();
 375         }
 376         if (!sym_is_optional(sym)) {
 377             for_all_choices(sym, prop) {
 378                 struct symbol *symw;
 379                 struct expr *exprw;
 380                 expr_list_for_each_sym(prop->expr, exprw, symw) {
 381                     struct boolexpr *wdep;
 382                     if (symw->dir_dep.expr != NULL) {
 383                         struct symbol *settrue[] = {sym, NULL};
 384                         wdep =
 385                             boolexpr_kconfig(gsymlist, symw->dir_dep.expr,
 386                                              false, settrue);
 387                     } else
 388                         wdep = boolexpr_true();
 389                     cnf_boolexpr(gsymlist, wdep);
 390                     if (el->rev_dep->type != BT_FALSE
 391                         && el->vis->type != BT_FALSE
 392                         && wdep->type != BT_FALSE) {
 393                         output_rules_symbol(boolsym->id);
 394                         if (el->rev_dep->type != BT_TRUE) {
 395                             output_rules_symbol(-1 * el->rev_dep->id);
 396                         }
 397                         if (el->vis->type != BT_TRUE) {
 398                             output_rules_symbol(-1 * el->vis->id);
 399                         }
 400                         if (wdep->type != BT_TRUE
 401                             && wdep->id != boolsym->id) {
 402                             output_rules_symbol(-1 * wdep->id);
 403                         }
 404                         output_rules_endterm();
 405                     }
 406                 }
 407             }
 408         }
 409     }
 410 }
 411
 412 #endif