#!/usr/bin/env python

import sys
import os
import argparse
import z3
import regex
import pickle
import random

def info(msg, ending="\n"):
  sys.stderr.write("INFO: %s%s" % (msg, ending))

def warning(msg, ending="\n"):
  sys.stderr.write("WARNING: %s%s" % (msg, ending))

def error(msg, ending="\n"):
  sys.stderr.write("ERROR: %s%s" % (msg, ending))

def get_kconfig_extract(formulas, arch):
  """Return a list of lists, where each list is a line from the kconfig_extract, currently only the config lines.  See docs/kconfig_extract_format.md.  Returns None if no file is found."""
  kconfig_extract_file = get_arch_kconfig_extract_file(formulas, arch)
  if not os.path.exists(kconfig_extract_file):
    warning("no kconfig_extract file found: %s", kconfig_extract_file)
    return None
  else:
    lists = []
    with open(kconfig_extract_file, 'r') as fp:
      for line in fp:
        line = line.strip()
        lists.append(line.split())
      return lists
  
def get_kclause_constraints(kclause_file):
  with open(kclause_file, 'r') as fp:
    # kclause, defined_vars, used_vars = pickle.load(fp)
    kclause = pickle.load(fp)

    kclause_constraints = {}
    for var in kclause.keys():
      kclause_constraints[var] = [ z3.parse_smt2_string(clause) for clause in kclause[var] ]

    constraints = []
    for var in kclause_constraints.keys():
      for z3_clause in kclause_constraints[var]:
        constraints.extend(z3_clause)

    return constraints

def unpickle_kmax_file(kmax_file):
  with open(kmax_file, 'r') as fp:
    kmax = pickle.load(fp)
    return kmax

def get_resolved_to_kbuild_map(kmax):
  # resolve all kbuild paths to file names, remove ../ relative
  # paths.  these paths are needed in the kmax formulas to preserve
  # the conditions on each subdirectory leading to the compilation
  # unit, which may not strictly be subdirectories.
  resolved_to_kbuild_map = {}
  for key in kmax.keys():
    resolved_filename = os.path.relpath(os.path.abspath(key))
    if key.endswith("/"):
      # preserve the ending slash, which signals a subdirectory
      # instead of a compilation unit in kbuild
      resolved_filename = resolved_filename + "/"
    resolved_to_kbuild_map[resolved_filename] = key
  return resolved_to_kbuild_map

def get_kmax_constraints(kmax_formulas, resolved_to_kbuild_map, compilation_unit, view=False):
  if compilation_unit not in resolved_to_kbuild_map.keys():
    return None
  else:
    kmax_constraints = []
    kbuild_path = resolved_to_kbuild_map[compilation_unit]
    info("Full path via Kbuild: %s" %(kbuild_path))
    if kbuild_path in kmax_formulas.keys():
      # add the condition for the compilation unit and each of its parent directories
      comp_unit_constraint = z3.parse_smt2_string(kmax_formulas[kbuild_path])
      kmax_constraints.extend(comp_unit_constraint)
      if view:
        print("%s\n%s\n" % (kbuild_path, comp_unit_constraint))
      if '/' in kbuild_path:
        subpath, basename = kbuild_path.rsplit('/', 1)
        elems = subpath.rsplit('/')
        for i in range(0, len(elems)):
          subarray = elems[0:(len(elems) - i)]
          subsubpath = '/'.join(subarray) + "/"
          if subsubpath in kmax_formulas.keys():
            subsubpath_constraint = z3.parse_smt2_string(kmax_formulas[subsubpath])
            kmax_constraints.extend(subsubpath_constraint)
            if view:
              print("%s\n%s\n" % (subsubpath, subsubpath_constraint))
          else:
            info("%s has no kmax formula, assuming it is unconstrained." % (subsubpath))
    return kmax_constraints

