search

sosy-lab / sv-benchmarks

Collection of Verification Tasks (MOVED, please follow the link)
https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks
184 stars 169 forks source link

Fix possible undefined behavior and intent of loops/linear_search and loops/linear_sea.ch #1278

Closed sim642 closed 3 years ago

sim642 commented 3 years ago

See issue #1241 for previous discussion, which didn't get the attention it deserves.

Possible undefined behavior

As discussed in #1241, reading malloc-ed memory without initializing it first is possibly undefined behavior, depending on whether to follow the C standard or the GCC implementation. It was also pointed out that there exists precedent for handling it here either way. Clearly there is a lack of consensus in this regard. Since this affects SV-COMP more widely than just these two tasks, it would be great to hear more opinions in the issue and hopefully this PR brings more peoples' attention to it.

This PR adds explicit malloc array initialization to these tasks, avoiding the problem altogether. I believe this change should be made now and thus the two tasks excluded from SV-COMP 2021, because with conflicting past opinions it has so far been unclear what the verifiers can assume about such memory.

Intent of the benchmarks

By adding explicit initialization, the question follows what should the array be initialized to. Initializing elements with __VERIFIER_nondet_int() would most closely match what could be assumed about the memory, if this isn't considered undefined behavior.

However, it was already pointed out that such nondeterministic initialization (explicit or implicit) very likely misses the original intent of the programs, which are searching for the specially inserted middle value 3 from the array, because the same value could've been nondeterministically added to any position. Therefore this PR zero-initializes the array, which makes their logic much more logical and realistic.

And as explicit initialization is required anyway to fix the intent of these anyway, then the possible undefined behavior question shouldn't matter for these tasks. Of course if it is agreed, that this isn't undefined behavior then it might be good to have benchmarks which also check hat but those should probably be separate and more thought-through than having an unrelated loops benchmark, whose intent it never was (the benchmarks used VLAs previously), accidentally depend on it. That would be something for future years when a clear consensus on the issue exists ahead of time.

PhilippWendler commented 3 years ago

These tasks have been submitted by the ESBMC project in 2012 (ddabbf90f66089f39786d410d024a222553d3bad), maybe some of the original authors can respond to what the intent was? @lucasccordeiro?

dbeyer commented 3 years ago

@holznerst approves with calloc, correct?

holznerst commented 3 years ago

@holznerst approves with calloc, correct?

Yes, thanks for implementing @sim642 :)