Field on a non-compound errors in SV-COMP SoftwareSystems

[sim642]

In my own run of Goblint on SV-COMP SoftwareSystems category, Goblint crashed with Errormsg.Error exception

Bug: typeOffset: Field on a non-compound

on the following benchmarks:

ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--pcmcia--pcmcia.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--usb--host--r8a66597-hcd.ko-main.cil.out.i
ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--rfc1051.ko-entry_point.cil.out.i
ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--capmode.ko-entry_point.cil.out.i
ldv-linux-3.16-rc1/205_9a_array_safes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--arcnet--arc-rawmode.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--mmc--host--rtsx_pci_sdmmc.ko-entry_point.cil.out.i
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--scsi--megaraid.ko.cil.i
ldv-linux-3.0/module_get_put-drivers-bluetooth-btmrvl.ko.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--isdn--mISDN--l1oip.ko-main.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--mmc--host--vub300.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--host--u132-hcd.ko.cil.i
ldv-validator-v0.8/linux-stable-063f96c-1-144_1a-drivers--mmc--host--vub300.ko.unsigned-entry_point_ldv-val-v0.8.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--message--fusion--mptsas.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-validator-v0.8/linux-stable-063f96c-1-144_2a-drivers--mmc--host--vub300.ko.unsigned-entry_point_ldv-val-v0.8.cil.out.i
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--scsi--advansys.ko.cil.i
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
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--usb--host--isp116x-hcd.ko.cil.i
ldv-linux-3.14/linux-3.14_linux-alloc-spinlock_drivers-net-ethernet-intel-i40e-i40e.cil.i
ldv-linux-3.14/linux-3.14_linux-drivers-clk1_drivers-net-ethernet-intel-i40e-i40e.cil.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--initio.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--scsi--initio.ko-entry_point.cil.out.i
ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--usb--host--max3421-hcd.ko-entry_point.cil.out.i
ldv-validator-v0.8/linux-stable-5fdb450-1-144_1a-drivers--mmc--host--vub300.ko-entry_point_ldv-val-v0.8.cil.out.i
ldv-validator-v0.8/linux-stable-5fdb450-1-144_2a-drivers--mmc--host--vub300.ko-entry_point_ldv-val-v0.8.cil.out.i
ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--net--usb--cdc_mbim.ko-entry_point.cil.out.i
ldv-challenges/linux-3.10-rc1-43_1a-bitvector-drivers--net--ethernet--broadcom--b44.ko--ldv_main0.cil.out.i
ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--memstick--host--jmb38x_ms.ko-entry_point.cil.out.i
ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--net--can--usb--usb_8dev.ko-entry_point.cil.out.i
ldv-commit-tester/m0_drivers-net-b44-ko--114_1a--073676f-1.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point.cil.out.i
ldv-linux-3.14/linux-3.14_linux-kernel-locking-mutex_drivers-net-wireless-libertas-libertas.cil.i
ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--scsi--vmw_pvscsi.ko-entry_point.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-drivers--net--wireless--hostap--hostap.ko-main.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--atm--idt77252.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--tty--n_r3964.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--bluetooth--hci_uart.ko-entry_point.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--isdn--i4l--isdn.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--advansys.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--libfc--libfc.ko-entry_point.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--net--wireless--rndis_wlan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--fusbh200-hcd.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--usb--host--fotg210-hcd.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--usb--host--fotg210-hcd.ko-entry_point.cil.out.i
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--media--dvb-core--dvb-core.ko.cil.i
ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-drivers--net--ethernet--broadcom--b44.ko-entry_point.cil.out.i
ldv-linux-3.0/module_get_put-drivers-scsi-megaraid.ko.cil.out.i
ldv-linux-3.14/linux-3.14_complex_emg_linux-kernel-locking-spinlock_drivers-net-ethernet-dlink-dl2k.cil.i
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--scsi--aacraid--aacraid.ko.cil.i
ldv-validator-v0.8/linux-stable-5742d35-1-136_1a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point_ldv-val-v0.8.cil.out.i
ldv-linux-4.0-rc1-mav/linux-4.0-rc1---drivers--scsi--pmcraid.ko.cil.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--gdm724x--gdmulte.ko-entry_point.cil.out.i
ldv-commit-tester/main3_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa-1.i
ldv-validator-v0.6/linux-stable-5742d35-1-136_1a-drivers--usb--serial--ti_usb_3410_5052.ko-entry_point.cil.out.i
ldv-commit-tester/main3_drivers-staging-usbip-vhci-hcd-ko--132_1a--927c3fa.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-32_7a-drivers--net--wireless--mwl8k.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--net--wireless--mwl8k.ko-entry_point.cil.out.i
ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--usb--host--r8a66597-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i
ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--net--can--usb--esd_usb2.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-08_1a-drivers--net--team--team.ko-entry_point.cil.out.i
ldv-linux-3.12-rc1/linux-3.12-rc1.tar.xz-144_2a-drivers--staging--gdm72xx--gdmwm.ko-entry_point.cil.out.i
ldv-linux-3.16-rc1/205_9a_array_unsafes_linux-3.16-rc1.tar.xz-205_9a-drivers--net--wireless--ath--ath9k--ath9k_htc.ko-entry_point.cil.out.i
ldv-linux-3.16-rc1/43_2a_bitvector_linux-3.16-rc1.tar.xz-43_2a-net--atm--lec.ko-entry_point.cil.out.i
ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--staging--wlan-ng--prism2_usb.ko-entry_point.cil.out.i
ldv-commit-tester/main0_drivers-net-wireless-ath-carl9170-carl9170-ko--32_7a--8a9f335.i
ldv-commit-tester/main0_drivers-net-wireless-ath-carl9170-carl9170-ko--32_7a--8a9f335-1.i

---

The first one at least originates from update_one_addr in Base:

analyzer/src/analyses/base.ml

Line 1066 in 3164939

| None -> Cil.typeOf (Lval(Var x, cil_offset)) in

[michael-schwarz]

For all of these examples, it would be good to extract a minimal example where the problem also occurs and add that to our regression tests.

[sim642]

I think this happens due to the cil_offset there not being a real syntactically valid offset constructed from Goblint's internal offset management. The PR #114 fixes a specific instance of that at least, where previously adding an offset (e.g. -40 constructed from offsetof) to a field offset (e.g. foo.bar) naïvely appended and gave something like foo.bar[-40] instead of just foo. I suppose this sort of weirdness can still happen with other unusual pointer arithmetic on fields.

In #114 I just wrapped my own typeOffset calls with try and made everything optional to quietly ignore this in the new check I added but clearly it's not good that such offsets come about in the first place.

[sim642]

From the first crashing benchmark (ldv-consumption/32_7a_cilled_linux-3.8-rc1-32_7a-drivers--usb--host--isp1362-hcd.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i) I managed to find one basic issue which I added as regression test 29/05: wrapping malloc into a function like ldv_malloc somehow breaks knowing the type of the allocated struct, hence offsets won't work.

When a struct is malloc-ed, its heap variable is initially given a type void:

analyzer/src/cdomains/baseDomain.ml

Lines 52 to 58 in 64250ed

	let get_heap_var loc =
	try Hashtbl.find heap_hash loc
	with Not_found ->
	let name = "(alloc@" ^ loc.file ^ ":" ^ string_of_int loc.line ^ ")" in
	let newvar = Goblintutil.create_var (makeGlobalVar name voidType) in
	Hashtbl.add heap_hash loc newvar;
	newvar

This makes sense because at that point it's not yet known that the variable will hold a struct or which struct. When the result of malloc is cast to the corresponding struct pointer, we refine that type:

analyzer/src/cdomains/valueDomain.ml

Lines 260 to 261 in 64250ed

	| Addr ({ vtype = TVoid _; _} as v, `NoOffset) -> (* we had no information about the type (e.g. malloc), so we add it TODO what about offsets? *)
	Addr ({ v with vtype = t }, `NoOffset)

In the regression test, this refinement does happen, but somehow is forgotten by the time it's necessary to get the rsrc_start field on it, so that will be attempted on void instead. I haven't been able to pinpoint where this gets lost, but I have a theory:
{ v with vtype = t } constructs a new varinfo with the refined type but that varinfo is problematic because it shares vid with the original one. So equality checks on varinfo are defined to just compare the vids so that would be considered equal to the original void-typed version and the refined type could thus easily disappear somewhere.

---

I also added a second regression test 29/06 from that same benchmark which I think models the actual problem but that only arises with exp.widen-context, which automagically fixes the first issue. This change in behavior is not surprising with the varinfo equality issue.

