openwsn-berkeley / lakers

EDHOC implemented in Rust, optimized for microcontrollers, with bindings for C and Python.
https://crates.io/crates/lakers
BSD 3-Clause "New" or "Revised" License
12 stars 10 forks source link

refactor: Apply suggestions from clippy #151

Closed chrysn closed 7 months ago

chrysn commented 7 months ago

The changes were hand-screened for whether they make sense in this particular case; most did.

Among other things, this replaces several returns with implicit returns, as is convenient for hax.

(Still a draft: This was just the ones a cargo clippy -p edhoc-rs -p edhoc-crypto -p edhoc-consts -p edhoc-ead-zeroconf -p edhoc-ead-none --no-default-features --features="edhoc-crypto/rustcrypto, ead-none" --fix produced, now starting to look at the output of clippy for more enhancements)

chrysn commented 7 months ago

The last two commits ("refactor: use map" and "refactor: use if-let") are trial balloons to see what hax has to say on them.

The latter is simple -- if we don't pass on the error, a big if-let that eventually implicitly returns, coupled with an implicit return in the error branch, does the trick.

Thing is, that doesn't work so smoothly when the error of the if-let-destructured thing needs processing. In that case, there are two options:

match my_thing {
    Ok((a, b, c)) => {
        // do with a, b, c
        Ok(f(a, b, c))
    }
    Err(e) => Err(e)
}

... or a map.

Using match is an option that I'm relatively sure will work for hax, but it's not pretty either, because of the lots of Ok'ing, and the trivial error passing-on line. (It's not unidiomatic enough to cause clippy to complain, though). The "Use map instead of unwrap pair" commit uses the map function. This should map quite straightforwardly to functional languages on the basic level, but given how this builds a closure that mutates around in locals before returning them, I'd rather want to see a hax check on this.

(In this particular case that using-locals-from-outside is completely needless -- the definition and default-population of plaintext_3 could just as well be moved into the closure; I deliberately didn't do that because that won't always be possible).

geonnave commented 7 months ago

I ran hax against it and it produces the two errors below.

$ cargo-hax -C -p edhoc-rs -p edhoc-consts  --no-default-features --features="edhoc-crypto/rustcrypto, ead-none" --release \; into -i '-edhoc_rs::generate_connection_identifier_cbor -edhoc_rs::generate_connection_identifier' fstar

... (truncated) ...

error[HAX0003]: (RefMut) The mutation of this &mut is not allowed here.
   --> lib/src/edhoc.rs:928:12
    |
928 |       p3.map(|p3| {
    |  ____________^
929 | |         plaintext_3.content[..p3.len].copy_from_slice(&p3.content[..p3.len]);
930 | |         plaintext_3.len = p3.len;
931 | |
932 | |         plaintext_3
933 | |     })
    | |_____^

error[HAX0006]: (LocalMutation) The bindings ["plaintext_3"] cannot be mutated here: they don't belong to the closure scope, and this is not allowed.
   --> lib/src/edhoc.rs:928:12
    |
928 |       p3.map(|p3| {
    |  ____________^
929 | |         plaintext_3.content[..p3.len].copy_from_slice(&p3.content[..p3.len]);
930 | |         plaintext_3.len = p3.len;
931 | |
932 | |         plaintext_3
933 | |     })
    | |_____^
chrysn commented 7 months ago

I've pushed an update to see whether a moderately more complex map function that does not reach out into the containing function's locals can work -- but CI won't let me run this.

This means I'll just start this over based on main, building a similar map function there (along with any clippy warnings still left to apply).

chrysn commented 7 months ago

Replaced by #154