Chalice: partial fixes to the broken refinement extension regression tests.

1 files changed, 27 insertions, 12 deletions

diff --git a/Chalice/src/main/scala/Resolver.scala b/Chalice/src/main/scala/Resolver.scala
index 9a5d50e8..dee231c8 100644
--- a/Chalice/src/main/scala/Resolver.scala
+++ b/Chalice/src/main/scala/Resolver.scala
@@ -1322,15 +1322,17 @@ object Resolver {
      CheckRunSpecification(e, context, allowMaxLock)

  }

 

- def ResolveTransform(mt: MethodTransform, context: ProgramContext) {

+ def ResolveTransform(mt: MethodTransform, baseContext: ProgramContext) {

+   val context = baseContext.SetClass(mt.Parent).SetMember(mt);

+

    mt.spec foreach {

      case Precondition(e) =>

        context.Error(e.pos, "Method refinement cannot add a pre-condition")

      case Postcondition(e) =>

-       ResolveExpr(e, context.SetClass(mt.Parent).SetMember(mt), true, true)(false)

+       ResolveExpr(e, context, true, true)(false)

      case _ : LockChange => throw new NotSupportedException("not implemented")

    }

-   if (mt.ins != mt.refines.Ins) context.Error(mt.pos, "Refinement must have same input arguments")

+   if (mt.ins != mt.refines.Ins) context.Error(mt.pos, "Refinement must have the same input arguments")

    if (! mt.outs.startsWith(mt.refines.Outs)) context.Error(mt.pos, "Refinement must declare all abstract output variables")

 

    mt.body = AST.refine(mt.refines.Body, mt.trans) match {

@@ -1338,18 +1340,29 @@ object Resolver {
      case AST.Unmatched(t) => context.Error(mt.pos, "Cannot match transform around " + t.pos); Nil

    }

                                 

-   def resolveBody(ss: List[Statement], con: ProgramContext, abs: List[Variable]) {

-     var ctx = con;

-     var locals = abs;

-     for (s <- ss) {

+   /**

+    * We thread two contexts for the concrete and abstract versions.

+    */

+   def resolveBody(ss: List[Statement], 

+     concreteContext: ProgramContext,

+     abstractContext: List[Variable]) {

+     var ctx = concreteContext;

+     var locals = abstractContext;

+     for (s <- ss) { 

        s match {

          case r @ RefinementBlock(c, a) =>

            // abstract globals available at this point in the program

-           r.before = locals

+           r.before = locals;

+

+           // resolve concrete version

            ResolveStmt(BlockStmt(c), ctx)

+

+           // compare declared local variables

            val vs = c flatMap {s => s.Declares};

-           for (v <- a flatMap {s => s.Declares}; if (! vs.contains(v)))

-             ctx.Error(r.pos, "Refinement block must declare a local variable from abstract program: " + v.id)

+           for (s <- a;

+                v <- s.Declares; 

+                if (! vs.contains(v)))

+             ctx.Error(r.pos, "Refinement block must declare a local variable from the abstract program: " + v.id)

          case w @ WhileStmt(guard, oi, ni, lks, body) =>

            for (inv <- ni) {

              ResolveExpr(inv, ctx, true, true)(false)

@@ -1364,8 +1377,9 @@ object Resolver {
            resolveBody(List(els), ctx, locals)

          case BlockStmt(ss) =>

            resolveBody(ss, ctx, locals)

-         case _ =>

+         case _ =>   

        }

+

        // declare concrete and abstract locals

        for (v <- s.Declares) ctx = ctx.AddVariable(v);

        s match {

@@ -1374,7 +1388,8 @@ object Resolver {
        }

      }

    }

-   resolveBody(mt.body, context.SetClass(mt.Parent).SetMember(mt), Nil)

+

+   resolveBody(mt.body, context, mt.refines.Ins ++ mt.refines.Outs)

  }

 

  def ResolveCouplingInvariant(ci: CouplingInvariant, cl: Class, context: ProgramContext) {