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

Extend stack pointer support in TriCera #24

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

Conversation

zafer-esen
Copy link
Collaborator

This PR aims to address #12.

The idea is to introduce an AST preprocessor package (perhaps to be named astpreprocessor), where we can run various translators on input programs that update / collect information on the AST prior to sending the final AST to CCReader. These AST preprocessors should also include a back-translator for translating back solutions and counterexamples.

Initially, we can consider a solution at AST-level to be all the contracts of the functions. The task would then be to translate contracts over the preprocessed AST to contracts over the AST prior to preprocessing. For instance if the preprocessor created copies of functions f_1, f_2, ..., f_n for some function f and the solution is for the copy functions, then the back-translator should merge those contracts into a single contract for f.

Task list

  1. Compile visitors in ccparser, currently only the ones in Absyn are compiled. (already done prior to creating this PR )
  2. Do type-inference in first pass (could be separate visitors or the same)
  3. Detect pointer types, rewrite call sites.
  4. Create copies of functions for stack & heap pointers.
  5. Add back-translators.
  6. Stretch goal: output contracts in ACSL AST, and implement preprocessors & back-translators using this.

A more detailed task list is inserted into CCReader as comments in the first commit of this PR.

@zafer-esen
Copy link
Collaborator Author

@woosh, I added you to the PR, hope that is okay!

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