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

[VCLLVM] Add partial contract support for LLVM #1034

Merged
merged 8 commits into from
Jun 28, 2023
Merged

Conversation

Drevanoorschot
Copy link
Contributor

This PR adds function contract support for LLVM programs. It's not entirely finished and there are still some issues. However, it compiles and to prevent future merge conflicts, I felt like it would be best to create this PR anyway.

Some of the issues/notes:

  • When using the \result keyword, the AmbigiousResult.ref reference is never set. I'm not sure why this is or where the reference assignment is supposed to happen either.
  • Since parsing the contract is delayed until one of the rewrite steps. The build definitions had to be altered slightly. Most notably it includes making parsers a dependency of rewrite.

@Drevanoorschot Drevanoorschot changed the title Add partial contract support for LLVM [VCLLVM] Add partial contract support for LLVM Jun 2, 2023
@Drevanoorschot
Copy link
Contributor Author

Latest commit on the branch solves both these issues:

  • When using the \result keyword, the AmbigiousResult.ref reference is never set. I'm not sure why this is or where the reference assignment is supposed to happen either.

We now make sure the parsed contracts are also passed through the resolver by making the the contract parsing part of the resolver.

  • Since parsing the contract is delayed until one of the rewrite steps. The build definitions had to be altered slightly. Most notably it includes making parsers a dependency of rewrite.

Since the resolver is part of the col module, the rewrite module does not depend on the parser module anymore. This change has also been reflected in the build definition

@Drevanoorschot
Copy link
Contributor Author

It would be nice if you could take this out now that we decided we should do parsing from resolution: it is also consistent with the notion that there should be no logic or unexpected stuff in the antlr -> col transformatiosn.

Latest commit should resolve above issue. I'm planning to implement invocations in contracts soon too. Since it's kind of related I could add to this PR or open a separate PR for it.

@pieter-bos
Copy link
Member

@Drevanoorschot What's the state of this now, should this be merged?

@Drevanoorschot
Copy link
Contributor Author

Yes, this branch can be merged. Apologies for not having been clear about the status of this PR

# Conflicts:
#	build.sc
#	src/col/vct/col/resolve/Resolve.scala
#	src/main/vct/main/stages/Resolution.scala
@pieter-bos pieter-bos merged commit 9e700f0 into dev Jun 28, 2023
14 checks passed
@pieter-bos pieter-bos deleted the vcllvm_contractparser branch June 28, 2023 14:45
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