Support for trait clause bounds #11
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Rather than having a hidden invariant, the translation from LLBC to krml's internal AST now repeats the const generic binders within expression binders too -- this aligns with what krml does. This change also introduces a new kind of binder, which will act as a stand-in for additional function parameters intended to hold trait clause methods.
… better, add more things to the blocklist to get unblocked
msprotz
commented
May 18, 2024
| @@ -172,6 +213,25 @@ module RustNames = struct | |||
| let from = | |||
| parse_pattern "core::convert::From<@T, @U>::from" | |||
|
|
|||
| let into_u16 = | |||
There was a problem hiding this comment.
@W95Psp I heard from @sonmarcho that there is a better, more concise way to do this, so this would be another interesting mini-task to add onto this PR -- refactor this bit to have more effective matching logic here, and in the main expression translation function
…' into protz_trait_clauses
sonmarcho
reviewed
May 21, 2024
| @@ -172,6 +213,25 @@ module RustNames = struct | |||
| let from = | |||
| parse_pattern "core::convert::From<@T, @U>::from" | |||
|
|
|||
| let into_u16 = | |||
| @@ -868,16 +1181,30 @@ let rec expression_of_raw_statement (env: env) (ret_var: C.var_id) (s: C.raw_sta | |||
| Krml.Helpers.with_unit K.(EAssign (dest, maybe_addrof env ty (with_type t (EBufRead (e1, e2))))) | |||
|
|
|||
| | Call { func = FnOpRegular fn_ptr; args; dest; _ } | |||
| when false && Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from fn_ptr -> | |||
| when ( | |||
| Charon.NameMatcher.match_fn_ptr env.name_ctx RustNames.config RustNames.from_u16 fn_ptr || | |||
There was a problem hiding this comment.
There was a problem hiding this comment.
Created #20 as a followup
| else if matches RustNames.from_i16 then Int16 | ||
| else if matches RustNames.from_i32 then Int32 | ||
| else if matches RustNames.from_i64 then Int64 | ||
| if matches RustNames.from_u16 || matches RustNames.into_u16 then UInt16 |
W95Psp
reviewed
May 21, 2024
…dice into protz_trait_clauses
…d still have the same signature -- add dummy cg parameters
…hecking and support for strings
…mensional arrays on the stack, and as top-level constants. This fixes #15
|
I'm merging this and opened #20 to track the specific issue of improving the name matcher logic. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This isn't quite working yet but I want to get this in place to start working through the code with @W95Psp.This is now on-par with what used to work before.
Let's try to block some time to go over this once you've had a chance to browse the list of changes. I've tried to add comments whenever I could, so hopefully some of this makes sense? Thanks!!