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_DUMP,
  27         OPT_ENV,
  28         OPT_HELP,
  29         OPT_KCONFIG,
  30         OPT_VARFILE,
  31         OPT_VAROPTION,
  32         OPT_VERBOSE,
  33 };
  34
  35 void print_help()
  36 {
  37         printf("Usage: kconfig2sat [options/actions]\n"
  38                "\n"
  39                "Options:\n"
  40                "  -b, --baseconf <.config>  Linux .config file with base configuration\n"
  41                "  --env <.conf.mk>          Set env. variables such as ARCH from .conf.mk\n"
  42                "  -k, --kconfig <Kconfig>   Kconfig file (with path)\n"
  43                "  --varfile <file>          File listing variable options (one option per line)\n"
  44                "\n"
  45                "Actions:\n"
  46                "  --dump                    Dump internal data (for debugging)\n"
  47                "  --cnf <file>              Generate CNF representation to <file>\n"
  48                 );
  49 }
  50
  51 char *expr_to_string(struct expr *e);
  52
  53 char *sym_to_string(struct symbol *sym)
  54 {
  55         char *ret;
  56
  57         if (sym->name)
  58                 asprintf(&ret, sym->name);
  59         else
  60                 asprintf(&ret, "NONAME%d", sym->lcp.id);
  61         return ret;
  62 }
  63
  64 char *expr_binop_to_string(struct expr *e, const char *op_str)
  65 {
  66         char *l = expr_to_string(e->left.expr);
  67         char *r = expr_to_string(e->right.expr);
  68         char *ret;
  69
  70         asprintf(&ret, "(%s %s %s)", l, op_str, r);
  71         free(l);
  72         free(r);
  73         return ret;
  74 }
  75
  76 char *expr_comp_to_string(struct expr *e, const char *op_str)
  77 {
  78         char *l = sym_to_string(e->left.sym);
  79         char *r = sym_to_string(e->right.sym);
  80         char *ret;
  81
  82         asprintf(&ret, "(%s %s %s)", l, op_str, r);
  83         free(l);
  84         free(r);
  85         return ret;
  86 }
  87
  88 char *expr_to_string(struct expr *e)
  89 {
  90         char *ret = NULL;
  91         char *tmp;
  92
  93         if (!e)
  94                 return NULL;
  95
  96         switch (e->type) {
  97         case E_NONE:
  98                 asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr));
  99                 return ret;
 100         case E_OR:
 101                 return expr_binop_to_string(e, "||");
 102         case E_AND:
 103                 return expr_binop_to_string(e, "&&");
 104         case E_NOT:
 105                 tmp = expr_to_string(e->left.expr);
 106                 asprintf(&ret, "!%s", tmp);
 107                 free(tmp);
 108                 return ret;
 109         case E_EQUAL:
 110                 return expr_comp_to_string(e, "==");
 111         case E_UNEQUAL:
 112                 return expr_comp_to_string(e, "!=");
 113         case E_LTH:
 114                 return expr_comp_to_string(e, "<");
 115         case E_LEQ:
 116                 return expr_comp_to_string(e, "<=");
 117         case E_GTH:
 118                 return expr_comp_to_string(e, ">");
 119         case E_GEQ:
 120                 return expr_comp_to_string(e, ">=");
 121         case E_LIST:
 122                 fprintf(stderr, "LIST not implemented\n");
 123                 exit(EXIT_FAILURE);
 124                 break;
 125         case E_SYMBOL:
 126                 return sym_to_string(e->left.sym);
 127         case E_RANGE:
 128                 fprintf(stderr, "RANGE not implemented\n");
 129                 exit(EXIT_FAILURE);
 130                 break;
 131         }
 132
 133         return ret;
 134 }
 135
 136
 137
 138 void dump_symbol(struct symbol *sym)
 139 {
 140         struct property *prop;
 141         const char *name = sym_to_string(sym);
 142         const char *type = sym_type_name(sym->type);
 143         const char *prompt = NULL;
 144         char *tmp;
 145         char flags[256] = "fl(";
 146         char val = '.';
 147
 148         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
 149                 switch (sym->curr.tri) {
 150                 case no:  val = 'n'; break;
 151                 case mod: val = 'm'; break;
 152                 case yes: val = 'y'; break;
 153                 }
 154         }
 155
 156 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
 157         FLAG(CONST);
 158         FLAG(CHECK);
 159         FLAG(CHOICE);
 160         FLAG(CHOICEVAL);
 161         FLAG(VALID);
 162         FLAG(OPTIONAL);
 163         FLAG(WRITE);
 164         FLAG(CHANGED);
 165         FLAG(AUTO);
 166         FLAG(CHECKED);
 167         FLAG(WARNED);
 168         FLAG(DEF_USER);
 169         FLAG(DEF_AUTO);
 170         FLAG(DEF3);
 171         FLAG(DEF4);
 172         if (flags[3])
 173                 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
 174 #undef FLAG
 175
 176         for_all_properties(sym, prop, P_PROMPT) {
 177                 prompt = prop->text;
 178         }
 179
 180         printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt);
 181
 182         if (verbosity > 0) {
 183                 if (sym->dir_dep.expr) {
 184                         tmp = expr_to_string(sym->dir_dep.expr);
 185                         printf("    depends %s\n", tmp);
 186                         free(tmp);
 187                 }
 188
 189                 for_all_properties(sym, prop, P_SELECT) {
 190                         assert(prop->expr->type == E_SYMBOL);
 191                         tmp = expr_to_string(prop->visible.expr);
 192                         printf("    selects %s if %s\n", prop->expr->left.sym->name, tmp);
 193                         free(tmp);
 194
 195                 }
 196         }
 197 }
 198
 199 void do_dump()
 200 {
 201     int i;
 202     struct symbol *sym;
 203     for_all_symbols(i, sym) {
 204             dump_symbol(sym);
 205     }
 206 }
 207
 208 void read_varfile(const char *varfile)
 209 {
 210         FILE *f = fopen(varfile, "r");
 211         char line[1000];
 212
 213         if (!f) {
 214                 perror(varfile);
 215                 exit(EXIT_FAILURE);
 216         }
 217
 218         int lineno = 0;
 219         while (fgets(line, sizeof(line), f)) {
 220                 char *p = line;
 221                 lineno++;
 222
 223                 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
 224                         p += strlen(CONFIG_);
 225
 226                 const char *sym_name = strtok(p, " =\n");
 227                 struct symbol *sym = sym_find(sym_name);
 228                 if (!sym) {
 229                         fprintf(stderr, "%s:%d: Invalid symbol: %s\n", varfile, lineno, sym_name);
 230                         exit(EXIT_FAILURE);
 231                 }
 232                 if (!(sym->flags & SYMBOL_WRITE)) {
 233                         fprintf(stderr, "%s:%d: Symbol %s not visible\n", varfile, lineno, sym_name);
 234                         exit(EXIT_FAILURE);
 235                 }
 236                 if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
 237                         fprintf(stderr, "%s:%d: Choice values not yet supported: %s", varfile, lineno, sym_name);
 238                         exit(EXIT_FAILURE);
 239                 }
 240                 struct property *prop;
 241                 const char *prompt = NULL;
 242                 for_all_properties(sym, prop, P_PROMPT) {
 243                         prompt = prop->text;
 244                 }
 245                 if (!prompt) {
 246                         fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
 247                 }
 248                 sym->lcp.variable = 1;
 249         }
 250         fclose(f);
 251 }
 252
 253 struct SatLiteral {
 254         struct symbol *sym;
 255         struct expr *expr;
 256
 257         SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
 258         SatLiteral(struct expr *e)   : sym(nullptr), expr(e) {}
 259         bool has_fixed_value() const { return sym && !sym->lcp.variable; }
 260         sat_id id() const { return sym ? sym->lcp.id : expr->lcp.id; }
 261         bool value() const { assert(sym); return sym->curr.tri == yes; }
 262 };
 263
 264 typedef vector<sat_id> SatClause;
 265
 266 struct SatExpr {
 267         sat_id left, right;
 268         enum expr_type op;
 269
 270         SatExpr(int l, enum expr_type o, int r)
 271                 : left(l), right(r), op(o) {}
 272         bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
 273 };
 274
 275 class SatLiterals : public vector<struct SatLiteral>
 276 {
 277 public:
 278         int fixed = {0};
 279         SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
 280         int count() const { return size() - 1; }
 281 };
 282
 283
 284 /*
 285  * bool FOO!=n => FOO
 286  * bool FOO!=y => !FOO
 287  * bool FOO==n => !FOO
 288  * bool FOO==y => FOO
 289  */
 290 struct expr *expr_eliminate_eq_yn(struct expr *e)
 291 {
 292         if (!e)
 293                 return NULL;
 294         switch (e->type) {
 295         case E_AND:
 296         case E_OR:
 297         case E_NOT:
 298                 e->left.expr = expr_eliminate_eq_yn(e->left.expr);
 299                 e->right.expr = expr_eliminate_eq_yn(e->right.expr);
 300                 break;
 301         case E_UNEQUAL:
 302                 // UNKNOWN symbols sometimes occur in dependency -
 303                 // e.g. ACPI_VIDEO on arm (the symbol is only defined
 304                 // for ACPI platforms (x86) but some drivers refer to
 305                 // it.
 306                 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
 307                         if (e->right.sym == &symbol_no) {
 308                                 // FOO!=n -> FOO
 309                                 e->type = E_SYMBOL;
 310                                 e->right.sym = NULL;
 311                         } else if (e->right.sym == &symbol_yes) {
 312                                 // FOO!=y -> !FOO
 313                                 e->type = E_SYMBOL;
 314                                 e->right.sym = NULL;
 315                                 e = expr_alloc_one(E_NOT, e);
 316                         }
 317                 }
 318                 break;
 319         case E_EQUAL:
 320                 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
 321                         if (e->right.sym == &symbol_yes) {
 322                                 // FOO==y -> FOO
 323                                 e->type = E_SYMBOL;
 324                                 e->right.sym = NULL;
 325                         } else if (e->right.sym == &symbol_no) {
 326                                 // FOO==n -> !FOO
 327                                 e->type = E_SYMBOL;
 328                                 e->right.sym = NULL;
 329                                 e = expr_alloc_one(E_NOT, e);
 330                         }
 331                 }
 332                 break;
 333         default:
 334                 ;
 335         }
 336         return e;
 337 }
 338
 339
 340 class SatData {
 341         SatLiterals literals = {};
 342         vector<SatClause> clauses = {};
 343         map<SatExpr, sat_id> expressions = {};
 344
 345 public:
 346
 347         SatData() {
 348                 symbols2literals();
 349                 expressions2literals();
 350                 symbols2clauses();
 351                 expressions2clauses();
 352         }
 353
 354         void add_symbol_literal(struct symbol *sym) {
 355                 literals.push_back(SatLiteral(sym));
 356                 sym->lcp.id = literals.count();
 357         }
 358
 359         void symbols2literals() {
 360                 int i;
 361                 struct symbol *sym;
 362
 363                 symbol_yes.type = S_TRISTATE;
 364                 symbol_no.type  = S_TRISTATE;
 365                 symbol_mod.type = S_TRISTATE;
 366
 367                 add_symbol_literal(&symbol_yes);
 368                 add_symbol_literal(&symbol_no);
 369                 add_symbol_literal(&symbol_mod);
 370
 371                 for_all_symbols(i, sym) {
 372                         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE || sym->type == S_UNKNOWN) {
 373                                 add_symbol_literal(sym);
 374                         }
 375                 }
 376         }
 377
 378         void expr2literal(struct expr *e) {
 379                 if (!e || e->lcp.id)
 380                         return;
 381
 382                 switch (e->type) {
 383                 case E_SYMBOL:
 384                         e->lcp.id = e->left.sym->lcp.id;
 385                         break;
 386                 case E_NONE:
 387                         fprintf(stderr, "NONE not implemented\n");
 388                         exit(EXIT_FAILURE);
 389                         break;
 390                 case E_NOT: {
 391                         expr2literal(e->left.expr);
 392
 393                         SatExpr se(e->left.expr->lcp.id, e->type, 0);
 394                         auto it = expressions.find(se);
 395                         if (it == expressions.end()) {
 396                                 literals.push_back(SatLiteral(e));
 397                                 expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
 398                                 e->lcp.id = literals.count();
 399                         } else
 400                                 e->lcp.id = it->second;
 401                         break;
 402                 }
 403                 case E_OR:
 404                 case E_AND: {
 405                         expr2literal(e->left.expr);
 406                         expr2literal(e->right.expr);
 407
 408                         SatExpr se(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id);
 409                         auto it = expressions.find(se);
 410                         if (it == expressions.end()) {
 411                                 literals.push_back(SatLiteral(e));
 412                                 expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
 413                                 e->lcp.id = literals.count();
 414                         } else
 415                                 e->lcp.id = it->second;
 416                         break;
 417                 }
 418                 case E_EQUAL:
 419                 case E_UNEQUAL:
 420                 case E_LTH:
 421                 case E_LEQ:
 422                 case E_GTH:
 423                 case E_GEQ: {
 424                         SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id);
 425                         auto it = expressions.find(se);
 426                         if (it == expressions.end()) {
 427                                 literals.push_back(SatLiteral(e));
 428                                 expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
 429                                 e->lcp.id = literals.count();
 430                         } else
 431                                 e->lcp.id = it->second;
 432                         break;
 433                 }
 434                 case E_LIST:
 435                         fprintf(stderr, "LIST not implemented\n");
 436                         exit(EXIT_FAILURE);
 437                         break;
 438                 case E_RANGE:
 439                         fprintf(stderr, "RANGE not implemented\n");
 440                         exit(EXIT_FAILURE);
 441                         break;
 442                 }
 443         }
 444
 445         void expressions2literals() {
 446                 int i;
 447                 struct symbol *sym;
 448                 struct property *prop;
 449
 450                 for_all_symbols(i, sym) {
 451                         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
 452                                 assert(sym->lcp.id);
 453                                 if (sym->flags & SYMBOL_VALID && !sym->lcp.variable)
 454                                         clauses.push_back(SatClause{ sym->curr.tri == yes ? sym->lcp.id : -sym->lcp.id });
 455
 456                                 sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
 457                                 expr2literal(sym->dir_dep.expr);
 458
 459                                 for_all_properties(sym, prop, P_SELECT) {
 460                                         assert(prop->expr->type == E_SYMBOL);
 461                                         prop->visible.expr = expr_eliminate_eq_yn(prop->visible.expr);
 462                                         expr2literal(prop->visible.expr);
 463                                 }
 464                         }
 465                 }
 466         }
 467
 468         void symbols2clauses() {
 469                 for (auto lit: literals)
 470                         if (lit.sym && lit.has_fixed_value())
 471                                 clauses.push_back(SatClause{ lit.value() ? lit.id() : -lit.id() });
 472         }
 473
 474         void expressions2clauses() {
 475                 // Tseitin Transformation - see https://en.wikipedia.org/wiki/Tseitin_transformation
 476                 // or http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
 477                 for (auto expr: expressions) {
 478                         SatExpr e = expr.first;
 479                         sat_id e_id = expr.second;
 480                         assert(e_id);
 481                         if (e.left == 0 || (e.right == 0 && e.op != E_NOT)) {
 482                                 unique_ptr<char> tmp(expr_to_string(literals[e_id].expr));
 483                                 printf("Unexpected sat_id == 0 in %s\n", tmp.get());
 484                                 //exit(1);
 485                         }
 486                         switch (e.op) {
 487                         case E_SYMBOL:
 488                         case E_NONE:
 489                                 assert(0);
 490                                 break;
 491                         case E_NOT:
 492                                 clauses.push_back(SatClause{  e_id,  e.left });
 493                                 clauses.push_back(SatClause{ -e_id, -e.left });
 494                                 break;
 495                         case E_OR:
 496                                 clauses.push_back(SatClause{ -e.left,  e_id });
 497                                 clauses.push_back(SatClause{ -e.right, e_id });
 498                                 clauses.push_back(SatClause{ -e_id,    e.left, e.right });
 499                                 break;
 500                         case E_AND:
 501                                 clauses.push_back(SatClause{ -e_id, e.left });
 502                                 clauses.push_back(SatClause{ -e_id, e.right });
 503                                 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
 504                                 break;
 505                         case E_EQUAL:
 506                                 clauses.push_back(SatClause{ -e_id, -e.left, e.right });
 507                                 clauses.push_back(SatClause{ -e_id, -e.right, e.left });
 508                                 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
 509                                 clauses.push_back(SatClause{ e.left, e.right, e_id });
 510                                 break;
 511                         case E_UNEQUAL:
 512                                 clauses.push_back(SatClause{ -e_id, -e.left, -e.right });
 513                                 clauses.push_back(SatClause{ -e_id, e.right, e.left });
 514                                 clauses.push_back(SatClause{ -e.left, e.right, e_id });
 515                                 clauses.push_back(SatClause{ e.left, -e.right, e_id });
 516                                 break;
 517                         case E_LTH:
 518                         case E_LEQ:
 519                         case E_GTH:
 520                         case E_GEQ: {
 521                                 struct expr *e = literals[e_id].expr;
 522                                 unique_ptr<char> tmp(expr_to_string(e));
 523                                 tristate val = expr_calc_value(e);
 524                                 //fprintf(stderr, "Comparison operators not implemented %s = %d\n", tmp.get(), val);
 525                                 //exit(EXIT_FAILURE);
 526                                 clauses.push_back(SatClause{ val == yes ? e_id : -e_id });
 527                                 break;
 528                         }
 529                         case E_LIST:
 530                                 fprintf(stderr, "LIST not implemented\n");
 531                                 exit(EXIT_FAILURE);
 532                                 break;
 533                         case E_RANGE:
 534                                 fprintf(stderr, "RANGE not implemented\n");
 535                                 exit(EXIT_FAILURE);
 536                                 break;
 537                         }
 538                 }
 539
 540         }
 541
 542         void write_dimacs_cnf(const char *cnf) {
 543                 FILE *f = fopen(cnf, "w");
 544
 545                 if (!f) {
 546                         perror(cnf);
 547                         exit(EXIT_FAILURE);
 548                 }
 549
 550                 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
 551
 552                 for (auto l: literals) {
 553                         if (l.sym) {
 554                                 char val = l.has_fixed_value() ? (l.value() ? 'y' : 'n') : '?';
 555                                 fprintf(f, "c SYM %d %s = %c\n", l.sym->lcp.id, l.sym->name, val);
 556                         }
 557                         if (l.expr) {
 558                                 char *tmp = expr_to_string(l.expr);
 559                                 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, tmp);
 560                                 free(tmp);
 561                         }
 562                 }
 563                 for (auto clause: clauses) {
 564                         for (sat_id id: clause) {
 565                                 assert(id != 0);
 566                                 fprintf(f, "%d ", id);
 567                         }
 568                         fprintf(f, "0\n");
 569                 }
 570                 fclose(f);
 571         }
 572 };
 573
 574 int main(int argc, char **argv)
 575 {
 576         int c;
 577
 578         char *baseconf = NULL;
 579         char *cnf = NULL;
 580         char *kconfig = NULL;
 581         char *varfile = NULL;
 582         int  dump = false;
 583
 584         while (1) {
 585                 int option_index = 0;
 586                 static struct option long_options[] = {
 587                         {"baseconf",    required_argument, 0,     OPT_BASECONFIG },
 588                         {"cnf",         required_argument, 0,     OPT_CNF },
 589                         {"env",         required_argument, 0,     OPT_ENV },
 590                         {"dump",        no_argument,       &dump, true },
 591                         {"help",        no_argument,       0,     OPT_HELP },
 592                         {"kconfig",     required_argument, 0,     OPT_KCONFIG },
 593                         {"varfile",     required_argument, 0,     OPT_VARFILE },
 594 //                      {"varopt",      required_argument, 0,     OPT_VAROPTION },
 595                         {"verbose",     no_argument,       0,     OPT_VERBOSE },
 596                         {0,             0,                 0,     0 }
 597                 };
 598
 599                 c = getopt_long(argc, argv, "b:hk:v",
 600                                 long_options, &option_index);
 601                 if (c == -1)
 602                         break;
 603
 604                 switch (c) {
 605                 case 0: /* long option with flag != NULL */
 606                         break;
 607                 case 'b':
 608                 case OPT_BASECONFIG:
 609                         baseconf = optarg;
 610                         break;
 611                 case OPT_CNF:
 612                         cnf = optarg;
 613                         break;
 614                 case OPT_ENV:
 615                         set_missing_env(optarg);
 616                         break;
 617                 case 'h':
 618                 case OPT_HELP:
 619                         print_help();
 620                         exit(EXIT_SUCCESS);
 621                 case 'k':
 622                 case OPT_KCONFIG:
 623                         kconfig = optarg;
 624                         break;
 625                 case 'v':
 626                 case OPT_VERBOSE:
 627                         verbosity++;
 628                         break;
 629                 case OPT_VARFILE:
 630                         varfile = optarg;
 631                         break;
 632                 case '?':
 633                 default:
 634                         print_help();
 635                         exit(EXIT_FAILURE);
 636                         printf("?? getopt returned character code 0%o ??\n", c);
 637                 }
 638         }
 639
 640         if (optind < argc) {
 641                 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
 642                 print_help();
 643                 exit(EXIT_FAILURE);
 644         }
 645
 646
 647         if (kconfig == NULL) {
 648                 fprintf(stderr, "--kconfig option missing\n");
 649                 exit(EXIT_FAILURE);
 650         }
 651
 652         setlocale(LC_ALL, "");
 653         bindtextdomain(PACKAGE, LOCALEDIR);
 654         textdomain(PACKAGE);
 655
 656         conf_parse_path(kconfig);
 657         if (baseconf)
 658                 conf_read(baseconf);
 659
 660         SatData sat_data;
 661
 662         if (varfile)
 663                 read_varfile(varfile);
 664
 665         if (dump)
 666                 do_dump();
 667
 668         if (cnf) {
 669                 sat_data.write_dimacs_cnf(cnf);
 670         }
 671
 672         return EXIT_SUCCESS;
 673 }