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  Clifford Wolf <clifford@clifford.at>
   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 os, sys, getopt, shutil, tempfile
  21 ##yosys-sys-path##
  22 from sby_core import SbyJob, SbyAbort
  23 from time import localtime
  24
  25 sbyfile = None
  26 workdir = None
  27 tasknames = list()
  28 opt_force = False
  29 opt_backup = False
  30 opt_tmpdir = False
  31 exe_paths = dict()
  32 throw_err = False
  33 dump_cfg = False
  34 dump_tasks = False
  35 reusedir = False
  36 setupmode = False
  37
  38 def usage():
  39     print("""
  40 sby [options] [<jobname>.sby [tasknames] | <dirname>]
  41
  42     -d <dirname>
  43         set workdir name. default: <jobname> (without .sby)
  44
  45     -f
  46         remove workdir if it already exists
  47
  48     -b
  49         backup workdir if it already exists
  50
  51     -t
  52         run in a temporary workdir (remove when finished)
  53
  54     -T taskname
  55         add taskname (useful when sby file is read from stdin)
  56
  57     -E
  58         throw an exception (incl stack trace) for most errors
  59
  60     --yosys <path_to_executable>
  61     --abc <path_to_executable>
  62     --smtbmc <path_to_executable>
  63     --suprove <path_to_executable>
  64     --aigbmc <path_to_executable>
  65     --avy <path_to_executable>
  66     --btormc <path_to_executable>
  67         configure which executable to use for the respective tool
  68
  69     --dumpcfg
  70         print the pre-processed configuration file
  71
  72     --dumptasks
  73         print the list of tasks
  74
  75     --setup
  76         set up the working directory and exit
  77 """)
  78     sys.exit(1)
  79
  80 try:
  81     opts, args = getopt.getopt(sys.argv[1:], "d:btfT:E", ["yosys=",
  82             "abc=", "smtbmc=", "suprove=", "aigbmc=", "avy=", "btormc=",
  83             "dumpcfg", "dumptasks", "setup"])
  84 except:
  85     usage()
  86
  87 for o, a in opts:
  88     if o == "-d":
  89         workdir = a
  90     elif o == "-f":
  91         opt_force = True
  92     elif o == "-b":
  93         opt_backup = True
  94     elif o == "-t":
  95         opt_tmpdir = True
  96     elif o == "-T":
  97         tasknames.append(a)
  98     elif o == "-E":
  99         throw_err = True
 100     elif o == "--yosys":
 101         exe_paths["yosys"] = a
 102     elif o == "--abc":
 103         exe_paths["abc"] = a
 104     elif o == "--smtbmc":
 105         exe_paths["smtbmc"] = a
 106     elif o == "--suprove":
 107         exe_paths["suprove"] = a
 108     elif o == "--aigbmc":
 109         exe_paths["aigbmc"] = a
 110     elif o == "--avy":
 111         exe_paths["avy"] = a
 112     elif o == "--btormc":
 113         exe_paths["btormc"] = a
 114     elif o == "--dumpcfg":
 115         dump_cfg = True
 116     elif o == "--dumptasks":
 117         dump_tasks = True
 118     elif o == "--setup":
 119         setupmode = True
 120     else:
 121         usage()
 122
 123 if len(args) > 0:
 124     sbyfile = args[0]
 125     if os.path.isdir(sbyfile):
 126         workdir = sbyfile
 127         sbyfile += "/config.sby"
 128         reusedir = True
 129         if not opt_force and os.path.exists(workdir + "/model"):
 130             print("ERROR: Use -f to re-run in existing directory.", file=sys.stderr)
 131             sys.exit(1)
 132         if len(args) > 1:
 133             print("ERROR: Can't use tasks when running in existing directory.", file=sys.stderr)
 134             sys.exit(1)
 135         if setupmode:
 136             print("ERROR: Can't use --setup with existing directory.", file=sys.stderr)
 137             sys.exit(1)
 138         if opt_force:
 139             for f in "PASS FAIL UNKNOWN ERROR TIMEOUT".split():
 140                 if os.path.exists(workdir + "/" + f):
 141                     os.remove(workdir + "/" + f)
 142     elif not sbyfile.endswith(".sby"):
 143         print("ERROR: Sby file does not have .sby file extension.", file=sys.stderr)
 144         sys.exit(1)
 145
 146 if len(args) > 1:
 147     tasknames = args[1:]
 148
 149
 150 early_logmsgs = list()
 151
 152 def early_log(workdir, msg):
 153     tm = localtime()
 154     early_logmsgs.append("SBY %2d:%02d:%02d [%s] %s" % (tm.tm_hour, tm.tm_min, tm.tm_sec, workdir, msg))
 155     print(early_logmsgs[-1])
 156
 157
 158 def read_sbyconfig(sbydata, taskname):
 159     cfgdata = list()
 160     tasklist = list()
 161
 162     pycode = None
 163     tasks_section = False
 164     task_tags_active = set()
 165     task_tags_all = set()
 166     task_skip_block = False
 167     task_skiping_blocks = False
 168
 169     def handle_line(line):
 170         nonlocal pycode, tasks_section, task_tags_active, task_tags_all
 171         nonlocal task_skip_block, task_skiping_blocks
 172
 173         line = line.rstrip("\n")
 174         line = line.rstrip("\r")
 175
 176         if pycode is not None:
 177             if line == "--pycode-end--":
 178                 gdict = globals().copy()
 179                 gdict["task"] = taskname
 180                 gdict["tags"] = set(task_tags_active)
 181                 gdict["output_lines"] = list()
 182                 exec("def output(line):\n  output_lines.append(line)\n" + pycode, gdict)
 183                 pycode = None
 184                 for line in gdict["output_lines"]:
 185                     handle_line(line)
 186                 return
 187             pycode += line + "\n"
 188             return
 189
 190         if line == "--pycode-begin--":
 191             pycode = ""
 192             return
 193
 194         if tasks_section and line.startswith("["):
 195             tasks_section = False
 196
 197         if task_skiping_blocks:
 198             if line == "--":
 199                 task_skip_block = False
 200                 task_skiping_blocks = False
 201                 return
 202
 203         found_task_tag = False
 204         task_skip_line = False
 205
 206         for t in task_tags_all:
 207             if line.startswith(t+":"):
 208                 line = line[len(t)+1:].lstrip()
 209                 match = t in task_tags_active
 210             elif line.startswith("~"+t+":"):
 211                 line = line[len(t)+2:].lstrip()
 212                 match = t not in task_tags_active
 213             else:
 214                 continue
 215
 216             if line == "":
 217                 task_skiping_blocks = True
 218                 task_skip_block = not match
 219                 task_skip_line = True
 220             else:
 221                 task_skip_line = not match
 222
 223             found_task_tag = True
 224             break
 225
 226         if len(task_tags_all) and not found_task_tag:
 227             tokens = line.split()
 228             if len(tokens) > 0 and tokens[0][0] == line[0] and tokens[0].endswith(":"):
 229                 print("ERROR: Invalid task specifier \"%s\"." % tokens[0], file=sys.stderr)
 230                 sys.exit(1)
 231
 232         if task_skip_line or task_skip_block:
 233             return
 234
 235         if tasks_section:
 236             if taskname is None:
 237                 cfgdata.append(line)
 238             if line.startswith("#"):
 239                 return
 240             line = line.split()
 241             if len(line) > 0:
 242                 tasklist.append(line[0])
 243             for t in line:
 244                 if taskname == line[0]:
 245                     task_tags_active.add(t)
 246                 task_tags_all.add(t)
 247
 248         elif line == "[tasks]":
 249             if taskname is None:
 250                 cfgdata.append(line)
 251             tasks_section = True
 252
 253         else:
 254             cfgdata.append(line)
 255
 256     for line in sbydata:
 257         handle_line(line)
 258
 259     return cfgdata, tasklist
 260
 261
 262 sbydata = list()
 263 with (open(sbyfile, "r") if sbyfile is not None else sys.stdin) as f:
 264     for line in f:
 265         sbydata.append(line)
 266
 267 if dump_cfg:
 268     assert len(tasknames) < 2
 269     sbyconfig, _ = read_sbyconfig(sbydata, tasknames[0] if len(tasknames) else None)
 270     print("\n".join(sbyconfig))
 271     sys.exit(0)
 272
 273 if len(tasknames) == 0:
 274     _, tasknames = read_sbyconfig(sbydata, None)
 275     if len(tasknames) == 0:
 276         tasknames = [None]
 277
 278 if dump_tasks:
 279     for task in tasknames:
 280         if task is not None:
 281             print(task)
 282     sys.exit(0)
 283
 284 if (workdir is not None) and (len(tasknames) != 1):
 285     print("ERROR: Exactly one task is required when workdir is specified.", file=sys.stderr)
 286     sys.exit(1)
 287
 288 def run_job(taskname):
 289     my_workdir = workdir
 290     my_opt_tmpdir = opt_tmpdir
 291
 292     if my_workdir is None and sbyfile is not None and not my_opt_tmpdir:
 293         my_workdir = sbyfile[:-4]
 294         if taskname is not None:
 295             my_workdir += "_" + taskname
 296
 297     if my_workdir is not None:
 298         if opt_backup:
 299             backup_idx = 0
 300             while os.path.exists("%s.bak%03d" % (my_workdir, backup_idx)):
 301                 backup_idx += 1
 302             early_log(my_workdir, "Moving direcory '%s' to '%s'." % (my_workdir, "%s.bak%03d" % (my_workdir, backup_idx)))
 303             shutil.move(my_workdir, "%s.bak%03d" % (my_workdir, backup_idx))
 304
 305         if opt_force and not reusedir:
 306             early_log(my_workdir, "Removing direcory '%s'." % (my_workdir))
 307             if sbyfile:
 308                 shutil.rmtree(my_workdir, ignore_errors=True)
 309
 310         if reusedir:
 311             pass
 312         elif os.path.isdir(my_workdir):
 313             print("ERROR: Direcory '%s' already exists." % (my_workdir))
 314             sys.exit(1)
 315         else:
 316             os.makedirs(my_workdir)
 317
 318     else:
 319         my_opt_tmpdir = True
 320         my_workdir = tempfile.mkdtemp()
 321
 322     junit_ts_name = os.path.basename(sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin"
 323     junit_tc_name = taskname if taskname is not None else "default"
 324
 325     if reusedir:
 326         junit_filename = os.path.basename(my_workdir)
 327     elif sbyfile is not None:
 328         junit_filename = os.path.basename(sbyfile[:-4])
 329         if taskname is not None:
 330             junit_filename += "_" + taskname
 331     elif taskname is not None:
 332         junit_filename = taskname
 333     else:
 334         junit_filename = "junit"
 335
 336     sbyconfig, _ = read_sbyconfig(sbydata, taskname)
 337     job = SbyJob(sbyconfig, my_workdir, early_logmsgs, reusedir)
 338
 339     for k, v in exe_paths.items():
 340         job.exe_paths[k] = v
 341
 342     if throw_err:
 343         job.run(setupmode)
 344     else:
 345         try:
 346             job.run(setupmode)
 347         except SbyAbort:
 348             pass
 349
 350     if my_opt_tmpdir:
 351         job.log("Removing direcory '%s'." % (my_workdir))
 352         shutil.rmtree(my_workdir, ignore_errors=True)
 353
 354     if setupmode:
 355         job.log("SETUP COMPLETE (rc=%d)" % (job.retcode))
 356     else:
 357         job.log("DONE (%s, rc=%d)" % (job.status, job.retcode))
 358     job.logfile.close()
 359
 360     if not my_opt_tmpdir and not setupmode:
 361         with open("%s/%s.xml" % (job.workdir, junit_filename), "w") as f:
 362             junit_errors = 1 if job.retcode == 16 else 0
 363             junit_failures = 1 if job.retcode != 0 and junit_errors == 0 else 0
 364             print('<?xml version="1.0" encoding="UTF-8"?>', file=f)
 365             print('<testsuites disabled="0" errors="%d" failures="%d" tests="1" time="%d">' % (junit_errors, junit_failures, job.total_time), file=f)
 366             print('<testsuite disabled="0" errors="%d" failures="%d" name="%s" skipped="0" tests="1" time="%d">' % (junit_errors, junit_failures, junit_ts_name, job.total_time), file=f)
 367             print('<properties>', file=f)
 368             print('<property name="os" value="%s"/>' % os.name, file=f)
 369             print('</properties>', file=f)
 370             print('<testcase classname="%s" name="%s" status="%s" time="%d">' % (junit_ts_name, junit_tc_name, job.status, job.total_time), file=f)
 371             if junit_errors:
 372                 print('<error message="%s" type="%s"/>' % (job.status, job.status), file=f)
 373             if junit_failures:
 374                 print('<failure message="%s" type="%s"/>' % (job.status, job.status), file=f)
 375             print('<system-out>', end="", file=f)
 376             with open("%s/logfile.txt" % (job.workdir), "r") as logf:
 377                 for line in logf:
 378                     print(line.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;").replace("\"", "&quot;"), end="", file=f)
 379             print('</system-out></testcase></testsuite></testsuites>', file=f)
 380         with open("%s/.stamp" % (job.workdir), "w") as f:
 381             print("%s %d %d" % (job.status, job.retcode, job.total_time), file=f)
 382
 383     return job.retcode
 384
 385
 386 retcode = 0
 387 for t in tasknames:
 388     retcode |= run_job(t)
 389
 390 sys.exit(retcode)