Merge pull request #389 from viperproject/ast-loops

Add support for loops formed via gotos

Author: gauravpartha

src/main/scala/viper/carbon/CarbonVerifier.scala

@@ -61,6 +61,7 @@ case class CarbonVerifier(override val reporter: Reporter,
   val setModule = new DefaultSetModule(this)
   val mapModule = new DefaultMapModule(this)
   val wandModule = new DefaultWandModule(this)
+  val loopModule = new DefaultLoopModule(this)
 
   // initialize all modules
   allModules foreach (m => {

src/main/scala/viper/carbon/modules/HeapModule.scala

@@ -17,6 +17,11 @@ import viper.silver.ast.{LocationAccess, MagicWand}
  */
 trait HeapModule extends Module with CarbonStateComponent {
 
+  /**
+    * The type used for heaps
+    */
+  def heapType: Type
+
   /**
    * The type used for references.
    */
@@ -172,4 +177,8 @@ trait HeapModule extends Module with CarbonStateComponent {
 
   // adds permission to field e to the secondary mask of the wand
   def addPermissionToWMask(wMask: Exp, e: sil.Exp): Stmt
+
+  // If expression evaluates to true then resultHeap is the sum of of heap1, where mask1 is defined,
+  // and heap2, where mask2 is defined.
+  def sumHeap(resultHeap: Exp, heap1: Exp, mask1: Exp, heap2: Exp, mask2: Exp): Exp
 }

src/main/scala/viper/carbon/modules/LoopModule.scala

@@ -0,0 +1,18 @@
+package viper.carbon.modules
+
+import viper.silver.{ast => sil}
+
+trait LoopModule extends Module {
+
+  /* Returns method annotated with loop information and initializes loop module accordingly.
+   * This must be called before starting the method translation and the returned method should be used for the
+   * translation.
+   */
+  def initializeMethod(m: sil.Method): sil.Method
+
+  // Return true iff the statement is solely used for the loop module itself and is irrelevant otherwise.
+  def isLoopDummyStmt(s: sil.Stmt) : Boolean
+
+  // Return true iff the axioms to sum states is required.
+  def sumOfStatesAxiomRequired : Boolean
+}

src/main/scala/viper/carbon/modules/PermModule.scala

@@ -83,6 +83,11 @@ trait PermModule extends Module with CarbonStateComponent {
     */
   def wandMaskField(wand: Exp): Exp
 
+  /**
+    * The type used for masks.
+    */
+  def maskType: Type
+
   /**
    * The type used to for predicate masks.
    */
@@ -114,8 +119,24 @@ trait PermModule extends Module with CarbonStateComponent {
   def sumMask(assmsToSmt: Exp => Stmt):Stmt
   */
 
+  /**
+    *
+    * @param summandMask1
+    * @param summandMask2
+    * @return expression for which its validity implies that the current mask is the sum of the two input masks
+    */
   def sumMask(summandMask1: Seq[Exp], summandMask2: Seq[Exp]): Exp
 
+  /**
+    *
+    * @param resultMask
+    * @param summandMask1
+    * @param summandMask2
+    * @return expression for which its validity implies that @{code resultMask} is the sum of the other two input
+    *         masks
+    */
+  def sumMask(resultMask: Seq[Exp], summandMask1: Seq[Exp], summandMask2: Seq[Exp]) : Exp
+
     /** returns a mask and the returned statement ensures that the mask  has non-zero permission at rcv.loc and zero
       * permission at all other location
       * this should only be used temporarily, i.e. if there are two calls to this then the previous tempMask returned

src/main/scala/viper/carbon/modules/StmtModule.scala

@@ -8,7 +8,7 @@ package viper.carbon.modules
 
 import viper.carbon.modules.components.{ComponentRegistry, StmtComponent}
 import viper.silver.{ast => sil}
-import viper.carbon.boogie.{Exp, Stmt, TrueLit}
+import viper.carbon.boogie.{Exp, Namespace, Stmt, TrueLit}
 
 /**
  * A module for translating Viper statements.
@@ -33,5 +33,5 @@ trait StmtModule extends Module with ComponentRegistry[StmtComponent] {
 
   def translateStmt(stmt: sil.Stmt, statesStackForPackageStmt: List[Any] = null, allStateAssms: Exp = TrueLit(), insidePackageStmt: Boolean = false): Stmt
 
-
+  def labelNamespace: Namespace
 }