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

Add extern attribute and captureState attribute to pass binary locations to boogie for better debugging #131

Merged
merged 11 commits into from
Nov 1, 2023

Conversation

ailrst
Copy link
Contributor

@ailrst ailrst commented Oct 27, 2023

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

  • Add BAssume to the boogie AST.
  • Add attributes to boogie commands and definitions
  • Add extern attribute to generated definitions
  • Add address to store ops in the BAP AST and load them from the adt file
  • Add address to store ops in IL
  • Add assert {:captureState "addr:0xxxx"} true to the end of store ops in generated boogie, and to the beginning of basic blocks
  • Changes IL statements to case classes; I feel like its likely there was a reason they weren't already case classes, please let me know if its a problem and I'll put them back.

@ailrst ailrst changed the title Add extern attribute and assumes with binary location captureState attribute Add extern attribute and captureState attribute to pass binary locations to boogie for better debugging Oct 27, 2023
@ailrst ailrst requested a review from l-kent October 30, 2023 00:21
@l-kent
Copy link
Contributor

l-kent commented Oct 30, 2023

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.

@ailrst
Copy link
Contributor Author

ailrst commented Oct 30, 2023

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.)

Yeah I agree that would be better I'll have a look at how much work it is to incorporate that instead.

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?

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.

I don't think the {:extern} attribute on an axiom even does anything either, as axioms don't have an identifier to override?

Yeah that's a mistake, thanks.

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.

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.

Copy link
Contributor

@l-kent l-kent left a 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.

src/main/scala/specification/Specification.scala Outdated Show resolved Hide resolved
src/main/scala/ir/Statement.scala Outdated Show resolved Hide resolved
@l-kent l-kent self-requested a review November 1, 2023 02:50
@ailrst ailrst merged commit a14ddea into main Nov 1, 2023
1 check passed
@ailrst ailrst deleted the extra-attributes branch November 6, 2023 23:52
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.

2 participants