search

AeneasVerif / charon

Interface with the rustc compiler for the purpose of program verification
https://aeneasverif.github.io/charon/charon_lib/index.html
Apache License 2.0
103 stars 17 forks source link

FInd a simple way of updating code which uses patterns #219

Open sonmarcho opened 5 months ago

sonmarcho commented 5 months ago

We regularly need to update the patterns which are used to catch specific definitions. This is a very manual and tedious process, and will definitely not scale as we add more and more definitions to our standard libraries. We should find a way of easily updating code which relies on patterns.

So far I think a possibility would be to write a small library which uses the old and the most recent version of Charon-ML as dependencies (not sure how to do that precisely, but there must be at least a hacky way). We would then catch the definitions which match the old patterns and patterns which match definitions according to the new version of the code to generate a mapping from old patterns to new patterns.

Nadrieril commented 5 months ago

What do you mean by "patterns"? Patterns of code like we match in our micro-passes, or patterns in the paths of items, or something else? And by "we", do you mean Charon, Aeneas, or our users?

sonmarcho commented 5 months ago

Patterns are the patterns in the paths of items. By "we" I mean the users (that is, Aeneas and Eurydice) who need to use those patterns to identify some definitions.

Nadrieril commented 5 months ago

What causes the paths to change?