Use signed types for signed scalars (rust-lang#1063)

* Use signed types for signed scalars

* Remove outdated comment

Author: adpaco-aws

src/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -157,15 +157,13 @@ impl<'tcx> GotocCtx<'tcx> {
         debug! {"codegen_scalar\n{:?}\n{:?}\n{:?}\n{:?}",s, ty, span, &ty.kind()};
         match (s, &ty.kind()) {
             (Scalar::Int(_), ty::Int(it)) => match it {
-                // We treat the data as bit vector. Thus, we extract the value as unsigned and set
-                // the type to signed int.
-                IntTy::I8 => Expr::int_constant(s.to_u8().unwrap(), Type::signed_int(8)),
-                IntTy::I16 => Expr::int_constant(s.to_u16().unwrap(), Type::signed_int(16)),
-                IntTy::I32 => Expr::int_constant(s.to_u32().unwrap(), Type::signed_int(32)),
-                IntTy::I64 => Expr::int_constant(s.to_u64().unwrap(), Type::signed_int(64)),
-                IntTy::I128 => Expr::int_constant(s.to_u128().unwrap(), Type::signed_int(128)),
+                IntTy::I8 => Expr::int_constant(s.to_i8().unwrap(), Type::signed_int(8)),
+                IntTy::I16 => Expr::int_constant(s.to_i16().unwrap(), Type::signed_int(16)),
+                IntTy::I32 => Expr::int_constant(s.to_i32().unwrap(), Type::signed_int(32)),
+                IntTy::I64 => Expr::int_constant(s.to_i64().unwrap(), Type::signed_int(64)),
+                IntTy::I128 => Expr::int_constant(s.to_i128().unwrap(), Type::signed_int(128)),
                 IntTy::Isize => {
-                    Expr::int_constant(s.to_machine_usize(self).unwrap(), Type::ssize_t())
+                    Expr::int_constant(s.to_machine_isize(self).unwrap(), Type::ssize_t())
                 }
             },
             (Scalar::Int(_), ty::Uint(it)) => match it {

src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -611,6 +611,18 @@ impl<'tcx> GotocCtx<'tcx> {
                         TagEncoding::Direct => {
                             let discr = def.discriminant_for_variant(self.tcx, *variant_index);
                             let discr_t = self.codegen_enum_discr_typ(pt);
+                            // The constant created below may not fit into the type.
+                            // https://github.com/model-checking/kani/issues/996
+                            //
+                            // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)`
+                            // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant`
+                            // because when it tries to codegen `std::cmp::Ordering` (which should produce
+                            // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types:
+                            //
+                            // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty);
+                            // DISCRIMINANT - val:255 ty:i8
+                            // DISCRIMINANT - val:0 ty:i8
+                            // DISCRIMINANT - val:1 ty:i8
                             let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t));
                             self.codegen_place(place)
                                 .goto_expr