From: N. Engelhardt Date: Mon, 23 Mar 2020 17:09:27 +0000 (+0100) Subject: Use .format() instead of % X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=30d7c32ec60532d06f332cc9b8e1d78c3090f6aa;p=SymbiYosys.git Use .format() instead of % Signed-off-by: N. Engelhardt --- diff --git a/sbysrc/sby.py b/sbysrc/sby.py index cdcaff4..f03dd0f 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -119,7 +119,7 @@ early_logmsgs = list() def early_log(workdir, msg): tm = localtime() - early_logmsgs.append("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg)) + early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg)) print(early_logmsgs[-1]) @@ -194,7 +194,7 @@ def read_sbyconfig(sbydata, taskname): if len(task_tags_all) and not found_task_tag: tokens = line.split() if len(tokens) > 0 and tokens[0][0] == line[0] and tokens[0].endswith(":"): - print("ERROR: Invalid task specifier \"%s\"." % tokens[0], file=sys.stderr) + print("ERROR: Invalid task specifier \"{}\".".format(tokens[0]), file=sys.stderr) sys.exit(1) if task_skip_line or task_skip_block: @@ -261,7 +261,7 @@ if dump_files: continue filename = line.split()[-1] file_set.add(process_filename(filename)) - + if len(tasknames): for taskname in tasknames: find_files(taskname) @@ -297,20 +297,20 @@ def run_job(taskname): if my_workdir is not None: if opt_backup: backup_idx = 0 - while os.path.exists("%s.bak%03d" % (my_workdir, backup_idx)): + while os.path.exists("{}.bak{:03d}".format(my_workdir, backup_idx)): backup_idx += 1 - early_log(my_workdir, "Moving directory '%s' to '%s'." % (my_workdir, "%s.bak%03d" % (my_workdir, backup_idx))) - shutil.move(my_workdir, "%s.bak%03d" % (my_workdir, backup_idx)) + early_log(my_workdir, "Moving directory '{}' to '{}'.".format(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx))) + shutil.move(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx)) if opt_force and not reusedir: - early_log(my_workdir, "Removing directory '%s'." % (my_workdir)) + early_log(my_workdir, "Removing directory '{}'.".format(my_workdir)) if sbyfile: shutil.rmtree(my_workdir, ignore_errors=True) if reusedir: pass elif os.path.isdir(my_workdir): - print("ERROR: Directory '%s' already exists." % (my_workdir)) + print("ERROR: Directory '{}' already exists.".format(my_workdir)) sys.exit(1) else: os.makedirs(my_workdir) @@ -348,37 +348,37 @@ def run_job(taskname): pass if my_opt_tmpdir: - job.log("Removing directory '%s'." % (my_workdir)) + job.log("Removing directory '{}'.".format(my_workdir)) shutil.rmtree(my_workdir, ignore_errors=True) if setupmode: - job.log("SETUP COMPLETE (rc=%d)" % (job.retcode)) + job.log("SETUP COMPLETE (rc={})".format(job.retcode)) else: - job.log("DONE (%s, rc=%d)" % (job.status, job.retcode)) + job.log("DONE ({}, rc={})".format(job.status, job.retcode)) job.logfile.close() if not my_opt_tmpdir and not setupmode: - with open("%s/%s.xml" % (job.workdir, junit_filename), "w") as f: + with open("{}/{}.xml".format(job.workdir, junit_filename), "w") as f: junit_errors = 1 if job.retcode == 16 else 0 junit_failures = 1 if job.retcode != 0 and junit_errors == 0 else 0 print('', file=f) - print('' % (junit_errors, junit_failures, job.total_time), file=f) - print('' % (junit_errors, junit_failures, junit_ts_name, job.total_time), file=f) + print(''.format(junit_errors, junit_failures, job.total_time), file=f) + print(''.format(junit_errors, junit_failures, junit_ts_name, job.total_time), file=f) print('', file=f) - print('' % os.name, file=f) + print(''.format(os.name), file=f) print('', file=f) - print('' % (junit_ts_name, junit_tc_name, job.status, job.total_time), file=f) + print(''.format(junit_ts_name, junit_tc_name, job.status, job.total_time), file=f) if junit_errors: - print('' % (job.status, job.status), file=f) + print(''.format(job.status, job.status), file=f) if junit_failures: - print('' % (job.status, job.status), file=f) + print(''.format(job.status, job.status), file=f) print('', end="", file=f) - with open("%s/logfile.txt" % (job.workdir), "r") as logf: + with open("{}/logfile.txt".format(job.workdir), "r") as logf: for line in logf: print(line.replace("&", "&").replace("<", "<").replace(">", ">").replace("\"", """), end="", file=f) print('', file=f) - with open("%s/status" % (job.workdir), "w") as f: - print("%s %d %d" % (job.status, job.retcode, job.total_time), file=f) + with open("{}/status".format(job.workdir), "w") as f: + print("{{{} {} {}}}".format(job.status, job.retcode, job.total_time), file=f) return job.retcode diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 2a6977c..e27a5c2 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -97,7 +97,7 @@ class SbyTask: if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)): if self.logfile is not None: print(line, file=self.logfile) - self.job.log("%s: %s" % (self.info, line)) + self.job.log("{}: {}".format(self.info, line)) def handle_exit(self, retcode): if self.terminated: @@ -111,7 +111,7 @@ class SbyTask: if self.job.opt_wait and not timeout: return if self.running: - self.job.log("%s: terminating process" % self.info) + self.job.log("{}: terminating process".format(self.info)) if os.name == "posix": os.killpg(self.p.pid, signal.SIGTERM) self.p.terminate() @@ -128,7 +128,7 @@ class SbyTask: if not dep.finished: return - self.job.log("%s: starting process \"%s\"" % (self.info, self.cmdline)) + self.job.log("{}: starting process \"{}\"".format(self.info, self.cmdline)) if os.name == "posix": def preexec_fn(): @@ -162,14 +162,14 @@ class SbyTask: self.handle_output(outs) if self.p.poll() is not None: - self.job.log("%s: finished (returncode=%d)" % (self.info, self.p.returncode)) + self.job.log("{}: finished (returncode={})".format(self.info, self.p.returncode)) self.job.tasks_running.remove(self) all_tasks_running.remove(self) self.running = False if self.p.returncode == 127: self.job.status = "ERROR" - self.job.log("%s: COMMAND NOT FOUND. ERROR." % self.info) + self.job.log("{}: COMMAND NOT FOUND. ERROR.".format(self.info)) self.terminated = True self.job.terminate() return @@ -178,7 +178,7 @@ class SbyTask: if self.checkretcode and self.p.returncode != 0: self.job.status = "ERROR" - self.job.log("%s: job failed. ERROR." % self.info) + self.job.log("{}: job failed. ERROR.".format(self.info)) self.terminated = True self.job.terminate() return @@ -229,13 +229,13 @@ class SbyJob: self.summary = list() - self.logfile = open("%s/logfile.txt" % workdir, "a") + self.logfile = open("{}/logfile.txt".format(workdir), "a") for line in early_logs: print(line, file=self.logfile, flush=True) if not reusedir: - with open("%s/config.sby" % workdir, "w") as f: + with open("{}/config.sby".format(workdir), "w") as f: for line in sbyconfig: print(line, file=f) @@ -266,25 +266,25 @@ class SbyJob: if self.opt_timeout is not None: total_clock_time = int(time() - self.start_clock_time) if total_clock_time > self.opt_timeout: - self.log("Reached TIMEOUT (%d seconds). Terminating all tasks." % self.opt_timeout) + self.log("Reached TIMEOUT ({} seconds). Terminating all tasks.".format(self.opt_timeout)) self.status = "TIMEOUT" self.terminate(timeout=True) def log(self, logmessage): tm = localtime() - print("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True) - print("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True) + print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True) + print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True) def error(self, logmessage): tm = localtime() - print("SBY %2d:%02d:%02d [%s] ERROR: %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True) - print("SBY %2d:%02d:%02d [%s] ERROR: %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True) + print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True) + print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True) self.status = "ERROR" if "ERROR" not in self.expect: self.retcode = 16 self.terminate() - with open("%s/%s" % (self.workdir, self.status), "w") as f: - print("ERROR: %s" % logmessage, file=f) + with open("{}/{}".format(self.workdir, self.status), "w") as f: + print("ERROR: {}".format(logmessage), file=f) raise SbyAbort(logmessage) def makedirs(self, path): @@ -297,7 +297,7 @@ class SbyJob: for dstfile, lines in self.verbatim_files.items(): dstfile = self.workdir + "/src/" + dstfile - self.log("Writing '%s'." % dstfile) + self.log("Writing '{}'.".format(dstfile)) with open(dstfile, "w") as f: for line in lines: @@ -305,7 +305,7 @@ class SbyJob: for dstfile, srcfile in self.files.items(): if dstfile.startswith("/") or dstfile.startswith("../") or ("/../" in dstfile): - self.error("destination filename must be a relative path without /../: %s" % dstfile) + self.error("destination filename must be a relative path without /../: {}".format(dstfile)) dstfile = self.workdir + "/src/" + dstfile srcfile = process_filename(srcfile) @@ -314,7 +314,7 @@ class SbyJob: if basedir != "" and not os.path.exists(basedir): os.makedirs(basedir) - self.log("Copy '%s' to '%s'." % (srcfile, dstfile)) + self.log("Copy '{}' to '{}'.".format(srcfile, dstfile)) copyfile(srcfile, dstfile) def handle_str_option(self, option_name, default_value): @@ -334,19 +334,19 @@ class SbyJob: def handle_bool_option(self, option_name, default_value): if option_name in self.options: if self.options[option_name] not in ["on", "off"]: - self.error("Invalid value '%s' for boolean option %s." % (self.options[option_name], option_name)) + self.error("Invalid value '{}' for boolean option {}.".format(self.options[option_name], option_name)) self.__dict__["opt_" + option_name] = self.options[option_name] == "on" self.used_options.add(option_name) else: self.__dict__["opt_" + option_name] = default_value def make_model(self, model_name): - if not os.path.isdir("%s/model" % self.workdir): - os.makedirs("%s/model" % self.workdir) + if not os.path.isdir("{}/model".format(self.workdir)): + os.makedirs("{}/model".format(self.workdir)) if model_name in ["base", "nomem"]: - with open("%s/model/design%s.ys" % (self.workdir, "" if model_name == "base" else "_nomem"), "w") as f: - print("# running in %s/src/" % self.workdir, file=f) + with open("{}/model/design{}.ys".format(self.workdir, "" if model_name == "base" else "_nomem"), "w") as f: + print("# running in {}/src/".format(self.workdir), file=f) for cmd in self.script: print(cmd, file=f) if model_name == "base": @@ -370,19 +370,19 @@ class SbyJob: print("opt -keepdc -fast", file=f) print("check", file=f) print("hierarchy -simcheck", file=f) - print("write_ilang ../model/design%s.il" % ("" if model_name == "base" else "_nomem"), file=f) + print("write_ilang ../model/design{}.il".format("" if model_name == "base" else "_nomem"), file=f) task = SbyTask(self, model_name, [], - "cd %s/src; %s -ql ../model/design%s.log ../model/design%s.ys" % (self.workdir, self.exe_paths["yosys"], - "" if model_name == "base" else "_nomem", "" if model_name == "base" else "_nomem")) + "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format(self.workdir, self.exe_paths["yosys"], + s="" if model_name == "base" else "_nomem")) task.checkretcode = True return [task] if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name): - with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f: - print("# running in %s/model/" % (self.workdir), file=f) - print("read_ilang design%s.il" % ("_nomem" if "_nomem" in model_name else ""), file=f) + with open("{}/model/design_{}.ys".format(self.workdir, model_name), "w") as f: + print("# running in {}/model/".format(self.workdir), file=f) + print("read_ilang design{}.il".format("_nomem" if "_nomem" in model_name else ""), file=f) if "_syn" in model_name: print("techmap", file=f) print("opt -fast", file=f) @@ -390,22 +390,22 @@ class SbyJob: print("opt_clean", file=f) print("stat", file=f) if "_stbv" in model_name: - print("write_smt2 -stbv -wires design_%s.smt2" % model_name, file=f) + print("write_smt2 -stbv -wires design_{}.smt2".format(model_name), file=f) elif "_stdt" in model_name: - print("write_smt2 -stdt -wires design_%s.smt2" % model_name, file=f) + print("write_smt2 -stdt -wires design_{}.smt2".format(model_name), file=f) else: - print("write_smt2 -wires design_%s.smt2" % model_name, file=f) + print("write_smt2 -wires design_{}.smt2".format(model_name), file=f) task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), - "cd %s/model; %s -ql design_%s.log design_%s.ys" % (self.workdir, self.exe_paths["yosys"], model_name, model_name)) + "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)) task.checkretcode = True return [task] if re.match(r"^btor(_syn)?(_nomem)?$", model_name): - with open("%s/model/design_%s.ys" % (self.workdir, model_name), "w") as f: - print("# running in %s/model/" % (self.workdir), file=f) - print("read_ilang design%s.il" % ("_nomem" if "_nomem" in model_name else ""), file=f) + with open("{}/model/design_{}.ys".format(self.workdir, model_name), "w") as f: + print("# running in {}/model/".format(self.workdir), file=f) + print("read_ilang design{}.il".format("_nomem" if "_nomem" in model_name else ""), file=f) print("flatten", file=f) print("setundef -undriven -anyseq", file=f) print("setattr -unset keep", file=f) @@ -417,17 +417,17 @@ class SbyJob: print("abc", file=f) print("opt_clean", file=f) print("stat", file=f) - print("write_btor design_%s.btor" % model_name, file=f) + print("write_btor design_{}.btor".format(model_name), file=f) task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"), - "cd %s/model; %s -ql design_%s.log design_%s.ys" % (self.workdir, self.exe_paths["yosys"], model_name, model_name)) + "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)) task.checkretcode = True return [task] if model_name == "aig": - with open("%s/model/design_aiger.ys" % (self.workdir), "w") as f: - print("# running in %s/model/" % (self.workdir), file=f) + with open("{}/model/design_aiger.ys".format(self.workdir), "w") as f: + print("# running in {}/model/".format(self.workdir), file=f) print("read_ilang design_nomem.il", file=f) print("flatten", file=f) print("setundef -undriven -anyseq", file=f) @@ -442,7 +442,7 @@ class SbyJob: print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f) task = SbyTask(self, "aig", self.model("nomem"), - "cd %s/model; %s -ql design_aiger.log design_aiger.ys" % (self.workdir, self.exe_paths["yosys"])) + "cd {}/model; {} -ql design_aiger.log design_aiger.ys".format(self.workdir, self.exe_paths["yosys"])) task.checkretcode = True return [task] @@ -485,7 +485,7 @@ class SbyJob: mode = None key = None - with open("%s/config.sby" % self.workdir, "r") as f: + with open("{}/config.sby".format(self.workdir), "r") as f: for line in f: raw_line = line if mode in ["options", "engines", "files"]: @@ -501,48 +501,48 @@ class SbyJob: if match: entries = match.group(1).split() if len(entries) == 0: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) if entries[0] == "options": mode = "options" if len(self.options) != 0 or len(entries) != 1: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) continue if entries[0] == "engines": mode = "engines" if len(self.engines) != 0 or len(entries) != 1: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) continue if entries[0] == "script": mode = "script" if len(self.script) != 0 or len(entries) != 1: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) continue if entries[0] == "file": mode = "file" if len(entries) != 2: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) current_verbatim_file = entries[1] if current_verbatim_file in self.verbatim_files: - self.error("duplicate file: %s" % entries[1]) + self.error("duplicate file: {}".format(entries[1])) self.verbatim_files[current_verbatim_file] = list() continue if entries[0] == "files": mode = "files" if len(entries) != 1: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) continue - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) if mode == "options": entries = line.split() if len(entries) != 2: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) self.options[entries[0]] = entries[1] continue @@ -562,19 +562,19 @@ class SbyJob: elif len(entries) == 2: self.files[entries[0]] = entries[1] else: - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) continue if mode == "file": self.verbatim_files[current_verbatim_file].append(raw_line) continue - self.error("sby file syntax error: %s" % line) + self.error("sby file syntax error: {}".format(line)) self.handle_str_option("mode", None) if self.opt_mode not in ["bmc", "prove", "cover", "live"]: - self.error("Invalid mode: %s" % self.opt_mode) + self.error("Invalid mode: {}".format(self.opt_mode)) self.expect = ["PASS"] if "expect" in self.options: @@ -583,7 +583,7 @@ class SbyJob: for s in self.expect: if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]: - self.error("Invalid expect value: %s" % s) + self.error("Invalid expect value: {}".format(s)) self.handle_bool_option("multiclock", False) self.handle_bool_option("wait", False) @@ -610,7 +610,7 @@ class SbyJob: self.error("Config file is lacking engine configuration.") if self.reusedir: - rmtree("%s/model" % self.workdir, ignore_errors=True) + rmtree("{}/model".format(self.workdir), ignore_errors=True) else: self.copy_src() @@ -639,7 +639,7 @@ class SbyJob: for opt in self.options.keys(): if opt not in self.used_options: - self.error("Unused option: %s" % opt) + self.error("Unused option: {}".format(opt)) self.taskloop() @@ -651,20 +651,20 @@ class SbyJob: self.total_time = total_process_time self.summary = [ - "Elapsed clock time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" % + "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), - "Elapsed process time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" % + "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time), ] + self.summary else: self.summary = [ - "Elapsed clock time [H:MM:SS (secs)]: %d:%02d:%02d (%d)" % + "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time), "Elapsed process time unvailable on Windows" ] + self.summary for line in self.summary: - self.log("summary: %s" % line) + self.log("summary: {}".format(line)) assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"] @@ -677,6 +677,6 @@ class SbyJob: if self.status == "TIMEOUT": self.retcode = 8 if self.status == "ERROR": self.retcode = 16 - with open("%s/%s" % (self.workdir, self.status), "w") as f: + with open("{}/{}".format(self.workdir, self.status), "w") as f: for line in self.summary: print(line, file=f) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index efab714..306bb36 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -31,24 +31,24 @@ def run(mode, job, engine_idx, engine): if abc_command[0] == "bmc3": if mode != "bmc": job.error("ABC command 'bmc3' is only valid in bmc mode.") - abc_command[0] += " -F %d -v" % job.opt_depth + abc_command[0] += " -F {} -v".format(job.opt_depth) elif abc_command[0] == "sim3": if mode != "bmc": job.error("ABC command 'sim3' is only valid in bmc mode.") - abc_command[0] += " -F %d -v" % job.opt_depth + abc_command[0] += " -F {} -v".format(job.opt_depth) elif abc_command[0] == "pdr": if mode != "prove": job.error("ABC command 'pdr' is only valid in prove mode.") else: - job.error("Invalid ABC command %s." % abc_command[0]) + job.error("Invalid ABC command {}.".format(abc_command[0])) - task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), - ("cd %s; %s -c 'read_aiger model/design_aiger.aig; fold; strash; %s; write_cex -a engine_%d/trace.aiw'") % + task = SbyTask(job, "engine_{}".format(engine_idx), job.model("aig"), + ("cd {}; {} -c 'read_aiger model/design_aiger.aig; fold; strash; {}; write_cex -a engine_{}/trace.aiw'").format (job.workdir, job.exe_paths["abc"], " ".join(abc_command), engine_idx), - logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) + logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) task.noprintregex = re.compile(r"^\.+$") task_status = None @@ -78,19 +78,19 @@ def run(mode, job, engine_idx, engine): assert task_status is not None job.update_status(task_status) - job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) - job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status)) + job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status)) + job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status)) job.terminate() if task_status == "FAIL" and job.opt_aigsmt != "none": - task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw --aig-noheader model/design_smt2.smt2") % + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), + ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw --aig-noheader model/design_smt2.smt2").format (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx), - logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), + job.opt_append, i=engine_idx, engine_idx, engine_idx, engine_idx), + logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) task2_status = None @@ -109,12 +109,11 @@ def run(mode, job, engine_idx, engine): assert task2_status is not None assert task2_status == "FAIL" - if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)): - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) task2.output_callback = output_callback2 task2.exit_callback = exit_callback2 task.output_callback = output_callback task.exit_callback = exit_callback - diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index b5b20e4..dbe05c5 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -40,16 +40,16 @@ def run(mode, job, engine_idx, engine): solver_cmd = " ".join([job.exe_paths["aigbmc"]] + solver_args[1:]) else: - job.error("Invalid solver command %s." % solver_args[0]) + job.error("Invalid solver command {}.".format(solver_args[0])) - task = SbyTask(job, "engine_%d" % engine_idx, job.model("aig"), - "cd %s; %s model/design_aiger.aig" % (job.workdir, solver_cmd), - logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) + task = SbyTask(job, "engine_{}".format(engine_idx), job.model("aig"), + "cd {}; {} model/design_aiger.aig".format(job.workdir, solver_cmd), + logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) task_status = None produced_cex = False end_of_cex = False - aiw_file = open("%s/engine_%d/trace.aiw" % (job.workdir, engine_idx), "w") + aiw_file = open("{}/engine_{}/trace.aiw".format(job.workdir, engine_idx), "w") def output_callback(line): nonlocal task_status @@ -66,7 +66,7 @@ def run(mode, job, engine_idx, engine): return None if line.startswith("u"): - return "No CEX up to depth %d." % (int(line[1:])-1) + return "No CEX up to depth {}.".format(int(line[1:])-1) if line in ["0", "1", "2"]: print(line, file=aiw_file) @@ -84,29 +84,29 @@ def run(mode, job, engine_idx, engine): aiw_file.close() job.update_status(task_status) - job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) - job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status)) + job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status)) + job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status)) job.terminate() if task_status == "FAIL" and job.opt_aigsmt != "none": if produced_cex: if mode == "live": - task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; %s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") % + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), + ("cd {}; {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - engine_idx, engine_idx, engine_idx, engine_idx), - logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), + i=engine_idx), + logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) else: - task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("cd %s; %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --aig model/design_aiger.aim:engine_%d/trace.aiw model/design_smt2.smt2") % + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), + ("cd {}; {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + "--dump-smtc engine_{i}/trace.smtc --aig model/design_aiger.aim:engine_{i}/trace.aiw model/design_smt2.smt2").format (job.workdir, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - job.opt_append, engine_idx, engine_idx, engine_idx, engine_idx), - logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), + job.opt_append, i=engine_idx), + logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) task2_status = None @@ -128,15 +128,14 @@ def run(mode, job, engine_idx, engine): else: assert task2_status == "FAIL" - if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)): - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) task2.output_callback = output_callback2 task2.exit_callback = exit_callback2 else: - job.log("engine_%d: Engine did not produce a counter example." % engine_idx) + job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx)) task.output_callback = output_callback task.exit_callback = exit_callback - diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 63d5cc9..1130a3a 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -29,22 +29,22 @@ def run(mode, job, engine_idx, engine): job.error("Unexpected BTOR engine options.") if solver_args[0] == "btormc": - solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax %d" % (job.opt_depth - 1) + solver_cmd = job.exe_paths["btormc"] + " --stop-first -v 1 -kmax {}".format(job.opt_depth - 1) if job.opt_skip is not None: - solver_cmd += " -kmin %d" % job.opt_skip + solver_cmd += " -kmin {}".format(job.opt_skip) solver_cmd += " ".join([""] + solver_args[1:]) else: - job.error("Invalid solver command %s." % solver_args[0]) + job.error("Invalid solver command {}.".format(solver_args[0])) - task = SbyTask(job, "engine_%d" % engine_idx, job.model("btor"), - "cd %s; %s model/design_btor.btor" % (job.workdir, solver_cmd), - logfile=open("%s/engine_%d/logfile.txt" % (job.workdir, engine_idx), "w")) + task = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"), + "cd {}; {} model/design_btor.btor".format(job.workdir, solver_cmd), + logfile=open("{}/engine_{}/logfile.txt".format(job.workdir, engine_idx), "w")) task_status = None produced_cex = False end_of_cex = False - wit_file = open("%s/engine_%d/trace.wit" % (job.workdir, engine_idx), "w") + wit_file = open("{}/engine_{}/trace.wit".format(job.workdir, engine_idx), "w") def output_callback(line): nonlocal task_status @@ -61,7 +61,7 @@ def run(mode, job, engine_idx, engine): end_of_cex = True if line.startswith("u"): - return "No CEX up to depth %d." % (int(line[1:])-1) + return "No CEX up to depth {}.".format(int(line[1:])-1) if solver_args[0] == "btormc": if "calling BMC on" in line: @@ -89,8 +89,8 @@ def run(mode, job, engine_idx, engine): wit_file.close() job.update_status(task_status) - job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status)) - job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status)) + job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status)) + job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status)) job.terminate() @@ -98,7 +98,7 @@ def run(mode, job, engine_idx, engine): if produced_cex: has_arrays = False - with open("%s/model/design_btor.btor" % job.workdir, "r") as f: + with open("{}/model/design_btor.btor".format(job.workdir), "r") as f: for line in f: line = line.split() if len(line) == 5 and line[1] == "sort" and line[2] == "array": @@ -106,28 +106,25 @@ def run(mode, job, engine_idx, engine): break if has_arrays: - setupcmd = "cd %s;" % (job.workdir) - finalwit = "engine_%d/trace.wit" % engine_idx + setupcmd = "cd {};".format(job.workdir) + finalwit = "engine_{}/trace.wit".format(engine_idx) else: - setupcmd = "cd %s; { echo sat; btorsim --states model/design_btor.btor engine_%d/trace.wit; } > engine_%d/simtrace.wit &&" % (job.workdir, engine_idx, engine_idx) - finalwit = "engine_%d/simtrace.wit" % engine_idx + setupcmd = "cd {}; { echo sat; btorsim --states model/design_btor.btor engine_{i}/trace.wit; } > engine_{i}/simtrace.wit &&".format(job.workdir, i=engine_idx) + finalwit = "engine_{}/simtrace.wit".format(engine_idx) if mode == "live": - task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("%s %s -g -s %s%s --noprogress --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --btorwit %s model/design_smt2.smt2") % - (setupcmd, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - engine_idx, engine_idx, engine_idx, finalwit), - logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), + ("{} {} -g -s {}{} --noprogress --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + "--dump-smtc engine_{i}/trace.smtc --btorwit {} model/design_smt2.smt2").format(setupcmd, job.exe_paths["smtbmc"], job.opt_aigsmt, "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), finalwit, i=engine_idx), + logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) else: - task2 = SbyTask(job, "engine_%d" % engine_idx, job.model("smt2"), - ("%s %s -s %s%s --noprogress --append %d --dump-vcd engine_%d/trace.vcd --dump-vlogtb engine_%d/trace_tb.v " + - "--dump-smtc engine_%d/trace.smtc --btorwit %s model/design_smt2.smt2") % + task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("smt2"), + ("{} {} -s {}{} --noprogress --append {} --dump-vcd engine_{i}/trace.vcd --dump-vlogtb engine_{i}/trace_tb.v " + + "--dump-smtc engine_{i}/trace.smtc --btorwit {} model/design_smt2.smt2").format (setupcmd, job.exe_paths["smtbmc"], job.opt_aigsmt, - "" if job.opt_tbtop is None else " --vlogtb-top %s" % job.opt_tbtop, - job.opt_append, engine_idx, engine_idx, engine_idx, finalwit), - logfile=open("%s/engine_%d/logfile2.txt" % (job.workdir, engine_idx), "w")) + "" if job.opt_tbtop is None else " --vlogtb-top {}".format(job.opt_tbtop), + job.opt_append, finalwit, i=engine_idx), + logfile=open("{}/engine_{}/logfile2.txt".format(job.workdir, engine_idx), "w")) task2_status = None @@ -149,15 +146,14 @@ def run(mode, job, engine_idx, engine): else: assert task2_status == "FAIL" - if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)): - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) task2.output_callback = output_callback2 task2.exit_callback = exit_callback2 else: - job.log("engine_%d: Engine did not produce a counter example." % engine_idx) + job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx)) task.output_callback = output_callback task.exit_callback = exit_callback - diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index d843ec2..fb5eab4 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -65,7 +65,7 @@ def run(mode, job, engine_idx, engine): job.error("smtbmc options --basecase and --induction are exclusive.") induction_only = True else: - job.error("Invalid smtbmc options %s." % o) + job.error("Invalid smtbmc options {}.".format(o)) xtra_opts = False for i, a in enumerate(args): @@ -86,7 +86,7 @@ def run(mode, job, engine_idx, engine): smtbmc_opts += ["--unroll"] if job.opt_smtc is not None: - smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc] + smtbmc_opts += ["--smtc", "src/{}".format(job.opt_smtc)] if job.opt_tbtop is not None: smtbmc_opts += ["--vlogtb-top", job.opt_tbtop] @@ -104,9 +104,9 @@ def run(mode, job, engine_idx, engine): run("prove_induction", job, engine_idx, engine) return - taskname = "engine_%d" % engine_idx - trace_prefix = "engine_%d/trace" % engine_idx - logfile_prefix = "%s/engine_%d/logfile" % (job.workdir, engine_idx) + taskname = "engine_{}".format(engine_idx) + trace_prefix = "engine_{}/trace".format(engine_idx) + logfile_prefix = "{}/engine_{}/logfile".format(job.workdir, engine_idx) if mode == "prove_basecase": taskname += ".basecase" @@ -130,13 +130,13 @@ def run(mode, job, engine_idx, engine): if job.opt_skip is not None: - t_opt = "%d:%d" % (job.opt_skip, job.opt_depth) + t_opt = "{}:{}".format(job.opt_skip, job.opt_depth) else: - t_opt = "%d" % job.opt_depth + t_opt = "{}".format(job.opt_depth) task = SbyTask(job, taskname, job.model(model_name), - "cd %s; %s %s -t %s --append %d --dump-vcd %s.vcd --dump-vlogtb %s_tb.v --dump-smtc %s.smtc model/design_%s.smt2" % - (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, trace_prefix, trace_prefix, trace_prefix, model_name), + "cd {}; {} {} -t {} --append {} --dump-vcd {p}.vcd --dump-vlogtb {p}_tb.v --dump-smtc {p}.smtc model/design_{}.smt2".format + (job.workdir, job.exe_paths["smtbmc"], " ".join(smtbmc_opts), t_opt, job.opt_append, model_name, p=trace_prefix), logfile=open(logfile_prefix + ".txt", "w"), logstderr=(not progress)) if mode == "prove_basecase": @@ -169,24 +169,24 @@ def run(mode, job, engine_idx, engine): def exit_callback(retcode): if task_status is None: - job.error("engine_%d: Engine terminated without status." % engine_idx) + job.error("engine_{}: Engine terminated without status.".format(engine_idx)) if mode == "bmc" or mode == "cover": job.update_status(task_status) task_status_lower = task_status.lower() if task_status == "PASS" else task_status - job.log("engine_%d: Status returned by engine: %s" % (engine_idx, task_status_lower)) - job.summary.append("engine_%d (%s) returned %s" % (engine_idx, " ".join(engine), task_status_lower)) + job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status_lower)) + job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status_lower)) if task_status == "FAIL" and mode != "cover": - if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)): - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) job.terminate() elif mode in ["prove_basecase", "prove_induction"]: task_status_lower = task_status.lower() if task_status == "PASS" else task_status - job.log("engine_%d: Status returned by engine for %s: %s" % (engine_idx, mode.split("_")[1], task_status_lower)) - job.summary.append("engine_%d (%s) returned %s for %s" % (engine_idx, " ".join(engine), task_status_lower, mode.split("_")[1])) + job.log("engine_{}: Status returned by engine for {}: {}".format(engine_idx, mode.split("_")[1], task_status_lower)) + job.summary.append("engine_{} ({}) returned {} for {}".format(engine_idx, " ".join(engine), task_status_lower, mode.split("_")[1])) if mode == "prove_basecase": for task in job.basecase_tasks: @@ -197,8 +197,8 @@ def run(mode, job, engine_idx, engine): else: job.update_status(task_status) - if os.path.exists("%s/engine_%d/trace.vcd" % (job.workdir, engine_idx)): - job.summary.append("counterexample trace: %s/engine_%d/trace.vcd" % (job.workdir, engine_idx)) + if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)): + job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx)) job.terminate() elif mode == "prove_induction": @@ -221,5 +221,3 @@ def run(mode, job, engine_idx, engine): task.output_callback = output_callback task.exit_callback = exit_callback - - diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index edb9b99..20ffe23 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -28,8 +28,8 @@ def run(job): engine = job.engines[engine_idx] assert len(engine) > 0 - job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.log("engine_{}: {}".format(engine_idx, " ".join(engine))) + job.makedirs("{}/engine_{}".format(job.workdir, engine_idx)) if engine[0] == "smtbmc": import sby_engine_smtbmc @@ -44,5 +44,4 @@ def run(job): sby_engine_btor.run("bmc", job, engine_idx, engine) else: - job.error("Invalid engine '%s' for bmc mode." % engine[0]) - + job.error("Invalid engine '{}' for bmc mode.".format(engine[0])) diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index 28c2f4d..b5dc022 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -27,13 +27,12 @@ def run(job): engine = job.engines[engine_idx] assert len(engine) > 0 - job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.log("engine_{}: {}".format(engine_idx, " ".join(engine))) + job.makedirs("{}/engine_{}".format(job.workdir, engine_idx)) if engine[0] == "smtbmc": import sby_engine_smtbmc sby_engine_smtbmc.run("cover", job, engine_idx, engine) else: - job.error("Invalid engine '%s' for cover mode." % engine[0]) - + job.error("Invalid engine '{}' for cover mode.".format(engine[0])) diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index 3a64ff0..9a046cb 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -28,13 +28,12 @@ def run(job): engine = job.engines[engine_idx] assert len(engine) > 0 - job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.log("engine_{}: {}".format(engine_idx, " ".join(engine))) + job.makedirs("{}/engine_{}".format(job.workdir, engine_idx)) if engine[0] == "aiger": import sby_engine_aiger sby_engine_aiger.run("live", job, engine_idx, engine) else: - job.error("Invalid engine '%s' for live mode." % engine[0]) - + job.error("Invalid engine '{}' for live mode.".format(engine[0])) diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index daabe8f..f3c3ac9 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -35,8 +35,8 @@ def run(job): engine = job.engines[engine_idx] assert len(engine) > 0 - job.log("engine_%d: %s" % (engine_idx, " ".join(engine))) - job.makedirs("%s/engine_%d" % (job.workdir, engine_idx)) + job.log("engine_{}: {}".format(engine_idx, " ".join(engine))) + job.makedirs("{}/engine_{}".format(job.workdir, engine_idx)) if engine[0] == "smtbmc": import sby_engine_smtbmc @@ -51,5 +51,4 @@ def run(job): sby_engine_abc.run("prove", job, engine_idx, engine) else: - job.error("Invalid engine '%s' for prove mode." % engine[0]) - + job.error("Invalid engine '{}' for prove mode.".format(engine[0]))