Mismatch between full and field insensitive alias analysis

[hernanponcedeleon]

With the full alias analysis, we return PASS for this SVCOMP benchmark (the expected result is FALSE according to the competition).

However, there are a bunch of warnings coming from the analysis

[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 101:r12 = load(*bv64 101:r11) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5791
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6369 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933 -> is_device_dma_capable @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5865
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 191:r47 = load(*bv64 192:r21 + bv64(8)) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5914
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_free_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6413
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 90:r37 = load(*bv64 91:r21) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5871
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6359 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 98:r48 = load(*bv64 99:r21) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5879
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6369 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 98:r37 = load(*bv64 99:r21) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5871
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6369 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 201:r47 = load(*bv64 202:r21 + bv64(8)) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5914
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_free_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6418
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 201:r53 = load(*bv64 202:r21 + bv64(8)) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5918
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_free_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6418
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 93:r12 = load(*bv64 93:r11) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5791
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6359 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933 -> is_device_dma_capable @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5865
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 90:r48 = load(*bv64 91:r21) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5879
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6359 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933
[09.05.2025] 19:53:25 �[33m[WARN]�[m InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 191:r53 = load(*bv64 192:r21 + bv64(8)) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5918
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_free_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6413

so I tried to run the field insensitive one. Now we report (it takes ~17min) an invalid function pointer

===== Program specification violation found =====
        E479:   ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> dma_zalloc_coherent @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6359 -> dma_alloc_attrs @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5933 -> @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#5879: Invalid function pointer
=================================================

Even in this case we have several warning related to desvirtualisations

[09.05.2025] 19:09:40 [WARN] NaiveDevirtualisation.devirtualise - Cannot resolve dynamic call "call bv64 r53(bv64 r54, bv32 r55, bv64 r56, bv64 r57, bv64 r58)", no matching functions found.
[09.05.2025] 19:09:40 [WARN] NaiveDevirtualisation.devirtualise - Cannot resolve dynamic call "bv64 r54 <- call bv64 r48(bv64 r49, bv32 r50, bv64 r51, bv32 r52, bv64 r53)", no matching functions found.
[09.05.2025] 19:09:40 [WARN] NaiveDevirtualisation.devirtualise - Cannot resolve dynamic call "call bv64 r1()", no matching functions found.

but the fact that both analysis result in different results shows that we have a problem.

[ThomasHaas]

What is the reason for the expected result according to SVCOMP?
The error we report looks fine to me: it seems the benchmark accesses a function pointer stored in an externally defined struct variable. This variable is never assigned to as far as I can see, and that is why devirtualization will not find any matching call targets (the call target is a function that is not defined in the program).
Seeing that the program accesses external memory like that, I wouldn't be surprised if it also uses pointers to external memory which the alias analysis will deem to be problematic.

I believe we do not handle code like this:

extern int* extPtr;
// ...
*extPtr = 42;
int r = *extPtr;

We probably need to allocate a memory object for the external pointer for otherwise it will point into NULL and/or a random unallocated address. The more imprecise alias analysis just hides the fact that we essentially have UB in the parsed program.

[hernanponcedeleon]

What is the reason for the expected result according to SVCOMP?

There is no description about why the assertion should fail. The benchmark was submitted by the CPALockator team and it seems that historically (I checked until 2019), that was the only tool that was able to find the bug. I strongly believe they just used their tool to come up with the expected result.

The error we report looks fine to me: it seems the benchmark accesses a function pointer stored in an externally defined struct variable.

You are referring to the case where we hit this branch before calling the function here, right?

[ThomasHaas]

Yes, I think the problem was around there.

[xeren]

The other analyses also have empty pointer sets. With the changes in #890, I get:

[16.05.2025] 18:04:24 [INFO] AliasAnalysis.fromConfig - Selected alias analysis: FIELD_INSENSITIVE
[16.05.2025] 18:04:29 [WARN] AndersenAliasAnalysis.processResults - Empty pointer set for store(*bv64 119:r7, bv32 110:r36) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7656
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> ldv_register_netdev_71 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6385 -> ldv_emg_register_netdev @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#8037 -> ldv_register_netdev_open_7_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7724 -> w83977af_net_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#8009 -> ldv_request_irq_75 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7357 -> ldv_emg_request_irq @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#8077 -> ldv_dispatch_irq_register_8_3 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7770
[16.05.2025] 18:04:29 [WARN] AndersenAliasAnalysis.processResults - Empty pointer set for store(*bv64 173:r7, bv64 DUMMY_REG#188) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7676
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> ldv_register_netdev_71 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6385 -> ldv_emg_register_netdev @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#8037 -> ldv_dispatch_register_7_4 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7731
[16.05.2025] 18:04:29 [WARN] AndersenAliasAnalysis.processResults - Empty pointer set for bv32 r18 = load(*bv64 r0) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7862
Context: T2:ldv_interrupt_scenario_2
[16.05.2025] 18:04:29 [WARN] AndersenAliasAnalysis.processResults - Empty pointer set for bv64 r22 = load(*bv64 r0) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7937
Context: T3:ldv_random_allocationless_scenario_3
[16.05.2025] 18:04:29 [INFO] AliasAnalysis.fromConfig - Finished alias analysis in 4.644 secs

[16.05.2025] 18:05:52 [INFO] AliasAnalysis.fromConfig - Selected alias analysis: FIELD_SENSITIVE
[16.05.2025] 18:05:52 [WARN] FieldSensitiveAndersen.processResults - Empty pointer set for store(*bv64 84:r4 + bv64(220) + bv64(8), bv32 3:r10) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6348
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249
[16.05.2025] 18:05:52 [WARN] FieldSensitiveAndersen.processResults - Empty pointer set for store(*bv64 84:r4 + bv64(220) + bv64(24), bv32 3:r14) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6349
Context: T1:ldv_insmod_4 -> ldv_insmod_w83977af_init_4_6 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7807 -> w83977af_init @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7840 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249 -> w83977af_open @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#6249
... (425 more)
[16.05.2025] 18:05:52 [WARN] FieldSensitiveAndersen.processResults - Empty pointer set for bv32 202:r48 = load(*bv64 131:r4 + bv64(344)) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7317
Context: T3:ldv_random_allocationless_scenario_3 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7946 -> ldv_random_allocationless_scenario_callback_3_3 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7965 -> w83977af_net_ioctl @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7988 -> w83977af_is_receiving @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7547
[16.05.2025] 18:05:52 [WARN] FieldSensitiveAndersen.processResults - Empty pointer set for store(*bv64 4:r7 + bv64(16), bv32 DUMMY_REG#427) @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7548
Context: T3:ldv_random_allocationless_scenario_3 -> Iter#2 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7946 -> ldv_random_allocationless_scenario_callback_3_3 @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7965 -> w83977af_net_ioctl @linux-3.14--drivers--net--irda--w83977af_ir.ko.cil.i#7988
[16.05.2025] 18:05:52 [INFO] AliasAnalysis.fromConfig - Finished alias analysis in 0.290 secs

AndersenAliasAnalysis has several points, where the pointer set is set to maxAddressSet. This explains why AndersenAliasAnalysis has less warnings: it assigns maxAddressSet eagerly and frequently. It does not explain, why you don't find the bug with the other analyses.