From 0ce0ad111d6454475f47b56a6315b6134b869400 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Fri, 23 Aug 2013 15:21:58 -0700
Subject: Applied Chris Hawblitzel's changes to deal with {:expand} Erased
 {:yields} in the resulting sequential program in OwickiGriesTransform

---
 Source/VCGeneration/VC.cs | 127 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 127 insertions(+)

(limited to 'Source/VCGeneration/VC.cs')

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;
-- 
cgit v1.2.3