Termination check no longer working with some loops

[xfoukas]

Hi,

I have written the following example that contains a simple for loop:

typedef unsigned char uint8_t;
typedef unsigned int uint32_t;

typedef struct bpf_map_def {
    uint32_t type;
    uint32_t key_size;
    uint32_t value_size;
    uint32_t max_entries;
    uint32_t map_flags;
    uint32_t inner_map_idx;
    uint32_t numa_node;
} bpf_map_def_t;
#define BPF_MAP_TYPE_ARRAY 2

#define ARRAY_LENGTH 16

typedef struct example_array {
  int cnt[ARRAY_LENGTH];
} t_example_array;

__attribute__((section("maps"), used))
bpf_map_def_t map =
  {.type = BPF_MAP_TYPE_ARRAY,
   .key_size = sizeof(int),
   .value_size = sizeof(t_example_array),
   .max_entries = 1};

static void* (*bpf_map_lookup_elem)(bpf_map_def_t* map, void* key) = (void*) 1;

int
foo(void* ctx)
{
    uint8_t index;
    int key = 0;

    t_example_array *example;
    example = (t_example_array *)bpf_map_lookup_elem(&map, &key);
    if (!example)
      return 0;

#pragma nounroll
    for (index = 0; index < ARRAY_LENGTH; index++)
      example->cnt[0] = index;

    return 0;
}

It produces the following code:

       0:       r6 = 0
       1:       *(u32 *)(r10 - 4) = r6
       2:       r2 = r10
       3:       r2 += -4
       4:       r1 = map_fd 1
       6:       r0 = map_lookup_elem:1(map_fd r1, map_key r2)
       7:       if r0 == 0 goto +9 <17>
       8:       r1 = *(u32 *)(r0 + 0)
       9:       r2 = r1
      10:       r1 = r6
      11:       r6 += 1
      12:       r3 = r6
      13:       r3 <<= 32
      14:       r3 >>= 32
      15:       if r3 != 17 goto -7 <9>
      16:       *(u32 *)(r0 + 0) = r2
      17:       r0 = 0
      18:       exit
map 0:(original_fd = 1, inner_map_fd = 1, type = 2, max_entries = 1, value_size = 64, key_size = 4)

The example passes verification, but when I add the --termination flag, it fails with the error:

Could not prove termination on join into: 9, 17,
Program terminates within 2147483647 instructions
0,0.002813,4432

However, if I try the same with an older commit, like 03285310ed91f1d257d4fbdf9f6d7f4b54229339, the termination check succeeds and I get the following message:

Program terminates within 78 instructions
1,0.003311,4396

I noticed that this happens now with all the examples that I have tried, which do not have unrolled loops and which used to pass termination checks in the past.
Is this expected?

[elazarg]

The reason is likely #441

[elazarg]

Closing as duplicate of #441