scripts/configurations.py

   1 import os
   2 import sys
   3 import tempfile
   4 import shutil
   5 import subprocess
   6 import time
   7 import hashlib
   8 import struct
   9
  10 import utils
  11 from conf import conf
  12 from conf import sf
  13 import exceptions
  14 import database
  15
  16 def __buildtempcnf__(variable_count, files, strlines):
  17         """ Builds temporally file for cnf formulas
  18           variable_count - number of variables in formulas
  19           files          - list of files with formulas
  20           strlines       - list of string lines with formulas"""
  21         lines = set()
  22         # Copy strlines
  23         for ln in strlines:
  24                 lines.add(ln)
  25         # Files
  26         for file in files:
  27                 with open(file, 'r') as f:
  28                         for ln in f:
  29                                 lines.add(ln.rstrip())
  30
  31         first_line = "p cnf " + str(variable_count) + " " + str(len(lines))
  32
  33         wfile = tempfile.NamedTemporaryFile(delete=False)
  34         wfile.write(bytes(first_line + '\n', 'UTF-8'))
  35         for ln in lines:
  36                 wfile.write(bytes(ln + ' 0\n', 'UTF-8'))
  37         wfile.close()
  38         return wfile.name
  39
  40 def __exec_sat__(file, args, conf_num):
  41         """Executes SAT solver and returns configuration."""
  42         picosat_cmd = [sf(conf.picosat), file]
  43         picosat_cmd += conf.picosat_args
  44         picosat_cmd += args
  45         stdout = utils.callsubprocess('picosat', picosat_cmd, conf.picosat_output,
  46                         True, allow_all_exit_codes = True)
  47
  48         rtn = []
  49         solut = []
  50         for line in stdout:
  51                 if line[0] == 's':
  52                         try:
  53                                 solut.remove(0)
  54                                 rtn.append(solut)
  55                         except ValueError:
  56                                 pass
  57                         solut = []
  58                         if not line.rstrip() == 's SATISFIABLE':
  59                                 raise exceptions.NoSolution()
  60                 elif line[0] == 'v':
  61                         for sl in line[2:].split():
  62                                 solut.append(int(sl))
  63         try:
  64                 solut.remove(0)
  65                 rtn.append(solut)
  66         except ValueError:
  67                 pass
  68         # Ensure smap existence
  69         utils.build_symbol_map()
  70         # Translate to dict
  71         con = list()
  72         for rt in rtn:
  73                 cond = dict()
  74                 for r in rt:
  75                         if r < 0:
  76                                 val = False
  77                                 r *= -1
  78                         else:
  79                                 val = True
  80                         if r > int(conf_num):
  81                                 break;
  82                         if 'NONAMEGEN' in utils.smap[r]: # ignore generated names
  83                                 continue
  84                         cond[utils.smap[r]] = val
  85                 con.append(cond)
  86         return con
  87
  88 def __txt_config__(con):
  89         config = []
  90         for key, val in con.items():
  91                 txt = 'CONFIG_' + key + '='
  92                 if val:
  93                         txt += 'y'
  94                 else:
  95                         txt += 'n'
  96                 config.append(txt)
  97         return config
  98
  99 def __write_temp_config_file__(con):
 100         wfile = tempfile.NamedTemporaryFile(delete=False)
 101         txt = __txt_config__(con)
 102         for ln in txt:
 103                 wfile.write(bytes(ln + '\n', sys.getdefaultencoding()))
 104         wfile.close()
 105         return wfile.name
 106
 107 def __load_config_text__(txt):
 108         rtn = dict()
 109         for ln in txt:
 110                 if not ln:
 111                         continue
 112                 if ln[0] == '#' or not '=' in ln:
 113                         continue
 114                 indx = ln.index('=')
 115                 if (ln[indx + 1] == 'y'):
 116                         rtn[ln[7:indx]] = True
 117                 else:
 118                         rtn[ln[7:indx]] = False
 119         return rtn
 120
 121
 122 def __load_config_file__(file):
 123         f = open(file, 'r')
 124         rtn = __load_config_text__(f)
 125         f.close()
 126         return rtn
 127
 128 def __calchash__(con):
 129         dt = database.database()
 130         csort = dt.get_configsort()
 131
 132         cstr = ""
 133         for c in csort:
 134                 try:
 135                         if con[c]:
 136                                 cstr += c
 137                 except KeyError:
 138                         pass
 139
 140         # Add missing
 141         for key, val in con.items():
 142                 try:
 143                         csort.index(key)
 144                 except ValueError:
 145                         indx = len(csort)
 146                         csort.append(key)
 147                         dt.add_configsort(key)
 148                         if val:
 149                                 cstr += key
 150
 151         hsh = hashlib.md5(bytes(cstr, 'UTF-8'))
 152         return hsh.hexdigest()
 153
 154
 155 def __calchash_file__(file):
 156         """Calculates hash from configuration file"""
 157         con = __load_config_file__(file)
 158         return __calchash__(con)
 159
 160 def __register_conf__(con, conf_num, generator):
 161         dtb = database.database()
 162         # Solution to configuration
 163         txtconfig = __txt_config__(con)
 164         hsh = __calchash__(con)
 165         cconf = dtb.get_configration(hsh)
 166         for cc in cconf:
 167                 print('hash: ' + hsh)
 168                 if compare_text(cc.config, txtconfig):
 169                         print("I: Generated existing configuration.")
 170                         return False
 171                 else:
 172                         print("W: Generated configuration with collision hash.")
 173                         # TODO this might have to be tweaked
 174                         raise Exception()
 175         dtb.add_configuration(hsh, txtconfig, generator)
 176         return True
 177
 178 def __generate_single__(var_num, conf_num):
 179         measure_list = set()
 180         if not os.path.isfile(sf(conf.single_generated_file)):
 181                 with open(sf(conf.measure_file), 'r') as fi:
 182                         for ln in fi:
 183                                 measure_list.add(int(ln))
 184         else:
 185                 with open(sf(conf.single_generated_file), 'r') as f:
 186                         for ln in f:
 187                                 measure_list.add(int(ln))
 188         if not measure_list:
 189                 return False
 190         tfile = __buildtempcnf__(var_num, (sf(conf.rules_file),
 191                 sf(conf.fixed_file)), [str(measure_list.pop())])
 192         with open(sf(conf.single_generated_file), 'w') as fo:
 193                 for ln in measure_list:
 194                         fo.write(str(ln) + '\n')
 195         try:
 196                 confs = __exec_sat__(tfile, ['-i', '0'], conf_num)
 197                 for con in confs:
 198                         if not __register_conf__(con, conf_num, 'single-sat'):
 199                                 return __generate_single__(var_num, conf_num)
 200         except exceptions.NoSolution:
 201                 return __generate_single__(var_num, conf_num)
 202         finally:
 203                 os.remove(tfile)
 204         return True
 205
 206 def __generate_random__(var_num, conf_num):
 207         tfile = __buildtempcnf__(var_num, (sf(conf.rules_file), sf(conf.fixed_file)), set())
 208         try:
 209                 while True:
 210                         seed = struct.unpack('<L', os.urandom(4))[0]
 211                         confs = __exec_sat__(tfile, ['-i', '3', '-s', str(seed)], conf_num)
 212                         for con in confs:
 213                                 if __register_conf__(con, conf_num, 'random-sat'):
 214                                         return True
 215         finally:
 216                 os.remove(tfile)
 217
 218 def generate():
 219         """Collect boolean equations from files rules and required
 220         And get solution with picosat
 221         """
 222         # Check if rules_file exist. If it was generated.
 223         if not os.path.isfile(sf(conf.rules_file)):
 224                 raise exceptions.MissingFile(conf.rules_file,"Run parse_kconfig.")
 225         if not os.path.isfile(sf(conf.fixed_file)):
 226                 raise exceptions.MissingFile(conf.required_file,"Run allconfig and initialization process.")
 227
 228         # Load variable count
 229         with open(sf(conf.variable_count_file)) as f:
 230                 var_num = f.readline().rstrip()
 231                 conf_num = f.readline().rstrip()
 232
 233         if __generate_single__(var_num, conf_num):
 234                 return
 235         elif __generate_random__(var_num, conf_num):
 236                 return
 237
 238         raise exceptions.NoNewConfiguration()
 239
 240 def compare(conf1, conf2):
 241         """Compared two configuration"""
 242         # This is not exactly best comparison method
 243         for key, val in conf1.items():
 244                 try:
 245                         if conf2[key] != val:
 246                                 return False
 247                 except ValueError:
 248                         return False
 249         for key, val in conf2.items():
 250                 try:
 251                         if conf1[key] != val:
 252                                 return False
 253                 except ValueError:
 254                         return False
 255         return True
 256
 257 def compare_text(text1, text2):
 258         conf1 = __load_config_text__(text1)
 259         conf2 = __load_config_text__(text2)
 260         return compare(conf1, conf2)
 261
 262 def compare_file(file1, file2):
 263         conf1 = __load_config_file__(file1)
 264         conf2 = __load_config_file__(file2)
 265         return compare(conf1, conf2)