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"""
27 with open(file, 'r') as f:
29 lines.add(ln.rstrip())
31 first_line = "p cnf " + str(variable_count) + " " + str(len(lines))
33 wfile = tempfile.NamedTemporaryFile(delete=False)
34 wfile.write(bytes(first_line + '\n', 'UTF-8'))
36 wfile.write(bytes(ln + ' 0\n', 'UTF-8'))
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
45 stdout = utils.callsubprocess('picosat', picosat_cmd, conf.picosat_output,
46 True, allow_all_exit_codes = True)
58 if not line.rstrip() == 's SATISFIABLE':
59 raise exceptions.NoSolution()
61 for sl in line[2:].split():
68 # Ensure smap existence
69 utils.build_symbol_map()
82 if 'NONAMEGEN' in utils.smap[r]: # ignore generated names
84 cond[utils.smap[r]] = val
88 def __txt_config__(con):
90 for key, val in con.items():
91 txt = 'CONFIG_' + key + '='
99 def __write_temp_config_file__(con):
100 wfile = tempfile.NamedTemporaryFile(delete=False)
101 txt = __txt_config__(con)
103 wfile.write(bytes(ln + '\n', sys.getdefaultencoding()))
107 def __load_config_text__(txt):
112 if ln[0] == '#' or not '=' in ln:
115 if (ln[indx + 1] == 'y'):
116 rtn[ln[7:indx]] = True
118 rtn[ln[7:indx]] = False
122 def __load_config_file__(file):
124 rtn = __load_config_text__(f)
128 def __calchash__(con):
129 dt = database.database()
130 csort = dt.get_configsort()
141 for key, val in con.items():
147 dt.add_configsort(key)
151 hsh = hashlib.md5(bytes(cstr, 'UTF-8'))
152 return hsh.hexdigest()
155 def __calchash_file__(file):
156 """Calculates hash from configuration file"""
157 con = __load_config_file__(file)
158 return __calchash__(con)
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)
167 print('hash: ' + hsh)
168 if compare_text(cc.config, txtconfig):
169 print("I: Generated existing configuration.")
172 print("W: Generated configuration with collision hash.")
173 # TODO this might have to be tweaked
175 dtb.add_configuration(hsh, txtconfig, generator)
178 def __generate_single__(var_num, conf_num):
179 utils.build_symbol_map()
181 if not os.path.isfile(sf(conf.single_generated_file)):
182 with open(sf(conf.measure_file), 'r') as fi:
184 measure_list.add(int(ln))
186 with open(sf(conf.single_generated_file), 'r') as f:
188 measure_list.add(int(ln))
191 measuring = measure_list.pop()
192 tfile = __buildtempcnf__(var_num, (sf(conf.rules_file),
193 sf(conf.fixed_file)), [str(measuring)])
194 with open(sf(conf.single_generated_file), 'w') as fo:
195 for ln in measure_list:
196 fo.write(str(ln) + '\n')
198 confs = __exec_sat__(tfile, ['-i', '0'], conf_num)
200 if not __register_conf__(con, conf_num, 'single-sat-'
201 + utils.smap[measuring]):
202 return __generate_single__(var_num, conf_num)
203 except exceptions.NoSolution:
204 return __generate_single__(var_num, conf_num)
209 def __generate_random__(var_num, conf_num):
210 tfile = __buildtempcnf__(var_num, (sf(conf.rules_file), sf(conf.fixed_file)), set())
213 seed = struct.unpack('<L', os.urandom(4))[0]
214 confs = __exec_sat__(tfile, ['-i', '3', '-s', str(seed)], conf_num)
216 if __register_conf__(con, conf_num, 'random-sat'):
222 """Collect boolean equations from files rules and required
223 And get solution with picosat
225 # Check if rules_file exist. If it was generated.
226 if not os.path.isfile(sf(conf.rules_file)):
227 raise exceptions.MissingFile(conf.rules_file,"Run parse_kconfig.")
228 if not os.path.isfile(sf(conf.fixed_file)):
229 raise exceptions.MissingFile(conf.required_file,"Run allconfig and initialization process.")
231 # Load variable count
232 with open(sf(conf.variable_count_file)) as f:
233 var_num = f.readline().rstrip()
234 conf_num = f.readline().rstrip()
236 if __generate_single__(var_num, conf_num):
238 elif __generate_random__(var_num, conf_num):
241 raise exceptions.NoNewConfiguration()
243 def compare(conf1, conf2):
244 """Compared two configuration"""
245 # This is not exactly best comparison method
246 for key, val in conf1.items():
248 if conf2[key] != val:
252 for key, val in conf2.items():
254 if conf1[key] != val:
260 def compare_text(text1, text2):
261 conf1 = __load_config_text__(text1)
262 conf2 = __load_config_text__(text2)
263 return compare(conf1, conf2)
265 def compare_file(file1, file2):
266 conf1 = __load_config_file__(file1)
267 conf2 = __load_config_file__(file2)
268 return compare(conf1, conf2)