Worklist algorithm, divide by 0, and widening/narrowing

[SangjunKo]

이름 Your Name

고상준 Sangjun Ko

질문 Question

안녕하세요.

이번 HW4 과제를 하면서 궁금했던 점이 여럿 생겨서 마감 이후에 이렇게 다시 질문드립니다.

질문을 제가 느낀 그대로 전달하고 싶어서 글이 길어진 점 죄송합니다. 질문 요약도 더불어 작성했습니다.

---

1. 할 일 하기 알고리즘(Worklist algorithm)

저는 두 가지 알고리즘 방법을 시도했는데, 이 알고리즘에서 분명 더 개선이 가능할 것 같고, 제가 놓치고 있는 부분이 있는 것 같아서 질문드립니다.

 

1.1) 첫번째 알고리즘

제가 처음에는 run 함수를

한 라벨을 할 일(worklist)에서 뽑기 -> transfer을 통해 메모리 구하기 -> 구한 메모리와 기존의 메모리를 widen/narrow 하기

로 구현하였습니다.

그런데 이렇게 구현하니 narrow단계에서, 여러블럭에서 메모리가 오는 경우 안전성(soundness)을 잃었습니다.
예를 들어, if블럭에서 [0,5]가 오고, else블럭에서 Bot(도달할 수 없는 블럭)가 오면, narrow단계에서 따로따로 계산을 하므로 Bot으로 바꿔버립니다.

<요약>
할 일에 업데이트 된 라벨들을 넣는 방식.
빠르지만 narrow단계에서 작동을 안함.

 

1.2) 두번째 알고리즘

그래서 두번째로는 렉쳐노트 8에 있는 할 일 하기 알고리즘 수식을 그대로 구현하였습니다.

한 라벨을 할 일에서 뽑기 -> 그 라벨로 들어오는 모든 라벨을 transfer하여 메모리를 구하고, 그 메모리들을 모두 join하기
-> join해서 구한 메모리와, 기존의 메모리를 narrow/widen 하기

그런데 문제는, 이렇게 하다보니 라벨의 이동을 역추적해야하고, 방향 그래프도 만들어야 했습니다.

그래서 방향 그래프를 함수에 전달하기 위해, run 함수안에 매개변수 개수를 늘린 새로운 함수를 만들고, 코드가 복잡해졌습니다.

<요약>
할 일에 업데이트 할 라벨들을 넣는 방식.
narrow에서 작동하지만 느리고 구현이 복잡함.

 

그렇게 워크리스트 알고리즘을 만들었더니, 남들보다 낮은 효율성을 보였습니다.

결국 저는 widen에는 첫 번째 방법을, narrow에는 두 번째 방법을 적용하여 효율성을 높이긴 했지만,

코드가 너무 길어지고 복잡해지는 상황이였습니다.

그래서 제 생각에는 아마 첫번째 방법처럼 역추적을 하지 않고 widen과 narrow를 동시에 작동시키는게 가능할 것 같은데,

어떻게 narrow할 때 역추적없이 안전성을 유지할 수 있을지 모르겠습니다.

아니면 번거롭게 두 가지를 나눠서 다른 알고리즘을 적용하는게 맞을까요?

 

[질문 요약]
안전성을 유지하면서, 역추적 없이 할 일 하기 알고리즘을 구현할 수 있나요?

 
 

---

2. 0으로 나누는 가능성이 있으면 Top으로 요약(abstraction)하는 이유

과제 Readme에,

The output of the abstract semantics of div is defined as top when the divisor can be potentially zero.

와 같이 되어있습니다.

 

그런데 여기서 나누기 0의 가능성이 있으면 왜 Top으로 요약하는지 이유가 있을까요?

수학에서는 나누기 0을 하면 양의 무한대 혹은 음의 무한대로 가지만(정확히는 나누는 수가 0에 가까워질수록),

컴퓨터에서는 나누기 0을 하면 런타임 에러를 내놓습니다.

