#135 Legal, but large, static arrays can fail.

Bug
closed
nobody
5
2013-03-21
2013-02-15
Jim Grundy
No

We've encounterd embedded programs that carve out large static arrays ... and they compile and run correctly, but CIL can't process them because the array's are too big.

In particular, CIL appears to use an OCaml int for an array size, but since OCaml int's are 1) signed 2) 1-bit shorter than machine ints to facilitate fast garbage collection; it is possible - and we do - have arrays with a size that is bigger than can be represented with an OCaml int.

Natrually this is a problem in practice only on 32-bit builds, but since all the pre-combiled Windows OCaml builds are 32-bit the problem occurs.

I believe this to be the cause because if I set the size to be one byte smaller than the largest 2s complement number representable in 31 bits it works.

Now, "morally", CIL should be able to process any C file that the compiler can process - but on a 32-bit machine this does break down here. I expect the right thing to do would be to modify CIL to use Nativeint library for storying array sizes.

Discussion

  • Gabriel Kerneis

    Gabriel Kerneis - 2013-02-15

    Since CIL 1.7 (I think), length of arrays is stored as a CInt64 when it is known explicitely. However, Cil.lenOfArray converts it to int (Cil.bitsSizeOf also has a similar behaviour, see bug 1641570). What are you trying to do and how does CIL fail exactly when you process these programs? Could you post a (script to generate) an example program?

     
  • Gabriel Kerneis

    Gabriel Kerneis - 2013-02-15

    I meant CIL 1.4, 1.7 does not even exist...

     
  • Jim Grundy

    Jim Grundy - 2013-02-15

    Hi Gabriel

    We're doing a source-to-source transform using Cil as a library. The error we are getting is:

    Length of array is too large

    Which looks like it comes from frontc/cabs2cil.ml/doType

    I'm not sure what's going on here ... but my guess is that it is tryng to compute the size of the array to record it as an attirbute, but the atributes use OCaml ints rather than 64-bit ints so it won't fit.

    The example program is just this - run with a 32-bit OCaml build on a 64-bit Windows machine.

    char big_array[1073741824];

    int main () {
    return 0;
    }

    All the best

    Jim

     
  • Gabriel Kerneis

    Gabriel Kerneis - 2013-02-15

    OK, Jim. I wonder if this is not some legacy check, and everything else (except lenOfArray and bitsSizeOf et al.) woud work correctly now. Could you try the stupid following patch, please?

    Many thanks,
    Gabriel

    --- a/src/frontc/cabs2cil.ml
    +++ b/src/frontc/cabs2cil.ml
    @@ -2839,7 +2839,7 @@ and doType (nameortype: attributeClass) (* This is AttrName if we are doing
    let size = mul_cilint elems (cilint_of_int elsz) in
    begin
    try ignore(int_of_cilint size)
    - with _ -> E.s (error "Length of array is too large")
    + with _ -> ignore (warn "Length of array is too large")
    end
    | l ->
    if isConstant l then

     
  • Jim Grundy

    Jim Grundy - 2013-02-15

    Thanks ... will try, but I'm about to get on a plane ... so it may take me 1.5 weeks :-(. I will try to get someone to try for me while I'm out.

     
  • Comment has been marked as spam. 
    Undo

    You can see all pending comments posted by this user  here

    Anonymous - 2013-02-21

    Hi Gabriel,

    Jim Grundy has asked me to check the patch you sent for cabs2cil.ml,
    and seems to be working as expected: those messages are sent out as warnings instead of errors.

    Thanks!

    Eran Talmor

     
    Last edit: Anonymous 2013-11-26
  • Gabriel Kerneis

    Gabriel Kerneis - 2013-03-21
    • status: open --> closed
     
  • Gabriel Kerneis

    Gabriel Kerneis - 2013-03-21

    Thanks for the report, Jim. This should be fixed in the repo now.

     

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks