Added volatile_load intrinsic (#987)

This PR adds the
[volatile_load](https://doc.rust-lang.org/std/intrinsics/fn.volatile_load.html)
intrinsic. For this semantics, memory being "volatile" is meaningless as
the we are not compiling any further, and aren't modeling any compiler
optimisations that could occur if we were to. Therefore this is
implemented as a simple dereference of the pointer and read of the value
at the location into the destination.

Author: dkcumming

kmir/src/kmir/kdist/mir-semantics/intrinsics.md

@@ -143,6 +143,26 @@ write the value to that location.
        ... </k>
 ```
 
+#### Volatile Load (`std::intrinsics::volatile_load`, `std::ptr::read_volatile`)
+
+The `volatile_load` intrinsic reads a value from a memory location through a pointer, ensuring the read is not
+optimised away by the compiler. Unlike normal loads, volatile loads are guaranteed to occur exactly once and
+in order with respect to other volatile operations. In the semantics, this is equivalent to a regular load
+through a dereferenced pointer. We extract the place from the pointer operand, add a deref projection, and
+read the value from that location into the destination. Since `#setLocalValue` is strict in its second argument,
+the dereferenced operand is evaluated (i.e., the value is read from memory) before being written to `DEST`.
+
+```k
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_load")), operandCopy(place(LOCAL, PROJ)) .Operands, DEST, _SPAN)
+        => #setLocalValue(DEST, operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))))
+       ... </k>
+
+  // for `operandMove` the pointer is moved, but the pointed-to value is copied (read, not consumed)
+  rule <k> #execIntrinsic(IntrinsicFunction(symbol("volatile_load")), operandMove(place(LOCAL, PROJ)) .Operands, DEST, _SPAN)
+        => #setLocalValue(DEST, operandCopy(place(LOCAL, appendP(PROJ, projectionElemDeref .ProjectionElems))))
+       ... </k>
+```
+
 #### Ptr Offset Computations (`std::intrinsics::ptr_offset_from`, `std::intrinsics::ptr_offset_from_unsigned`)
 
 The `ptr_offset_from[_unsigned]` calculates the distance between two pointers within the same allocation,

kmir/src/tests/integration/data/prove-rs/read_volatile.rs

@@ -0,0 +1,11 @@
+fn main() {
+    let a: i32 = 5555;
+    let a_ptr = &a as *const _;
+
+    let b: i32;
+    unsafe {
+        b = std::ptr::read_volatile(a_ptr);
+    }
+
+    assert!(b == 5555);
+}

kmir/src/tests/integration/data/prove-rs/volatile_load.rs

@@ -0,0 +1,12 @@
+#![feature(core_intrinsics)]
+fn main() {
+    let a: i32 = 5555;
+    let a_ptr = &a as *const _;
+
+    let b: i32;
+    unsafe {
+        b = std::intrinsics::volatile_load(a_ptr);
+    }
+
+    assert!(b == 5555);
+}