그러면 런타임 에러 이후의 코드들은 모두 도달할 수 없는 곳(unreachable)이 될텐데, 0으로 나눌 때는 Bot으로 요약해야하는거 아닌가요?

 

만약 예를들어, x = [1, 10] / [-2,2]의 경우가 있다고 가정하겠습니다.
그러면 가능한 경우의 수는

 

-2로 나누는 경우 -> [-5, 0]
-1로 나누는 경우 -> [-10, -1]
0으로 나누는 경우 -> 런타임 에러(Bot)
1로 나누는 경우 -> [1, 10]
2로 나누는 경우 -> [0, 5]

 

이고,

이를 join하면 [-10, 10]이 됩니다.

 

결국, 저 [1,10] / [-2, 2]의 상황 이후에, x는 런타임 에러이거나, [-10, 10]입니다. (이 때, 만약 나누기 0을 Bot으로 표현한다면, 둘이 join해서 최종적으로 x -> [-10, 10] 의 정보를 들고 다음 라벨로 넘어갈 것입니다.)

 

그런데, 정적 분석기는 한 곳에서 멈춰서지 않고, 가능한 모든 에러를 한번에 잡아주는게 좋은 정적분석기인데,

나누기 0을 Top으로 요약하게 되면,

[-10, 10]이 아니라 Top으로 요약하게 되버려서 x = [1, 10] / [-2, 2]의 상황이후로 x의 정보를 손실해버리는거 아닌가요?

예를 들어 저 상황 이후에

int z = y / (x + 11);

라는 상황이 오면, [-10, 10]일 때는 x+11이 [1, 21]이 되어 오탐을 안하지만, Top으로 갔을 때는 x+11이 그대로 Top이게 되어 오탐을 하게되지 않나요?

아니면, 혹시 나누기 0을 Top으로 요약해야하는 이유가 있을까요?

 

[질문 요약]
나누기 0의 요약(abstraction)을 Bot으로 정의하면 안되나요?

 
 

---

3. Widen/Narrow가 불필요한 경우

Widen과 Narrow의 목적은 무한한 시간이 걸리는 과정을 유한한 시간안에 끝내는 것입니다.

그렇다면 만약 어떤 원소든간에,

도메인의 상한(Top)까지 유한한 스텝으로 도달할 수 있으면, 굳이 widen을 쓰지 않고 join만 하면 정확도를 올릴 수 있지 않나요?

또한, 도메인의 하한(Bot)까지 유한한 스텝으로 도달할 수 있으면, 굳이 narrow을 쓰지 않고 intersection만 하면 정확도를 올릴 수 있지 않나요?

 

예를 들어, 구간(interval) 도메인은 어떤 원소든 유한한 스텝으로 Bot에 도달할 수 있으므로,
굳이 narrow을 쓰지 않고 intersection을 쓰는게 더 좋은 정확도를 얻을 수 있는거 아닌가요?

 

[질문 요약]
도메인의 상한(Top)또는 하한(Bot)까지 유한 번의 연산을 통해 도달할 수 있으면,
widen과 narrow가 필요한가요?

 
 

긴 글 읽어주셔서 감사합니다!

번역본 Translated Version

Hello.

I have several questions that arose while working on the HW4 assignment, so I am asking them now after the deadline.

I apologize for the length of the text, as I wanted to convey the questions exactly as I felt them. I have also included a summary for each question.

---

1. Worklist algorithm

I tried two algorithmic methods, and I am asking because it seems that further improvement is definitely possible and there are parts I might be missing.

 

1.1) First Algorithm

Initially, I implemented the run function as follows:

Pick a label from the worklist -> obtain memory through transfer -> widen/narrow the obtained memory with the existing memory.

However, with this implementation, I lost soundness during the narrowing phase when memory comes from multiple blocks. For example, if [0, 5] comes from an if block and Bot (unreachable block) comes from an else block, the narrowing phase calculates them separately and mistakenly changes it to Bot.

