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

Relax the Symbol requirement to ConstBlockAddr #87

Merged
merged 3 commits into from
Oct 13, 2021

Conversation

Ptival
Copy link
Contributor

@Ptival Ptival commented Oct 7, 2021

As part of an attempt to fix GaloisInc/llvm-pretty-bc-parser#149 , I believe we may need some version of ConstBlockAddr that is more lazy in the symbol.

That is, the value of the symbol field is a forward reference, and eagerly trying to evaluate it leads to an infinite loop.

I am not very familiar with either code bases, so I don't know whether this is the recommended way of solving such issues, but I can at least confirm that such a constructor helps with that problem.

I'd also like to make sure that this:

https://github.com/elliottt/llvm-pretty/blob/5a821ad50edc33047c75311b7d7b31bd5fc52c21/src/Text/LLVM/Labels.hs#L118

does the right generic thing corresponding to what happens here:

https://github.com/elliottt/llvm-pretty/blob/5a821ad50edc33047c75311b7d7b31bd5fc52c21/src/Text/LLVM/Labels.hs#L140

Works like `ValConstExpr (ConstBlockAddr sym bid)`, except the `sym` is left as
an expression to be resolved later.
Copy link
Collaborator

@elliottt elliottt left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The Symbol on ConstBlockAddr is already not strict, why does adding this new constructor help? Is the value represented different from ValConstExpr (ConstBlockAddr sym lab)?

@Ptival
Copy link
Contributor Author

Ptival commented Oct 11, 2021

Sorry, my use of the word lazy was misleading.

The problem as I understand it is that in order to put a Symbol-typed expression there, the parser has to run elimValSymbol (typedValue (forwardRef ctx valref t)), a computation whose spine depends on the result of its sub-expression:

https://github.com/elliottt/llvm-pretty/blob/641ae933652369cf0d7e1e47c8928f631fb71858/src/Text/LLVM/AST.hs#L1041-L1043

So we would either need a way of having a Symbol-typed value that has delayed its forward reference evaluation, or we need some way to store something other than a Symbol giving us evaluation flexibility. Does this make sense?

@elliottt
Copy link
Collaborator

Yep, this makes sense to me. What do you think about changing ConstBlockAddr to no longer take a Symbol, and instead take a Typed (Value' lab) for the symbol part? That would mean that you could remove the use of elimValSymbol when parsing, and validate that the argument is a symbol at a later stage once you're no longer in a context where the symbol might be defined lazily.

@elliottt
Copy link
Collaborator

An alternative approach would be to make a partial version of elimValSymbol, which would mean that you could decouple the check that it's a symbol from the sequencing of the Parse monad. Up to you about which seems like the better approach here, debugging lazy values with errors can be a bit of a trial, but I think there are other cases where that's done already in llvm-pretty-bc-parser.

@Ptival
Copy link
Contributor Author

Ptival commented Oct 11, 2021

I like the first approach. I think I was worried that Const meant I shouldn't put expressions in there, but looking back, there are already many Typed (Value' lab) in there. Will update!

@Ptival
Copy link
Contributor Author

Ptival commented Oct 11, 2021

This trick no longer works:

https://github.com/elliottt/llvm-pretty/blob/641ae933652369cf0d7e1e47c8928f631fb71858/src/Text/LLVM/Labels.hs#L140

Is the generic instance good enough, or ought this really evaluate the symbol to be able to call f on l?

@elliottt
Copy link
Collaborator

You could match on the typed value to call out the special case when a symbol is present, and otherwise fall back on the generic instance.

@elliottt
Copy link
Collaborator

However this might introduce additional strictness that could break what you're going for here. The difficulty is that the relabeling needs to know that the label comes from a different function, but the only mechanism to signal that is when the symbol value is present. I don't remember when the relabeling occurs in llvm-pretty-bc-parser, but that would be a good thing to check to determine if this is a change that would make sense.

@Ptival
Copy link
Contributor Author

Ptival commented Oct 11, 2021

The updated version seems to solve my problems and not blow up in any of my examples!

@elliottt elliottt changed the title add ValBlockAddr Relax the Symbol requirement to ConstBlockAddr Oct 13, 2021
@elliottt elliottt merged commit 15bc003 into GaloisInc:master Oct 13, 2021
@Ptival Ptival deleted the vr/val-block-addr branch October 13, 2021 18:28
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Oct 25, 2021
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Dec 5, 2021
This bumps the `llvm-pretty` submodule to bring in the following PRs:

* GaloisInc/llvm-pretty#86 (support LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty#87 (Relax the Symbol requirement to `ConstBlockAddr`)
* GaloisInc/llvm-pretty#88 (add LLVM12 poison value)

This also bumps the `llvm-pretty-bc-parser` submodule to bring in the
following PRs:

* GaloisInc/llvm-pretty-bc-parser#171 (don't consume fast math flag entry)
* GaloisInc/llvm-pretty-bc-parser#169 (make `getBitString` assumptions explicit)
* GaloisInc/llvm-pretty-bc-parser#168 (support for LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty-bc-parser#170 (remove `Aligned` from `SubWord`)
* GaloisInc/llvm-pretty-bc-parser#172 (fix BLOCKADDRESS parsing)
* GaloisInc/llvm-pretty-bc-parser#173 (parse LLVM12 poison value)
* GaloisInc/llvm-pretty-bc-parser#178 (use Seq over list in PartialModule)

