Update LLBC backend for Trait support and translation of projection (#…

…3807)

1. Update LLBC backend to adapt to the changes of Charon submodule to
AeneasVerif/charon@adc0a85:
Changing translate_place to fit with the current place representation of
Charon.
3. Support translation of programs that use Trait, but translating the
trait impl functions into monomorphized functions.

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

---------

Co-authored-by: Zyad Hassan <[email protected]>

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -109,6 +109,7 @@ impl LlbcCodegenBackend {
 
         // Translate all the items
         for item in &items {
+            debug!("Translating: {item:?}");
             match item {
                 MonoItem::Fn(instance) => {
                     let mut fcx = Context::new(
@@ -387,12 +388,14 @@ where
 fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
     let options = TransformOptions {
         no_code_duplication: false,
-        hide_marker_traits: false,
+        hide_marker_traits: true,
         no_merge_goto_chains: false,
         item_opacities: Vec::new(),
     };
     let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
-    let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
+    let mut translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
+    //This option setting is for Aeneas compatibility
+    translated.options.hide_marker_traits = true;
     let errors = ErrorCtx::new(true, false);
     TransformCtx { options, translated, errors }
 }