ddsmt / ddSMT

A delta debugger for SMT benchmarks in SMT-LIB v2.
https://ddsmt.readthedocs.io
Other
50 stars 17 forks source link

Avoid divide-by-zero when parsing an SMT file with no expressions #28

Closed aytey closed 3 years ago

aytey commented 3 years ago

If you try to parse either a file that contains only comments or a file that contains "nonsense" (i.e., no SMTLIB commands), then ddSMT falls over:

(venv) avj@platypus ~/clones/ddSMT/master$ git rev-parse --short HEAD
6997167
(venv) avj@platypus ~/clones/ddSMT/master$ cat comment.smt2
; I'm a comment!
(venv) avj@platypus ~/clones/ddSMT/master$ ./bin/ddsmt -v -v -v -v comment.smt2 moo /bin/false |& tail -n 10
[ddSMT CHAT] pass 5 / 5
[ddSMT INFO] No further simplification found
Traceback (most recent call last):
  File "./bin/ddsmt", line 36, in <module>
    __main__.main()
  File "/home/avj/clones/ddSMT/master/bin/../ddsmt/__main__.py", line 11, in main
    cli.ddsmt_main()
  File "/home/avj/clones/ddSMT/master/bin/../ddsmt/cli.py", line 144, in ddsmt_main
    exprperc = exprcount / nexprs * 100
ZeroDivisionError: division by zero

This PR fixes this such that ddSMT prints inf% if the original input file has no expressions:

(venv) avj@platypus ~/clones/ddSMT/div_zero$ ./bin/ddsmt -v -v -v -v comment.smt2 moo /bin/false |& tail -n 10
[ddSMT INFO]
[ddSMT INFO] runtime:         0.03 s
[ddSMT DEBUG] main process:   0.02 s
[ddSMT INFO] tests:           0
[ddSMT INFO] input file:
[ddSMT INFO]   file size:     17 B
[ddSMT INFO]   s-expressions: 0
[ddSMT INFO] reduced file:
[ddSMT INFO]   file size:     0 B (0.0%)
[ddSMT INFO]   s-expressions: 0 (inf%)

Signed-off-by: Andrew V. Jones andrewvaughanj@gmail.com