Remove further uses of Location::none (model-checking#3253)

We now only have 12 uses of `Location::none` left, all of which have no
reasonable location to use.

Resolves: model-checking#136

cprover_bindings/src/goto_program/expr.rs

@@ -140,6 +140,7 @@ pub enum ExprValue {
     /// `({ op1; op2; ...})`
     StatementExpression {
         statements: Vec<Stmt>,
+        location: Location,
     },
     /// A raw string constant. Note that you normally actually want a pointer to the first element.
     /// `"s"`
@@ -739,10 +740,10 @@ impl Expr {
     /// <https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html>
     /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })`
     /// `({ op1; op2; ...})`
-    pub fn statement_expression(ops: Vec<Stmt>, typ: Type) -> Self {
+    pub fn statement_expression(ops: Vec<Stmt>, typ: Type, loc: Location) -> Self {
         assert!(!ops.is_empty());
         assert_eq!(ops.last().unwrap().get_expression().unwrap().typ, typ);
-        expr!(StatementExpression { statements: ops }, typ)
+        expr!(StatementExpression { statements: ops, location: loc }, typ).with_location(loc)
     }
 
     /// Internal helper function for Struct initalizer

cprover_bindings/src/irep/to_irep.rs

@@ -299,9 +299,9 @@ impl ToIrep for ExprValue {
                 named_sub: linear_map![],
             },
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
-            ExprValue::StatementExpression { statements: ops } => side_effect_irep(
+            ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
                 IrepId::StatementExpression,
-                vec![Stmt::block(ops.to_vec(), Location::none()).to_irep(mm)],
+                vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
             ),
             ExprValue::StringConstant { s } => Irep {
                 id: IrepId::StringConstant,

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

@@ -252,7 +252,7 @@ impl<'tcx> GotocCtx<'tcx> {
             t.nondet().as_stmt(loc),
         ];
 
-        Expr::statement_expression(body, t).with_location(loc)
+        Expr::statement_expression(body, t, loc)
     }
 
     /// Kani does not currently support all MIR constructs.
@@ -356,7 +356,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     // Encode __CPROVER_r_ok(ptr, size).
                     // First, generate a CBMC expression representing the pointer.
                     let ptr = {
-                        let ptr_projection = self.codegen_place_stable(&ptr_place).unwrap();
+                        let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap();
                         let place_ty = self.place_ty_stable(place);
                         if self.use_thin_pointer_stable(place_ty) {
                             ptr_projection.goto_expr().clone()

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

@@ -3,7 +3,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
-use cbmc::goto_program::Lambda;
+use cbmc::goto_program::{Lambda, Location};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
@@ -105,7 +105,11 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Convert the Kani level contract into a CBMC level contract by creating a
     /// CBMC lambda.
-    fn codegen_modifies_contract(&mut self, modified_places: Vec<Local>) -> FunctionContract {
+    fn codegen_modifies_contract(
+        &mut self,
+        modified_places: Vec<Local>,
+        loc: Location,
+    ) -> FunctionContract {
         let goto_annotated_fn_name = self.current_fn().name();
         let goto_annotated_fn_typ = self
             .symbol_table
@@ -120,7 +124,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 Lambda::as_contract_for(
                     &goto_annotated_fn_typ,
                     None,
-                    self.codegen_place_stable(&local.into()).unwrap().goto_expr.dereference(),
+                    self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(),
                 )
             })
             .collect();
@@ -138,7 +142,8 @@ impl<'tcx> GotocCtx<'tcx> {
         assert!(self.current_fn.is_none());
         let body = instance.body().unwrap();
         self.set_current_fn(instance, &body);
-        let goto_contract = self.codegen_modifies_contract(modified_places);
+        let goto_contract =
+            self.codegen_modifies_contract(modified_places, self.codegen_span_stable(body.span));
         let name = self.current_fn().name();
 
         self.symbol_table.attach_contract(name, goto_contract);

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

@@ -50,6 +50,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
         let fn_name = self.symbol_name_stable(instance).intern();
+        let loc = self.codegen_span_stable(instance.def.span());
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
             self.symbol_table.lookup(fn_name).unwrap()
@@ -63,8 +64,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // https://github.com/model-checking/kani/issues/2426
             self.ensure(fn_name, |gcx, _| {
                 let typ = gcx.codegen_ffi_type(instance);
-                Symbol::function(fn_name, typ, None, instance.name(), Location::none())
-                    .with_is_extern(true)
+                Symbol::function(fn_name, typ, None, instance.name(), loc).with_is_extern(true)
             })
         } else {
             let shim_name = format!("{fn_name}_ffi_shim");
@@ -77,7 +77,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     typ,
                     Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)),
                     instance.name(),
-                    Location::none(),
+                    loc,
                 )
             })
         }
@@ -109,7 +109,7 @@ impl<'tcx> GotocCtx<'tcx> {
         } else {
             let ret_expr = unwrap_or_return_codegen_unimplemented_stmt!(
                 self,
-                self.codegen_place_stable(ret_place)
+                self.codegen_place_stable(ret_place, loc)
             )
             .goto_expr;
             let ret_type = ret_expr.typ().clone();

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

@@ -33,11 +33,12 @@ impl<'tcx> GotocCtx<'tcx> {
         place: &Place,
         mut fargs: Vec<Expr>,
         f: F,
+        loc: Location,
     ) -> Stmt {
         let arg1 = fargs.remove(0);
         let arg2 = fargs.remove(0);
         let expr = f(arg1, arg2);
-        self.codegen_expr_to_place_stable(place, expr, Location::none())
+        self.codegen_expr_to_place_stable(place, expr, loc)
     }
 
     /// Given a call to an compiler intrinsic, generate the call and the `goto` terminator
@@ -178,7 +179,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // Intrinsics which encode a simple binary operation
         macro_rules! codegen_intrinsic_binop {
-            ($f:ident) => {{ self.binop(place, fargs, |a, b| a.$f(b)) }};
+            ($f:ident) => {{ self.binop(place, fargs, |a, b| a.$f(b), loc) }};
         }
 
         // Intrinsics which encode a simple binary operation which need a machine model
@@ -208,7 +209,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let alloc = stable_instance.try_const_eval(place_ty).unwrap();
                 // We assume that the intrinsic has type checked at this point, so
                 // we can use the place type as the expression type.
-                let expr = self.codegen_allocation(&alloc, place_ty, Some(span));
+                let expr = self.codegen_allocation(&alloc, place_ty, loc);
                 self.codegen_expr_to_place_stable(&place, expr, loc)
             }};
         }
@@ -727,7 +728,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let res = self.codegen_binop_with_overflow(binop, left, right, result_type.clone(), loc);
         self.codegen_expr_to_place_stable(
             place,
-            Expr::statement_expression(vec![res.as_stmt(loc)], result_type),
+            Expr::statement_expression(vec![res.as_stmt(loc)], result_type, loc),
             loc,
         )
     }
@@ -1042,9 +1043,11 @@ impl<'tcx> GotocCtx<'tcx> {
         let is_lhs_ok = lhs_var.clone().is_nonnull();
         let is_rhs_ok = rhs_var.clone().is_nonnull();
         let should_skip_pointer_checks = is_len_zero.and(is_lhs_ok).and(is_rhs_ok);
-        let place_expr =
-            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place))
-                .goto_expr;
+        let place_expr = unwrap_or_return_codegen_unimplemented_stmt!(
+            self,
+            self.codegen_place_stable(place, loc)
+        )
+        .goto_expr;
         let res = should_skip_pointer_checks.ternary(
             Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned)
             BuiltinFn::Memcmp
@@ -1634,7 +1637,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 loc,
             )
         } else {
-            self.binop(p, fargs, op_fun)
+            self.binop(p, fargs, op_fun, loc)
         }
     }