A method of putting updated labels into the worklist. It is fast, but it does not work during the **narrowing** phase.

 

1.2) Second Algorithm

So, for the second attempt, I implemented the worklist algorithm formula exactly as it appears in Lecture Note 8.

Pick a label from the worklist -> transfer all labels coming into that label to obtain memories, and join all those memories -> narrow/widen the joined memory with the existing memory.

The problem, however, was that this required backtracing label movements and creating a directed graph. Consequently, to pass the directed graph to the function, I had to create a new function inside the run function with an increased number of parameters, making the code complex.

A method of putting labels to be updated into the worklist. It works in **narrowing**, but it is slow and the implementation is complex.

 

After creating the worklist algorithm that way, it showed lower efficiency compared to others.

In the end, I improved efficiency by applying the first method to widen and the second method to narrow, but the code was becoming too long and complicated.

Therefore, I think it might be possible to operate widen and narrow simultaneously without backtracing like the first method, but I do not know how to maintain soundness when narrowing without backtracing. Or is it correct to apply different algorithms by separating the two inconveniently?

 

[Question Summary]
Is it possible to implement a worklist algorithm without backtracing while maintaining soundness?

 
 

---

2. Reason for abstracting to Top when there is a possibility of dividing by zero

In the assignment Readme:

"The output of the abstract semantics of div is defined as top when the divisor can be potentially zero."

It is stated as above.

 

However, is there a reason why it is abstracted to $Top$ when there is a possibility of dividing by zero?

In mathematics, dividing by zero leads to positive or negative infinity, but in computers, dividing by zero results in a runtime error. Then, wouldn't all the code after the runtime error become unreachable, so it should be abstracted as $Bot$ when dividing by zero?

 

Suppose, for example, there is a case of $x = [1, 10] / [-2, 2]$. Then the possible cases are:

 

Dividing by -2 -> [-5, 0]
Dividing by -1 -> [-10, -1]
Dividing by 0 -> Runtime Error ($Bot$)
Dividing by 1 -> [1, 10]
Dividing by 2 -> [0, 5]

 

And joining them results in [-10, 10].

 

Ultimately, after that situation of $x = [1, 10] / [-2, 2]$, $x$ is either a runtime error or [-10, 10]. (At this time, if dividing by zero is expressed as $Bot$, the two will join and finally move to the next label with the information of $x \rightarrow [-10, 10]$.)

 

However, a good static analyzer is one that catches all possible errors at once without stopping at one place. If dividing by zero is abstracted to $Top$:

Instead of [-10, 10], it is abstracted to $Top$, so isn't the information of $x$ lost after the situation $x = [1, 10] / [-2, 2]$?

For example, if a situation like "int z = y / (x + 11);" comes after that: In the case of [-10, 10], $x + 11$ becomes [1, 21], so no false positive occurs. But when it goes to $Top$, $x + 11$ remains $Top$, causing a false positive.

Is there a reason why dividing by zero must be abstracted to $Top$?

 

[Question Summary]
Can't the abstraction of dividing by zero be defined as $Bot$?

 
 

---

3. When Widen/Narrow is unnecessary

The purpose of Widen and Narrow is to end a process that takes infinite time within a finite time.

If that is the case, if any element can reach the upper bound (Top) of the domain in finite steps, wouldn't using only join instead of widen improve accuracy?

Also, if it can reach the lower bound (Bot) of the domain in finite steps, wouldn't using only intersection instead of narrow improve accuracy?

 

For example, since the interval domain can reach $Bot$ in finite steps for any element, wouldn't using intersection instead of narrow provide better accuracy?

 

[Question Summary]
If the upper bound (Top) or lower bound (Bot) of a domain can be reached through a finite number of operations, are widen and narrow necessary?

 
 

Thank you for reading this long post!

[KihongHeo]

상준,
항상 새벽에 좋은 질문이 많이 떠오르나 보군요. 멋집니다.

