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 conf import sf
   9 from exceptions import NoSolution
  10
  11 def generate():
  12         """Collect boolean equations from files: rules, solved and required
  13         And get solution with minisat
  14
  15         Relevant configurations
  16            rules_file
  17            solver_file
  18            required_file
  19            solution_file
  20         """
  21         # Check if rules_file exist. If it was generated.
  22         if not os.path.isfile(sf(conf.rules_file)):
  23                 raise Exception("Rules file missing. Run parse_kconfig and check ecistence of " + rules_file)
  24
  25         w_file = tempfile.NamedTemporaryFile(delete=False)
  26         # Join files to one single temporary file
  27         lines = set()
  28         with open(sf(conf.rules_file), 'r') as f:
  29                 for lnn in open(sf(conf.rules_file), 'r'):
  30                         ln = lnn.rstrip()
  31                         if ln not in lines:
  32                                 lines.add(ln)
  33         if os.path.isfile(sf(conf.solved_file)):
  34                 for lnn in open(sf(conf.solved_file), 'r'):
  35                         ln = lnn.rstrip()
  36                         if ln not in lines:
  37                                 lines.add(ln)
  38         if os.path.isfile(sf(conf.required_file)):
  39                 for lnn in open(sf(conf.required_file), 'r'):
  40                         ln = lnn.rstrip()
  41                         if ln not in lines:
  42                                 lines.add(ln)
  43
  44         with open(sf(conf.variable_count_file)) as f:
  45                 var_num = f.readline()
  46         lines_count = len(lines)
  47
  48         first_line = "p cnf " + 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         if conf.minisat_output:
  57                 subprocess.call([conf.picosat, w_file.name, '-o',
  58                         sf(conf.solution_file)] + conf.picosat_args)
  59         else:
  60                 subprocess.call([conf.picosat, w_file.name, '-o',
  61                         sf(conf.solution_file)] + conf.picosat_args,
  62                         stdout=subprocess.DEVNULL)
  63
  64         os.remove(w_file.name)
  65
  66 def apply():
  67         """Apply generated solution to kernel source.
  68         """
  69         # Check if solution_file exist
  70         if not os.path.isfile(sf(conf.solution_file)):
  71                 raise Exception("Solution file is missing. Run sat_solution and check existence of " + sf(conf.solution_file))
  72
  73         utils.build_symbol_map() # Ensure smap existence
  74
  75         # Read solution if satisfiable
  76         solut = []
  77         with open(sf(conf.solution_file), 'r') as f:
  78                 if not f.readline().rstrip() == 's SATISFIABLE':
  79                         raise NoSolution()
  80                 for line in f:
  81                         if line[0] == 'v':
  82                                 solut += line[2:].split()
  83         solut.remove('0') # Remove 0 at the end
  84
  85         # Write solution to output_confs file
  86         with open(sf(conf.output_confs), 'a') as f:
  87                 iteration = 0
  88                 with open(sf(conf.iteration_file)) as ff:
  89                         iteration = int(ff.readline())
  90                 f.write(str(iteration) + ':')
  91                 for txt in solut:
  92                         f.write(txt + ' ')
  93                 f.write('\n')
  94
  95         # Write negotation solution to solver_file
  96         with open(sf(conf.solved_file), 'a') as f:
  97                 for txt in solut:
  98                         if txt[0] == '-':
  99                                 ntx = ""
 100                                 txt = txt[1:]
 101                         else:
 102                                 ntx = "-"
 103                         f.write( ntx + txt + " ")
 104                 f.write("\n")
 105
 106         # Load variable count
 107         with open(sf(conf.symbol_map_file)) as f:
 108                 for var_num, l in enumerate(f):
 109                         pass
 110                 var_num += 1
 111         # Write solution to .config file in linux source folder
 112         with open(sf(conf.linux_dot_config), 'w') as f:
 113                 for txt in solut:
 114                         if txt[0] == '-':
 115                                 nt = True
 116                                 txt = txt[1:]
 117                         else:
 118                                 nt = False
 119                         if int(txt) >= var_num:
 120                                 break;
 121                         if 'NONAMEGEN' in utils.smap[txt]: # ignore generated names
 122                                 continue
 123
 124                         f.write('CONFIG_' + utils.smap[txt] + '=')
 125                         if not nt:
 126                                 f.write('y')
 127                         else:
 128                                 f.write('n')
 129                         f.write('\n')