import os import sys import tempfile import subprocess import time import utils from conf import conf from conf import sf import exceptions def generate(): """Collect boolean equations from files: rules, solved and required And get solution with picosat """ # Check if rules_file exist. If it was generated. if not os.path.isfile(sf(conf.rules_file)): raise exceptions.MissingFile(conf.rules_file,"Run parse_kconfig.") if os.path.isfile(sf(conf.solution_file)) and conf.gen_all_solution_oninit: raise exceptions.SolutionGenerated() w_file = tempfile.NamedTemporaryFile(delete=False) # Join files to one single temporary file lines = set() with open(sf(conf.rules_file), 'r') as f: for lnn in open(sf(conf.rules_file), 'r'): ln = lnn.rstrip() if ln not in lines: lines.add(ln) if os.path.isfile(sf(conf.solved_file)): for lnn in open(sf(conf.solved_file), 'r'): ln = lnn.rstrip() if ln not in lines: lines.add(ln) if os.path.isfile(sf(conf.required_file)): for lnn in open(sf(conf.required_file), 'r'): ln = lnn.rstrip() if ln not in lines: lines.add(ln) with open(sf(conf.variable_count_file)) as f: var_num = f.readline() lines_count = len(lines) first_line = "p cnf " + var_num + " " + str(lines_count) w_file.write(bytes(first_line + '\n', 'UTF-8')) for ln in lines: w_file.write(bytes(ln + ' 0\n', 'UTF-8')) w_file.close() # Execute picosat try: os.mkdir(sf(conf.log_folder)) except OSError: pass picosat_cmd = [sf(conf.picosat), w_file.name] if (conf.gen_all_solution_oninit): picosat_cmd += ['--all'] satprc = subprocess.Popen(picosat_cmd, stdout = subprocess.PIPE) with open(os.path.join(sf(conf.log_folder), "picosat.log"), 'a') as f: f.write("::" + time.strftime("%y-%m-%d-%H-%M-%S") + "::\n") solut = [] for linen in satprc.stdout: line = linen.decode(sys.getdefaultencoding()) f.write(line) if conf.picosat_output: print(line, end="") if line[0] == 's': if line.rstrip() == 's SATISFIABLE': try: solut.remove(0) with open(sf(conf.config_map_file), 'a') as fm: fm.write(str(utils.hash_config(solut)) + ':') for sl in solut: fm.write(str(sl) + ' ') fm.write('\n') with open(sf(conf.solved_file), 'a') as fs: for sl in solut: fs.write(str(-1 * sl) + ' ') fs.write('\n') except ValueError: pass solut = [] else: os.remove(w_file.name) raise exceptions.NoSolution() elif line[0] == 'v': for sl in line[2:].split(): solut.append(int(sl)) os.remove(w_file.name) def apply(): """Apply generated solution to kernel source. """ utils.build_symbol_map() # Ensure smap existence solved = set() solution = [] # Load set of solved solutions if os.path.isfile(sf(config_solved_file)): with open(sf(conf.config_solved_file)) as f: for ln in f: solved.add(ln.strip()) # Load one solution if it is not in solved with open(sf(conf.config_map_file)) as f: while True: w = f.readline().split(sep=':') if not w[0] in solved: solution = utils.config_strtoint(w[1]) break; if not solution: raise exceptions.NoApplicableSolution() # Load variable count with open(sf(conf.symbol_map_file)) as f: for var_num, l in enumerate(f): pass var_num += 1 # Write solution to .config file in linux source folder with open(sf(conf.linux_dot_config), 'w') as f: for s in solution: if s < 0: nt = True s *= -1 else: nt = False if s >= var_num: break; if 'NONAMEGEN' in utils.smap[s]: # ignore generated names continue f.write('CONFIG_' + utils.smap[s] + '=') if not nt: f.write('y') else: f.write('n') f.write('\n')