Of these, the only PR that requires code changes in Crucible is
GaloisInc/llvm-pretty#88 (add LLVM12 poison value), as this adds a new
`ValPoison` constructor to `Value'`. Properly handling LLVM poison is a large
task that I do not wish to tackle here (see #366 for discussion of how one
might do this). For now, this PR does the bare minimum:

* In `Lang.Crucible.LLVM.Translation.BlockInfo.useVal`, treat `ValPoison`
  as not referencing any identifiers.
* The other two potential sites where `ValPoison` could be matched on are in
  `Lang.Crucible.LLVM.Translation.Constant.transConstant'` and
  `Lang.Crucible.LLVM.Translation.Expr.transValue`. Since we are not handling
  `ValPoison` for now, both of these functions will simply error if they
  encounter `ValPoison`.
* I have added a section to `crucible-llvm`'s `limitations.md` document which
  describes the above limitations of poison handling.
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Dec 6, 2021
This bumps the `llvm-pretty` submodule to bring in the following PRs:

* GaloisInc/llvm-pretty#86 (support LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty#87 (Relax the Symbol requirement to `ConstBlockAddr`)
* GaloisInc/llvm-pretty#88 (add LLVM12 poison value)
* GaloisInc/llvm-pretty#90 (Support structs with bitfields in `Text.LLVM.DebugUtils`)

This also bumps the `llvm-pretty-bc-parser` submodule to bring in the
following PRs:

* GaloisInc/llvm-pretty-bc-parser#171 (don't consume fast math flag entry)
* GaloisInc/llvm-pretty-bc-parser#169 (make `getBitString` assumptions explicit)
* GaloisInc/llvm-pretty-bc-parser#168 (support for LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty-bc-parser#170 (remove `Aligned` from `SubWord`)
* GaloisInc/llvm-pretty-bc-parser#172 (fix BLOCKADDRESS parsing)
* GaloisInc/llvm-pretty-bc-parser#173 (parse LLVM12 poison value)
* GaloisInc/llvm-pretty-bc-parser#178 (use Seq over list in PartialModule)

Of these, the only PR that requires code changes in Crucible is
GaloisInc/llvm-pretty#88 (add LLVM12 poison value), as this adds a new
`ValPoison` constructor to `Value'`. Properly handling LLVM poison is a large
task that I do not wish to tackle here (see #366 for discussion of how one
might do this). For now, this PR does the bare minimum:

* In `Lang.Crucible.LLVM.Translation.BlockInfo.useVal`, treat `ValPoison`
  as not referencing any identifiers.
* The other two potential sites where `ValPoison` could be matched on are in
  `Lang.Crucible.LLVM.Translation.Constant.transConstant'` and
  `Lang.Crucible.LLVM.Translation.Expr.transValue`. Since we are not handling
  `ValPoison` for now, both of these functions will simply error if they
  encounter `ValPoison`.
* I have added a section to `crucible-llvm`'s `limitations.md` document which
  describes the above limitations of poison handling.
RyanGlScott added a commit to GaloisInc/crucible that referenced this pull request Dec 6, 2021
This bumps the `llvm-pretty` submodule to bring in the following PRs:

* GaloisInc/llvm-pretty#86 (support LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty#87 (Relax the Symbol requirement to `ConstBlockAddr`)
* GaloisInc/llvm-pretty#88 (add LLVM12 poison value)
* GaloisInc/llvm-pretty#90 (Support structs with bitfields in `Text.LLVM.DebugUtils`)

This also bumps the `llvm-pretty-bc-parser` submodule to bring in the
following PRs:

* GaloisInc/llvm-pretty-bc-parser#171 (don't consume fast math flag entry)
* GaloisInc/llvm-pretty-bc-parser#169 (make `getBitString` assumptions explicit)
* GaloisInc/llvm-pretty-bc-parser#168 (support for LLVM 11 `IsDefault` fields in metadata)
* GaloisInc/llvm-pretty-bc-parser#170 (remove `Aligned` from `SubWord`)
* GaloisInc/llvm-pretty-bc-parser#172 (fix BLOCKADDRESS parsing)
* GaloisInc/llvm-pretty-bc-parser#173 (parse LLVM12 poison value)
* GaloisInc/llvm-pretty-bc-parser#178 (use Seq over list in PartialModule)

Of these, the only PR that requires code changes in Crucible is
GaloisInc/llvm-pretty#88 (add LLVM12 poison value), as this adds a new
`ValPoison` constructor to `Value'`. Properly handling LLVM poison is a large
task that I do not wish to tackle here (see #366 for discussion of how one
might do this). For now, this PR does the bare minimum:

* In `Lang.Crucible.LLVM.Translation.BlockInfo.useVal`, treat `ValPoison`
  as not referencing any identifiers.
* The other two potential sites where `ValPoison` could be matched on are in
  `Lang.Crucible.LLVM.Translation.Constant.transConstant'` and
  `Lang.Crucible.LLVM.Translation.Expr.transValue`. Since we are not handling
  `ValPoison` for now, both of these functions will simply error if they
  encounter `ValPoison`.
* I have added a section to `crucible-llvm`'s `limitations.md` document which
  describes the above limitations of poison handling.
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.

Error when parsing Linux kernel compiled with LLVM 8
2 participants