F* extraction hangs

[franziskuskiefer]

The following crate can not get extract to F* with hax right now. It allocates a lot of memory and uses CPU cycles but does not seem to finish (I stopped it after 10 minutes).

use hmac::{Hmac, Mac};
use sha2::Sha256;

pub fn hmac() {
    let mut m = Hmac::<Sha256>::new_from_slice(&[13; 16]).unwrap();
    m.update(&[9; 32]);
    let _mac = m.finalize().into_bytes().to_vec();
}

Use cargo add hmac sha2 to add the required dependencies.

[W95Psp]

I just took a look at that:

• to find what is slow in the engine cargo hax into --profile BACKEND is helpful
• the AST import is very slow, despite the JSON being somehow small (1.4M)

Details:

info: hax[profiling]: Other (parse_options): 1604.573815ms, memory=68416271, 1 item
info: hax[profiling]: AST import: 111876.683539ms, memory=36565152608, 8 items
info: hax[profiling]: reject_RawOrMutPointer: 11712.153839ms, memory=936238220, 8 items
info: hax[profiling]: TransformHaxLibInline: 13310.437220ms, memory=936242543, 8 items
info: hax[profiling]: Specialize: 11294.574264ms, memory=2557814909, 8 items
info: hax[profiling]: DropSizedTrait: 11630.991998ms, memory=2557806758, 8 items
info: hax[profiling]: SimplifyQuestionMarks: 12669.82560ms, memory=936238685, 8 items

Action items:

• [ ] measure and trace functions in THIR import to understand what is that slow

[W95Psp]

I looked at this issue yesterday. In import_thir, the slow part is not so much importing, but renaming local instance names. The problem is not about this specific operation, but about visitors: types are repeated a lot, and visiting such an AST is slow.

This issue exists with every visitor and phase in the AST, and I'm not sure how to deal with that.

One thing I tried is getting rid of Sized constraints, but that was not enough. Also, I tried to memoize some nodes in the import phase, but that doesn't impact much the performances.

We may need to do some sort of automatic memoization in the visitors and/or the phases, but since OCaml is an effectful language, that might be hard to do. The good news is since we generate ourselfs visitors, we can do whatever we want.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[clementblaudeau]

Still relevant. It is caused by duplication (mostly of types / traits contraints when the type hierarchy is big). Would be fixed by a better memoïzation in the AST (as early as the importing of the THIR). A priori, the rust engine would also be affected.