[CIL users] Simplifying --dosimplify, continued

[Pavel S. <pav...@gm...>]

As a follow-up to one of my previous patch, here's another patch that 
will make --dosimplify more suitable for generating code, better suited 
for software verification.

The patch adds --no-convert-field-offsets option for --dosimplify 
extension.  This option makes CIL not convert structure field access "x-
>p" to, essentially, "(int*)( (int*)x +  8), where "8" (or any other 
similar number) is a machine-dependent offset of a field relative to the 
beginning of the structure.  However, other memory access 
simplifications still work.

Sample file that had this problem is attached as "mem.c".  Try it as 

cilly.asm.exe --printCilAsIs --domakeCFG --dosimplify --no-convert-
field-offsets mem.c


However, in rare cases, there is a problem with arrays and their 
modifiers.  The option requires CIL to generate temporary variables with 
more complex types than previously, and the resultant code is not always 
compilable.  Consider the following file (volatile_fail.c):

struct M {
  unsigned char volatile   completed[46U] ;
} volatile *m;

int main()
{
  return &m->completed;
}


The result of the conversion is:


struct M {
   unsigned char volatile   completed[46U] ;
};
struct M  volatile  *m  ;
int main(void) 
{
  // Compile error here:
  unsigned char volatile   ( volatile  (*__cil_tmp1))[46U] ;

  __cil_tmp1 = (unsigned char volatile   ( volatile  (*))[46U])m;
  return ((int )__cil_tmp1);
}

So,
1) could anyone give me a hint how to fix this?
2) could this patch be added to upstream nevertheless?  I think that the 
benefits to the verification tools, for which the options is useful, are 
much greater than the very rarely encountered issue with "very volatile" 
structs with array fields.  Besides, the behavior without this command-
line option is retained.

-- 
Pavel Shved
website: http://coldattic.info/
e-mail: pav...@gm...