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