YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
387 stars 73 forks source link

fix 'junit_type' referenced before assignment error #149

Closed jix closed 2 years ago

jix commented 2 years ago

This fixes #143

nakengelhardt commented 2 years ago

OK yeah, I understand how that ended up there now.

The actual type of failure in this case is "unexpected result", as you should only end up in this code path if the return status is not in the expect list, but there were no errors in running the build... maybe we should put in type="EXPECT" instead?

Is that the context where you ran across it, or did it pop up in different circumstances as well?

jix commented 2 years ago

I did not pay close attention to when exactly this happened, I can double check that tomorrow, but I also just noticed that independent of this change, that line causes an error if there's a syntax error in the sby file:

SBY 20:21:48 [test] ERROR: sby file syntax error: [engine]
SBY 20:21:48 [test] DONE (ERROR, rc=16)
Traceback (most recent call last):
  File "/home/jix/work/sby/sbysrc/sby.py", line 469, in <module>
    task_retcode = run_task(task)
  File "/home/jix/work/sby/sbysrc/sby.py", line 458, in run_task
    task.print_junit_result(f, junit_ts_name, junit_tc_name, junit_format_strict=False)
  File "/home/jix/work/sby/sbysrc/sby_core.py", line 817, in print_junit_result
    junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode
AttributeError: 'SbyTask' object has no attribute 'opt_mode'
nakengelhardt commented 2 years ago

Oh yeah, that's expected: there is no checking of the input file at all, so if you get anything wrong there it errors all over the place in cryptic ways. (Fixing that in general, and https://github.com/YosysHQ/sby/issues/81 specifically, has been on my to-do list for two years now...)

jix commented 2 years ago

Just checked this again, and without this PR I get the local variable 'junit_type' referenced before assignment error also for tasks that are expected to pass but have a failed assertion. E.g. if I take docs/examples/quickstart/demo.sby and change demo.sv:16 to assert (counter < 2); to make it fail.

nakengelhardt commented 2 years ago

OK, I've looked into it more and I would prefer a different way of solving this, that incidentally also allows me to easily avoid the traceback above. I'm working on a new PR, but I've just unearthed another bug in the "expect" handling...

nakengelhardt commented 2 years ago

150 is my suggestion for how to do it.