Merge pull request #1191 from GaloisInc/dholland-cast

Implement byte-to-char casts for crucible-mir.

crucible-mir/src/Mir/Trans.hs

@@ -789,12 +789,15 @@ evalCast' ck ty1 e ty2  = do
        -> baseSizeToNatCont bsz $ \w ->
            return $ MirExp (C.BVRepr w) (R.App $ E.BVIte e0 w (R.App $ eBVLit w 1) (R.App $ eBVLit w 0))
 
-      -- char to uint
+      -- char to usize
       (M.Misc, M.TyChar, M.TyUint  M.USize)
        | MirExp (C.BVRepr sz) e0 <- e
        -> return $ MirExp UsizeRepr (bvToUsize sz R.App e0)
+      -- char to other uint
       (M.Misc, M.TyChar, M.TyUint s) -> baseSizeToNatCont s $ extendUnsignedBV e
 
+      -- byte to char
+      (M.Misc, M.TyUint B8, M.TyChar) -> baseSizeToNatCont M.B32 $ extendUnsignedBV e
 
 
 

crux-mir/test/conc_eval/num/byte_to_char.rs

@@ -0,0 +1,10 @@
+pub fn b() -> u8 {
+    97
+}
+
+#[cfg_attr(crux, crux::test)]
+pub fn crux_test() -> char {
+    b() as char
+}
+
+pub fn main() { println!("{:?}", crux_test()); }