Skip to content

Commit

Permalink
Adds outline for the work to be done
Browse files Browse the repository at this point in the history
  • Loading branch information
zafer-esen committed Sep 17, 2024
1 parent 77ede6a commit 97d4005
Showing 1 changed file with 26 additions and 0 deletions.
26 changes: 26 additions & 0 deletions src/tricera/concurrency/CCReader.scala
Original file line number Diff line number Diff line change
Expand Up @@ -163,6 +163,32 @@ object CCReader {
}

////////////////////////////////////////////////////////////////////////////////
trait ProgramBackTranslator
object DummyBackTranslator extends ProgramBackTranslator

trait CCASTPreprocessor {
def translate(prog : Program) : (Program, ProgramBackTranslator)
}

// 0) Compile visitors in ccparser, currently only the ones in Absyn are compiled.
// Look up Princess SMT-LIB parser, which had the same problem which is now fixed.
// -- Do the same for the ACSL parser as well.
// 1) Do type-inference in first pass (could be separate visitors or the same)
// Extend EVar class and create a new AST after the pass.
// We could also extend the grammar, e.g.,
// EvarWithType. Exp17 ::= "$$" CIdent ":" [Declaration_specifier] "##";
// This has the advantage of making all generated visitors know about this.
// Challenge:
// -- ComposVisitor will revert back to the old AST -- won't know about
// the augmented classes.
// -- Solution: Extend ComposVisitor so that it knows about the new types.
// 2) Detect pointer types, rewrite call sites.
// -- At each call, i) if it is a stack pointer rewrite using a new function
// name and global variables.
// 3) Create copies of functions for stack & heap pointers.
// 4) Add back-translators.
// 5) Stretch goal: output contracts in ACSL AST, and implement preprocessors &
// back-translators using this.

class CCReader private (prog : Program,
entryFunction : String,
Expand Down

0 comments on commit 97d4005

Please sign in to comment.