[Question][Hw5] Accuracy of hw5 analyzer

[healwon]

Hello.
I'm working with hw5, and I am confused about context-insensitive analysis.
Our analyzer is context-insensitive, so we should design more precise update strategy (as a quiz), as I understand.

Since it is context-insensitive, I think it is hard to be as precise as a context-sensitive one even with the "more precise update strategy". So, I want to know how precise it should be.

For example,

#include "homework.h"

void f(int x) {
  if (x == 10) {
    int y = 10 / x;  // div 1: May the analyzer capture this?
    return;
  } else {
    f(x + 1);
  }
  int k = 5 / x; // div 2: Analyzer should capture this, as seen in example5
  return;
}

int main() {
  void (*fp)(int);
  int i = input();
  fp = f;
  (*fp)(-1);

  return 0;
}

div 1 is actually safe, but my design may capture div 1 as potential division-by-zero. Is it okay?

Always thanks for the great lecture!

[goodtaeeun]

Hi,
At least in this assignment, the term context can be understood as the function. So, by saying the analysis is context-insensitive, it means that when we are analyzing a function body, the analysis does not consider where the function is called.

In your example, the ability to recognize div 1 to be safe is not related to context-sensitivity. It is rather related to the filtering on the variable x.

So, it is not okay for your analyzer to capture div 1 as a potential division-by-zero.
Please let me know if you need more elaboration.

Regards,
Tae Eun.

[healwon]

Oh I was misunderstanding the concepts. Thank you!

[f52985]

I think that the div 1 should be (falsely) reported as a potential division-by-zero in this assignment.

Since the analysis is context insensitive and f is a recursive function, the weak update should be applied to the variable that is allocated in function f.
x, the parameter of function f, therefore should be updated using weak update.
The said filtering is also basically an "updating" the mapped value of variable x in the memory in to a refined value, so the weak update should be applied here too.
Before the filtering (or updating), I think most implementation would map x into an abstract value that contains 0, so even after the filtering (or updating), the 0 should still be there, since weak update in used.

Or we can view it as following:
The actual concrete memory should look like following when we reach div 1:

[
  x @ [*fp] -> -1,
  x @ [*fp, f] -> 0,
  ...,
  x @ [*fp, f, f, f, ..., f] -> 10,
]

(By the way, this memory layout where the domain of memory is a pair of a location and an instance is borrowed from the lecture slide, not the specification document of the homework where the notation of instances is omitted. I think this is kinda related to this issue.)

Then, the sound abstraction of x's should be larger than [-1, 10] since all of integers from -1 and 10 can be possibly a concrete value of x, which means that at the point of div 1, the div-by-0 should be reported.

[KAIST-JongchanPark]

Sorry for wrong answer, we mislook the example code. (we miss the recursive function call of f)

div 1 should be captured as potential division-by-zero when using weak update.

Thanks for correcting our mistake, @f52985 .

Regards,
Jongchan

[healwon]

@f52985 Thank you for your opinion!

However, I am trouble appling weak update in filtering.
Because (in the code) filter doesn't take callgraph as argument, we cannot know whether the updating location is related to recursive function. Is it possible to know function information in filter?

[woojinnn]

I don't get @f52985 's comment saying

The said filtering is also basically an "updating" the mapped value of variable x in the memory in to a refined value, so the weak update should be applied here too.

I think filtering can be(and should be) strong update

---

Oh, I was wrong. weak update would be more appropriate

[KihongHeo]

Interesting discussion. Go ahead.

Let me put only one thing here. We don't have to unnecessarily make our analyzer imprecise. We always have to make our analyzer as precise as possible (while still preserving soundness).
The whole above discussion can be simply summarized to the following question:
If we say x is 10 at div 1, is this unsound? Why? or Why not?

[f52985]

@healwon
That was the exact problem I encountered during the implementation XD.
I think there might be a several workaround for the problem without changing the type signature of the filter function,
and the one I used was to define weak_filter and use it when appropriate.

[healwon]

Thanks for all comments and discussions. I'll close this issue.
I need to think about the soundness more...