def print_model_as_config(model, fp=sys.stdout, kconfig_extract=None):
  info("Printing model as config file to %s." % ("stdout" if fp == sys.stdout else (fp.name)))

  if kconfig_extract == None:
    info("No kconfig_extract file available.  Assuming all configuration options are Boolean")
    types = None
  else:
    types = {}
    for kconfig_line in kconfig_extract:
      # see docs/kconfig_extract_format.md for more info
      if kconfig_line[0] == "config":
        types[kconfig_line[1]] = kconfig_line[2]

  if model is not None:
    # print the model in .config format
    token_pattern = regex.compile("CONFIG_[A-Za-z0-9_]+")
    for entry in model:
      str_entry = str(entry)
      matches = token_pattern.match(str_entry)
      if matches:
        # if str_entry not in kclause_constraints.keys():
        #   sys.stderr.write("warning: %s was not defined in the kconfig spec, but may be required for this unit.\n" % (str_entry))
        if model[entry]:
          # todo: for non-boolen values, these are simplistic
          # placeholders. use defaults from kconfig instead. these
          # have their own dependencies but are not part of
          # constraints themselves.
          if types[str_entry] == "bool" or types[str_entry] == "tristate":
            fp.write("%s=y\n" % (str_entry))
          elif types[str_entry] == "string":
            fp.write("%s=\n" % (str_entry))
          elif types[str_entry] == "number":
            fp.write("%s=0\n" % (str_entry))
          elif types[str_entry] == "hex":
            fp.write("%s=0x0\n" % (str_entry))
          else:
            assert(False)
        else:
          fp.write("# %s is not set\n" % (str_entry))
      # else:
      #   sys.stderr.write("omitting non-config var %s\n" % (str_entry))
  else:
    warning("model is None.  Not printing.")

def optimize_model(optimize, constraints):
  solver = z3.Solver()
  solver.set(unsat_core=True)
  for constraint in constraints:
    solver.add(constraint)

  # try to match the given .config file as much as possible.
  # there are two approaches to try: (1) add the .config has
  # constraints, get the unsat core and try to remove assumptions
  # until we get something sat, (2) add the .config has soft
  # assertions.

  assumptions = get_config_file_constraints(optimize)

  # (1) unsat core approach. keep removing assumptions until the formula is satisfiable
  res = solver.check(assumptions)
  if res == z3.sat:
    info("Already satisfiable.  No optimization needed.")
    return solver.model()
  else:
    info("Optimizing via unsat core approach.")
    info("%d assumptions left to try removing." % (len(assumptions)), ending="\r")
    while res == z3.unsat:
      core = solver.unsat_core()
      # remove all assumptions that in the core.  todo, try randomizing this or removing only some assumptions each iteration.
      assumptions = [ assumption for assumption in assumptions if assumption not in core ]
      info(len(assumptions), ending="\r")
      res = solver.check(assumptions)
      core = solver.unsat_core()
      res = solver.check(assumptions)
    info("\nFound satisfying config.")
    return solver.model()
  
  # (2) soft assertion approach. (todo)

on_pattern = regex.compile("^(CONFIG_[A-Za-z0-9_]+)=[ym]")
off_pattern = regex.compile("^# (CONFIG_[A-Za-z0-9_]+) is not set")
def get_config_file_constraints(config_file):
  # todo: don't allow invisible defaults to be turned off (get them from kclause), reduces size of constraints

  constraints = []
  # add the .config as constraints
  with open(config_file, 'r') as optimize_fp:
    lines = optimize_fp.readlines()
    for line in lines:
      line = line.strip()
      off = off_pattern.match(line)
      if off:
        constraint = z3.Not(z3.Bool(off.group(1)))
        constraints.append(constraint)
      else:
        on = on_pattern.match(line)
        if on:
          constraint = z3.Bool(on.group(1))
          constraints.append(constraint)

    return constraints
  
ad_hoc_on_pattern = regex.compile("^(CONFIG_[A-Za-z0-9_]+)$")
ad_hoc_off_pattern = regex.compile("^!(CONFIG_[A-Za-z0-9_]+)$")
def get_ad_hoc_constraints(config_file):
  constraints = []
  with open(config_file, 'r') as fp:
    lines = fp.readlines()
    for line in lines:
      line = line.strip()
      off = ad_hoc_off_pattern.match(line)
      if off:
        constraint = z3.Not(z3.Bool(off.group(1)))
        constraints.append(constraint)
      else:
        on = ad_hoc_on_pattern.match(line)
        if on:
          constraint = z3.Bool(on.group(1))
          constraints.append(constraint)

    return constraints

# names of architectures corresponding to make and make.cross's ARCH variable
architectures = ["i386", "x86_64", "alpha", "arc", "arm", "arm64", "c6x", "csky", "h8300", "hexagon", "ia64", "m68k", "microblaze", "mips", "nds32", "nios2", "openrisc", "parisc", "powerpc", "riscv", "s390", "sh", "sh64", "sparc", "sparc64", "um", "um32", "unicore32",  "xtensa"]

