Stack overflow for deep expressions in bincode serialization/deserialization

[maximebuyse]

With rust code containing deep expressions, hax fails with a stack overflow. For example:

fn main() -> i32 {
        1 + 1 + 1 + 1 + 1 + 1 + 1 + 
        1 + 1 + 1 + 1 + 1 + 1 + 1 + 
        1 + 1 + 1 + 1 + 1 + 1 + 1 + 
        1 + 1 + 1 + 1 + 1 + 1 + 1
}

The stack trace suggests that this has to do with serialization/deserialization with bincode that was introduced in #743. However this problem cannot be reproduced with the merge commit of #743 itself (but it loops for a long time). The version of bincode hasn't changed since then so there might be an interaction with another later change that triggers the stack overflow.

[franziskuskiefer]

cargo hax json works fine for me. So the frontend seems fine. Only when extracting F* it fails for me (actually it just doesn't finish before I kill it).

[maximebuyse]

@franziskuskiefer You were right, the problem is in the engine. It happens in phase specialize where in some cases recursive calls are done twice over the same thing resulting in exponential complexity.
I don't know why this started making Rust stack overflows instead of just taking a long time.

[maximebuyse]

It turns out this fix doesn't improve the original problem. The example of deep expressions was only an attempt to minimize that had a different problem.

My current understanding is that when we have a rather big (or deep) module hierarchy, the items in HaxMeta contain a lot of data, and the data for a submodule seems to be duplicated in every parent module. There is no problem for encoding this with bincode, but decoding uses recursion and gives a stack overflow.

I tested a few serialization libraries and most don't support recursive types. Among those that do it seemed that bincode was one of the most efficient (I found none that seemed to behave better with deep recursive data).