-
Notifications
You must be signed in to change notification settings - Fork 20
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
Add support for parsing asm goto
#92
Conversation
@@ -1044,6 +1044,7 @@ and instr = | |||
(string option * string * exp) list * | |||
(* inputs with optional names and constraints *) | |||
string list * (* register clobbers *) | |||
string list) option * (* goto locations *) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's not clear from here, why this additional option
wrapping is necessary or what the None
then means.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we should also add tests here so we don't accidently break support in the future.
@@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self) | |||
|
|||
method! vinst i = | |||
let handle_inst iosh i = match i with | |||
| Asm(_,_,slvl,_,_,_) -> List.iter (fun (_,s,lv) -> | |||
| Asm(_,_,Some(slvl,_,_,_),_) -> List.iter (fun (_,s,lv) -> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is just ignoring the None
case the same that we would have had for the dummy statement before?
@@ -102,7 +102,7 @@ class usedDefsCollectorClass = object(self) | |||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Commenting here since I can only comment on the diff: We should check if these zrapp
analysis potentially break after this change (quite likely).
Unless we're super sure that they don't break, we should comment that they assume no asm gotos
. We mostly have these for historical reasons anyway (came from original CIL), so it's not worth adding proper handling here (as our focus is on Goblint).
Nevertheless, let's add comments that make it clear we have not patched them to support these new constructs.
@@ -1692,4 +1693,17 @@ asmcloberlst_ne: | |||
| one_string_constant COMMA asmcloberlst_ne { $1 :: $3 } | |||
; | |||
|
|||
asmgoto: | |||
/* empty */ { [] } | |||
| COLON asmgotolst { $2 } |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
is just COLON
a valid asmgoto
?
Once we get the remaining open issues addressed, I think it make sense to merge this, even if Goblint will trail behind for a bit, i.e., while the better handling of asm is not yet merged into Goblint. |
I wouldn't rush this so much, but would wait until we have some Goblint PR ready to handle the change to |
Closing in favor of PR to be created by students from the Goblint practical which will address this issue in a principled way. |
Implements parsing of
asm goto
statements for #81 and tracking if a asm statement is basic or advanced as required for my thesis.This change requires bottbenj/analyzer@e3af268 in analyzer.
This currently doesn't handle the controlflow resulting from an
asm goto
but should be sufficient for parsing projects that happen to contain such statements.