Bug: Type dependencies not resolved

[ssyram]

Now Eurydice might generate codes having a wrong order in the types. I.e., there might be cases:

typedef struct Option_hash { Option_hash_tags tag; InternalTyp f0; }

But the internal type InternalTyp is defined below this type Option_hash.

This becomes obvious and troublesome to handle when translating large scale programs.

We suggest the following plan for handling type declarations:

• Firstly, collect all the possible types, and have them all declared forwardly;
• Then, we collect the actual type dependencies in the types and print the types in topological order by the dependency tree.

[Nadrieril]

Note that Charon already computes the complete dependencies between all items and sorts them in an order that is deterministic, topological, and resembles the order they were written in. This can be found in translated.reordered_decls.

[ssyram]

Thanks, we will firstly have a try to see if this order works! A potential point may be that the mutually dependent types should have preceding declarations and the one not using the pointer type should get the latter position. But the pointer type stuff might be rather complex to explore in Charon?

E.g., A has a pointer of B and B has a field of type A. Then there should be a forwarding type declaration of B, followed by the definition of A and then definition of B.

[Nadrieril]

Mutually dependent items are regrouped in a GDeclarationGroup::Rec which contains the whole connected component. It is up to the consumer to decide how to resolve such a loop. Presumably in your case you'll always want to emit the type decls before the functions/trait decls, and then among type decls you'll do your forward decl thing?

[Nadrieril]

I guess this will require you to do a bit of topological ordering yourself 🤔 I agree it would be easier if Charon did it, and I agree that this does not seem like the type of thing it would make sense for Charon to do, it feels too specific to this usecase.

[protz]

But the internal type InternalTyp is defined below this type Option_hash.

Can you clarify whether the generated code is incorrect, or could be better?

@Nadrieril Eurydice performs many topological sorts and reorderings so no point on doing it on the Charon side, it would be redone anyhow

[ssyram]

Yes, we should place the definition of the internal type before that Option definition. And now we are experiencing many such problems in our internal project. We think the above algorithms should resolve this and thank @Nadrieril for his info. But there still seems to be necessary to apply the algorithm within each group.

[protz]

So the generated code does not compile?

Can you send a repro?

[ssyram]

Yes, they cannot compile... But I'm afraid the codes are private, so the reproduction is hard...

So basically if there is no mechanism to guarantee the correct order, this could naturally happen in real-world codes?

[protz]

https://github.com/AeneasVerif/eurydice/blob/main/lib/Bundles.ml#L358

this is supposed to do a topological sort

so probably this is not working as intended

[ssyram]

Yes, I think so. And the codes do not seem to handle the complex situation as mentioned.