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