Feature request: add a pass to filter the useless external declarations

[sonmarcho]

It sometimes happens that the crate serialized by Charon contains some external definitions which are actually not used anywhere. It regularly happens for instance with core::intrinsics::discriminant_value, as a micro-pass attempts to eliminate its uses from the LLBC. It can cause issues because, as of today, (one of the dependencies of) core::intrinsics::discriminant_value doesn't fit in the subset supported by some users of Charon (e.g., Aeneas). For this reason, it would be good to implement an additional pass to eliminate those useless definitions by doing a reachability analysis.

Code snippet:

#[derive(PartialEq)]
enum S { Variant1, Variant2 }

Current Charon output:

The output of charon --print-llbc contains, among others:

#[lang_item("discriminant_kind")]
pub trait core::marker::DiscriminantKind<Self>
{
    ... // omitted
}

pub fn core::intrinsics::discriminant_value<'_0, T>(@1: &'_0 (T)) -> core::marker::DiscriminantKind<T>::Discriminant
where
    [@TraitClause0]: core::marker::Sized<T>,

After implementing this pass, those definitions should not be present anymore.

[Nadrieril]

We already compute a graph of all definitions in reorder_decls; it might be relatively easy to add a reachability analysis to it, where the roots of the reachability would be the items selected by --start-from.