[Question][Paper presentation] Alive2 : domain of values about is661-advanced-software-security HOT 2 CLOSED

Abstraction doesn't happen during the Alive2.
Here are the detailed steps to TV the example. Hope it could help:

[Get final-state of src]

1. foo (int x):
   Alive2 assumes that function arguments can be arbitrary values, so they can be undef, poison, or well-defined value.
   It can be encoded into:
   (= %x ((ite isundef(%x) undef %x), ispoison(%x)))
   FYI, x is an SMT bitvector

2. y=(x+0):
   By the defined semantics of add, following holds:
   a) x = poison -> y = poison
   b) x = {n} -> y = {n + 0} = {n}
   c) x = undef -> y = {n + 0 | -2^31 <= n <= 2^31}
   It can be encoded into:
   (= %y ((ite isundef(%x) undef %x) + 0, ispoison(%x)))

   Note that, in alive2, the value could be a poison, set of integer/floating-point numbers or pointers. And the set of values is not a singleton if the value is undef.

3. return y:
   End the execution and emit the final-state <y, empty, false>. Note that the definition of the final-state is ValueNoRet x Memory x bool, in which each of them represents return value, memory, and whether the undefined behavior has occurred or not.

[Get final-state of tgt]
Same above, the final-state of the target is <y, empty, false>

[Check the refinement]
Since no operation manipulates the memory or triggers the UB, this example can be validated by only checking the refinement between the return values.

Let's rename the return value to avoid confusion.

• y_src: return value of src
• y_tgt: return value of tgt

Then we can say that, for all valid input, if y_tgt is a refinement of the y_src, then the target function is a refinement of the source.

Therefore if the following condition is true, the target function is a refinement of the source function(=, <= are symbols of set):

ispoison(y_tgt)
\/ (isdefined(y_src) /\ isdefined(y_tgt) /\ y_src = y_tgt)
\/ (isundef(y_src) /\ (y_tgt <= y_src))

And it could be checked by the off-the-shelf SMT solver like Z3.

from is661-advanced-software-security.

Thanks for the detailed response!

from is661-advanced-software-security.