Question about `__set_array_length()` builtin

[cdisselkoen]

Not an issue per se, just a question. (It seems GitHub issues are the way to ask questions about Infer? Is there a better way?)

I'm wondering which analyses the __set_array_length() builtin has an effect on. Clearly it affects bufferoverrun, but from looking at the Infer source, it seems it also has an effect on biabduction? I haven't been able to easily come up with any test case of C code where adding a __set_array_length() annotation changes biabduction's report for that code. Do you know of such an example? Or is __set_array_length() intended for only the bufferoverrun checker?

[jvillard]

Hi @cdisselkoen, thanks for your question. GitHub is our only place for questions at the moment so you were right to ask here.

__set_array_length affects bufferoverrun and biabduction, as you noted. It's an internal function name used mainly in our clang frontend to translate some array operations, and in biabduction's models, written in source code, e.g. https://github.com/facebook/infer/blob/50c3f0ba64236ed61550a731daac4fefde79dea6/infer/models/c/src/glib.c#L38

It's supposed to tell the analysis of the length of the array (though as you noted not many analyses care about that). What have you tried?

[cdisselkoen]

I guess it's a case of "have hammer, looking for nail". We have an analysis which can add __set_array_length() (and some other assumptions) to C code and are wondering if there are cases where this would help Infer.

Below are two examples we found, where Infer gives a false positive and false negative respectively. Although the examples use arrays, the __set_array_length() annotation doesn't change Infer's behavior in either case. Honestly, the array length may not matter for these examples; which brings us back to the original question, are there any examples out there where __set_array_length() actually does change biabduction's behavior.

As a strawman, if we replaced biabduction's implementation of __set_array_length() here with a no-op, would any Infer unit tests fail? We were going to check this ourselves but ran into #1473.

Example 1 - Infer gives false positive (the code path with the violation is actually unreachable):

int foo(int* arr) {
  for (unsigned i = 0; i < 12; i++) {
    arr[i] = 76;
  }
  if (arr[0] == 76) {
    return 0;
  } else {
    int* ptr = NULL;
    return *ptr;
  }
}

In this example, if we replace the loop with the single line arr[0] = 76;, Infer correctly deduces that the path with the violation is unreachable, and there is no false positive.

Example 2 - Infer gives false negative (this function performs a NULL dereference):

int bar(int** arr) {
  for (unsigned i = 0; i < 12; i++) {
    arr[i] = NULL;
  }
  return *(arr[0]);
}

In this example, if we change the loop condition to i < 1, Infer correctly finds the violation, but at i < 2, it does not.