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

Update deps #1489

Merged
merged 9 commits into from
Oct 27, 2021
Merged

Update deps #1489

merged 9 commits into from
Oct 27, 2021

Conversation

brianhuffman
Copy link
Contributor

No description provided.

@brianhuffman brianhuffman added the PR: submodule bump Pull requests that include a submodule bump label Oct 25, 2021
@brianhuffman brianhuffman added the PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run label Oct 26, 2021
@brianhuffman
Copy link
Contributor Author

I did add one FIXME to this PR, in SAWScript/Crucible/LLVM/MethodSpecIR.hs, saying that we should eventually do something with any translation warnings that may now be returned by the LLVM-to-Crucible translation. I figured we could open a separate ticket to track that tech debt.

@robdockins
Copy link
Contributor

It looks like the test failures are all due to the new def/use analysis claiming that some LLVM virtual register use is not properly dominated by its definition. That suggests to me that there is some bug causing the analysis to be too conservative.

@brianhuffman
Copy link
Contributor Author

Well, it looks like I get to spend another afternoon doing builds and tests. I'll bisect and see where this failure was introduced.

@robdockins
Copy link
Contributor

robdockins commented Oct 26, 2021

I'm pretty confident it's due to GaloisInc/crucible#886 (in fact, this commit is probably the proximate cause GaloisInc/crucible@c914655)

I'm taking a look at the involved bitcode files now to see if there is an obvious cause.

@robdockins
Copy link
Contributor

robdockins commented Oct 26, 2021

The two cases I've found that are causing trouble are both 1) generated from rust code and 2) involve the return value of an invoke instruction. I think the problem is that invoke is an unusual instruction that is both a block terminator and can define a virtual register; probably it is not being handled correctly.

EDIT: indeed, I'll have to fix this case. The use sets of arguments to invoke and the use sets of the blocks it jumps to are treated the same; however, they need to be handled differently, as the normal return successor block should have the result of the invoke in scope.

@robdockins
Copy link
Contributor

I think that GaloisInc/crucible#895 should resolve this problem.

@brianhuffman
Copy link
Contributor Author

I just reordered some commits and force-pushed a branch without the offending crucible update. I'll test GaloisInc/crucible#895 on top of that separately.

Copy link
Contributor

@robdockins robdockins left a comment

Choose a reason for hiding this comment

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

I don't have any real context for the Macaw changes, but this seems OK to me.

@brianhuffman
Copy link
Contributor Author

I talked separately with @travitch specifically about adapting to GaloisInc/macaw#226, and he agreed that using unsupportedSyscalls was the right thing to do there.

@brianhuffman
Copy link
Contributor Author

It looks like a couple of tests have failed due to failure to download yices. I'll restart the tests and hopefully they'll work without changes.

@mergify mergify bot merged commit 9ddb617 into master Oct 27, 2021
@mergify mergify bot deleted the update-deps branch October 27, 2021 18:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
PR: ready to merge Magic flag for pull requests to ask Mergify to merge given an approval and a successful CI run PR: submodule bump Pull requests that include a submodule bump
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants