search

goblint / analyzer

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

Consider submitting C2PO tests to SV-COMP #1571

Open michael-schwarz opened 2 months ago

michael-schwarz commented 2 months ago

These tests seem to be full of obscure pointer aliasing things. Do we plan to submit these to sv-benchmarks as well? Or is there undefined behavior in some?

It would be very interesting to know how other tools with their approaches cope with these. Or maybe the tests are quite deterministic/small that simple execution/model checking can just decide these?

_Originally posted by @sim642 in https://github.com/goblint/analyzer/pull/1485#discussion_r1711032767_

sim642 commented 2 months ago

This might not yet be publicly announced, but the deadline for new task submission to SV-COMP 2025 should be October 15, 2024. This can be done before #1485 is merged. Do you have plans for this or should I allocate some time and do it?

michael-schwarz commented 2 months ago

We don't have any concrete plans to do this. If you can spare the time to do this, it's probably nice-to-have, though I'm not sure if it needs to be top priority to get them into SV-COMP, especially if we don't activate C-2PO yet this year.

For next year, it might be even better to submit the instrumented programs (maybe only those assertions the basic setting without C-2P0 cannot re-establish).

sim642 commented 2 months ago

I thought it'd be a good way to review the tests at the same time, but already with the first test I realized this would be so much work. It already has so many issues:

  1. Pointer k is uninitialized to get a nondet pointer, but there's no SV-COMP analogue of that (I guess it could also just be malloc though).
  2. Pointer k is dereferenced, so there needs to be an initialized value to be free of UB.
  3. Pointer j is malloced with size sizeof(int)+7 which is weird for an array of int*.
  4. Pointer (j+3) is dereferenced, but it's OOB for sizeof(int)+7.

Basically, getting these to be free of UB (memory safe, everything allocated, everything in bounds, everything initialized), is a lot of work. Without that these cannot go into SV-COMP for their assertions.