scripts/configurations.py

   1 import os
   2 import sys
   3 import tempfile
   4 import subprocess
   5 import time
   6
   7 import utils
   8 from conf import conf
   9 from conf import sf
  10 import exceptions
  11 import database
  12
  13 def __buildtempcnf__(variable_count, files, strlines):
  14         """ Builds temporally file for cnf formulas
  15           variable_count - number of variables in formulas
  16           files          - list of files with formulas
  17           strlines       - list of string lines with formulas"""
  18         lines = set()
  19         # Copy strlines
  20         for ln in strlines:
  21                 lines.add(ln)
  22         # Files
  23         for file in files:
  24                 with open(file, 'r') as f:
  25                         for ln in f:
  26                                 lines.add(ln.rstrip())
  27
  28         first_line = "p cnf " + str(variable_count) + " " + str(len(lines))
  29
  30         wfile = tempfile.NamedTemporaryFile(delete=False)
  31         wfile.write(bytes(first_line + '\n', 'UTF-8'))
  32         for ln in lines:
  33                 wfile.write(bytes(ln + ' 0\n', 'UTF-8'))
  34         wfile.close()
  35         return wfile.name
  36
  37 def __exec_sat__(file, args):
  38         """Executes SAT solver and returns configuration."""
  39         picosat_cmd = [sf(conf.picosat), file]
  40         picosat_cmd += conf.picosat_args
  41         stdout = utils.callsubprocess('picosat', conf.picosat_cmd, conf.picosat_output, ".")
  42
  43         rtn = []
  44         solut = []
  45         for line in stdout:
  46                 if line[0] == 's':
  47                         try:
  48                                 solut.remove(0)
  49                                 rtn.append(solut)
  50                         except ValueError:
  51                                 pass
  52                         solut = []
  53                         if not line.rstrip() == 's SATISFIABLE':
  54                                 raise exceptions.NoSolution()
  55                 elif line[0] == 'v':
  56                         for sl in line[2:].split():
  57                                 solut.append(int(sl))
  58         return rtn
  59
  60 def __write_temp_config_file__(conf):
  61         # Ensure smap existence
  62         utils.build_symbol_map()
  63         # Load variable count
  64         with open(sf(conf.variable_count_file)) as f:
  65                 f.readline()
  66                 var_num = int(f,readline())
  67         # Write temporally file
  68         wfile = tempfile.NamedTemporaryFile(delete=False)
  69         for s in conf:
  70                 if s < 0:
  71                         nt = True
  72                         s *= -1
  73                 else:
  74                         nt = False
  75                 if s > var_num:
  76                         break;
  77                 if 'NONAMEGEN' in utils.smap[s]: # ignore generated names
  78                         continue
  79                 wfile.write('CONFIG_' + utils.smap[s] + '=')
  80                 if not nt:
  81                         wfile.write('y')
  82                 else:
  83                         wfile.write('n')
  84                 wfile.write('\n')
  85         wfile.close()
  86         return wfile.name
  87
  88 def __load_config_file__(file):
  89         rtn = dict()
  90         with open(file, 'r') as f:
  91                 for ln in f:
  92                         if ln[0] == '#' or not '=' in ln:
  93                                 continue
  94                         indx = ln.index('=')
  95                         if (ln[indx + 1] == 'y'):
  96                                 rtn[line[7:indx]] = True
  97                         else:
  98                                 rtn[line[7:indx]] = True
  99         return rtn
 100
 101 def __calchash__(file):
 102         """Calculates hash from configuration file"""
 103         # Build hashconfigsort
 104         csort = []
 105         try:
 106                 with open(conf.hashconfigsort, 'r') as f:
 107                         for ln in f:
 108                                 csort.append(ln.rstrip())
 109         except FileNotFoundError:
 110                 pass
 111
 112         conf = __load_config_file__(file)
 113         cstr = ""
 114         for c in csort:
 115                 try:
 116                         if conf[c]:
 117                                 cstr += '+'
 118                         else:
 119                                 cstr += '-'
 120                 except ValueError:
 121                         cstr += '0'
 122
 123         # Add missing
 124         csortfile = open(conf.hashconfigsort, 'a');
 125         for key, val in conf:
 126                 try:
 127                         csort.index(key)
 128                 except ValueError:
 129                         indx = len(csort)
 130                         csort.append(key)
 131                         csortfile.write(key + '\n')
 132                         if val:
 133                                 cstr += '+'
 134                         else:
 135                                 cstr += '-'
 136         close(csortfile)
 137
 138         hsh = hashlib.md5(bytes(cstr, 'UTF-8'))
 139         return hsh.hexdigest()
 140
 141 def __register_conf__(conf):
 142         with open(sf(conf.variable_count_file)) as f:
 143                 var_num = int(f.readline())
 144
 145         dtb = database.database()
 146                 # Solution to configuration
 147         wfile = __write_temp_config_file__(conf)
 148         hsh = __calchash__(wfile.name)
 149         filen = os.path.join(sf(conf.configuration_folder, hsh))
 150         hshf = hsh
 151         if os.path.isfile(filen):
 152                 if compare(filen, wfile):
 153                         print("I: Generated existing configuration.")
 154                         continue
 155                 else:
 156                         print("W: Generated configuration with collision hash.")
 157                         # TODO this might have to be tweaked
 158                         raise Exception()
 159         os.rename(wfile.name, filen)
 160         dtb.add_configuration(hsh, hshf)
 161
 162
 163 def generate():
 164         """Collect boolean equations from files rules and required
 165         And get solution with picosat
 166         """
 167         # Check if rules_file exist. If it was generated.
 168         if not os.path.isfile(sf(conf.rules_file)):
 169                 raise exceptions.MissingFile(conf.rules_file,"Run parse_kconfig.")
 170         if not os.path.isfile(sf(conf.required_file)):
 171                 raise exceptions.MissingFile(conf.required_file,"Run allconfig.")
 172
 173         tfile = __buildtempcnf__(var_num, (conf.rules_file, conf.required_file), ())
 174         try:
 175                 confs = __exec_sat__(tfile)
 176                 os.remove(tfile)
 177                 for conf in confs:
 178                         __register_conf__(conf)
 179         except exceptions.NoSolution:
 180                 os.remove(tfile)
 181                 raise exceptions.NoSolution()
 182
 183 def compare(file1, file2):
 184         """Compared two configuration"""
 185         conf1 = __load_config_file__(file1)
 186         conf2 = __load_config_file__(file2)
 187
 188         # This is not exactly best comparison method
 189         for key, val in conf1:
 190                 try:
 191                         if conf2[key] != val:
 192                                 return False
 193                 except ValueError:
 194                         return False
 195         for key, val in conf2:
 196                 try:
 197                         if conf1[key] != val:
 198                                 return False
 199                 except ValueError:
 200                         return False
 201         return True