Add pointer equality semantics (#736)

- Tackle this issue:
#735

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1762,6 +1762,39 @@ The unary operation `unOpPtrMetadata`, when given a reference or pointer to a sl
   // could add a rule for cases without metadata
 ```
 
+#### Pointer equality
+
+Raw pointer comparisons ignore mutability, but require the address and metadata to match.
+
+```k
+  syntax Bool ::= #ptrLocalEq(Value, Value) [function, total]
+
+  rule #ptrLocalEq(
+          PtrLocal(OFFSET1, PLACE1, _, PTRMETA1),
+          PtrLocal(OFFSET2, PLACE2, _, PTRMETA2)
+       )
+    =>  OFFSET1 ==Int OFFSET2
+     andBool PLACE1 ==K PLACE2
+     andBool PTRMETA1 ==K PTRMETA2
+  rule #ptrLocalEq(_, _) => false [owise]
+
+  rule #applyBinOp(
+          binOpEq,
+          PtrLocal(_, _, _, _) #as PTR1,
+          PtrLocal(_, _, _, _) #as PTR2,
+          _
+       )
+    => BoolVal(#ptrLocalEq(PTR1, PTR2))
+
+  rule #applyBinOp(
+          binOpNe,
+          PtrLocal(_, _, _, _) #as PTR1,
+          PtrLocal(_, _, _, _) #as PTR2,
+          _
+       )
+    => BoolVal(notBool #ptrLocalEq(PTR1, PTR2))
+```
+
 
 
 #### Pointer Artithmetic

kmir/src/tests/integration/data/exec-smir/pointers/ref_ptr_cases.rs

@@ -0,0 +1,43 @@
+fn aliasing_refs_have_same_pointer() {
+    let value = 42_i32;
+    let first = &value;
+    let second = &value;
+
+    assert!((first as *const i32) == (second as *const i32));
+    assert!(std::ptr::eq(first, second));
+}
+
+fn distinct_locals_have_distinct_pointers() {
+    let left = 10_i32;
+    let right = 10_i32;
+
+    assert!((&left as *const i32) != (&right as *const i32));
+}
+
+fn array_element_addresses_are_distinct() {
+    let items = [3_u8, 5, 7];
+    let first = &items[0];
+    let first_again = &items[0];
+    let second = &items[1];
+
+    assert!((first as *const u8) == (first_again as *const u8));
+    assert!((first as *const u8) != (second as *const u8));
+}
+
+fn reborrow_mut_pointer_roundtrip() {
+    let mut byte = 0_u8;
+    let ptr = &mut byte as *mut u8;
+
+    unsafe {
+        *ptr = 1;
+    }
+
+    assert_eq!(byte, 1);
+}
+
+fn main() {
+    aliasing_refs_have_same_pointer();
+    distinct_locals_have_distinct_pointers();
+    array_element_addresses_are_distinct();
+    reborrow_mut_pointer_roundtrip();
+}