# architecture-specific configs, enabled/disabled based on the architecture selected
architecture_configs = set([ "CONFIG_ALPHA", "CONFIG_ARC", "CONFIG_ARM", "CONFIG_ARM64", "CONFIG_C6X", "CONFIG_CSKY", "CONFIG_H8300", "CONFIG_HEXAGON", "CONFIG_IA64", "CONFIG_M68K", "CONFIG_MICROBLAZE", "CONFIG_MIPS", "CONFIG_NDS32", "CONFIG_NIOS2", "CONFIG_OPENRISC", "CONFIG_PARISC", "CONFIG_PPC64", "CONFIG_PPC32", "CONFIG_PPC", "CONFIG_RISCV", "CONFIG_S390", "CONFIG_SUPERH64", "CONFIG_SUPERH32", "CONFIG_SUPERH", "CONFIG_SPARC64", "CONFIG_SPARC32", "CONFIG_SPARC", "CONFIG_UML", "CONFIG_UNICORE32", "CONFIG_X86_64", "CONFIG_X86_32", "CONFIG_X86", "CONFIG_XTENSA" ])

# dependency on CONFIG_BROKEN will prevent a build, so we check for it
config_broken = z3.Not(z3.Bool("CONFIG_BROKEN"))

def get_archs_from_subdir(kbuild_path):
  """Get the architectures associated with the given arch/ subdirectory."""
  assert(kbuild_path.startswith("arch/"))
  elems = kbuild_path.split("/")
  if (len(elems) < 3):
    warning("need at least three elements, i.e., arch/NAME/unit.o to get arch name.")
    return []
  else:
    subdir = elems[1]
    # todo: handle um archs
    if subdir == "um" or elems[2] == "um":
      archs = [ "um", "um32" ]
    elif subdir == "x86":
      archs = [ "x86_64", "i386" ]
    elif subdir == "sh":
      archs = [ "sh", "sh64" ]
    elif subdir == "sparc":
      archs = [ "sparc", "sparc64" ]
    else:
      # arch matches subdir name
      archs = [ subdir ]
    return archs

def get_arch_kclause_subdir(formulas, arch):
  if arch == "um":
    subdir = "x86_64"
  elif arch == "um32":
    subdir = "i386"
  else:
    subdir = arch
  return os.path.join(os.path.join(os.path.join(formulas, "kclause"), subdir))
  
def get_arch_kclause_file(formulas, arch):
  return os.path.join(get_arch_kclause_subdir(formulas, arch), "kclause")

def get_arch_kconfig_extract_file(formulas, arch):
  return os.path.join(get_arch_kclause_subdir(formulas, arch), "kconfig_extract")

