sbysrc/sby.py

   1 #!/usr/bin/env python3
   2 #
   3 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
   4 #
   5 # Copyright (C) 2016  Claire Xenia Wolf <claire@yosyshq.com>
   6 #
   7 # Permission to use, copy, modify, and/or distribute this software for any
   8 # purpose with or without fee is hereby granted, provided that the above
   9 # copyright notice and this permission notice appear in all copies.
  10 #
  11 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  12 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  13 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  14 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  15 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  16 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  17 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  18 #
  19
  20 import argparse, json, os, sys, shutil, tempfile, re
  21 ##yosys-sys-path##
  22 from sby_core import SbyConfig, SbyTask, SbyAbort, process_filename
  23 import time, platform
  24
  25 class DictAction(argparse.Action):
  26     def __call__(self, parser, namespace, values, option_string=None):
  27         assert isinstance(getattr(namespace, self.dest), dict), f"Use ArgumentParser.set_defaults() to initialize {self.dest} to dict()"
  28         name = option_string.lstrip(parser.prefix_chars).replace("-", "_")
  29         getattr(namespace, self.dest)[name] = values
  30
  31 parser = argparse.ArgumentParser(prog="sby",
  32         usage="%(prog)s [options] [<jobname>.sby [tasknames] | <dirname>]")
  33 parser.set_defaults(exe_paths=dict())
  34
  35 parser.add_argument("-d", metavar="<dirname>", dest="workdir",
  36         help="set workdir name. default: <jobname> or <jobname>_<taskname>. When there is more than one task, use --prefix instead")
  37 parser.add_argument("--prefix", metavar="<dirname>", dest="workdir_prefix",
  38         help="set the workdir name prefix. `_<taskname>` will be appended to the path for each task")
  39 parser.add_argument("-f", action="store_true", dest="force",
  40         help="remove workdir if it already exists")
  41 parser.add_argument("-b", action="store_true", dest="backup",
  42         help="backup workdir if it already exists")
  43 parser.add_argument("-t", action="store_true", dest="tmpdir",
  44         help="run in a temporary workdir (remove when finished)")
  45 parser.add_argument("-T", metavar="<taskname>", action="append", dest="tasknames", default=list(),
  46         help="add taskname (useful when sby file is read from stdin)")
  47 parser.add_argument("-E", action="store_true", dest="throw_err",
  48         help="throw an exception (incl stack trace) for most errors")
  49 parser.add_argument("--autotune", action="store_true", dest="autotune",
  50         help="automatically find a well performing engine and engine configuration for each task")
  51 parser.add_argument("--autotune-config", dest="autotune_config",
  52         help="read an autotune configuration file (overrides the sby file's autotune options)")
  53
  54 parser.add_argument("--yosys", metavar="<path_to_executable>",
  55         action=DictAction, dest="exe_paths")
  56 parser.add_argument("--abc", metavar="<path_to_executable>",
  57         action=DictAction, dest="exe_paths")
  58 parser.add_argument("--smtbmc", metavar="<path_to_executable>",
  59         action=DictAction, dest="exe_paths")
  60 parser.add_argument("--suprove", metavar="<path_to_executable>",
  61         action=DictAction, dest="exe_paths")
  62 parser.add_argument("--aigbmc", metavar="<path_to_executable>",
  63         action=DictAction, dest="exe_paths")
  64 parser.add_argument("--avy", metavar="<path_to_executable>",
  65         action=DictAction, dest="exe_paths")
  66 parser.add_argument("--btormc", metavar="<path_to_executable>",
  67         action=DictAction, dest="exe_paths")
  68 parser.add_argument("--pono", metavar="<path_to_executable>",
  69         action=DictAction, dest="exe_paths",
  70         help="configure which executable to use for the respective tool")
  71 parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg",
  72         help="print the pre-processed configuration file")
  73 parser.add_argument("--dumptags", action="store_true", dest="dump_tags",
  74         help="print the list of task tags")
  75 parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks",
  76         help="print the list of tasks")
  77 parser.add_argument("--dumpdefaults", action="store_true", dest="dump_defaults",
  78         help="print the list of default tasks")
  79 parser.add_argument("--dumptaskinfo", action="store_true", dest="dump_taskinfo",
  80         help="output a summary of tasks as JSON")
  81 parser.add_argument("--dumpfiles", action="store_true", dest="dump_files",
  82         help="print the list of source files")
  83 parser.add_argument("--setup", action="store_true", dest="setupmode",
  84         help="set up the working directory and exit")
  85
  86 parser.add_argument("--init-config-file", dest="init_config_file",
  87         help="create a default .sby config file")
  88 parser.add_argument("sbyfile", metavar="<jobname>.sby | <dirname>", nargs="?",
  89         help=".sby file OR directory containing config.sby file")
  90 parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*",
  91         help="tasks to run (only valid when <jobname>.sby is used)")
  92
  93 args = parser.parse_args()
  94
  95 sbyfile = args.sbyfile
  96 workdir = args.workdir
  97 workdir_prefix = args.workdir_prefix
  98 if workdir is not None and workdir_prefix is not None:
  99     print("ERROR: -d and --prefix are mutually exclusive.", file=sys.stderr)
 100     sys.exit(1)
 101 tasknames = args.arg_tasknames + args.tasknames
 102 opt_force = args.force
 103 opt_backup = args.backup
 104 opt_tmpdir = args.tmpdir
 105 exe_paths = args.exe_paths
 106 throw_err = args.throw_err
 107 dump_cfg = args.dump_cfg
 108 dump_tags = args.dump_tags
 109 dump_tasks = args.dump_tasks
 110 dump_defaults = args.dump_defaults
 111 dump_taskinfo = args.dump_taskinfo
 112 dump_files = args.dump_files
 113 reusedir = False
 114 setupmode = args.setupmode
 115 autotune = args.autotune
 116 autotune_config = args.autotune_config
 117 init_config_file = args.init_config_file
 118
 119 if sbyfile is not None:
 120     if os.path.isdir(sbyfile):
 121         if workdir is not None:
 122             print("ERROR: Can't use -d when running in existing directory.", file=sys.stderr)
 123             sys.exit(1)
 124         workdir = sbyfile
 125         sbyfile += "/config.sby"
 126         reusedir = True
 127         if not opt_force and os.path.exists(workdir + "/model"):
 128             print("ERROR: Use -f to re-run in existing directory.", file=sys.stderr)
 129             sys.exit(1)
 130         if tasknames:
 131             print("ERROR: Can't use tasks when running in existing directory.", file=sys.stderr)
 132             sys.exit(1)
 133         if setupmode:
 134             print("ERROR: Can't use --setup with existing directory.", file=sys.stderr)
 135             sys.exit(1)
 136         if opt_force:
 137             for f in "PASS FAIL UNKNOWN ERROR TIMEOUT".split():
 138                 if os.path.exists(workdir + "/" + f):
 139                     os.remove(workdir + "/" + f)
 140     elif not sbyfile.endswith(".sby"):
 141         print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr)
 142         sys.exit(1)
 143
 144 elif init_config_file is not None:
 145     sv_file = init_config_file + ".sv"
 146     sby_file = init_config_file + ".sby"
 147     with open(sby_file, 'w') as config:
 148         config.write(f"""[options]
 149 mode bmc
 150
 151 [engines]
 152 smtbmc
 153
 154 [script]
 155 read -formal {sv_file}
 156 prep -top top
 157
 158 [files]
 159 {sv_file}
 160 """)
 161
 162     print(f"sby config written to {sby_file}", file=sys.stderr)
 163     sys.exit(0)
 164
 165 early_logmsgs = list()
 166
 167 def early_log(workdir, msg):
 168     tm = time.localtime()
 169     early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
 170     print(early_logmsgs[-1])
 171
 172 def read_sbyconfig(sbydata, taskname):
 173     cfgdata = list()
 174     tasklist = list()
 175     defaultlist = None
 176     task_matched = False
 177
 178     pycode = None
 179     tasks_section = False
 180     task_tags_active = set()
 181     task_tags_all = set()
 182     task_skip_block = False
 183     task_skiping_blocks = False
 184
 185     def handle_line(line):
 186         nonlocal pycode, tasks_section, task_tags_active, task_tags_all
 187         nonlocal task_skip_block, task_skiping_blocks, task_matched
 188         nonlocal defaultlist
 189
 190         line = line.rstrip("\n")
 191         line = line.rstrip("\r")
 192
 193         if pycode is not None:
 194             if line == "--pycode-end--":
 195                 gdict = globals().copy()
 196                 gdict["task"] = taskname
 197                 gdict["tags"] = set(task_tags_active)
 198                 gdict["output_lines"] = list()
 199                 exec("def output(line):\n  output_lines.append(line)\n" + pycode, gdict)
 200                 pycode = None
 201                 for line in gdict["output_lines"]:
 202                     handle_line(line)
 203                 return
 204             pycode += line + "\n"
 205             return
 206
 207         if line == "--pycode-begin--":
 208             pycode = ""
 209             return
 210
 211         if tasks_section and line.startswith("["):
 212             tasks_section = False
 213
 214         if task_skiping_blocks:
 215             if line == "--":
 216                 task_skip_block = False
 217                 task_skiping_blocks = False
 218                 return
 219
 220         if not tasks_section:
 221             found_task_tag = False
 222             task_skip_line = False
 223
 224             for t in task_tags_all:
 225                 if line.startswith(t+":"):
 226                     line = line[len(t)+1:].lstrip()
 227                     match = t in task_tags_active
 228                 elif line.startswith("~"+t+":"):
 229                     line = line[len(t)+2:].lstrip()
 230                     match = t not in task_tags_active
 231                 else:
 232                     continue
 233
 234                 if line == "":
 235                     task_skiping_blocks = True
 236                     task_skip_block = not match
 237                     task_skip_line = True
 238                 else:
 239                     task_skip_line = not match
 240
 241                 found_task_tag = True
 242                 break
 243
 244             if len(task_tags_all) and not found_task_tag:
 245                 tokens = line.split()
 246                 if len(tokens) > 0 and tokens[0][0] == line[0] and tokens[0].endswith(":"):
 247                     print(f"ERROR: Invalid task specifier \"{tokens[0]}\".", file=sys.stderr)
 248                     sys.exit(1)
 249
 250             if task_skip_line or task_skip_block:
 251                 return
 252
 253         if tasks_section:
 254             if taskname is None:
 255                 cfgdata.append(line)
 256             if line.startswith("#"):
 257                 return
 258
 259             line = line.split(":")
 260             if len(line) == 1:
 261                 line = line[0].split()
 262                 if len(line) > 0:
 263                     lhs, rhs = line[:1], line[1:]
 264                 else:
 265                     return
 266             elif len(line) == 2:
 267                 lhs, rhs = line[0].split(), line[1].split()
 268             else:
 269                 print("ERROR: Syntax error in tasks block.", file=sys.stderr)
 270                 sys.exit(1)
 271
 272             for tagname in rhs:
 273                 if tagname == "default":
 274                     continue
 275                 if all(map(lambda c: c not in "(?*.[]|)", tagname)):
 276                     task_tags_all.add(tagname)
 277
 278             for tname in lhs:
 279                 if all(map(lambda c: c not in "(?*.[]|)", tname)):
 280                     if tname not in tasklist:
 281                         tasklist.append(tname)
 282                     if "default" in rhs:
 283                         if defaultlist is None:
 284                             defaultlist = list()
 285                         if tname not in defaultlist:
 286                             defaultlist.append(tname)
 287                     task_tags_all.add(tname)
 288
 289                 if taskname is not None and re.fullmatch(tname, taskname):
 290                     task_matched = True
 291                     task_tags_active.add(tname)
 292                     for tagname in rhs:
 293                         if tagname == "default":
 294                             continue
 295                         if all(map(lambda c: c not in "(?*.[]|)", tagname)):
 296                             task_tags_active.add(tagname)
 297                         else:
 298                             for t in task_tags_all:
 299                                 if re.fullmatch(tagname, t):
 300                                     task_tags_active.add(t)
 301
 302         elif line == "[tasks]":
 303             if taskname is None:
 304                 cfgdata.append(line)
 305             tasks_section = True
 306
 307         else:
 308             cfgdata.append(line)
 309
 310     for line in sbydata:
 311         handle_line(line)
 312
 313     if taskname is not None and not task_matched:
 314         print(f"ERROR: Task name '{taskname}' didn't match any lines in [tasks].", file=sys.stderr)
 315         sys.exit(1)
 316
 317     if defaultlist is None:
 318         defaultlist = tasklist
 319
 320     return cfgdata, tasklist, defaultlist, sorted(list(task_tags_all))
 321
 322
 323 sbydata = list()
 324 with (open(sbyfile, "r") if sbyfile is not None else sys.stdin) as f:
 325     for line in f:
 326         sbydata.append(line)
 327
 328 if dump_cfg:
 329     assert len(tasknames) < 2
 330     sbyconfig, _, _, _ = read_sbyconfig(sbydata, tasknames[0] if len(tasknames) else None)
 331     print("\n".join(sbyconfig))
 332     sys.exit(0)
 333
 334 if dump_files:
 335     file_set = set()
 336
 337     def find_files(taskname):
 338         sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
 339
 340         start_index = -1
 341         for i in range(len(sbyconfig)):
 342             if sbyconfig[i].strip() == "[files]":
 343                 start_index = i
 344                 break
 345
 346         if start_index == -1:
 347             return
 348
 349         for line in sbyconfig[start_index+1:]:
 350             line = line.strip()
 351             if line.startswith("["):
 352                 break
 353             if line == "" or line.startswith("#"):
 354                 continue
 355             filename = line.split()[-1]
 356             file_set.add(process_filename(filename))
 357
 358     if len(tasknames):
 359         for taskname in tasknames:
 360             find_files(taskname)
 361     else:
 362         find_files(None)
 363     print("\n".join(file_set))
 364     sys.exit(0)
 365
 366 if dump_tags:
 367     _, _, _, tagnames = read_sbyconfig(sbydata, None)
 368     for tag in tagnames:
 369         print(tag)
 370     sys.exit(0)
 371
 372 if dump_tasks or dump_defaults or dump_tags:
 373     _, tasks, dtasks, tags = read_sbyconfig(sbydata, None)
 374     for name in tasks if dump_tasks else dtasks if dump_defaults else tags:
 375         if name is not None:
 376             print(name)
 377     sys.exit(0)
 378
 379 if dump_taskinfo:
 380     _, _, tasknames, _ = read_sbyconfig(sbydata, None)
 381     taskinfo = {}
 382     for taskname in tasknames or [None]:
 383         task_sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
 384         taskinfo[taskname or ""] = info = {}
 385         cfg = SbyConfig()
 386         cfg.parse_config(task_sbyconfig)
 387         taskinfo[taskname or ""] = {
 388             "mode": cfg.options.get("mode"),
 389             "engines": cfg.engines,
 390             "script": cfg.script,
 391         }
 392     print(json.dumps(taskinfo, indent=2))
 393     sys.exit(0)
 394
 395 if len(tasknames) == 0:
 396     _, _, tasknames, _ = read_sbyconfig(sbydata, None)
 397     if len(tasknames) == 0:
 398         tasknames = [None]
 399
 400 if (workdir is not None) and (len(tasknames) != 1):
 401     print("ERROR: Exactly one task is required when workdir is specified. Specify the task or use --prefix instead of -d.", file=sys.stderr)
 402     sys.exit(1)
 403
 404 def run_task(taskname):
 405     sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
 406
 407     my_opt_tmpdir = opt_tmpdir
 408     my_workdir = None
 409
 410     if workdir is not None:
 411         my_workdir = workdir
 412     elif workdir_prefix is not None:
 413         if taskname is None:
 414             my_workdir = workdir_prefix
 415         else:
 416             my_workdir = workdir_prefix + "_" + taskname
 417
 418     if my_workdir is None and sbyfile is not None and not my_opt_tmpdir:
 419         my_workdir = sbyfile[:-4]
 420         if taskname is not None:
 421             my_workdir += "_" + taskname
 422
 423     if my_workdir is not None:
 424         if opt_backup:
 425             backup_idx = 0
 426             while os.path.exists("{}.bak{:03d}".format(my_workdir, backup_idx)):
 427                 backup_idx += 1
 428             early_log(my_workdir, "Moving directory '{}' to '{}'.".format(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx)))
 429             shutil.move(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx))
 430
 431         if opt_force and not reusedir:
 432             early_log(my_workdir, f"Removing directory '{os.path.abspath(my_workdir)}'.")
 433             if sbyfile:
 434                 shutil.rmtree(my_workdir, ignore_errors=True)
 435
 436         if reusedir:
 437             pass
 438         elif os.path.isdir(my_workdir):
 439             print(f"ERROR: Directory '{my_workdir}' already exists, use -f to overwrite the existing directory.")
 440             sys.exit(1)
 441         else:
 442             os.makedirs(my_workdir)
 443
 444     else:
 445         my_opt_tmpdir = True
 446         my_workdir = tempfile.mkdtemp()
 447
 448     if os.getenv("SBY_WORKDIR_GITIGNORE"):
 449         with open(f"{my_workdir}/.gitignore", "w") as gitignore:
 450             print("*", file=gitignore)
 451
 452     junit_ts_name = os.path.basename(sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin"
 453     junit_tc_name = taskname if taskname is not None else "default"
 454
 455     if reusedir:
 456         junit_filename = os.path.basename(my_workdir)
 457     elif sbyfile is not None:
 458         junit_filename = os.path.basename(sbyfile[:-4])
 459         if taskname is not None:
 460             junit_filename += "_" + taskname
 461     elif taskname is not None:
 462         junit_filename = taskname
 463     else:
 464         junit_filename = "junit"
 465
 466     task = SbyTask(sbyconfig, my_workdir, early_logmsgs, reusedir)
 467
 468     for k, v in exe_paths.items():
 469         task.exe_paths[k] = v
 470
 471     try:
 472         if autotune:
 473             import sby_autotune
 474             sby_autotune.SbyAutotune(task, autotune_config).run()
 475         else:
 476             task.run(setupmode)
 477     except SbyAbort:
 478         if throw_err:
 479             raise
 480
 481     if my_opt_tmpdir:
 482         task.log(f"Removing directory '{my_workdir}'.")
 483         shutil.rmtree(my_workdir, ignore_errors=True)
 484
 485     if setupmode:
 486         task.log(f"SETUP COMPLETE (rc={task.retcode})")
 487     else:
 488         task.log(f"DONE ({task.status}, rc={task.retcode})")
 489     task.logfile.close()
 490
 491     if not my_opt_tmpdir and not setupmode and not autotune:
 492         with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f:
 493             task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False)
 494
 495         with open(f"{task.workdir}/status", "w") as f:
 496             print(f"{task.status} {task.retcode} {task.total_time}", file=f)
 497
 498     return task.retcode
 499
 500
 501 failed = []
 502 retcode = 0
 503 for task in tasknames:
 504     task_retcode = run_task(task)
 505     retcode |= task_retcode
 506     if task_retcode:
 507         failed.append(task)
 508
 509 if failed and (len(tasknames) > 1 or tasknames[0] is not None):
 510     tm = time.localtime()
 511     print("SBY {:2d}:{:02d}:{:02d} The following tasks failed: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, failed))
 512
 513 sys.exit(retcode)