Αρχιτεκτονική προσέγγιση και σκοπιμότητα

Σε αντίθεση με τους παραδοσιακούς compilers που στοχεύουν στη βελτιστοποίηση για το hardware, το Eurydice εστιάζει στη διατήρηση της αναγνωσιμότητας και της δομής του κώδικα. Αυτό είναι κρίσιμο για τομείς όπως η κρυπτογραφία και το λογισμικό υψηλής διασφάλισης, όπου ο κώδικας πρέπει να υποβληθεί σε ελέγχους από εργαλεία τυπικής επαλήθευσης (formal verification) που είναι σχεδιασμένα αποκλειστικά για C.

Η διαδικασία μετατροπής και το pipeline

Το Eurydice δεν υλοποιεί δικό του parser. Αντ' αυτού, αξιοποιεί το εργαλείο Charon για να εξάγει το MIR από τον rustc σε μορφή JSON. Στη συνέχεια, μετατρέπει αυτή την αναπαράσταση σε μια ενδιάμεση μορφή που χρησιμοποιείται από το KaRaMeL, το οποίο αναλαμβάνει την τελική παραγωγή του κώδικα C. Η διαδικασία περιλαμβάνει μια σειρά από passes που αφαιρούν στοιχεία ειδικά για τη Rust, όπως iterators ή πολύπλοκα generics.

Προκλήσεις και περιορισμοί

Η μεταγλώττιση από μια γλώσσα με πλούσιο σύστημα τύπων σε μια πιο περιορισμένη όπως η C παρουσιάζει σημαντικές δυσκολίες:

  • Monomorphization: Η έλλειψη generics στη C αναγκάζει το Eurydice να παράγει πολλαπλές εκδόσεις συναρτήσεων.
  • Strict Aliasing: Για τη διαχείριση δυναμικών τύπων, το εργαλείο παράγει διαφορετικές αναπαραστάσεις που ενδέχεται να παραβιάζουν τους κανόνες strict-aliasing της C, καθιστώντας απαραίτητη τη χρήση του flag -fno-strict-aliasing.
  • Scalability: Προς το παρόν, το εργαλείο δυσκολεύεται με σύγχρονα χαρακτηριστικά της Rust, όπως τα const generics, περιορίζοντας τη χρήση του σε μικρότερα, αυτοτελή προγράμματα.