def get_arch_specific_constraints(arch, architecture_configs):
  if arch == "x86_64":
    constraints = [ z3.Bool("CONFIG_X86"), z3.Bool("CONFIG_X86_64"), z3.Not(z3.Bool("CONFIG_X86_32")), z3.Bool("BITS=64"), z3.Not(z3.Bool("BITS=32")) ]
    disabled = architecture_configs.difference(set(["CONFIG_X86", "CONFIG_X86_64", "CONFIG_X86_32"]))
  elif arch == "i386":
    constraints = [ z3.Bool("CONFIG_X86"), z3.Bool("CONFIG_X86_32"), z3.Not(z3.Bool("CONFIG_X86_64")), z3.Bool("BITS=32"), z3.Not(z3.Bool("BITS=64")) ]
    disabled = architecture_configs.difference(set(["CONFIG_X86", "CONFIG_X86_64", "CONFIG_X86_32"]))
  elif arch == "powerpc":
    constraints = [ z3.Bool("CONFIG_PPC") ]
    disabled = architecture_configs.difference(set(["CONFIG_PPC", "CONFIG_PPC32", "CONFIG_PPC64"]))
  elif arch == "sh":
    constraints = [ z3.Bool("CONFIG_SUPERH"), z3.Bool("CONFIG_SUPERH32"), z3.Not(z3.Bool("CONFIG_SUPERH64")), z3.Bool("BITS=32"), z3.Not(z3.Bool("BITS=64")) ]
    disabled = architecture_configs.difference(set(["CONFIG_SUPERH", "CONFIG_SUPERH32", "CONFIG_SUPERH64"]))
  elif arch == "sh64":
    constraints = [ z3.Bool("CONFIG_SUPERH"), z3.Bool("CONFIG_SUPERH64"), z3.Not(z3.Bool("CONFIG_SUPERH32")), z3.Bool("BITS=64"), z3.Not(z3.Bool("BITS=32")) ]
    disabled = architecture_configs.difference(set(["CONFIG_SUPERH", "CONFIG_SUPERH32", "CONFIG_SUPERH64"]))
  elif arch == "sparc":
    constraints = [ z3.Bool("CONFIG_SPARC"), z3.Bool("CONFIG_SPARC32"), z3.Not(z3.Bool("CONFIG_SPARC64")), z3.Bool("BITS=32"), z3.Not(z3.Bool("BITS=64")) ]
    disabled = architecture_configs.difference(set(["CONFIG_SPARC", "CONFIG_SPARC32", "CONFIG_SPARC64"]))
  elif arch == "sparc64":
    constraints = [ z3.Bool("CONFIG_SPARC"), z3.Bool("CONFIG_SPARC64"), z3.Not(z3.Bool("CONFIG_SPARC32")), z3.Bool("BITS=64"), z3.Not(z3.Bool("BITS=32")) ]
    disabled = architecture_configs.difference(set(["CONFIG_SPARC", "CONFIG_SPARC32", "CONFIG_SPARC64"]))
  elif arch == "um":
    constraints = [ z3.Bool("UML"), z3.Bool("CONFIG_X86"), z3.Bool("CONFIG_X86_64"), z3.Not(z3.Bool("CONFIG_X86_32")) ]
    disabled = architecture_configs.difference(set(["CONFIG_UML", "CONFIG_X86", "CONFIG_X86_64", "CONFIG_X86_32"]))
  elif arch == "um32":
    constraints = [ z3.Bool("UML"), z3.Bool("CONFIG_X86"), z3.Bool("CONFIG_X86_32"), z3.Not(z3.Bool("CONFIG_X86_64")) ]
    disabled = architecture_configs.difference(set(["CONFIG_UML", "CONFIG_X86", "CONFIG_X86_64", "CONFIG_X86_32"]))
  else:
    arch_var = "CONFIG_%s" % (arch.upper())
    constraints = [ z3.Bool(arch_var) ]
    disabled = architecture_configs.difference(set([ arch_var ]))
  disabled_z3 = [ z3.Not(z3.Bool(var)) for var in disabled ]
  return constraints + disabled_z3

