Fix crash when constant = bool in diagram

[dranov]

When a model contains something of the form constant = true, there's a crash in const_subst().

Before this commit, in logic.py:const_subst() you would get something like:

BinaryExpr(op='EQUAL', arg1=Id(name='integer_is_decidable', n_new=0,
span=None), arg2=Id(name={(): True}, n_new=0, span=None), span=None)

This would crash with a "TypeError: unhashable type: dict" when executing ans[e.arg2] = e.arg.

I saw this running UPDR on a specification that had a constant of sort bool.

I'm not sure if this is the best way to fix the issue, but it is the work-around I used.

[odedp]

Thank you for submitting this! Can you share a (ideally minimized) example and command line that demonstrates the bug?

[dranov]

Hi @odedp.

On the latest master (commit b38ef57), running:

time mypyvy updr simplified_token.pyv
/usr/bin/python3 /usr/local/bin/mypyvy updr simplified_token.pyv
checking init:
  implies invariant on line 89... ok. (0:00:00.000101)
Traceback (most recent call last):
  File "/usr/local/bin/mypyvy", line 807, in <module>
    main()
  File "/usr/local/bin/mypyvy", line 798, in main
    utils.args.main(s)
  File "/usr/local/bin/mypyvy", line 73, in do_updr
    fs.search()
  File "/home/dranov/src/mypyvy/src/updr.py", line 406, in search
    self.establish_safety()
  File "/home/dranov/src/mypyvy/src/updr.py", line 124, in establish_safety
    self.block(diag_or_expr, frame_no, [(None, diag_or_expr)])
  File "/home/dranov/src/mypyvy/src/updr.py", line 241, in block
    pre_diag = Diagram(cti.as_state(0))
  File "/home/dranov/src/mypyvy/src/logic.py", line 351, in __init__
    self.simplify_consts()
  File "/home/dranov/src/mypyvy/src/logic.py", line 453, in simplify_consts
    subst = self.const_subst()
  File "/home/dranov/src/mypyvy/src/logic.py", line 439, in const_subst
    ans[e.arg2] = e.arg1
  File "<string>", line 3, in __hash__
TypeError: unhashable type: 'dict'

real    0m25.020s
user    0m24.879s

This is the file (rename it to .pyv): simplified_token.txt

It's automatically generated from Ivy, so does not look very nice, but it is valid.

[dranov]

Here's a version that's better to work with:
minimized_simplified_token.txt

It crashes on master, and the fixed branch takes about 20 seconds to find the invariant, which passes mypyvy verify.

[odedp]

Thank you @dranov. I suspect that it can be minimized much further. Ideally into something we can add to our regression tests.

Anyway, @wilcoxjay what do you think about this bug and the proposed fix?