Migrating to Monomorphised LLBC

[Lin23299]

This PR is for #257. The current goal is to support monomorphised LLBC (add --monomorphize for charon in Makefile). Hopefully we can support both monomorphized and generic code.

The first fix is to eliminate core::option::Option which was previouly removed by Monomorphization.datatypes. Now it's removed by drop_unused_type following the style of drop_unused in krml/Inlining.ml

[Lin23299]

Now the problem is the matching of certain functions using cremepat. For example, the remove_array_eq :

  method! visit_expr ((n_cgs, n_binders) as env, _) e =
    match e with
    | [%cremepat {| core::array::equality::?impl::eq[#?n](#?..)<?t,?u>(?a1, ?a2) |}] ->
        let rec is_flat = function

was used to match

core.array.equality.{core::cmp::PartialEq<@Array<U,␣N>>␣for␣@Array<T,␣N>}.eq
  < int32_t > 
  < int32_t >
  [[2size_t]]
  [[core.cmp.impls.{core::cmp::PartialEq<i32>␣for␣i32}.eq]]
  uu____4@1
  uu____5@0;

now we want it to match the monomorphised

core.array.equality.{core::cmp::PartialEq::<@Array<i32,␣2usize>,␣@Array<i32,␣2usize>>}.eq.<i32,␣i32,␣2usize>
  uu____4@1
  uu____5@0;

Since we are not familiar with cremepat (I'm trying), maybe @msprotz do you have any plan or idea to extend the pattern matching mechanism and match both mono and non-mono versions of these functions?

[ssyram]

@protz The table has been implemented as lid_full_generic in AstOfLlbc. We also implemented a function re_polymorphize right below the table. We can simply call this function to transform the expression before the pattern matching to be made. So that there seems to be no need to fix the cremepat here. Could you please have a look and comment on it? We have tested the function on a PreCleanup pass, where the re_polymorphize function works perfectly with the existing cremepat mechanism. But there is an issue of matching exact string in the same function that we are trying to fix tomorrow.

[ssyram]

We are now implementing the transition, but the transition is now based on the current version (not the one in the PR), and we have observed several issues with this transition:

1. The example array.rs caused the follow problems:

   • in Charon @Nadrieril , the following problem is raised:

   warning: Could not compute the value of Clause0_0::Clause1::Output (Some(Clause(Bound(DeBruijnId { index: 0 }, 0)))) needed to update generics  for item core::ops::function::FnMut::<array::mk_incr2::closure::<10 : usize><'_>, (usize)>.
        Constraints in scope:
   

   • Also in Charon, we found that the mk_incr function has two versions: the generic version of mk_incr<const K : usize> and the monomorphized version mk_incr::<10 : usize>. This could be temporarily resolved by also having --monomorphize-conservative at the same time. But it is surely a bug.
   • The problem in Eurydice only @protz : to remove the from_fn function, ETApp should keep the fn_mut, fn_once functions, but these functions cannot be easily obtained here in the re_polymorphize function. I have confirmed that the third element of ETApp is ONLY used in the removal of from_fn function and this seems to be hard to recover in the monomorphized case? This pass seems to be very hard to cope with in the mono case.

2. The example const_generic.rs caused TError in Charon @Nadrieril if --monomorphize is called;

3. The example dst.rs has the problem of unknown unsized cast. The problem is caused by that now S<[i32; 4]> and S<[i32]> are now totally different types, the original casting could not handle it. But this should be fixed in the Explicit Unsized Metadata & Unified DST Handling #259, temporarily ignored here;

[Nadrieril]

I'm looking into these errors

[Nadrieril]

• The problem in Eurydice only @protz : to remove the from_fn function, ETApp should keep the fn_mut, fn_once functions, but these functions cannot be easily obtained here in the re_polymorphize function. I have confirmed that the third element of ETApp is ONLY used in the removal of from_fn function and this seems to be hard to recover in the monomorphized case? This pass seems to be very hard to cope with in the mono case.

We could add the trait refs to the re-polymorphization side table. Or if not the trait refs themselves, the output of build_trait_ref_mapping on them.

Alternatively you can safely assume that the generic parameter F of from_fn will be to a closure. Using the re-polymorphization side-table, you should be able to get the type_decl of the closure struct we care about. In its src parameter you'll find a pointer to the impl FnMut for <closure> from which you can get the fn_mut method.

[Nadrieril]

• Also in Charon, we found that the mk_incr function has two versions: the generic version of mk_incr<const K : usize> and the monomorphized version mk_incr::<10 : usize>.

That's a maybe-weird design choice: --monomorphize translates all items it sees including the generic ones. If you want only the mono items required to run main, you can pass --start-from=crate::main. I'm open to changing that honestly, it is indeed confusing.

[ssyram]

Thanks for the discussion! For your points:

• For the re-poly mechanism & from_fn: OK, I'm having a try to fix this case. I think it may be worth doing a trick to add additionally the fn_ptrs in the expression_of_fn_ptr function to the name added for f. This is quite an ugly trick but should be a quick fix. Will report the effect later.
• For the --monomorphize, it is still strange to have --start-from=crate::main? Because we may be working on a library crate instead of binary? I guess simply removing the non-monomorphized function is the best? Because we have all the monomorphized functions at hand and all the usages are with the mono instances instead of the generic template itself?

[Nadrieril]

I guess simply removing the non-monomorphized function is the best?

Yeah I agree actually. This and the other bugs reported above have been fixed in AeneasVerif/charon#810.

[ssyram]

Thank you so much for the quick fix!

[Lin23299]

Hi @Nadrieril @msprotz , I'm trying to fix the rewriting of from_fn. Now this function can be rewritten into a for loop using the closure function named as:

array.mk_incr.{core::ops::function::FnMut::<array::mk_incr::closure::<10usize>,␣(usize)>}.call_mut.<10usize>

While the generated function definition for it is named as:

array_mk_incr_{core::ops::function::FnMut::<array::mk_incr::closure::<10usize>, (usize)>}_call_mut_<10usize>

The names are slightly different and eurydice refuses to compile cuz it can not find the implementation of this function.
I'm confused that whether this name mismatch comes from some inconsistent naming mechanism between charon and eurydice? Or It's just my mistakes in translating the C.trait_refs into K.expr list. Any idea will be helpful :)

For reference, I'm using the test case:

fn mk_incr<const K: usize>() -> [u32; K] {
    core::array::from_fn(|i| i as u32)
}

fn main() {
    let a: [u32; 10] = mk_incr();
    assert_eq!(a[9], 9);
}

[Nadrieril]

It seems a bit of name normalization is missing. The name that we pass to krml is a list of path elements, I don't think eurydice does any more manipulation of the name; so the difference is due to karamel.

Looking through krml, the only place that inserts the special ␣ char is the xstring function. The first identifier you show therefore looks to be the output of print_lident, whereas the second one looks like the output of string_of_lident (found by grepping for String.concat "_"). I'm guessing these two are used inconsistently.

[ssyram]

After quite a long debugging, the mono migration for built-in functions are now handled. The ultimate scheme turns out to be quite simple with some tricky points.

1. We should have a mechanism to match the patterns with monomorphised names. This is implemented in Mono Name-Matcher charon#820 , which supports matching the monomorphised items with patterns, e.g., those defined in AstOfLlbc.ml.
2. Then, it turns out that some monomorphised functions are having different patterns as compared to the original ones, this, as far as I know, is caused by that associated types are now fully resolved and will not live as additional generics in mono items. This is of course good as it is a more thorough and general solution. But this requires different forms, which are added in known_builtins. For example, we now have: parse_pattern "core::array::{core::ops::index::Index<[@T; @N], @I>}::index<'_, @, core::ops::range::Range<usize>, @>", Builtin.array_to_subslice_mono.
3. Besides, the actual built-in functions are having different types than their generics counterparts. So, new functions like array_to_subslice_mono are declared and also implemented in just eurydice_glue --- notably, this frees us from implementing the built-in functions with abstract syntax!
4. Besides, we should re-polymorphise the built-in functions in the expression_of_fn_ptr procedure --- the built-in functions should be considered and handled as the original generic functions, hence new mechanisms for taking out and managing the generics are introduced.
5. Notably, for the previous step, one should be very careful about the re-polymorphising in expression_of_fn_ptr. This is because the re-poly should only be applied on the built-in functions as they actually have the poly implementations. And if we re-polymorphise the other function calls, it will easily refer to some unknown generic functions. Remember, all functions are mono, hence the expression_of_fn_ptr for these functions should return a call to a mono function, instead of a generic one.

[ssyram]

@protz Here's another point I want to discuss with you. First of all, I'm still not completely sure what is the third field of ETApp, the comments there are not very clear and I even cannot decode the English. I can understand that it collects something to be used in the later passes, but this "something" is quite messy. In remove_slice_eq, it refers to the internal eq function. While in remove_array_from_fn, it refers to the closure function calls. Would you mind providing a more comprehensive explanation of what they are, intuitively and as an overview, how are they computed?

Then, here comes the key question. In expression_of_fn_ptr for generating these third-field-content of ETApp, it involves a heavy computation involving the types and the generics. So there are two ways of handling them that I can conceive:

1. (Experimental & Risky) We have two completely different schemes, one just for computing the third field another for computing the ultimate type. So that, in the generic case, the first scheme simply computes useful info for the second, as original. While in the mono case, the first is completely separated and a full re-polymorphisation is performed there, while the second simply takes the mono type. As I'm not very sure what is the internal computation, the first step might be potentially risky that some info might still be missing even if we try to re-polymorphise the items. It would be greatly appreciated if you are interested in and would be so kind as to handling this case.
2. (Straightforward while with Sacrifice) We keep the current mechanism and ONLY allow the built-in functions to be re-polymorphise and treat all other functions, including the impl of eq (used in remove_slice_eq), the core::array::from_fn, purely mono functions. This is safe and straightforward while with the explicit sacrifice that some passes like the above two are not going to work for mono codes. But as they are fully monomorphised, it should not be hard to provide manual implementation.
3. (Neutral) For just the eq case, there is an ugly trick of only allowing such to be re-polymorphised and the trait-refs to be collected. But I've confirmed that from_fn will trigger error with this partially allowance. It means we will have to manually implement from_fn.

[ssyram]

Besides, there still seems to be the No rule to make target 'test-array', needed by 'custom-test-array' issue. So, I have fully tested and confirmed the problems solely for the C cases but could not yet confirm the Cpp cases.

[ssyram]

Summary of current status: All C cases have been tested and fixed, except the following:

• array: Wait for Translating rust array type [T;C] into struct arr { T[C] data; }  #252 to fix.
• dst: Wait for Explicit Unsized Metadata & Unified DST Handling #259 to fix.
• fn_higher_order & nested_arrays: to fix the loop resugarring -- @protz the error message of cremepat is quite confusing, if it is a quick fix, would you please have a look? Please note to apply AstOfLlbc.re_polymorphize.
• issue_49, issue_105, issue_123, step_by, symcrust, where_clauses_fncg: they are all Charon bugs to be fixed, as reported in Bug: A Couple of Mono Bugs Found in Eurydice charon#822 .

[Nadrieril]

Note: AeneasVerif/charon#854 changes how we represent monomorphized names a tiny bit. For your purposes, you'll just have to add a few .binder_value and that's all.