if __name__ == '__main__':    
  argparser = argparse.ArgumentParser()
  argparser.add_argument('--formulas',
                         type=str,
                         default=".kmax/",
                         help="""Path to the formulas which contain one kmax file for all compilation units and one directory for each architecture containing kclause files.  Defaults to \".kmax/\"""")
  argparser.add_argument('--kmax-formulas',
                         type=str,
                         default=None,
                         help="""The file containing the Kbuild constraints as a pickled dictionary from compilation unit to formula.  Defaults to \"kmax\" in the --formulas directory.""")
  argparser.add_argument('--kclause-formulas',
                         type=str,
                         default=None,
                         help="""The file containing the a pickled tuple with a mapping from configuration option to its formulas and a list of additional constraints.  This overrides --arch.""")
  argparser.add_argument('--constraints-file',
                         type=str,
                         help="""A text file containing ad-hoc constraints.  One configuration option name per line.  Prefix with ! to force it off; no prefix means force on.""")
  argparser.add_argument('-a',
                         '--arch',
                         action="append",
                         default=[],
                         help="""Specify each architecture to try.  These archs will be tried first in order if --all is also given.  Defaults to all.  Available architectures: %s""" % (", ".join(architectures)))
  argparser.add_argument('--all',
                         action="store_true",
                         help="""Check all architectures for a satisfying configuration.  This tries each architecture's formulas given in the --formulas folder.""")
  argparser.add_argument('-o',
                         '--output',
                         type=str,
                         default=".config",
                         help="""Name of the output .config file.  Defaults to .config.""")
  argparser.add_argument('--optimize',
                         type=str,
                         help="""An existing .config file to use to try to match as closely as possible while still containing the desired objective.""")
  argparser.add_argument('-u',
                         '--show-unsat-core',
                         action="store_true",
                         help="""Show the unsatisfiable core if the formula is unsatisfiable.""")
  argparser.add_argument('-D',
                         '--define',
                         action="append",
                         default=[],
                         help="""Manually set a configuration option to be enabled.""")
  argparser.add_argument('-U',
                         '--undefine',
                         action="append",
                         default=[],
                         help="""Manually set a configuration option to be disabled.""")
  argparser.add_argument('--allow-config-broken',
                         action="store_true",
                         help="""Allow CONFIG_BROKEN dependencies.""")
  argparser.add_argument('--view-kbuild',
                         action="store_true",
                         help="""Just show the Kbuild constraints for the given compilation unit.  All other arguments are ignored.""")
  argparser.add_argument("compilation_unit", nargs='?', help="The path of the compilation unit (.o file) to generate a .config for, relative to the top of the source tree.")
  args = argparser.parse_args()

  formulas = args.formulas
  kmax_file = args.kmax_formulas
  kclause_file = args.kclause_formulas
  archs = args.arch
  allarchs = args.all
  constraints_file = args.constraints_file
  output_file = args.output
  show_unsat_core = args.show_unsat_core
  optimize = args.optimize
  define = args.define
  undefine = args.undefine
  disable_config_broken = not args.allow_config_broken
  view_kbuild = args.view_kbuild
  compilation_unit = args.compilation_unit

  if compilation_unit is None and len(archs) == 0 and not allarchs:
    argparser.print_help()
    warning("No formulas found.  Download them from https://kmaxtools.opentheblackbox.net/formulas/ or see the README.md to generate them.\n")
    exit(0)

  if not os.path.exists(formulas):
    error("No formulas found.  Download them from https://kmaxtools.opentheblackbox.net/formulas/ or see the README.md to generate them.\n")
    exit(1)

  if not kmax_file:
    kmax_file = os.path.join(formulas, "kmax")
  info("Kmax formula file: %s" % (kmax_file))
    
  if compilation_unit is not None and not os.path.isfile(kmax_file):
    error("Cannot find kmax formulas file: %s" % (kmax_file))
    exit(1)

  if not compilation_unit.endswith(".o"):
    compilation_unit = os.path.splitext(compilation_unit)[0] + ".o"
    warning("Forcing file extension to be .o, since lookup is by compilation unit: %s" % (compilation_unit))

  if view_kbuild:
    if compilation_unit is not None:
      info("The Kbuild constraints for %s:" % (compilation_unit))
      kmax_formulas = unpickle_kmax_file(kmax_file)
      resolved_to_kbuild_map = get_resolved_to_kbuild_map(kmax_formulas)
      get_kmax_constraints(kmax_formulas, resolved_to_kbuild_map, compilation_unit, view=True)
      exit(0)
    else:
      error("Please provide a compilation unit when using --view-kbuild.")
      exit(1)

  kclause_to_try = {}
  if kclause_file:
    if not os.path.isfile(kclause_file):
      error("Cannot find kclause formulas file: %s" % (kclause_file))
      exit(1)
    if (len(archs) > 0 or allarchs):
      warning("--kclause-formulas overrides --arch and --all.")
    kclause_to_try = {None : kclause_file}
  else:
    if len(archs) == 0:
      # try popular ones first
      archs = [ "x86_64", "i386", "arm", "arm64", "sparc64", "sparc", "powerpc", "mips" ]
      allarchs = True
    if allarchs:
      # add those not already requested by the user
      archs = archs + [ arch for arch in architectures if arch not in archs ]
    info("Trying the following architectures: %s" % (" ".join(archs)))
    for arch in archs:
      arch_kclause = get_arch_kclause_file(formulas, arch)
      if not os.path.isfile(arch_kclause):
        info("Skipping %s, because no kclause found at %s." % (arch, arch_kclause))
      else:
        kclause_to_try[arch] = arch_kclause
        
  if len(kclause_to_try.keys()) == 0:
    error("No kclause files found.  Please check --formulas directory or use --kclause-formula explicitly.")
    exit(1)
  elif not compilation_unit:
    if len(kclause_to_try.keys()) == 1:
      info("No compilation unit given.  Generating configuration only based on kclause constraints.")
    elif len(kclause_to_try.keys()) > 1:
      error("Trying multiple architectures without a target compilation unit is not provided.  Give one architecture or --kclause-formula to generate a config file without providing a compilation unit.")
      exit(1)
    else:
      assert(False)

  # if os.path.exists(output_file):
  #   def randstring(n):
  #     return ''.join(random.choice('ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789') for i in range(n))
  #   tries = 0
  #   maxtries = 5
  #   backup_file = "%s.saved_%s" % (output_file, randstring(5))
  #   while os.path.exists(backup_file) and tries < maxtries:
  #     backup_file = "%s.saved_%s" % (output_file, randstring(5))
  #     tries += 1
  #   if tries == maxtries:
  #     error("Output file \"%s\" already exists and cannot find a suitable backup file name.  Please delete the file manually or specify another output file." % (output_file))
  #     exit(1)
  #   info("Output file \"%s\" already exists.  Moving to \"%s\"." % (output_file, backup_file))
  #   os.rename(output_file, backup_file)
  info("Using output file \"%s\"." % (output_file))

  # add kmax constraints
  kmax_constraints = None
  if compilation_unit is not None:
    kmax_formulas = unpickle_kmax_file(kmax_file)
    resolved_to_kbuild_map = get_resolved_to_kbuild_map(kmax_formulas)
    kmax_constraints = get_kmax_constraints(kmax_formulas, resolved_to_kbuild_map, compilation_unit)
    if kmax_constraints is None:
      error("%s not found in %s.  Please check that the compilation unit is in the kmax file." % (compilation_unit, kmax_file))
      exit(1)
    # check for compilation-unit in arch/ subfolder
    kbuild_path = resolved_to_kbuild_map[compilation_unit]
    if kbuild_path.startswith("arch/"):
      # narrow the set of possible architectures
      unit_arch = get_archs_from_subdir(kbuild_path)
      archs = [ arch for arch in archs if arch in unit_arch ]

  archlist = [ arch for arch in archs if arch in kclause_to_try.keys() ]
  if None in kclause_to_try.keys():
    archlist = [None] + archlist
  assert(len(archlist) > 0)
  seen_unsat = False
  for arch in archlist:
    kclause_file = kclause_to_try[arch]
    if arch is not None:
      info("Trying \"%s\"" % (arch))
    info("Kclause formulas file: %s" % (kclause_file))
    if not os.path.exists(kclause_file):
      error("Cannot find kclause formulas file: %s" % (kclause_file))
    else:
      constraints = []

      if kmax_constraints:
        constraints.extend(kmax_constraints)

      if constraints_file:
        constraints.extend(get_ad_hoc_constraints(constraints_file))

      # add kclause constraints
      constraints.extend(get_kclause_constraints(kclause_file))

      # add user-specified constraints
      for user_define in define:
        constraints.append(z3.Bool(user_define))
      for user_undefine in undefine:
        constraints.append(z3.Not(z3.Bool(user_undefine)))

      if arch is not None:
        constraints.extend(get_arch_specific_constraints(arch, architecture_configs))

      if disable_config_broken: constraints.append(config_broken)

      solver = z3.Solver()
      solver.set(unsat_core=True)

      if (solver.check(constraints) == z3.unsat):
        if disable_config_broken and config_broken in solver.unsat_core():
          error("This compilation unit seems to depend on CONFIG_BROKEN, so it may not be buildable.  Stopping the search.  Run again with --allow-config-broken to search anyway.")
          exit(2)
        else:
          info("The constraints are unsatisfiable.  This either means no configuration is possible or kmax formulas are overconstrained.")
        if show_unsat_core:
          info("The following constraint(s) prevented satisfiability:\n%s" % (str(solver.unsat_core())))
        else:
          if not seen_unsat:
            info("Run with --show-unsat-core to see what constraints prevented satisfiability.")
            seen_unsat = True
      else:
        info("The constraints are satisfiable.")
        model = solver.model()
        if optimize:
          model = optimize_model(optimize, constraints)
        if model is not None:
          info("Writing the configuration to %s" % (output_file))
          if arch is not None:
            kconfig_extract = get_kconfig_extract(formulas, arch)
          else:
            kconfig_extract = None
          print_model_as_config(model, open(output_file, 'w'), kconfig_extract)
          if arch is not None:
            info("Generated configuration for %s" % (arch))
            info("Build with \"make.cross ARCH=%s olddefconfig; make.cross ARCH=%s clean %s\"." % (arch, arch, compilation_unit))
            print(arch)
          exit(0)
  error("No satisfying configuration found.")
  exit(1)