[michael-schwarz]

If you change the computation of the correct type to set in update_one_addr to simply take the type of the AD.t if we can not correctly determine the type of the thing pointed to, it seems to work again.
I guess it can be justified by saying that the variable at this point still has void type and only gets the different type once it is written through this pointer.

      let t = match t_override with
        | Some t -> t
        | None -> try Cil.typeOf (Lval(Var x, cil_offset))
          with _ -> AD.get_type lval
        in

[michael-schwarz]

Sort of related is that one would probably like to treat these ldv_malloc analogous to malloc calls, otherwise we are stuck with only one heap object for all things allocated via ldv_malloc as they all use the same malloc call.

[sim642]

If AD.get_type is the backup, then the natural question would be: why not only use just that all of the time instead of bothering with Cil.typeOf and cil_offset?
Also, it doesn't seem super safe either because it essentially boils down to AD.type_offset which has numerous ways to fail as well. I tried it at some point but it didn't solve 29/06 still if I remember correctly.

Indeed, malloc wrappers really make our heap variables useless. I think ldv_malloc is used a lot in SoftwareSystems so it could be another big source for imprecision for us there.
I'm not sure if making ldv_malloc special is a good idea though. There are different variations of its implementation, some of which explicitly make returning NULL an option to force everyone to consider failing allocations. I haven't yet thought much about this but maybe adding some kind of context into them would keep them separate with less hard-coding.

[michael-schwarz]

If AD.get_type is the backup, then the natural question would be: why not only use just that all of the time instead of bothering with Cil.typeOf and cil_offset?

Requiring a type for VD.update_offset is a quite recent development which was introduced during all the fixups we were doing on the int domains. The motivation there was to support code such as this:

unsigned char a;
if(top) a=7; else a = 12;

signed char x;
unsigned char* y = &x
*y = a;

In this case we want to perform a cast to the correct type of x when writing through the pointer. This was a pattern that appeared quite often in some of the bigger examples.

---

I think there is something to be said for this approach of using the AD.get_type for the case of writing to things where the memory has void type. Actually modifying the vtype of the malloc@.... varinfo not just in the address would be a bit strange anyway: The type of a varinfo should not change throughout the program. But what would we do in cases such as this:

size_t large_enough = // Large enough for both struct t1 and struct t2
void* ptr = malloc();

struct t1* ptr1 = NULL;
struct t2* ptr2 = NULL;

if(top) {
   ptr1 = (struct t1*) ptr;
} else {
   ptr2 = (struct t2*) ptr;
}

[sim642]

One option for the latter example could be something like partitioning the malloc-ed blob value by type. That might also increase the amount of type tracking we'd have to do to know at every access which type partition of the blob to look at.

Or maybe a more hacky version of that idea, where a cast of the malloc-ed variable creates a new varinfo which also has the type in its name and makes the original untyped variable point at the new one.

[michael-schwarz]

For the second example 29/06, I think it is an unrelated issue: We are for some reason trying to set a value of a member of something that has type unsigned_long[0]:

analyzer/tests/regression/29-svcomp/06-isp1362-widen-context.c

Lines 12 to 16 in 8f756ee

	struct usb_hcd {
	resource_size_t rsrc_start ;
	unsigned long hcd_priv[0U] ;
	};

%%% set: (tests/regression/29-svcomp/06-isp1362-widen-context.c:51)
  lval: {&(alloc@tests/regression/29-svcomp/06-isp1362-widen-context.c:28).hcd_priv.data_reg}
  value: {NULL, ?}

Trying to do this is already a bug somewhere in Goblint.

[sim642]

That's not very surprising because that field is used via a cast to struct: ((struct isp1362_hcd *)(& hcd->hcd_priv)).

I'm actually wondering if this program makes any sense to begin with because besides the weird use of unsigned long there, it's an empty array, so no memory would be allocated for the isp1362_hcd struct inside. And that was already the case in the original SV-COMP benchmark I think.

[michael-schwarz]

it's an empty array

It is GCC alternative syntax for flexible array members. So the program might make some sense, if enough memory is allocated for this struct such that there is space for another pointer in it.

My guess would be that the reduced example is undefined behavior on most platforms.

Regardless of that, what we are doing for this case is somehow buggy.