[Boogie Backend] Codegen the arguments to Kani intrinsics inside the functions that handle the intrinsics

[zhassan-aws]

This is a refactor change: currently, the functions that codegen Kani intrinsics (asserts, assumes, etc.) take the arguments to the intrinsics as Boogie expressions (boogie_ast::boogie_program::Expr). In other words, the MIR arguments (rustc_middle::mir::syntax::Operand) are converted to Boogie expressions before passing them to the functions.

This PR changes the functions to take the MIR arguments directly, and perform the codegen into Boogie expressions inside the functions. This allows those functions to query any information in the MIR Operand, that is not available after codegen to Boogie expressions.

Note: it may make sense to do the same change for the Goto backend to avoid having to pattern match on the expressions (e.g.

kani/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

Line 74 in 2aca488

let msg = tcx.extract_const_message(&msg).unwrap();

), and instead get the information needed from the MIR operand directly.

Resolves #ISSUE-NUMBER

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.