1. 좋은 관찰인데요. 좀 더 깔끔하게 할 방법이 있지 않을까요? 다음 숙제도 이전 숙제의 확장판이니 한번 생각해보세요. 최적화와 디버깅 과정이야말로 우리가 배운 것을 뼈에 아로새기는 소중한 시간입니다. 교수나 AI에게 함부로 빼앗기지 마시길 바랍니다.

2. 이것도 좋은 지적인데요. 당연히 이론적으로는 둘 다 안전하지요. 정답은 없고 실용성에 따라서 선택하기 나름입니다. 숙제 문서에는 예전의 유산이 남아있어서 그렇게 써놓은 것을 미처 고치지 못했네요. 아래와 같은 코드를 보면. 2번줄에서 프로그램이 죽고 3번줄 코드가 실행되지 않는 상황을 상준씨처럼 정확히 분석하는 것도 옳습니다. 그때는 2번 줄에만 알람이 나오겠네요. 하지만 실제 현장에서는 3번줄도 함께 보고하는 것이 효율적일 때도 있겠지요. 개발자들이 한 번에 고칠 수도 있으니까요. 그런 실용적인 이유이고, 이론적으로는 상준씨의 해석이 맞습니다.

x = 0;
y = 1 / x;    
z = 1 /z;

3. 이 질문은 재미있어보이는데 제가 완벽히 이해를 못했네요. 구간 도메인은 높이가 무한한데 어떻게 항상 유한하게 목표에 도달할 수 있는지? 월요일 수업 마치고 이야기해볼까요?

---

Sangjun,

It seems you often come up with good questions late at night. Impressive.

1. That’s a very good observation. Do you think there might be a cleaner way to approach it? The next assignment is also an extension of the previous one, so it would be worth thinking further about it. The process of optimization and debugging is precisely the valuable time when what we’ve learned truly sinks in. I hope you don’t give that away too easily to professors or AI.

2. This is also a good point. Theoretically, both approaches are of course sound. There isn’t a single correct answer—it depends on practicality. The assignment document still contains some legacy wording that I didn’t get a chance to revise. Looking at the code below, your analysis is perfectly valid: the program crashes on line 2, so line 3 is never executed, and only line 2 would raise an alarm. However, in practice, it can sometimes be more efficient to report line 3 as well, since developers may be able to fix multiple issues at once. So this is a practical consideration; theoretically, your interpretation is correct.

x = 0;
y = 1 / x;    
z = 1 / z;

3. This question seems interesting, but I don’t think I fully understood it. If the interval domain has infinite height, how can it always reach a finite target? Shall we talk about it after Monday’s class?

[SangjunKo]

답변 감사합니다!
1번은 계속 틈틈히 생각해보겠습니다! 3번은 월요일에 수업끝나고 질문 다시 드리겠습니다!

2번은
나누기 0의 결과값을 도달 불가능한 곳으로 처리하면 한번에 많은 알람을 내놓지 못하네요.
그래서 생각해봤는데,

1. 오로지 0으로 나누는 경우밖에 없는경우(즉, [0,0]으로 나누는 경우)에는 나누기 결과값을 Top으로 두고,
2. 0으로 나누는 경우를 포함하는 경우(예시로, [-2,2]로 나누는 경우)에는 나누는 값에서 0을 제거하고 나누기 결과값을 구하는 것 어떤가요?

---

예시)
[2, 4] / [0,0] = Top

[2, 4] / [-2, 2]
= [2, 4] / [-2, -1] join [2, 4] / [1, 2]
= [-4, -1] join [1, 4]
= [-4, 4]

---

이러면,

1. 나누기 0이 나올 때 도달 불가능한 곳이 되는게 아니라 멈추지 않고 뒤의 코드까지 분석할 수 있으며,
2. 0이 아닌 다른 수로 나눌 가능성이 있는 경우에, 나눈 값들의 정보를 보존할 수 있습니다. 위의 [2, 4]/[-2,2] 예시처럼요.

---

Thank you for the answer!
I will keep thinking about #1 whenever I have a moment. For #3, I will ask you again on Monday after my class ends.

