Update toolchain to nightly 2023-08-04

Cargo.lock

@@ -162,9 +162,12 @@ dependencies = [
 
 [[package]]
 name = "cc"
-version = "1.0.79"
+version = "1.0.81"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "50d30906286121d95be3d479533b458f87493b30a4b5f79a607db8f5d11aa91f"
+checksum = "6c6b2562119bf28c3439f7f02db99faf0aa1a8cdfe5772a2ee155d32227239f0"
+dependencies = [
+ "libc",
+]
 
 [[package]]
 name = "cfg-if"
@@ -205,7 +208,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn 2.0.27",
+ "syn 2.0.28",
 ]
 
 [[package]]
@@ -365,9 +368,9 @@ checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5"
 
 [[package]]
 name = "errno"
-version = "0.3.1"
+version = "0.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "4bcfec3a70f97c962c307b2d2c56e358cf1d00b558d74262b5f929ee8cc7e73a"
+checksum = "6b30f669a7961ef1631673d2766cc92f52d64f7ef354d4fe0ddfd30ed52f0f4f"
 dependencies = [
  "errno-dragonfly",
  "libc",
@@ -553,7 +556,7 @@ dependencies = [
  "proc-macro-error",
  "proc-macro2",
  "quote",
- "syn 2.0.27",
+ "syn 2.0.28",
 ]
 
 [[package]]
@@ -590,9 +593,9 @@ dependencies = [
 
 [[package]]
 name = "linux-raw-sys"
-version = "0.4.3"
+version = "0.4.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09fc20d2ca12cb9f044c93e3bd6d32d523e6e2ec3db4f7b2939cd99026ecd3f0"
+checksum = "57bcfdad1b858c2db7c38303a6d2ad4dfaf5eb53dfeb0910128b2c26d6158503"
 
 [[package]]
 name = "lock_api"
@@ -933,7 +936,7 @@ checksum = "b2eae68fc220f7cf2532e4494aded17545fce192d59cd996e0fe7887f4ceb575"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-automata 0.3.3",
+ "regex-automata 0.3.4",
  "regex-syntax 0.7.4",
 ]
 
@@ -948,9 +951,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.3.3"
+version = "0.3.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "39354c10dd07468c2e73926b23bb9c2caca74c5501e38a35da70406f1d923310"
+checksum = "b7b6d6190b7594385f61bd3911cd1be99dfddcfc365a4160cc2ab5bff4aed294"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -984,9 +987,9 @@ dependencies = [
 
 [[package]]
 name = "rustix"
-version = "0.38.4"
+version = "0.38.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0a962918ea88d644592894bc6dc55acc6c0956488adcebbfb6e273506b7fd6e5"
+checksum = "1ee020b1716f0a80e2ace9b03441a749e402e86712f15f16fe8a8f75afac732f"
 dependencies = [
  "bitflags 2.3.3",
  "errno",
@@ -1033,29 +1036,29 @@ dependencies = [
 
 [[package]]
 name = "serde"
-version = "1.0.175"
+version = "1.0.180"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5d25439cd7397d044e2748a6fe2432b5e85db703d6d097bd014b3c0ad1ebff0b"
+checksum = "0ea67f183f058fe88a4e3ec6e2788e003840893b91bac4559cabedd00863b3ed"
 dependencies = [
  "serde_derive",
 ]
 
 [[package]]
 name = "serde_derive"
-version = "1.0.175"
+version = "1.0.180"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b23f7ade6f110613c0d63858ddb8b94c1041f550eab58a16b371bdf2c9c80ab4"
+checksum = "24e744d7782b686ab3b73267ef05697159cc0e5abbed3f47f9933165e5219036"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.27",
+ "syn 2.0.28",
 ]
 
 [[package]]
 name = "serde_json"
-version = "1.0.103"
+version = "1.0.104"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d03b412469450d4404fe8499a268edd7f8b79fecb074b0d812ad64ca21f4031b"
+checksum = "076066c5f1078eac5b722a31827a8832fe108bed65dfa75e233c89f8206e976c"
 dependencies = [
  "itoa",
  "ryu",
@@ -1073,9 +1076,9 @@ dependencies = [
 
 [[package]]
 name = "serde_test"
-version = "1.0.175"
+version = "1.0.176"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "29baf0f77ca9ad9c6ed46e1b408b5e0f30b5184bcd66884e7f6d36bd7a65a8a4"
+checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab"
 dependencies = [
  "serde",
 ]
@@ -1200,9 +1203,9 @@ dependencies = [
 
 [[package]]
 name = "syn"
-version = "2.0.27"
+version = "2.0.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b60f673f44a8255b9c8c657daf66a596d435f2da81a555b06dc644d080ba45e0"
+checksum = "04361975b3f5e348b2189d8dc55bc942f278b2d482a6a0365de5bdd62d351567"
 dependencies = [
  "proc-macro2",
  "quote",
@@ -1226,7 +1229,7 @@ checksum = "090198534930841fab3a5d1bb637cde49e339654e606195f8d9c76eeb081dc96"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.27",
+ "syn 2.0.28",
 ]
 
 [[package]]
@@ -1293,7 +1296,7 @@ checksum = "5f4f31f56159e98206da9efd823404b79b6ef3143b4a7ab76e67b1751b25a4ab"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 2.0.27",
+ "syn 2.0.28",
 ]
 
 [[package]]
@@ -1595,9 +1598,9 @@ checksum = "1a515f5799fe4961cb532f983ce2b23082366b898e52ffbce459c86f67c8378a"
 
 [[package]]
 name = "winnow"
-version = "0.5.1"
+version = "0.5.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "25b5872fa2e10bd067ae946f927e726d7d603eaeb6e02fa6a350e0722d2b8c11"
+checksum = "f46aab759304e4d7b2075a9aecba26228bb073ee8c50db796b2c72c676b5d807"
 dependencies = [
  "memchr",
 ]

cprover_bindings/src/goto_program/expr.rs

@@ -1410,7 +1410,7 @@ impl Expr {
         ArithmeticOverflowResult { result, overflowed }
     }
 
-    /// Uses CBMC's [binop]-with-overflow operation that performs a single arithmetic
+    /// Uses CBMC's \[binop\]-with-overflow operation that performs a single arithmetic
     /// operation
     /// `struct (T, bool) overflow(binop, self, e)` where `T` is the type of `self`
     /// Pseudocode:

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

@@ -110,16 +110,15 @@ impl<'tcx> GotocCtx<'tcx> {
             .args
             .iter()
             .enumerate()
-            .filter_map(|(idx, arg)| {
-                (!arg.is_ignore()).then(|| {
-                    let arg_name = format!("{fn_name}::param_{idx}");
-                    let base_name = format!("param_{idx}");
-                    let arg_type = self.codegen_ty(arg.layout.ty);
-                    let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
-                        .with_is_parameter(true);
-                    self.symbol_table.insert(sym);
-                    arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
-                })
+            .filter(|&(_, arg)| (!arg.is_ignore()))
+            .map(|(idx, arg)| {
+                let arg_name = format!("{fn_name}::param_{idx}");
+                let base_name = format!("param_{idx}");
+                let arg_type = self.codegen_ty(arg.layout.ty);
+                let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc)
+                    .with_is_parameter(true);
+                self.symbol_table.insert(sym);
+                arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into()))
             })
             .collect();
         let ret_type = self.codegen_ty(fn_abi.ret.layout.ty);

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

@@ -187,7 +187,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let tupe = sig.inputs().last().unwrap();
         let args = match tupe.kind() {
-            ty::Tuple(substs) => *substs,
+            ty::Tuple(args) => *args,
             _ => unreachable!("a function's spread argument must be a tuple"),
         };
         let starting_idx = sig.inputs().len();

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

@@ -245,7 +245,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         macro_rules! codegen_size_align {
             ($which: ident) => {{
-                let tp_ty = instance.substs.type_at(0);
+                let tp_ty = instance.args.type_at(0);
                 let arg = fargs.remove(0);
                 let size_align = self.size_and_align_of_dst(tp_ty, arg);
                 self.codegen_expr_to_place(p, size_align.$which)
@@ -422,7 +422,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "cttz" => codegen_count_intrinsic!(cttz, true),
             "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
             "discriminant_value" => {
-                let ty = instance.substs.type_at(0);
+                let ty = instance.args.type_at(0);
                 let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
                 self.codegen_expr_to_place(p, e)
             }
@@ -764,7 +764,7 @@ impl<'tcx> GotocCtx<'tcx> {
         intrinsic: &str,
         span: Option<Span>,
     ) -> Stmt {
-        let ty = instance.substs.type_at(0);
+        let ty = instance.args.type_at(0);
         let layout = self.layout_of(ty);
         // Note: We follow the pattern seen in `codegen_panic_intrinsic` from `rustc_codegen_ssa`
         // https://github.com/rust-lang/rust/blob/master/compiler/rustc_codegen_ssa/src/mir/block.rs
@@ -1034,7 +1034,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let offset = fargs.remove(0);
 
         // Check that computing `offset` in bytes would not overflow
-        let ty = self.monomorphize(instance.substs.type_at(0));
+        let ty = self.monomorphize(instance.args.type_at(0));
         let (offset_bytes, bytes_overflow_check) =
             self.count_in_bytes(offset.clone(), ty, Type::ssize_t(), intrinsic, loc);
 
@@ -1184,7 +1184,7 @@ impl<'tcx> GotocCtx<'tcx> {
         p: &Place<'tcx>,
         loc: Location,
     ) -> Stmt {
-        let ty = self.monomorphize(instance.substs.type_at(0));
+        let ty = self.monomorphize(instance.args.type_at(0));
         let dst = fargs.remove(0).cast_to(Type::void_pointer());
         let val = fargs.remove(0).cast_to(Type::void_pointer());
         let layout = self.layout_of(ty);

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

@@ -139,7 +139,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             ConstValue::ZeroSized => match lit_ty.kind() {
                 // Rust "function items" (not closures, not function pointers, see `codegen_fndef`)
-                ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span),
+                ty::FnDef(d, args) => self.codegen_fndef(*d, args, span),
                 _ => Expr::init_unit(self.codegen_ty(lit_ty), &self.symbol_table),
             },
         }
@@ -699,11 +699,11 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_fndef(
         &mut self,
         d: DefId,
-        substs: ty::subst::SubstsRef<'tcx>,
+        args: ty::GenericArgsRef<'tcx>,
         span: Option<&Span>,
     ) -> Expr {
         let instance =
-            Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, substs).unwrap().unwrap();
+            Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), d, args).unwrap().unwrap();
         self.codegen_fn_item(instance, span)
     }
 

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

@@ -367,7 +367,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option<Expr> {
         match ty.kind() {
             // A local that is itself a FnDef, like Fn::call_once
-            ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)),
+            ty::FnDef(defid, args) => Some(self.codegen_fndef(*defid, args, None)),
             // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut
             ty::RawPtr(inner) => self
                 .codegen_local_fndef(inner.ty)
@@ -512,14 +512,14 @@ impl<'tcx> GotocCtx<'tcx> {
                 // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html
                 match before.mir_typ().kind() {
                     ty::Array(ty, len) => {
-                        let len = len.kind().try_to_target_usize(self.tcx).unwrap();
+                        let len = len.try_to_target_usize(self.tcx).unwrap();
                         let subarray_len = if from_end {
                             // `to` counts from the end of the array
                             len - to - from
                         } else {
                             to - from
                         };
-                        let typ = self.tcx.mk_array(*ty, subarray_len);
+                        let typ = Ty::new_array(self.tcx, *ty, subarray_len);
                         let goto_typ = self.codegen_ty(typ);
                         // unimplemented
                         Err(UnimplementedData::new(
@@ -541,9 +541,9 @@ impl<'tcx> GotocCtx<'tcx> {
                         } else {
                             Expr::int_constant(to - from, Type::size_t())
                         };
-                        let typ = self.tcx.mk_slice(*elemt);
+                        let typ = Ty::new_slice(self.tcx, *elemt);
                         let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut };
-                        let ptr_typ = self.tcx.mk_ptr(typ_and_mut);
+                        let ptr_typ = Ty::new_ptr(self.tcx, typ_and_mut);
                         let goto_type = self.codegen_ty(ptr_typ);
 
                         let index = Expr::int_constant(from, Type::ssize_t());
@@ -703,7 +703,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match before.mir_typ().kind() {
             //TODO, ask on zulip if we can ever have from_end here?
             ty::Array(elemt, length) => {
-                let length = length.kind().try_to_target_usize(self.tcx).unwrap();
+                let length = length.try_to_target_usize(self.tcx).unwrap();
                 assert!(length >= min_length);
                 let idx = if from_end { length - offset } else { offset };
                 let idxe = Expr::int_constant(idx, Type::ssize_t());