Force intptrcast for binary operations

src/lib.rs

@@ -637,15 +637,17 @@ fn ptr_to_int(
 
         let alloc = memory.get(ptr.alloc_id)?;
 
-        let base_addr = match alloc.extra.base_addr.borrow().clone() { 
-            Some(base_addr) => base_addr,
+        let mut base_addr = alloc.extra.base_addr.borrow_mut();
+        
+        let addr = match *base_addr { 
+            Some(addr) => addr,
             None => {
-                let base_addr = extra.addr;
+                let addr = extra.addr;
                 extra.addr += alloc.bytes.len() as u64;
 
-                *alloc.extra.base_addr.borrow_mut() = Some(base_addr);
+                *base_addr = Some(addr);
 
-                let elem = (base_addr, ptr.alloc_id);
+                let elem = (addr, ptr.alloc_id);
 
                 if let Err(pos) = extra.vec.binary_search(&elem) {
                     extra.vec.insert(pos, elem);
@@ -653,10 +655,10 @@ fn ptr_to_int(
                     return err!(Unreachable);
                 }
 
-                base_addr
+                addr
             }
         };
 
-        Ok(base_addr + ptr.offset.bytes())
+        Ok(addr + ptr.offset.bytes())
     }
 }

src/operator.rs

@@ -44,6 +44,16 @@ fn ptr_op(
 
         trace!("ptr_op: {:?} {:?} {:?}", *left, bin_op, *right);
 
+        if self.memory().extra.seed.is_some() && bin_op != Offset {
+            let l_bits = self.force_bits(left.imm.to_scalar()?, left.layout.size)?;
+            let r_bits = self.force_bits(right.imm.to_scalar()?, right.layout.size)?;
+            
+            let left = ImmTy::from_scalar(Scalar::from_uint(l_bits, left.layout.size), left.layout);
+            let right = ImmTy::from_scalar(Scalar::from_uint(r_bits, left.layout.size), right.layout);
+
+            return self.binary_op(bin_op, left, right);
+        } 
+
         // Operations that support fat pointers
         match bin_op {
             Eq | Ne => {

tests/run-pass/intptrcast-truncate.rs

@@ -0,0 +1,8 @@
+// compile-flags: -Zmiri-seed=0000000000000000
+
+fn main() {
+    let x = &42 as *const i32 as usize; 
+    let y = x * 2;
+    let z = y as u8 as usize;
+    assert_eq!(z, y % 256);
+}