Add support for unaligned_volatile_load and unaligned_volatile_store

[ivmat]

Completes the volatile intrinsic family on the tracking issue #1163, on top of #4672
(volatile copy/set).

Depends on #4672 and includes its commit. GitHub cannot base a PR on a branch that
lives in a fork, so this is opened against main and its diff currently contains both
commits; the two are separate and separately titled in the commit list. Happy to rebase
and shrink this to its own commit as soon as #4672 lands, or to squash the two into a
single PR if you would rather review them together.

The dependency is real, not just presentational: the core_intrinsics.rs change below is
only correct once both volatile_set_memory and unaligned_volatile_store are
supported, and unstable_codegen! only becomes unused once all five arms are gone.

With these two, unstable_codegen! has no remaining uses anywhere in kani-compiler and
is removed — these five volatile/unaligned entries were the last gated intrinsics in the
codegen match.

Modelling

Neither intrinsic has an alignment requirement, so neither emits an alignment assertion —
tolerating a misaligned pointer is the entire purpose of the unaligned_* variants.
unaligned_volatile_load was already sketched behind the gate as a plain dereference;
unaligned_volatile_store had no codegen and no Intrinsic variant at all, and is added
mirroring volatile_store minus the alignment check. Dereferenceability is still checked
by --pointer-check, as for the aligned variants.

That leaves one question worth being explicit about: is a misaligned typed dereference
modelled byte-precisely, or does it quietly assume alignment? The tests answer it rather
than assume it. Each proof compares the accessed value against a byte-wise oracle at a
deliberately misaligned offset, so an implementation that touched the aligned word instead
would fail rather than silently pass:

• Reading a u32 at byte offset 1 of a known pattern, the only correct little-endian
  answer is 0x55443322; an alignment-assuming read from offset 0 would give 0x44332211.
• The store proof checks the neighbouring bytes are untouched, so a wrongly-aligned write
  shows up as a clobbered neighbour.
• A third proof leaves the offset symbolic and compares against u32::from_le_bytes at
  every offset, so the result cannot be reached by constant folding.

Tests

• tests/kani/Intrinsics/Volatile/unaligned.rs — the three proofs above.
• tests/kani/VolatileIntrinsics/core_intrinsics.rs — this was marked kani-verify-fail,
  but that expectation existed only because unaligned_volatile_store (and
  volatile_set_memory) were unsupported. With both implemented the proof verifies,
  0 of 120 failed, so the header is removed and it becomes a passing test.

Note

tests/kani/VolatileIntrinsics/main_fixme.rs is left untouched (it is skipped as a fixme
test). Its test_copy_volatile names its arguments as though volatile_copy_memory were
(src, dst, count); the assertion it makes happens to hold under either argument order, so
it neither catches nor is broken by the ordering. Worth a separate look if that suite is
ever revived.

By submitting this pull request, I confirm that my contribution is made under the terms of
the Apache 2.0 and MIT licenses.

[ivmat]

Marking this as a draft until #4672 is reviewed and lands. Nothing has changed in the content — this is just to make the ordering explicit, since GitHub cannot base a cross-fork PR on a fork branch and this diff therefore currently shows #4672's commits as well. Once #4672 merges I will rebase this down to its own two commits and mark it ready.

[ivmat]

Pushed a follow-up commit after a review pass. One item was a regression this PR itself introduced, so flagging it explicitly rather than folding it in quietly.

ICE. Adding the UnalignedVolatileStore variant without teaching the points-to analysis about it routed the intrinsic into that pass's terminal unimplemented!(). Before this feature it resolved to Intrinsic::Unimplemented, which that pass handles gracefully — so the change turned a clean "unsupported" into a compiler panic for anyone running -Z uninit-checks over code calling it. It now shares the VolatileStore arm; the aliasing semantics (*a = b) are identical. The asymmetry was visible in the diff: the load was handled and the store was not.

The same omission existed in check_uninit's visitor. Root cause for both: the compiler matches on Intrinsic in three places — codegen, points-to, and the memory-initialization visitor — and they need updating as a set.

ZST guard. unaligned_volatile_store dereferenced unconditionally, while codegen_volatile_store guards exactly that case. A ZST pointer may legally be dangling-but-aligned, so the path is reachable. Guard replicated, regression test added.

Endianness. The oracle tests no longer assume little-endian — they use u32::from_ne_bytes/to_ne_bytes, which discriminates identically (an alignment-assuming read of bytes 0..4 differs from the correct 1..5 under either endianness) without pinning the suite to one target.

Verified: -Z uninit-checks over code calling both unaligned_volatile_store and volatile_set_memory now verifies cleanly, with no panic and no spurious memory-initialization failure. Full regression on CBMC 6.10.0 introduces no failures.

The soundness comment was also reworded — see the note on #4672; the same conservative-direction correction applies here.