diff options
| -rw-r--r-- | conf.py | 9 | ||||
| -rw-r--r-- | scripts/configurations.py | 294 | ||||
| -rwxr-xr-x | scripts/initialize.py | 5 |
3 files changed, 182 insertions, 126 deletions
@@ -28,8 +28,8 @@ nbscript = 'scripts/nbscript' boot_command = ['scripts/novaboot/novaboot', nbscript] + novaboot_args # picosat_args -# Arguments passed to PicoSAT. -picosat_args = ['--all'] +# Additional arguments passed to PicoSAT. +picosat_args = [] # db_database # Database in PostgreSQL to be used for this tools @@ -91,12 +91,13 @@ phase_file = build_folder + 'phase' symbol_map_file = build_folder + 'symbol_map' # Also defined in parse_kconfig rules_file = build_folder + 'rules' # Also defined in parse_kconfig variable_count_file = build_folder + 'variable_count' # Also defined in parse_kconfig -config_map_file = build_folder + 'config_map' -config_solved_file = build_folder + 'config_solved' required_file = build_folder + 'required' dot_config_back_file = build_folder + 'dot_config_back' iteration_file = build_folder + 'iteration' +configurations_folder = 'configurations/' +hashconfigsort = configurations_folder + 'hashconfigsort' + output_folder = 'output/' result_folder = 'result/' log_folder = 'log/' diff --git a/scripts/configurations.py b/scripts/configurations.py index 722aaaf..1de764b 100644 --- a/scripts/configurations.py +++ b/scripts/configurations.py @@ -8,134 +8,194 @@ import utils from conf import conf from conf import sf import exceptions +import database -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)): - raise exceptions.SolutionGenerated() - - w_file = tempfile.NamedTemporaryFile(delete=False) - # Join files to one single temporary file +def __buildtempcnf__(variable_count, files, strlines): + """ Builds temporally file for cnf formulas + variable_count - number of variables in formulas + files - list of files with formulas + strlines - list of string lines with formulas""" 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.required_file)): - for lnn in open(sf(conf.required_file), 'r'): - ln = lnn.rstrip() - if ln not in lines: - lines.add(ln) + # Copy strlines + for ln in strlines: + lines.add(ln) + # Files + for file in files: + with open(file, 'r') as f: + for ln in f: + lines.add(ln.rstrip()) - with open(sf(conf.variable_count_file)) as f: - var_num = f.readline() - lines_count = len(lines) + first_line = "p cnf " + str(variable_count) + " " + str(len(lines)) - first_line = "p cnf " + var_num + " " + str(lines_count) - w_file.write(bytes(first_line + '\n', 'UTF-8')) + wfile = tempfile.NamedTemporaryFile(delete=False) + wfile.write(bytes(first_line + '\n', 'UTF-8')) for ln in lines: - w_file.write(bytes(ln + ' 0\n', 'UTF-8')) + wfile.write(bytes(ln + ' 0\n', 'UTF-8')) + wfile.close() + return wfile.name - w_file.close() +def __exec_sat__(file, args): + """Executes SAT solver and returns configuration.""" + picosat_cmd = [sf(conf.picosat), file] + picosat_cmd += conf.picosat_args + stdout = utils.callsubprocess('picosat', conf.picosat_cmd, conf.picosat_output, ".") + + rtn = [] + solut = [] + for line in stdout: + if line[0] == 's': + try: + solut.remove(0) + rtn.append(solut) + except ValueError: + pass + solut = [] + if not line.rstrip() == 's SATISFIABLE': + raise exceptions.NoSolution() + elif line[0] == 'v': + for sl in line[2:].split(): + solut.append(int(sl)) + return rtn + +def __write_temp_config_file__(conf): + # Ensure smap existence + utils.build_symbol_map() + # Load variable count + with open(sf(conf.variable_count_file)) as f: + f.readline() + var_num = int(f,readline()) + # Write temporally file + wfile = tempfile.NamedTemporaryFile(delete=False) + for s in conf: + 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 + wfile.write('CONFIG_' + utils.smap[s] + '=') + if not nt: + wfile.write('y') + else: + wfile.write('n') + wfile.write('\n') + wfile.close() + return wfile.name + +def __load_config_file__(file): + rtn = dict() + with open(file, 'r') as f: + for ln in f: + if ln[0] == '#' or not '=' in ln: + continue + indx = ln.index('=') + if (ln[indx + 1] == 'y'): + rtn[line[7:indx]] = True + else: + rtn[line[7:indx]] = True + return rtn - # Execute picosat +def __calchash__(file): + """Calculates hash from configuration file""" + # Build hashconfigsort + csort = [] try: - os.mkdir(sf(conf.log_folder)) - except OSError: + with open(conf.hashconfigsort, 'r') as f: + for ln in f: + csort.append(ln.rstrip()) + except FileNotFoundError: pass - picosat_cmd = [sf(conf.picosat), w_file.name] - picosat_cmd += conf.picosat_args + conf = __load_config_file__(file) + cstr = "" + for c in csort: + try: + if conf[c]: + cstr += '+' + else: + cstr += '-' + except ValueError: + cstr += '0' + + # Add missing + csortfile = open(conf.hashconfigsort, 'a'); + for key, val in conf: + try: + csort.index(key) + except ValueError: + indx = len(csort) + csort.append(key) + csortfile.write(key + '\n') + if val: + cstr += '+' + else: + cstr += '-' + close(csortfile) - 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': - 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') - except ValueError: - pass - solut = [] - if not line.rstrip() == 's SATISFIABLE': - 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 + hsh = hashlib.md5(bytes(cstr, 'UTF-8')) + return hsh.hexdigest() - solved = set() - solution = [] - # Load set of solved solutions - if os.path.isfile(sf(conf.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 - hash = '' - with open(sf(conf.config_map_file)) as f: - while True: - w = f.readline().split(sep=':') - if not w[0]: - break - if not w[0] in solved: - solution = utils.config_strtoint(w[1], True) - hash = w[0] - break - if not solution: - raise exceptions.NoApplicableSolution() - - # Write hash to config_solved - with open(sf(conf.config_solved_file), 'a') as f: - f.write(hash) - f.write('\n') +def __register_conf__(conf): + with open(sf(conf.variable_count_file)) as f: + var_num = int(f.readline()) + + dtb = database.database() + # Solution to configuration + wfile = __write_temp_config_file__(conf) + hsh = __calchash__(wfile.name) + filen = os.path.join(sf(conf.configuration_folder, hsh)) + hshf = hsh + if os.path.isfile(filen): + if compare(filen, wfile): + print("I: Generated existing configuration.") + continue + else: + print("W: Generated configuration with collision hash.") + # TODO this might have to be tweaked + raise Exception() + os.rename(wfile.name, filen) + dtb.add_configuration(hsh, hshf) - # 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') +def generate(): + """Collect boolean equations from files rules 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 not os.path.isfile(sf(conf.required_file)): + raise exceptions.MissingFile(conf.required_file,"Run allconfig.") + + tfile = __buildtempcnf__(var_num, (conf.rules_file, conf.required_file), ()) + try: + confs = __exec_sat__(tfile) + os.remove(tfile) + for conf in confs: + __register_conf__(conf) + except exceptions.NoSolution: + os.remove(tfile) + raise exceptions.NoSolution() + +def compare(file1, file2): + """Compared two configuration""" + conf1 = __load_config_file__(file1) + conf2 = __load_config_file__(file2) + + # This is not exactly best comparison method + for key, val in conf1: + try: + if conf2[key] != val: + return False + except ValueError: + return False + for key, val in conf2: + try: + if conf1[key] != val: + return False + except ValueError: + return False + return True diff --git a/scripts/initialize.py b/scripts/initialize.py index 146acbf..f48156d 100755 --- a/scripts/initialize.py +++ b/scripts/initialize.py @@ -10,16 +10,11 @@ from conf import conf from conf import sf import exceptions import loop -import configurations def all(): base() parse_kconfig() gen_requred() - try: - configurations.generate() - except exceptions.NoSolution: - pass # check if database is initialized database.database() |