[Question][Hw4] details of the filter function

[AnHaechan]

I have a few questions about filter function at branch instruction.

As far as I'm correct, what we have to do at the instruction br (x<10) label1 label2 is:
(1) filter the input abstract memory to satisfiy x<10 and send to label1 AND
(2) filter the input abstract memory to satisfy x>=10 and send to label2.

In order to filter the input memory with the condition inside branching instruction, in this case, x<10,
we will refine the value for variable x in the input memory, with predicate< 10, by the filter function of current value domain(sign and interval).

Question 1.
Then, what should we do for the case x<y?
Should we refine m(x) w.r.t. < m(y)orm(y)w.r.t.> m(x)` or somehow both?

Question 2.
Should we also consider the case 10<x (that variable is not at LHS)?
I think I should, of course, but just to make it sure...

[hyunsukimsokcho]

Q1. The correct implementation would be refining in both directions. Consider x = Pos or [1, 2], y = Neg or [-3, -2] in your example, and try to come up with expected memory in each then and else branch.

Q2. The answer to Q1 clarifies this.