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.

Sign up for GitHub

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

Jump to bottom

crucible-llvm: Annotate errors with call stacks #914

Merged
merged 2 commits into from
Nov 16, 2021
Merged

crucible-llvm: Annotate errors with call stacks #914

merged 2 commits into from
Nov 16, 2021

Conversation

langston-barrett
Copy link
Contributor

@langston-barrett langston-barrett commented Nov 6, 2021 •
edited
Loading

Still WIP, since:

  • There are probably other projects in this repo that will need changes to typecheck
  • The Crux-LLVM golden tests are probably failing
  • Most importantly: There's a spot where I could use help on how to proceed (see inline comment)

@robdockins
Copy link
Contributor

Glancing through the code, I don't see where the callstacks are generated from. Are they just compute from the sequence of pushed frames in the memory?

@robdockins
Copy link
Contributor

This PR highlights something that I think we'll need to address going forward as we refactor the memory model. Right now, the memory is tightly coupled with a program's control flow via the StackFrame and BranchFrame constructors. If we ever want to take concurrency seriously, we'll need to decouple these concepts, as control flow is an essentially thread-local concept.

@langston-barrett
crucible-llvm: Thread memory variable through LLVM exprs
6cf26f4 
This isn't useful on its own, but will support later commits which will annotate
structured LLVM errors with callstacks.
@langston-barrett langston-barrett force-pushed the lb/llvm-callstack branch 4 times, most recently from fee59a5 to 388ef83 Compare November 11, 2021 22:14
@langston-barrett langston-barrett marked this pull request as ready for review November 11, 2021 22:31
@langston-barrett
Copy link
Contributor Author

The only remaining CI failure seems unrelated (it's during installation of Nix).

@RyanGlScott
Copy link
Contributor

it's during installation of Nix

Sigh. It looks like NixOS/nix#3605 is biting again.

@langston-barrett langston-barrett merged commit 4f81a72 into master Nov 16, 2021
@langston-barrett langston-barrett deleted the lb/llvm-callstack branch November 16, 2021 16:03
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Nov 23, 2021
@RyanGlScott
Adapt to GaloisInc/crucible#914
7e0db49 
This bumps the `crucible` submodule to include GaloisInc/crucible#914. This
also bumps the `macaw` submodule to include GaloisInc/macaw#244, which adapts
`macaw-symbolic` to the `crucible` changes. These `crucible` changes require
some tweaks in the following libraries:

* In `heapster-saw`, we need to add a `NuMatching1` instance for `GlobalVar`
  now that `LLVM_SideConditions` has a field of type `GlobalVar Mem`. This
  also requires defining an opaque `NuMatching` instance for `Nonce` to support
  the `NuMatching1` instance for `GlobalVar`.

  Elsewhere in `heapster-saw`, we need to adapt a pattern match on
  `LLVM_SideConditions` to accommodate its new field.
* In `saw-script`, we need to make sure that `?recordLLVMAnnotation` is given
  three arguments, not two, so that its type matches what `HasLLVMAnn` expects.
@RyanGlScott RyanGlScott mentioned this pull request Nov 23, 2021
Merged
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Nov 29, 2021
@RyanGlScott
Adapt to GaloisInc/crucible#914
cfb08e7 
This bumps the `crucible` submodule to include GaloisInc/crucible#914. This
also bumps the `macaw` submodule to include GaloisInc/macaw#244, which adapts
`macaw-symbolic` to the `crucible` changes. These `crucible` changes require
some tweaks in the following libraries:

* In `heapster-saw`, we need to add a `NuMatching1` instance for `GlobalVar`
  now that `LLVM_SideConditions` has a field of type `GlobalVar Mem`. This
  also requires defining an opaque `NuMatching` instance for `Nonce` to support
  the `NuMatching1` instance for `GlobalVar`.

  Elsewhere in `heapster-saw`, we need to adapt a pattern match on
  `LLVM_SideConditions` to accommodate its new field.
* In `saw-script`, we need to make sure that `?recordLLVMAnnotation` is given
  three arguments, not two, so that its type matches what `HasLLVMAnn` expects.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Dec 3, 2021
@RyanGlScott
Adapt to GaloisInc/crucible#914
0cc4525 
This bumps the `crucible` submodule to include GaloisInc/crucible#914. This
also bumps the `macaw` submodule to include GaloisInc/macaw#244, which adapts
`macaw-symbolic` to the `crucible` changes. These `crucible` changes require
some tweaks in the following libraries:

* In `heapster-saw`, we need to add a `NuMatching1` instance for `GlobalVar`
  now that `LLVM_SideConditions` has a field of type `GlobalVar Mem`. This
  also requires defining an opaque `NuMatching` instance for `Nonce` to support
  the `NuMatching1` instance for `GlobalVar`.

  Elsewhere in `heapster-saw`, we need to adapt a pattern match on
  `LLVM_SideConditions` to accommodate its new field.
* In `saw-script`, we need to make sure that `?recordLLVMAnnotation` is given
  three arguments, not two, so that its type matches what `HasLLVMAnn` expects.
RyanGlScott added a commit to GaloisInc/saw-script that referenced this pull request Dec 6, 2021
@RyanGlScott
Merge pull request #1521 from GaloisInc/crucible-submod-bump
96272c0 
Submodules: Adapt to GaloisInc/crucible#914, GaloisInc/crucible#906, and GaloisInc/crucible#928
@RyanGlScott RyanGlScott mentioned this pull request May 9, 2022
Closed
RyanGlScott added a commit that referenced this pull request May 9, 2022
@RyanGlScott
crux-llvm: Fix test suite with Clang 12
22a4adb 
Fixing `T847-fail2` is as simple as accepting the new output resulting from
#914.

Fixing `invoke-test` requires updating the LLVM to use `sret` syntax specific
to LLVM 12 or later. (See
https://releases.llvm.org/12.0.0/docs/LangRef.html#parameter-attributes).
As a result, this test is now only ran on Clang 12 or later.

Fixes #977.
@RyanGlScott RyanGlScott mentioned this pull request May 9, 2022
Merged
RyanGlScott added a commit that referenced this pull request May 10, 2022
@RyanGlScott
crux-llvm: Fix test suite with Clang 12 (#979)
b0d1580 
Fixing `T847-fail2` is as simple as accepting the new output resulting from
#914.

Fixing `invoke-test` requires updating the LLVM to use `sret` syntax specific
to LLVM 12 or later. (See
https://releases.llvm.org/12.0.0/docs/LangRef.html#parameter-attributes).
As a result, this test is now only ran on Clang 12 or later.

Fixes #977.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@robdockins robdockins robdockins approved these changes

Assignees
No one assigned
Labels
llvm
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@langston-barrett @robdockins @RyanGlScott