-
Notifications
You must be signed in to change notification settings - Fork 0
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 extern attribute and captureState attribute to pass binary locations to boogie for better debugging #131
Conversation
Rather than using the address field for the captureState assumes, I'd suggest using the 'line' field from the BAP instead (this is '%000006af' etc.) - I think it's more useful because it directly be compared to the .bir as well as the .adt files. BAP also doesn't give an address for everything, since the statements that are generated by BAP's basic analysis rather than having directly existed in the binary can't have addresses. I don't really like the generalised attributes approach - different attributes only meaningfully apply to certain things in Boogie, so I'd prefer to keep things specific and only have the options for relevant attributes? I don't think the {:extern} attribute on an axiom even does anything either, as axioms don't have an identifier to override? The IR doesn't use case classes for most of the classes because they contain mutable data. Case classes are only really designed to hold immutable data. |
Yeah I agree that would be better I'll have a look at how much work it is to incorporate that instead.
Yeah, I guess this implementation doesn't prevent you from setting attributes that aren't meaningful in the context, its just a non-trivial amount of refactoring to add in any new attribute, plus it requires another field for each one. I prefer to have a list like this for that convenience. If we really want to I'd define the attributes an enum and the attribute list key as a union of the allowed values.
Yeah that's a mistake, thanks.
Cool makes sense, I'll see if I can define an extractor for pattern matching since that would be convenient for this, and also for writing more complex visitors in the future. |
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.
This is fine to merge once you've fixed these minor issues and then updated the expected files again.
This PR is to pass binary instruction addresses all the way through so that boogie's
/mv
flag can split the counterexample into states for us for #127.To do this it adds attributes and assumes to the Boogie AST.
Changes
BAssume
to the boogie AST.assert {:captureState "addr:0xxxx"} true
to the end of store ops in generated boogie, and to the beginning of basic blocks