Possible issue with pet_scop_get_context generating incorrect context for specific loop case

[Maciej Poliwoda]

Hello,

I’m experiencing a problem with the following loop.
It seems that in this particular case, the pet_scop_extract_from_C_source function (
petScop = pet_scop_extract_from_C_source(ctx, "./work_test.c", NULL);
) produces an incorrect context when calling
isl_set *contextPet = pet_scop_get_context(petScop);.

Based on the obtained contextPet, it is not possible to correctly generate the resulting code.
Could you please take a look at this issue and, if possible, suggest a solution?

Kind regards,
Maciej Poliwoda

Example code:
########

int paired(int, int);
int MAX(int, int);

void foo2(int N, int l, int **M, int *Puu, int **Pbp, double delta) {
#pragma scop
  for (int i = N - 1; i >= 0; i--) {
    for (int j = i + 1; j < N; j++) {
      for (int k = 0; k < j - i - l; k++) {
        M[i][j] = MAX(M[i][j],
                      M[i][k + i - 1] + M[k + i + 1][j - 1] + delta * Pbp[k + i][j])
                  * paired(k + i, j - 1);
      }
      M[i][j] = MAX(M[i][j], M[i][j - 1] + Puu[j - 1]);
    }
  }
#pragma endscop
}


########
Code extraction:
########

petScop = pet_scop_extract_from_C_source(ctx, "./work_test.c", NULL);


Resulting schedule:

S := [N, l] -> {
  S_1[i, j] -> [-i, j, 1, 0] : i >= 0 and i < j < N;
  S_0[i, j, k] -> [-i, j, 0, k] : i >= 0 and i < j < N and 0 <= k < -l - i + j;
};


########
Code generation:
########

isl_set *contextPet = pet_scop_get_context(petScop);
isl_ast_build *ast_build = isl_ast_build_from_context(contextPet);


contextPet is computed as:

contextPet := [N, l] -> {
  : -2147483648 <= N <= 2147483647 and l <= 2147483647 and
    ((N <= 1 and l >= -2147483648) or (N >= 2 and l >= -1 + N))
};


Generating code with:

codegen(S * contextPet);


Produces:

if (N <= 2147483647 && l + 1 >= N && l <= 2147483647)
  for (int c0 = -N + 2; c0 <= 0; c0 += 1)
    for (int c1 = -c0 + 1; c1 < N; c1 += 1)
      S_1(-c0, c1);

########
Issue description:
########

I’m not sure how exactly this contextPet was computed.
In my opinion, it should be derived as follows:

B := [N, l] -> {
  : exists i, j, k :
    (
      i <= N - 1 and i >= 0 and j >= i + 1 and j < N
      and 0 <= i <= 2147483647 and 0 <= j <= 2147483647
      and 0 <= j - 1 <= 2147483647
    )
  or
    (
      0 <= i <= 2147483647 and 0 <= j <= 2147483647
      and 0 <= k + i - 1 <= 2147483647 and 0 <= k + i + 1 <= 2147483647
      and 0 <= j - 1 <= 2147483647 and 0 <= k + i <= 2147483647
      and i <= N - 1 and i >= 0 and j >= i + 1 and j < N
      and k >= 0 and k < j - i - l
    )
};


Which simplifies to:

[N, l] -> { : N >= 2 }

########
Expected code generation:
########

With:

B := [N, l] -> { : N >= 2 };
codegen(S * B);


The resulting code is:

for (int c0 = -N + 2; c0 <= 0; c0 += 1)
  for (int c1 = -c0 + 1; c1 < N; c1 += 1) {
    for (int c3 = 0; c3 < -l + c0 + c1; c3 += 1)
      S_0(-c0, c1, c3);
    S_1(-c0, c1);
  }


########
Verification:
########

S := [N, l] -> {
  S_1[i, j] -> [-i, j, 1, 0] : i >= 0 and i < j < N;
  S_0[i, j, k] -> [-i, j, 0, k] : i >= 0 and i < j < N and 0 <= k < -l - i + j;
};

B := [N, l] -> { : N = 1 and l = 0 };
scan(S * B);

B := [N, l] -> { : N = 2 and l = 0 };
scan(S * B);

B := [N, l] -> { : N = 2 and l = 1 };
scan(S * B);


########
Verification result:
########

[N, l] -> { }
[N, l] -> { S_1[0, 1] -> [0, 1, 1, 0] : N = 2 and l = 0; S_0[0, 1, 0] -> [0, 1, 0, 0] : N = 2 and l = 0 }
[N, l] -> { S_1[0, 1] -> [0, 1, 1, 0] : N = 2 and l = 1 }

########

[Sven Verdoolaege]

On Mon, Oct 20, 2025 at 01:20:05AM -0700, Maciej Poliwoda wrote:
> I’m not sure how exactly this contextPet was computed.

It looks like it is making sure the first statement is _not_ executed
to avoid invalid accesses.

> void foo2(int N, int l, int **M, int *Puu, int **Pbp, double delta) {
> #pragma scop
> for (int i = N - 1; i >= 0; i--) {
> for (int j = i + 1; j < N; j++) {
> for (int k = 0; k < j - i - l; k++) {
> M[i][j] = MAX(M[i][j],
> M[i][k + i - 1] + M[k + i + 1][j - 1] + delta * Pbp[k
> + i][j])

If this statement is ever executed, then it is also executed
for i = 0 and k = 0, resulting in an invalid access M[0][-1].

skimo