sbysrc/sby_core.py

   1 #
   2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
   3 #
   4 # Copyright (C) 2016  Clifford Wolf <clifford@clifford.at>
   5 #
   6 # Permission to use, copy, modify, and/or distribute this software for any
   7 # purpose with or without fee is hereby granted, provided that the above
   8 # copyright notice and this permission notice appear in all copies.
   9 #
  10 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17 #
  18
  19 import os, re, sys, signal
  20 if os.name == "posix":
  21     import resource, fcntl
  22 import subprocess
  23 from shutil import copyfile, rmtree
  24 from select import select
  25 from time import time, localtime, sleep
  26
  27 all_tasks_running = []
  28
  29 def force_shutdown(signum, frame):
  30     print("SBY ---- Keyboard interrupt or external termination signal ----", flush=True)
  31     for task in list(all_tasks_running):
  32         task.terminate()
  33     sys.exit(1)
  34
  35 if os.name == "posix":
  36     signal.signal(signal.SIGHUP, force_shutdown)
  37 signal.signal(signal.SIGINT, force_shutdown)
  38 signal.signal(signal.SIGTERM, force_shutdown)
  39
  40 def process_filename(filename):
  41     if filename.startswith("~/"):
  42         filename = os.environ['HOME'] + filename[1:]
  43
  44     filename = os.path.expandvars(filename)
  45
  46     return filename
  47
  48 class SbyTask:
  49     def __init__(self, job, info, deps, cmdline, logfile=None, logstderr=True, silent=False):
  50         self.running = False
  51         self.finished = False
  52         self.terminated = False
  53         self.checkretcode = False
  54         self.job = job
  55         self.info = info
  56         self.deps = deps
  57         if os.name == "posix":
  58             self.cmdline = cmdline
  59         else:
  60             # Windows command interpreter equivalents for sequential
  61             # commands (; => &) command grouping ({} => ()).
  62             replacements = {
  63                 ";" : "&",
  64                 "{" : "(",
  65                 "}" : ")",
  66             }
  67
  68             cmdline_copy = cmdline
  69             for u, w in replacements.items():
  70                 cmdline_copy = cmdline_copy.replace(u, w)
  71             self.cmdline = cmdline_copy
  72         self.logfile = logfile
  73         self.noprintregex = None
  74         self.notify = []
  75         self.linebuffer = ""
  76         self.logstderr = logstderr
  77         self.silent = silent
  78
  79         self.job.tasks_pending.append(self)
  80
  81         for dep in self.deps:
  82             dep.register_dep(self)
  83
  84         self.output_callback = None
  85         self.exit_callback = None
  86
  87     def register_dep(self, next_task):
  88         if self.finished:
  89             next_task.poll()
  90         else:
  91             self.notify.append(next_task)
  92
  93     def log(self, line):
  94         if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
  95             if self.logfile is not None:
  96                 print(line, file=self.logfile)
  97             self.job.log("{}: {}".format(self.info, line))
  98
  99     def handle_output(self, line):
 100         if self.terminated or len(line) == 0:
 101             return
 102         if self.output_callback is not None:
 103             line = self.output_callback(line)
 104         self.log(line)
 105
 106     def handle_exit(self, retcode):
 107         if self.terminated:
 108             return
 109         if self.logfile is not None:
 110             self.logfile.close()
 111         if self.exit_callback is not None:
 112             self.exit_callback(retcode)
 113
 114     def terminate(self, timeout=False):
 115         if self.job.opt_wait and not timeout:
 116             return
 117         if self.running:
 118             if not self.silent:
 119                 self.job.log("{}: terminating process".format(self.info))
 120             if os.name == "posix":
 121                 try:
 122                     os.killpg(self.p.pid, signal.SIGTERM)
 123                 except PermissionError:
 124                     pass
 125             self.p.terminate()
 126             self.job.tasks_running.remove(self)
 127             all_tasks_running.remove(self)
 128         self.terminated = True
 129
 130     def poll(self):
 131         if self.finished or self.terminated:
 132             return
 133
 134         if not self.running:
 135             for dep in self.deps:
 136                 if not dep.finished:
 137                     return
 138
 139             if not self.silent:
 140                 self.job.log("{}: starting process \"{}\"".format(self.info, self.cmdline))
 141
 142             if os.name == "posix":
 143                 def preexec_fn():
 144                     signal.signal(signal.SIGINT, signal.SIG_IGN)
 145                     os.setpgrp()
 146
 147                 self.p = subprocess.Popen(["/usr/bin/env", "bash", "-c", self.cmdline], stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
 148                         stderr=(subprocess.STDOUT if self.logstderr else None), preexec_fn=preexec_fn)
 149
 150                 fl = fcntl.fcntl(self.p.stdout, fcntl.F_GETFL)
 151                 fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK)
 152
 153             else:
 154                 self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
 155                         stderr=(subprocess.STDOUT if self.logstderr else None))
 156
 157             self.job.tasks_pending.remove(self)
 158             self.job.tasks_running.append(self)
 159             all_tasks_running.append(self)
 160             self.running = True
 161             return
 162
 163         while True:
 164             outs = self.p.stdout.readline().decode("utf-8")
 165             if len(outs) == 0: break
 166             if outs[-1] != '\n':
 167                 self.linebuffer += outs
 168                 break
 169             outs = (self.linebuffer + outs).strip()
 170             self.linebuffer = ""
 171             self.handle_output(outs)
 172
 173         if self.p.poll() is not None:
 174             if not self.silent:
 175                 self.job.log("{}: finished (returncode={})".format(self.info, self.p.returncode))
 176             self.job.tasks_running.remove(self)
 177             all_tasks_running.remove(self)
 178             self.running = False
 179
 180             if self.p.returncode == 127:
 181                 self.job.status = "ERROR"
 182                 if not self.silent:
 183                     self.job.log("{}: COMMAND NOT FOUND. ERROR.".format(self.info))
 184                 self.terminated = True
 185                 self.job.terminate()
 186                 return
 187
 188             self.handle_exit(self.p.returncode)
 189
 190             if self.checkretcode and self.p.returncode != 0:
 191                 self.job.status = "ERROR"
 192                 if not self.silent:
 193                     self.job.log("{}: job failed. ERROR.".format(self.info))
 194                 self.terminated = True
 195                 self.job.terminate()
 196                 return
 197
 198             self.finished = True
 199             for next_task in self.notify:
 200                 next_task.poll()
 201             return
 202
 203
 204 class SbyAbort(BaseException):
 205     pass
 206
 207
 208 class SbyJob:
 209     def __init__(self, sbyconfig, workdir, early_logs, reusedir):
 210         self.options = dict()
 211         self.used_options = set()
 212         self.engines = list()
 213         self.script = list()
 214         self.files = dict()
 215         self.verbatim_files = dict()
 216         self.models = dict()
 217         self.workdir = workdir
 218         self.reusedir = reusedir
 219         self.status = "UNKNOWN"
 220         self.total_time = 0
 221         self.expect = []
 222
 223         self.exe_paths = {
 224             "yosys": "yosys",
 225             "abc": "yosys-abc",
 226             "smtbmc": "yosys-smtbmc",
 227             "suprove": "suprove",
 228             "aigbmc": "aigbmc",
 229             "avy": "avy",
 230             "btormc": "btormc",
 231             "pono": "pono",
 232         }
 233
 234         self.tasks_running = []
 235         self.tasks_pending = []
 236
 237         self.start_clock_time = time()
 238
 239         if os.name == "posix":
 240             ru = resource.getrusage(resource.RUSAGE_CHILDREN)
 241             self.start_process_time = ru.ru_utime + ru.ru_stime
 242
 243         self.summary = list()
 244
 245         self.logfile = open("{}/logfile.txt".format(workdir), "a")
 246
 247         for line in early_logs:
 248             print(line, file=self.logfile, flush=True)
 249
 250         if not reusedir:
 251             with open("{}/config.sby".format(workdir), "w") as f:
 252                 for line in sbyconfig:
 253                     print(line, file=f)
 254
 255     def taskloop(self):
 256         for task in self.tasks_pending:
 257             task.poll()
 258
 259         while len(self.tasks_running):
 260             fds = []
 261             for task in self.tasks_running:
 262                 if task.running:
 263                     fds.append(task.p.stdout)
 264
 265             if os.name == "posix":
 266                 try:
 267                     select(fds, [], [], 1.0) == ([], [], [])
 268                 except InterruptedError:
 269                     pass
 270             else:
 271                 sleep(0.1)
 272
 273             for task in self.tasks_running:
 274                 task.poll()
 275
 276             for task in self.tasks_pending:
 277                 task.poll()
 278
 279             if self.opt_timeout is not None:
 280                 total_clock_time = int(time() - self.start_clock_time)
 281                 if total_clock_time > self.opt_timeout:
 282                     self.log("Reached TIMEOUT ({} seconds). Terminating all tasks.".format(self.opt_timeout))
 283                     self.status = "TIMEOUT"
 284                     self.terminate(timeout=True)
 285
 286     def log(self, logmessage):
 287         tm = localtime()
 288         print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
 289         print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
 290
 291     def error(self, logmessage):
 292         tm = localtime()
 293         print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
 294         print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
 295         self.status = "ERROR"
 296         if "ERROR" not in self.expect:
 297             self.retcode = 16
 298         self.terminate()
 299         with open("{}/{}".format(self.workdir, self.status), "w") as f:
 300             print("ERROR: {}".format(logmessage), file=f)
 301         raise SbyAbort(logmessage)
 302
 303     def makedirs(self, path):
 304         if self.reusedir and os.path.isdir(path):
 305             rmtree(path, ignore_errors=True)
 306         os.makedirs(path)
 307
 308     def copy_src(self):
 309         os.makedirs(self.workdir + "/src")
 310
 311         for dstfile, lines in self.verbatim_files.items():
 312             dstfile = self.workdir + "/src/" + dstfile
 313             self.log("Writing '{}'.".format(dstfile))
 314
 315             with open(dstfile, "w") as f:
 316                 for line in lines:
 317                     f.write(line)
 318
 319         for dstfile, srcfile in self.files.items():
 320             if dstfile.startswith("/") or dstfile.startswith("../") or ("/../" in dstfile):
 321                 self.error("destination filename must be a relative path without /../: {}".format(dstfile))
 322             dstfile = self.workdir + "/src/" + dstfile
 323
 324             srcfile = process_filename(srcfile)
 325
 326             basedir = os.path.dirname(dstfile)
 327             if basedir != "" and not os.path.exists(basedir):
 328                 os.makedirs(basedir)
 329
 330             self.log("Copy '{}' to '{}'.".format(srcfile, dstfile))
 331             copyfile(srcfile, dstfile)
 332
 333     def handle_str_option(self, option_name, default_value):
 334         if option_name in self.options:
 335             self.__dict__["opt_" + option_name] = self.options[option_name]
 336             self.used_options.add(option_name)
 337         else:
 338             self.__dict__["opt_" + option_name] = default_value
 339
 340     def handle_int_option(self, option_name, default_value):
 341         if option_name in self.options:
 342             self.__dict__["opt_" + option_name] = int(self.options[option_name])
 343             self.used_options.add(option_name)
 344         else:
 345             self.__dict__["opt_" + option_name] = default_value
 346
 347     def handle_bool_option(self, option_name, default_value):
 348         if option_name in self.options:
 349             if self.options[option_name] not in ["on", "off"]:
 350                 self.error("Invalid value '{}' for boolean option {}.".format(self.options[option_name], option_name))
 351             self.__dict__["opt_" + option_name] = self.options[option_name] == "on"
 352             self.used_options.add(option_name)
 353         else:
 354             self.__dict__["opt_" + option_name] = default_value
 355
 356     def make_model(self, model_name):
 357         if not os.path.isdir("{}/model".format(self.workdir)):
 358             os.makedirs("{}/model".format(self.workdir))
 359
 360         if model_name in ["base", "nomem"]:
 361             with open("{}/model/design{}.ys".format(self.workdir, "" if model_name == "base" else "_nomem"), "w") as f:
 362                 print("# running in {}/src/".format(self.workdir), file=f)
 363                 for cmd in self.script:
 364                     print(cmd, file=f)
 365                 if model_name == "base":
 366                     print("memory_nordff", file=f)
 367                 else:
 368                     print("memory_map", file=f)
 369                 if self.opt_multiclock:
 370                     print("clk2fflogic", file=f)
 371                 else:
 372                     print("async2sync", file=f)
 373                     print("chformal -assume -early", file=f)
 374                 if self.opt_mode in ["bmc", "prove"]:
 375                     print("chformal -live -fair -cover -remove", file=f)
 376                 if self.opt_mode == "cover":
 377                     print("chformal -live -fair -remove", file=f)
 378                 if self.opt_mode == "live":
 379                     print("chformal -assert2assume", file=f)
 380                     print("chformal -cover -remove", file=f)
 381                 print("opt_clean", file=f)
 382                 print("setundef -anyseq", file=f)
 383                 print("opt -keepdc -fast", file=f)
 384                 print("check", file=f)
 385                 print("hierarchy -simcheck", file=f)
 386                 print("write_ilang ../model/design{}.il".format("" if model_name == "base" else "_nomem"), file=f)
 387
 388             task = SbyTask(self, model_name, [],
 389                     "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format(self.workdir, self.exe_paths["yosys"],
 390                     s="" if model_name == "base" else "_nomem"))
 391             task.checkretcode = True
 392
 393             return [task]
 394
 395         if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):
 396             with open("{}/model/design_{}.ys".format(self.workdir, model_name), "w") as f:
 397                 print("# running in {}/model/".format(self.workdir), file=f)
 398                 print("read_ilang design{}.il".format("_nomem" if "_nomem" in model_name else ""), file=f)
 399                 if "_syn" in model_name:
 400                     print("techmap", file=f)
 401                     print("opt -fast", file=f)
 402                     print("abc", file=f)
 403                     print("opt_clean", file=f)
 404                 print("stat", file=f)
 405                 if "_stbv" in model_name:
 406                     print("write_smt2 -stbv -wires design_{}.smt2".format(model_name), file=f)
 407                 elif "_stdt" in model_name:
 408                     print("write_smt2 -stdt -wires design_{}.smt2".format(model_name), file=f)
 409                 else:
 410                     print("write_smt2 -wires design_{}.smt2".format(model_name), file=f)
 411
 412             task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"),
 413                     "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name))
 414             task.checkretcode = True
 415
 416             return [task]
 417
 418         if re.match(r"^btor(_syn)?(_nomem)?$", model_name):
 419             with open("{}/model/design_{}.ys".format(self.workdir, model_name), "w") as f:
 420                 print("# running in {}/model/".format(self.workdir), file=f)
 421                 print("read_ilang design{}.il".format("_nomem" if "_nomem" in model_name else ""), file=f)
 422                 print("flatten", file=f)
 423                 print("setundef -undriven -anyseq", file=f)
 424                 if "_syn" in model_name:
 425                     print("opt -full", file=f)
 426                     print("techmap", file=f)
 427                     print("opt -fast", file=f)
 428                     print("abc", file=f)
 429                     print("opt_clean", file=f)
 430                 else:
 431                     print("opt -fast", file=f)
 432                 print("delete -output", file=f)
 433                 print("stat", file=f)
 434                 print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
 435
 436             task = SbyTask(self, model_name, self.model("nomem" if "_nomem" in model_name else "base"),
 437                     "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name))
 438             task.checkretcode = True
 439
 440             return [task]
 441
 442         if model_name == "aig":
 443             with open("{}/model/design_aiger.ys".format(self.workdir), "w") as f:
 444                 print("# running in {}/model/".format(self.workdir), file=f)
 445                 print("read_ilang design_nomem.il", file=f)
 446                 print("flatten", file=f)
 447                 print("setundef -undriven -anyseq", file=f)
 448                 print("setattr -unset keep", file=f)
 449                 print("delete -output", file=f)
 450                 print("opt -full", file=f)
 451                 print("techmap", file=f)
 452                 print("opt -fast", file=f)
 453                 print("abc -g AND -fast", file=f)
 454                 print("opt_clean", file=f)
 455                 print("stat", file=f)
 456                 print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f)
 457
 458             task = SbyTask(self, "aig", self.model("nomem"),
 459                     "cd {}/model; {} -ql design_aiger.log design_aiger.ys".format(self.workdir, self.exe_paths["yosys"]))
 460             task.checkretcode = True
 461
 462             return [task]
 463
 464         assert False
 465
 466     def model(self, model_name):
 467         if model_name not in self.models:
 468             self.models[model_name] = self.make_model(model_name)
 469         return self.models[model_name]
 470
 471     def terminate(self, timeout=False):
 472         for task in list(self.tasks_running):
 473             task.terminate(timeout=timeout)
 474
 475     def update_status(self, new_status):
 476         assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
 477
 478         if new_status == "UNKNOWN":
 479             return
 480
 481         if self.status == "ERROR":
 482             return
 483
 484         if new_status == "PASS":
 485             assert self.status != "FAIL"
 486             self.status = "PASS"
 487
 488         elif new_status == "FAIL":
 489             assert self.status != "PASS"
 490             self.status = "FAIL"
 491
 492         elif new_status == "ERROR":
 493             self.status = "ERROR"
 494
 495         else:
 496             assert 0
 497
 498     def run(self, setupmode):
 499         mode = None
 500         key = None
 501
 502         with open("{}/config.sby".format(self.workdir), "r") as f:
 503             for line in f:
 504                 raw_line = line
 505                 if mode in ["options", "engines", "files"]:
 506                     line = re.sub(r"\s*(\s#.*)?$", "", line)
 507                     if line == "" or line[0] == "#":
 508                         continue
 509                 else:
 510                     line = line.rstrip()
 511                 # print(line)
 512                 if mode is None and (len(line) == 0 or line[0] == "#"):
 513                     continue
 514                 match = re.match(r"^\s*\[(.*)\]\s*$", line)
 515                 if match:
 516                     entries = match.group(1).split()
 517                     if len(entries) == 0:
 518                         self.error("sby file syntax error: {}".format(line))
 519
 520                     if entries[0] == "options":
 521                         mode = "options"
 522                         if len(self.options) != 0 or len(entries) != 1:
 523                             self.error("sby file syntax error: {}".format(line))
 524                         continue
 525
 526                     if entries[0] == "engines":
 527                         mode = "engines"
 528                         if len(self.engines) != 0 or len(entries) != 1:
 529                             self.error("sby file syntax error: {}".format(line))
 530                         continue
 531
 532                     if entries[0] == "script":
 533                         mode = "script"
 534                         if len(self.script) != 0 or len(entries) != 1:
 535                             self.error("sby file syntax error: {}".format(line))
 536                         continue
 537
 538                     if entries[0] == "file":
 539                         mode = "file"
 540                         if len(entries) != 2:
 541                             self.error("sby file syntax error: {}".format(line))
 542                         current_verbatim_file = entries[1]
 543                         if current_verbatim_file in self.verbatim_files:
 544                             self.error("duplicate file: {}".format(entries[1]))
 545                         self.verbatim_files[current_verbatim_file] = list()
 546                         continue
 547
 548                     if entries[0] == "files":
 549                         mode = "files"
 550                         if len(entries) != 1:
 551                             self.error("sby file syntax error: {}".format(line))
 552                         continue
 553
 554                     self.error("sby file syntax error: {}".format(line))
 555
 556                 if mode == "options":
 557                     entries = line.split()
 558                     if len(entries) != 2:
 559                         self.error("sby file syntax error: {}".format(line))
 560                     self.options[entries[0]] = entries[1]
 561                     continue
 562
 563                 if mode == "engines":
 564                     entries = line.split()
 565                     self.engines.append(entries)
 566                     continue
 567
 568                 if mode == "script":
 569                     self.script.append(line)
 570                     continue
 571
 572                 if mode == "files":
 573                     entries = line.split()
 574                     if len(entries) == 1:
 575                         self.files[os.path.basename(entries[0])] = entries[0]
 576                     elif len(entries) == 2:
 577                         self.files[entries[0]] = entries[1]
 578                     else:
 579                         self.error("sby file syntax error: {}".format(line))
 580                     continue
 581
 582                 if mode == "file":
 583                     self.verbatim_files[current_verbatim_file].append(raw_line)
 584                     continue
 585
 586                 self.error("sby file syntax error: {}".format(line))
 587
 588         self.handle_str_option("mode", None)
 589
 590         if self.opt_mode not in ["bmc", "prove", "cover", "live"]:
 591             self.error("Invalid mode: {}".format(self.opt_mode))
 592
 593         self.expect = ["PASS"]
 594         if "expect" in self.options:
 595             self.expect = self.options["expect"].upper().split(",")
 596             self.used_options.add("expect")
 597
 598         for s in self.expect:
 599             if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]:
 600                 self.error("Invalid expect value: {}".format(s))
 601
 602         self.handle_bool_option("multiclock", False)
 603         self.handle_bool_option("wait", False)
 604         self.handle_int_option("timeout", None)
 605
 606         self.handle_str_option("smtc", None)
 607         self.handle_int_option("skip", None)
 608         self.handle_str_option("tbtop", None)
 609
 610         if self.opt_smtc is not None:
 611             for engine in self.engines:
 612                 if engine[0] != "smtbmc":
 613                     self.error("Option smtc is only valid for smtbmc engine.")
 614
 615         if self.opt_skip is not None:
 616             if self.opt_skip == 0:
 617                 self.opt_skip = None
 618             else:
 619                 for engine in self.engines:
 620                     if engine[0] not in ["smtbmc", "btor"]:
 621                         self.error("Option skip is only valid for smtbmc and btor engines.")
 622
 623         if len(self.engines) == 0:
 624             self.error("Config file is lacking engine configuration.")
 625
 626         if self.reusedir:
 627             rmtree("{}/model".format(self.workdir), ignore_errors=True)
 628         else:
 629             self.copy_src()
 630
 631         if setupmode:
 632             self.retcode = 0
 633             return
 634
 635         if self.opt_mode == "bmc":
 636             import sby_mode_bmc
 637             sby_mode_bmc.run(self)
 638
 639         elif self.opt_mode == "prove":
 640             import sby_mode_prove
 641             sby_mode_prove.run(self)
 642
 643         elif self.opt_mode == "live":
 644             import sby_mode_live
 645             sby_mode_live.run(self)
 646
 647         elif self.opt_mode == "cover":
 648             import sby_mode_cover
 649             sby_mode_cover.run(self)
 650
 651         else:
 652             assert False
 653
 654         for opt in self.options.keys():
 655             if opt not in self.used_options:
 656                 self.error("Unused option: {}".format(opt))
 657
 658         self.taskloop()
 659
 660         total_clock_time = int(time() - self.start_clock_time)
 661
 662         if os.name == "posix":
 663             ru = resource.getrusage(resource.RUSAGE_CHILDREN)
 664             total_process_time = int((ru.ru_utime + ru.ru_stime) - self.start_process_time)
 665             self.total_time = total_process_time
 666
 667             self.summary = [
 668                 "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 669                         (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
 670                 "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 671                         (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time),
 672             ] + self.summary
 673         else:
 674             self.summary = [
 675                 "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 676                         (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
 677                 "Elapsed process time unvailable on Windows"
 678             ] + self.summary
 679
 680         for line in self.summary:
 681             self.log("summary: {}".format(line))
 682
 683         assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
 684
 685         if self.status in self.expect:
 686             self.retcode = 0
 687         else:
 688             if self.status == "PASS": self.retcode = 1
 689             if self.status == "FAIL": self.retcode = 2
 690             if self.status == "UNKNOWN": self.retcode = 4
 691             if self.status == "TIMEOUT": self.retcode = 8
 692             if self.status == "ERROR": self.retcode = 16
 693
 694         with open("{}/{}".format(self.workdir, self.status), "w") as f:
 695             for line in self.summary:
 696                 print(line, file=f)