Applied Chris Hawblitzel's changes to deal with {:expand}

Erased {:yields} in the resulting sequential program in OwickiGriesTransform

1 files changed, 127 insertions, 0 deletions

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 4806318a..16a5e720 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1467,6 +1467,133 @@ namespace VC {
       ModelViewInfo mvInfo;

       var gotoCmdOrigins = PassifyImpl(impl, out mvInfo);

 

+      // If "expand" attribute is supplied, expand any assertion of conjunctions into multiple assertions, one per conjunct

+      foreach (var b in impl.Blocks)

+      {

+        List<Cmd> newCmds = new List<Cmd>();

+        bool changed = false;

+        foreach (var c in b.Cmds)

+        {

+          var a = c as AssertCmd;

+          var ar = c as AssertRequiresCmd;

+          var ae = c as AssertEnsuresCmd;

+          var ai = c as LoopInitAssertCmd;

+          var am = c as LoopInvMaintainedAssertCmd;

+          // TODO:

+          //use Duplicator and Substituter rather than new

+          //nested IToken?

+          //document expand attribute (search for {:ignore}, for example)

+          //fix up new CallCmd, new Requires, new Ensures in OwickiGries.cs

+          Func<Expr,Expr,Expr> withType = (Expr from, Expr to) =>

+          {

+            NAryExpr nFrom = from as NAryExpr;

+            NAryExpr nTo = to as NAryExpr;

+            to.Type = from.Type;

+            if (nFrom != null && nTo != null) nTo.TypeParameters = nFrom.TypeParameters;

+            return to;

+          };

+

+          Action<int,Expr,Action<Expr>> traverse = null;

+          traverse = (depth, e, act) =>

+          {

+            ForallExpr forall = e as ForallExpr;

+            NAryExpr nary = e as NAryExpr;

+            if (forall != null)

+            {

+              traverse(depth, forall.Body, e1 => act(withType(forall,

+                new ForallExpr(e1.tok, forall.TypeParameters, forall.Dummies, forall.Attributes, forall.Triggers, e1))));

+              return;

+            }

+            if (nary != null)

+            {

+              var args = nary.Args;

+              IAppliable fun = nary.Fun;

+              BinaryOperator bop = fun as BinaryOperator;

+              FunctionCall call = fun as FunctionCall;

+              if (bop != null)

+              {

+                switch (bop.Op)

+                {

+                  case BinaryOperator.Opcode.And:

+                    traverse(depth, args[0], act);

+                    traverse(depth, args[1], act);

+                    return;

+                  case BinaryOperator.Opcode.Imp:

+                    traverse(depth, args[1], e1 => act(withType(nary,

+                      new NAryExpr(e1.tok, fun, new List<Expr>() { args[0], e1 }))));

+                    return;

+                }

+              }

+              if (depth > 0 && call != null && call.Func != null)

+              {

+                Function cf = call.Func;

+                Expr body = cf.Body;

+                List<Variable> ins = cf.InParams;

+                if (body == null && cf.DefinitionAxiom != null)

+                {

+                  ForallExpr all = cf.DefinitionAxiom.Expr as ForallExpr;

+                  if (all != null)

+                  {

+                    NAryExpr def = all.Body as NAryExpr;

+                    if (def != null && def.Fun is BinaryOperator && ((BinaryOperator) (def.Fun)).Op == BinaryOperator.Opcode.Iff)

+                    {

+                      body = def.Args[1];

+                      ins = all.Dummies;

+                    }

+                  }

+                }

+                if (body != null)

+                {

+                  Func<Expr,Expr> new_f = e1 =>

+                  {

+                    Function f = new Function(cf.tok, "expand<" + cf.Name + ">", cf.TypeParameters, ins, cf.OutParams[0], cf.Comment);

+                    f.Body = e1;

+                    Token tok = new Token(e1.tok.line, e1.tok.col);

+                    tok.filename = e.tok.filename + "(" + e.tok.line + "," + e.tok.col + ") --> " + e1.tok.filename;

+                    return withType(nary, new NAryExpr(tok, new FunctionCall(f), args));

+                  };

+                  traverse(depth - 1, body, e1 => act(new_f(e1)));

+                  return;

+                }

+              }

+            }

+            act(e);

+          };

+

+          if (a != null)

+          {

+            var attr = a.Attributes;

+            if (ar != null && ar.Requires.Attributes != null) attr = ar.Requires.Attributes;

+            if (ar != null && ar.Call.Attributes != null) attr = ar.Call.Attributes;

+            if (ae != null && ae.Ensures.Attributes != null) attr = ae.Ensures.Attributes;

+            if (QKeyValue.FindExprAttribute(attr, "expand") != null || QKeyValue.FindBoolAttribute(attr, "expand"))

+            {

+              int depth = QKeyValue.FindIntAttribute(attr, "expand", 100);

+              Func<Expr,Expr> fe = e => Expr.Or(a.Expr, e);

+              //traverse(depth, a.Expr, e => System.Console.WriteLine(e.GetType() + " :: " + e + " @ " + e.tok.line + ", " + e.tok.col));

+              traverse(depth, a.Expr, e =>

+                {

+                  AssertCmd new_c = 

+                    (ar != null) ? new AssertRequiresCmd(ar.Call, new Requires(e.tok, ar.Requires.Free, fe(e), ar.Requires.Comment)) :

+                    (ae != null) ? new AssertEnsuresCmd(new Ensures(e.tok, ae.Ensures.Free, fe(e), ae.Ensures.Comment)) :

+                    (ai != null) ? new LoopInitAssertCmd(e.tok, fe(e)) :

+                    (am != null) ? new LoopInvMaintainedAssertCmd(e.tok, fe(e)) :

+                    new AssertCmd(e.tok, fe(e));

+                  new_c.Attributes = new QKeyValue(e.tok, "subsumption", new List<object>() { new LiteralExpr(e.tok, BigNum.FromInt(0)) }, a.Attributes);

+                  newCmds.Add(new_c);

+                });

+            }

+            newCmds.Add(c);

+            changed = true;

+          }

+          else

+          {

+            newCmds.Add(c);

+          }

+        }

+        if (changed) b.Cmds = newCmds;

+      }

+

       double max_vc_cost = CommandLineOptions.Clo.VcsMaxCost;

       int tmp_max_vc_cost = -1, max_splits = CommandLineOptions.Clo.VcsMaxSplits, 

           max_kg_splits = CommandLineOptions.Clo.VcsMaxKeepGoingSplits;