Add missing type unrollings #1677
Conversation
|
Are there any circumstances under which unrolling might be the wrong thing to do? |
Yes, some places actually want to match |
It should always be int.
…holds It should always be int.
src/analyses/base.ml
Outdated
| if Cil.isVoidType t_override then ( | ||
| M.warn ~category:M.Category.Program "Returning a value from a void function"; | ||
| assert false | ||
| ); |
There was a problem hiding this comment.
This is unrelated to the main topic of this PR, but doesn't the assert false cause the program to crash, and the warning before to never be printed? Does not seem to make much sense.
There was a problem hiding this comment.
That might be true indeed if we aren't doing early warnings or such. I'll think about it and perhaps turn it into logging/failwith.
There was a problem hiding this comment.
I just tried triggering this case and couldn't even do it. Apparently CIL already covers it here: https://github.com/goblint/cil/blob/f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f/src/frontc/cabs2cil.ml#L6840-L6843. I think we don't show the CIL warning but CIL removes the returned expression anyway, so Goblint never sees it.
I'll change this to a plain assert without a more specific message because this shouldn't even be triggerable by the user.
| @@ -311,6 +311,7 @@ class addTypeAttributeVisitor = object | |||
|
|
|||
| (*Set arrays with important types for thread analysis to unroll*) | |||
| method! vtype typ = | |||
| (* TODO: reuse predicates in Access module (also handles TNamed correctly) *) | |||
There was a problem hiding this comment.
Should we not do this rather than leave new TODOs in the code base?
There was a problem hiding this comment.
Right now the ones in Access aren't directly suitable for reuse here: what Access considers ignorable isn't exactly what unrolling considers important (e.g. FILE, jmp_buf, etc).
I think this needs a bit bigger refactoring. In particular, what I'd like to have is something like LibraryTypes (but initially at least less DSLy than LibraryFunctions). These are currently unconditional everywhere, but they should also be controlled by lib.activated.
I think recently @karoliineh found something in sv-benchmarks where our Linux kernel-specific overrides trigger on LDV tasks because they use the same names, but actually have stub implementations different from the kernel's. In the specific case we were perhaps imprecise because of it (?) but this is actually accidental task fingerprinting.
Closes #1600. I once started working on it, but never completed it.
PR #1676 independently found two places with missing type unrolling (which are also among the ones found here) that have clear impact on precision. Thus, it would be a good idea to more systematically fix the issue as a preventative measure.
Currently this PR is mostly a scattering of TODOs that still need to be looked at.