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
  50 parser.add_argument("--yosys", metavar="<path_to_executable>",
  51         action=DictAction, dest="exe_paths")
  52 parser.add_argument("--abc", metavar="<path_to_executable>",
  53         action=DictAction, dest="exe_paths")
  54 parser.add_argument("--smtbmc", metavar="<path_to_executable>",
  55         action=DictAction, dest="exe_paths")
  56 parser.add_argument("--suprove", metavar="<path_to_executable>",
  57         action=DictAction, dest="exe_paths")
  58 parser.add_argument("--aigbmc", metavar="<path_to_executable>",
  59         action=DictAction, dest="exe_paths")
  60 parser.add_argument("--avy", metavar="<path_to_executable>",
  61         action=DictAction, dest="exe_paths")
  62 parser.add_argument("--btormc", metavar="<path_to_executable>",
  63         action=DictAction, dest="exe_paths")
  64 parser.add_argument("--pono", metavar="<path_to_executable>",
  65         action=DictAction, dest="exe_paths",
  66         help="configure which executable to use for the respective tool")
  67 parser.add_argument("--dumpcfg", action="store_true", dest="dump_cfg",
  68         help="print the pre-processed configuration file")
  69 parser.add_argument("--dumptags", action="store_true", dest="dump_tags",
  70         help="print the list of task tags")
  71 parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks",
  72         help="print the list of tasks")
  73 parser.add_argument("--dumpdefaults", action="store_true", dest="dump_defaults",
  74         help="print the list of default tasks")
  75 parser.add_argument("--dumptaskinfo", action="store_true", dest="dump_taskinfo",
  76         help="output a summary of tasks as JSON")
  77 parser.add_argument("--dumpfiles", action="store_true", dest="dump_files",
  78         help="print the list of source files")
  79 parser.add_argument("--setup", action="store_true", dest="setupmode",
  80         help="set up the working directory and exit")
  81
  82 parser.add_argument("--init-config-file", dest="init_config_file",
  83         help="create a default .sby config file")
  84 parser.add_argument("sbyfile", metavar="<jobname>.sby | <dirname>", nargs="?",
  85         help=".sby file OR directory containing config.sby file")
  86 parser.add_argument("arg_tasknames", metavar="tasknames", nargs="*",
  87         help="tasks to run (only valid when <jobname>.sby is used)")
  88
  89 args = parser.parse_args()
  90
  91 sbyfile = args.sbyfile
  92 workdir = args.workdir
  93 workdir_prefix = args.workdir_prefix
  94 if workdir is not None and workdir_prefix is not None:
  95     print("ERROR: -d and --prefix are mutually exclusive.", file=sys.stderr)
  96     sys.exit(1)
  97 tasknames = args.arg_tasknames + args.tasknames
  98 opt_force = args.force
  99 opt_backup = args.backup
 100 opt_tmpdir = args.tmpdir
 101 exe_paths = args.exe_paths
 102 throw_err = args.throw_err
 103 dump_cfg = args.dump_cfg
 104 dump_tags = args.dump_tags
 105 dump_tasks = args.dump_tasks
 106 dump_defaults = args.dump_defaults
 107 dump_taskinfo = args.dump_taskinfo
 108 dump_files = args.dump_files
 109 reusedir = False
 110 setupmode = args.setupmode
 111 init_config_file = args.init_config_file
 112
 113 if sbyfile is not None:
 114     if os.path.isdir(sbyfile):
 115         if workdir is not None:
 116             print("ERROR: Can't use -d when running in existing directory.", file=sys.stderr)
 117             sys.exit(1)
 118         workdir = sbyfile
 119         sbyfile += "/config.sby"
 120         reusedir = True
 121         if not opt_force and os.path.exists(workdir + "/model"):
 122             print("ERROR: Use -f to re-run in existing directory.", file=sys.stderr)
 123             sys.exit(1)
 124         if tasknames:
 125             print("ERROR: Can't use tasks when running in existing directory.", file=sys.stderr)
 126             sys.exit(1)
 127         if setupmode:
 128             print("ERROR: Can't use --setup with existing directory.", file=sys.stderr)
 129             sys.exit(1)
 130         if opt_force:
 131             for f in "PASS FAIL UNKNOWN ERROR TIMEOUT".split():
 132                 if os.path.exists(workdir + "/" + f):
 133                     os.remove(workdir + "/" + f)
 134     elif not sbyfile.endswith(".sby"):
 135         print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr)
 136         sys.exit(1)
 137
 138 elif init_config_file is not None:
 139     sv_file = init_config_file + ".sv"
 140     sby_file = init_config_file + ".sby"
 141     with open(sby_file, 'w') as config:
 142         config.write(f"""[options]
 143 mode bmc
 144
 145 [engines]
 146 smtbmc
 147
 148 [script]
 149 read -formal {sv_file}
 150 prep -top top
 151
 152 [files]
 153 {sv_file}
 154 """)
 155
 156     print(f"sby config written to {sby_file}", file=sys.stderr)
 157     sys.exit(0)
 158
 159 early_logmsgs = list()
 160
 161 def early_log(workdir, msg):
 162     tm = time.localtime()
 163     early_logmsgs.append("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
 164     print(early_logmsgs[-1])
 165
 166 def read_sbyconfig(sbydata, taskname):
 167     cfgdata = list()
 168     tasklist = list()
 169     defaultlist = None
 170     task_matched = False
 171
 172     pycode = None
 173     tasks_section = False
 174     task_tags_active = set()
 175     task_tags_all = set()
 176     task_skip_block = False
 177     task_skiping_blocks = False
 178
 179     def handle_line(line):
 180         nonlocal pycode, tasks_section, task_tags_active, task_tags_all
 181         nonlocal task_skip_block, task_skiping_blocks, task_matched
 182         nonlocal defaultlist
 183
 184         line = line.rstrip("\n")
 185         line = line.rstrip("\r")
 186
 187         if pycode is not None:
 188             if line == "--pycode-end--":
 189                 gdict = globals().copy()
 190                 gdict["task"] = taskname
 191                 gdict["tags"] = set(task_tags_active)
 192                 gdict["output_lines"] = list()
 193                 exec("def output(line):\n  output_lines.append(line)\n" + pycode, gdict)
 194                 pycode = None
 195                 for line in gdict["output_lines"]:
 196                     handle_line(line)
 197                 return
 198             pycode += line + "\n"
 199             return
 200
 201         if line == "--pycode-begin--":
 202             pycode = ""
 203             return
 204
 205         if tasks_section and line.startswith("["):
 206             tasks_section = False
 207
 208         if task_skiping_blocks:
 209             if line == "--":
 210                 task_skip_block = False
 211                 task_skiping_blocks = False
 212                 return
 213
 214         if not tasks_section:
 215             found_task_tag = False
 216             task_skip_line = False
 217
 218             for t in task_tags_all:
 219                 if line.startswith(t+":"):
 220                     line = line[len(t)+1:].lstrip()
 221                     match = t in task_tags_active
 222                 elif line.startswith("~"+t+":"):
 223                     line = line[len(t)+2:].lstrip()
 224                     match = t not in task_tags_active
 225                 else:
 226                     continue
 227
 228                 if line == "":
 229                     task_skiping_blocks = True
 230                     task_skip_block = not match
 231                     task_skip_line = True
 232                 else:
 233                     task_skip_line = not match
 234
 235                 found_task_tag = True
 236                 break
 237
 238             if len(task_tags_all) and not found_task_tag:
 239                 tokens = line.split()
 240                 if len(tokens) > 0 and tokens[0][0] == line[0] and tokens[0].endswith(":"):
 241                     print(f"ERROR: Invalid task specifier \"{tokens[0]}\".", file=sys.stderr)
 242                     sys.exit(1)
 243
 244             if task_skip_line or task_skip_block:
 245                 return
 246
 247         if tasks_section:
 248             if taskname is None:
 249                 cfgdata.append(line)
 250             if line.startswith("#"):
 251                 return
 252
 253             line = line.split(":")
 254             if len(line) == 1:
 255                 line = line[0].split()
 256                 if len(line) > 0:
 257                     lhs, rhs = line[:1], line[1:]
 258                 else:
 259                     return
 260             elif len(line) == 2:
 261                 lhs, rhs = line[0].split(), line[1].split()
 262             else:
 263                 print("ERROR: Syntax error in tasks block.", file=sys.stderr)
 264                 sys.exit(1)
 265
 266             for tagname in rhs:
 267                 if tagname == "default":
 268                     continue
 269                 if all(map(lambda c: c not in "(?*.[]|)", tagname)):
 270                     task_tags_all.add(tagname)
 271
 272             for tname in lhs:
 273                 if all(map(lambda c: c not in "(?*.[]|)", tname)):
 274                     if tname not in tasklist:
 275                         tasklist.append(tname)
 276                     if "default" in rhs:
 277                         if defaultlist is None:
 278                             defaultlist = list()
 279                         if tname not in defaultlist:
 280                             defaultlist.append(tname)
 281                     task_tags_all.add(tname)
 282
 283                 if taskname is not None and re.fullmatch(tname, taskname):
 284                     task_matched = True
 285                     task_tags_active.add(tname)
 286                     for tagname in rhs:
 287                         if tagname == "default":
 288                             continue
 289                         if all(map(lambda c: c not in "(?*.[]|)", tagname)):
 290                             task_tags_active.add(tagname)
 291                         else:
 292                             for t in task_tags_all:
 293                                 if re.fullmatch(tagname, t):
 294                                     task_tags_active.add(t)
 295
 296         elif line == "[tasks]":
 297             if taskname is None:
 298                 cfgdata.append(line)
 299             tasks_section = True
 300
 301         else:
 302             cfgdata.append(line)
 303
 304     for line in sbydata:
 305         handle_line(line)
 306
 307     if taskname is not None and not task_matched:
 308         print(f"ERROR: Task name '{taskname}' didn't match any lines in [tasks].", file=sys.stderr)
 309         sys.exit(1)
 310
 311     if defaultlist is None:
 312         defaultlist = tasklist
 313
 314     return cfgdata, tasklist, defaultlist, sorted(list(task_tags_all))
 315
 316
 317 sbydata = list()
 318 with (open(sbyfile, "r") if sbyfile is not None else sys.stdin) as f:
 319     for line in f:
 320         sbydata.append(line)
 321
 322 if dump_cfg:
 323     assert len(tasknames) < 2
 324     sbyconfig, _, _, _ = read_sbyconfig(sbydata, tasknames[0] if len(tasknames) else None)
 325     print("\n".join(sbyconfig))
 326     sys.exit(0)
 327
 328 if dump_files:
 329     file_set = set()
 330
 331     def find_files(taskname):
 332         sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
 333
 334         start_index = -1
 335         for i in range(len(sbyconfig)):
 336             if sbyconfig[i].strip() == "[files]":
 337                 start_index = i
 338                 break
 339
 340         if start_index == -1:
 341             return
 342
 343         for line in sbyconfig[start_index+1:]:
 344             line = line.strip()
 345             if line.startswith("["):
 346                 break
 347             if line == "" or line.startswith("#"):
 348                 continue
 349             filename = line.split()[-1]
 350             file_set.add(process_filename(filename))
 351
 352     if len(tasknames):
 353         for taskname in tasknames:
 354             find_files(taskname)
 355     else:
 356         find_files(None)
 357     print("\n".join(file_set))
 358     sys.exit(0)
 359
 360 if dump_tags:
 361     _, _, _, tagnames = read_sbyconfig(sbydata, None)
 362     for tag in tagnames:
 363         print(tag)
 364     sys.exit(0)
 365
 366 if dump_tasks or dump_defaults or dump_tags:
 367     _, tasks, dtasks, tags = read_sbyconfig(sbydata, None)
 368     for name in tasks if dump_tasks else dtasks if dump_defaults else tags:
 369         if name is not None:
 370             print(name)
 371     sys.exit(0)
 372
 373 if dump_taskinfo:
 374     _, _, tasknames, _ = read_sbyconfig(sbydata, None)
 375     taskinfo = {}
 376     for taskname in tasknames or [None]:
 377         task_sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
 378         taskinfo[taskname or ""] = info = {}
 379         cfg = SbyConfig()
 380         cfg.parse_config(task_sbyconfig)
 381         taskinfo[taskname or ""] = {
 382             "mode": cfg.options.get("mode"),
 383             "engines": cfg.engines,
 384             "script": cfg.script,
 385         }
 386     print(json.dumps(taskinfo, indent=2))
 387     sys.exit(0)
 388
 389 if len(tasknames) == 0:
 390     _, _, tasknames, _ = read_sbyconfig(sbydata, None)
 391     if len(tasknames) == 0:
 392         tasknames = [None]
 393
 394 if (workdir is not None) and (len(tasknames) != 1):
 395     print("ERROR: Exactly one task is required when workdir is specified. Specify the task or use --prefix instead of -d.", file=sys.stderr)
 396     sys.exit(1)
 397
 398 def run_task(taskname):
 399     my_opt_tmpdir = opt_tmpdir
 400     my_workdir = None
 401
 402     if workdir is not None:
 403         my_workdir = workdir
 404     elif workdir_prefix is not None:
 405         my_workdir = workdir_prefix + "_" + taskname
 406
 407     if my_workdir is None and sbyfile is not None and not my_opt_tmpdir:
 408         my_workdir = sbyfile[:-4]
 409         if taskname is not None:
 410             my_workdir += "_" + taskname
 411
 412     if my_workdir is not None:
 413         if opt_backup:
 414             backup_idx = 0
 415             while os.path.exists("{}.bak{:03d}".format(my_workdir, backup_idx)):
 416                 backup_idx += 1
 417             early_log(my_workdir, "Moving directory '{}' to '{}'.".format(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx)))
 418             shutil.move(my_workdir, "{}.bak{:03d}".format(my_workdir, backup_idx))
 419
 420         if opt_force and not reusedir:
 421             early_log(my_workdir, f"Removing directory '{os.path.abspath(my_workdir)}'.")
 422             if sbyfile:
 423                 shutil.rmtree(my_workdir, ignore_errors=True)
 424
 425         if reusedir:
 426             pass
 427         elif os.path.isdir(my_workdir):
 428             print(f"ERROR: Directory '{my_workdir}' already exists, use -f to overwrite the existing directory.")
 429             sys.exit(1)
 430         else:
 431             os.makedirs(my_workdir)
 432
 433     else:
 434         my_opt_tmpdir = True
 435         my_workdir = tempfile.mkdtemp()
 436
 437     if os.getenv("SBY_WORKDIR_GITIGNORE"):
 438         with open(f"{my_workdir}/.gitignore", "w") as gitignore:
 439             print("*", file=gitignore)
 440
 441     junit_ts_name = os.path.basename(sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin"
 442     junit_tc_name = taskname if taskname is not None else "default"
 443
 444     if reusedir:
 445         junit_filename = os.path.basename(my_workdir)
 446     elif sbyfile is not None:
 447         junit_filename = os.path.basename(sbyfile[:-4])
 448         if taskname is not None:
 449             junit_filename += "_" + taskname
 450     elif taskname is not None:
 451         junit_filename = taskname
 452     else:
 453         junit_filename = "junit"
 454
 455     sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
 456     task = SbyTask(sbyconfig, my_workdir, early_logmsgs, reusedir)
 457
 458     for k, v in exe_paths.items():
 459         task.exe_paths[k] = v
 460
 461     try:
 462         task.run(setupmode)
 463     except SbyAbort:
 464         if throw_err:
 465             raise
 466
 467     if my_opt_tmpdir:
 468         task.log(f"Removing directory '{my_workdir}'.")
 469         shutil.rmtree(my_workdir, ignore_errors=True)
 470
 471     if setupmode:
 472         task.log(f"SETUP COMPLETE (rc={task.retcode})")
 473     else:
 474         task.log(f"DONE ({task.status}, rc={task.retcode})")
 475     task.logfile.close()
 476
 477     if not my_opt_tmpdir and not setupmode:
 478         with open("{}/{}.xml".format(task.workdir, junit_filename), "w") as f:
 479             task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False)
 480
 481         with open(f"{task.workdir}/status", "w") as f:
 482             print(f"{task.status} {task.retcode} {task.total_time}", file=f)
 483
 484     return task.retcode
 485
 486
 487 failed = []
 488 retcode = 0
 489 for task in tasknames:
 490     task_retcode = run_task(task)
 491     retcode |= task_retcode
 492     if task_retcode:
 493         failed.append(task)
 494
 495 if failed and (len(tasknames) > 1 or tasknames[0] is not None):
 496     tm = time.localtime()
 497     print("SBY {:2d}:{:02d}:{:02d} The following tasks failed: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, failed))
 498
 499 sys.exit(retcode)