search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

Add primitive verdict-based YAML violation witness rejection #1512

Open sim642 opened 2 weeks ago

sim642 commented 2 weeks ago

Closes #1301.

Most of this is just adding YAML witness violation_sequence parsing support and adapting the parsing of locations in YAML witnesses to allow for fields which the updated 2.0 format allows to omit.

The actual rejection part is laughably trivial: do nothing!

  1. If program is correct and we can prove it, we output true, which counts as refutation of violation witness.
  2. If program is correct and we cannot prove it, we output unknown.
  3. If program is incorrect, we output unknown.

Actually using any of the information in the violation sequence is a separate issue. We should be able to kill some paths or refine some values based on that, a la (linear) observer automaton.

TODO

sim642 commented 1 week ago

I tried running this on SV-COMP 2024 YAML violation witnesses (it's extremely difficult to even get them). If I did everything correctly, there are at most 160 (probably even much fewer) tasks with expected true verdict. Among them, only two of CPAchecker's we terminate with unknown. So we cannot reject anything.

Also doing some refinement with violation sequences might allow us to reject witnesses even for tasks with expected verdict false, if the error path cannot lead to the violation. But I'm not very hopeful about that.