Integrate VeriWasm.

[cfallin]

This commit brings in VeriWasm, a static analysis tool that independently verifies the sound heap-sandboxing and other properties of machine code generated by Cranelift as used by Lucet. It adds an option --veriwasm to the compiler lucetc so that, in concert with changes recently made to VeriWasm and Cranelift, we can verify generated code in memory, right after we generate it, and with reasonable overhead (measured at ~30% additional compile time for some simple test cases).

This PR currently refers to my fork of VeriWasm as a submodule; the fork has additional work on top of upstream that was reviewed internally by @iximeow. Once we work out where this should live permanently, we can update the submodule location, but this should be good enough for review.

[pchickey]

Do you think we can pull this off by depending on a crates.io release of veriwasm? see https://github.com/bytecodealliance/lucet/pull/660

[cfallin]

Do you think we can pull this off by depending on a crates.io release of veriwasm? see #660

Unfortunately not quite: this depends on changes I have in my fork (cfallin/veriwasm) but that have not been integrated into upstream (PLSysSec/veriwasm). We already reviewed those changes internally (thanks @iximeow) so the blocking factor here is just having the repo in its final place...

... specifically, after talking with @tschneidereit, @deian, and others a few weeks ago, we agreed that it made sense to move veriwasm into the bytecodealliance org, but I don't know the latest status on that (any updates, Till?). Once that happens, I can push my changes there, and then we can update the submodule ref here and get this reviewed and merged.

[iximeow]

have not been integrated into upstream (PLSysSec/veriwasm)

i think i've got good news for you! check out https://github.com/PLSysSec/veriwasm/pull/2 - i believe these are all of your patches, so the two forks should match now.

of course, the thoughts about which veriwasm/where apply. but i think veriwasm is pretty close to being cargo-able? the one blocker for that being me doing an appropriate crate release of yaxpeax-core.

[cfallin]

Oh hey, cool! Thanks for that @enjhnsn2. Once yaxpeax has the right version on crates.io we could create a PR over there and then we can ask for a crates.io release, which decouples us from the repo location question.

[cfallin]

Updated now to crates.io-released version of VeriWasm (and transitively, yaxpeax). However there seems to be an issue with the published version of yaxpeax:

error[E0382]: use of moved value: `values`
   --> /home/cfallin/.cargo/registry/src/github.com-1ecc6299db9ec823/yaxpeax-core-0.0.1-vw-tweaks/src/arch/x86_64/analyses/evaluators/value_set.rs:271:77
    |
265 | ...                   if let Some(Data::ValueSet(values)) = referent(instr, &op, addr, dfg, contexts) {
    |                                                  ------ move occurs because `values` has type `Vec<ValueRange>`, which does not implement the `Copy` trait
...
271 | ...                               DataDisplay { data: &Data::ValueSet(values), colors: None },
    |                                                                       ^^^^^^
    |                                                                       |
    |                                                                       value moved here
    |

@iximeow, thoughts?

[iximeow]

it turns out the macro expansion with tracing's log feature expands something like trace!("data: {}", expr) to textually duplicate expr. since DataDisplay { data: &Data::ValueSet(values), colors: None }, moves values, the second copy of that expression uses the value moved in the first copy and :boom:

i've fixed this in yaxpeax-core, verified that this branch builds with a patched dependency, and published as 0.0.2-vw-tweaks. once there's a veriwasm 0.1.1, i think we should be good to go here.

[cfallin]

Updated with latest VeriWasm; should be good for review now!

[cfallin]

Removed veriwasm from CRATES_NOT_TESTED in the Makefile since it's not a submodule anymore.