Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[c-parser] remove continue statement #85

Closed
wants to merge 2 commits into from

Conversation

isubasinghe
Copy link

@isubasinghe isubasinghe commented Nov 28, 2023

I needed to make this change to make the C-parser accept the code.
Not entirely sure why the C-parser blew up when it saw the continue statement, I am unsure if this is a bug in the C-parser or just not supported by it.

@isubasinghe isubasinghe changed the title fix: remove continue statement to get c-parser to accept output [c-parser] remove continue statement Nov 28, 2023
Signed-off-by: isubasinghe <[email protected]>
@Ivan-Velickovic
Copy link
Collaborator

I'd like to understand why continue is not supported/working first.

@isubasinghe
Copy link
Author

I'd like to understand why continue is not supported/working first.

Yeah sounds good, I think @lsf37 might know the answer to this, I'll leave this as it is until Gerwin returns from leave and addresses this.

@Xaphiosis
Copy link
Member

It would be helpful to see how it "blew up". The C parser itself does support continue, at least as much as is seen in https://github.com/seL4/l4v/blob/master/tools/c-parser/testfiles/breakcontinue.c
There might be an interplay here between the continue, switch and break in some manner, but I'm just guessing via a quick glance at the diff

@isubasinghe
Copy link
Author

It would be helpful to see how it "blew up". The C parser itself does support continue, at least as much as is seen in https://github.com/seL4/l4v/blob/master/tools/c-parser/testfiles/breakcontinue.c There might be an interplay here between the continue, switch and break in some manner, but I'm just guessing via a quick glance at the diff

Ah thanks for the comment, not entirely sure what caused it to error out, I just bisected through the code until I found out that rewriting the continue statement makes the C parser accept the C code.

I will try and get more helpful output next week and update here, got a bunch of deadlines to worry about this week.

@Ivan-Velickovic
Copy link
Collaborator

Did we find out what the problem was?

@lsf37
Copy link
Member

lsf37 commented Jan 27, 2024

continue is definitely supported, so it would be good to figure out what is going on. This change seems to be doing a whole lot of other stuff too, though. Could it be somewhere in there?

@isubasinghe
Copy link
Author

Sorry this is on my (fairly large) todo list.
All the information I have for now is this:

When all the debug related functions and statements were stripped out, the C parser did end up working.
I cannot give an estimate as to when I will get back to this issue, this is somewhat low priority for me until the March deadline is over with.

@lsf37
Copy link
Member

lsf37 commented Jan 27, 2024

Sorry this is on my (fairly large) todo list. All the information I have for now is this:

When all the debug related functions and statements were stripped out, the C parser did end up working.

That makes more sense -- I don't know how putc is defined/handled, but we are avoiding string literals and printing in the kernel, so at least those kinds of things would be much less tested. Would still be good to figure it out at some point.

I cannot give an estimate as to when I will get back to this issue, this is somewhat low priority for me until the March deadline is over with.

Ok, no hurry.

@isubasinghe
Copy link
Author

When all the debug related functions and statements were stripped out, the C parser did end up working.

This statement was incorrect, apologies, it was a while since I looked at this, the issue isn't actually with the C parser but the translation to GraphLang.

I've added the program here: https://gist.github.com/isubasinghe/b8fb5abb5db9b6c769ad97c3e2b63866

Here is the export script: https://gist.github.com/isubasinghe/0a568ff2060443b8b43bf23474c37c55

@Ivan-Velickovic
Copy link
Collaborator

Closing because @isubasinghe won't be pursuing this anymore and we are likely looking at a change to verification tooling that would not need this patch.

If we do need it we can always re-open.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants