Speed up verification of C files when many headers/libraries are included.

[sakehl]

With a lot of my Halide/HaliVer examples, VerCors takes more time to process the file than the actual verification of Viper.

One culprit here is that I'm always including a lot of header files, since many might be needed.

VerCors will than use all the definitions in the header files and process them.

I think it might be nice to mark global declarations with "/@library@/" or something similar, telling VerCors to remove these declarations/definitions if they are never used in non-library code. This way we need to do way less checking. See it as a remove dead code pass from a regular compiler.

Even better would be if this code was removed before the parsing stage, since parsing is so slow for these things.

[bobismijnnaam]

Can those header defs be loaded with protobuf, similar to the simplification rules?

An unused-library-code-removal pass would be a good addition. The java frontend could also use this, provided it's implemented as a generic COL thing.

Edit: just an annoying nitpick, but I figured it's worth pointing out:

I think it might be nice to mark global declarations with "/@library@/" or something similar, telling VerCors to remove these declarations/definitions if they are never used in non-library code.

Doing this analysis without parsing (so essentially doing some hand written regex matching) sounds like a bad idea to me... Though I admit parsing is becoming a problem, even for veymont development atm, which only involves pvl definitions...

[sakehl]

Can those header defs be loaded with protobuf, similar to the simplification rules?

Hmm, I'm unsure? The headers are now just plain .h files, which I think clang deals with all the preprocessing stuff? So not really sure.

Doing this analysis without parsing (so essentially doing some hand written regex matching) sounds like a bad idea to me...

Yeah fair. Maybe using (what I think Ömer told us, the company he was visiting suggested?), the parser from clang, to minimize our AST, and then actual parse it?

or maybe, just really investigate how parsing can be improved. :p

[superaxander]

I think what Bob meant is that you could parse those headers on their own and store the resulting AST with the protobuf stuff. Then when you're verifying a file you get rid of the include before passing it to clang and then (assuming there were not #define's in there) you can simply merge the two ASTs before resolution.

[sakehl]

Ah cool thats pretty neat. I think its a good idea to not have defines in headers anyway, although I'm not completely sure if any programs ever depend on those

[sakehl]

But that should at least really speed up the parsing there, and then you can just use the Resolution step to keep any definitions we still need.