scripts/solution.py

   1 import os
   2 import sys
   3 import tempfile
   4 import subprocess
   5
   6 import utils
   7 from conf import conf
   8 from exceptions import NoSolution
   9
  10 def generate():
  11         """Collect boolean equations from files: rules, solved and required
  12         And get solution with minisat
  13
  14         Relevant configurations
  15            rules_file
  16            solver_file
  17            required_file
  18            solution_file
  19         """
  20         # Check if rules_file exist. If it was generated.
  21         if not os.path.isfile(conf.rules_file):
  22                 raise Exception("Rules file missing. Run kconfig_parse and check ecistence of " + rules_file)
  23
  24         w_file = tempfile.NamedTemporaryFile(delete=False)
  25         # Join files to one single temporary file
  26         lines = set()
  27         with open(conf.rules_file, 'r') as f:
  28                 for lnn in open(conf.rules_file, 'r'):
  29                         ln = lnn.rstrip()
  30                         if ln not in lines:
  31                                 lines.add(ln)
  32         if os.path.isfile(conf.solved_file):
  33                 for lnn in open(conf.solved_file, 'r'):
  34                         ln = lnn.rstrip()
  35                         if ln not in lines:
  36                                 lines.add(ln)
  37         if os.path.isfile(conf.required_file):
  38                 for lnn in open(conf.required_file, 'r'):
  39                         ln = lnn.rstrip()
  40                         if ln not in lines:
  41                                 lines.add(ln)
  42
  43         with open(conf.symbol_map_file) as f:
  44                 for var_num, l in enumerate(f):
  45                         pass
  46                 var_num += 1
  47         lines_count = len(lines)
  48
  49         first_line = "p cnf " + str(var_num) + " " + str(lines_count)
  50         w_file.write(bytes(first_line + '\n', 'UTF-8'))
  51         for ln in lines:
  52                 w_file.write(bytes(ln + ' 0\n', 'UTF-8'))
  53
  54         w_file.close()
  55
  56         # Execute minisat
  57         if conf.minisat_output:
  58                 subprocess.call(['minisat', w_file.name, conf.solution_file])
  59         else:
  60                 subprocess.call(['minisat', w_file.name, conf.solution_file], stdout=subprocess.DEVNULL)
  61
  62         os.remove(w_file.name)
  63
  64 def apply():
  65         """Apply generated solution to kernel source.
  66         """
  67         # Check if solution_file exist
  68         if not os.path.isfile(conf.solution_file):
  69                 raise Exception("Solution file is missing. Run sat_solution and check existence of " + conf.solution_file)
  70
  71         utils.build_symbol_map() # Ensure smap existence
  72
  73         # Read solution if satisfiable
  74         with open(conf.solution_file, 'r') as f:
  75                 if not f.readline().rstrip() == 'SAT':
  76                         raise NoSolution()
  77                 solut = f.readline().split()
  78         solut.remove('0') # Remove 0 at the end
  79
  80         # Write negotation solution to solver_file
  81         with open(conf.solved_file, 'a') as f:
  82                 for txt in solut:
  83                         if txt[0] == '-':
  84                                 ntx = ""
  85                                 txt = txt[1:]
  86                         else:
  87                                 ntx = "-"
  88                         f.write( ntx + txt + " ")
  89                 f.write("\n")
  90
  91         # Write solution to .config file in linux source folder
  92         with open(conf.linux_sources + '/.config', 'w') as f:
  93                 with open(conf.dot_config_file, 'r') as fconf:
  94                         for line in fconf:
  95                                 f.write(line)
  96
  97                 for txt in solut:
  98                         if txt[0] == '-':
  99                                 nt = True
 100                                 txt = txt[1:]
 101                         else:
 102                                 nt = False
 103                         if 'NONAMEGEN' in utils.smap[txt]: # ignore generated names
 104                                 continue
 105
 106                         f.write('CONFIG_' + utils.smap[txt] + '=')
 107                         if not nt:
 108                                 f.write('y')
 109                         else:
 110                                 f.write('n')
 111                         f.write('\n')