zetzit / zz

πŸΊπŸ™ ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

Module search is not predictable #155

Closed sternenseemann closed 3 years ago

sternenseemann commented 3 years ago

Something which I have discovered while writing this change is that zz uses a HashSet internally to represent the modules search path.

This is an issue because it leads to inconsistent behavior if two different modules with the same name are in the search path: Say an user sets ZZ_MODULES_PATH to include a local checkout of zz where they are hacking on the standard library. zz could then while resolving which module to use either pick the one shipped with the compiler or the one in ZZ_MODULES_PATH because HashSet has no guaranteed iteration error. What's more this could be inconsistent across runs and machines.

aep commented 3 years ago

Thanks for reporting. This is indeed not correct, but fortunately easy to fix

aep commented 3 years ago

@sternenseemann as for your actual issue with zz referencing the build dir, i believe this also needs to be addressed.

How about we just add a super long string to the default list which you can sed replace? Odd that there's no tool for replacing strings in binaries properly.

Or could you patch the source if we added all the distro specific stuff to a single file?

sternenseemann commented 3 years ago

Since we need to generate a shell wrapper anyways for z3, patching out the CARGO_MANIFEST_DIR thing is actually enough. Also /nix/store/modules remaining in the search path is not pretty, but no problem at all since that directory will never exist.

I'm not sure which search path entry you are referring to exactly with your proposal, but I'd prefer it to patch the source rather than the binary. It doesn't need to be sed-able, I can also just vendor in a patch, but it'd be nice if that wouldn't require updating at every version bump.

aep commented 3 years ago

specifically would it help if we moved this

https://github.com/zetzit/zz/blob/9b4bfa0248dd27f00512ece635f9d5960ed7f0bd/src/lib.rs#L120

to a separate file that only contains something like

const vendor_modules = vec![std::path::Path::new(env!("CARGO_MANIFEST_DIR")).join("modules"))];

so you can replace it here

since the file will just contain vendor paths, patches will probably apply for a long time

sternenseemann commented 3 years ago

Yes that would work!

Also I'm wondering if we could make this bit a configuration option or something while we're at it:

https://github.com/zetzit/zz/blob/9b4bfa0248dd27f00512ece635f9d5960ed7f0bd/src/lib.rs#L107-L119