Chapter 9 / Python: any_tuple_load

[proglang]

The translation of any_tuple_load at the end of section 9.5 is weird.

• a couple of valueOf are missing
• the macro any_len expects a tagged value, which has to be a tuple. Why don't we pass it untagged? It returns an untagged integer, which seems inconsistent (either all I/O tagged or untagged).
• the macro any_tuple_load appears recursively, which does not seem to be a good idea... I was expecting a Subscript operation at that point. Also the typing is inconsistent.

[jsiek]

The index argument of any_tuple_load is required (statically) to be an integer. So no ValueOf's are needed. I've updated the type checker to make this clear.

[jsiek]

Regarding any_len, why not untagged? Because it's difficult to give a type to the result of untagging the tuple. I use to do that, but it was a pain.

Why return an untagged integer? Because when we use any_len inside of the translation of any_tuple_load in the reveal_casts pass, we want the integer for purposes of doing the bounds check.

[jsiek]

Regarding any_tuple_load translating to any_tuple_load... the later should be renamed to unsafe_any_tuple_load.

[jsiek]

What was the inconsistency regarding the typing of any_tuple_load?

[jsiek]

I see that the cast insertion for subscript was broken in the book, and too limited in the implementation. I've fixed that now. Sorry for these bugs!