Regarding #2,
Treating the result of division by zero as "unreachable" prevents the system from generating multiple alarms at once. So, I’ve been thinking about this:

1. In cases where division is performed only by zero (i.e., dividing by $[0, 0]$), the result should be set to Top.
2. In cases that include division by zero (e.g., dividing by $[-2, 2]$), how about removing zero from the divisor before calculating the result?

---

Example)
$[2, 4] / [0, 0] = \text{Top}$

$[2, 4] / [-2, 2]$
$= [2, 4] / [-2, -1] \text{ join } [2, 4] / [1, 2]$
$= [-4, -1] \text{ join } [1, 4]$
$= [-4, 4]$

---

By doing this:

1. When division by zero occurs, it won't become unreachable; instead, the analysis can continue through the rest of the code without stopping.
2. In cases where there is a possibility of dividing by a non-zero number, we can preserve the information of the divided values, as shown in the $[2, 4] / [-2, 2]$ example above.

[KihongHeo]

2번: 상황에 따라 그렇게 해도 됩니다. 그 때부터는 이론의 영역이 아니라 실전 영역입니다. 정답이란 없고 쓰는 사람이 편하게, 용도에 맞게 정의하면 되겠지요. 중요한 것은 여러분들이 중요한 선택지를 주먹구구로 설계하는 것이 아니라 근본 원리를 이해하고 알맞게 설계하는 것입니다. 그게 수업을 통해 전하고 싶은 내용이니다.

3번: 아까 상준씨의 질문에 따르면, 아래와 같이 좁히기(narrowing)을 정의하면 안되냐 하는 것이었지요?

$[a,b] \triangle [c,d] = [(a = -\infty? c:a), d]$

문제가 있어보이는데... 한 번 반례를 찾아보세요. 혹은 안전함을 증명해보거나. 좋은 연습 문제입니다.

---

2:
It is fine to do so depending on the situation. From that point on, it is no longer a matter of theory but of practice. There is no single correct answer—you can define it in a way that is convenient and suited to your purpose. What matters is that you do not design important choices in an ad hoc manner, but rather understand the underlying principles and design them appropriately. That is what this course aims to convey.

According to Sangjun’s earlier question, you were asking whether narrowing could be defined as follows:

$[a,b] \triangle [c,d] = [(a = -\infty ? c : a), d]$

This seems problematic… Try to find a counterexample. Alternatively, try to prove its soundness. It would be a good exercise.

[SangjunKo]

정확히는
$[a, b]\triangle[c, d] = [c, d]$
로 정의하면 안되는지 묻는 것이었습니다.

생각해봤는데
$[-\infty, 0], [-\infty, -1], [-\infty, -2], ... $

이런 반례가 있을 수 있네요..

이 체인은 아무리 좁히기(narrowing)로 연산을 해도 무한한 체인이 되네요.

체인은 항상 작아지는(decreasing) 체인이고, 가장 작은 원소는 $Bot$이기 때문에, 모든 체인이 유한한 시간내에 $Bot$에 도달 할 수 있다고 착각했었습니다.

또한, $x\triangle y$에서 $y$에는 $\infty$를 포함한 구간이 오지 않을거라고 무의식적으로 생각했었네요.

감사합니다!

[KihongHeo]

맞습니다. 바로 그것 때문에 안되지요. 해당 문제를 일으키는 C 프로그램도 한 번 만들어보세요.

[SangjunKo]

게속 고민해봤는데 생각보다 저 반례를 나타내는 C 프로그램 만들기가 어렵네요...
조건문에서 작아지는 필터링(filtering)을 무한히 반복해서 줄여나가야 할 것 같은데, 무한히 반복하려면 또 루프가 필요하니 필터링에 필요한 값들이 join이 되고, 그러면 필터링이 작아지지는 않아서 어려운 것 같습니다.
좀 더 오래 고민해보고 생각이 나면 공유해보겠습니다..!