Limiting casts: No cast on read from a variable

[michael-schwarz]

Following up on all of these discussion with casting for writes through pointers of different types, I took a look at the standard (see Slack).

The resulting idea is casting to the pointed-to type on writes via pointers to memory that has not been dynamically allocated, and casting on reads for dynamically allocated memory.

I will have to test if this causes #119 to resurface. To this end, if we check that Cil.typeOfLval is only called on lvals stemming from the C-program, we should be good. I'll also run the tests that showed #119 again.

This a a prerequisite for merging #145 (and also #137 iirc). It will require changes to #121 such that values of two different ikinds can once again be joined, yielding top.

[michael-schwarz]

Still happens for:

• c/ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--scsi--megaraid.ko.cil.i:19023
• c/ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--ethernet--chelsio--cxgb4--cxgb4.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i:25590
• c/ldv-linux-3.14/linux-3.14_linux-alloc-spinlock_drivers-net-ethernet-intel-i40e-i40e.cil.i:46485
• c/ldv-linux-3.14/linux-3.14_linux-drivers-clk1_drivers-net-ethernet-intel-i40e-i40e.cil.i

[michael-schwarz]

One of the failing ones is due to this pattern:

#include<stdio.h>
struct __anonstruct_mbox_t_232 {
   int one;
   int two;
};
typedef struct __anonstruct_mbox_t_232 mbox_t;

int main(void) {
    unsigned char raw_mbox[15U];
    mbox_t *mbox ;
    mbox = (mbox_t *)(& raw_mbox);
    memset((void *)(& mbox->one), 0, 15UL);
}

[sim642]

One case we looked at in #119 did something similar: #119 (comment). Using an array of a primitive type always cast to some struct.

[michael-schwarz]

I am very tempted to do this on a best-effort base:

let is_heap_var = match a (Q.IsHeapVar x) with `Bool(true) -> true | _ -> false in
if is_heap_var then
      (* the vtype of heap vars will be TVoid, so we need to trust the pointer we *)
      (* got to this to be of the right type *)
      (* i.e. use the static type of the pointer here *)
      lval_type
else
     try
        Cil.typeOfLval (Var x, cil_offset)
      with _ ->
         lval_type

So we would go with the type of the lval for the case of dynamically allocated memory. If memory is not dynamically allocated, we try to get the right type for the thing we are writing to. If we can't do this, we stick with the type of lval. If it matches the type that was declared for the variable, we are lucky. Otherwise if we are doing some weird things we will have a type mismatch in the ValueDomain and go to supertop.

[sim642]

I'm wondering if it's be a good idea to make the with case output a warning or something to make it clear later that we made some assumption there.

[michael-schwarz]

I'm wondering if it's be a good idea to make the with case output a warning or something to make it clear later that we made some assumption there.

Yes, good idea! Feel free to add, or I can do it tomorrow morning.