search

prosyslab-classroom / cs348-information-security

61 stars 10 forks source link

[Question][Hw5] How to compare signs? #128

Closed Standchen closed 3 years ago

Standchen commented 3 years ago

Hello. Implementing function cmp in module Sign, I'd like to ask how to compare two signs.

Can I get an example for such comparison, or any reference to look up?

Thank you in advance.

KihongHeo commented 3 years ago

Do you mean its design or implementation? If you mean design, you can first think of the concrete version (i.e., original C and LLVM semantics). Then try to design a sound approximation of the comparison operator. In principle <, <=, etc are just binary operators. Recall how we designed the abstract + operator.

Standchen commented 3 years ago

@KihongHeo Thank you for the answer. However, comparison operator in C and other languages returns Boolean, not the type of the numerical value itself, to my only knowledge. And the signature of VALUE_DOMAIN demands the function cmp to return Sign. I have no idea how to extend the result of comparison operator to sign abstrat domain. I thought of the semantics of cmp to be like: cmp < Top Zero --> Neg, but such semantics is more likely to be that of filter. I could come up with other functions like add, sub, div, or mul, but cmp is a bit more difficult I guess..

KihongHeo commented 3 years ago

Aha. There is no boolean in C and LLVM. You can think 0 as false 1 as true.

Standchen commented 3 years ago

Now I get it. Appreciate your kindesss!