search

FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
394 stars 58 forks source link

Introduce -faggressive-inlining #469

Closed mtzguido closed 1 week ago

mtzguido commented 3 weeks ago

Hi Jonathan, thanks for the tip yesterday about the inlining phase! It does make our code look much nicer.

In fact, I was thinking I would like this to be always done regardless of name and without requiring any attributes, so thought about adding this option, do you think it would be useful for others?

I could also add an attribute-based mechanism like you suggested if that's useful. If so, and if this option isn't desirable, maybe I can just have Pulse always add the attribute.

msprotz commented 3 weeks ago

Personally, I'd rather have an attribute, since currently we're doing a bunch of hacks in HACL-rs to name some variables uu_ to avoid intermediary let-bindings that cause move-outs in Rust (see https://github.com/hacl-star/hacl-star/blob/afromher_rs/code/streaming/Hacl.Streaming.Functor.fst#L270 for instance). It would be cleaner if we could mark these let-bindings as [@inline] with a descriptive name (instead of uu_).

But I also appreciate that the "clean" solution is probably a little bit of work to propagate, so I'm fine with the flag too. Feel free to merge is that makes a significant difference for you (with the understanding that none of my projects will use this flag, so you'll have to keep an eye on it to make sure it doesn't regress).

mtzguido commented 3 weeks ago

Sounds good, let me try that and get back.

mtzguido commented 1 week ago

This was superseded by #470. I don't really need the flag anymore, hence closing, but I rebased it just in case it becomes useful at a point. We could also consider an F* flag to always add the attribute.