cil-project / cil

C Intermediate Language
Other
348 stars 86 forks source link

This pull request solves two minor bugs and a more important one #24

Closed scolin closed 8 years ago

scolin commented 8 years ago

Global variables initializations may refer to function pointers. If the variables appear in several C files to be merged (as declarations and/or definitions), depending on the order in which the merge is done, their initializations may be incorrectly unified.

Please find the attached minimal example with a source to be compiled and a subdirectory (to be passed to the executable) that contains the example. minimal-example.zip Note: the code in the example is not legal C code (it uses variables instead of function pointers), but I think it conveys the idea of the bug better.

The source file uses cilPrinter that displays the vid of the varinfos. When displaying the merged files with this printer, one ends up with:

Preprocessing ../sources/test4/mod2.c
Preprocessing ../sources/test4/mod1.c
Preprocessing ../sources/test4/mod4.c
Preprocessing ../sources/test4/mod3_1_usage.c
Preprocessing ../sources/test4/mod3_2_definition.c
Sort order before merge: mod1.i,mod2.i,mod3_1_usage.i,mod3_2_definition.i,mod4.i
/* Generated by CIL v. 1.7.3 */
/* print_CIL_Input is false */

int const   var1 [570];
int const   var1 [570] =    (int const   )0;
int const   var2 [1141];
int const   var2 [1141] =    (int const   )1;
int table[3] [284];
void doStuff(void) [285]
{ 
  int x [287];

  {
  x[287] = table[284][1];
  return;
}
}
int const   var4 [856];
int table[3] [284] = {      (int )var1[854],      (int )var2[855],      (int )var4[856]};
int const   var4 [856] =    (int const   )2;

One can see that the var1 and var2 in the initialization of table do not have the correct vid.

While this is not legal C code (gcc will not accept it), this is what happens when var1 and var2 are function pointers (in which case it is legal C code).

kerneis commented 8 years ago

Thanks a lot for the patches. They look sane and I'll do my best to review them shortly. Do you think you could come up with tests, ideally added to the test suite, for the first and third one? I'll try and fix the continuous integration in the meantime, it is broken because i haven't updated it for.recent versions of opam.

scolin commented 8 years ago

I think I can indeed write tests for the __asm and the init patches. I'll keep in touch.

kerneis commented 8 years ago

Travis is fixed and tests pass. Please rebase your changes against develop branch and update this PR. Thanks!

kerneis commented 8 years ago

I've cherry-picked the size_t fix, and added a CI build for windows (using https://github.com/fdopen/opam-repository-mingw/). It works, whereas it didn't without your patch, which is nice. Beware that the windows CI does not run the test suite, it merely compiles CIL.

Please ping me once you have updated the two other patches.

scolin commented 8 years ago

I seem to have difficulties coming up with a relevant test for the merge/init problem. I can write legit C files (with an array of function pointers) that show the problem, but the C generated by cilly does not keep the vids hence the problem is not apparent. I next tried to see if there is an extension that would malfunction because of this bug (for instance, the fact that the vids are not unified cause the vaddrof not to be set to true, which might cause a simpiification to eliminate the function that never seems to be called), but I could not find any. Plus, it would make the test depend on both the merge functionality and the extension. Anyway. In the end, the problem is that the cilly-based test infrastructure does not seem to be adapted to such "internal" bugs and thus I have half a mind to augment the test infrastructure with a more unit-test/quickcheck-oriented one. What do you think ?

kerneis commented 8 years ago

My guess would be to run cilly with --strictcheck for the test. If that does not catch the inconsistency (pre-patch), then ideally the consistency checker would be improved to catch it. Pragmatically, I would rather accept your patch with no test than rejecting it because it is too hard to test though.

scolin commented 8 years ago

With --strictcheck the problem is not caught, but the mechanism mostly seem to be there in check.ml (checkInit->checkExp->...). I'll try to find why the consistency checker does not find it and improve it, then.

scolin commented 8 years ago

Hi, I complemented each patch with a test (I tried to put them where they seemed to be the most relevant), and reformulated a commit message so as to be more understandable. So all should be well.

kerneis commented 8 years ago

Merged, thanks again.