Merge changes to support Corral in fixedpoint backend

8 files changed, 597 insertions, 71 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 0bb5e6de..f2299cc9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -463,6 +463,7 @@ namespace Microsoft.Boogie {
     public string PrintCFGPrefix = null;

     public bool ForceBplErrors = false; // if true, boogie error is shown even if "msg" attribute is present

     public bool UseArrayTheory = false;

+    public bool WeakArrayTheory = false;

     public bool UseLabels = true;

     public bool MonomorphicArrays {

       get {

@@ -1300,6 +1301,7 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("z3multipleErrors", ref z3AtFlag, false) ||

               ps.CheckBooleanFlag("monomorphize", ref Monomorphize) ||

               ps.CheckBooleanFlag("useArrayTheory", ref UseArrayTheory) ||

+              ps.CheckBooleanFlag("weakArrayTheory", ref WeakArrayTheory) || 

               ps.CheckBooleanFlag("doModSetAnalysis", ref DoModSetAnalysis) ||

               ps.CheckBooleanFlag("doNotUseLabels", ref UseLabels, false) ||

               ps.CheckBooleanFlag("contractInfer", ref ContractInfer) ||

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 3004fafa..be98eb5b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -395,7 +395,8 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();

     }

 

-    private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler)

+    private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, 

+                                 Dictionary<int,Dictionary<string,string>> varSubst)

     {

         Dictionary<string, RPFP.Node> nmap = new Dictionary<string,RPFP.Node>();

         Dictionary<string, RPFP.Node> pmap = new Dictionary<string,RPFP.Node>();

@@ -410,16 +411,17 @@ namespace Microsoft.Boogie.SMTLib
         for (int i = 0; i < lines.Length-1; i++)

         {

             var line = lines[i];

-            if (line.ArgCount != 5)

+            if (line.ArgCount != 6)

             {

                 HandleProverError("bad derivation line from prover: " + line.ToString());

                 return null;

             }

             var name = line[0];

             var conseq = line[1];

-            var subst = line[2];

-            var labs = line[3];

-            var refs = line[4];

+            var rule = line[2];

+            var subst = line[3];

+            var labs = line[4];

+            var refs = line[5];

             var predName = conseq.Name;

             RPFP.Node node = null;

             if (!pmap.TryGetValue(predName, out node))

@@ -452,18 +454,54 @@ namespace Microsoft.Boogie.SMTLib
                     Chs.Add(ch);

                 }

             }

-            RPFP.Edge e = rpfp.CreateEdge(cexnode, node.Outgoing.F, Chs.ToArray());

+

+            if (!rule.Name.StartsWith("rule!"))

+            {

+                HandleProverError("bad rule name from prover: " + refs.ToString());

+                return null;

+            }

+            int ruleNum = Convert.ToInt32(rule.Name.Substring(5)) - 1;

+            if(ruleNum < 0 || ruleNum > rpfp.edges.Count)

+            {

+                HandleProverError("bad rule name from prover: " + refs.ToString());

+                return null;

+            }

+            RPFP.Edge orig_edge = rpfp.edges[ruleNum];

+            RPFP.Edge e = rpfp.CreateEdge(cexnode, orig_edge.F, Chs.ToArray());

+            e.map = orig_edge;

             topnode = cexnode;

 

             if (labs.Name != "labels")

             {

-                HandleProverError("bad labels from prover: " + refs.ToString());

+                HandleProverError("bad labels from prover: " + labs.ToString());

                 return null;

             }

             e.labels = new HashSet<string>();

             foreach (var l in labs.Arguments)

                 e.labels.Add(l.Name);

 

+            if (subst.Name != "subst")

+            {

+                HandleProverError("bad subst from prover: " + subst.ToString());

+                return null;

+            }

+            Dictionary<string, string> dict = new Dictionary<string, string>();

+            varSubst[e.number] = dict;

+            foreach (var s in subst.Arguments)

+            {

+                if(s.Name != "=" || s.Arguments.Length != 2)

+                {

+                    HandleProverError("bad equation from prover: " + s.ToString());

+                    return null;

+                }

+                string uniqueName = s.Arguments[0].Name;

+                string spacer = "@@"; // Hack! UniqueNamer is adding these and I can't stop it!

+                int pos = uniqueName.LastIndexOf(spacer);

+                if (pos >= 0)

+                    uniqueName = uniqueName.Substring(0, pos);

+                dict.Add(uniqueName, s.Arguments[1].ToString());

+            }

+

         }

         if (topnode == null)

         {

@@ -472,7 +510,41 @@ namespace Microsoft.Boogie.SMTLib
         return topnode;

     }

 

-    public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, out RPFP.Node cex)

+    private string QuantifiedVCExpr2String(VCExpr x)

+    {

+        return VCExpr2String(x, 1); 

+#if false

+        if (!(x is VCExprQuantifier))

+            return VCExpr2String(x, 1);

+        VCExprQuantifier node = (x as VCExprQuantifier);

+        if(node.BoundVars.Count == 0)

+            return VCExpr2String(x, 1);

+

+        StringWriter wr = new StringWriter();

+

+        string kind = node.Quan == Quantifier.ALL ? "forall" : "exists"; 

+        wr.Write("({0} (", kind);

+

+        for (int i = 0; i < node.BoundVars.Count; i++)

+        {

+            VCExprVar var = node.BoundVars[i];

+            Contract.Assert(var != null);

+            string printedName = Namer.GetQuotedName(var, var.Name);

+            Contract.Assert(printedName != null);

+            wr.Write("({0} {1}) ", printedName, SMTLibExprLineariser.TypeToString(var.Type));

+        }

+

+        wr.Write(") ");

+        wr.Write(VCExpr2String(node.Body, 1));

+        wr.Write(")");

+        string res = wr.ToString();

+        return res;

+#endif

+    }

+

+    public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, 

+                                      out RPFP.Node cex,

+                                      Dictionary<int,Dictionary<string,string>> varSubst)

     {

         //Contract.Requires(descriptiveName != null);

         //Contract.Requires(vc != null);

@@ -488,6 +560,7 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

         {

             DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);

@@ -499,10 +572,10 @@ namespace Microsoft.Boogie.SMTLib
         List<string> ruleStrings = new List<string>();

         foreach (var edge in rpfp.edges)

         {

-            string ruleString = "(rule " + VCExpr2String(rpfp.GetRule(edge), 1) + "\n)";

+            string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";

             ruleStrings.Add(ruleString);

         }

-        string queryString = "(query " + VCExpr2String(rpfp.GetQuery(), 1) + "\n   :engine duality\n  :print-certificate true\n)";

+        string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n   :engine duality\n  :print-certificate true\n)";

         LineariserOptions.Default.LabelsBelowQuantifiers = false;

         FlushAxioms();

 

@@ -557,7 +630,7 @@ namespace Microsoft.Boogie.SMTLib
                         resp = Process.GetProverResponse();

                         if (resp.Name == "derivation")

                         {

-                            cex = SExprToCex(resp, handler);

+                            cex = SExprToCex(resp, handler,varSubst);

                         }

                         else

                             HandleProverError("Unexpected prover response: " + resp.ToString());

@@ -577,6 +650,7 @@ namespace Microsoft.Boogie.SMTLib
             }

 #endif

         }

+        SendThisVC("(fixedpoint-pop)");

         return result;

     }

 

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 8081603e..81d5d5d1 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -259,6 +259,12 @@ namespace Microsoft.Boogie.SMTLib
                 if (options.Inspector != null)

                     options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

 

+                if (CommandLineOptions.Clo.WeakArrayTheory)

+                {

+                    // TODO: these options don't seem to exist in recent Z3

+                    // options.AddWeakSmtOption("ARRAY_WEAK", "true");

+                    // options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");

+                } 

             }

             else

             {

@@ -320,8 +326,13 @@ namespace Microsoft.Boogie.SMTLib
 

                 if (options.Inspector != null)

                     options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

-

-

+                

+                if (CommandLineOptions.Clo.WeakArrayTheory)

+                {

+                    options.AddWeakSmtOption("ARRAY_WEAK", "true");

+                    options.AddWeakSmtOption("ARRAY_EXTENSIONAL", "false");

+                }

+                

             }

 

             // legacy option handling

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 607476e7..e88c000e 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -406,7 +406,9 @@ namespace Microsoft.Boogie {
     }

     public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);

     

-    public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler, out RPFP.Node cex)

+    public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler,

+                                     out RPFP.Node cex,

+                                     Dictionary<int, Dictionary<string, string>> varSubst)

     {

         throw new System.NotImplementedException();

     }

diff --git a/Source/VCGeneration/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs
index 67837833..d63f4fc2 100644
--- a/Source/VCGeneration/ExprExtensions.cs
+++ b/Source/VCGeneration/ExprExtensions.cs
@@ -139,10 +139,29 @@ namespace Microsoft.Boogie.ExprExtensions
             return Function(f, args);

         }

 

+        public Term MkApp(FuncDecl f, Term[] args, Type[]/*!*/ typeArguments)

+        {

+            return Function(f, args, typeArguments);

+        }

+

         public Term MkApp(FuncDecl f, Term arg)

         {

             return Function(f, arg);

         }

+

+        public Term CloneApp(Term t, Term[] args)

+        {

+            var f = t.GetAppDecl();

+            var typeArgs = (t as VCExprNAry).TypeArguments;

+            if (typeArgs != null && typeArgs.Count > 0)

+            {

+                return MkApp(f, args, typeArgs.ToArray());

+            }

+            else

+            {

+                return MkApp(f, args);

+            }

+        }

         

         public Term MkAnd(Term[] args)

         {

@@ -186,6 +205,8 @@ namespace Microsoft.Boogie.ExprExtensions
 

         public Term MkForall(Term[] bounds, Term body)

         {

+            if (bounds.Length == 0)

+                return body;

             List<VCExprVar> vbs = new List<VCExprVar>();

             foreach(var v in bounds)

                 vbs.Add(v as VCExprVar);

@@ -194,10 +215,110 @@ namespace Microsoft.Boogie.ExprExtensions
 

         public Term MkExists(Term[] bounds, Term body)

         {

+            if (bounds.Length == 0)

+                return body; 

             List<VCExprVar> vbs = new List<VCExprVar>();

             foreach (var v in bounds)

                 vbs.Add(v as VCExprVar);

             return Exists(vbs, new List<VCTrigger>(), body);

         }

+

+        private class Letifier

+        {

+            private class counter

+            {

+                public int cnt = 0;

+            }

+            Dictionary<Term, counter> refcnt = new Dictionary<Term, counter>();

+            List<VCExprLetBinding> bindings = new List<VCExprLetBinding>();

+            Dictionary<Term, VCExprVar> bindingMap = new Dictionary<Term, VCExprVar>();

+            int letcnt = 0;

+            Context ctx;

+

+            public Letifier(Context _ctx) { ctx = _ctx; }

+

+            private void RefCnt(Term t)

+            {

+                counter cnt;

+                if (!refcnt.TryGetValue(t, out cnt))

+                {

+                    cnt = new counter();

+                    refcnt.Add(t, cnt);

+                }

+                cnt.cnt++;

+                if (cnt.cnt == 1)

+                {

+                    var kind = t.GetKind();

+                    if (kind == TermKind.App)

+                    {

+                        var args = t.GetAppArgs();

+                        foreach (var arg in args)

+                            RefCnt(arg);

+                    }

+                    else if (t is VCExprQuantifier)

+                    {

+                        RefCnt((t as VCExprQuantifier).Body);

+                    }

+                }

+            }

+

+            private Term Doit(Term t)

+            {

+                VCExprVar v;

+                if (bindingMap.TryGetValue(t, out v))

+                {

+                    return v;

+                }

+                Term res = null;

+                var kind = t.GetKind();

+                bool letok = false;

+                if (kind == TermKind.App)

+                {

+                    var f = t.GetAppDecl();

+                    var args = t.GetAppArgs();

+                    args = args.Select(x => Doit(x)).ToArray();

+                    res = ctx.MkApp(f, args);

+                    letok = true;

+                }

+                else if (t is VCExprQuantifier)

+                {

+                    var q = t as VCExprQuantifier;

+                    var newbody = ctx.Letify(q.Body);

+                    if (q.Quan == Quantifier.ALL)

+                        res = ctx.Forall(q.BoundVars, q.Triggers, newbody);

+                    else

+                        res = ctx.Exists(q.BoundVars, q.Triggers, newbody);

+                    letok = true;

+                }

+                else res = t;

+                if (letok && refcnt[t].cnt > 1)

+                {

+                    VCExprVar lv = ctx.MkConst("fpvc$" + Convert.ToString(letcnt), t.GetSort()) as VCExprVar;

+                    VCExprLetBinding b = ctx.LetBinding(lv, res);

+                    bindings.Add(b);

+                    bindingMap.Add(t, lv);

+                    res = lv;

+                    letcnt++;

+                }

+                return res;

+            }

+

+            public Term Letify(Term t)

+            {

+                RefCnt(t);

+                Term res = Doit(t);

+                if (bindings.Count > 0)

+                    res = ctx.Let(bindings, res);

+                return res;

+            }

+

+        }

+

+        public Term Letify(Term t)

+        {

+            var thing = new Letifier(this);

+            return thing.Letify(t);

+        }

+

     };

 }

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index adc801d5..bc6a7ce0 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -65,6 +65,7 @@ namespace Microsoft.Boogie
         Dictionary<string, Term> labels = new Dictionary<string, Term> ();

         List<Term> DualityVCs = new List<Term>();

         Dictionary<string, bool> summaries = new Dictionary<string, bool>();

+        Dictionary<Block, List<Block>> edgesCut = new Dictionary<Block, List<Block>>();

         string main_proc_name = "main";

         

         

@@ -185,9 +186,12 @@ namespace Microsoft.Boogie
 #endif

                 foreach (Variable v in /* impl.LocVars */ header.liveVarsBefore)

                 {

-                    vars.Add(v);

-                    names.Add(v.ToString()); 

-                    exprs.Add(new IdentifierExpr(Token.NoToken, v));

+                    if (!(v is BoundVariable))

+                    {

+                        vars.Add(v);

+                        names.Add(v.ToString());

+                        exprs.Add(new IdentifierExpr(Token.NoToken, v));

+                    }

                 }

             }

             else

@@ -611,7 +615,7 @@ namespace Microsoft.Boogie
                             exprs.Add(ie);

                         }

                         Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);

-#if false

+#if true

                         if(mode == Mode.Corral || mode == Mode.OldCorral)

                             proc.Ensures.Add(new Ensures(Token.NoToken, true, freePostExpr, "", new QKeyValue(Token.NoToken, "si_fcall", new List<object>(), null)));

 #endif

@@ -656,7 +660,7 @@ namespace Microsoft.Boogie
             }

         }

 

-        private Term ExtractSmallerVCsRec(Dictionary<Term, Term> memo, Term t, List<Term> small)

+        private Term ExtractSmallerVCsRec(Dictionary<Term, Term> memo, Term t, List<Term> small, Term lbl = null)

         {

             Term res;

             if (memo.TryGetValue(t, out res))

@@ -677,7 +681,7 @@ namespace Microsoft.Boogie
                             {

                                 q = ctx.MkImplies(lhsargs[i], q);

                             }

-                            res = ExtractSmallerVCsRec(memo, q, small);

+                            res = ExtractSmallerVCsRec(memo, q, small,lbl);

                             goto done;

                         }

                         if (r.GetKind() == DeclKind.Label)

@@ -689,6 +693,8 @@ namespace Microsoft.Boogie
                             if (!(annotationInfo.ContainsKey(arg.GetAppDecl().GetDeclName()) && annotationInfo[arg.GetAppDecl().GetDeclName()].type == AnnotationInfo.AnnotationType.LoopInvariant))

                                 goto normal;

                             var sm = ctx.MkImplies(lhs, ExtractSmallerVCsRec(memo, t.GetAppArgs()[1], small));

+                            if (lbl != null)

+                                sm = ctx.MkImplies(lbl, sm);

                             small.Add(sm);

                             res = ctx.MkTrue();

                             goto done;

@@ -699,13 +705,18 @@ namespace Microsoft.Boogie
                             if (!(annotationInfo.ContainsKey(arg.GetAppDecl().GetDeclName()) && annotationInfo[arg.GetAppDecl().GetDeclName()].type == AnnotationInfo.AnnotationType.LoopInvariant))

                                 goto normal;

                             var sm = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small));

+                            if (lbl != null)

+                                sm = ctx.MkImplies(lbl, sm); 

                             small.Add(sm);

                             res = ctx.MkTrue();

                             goto done;

                         }

                     }

                 normal:

-                    res = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small));

+                    Term newlbl = null;

+                    if (lhs.IsLabel() && lhs.GetAppArgs()[0] == ctx.MkTrue())

+                        newlbl = lhs;

+                    res = ctx.MkImplies(lhs,ExtractSmallerVCsRec(memo,t.GetAppArgs()[1],small,newlbl));

                 }

                 else if (f.GetKind() == DeclKind.And)

                 {

@@ -870,9 +881,9 @@ namespace Microsoft.Boogie
             var kind = t.GetKind();

             if (kind == TermKind.App)

             {

-                var f = t.GetAppDecl();

+                // var f = t.GetAppDecl();

                 var args = t.GetAppArgs().Select(x => SubstRec(memo, x)).ToArray();

-                res = ctx.MkApp(f, args);

+                res = ctx.CloneApp(t, args);

             }

             else res = t;

             memo.Add(t, res);

@@ -985,7 +996,7 @@ namespace Microsoft.Boogie
             if (mode == Mode.Boogie && style == AnnotationStyle.Flat && impl.Name != main_proc_name)

                 return;

             Contract.Assert(impl != null);

-            ConvertCFG2DAG(impl);

+            ConvertCFG2DAG(impl,edgesCut);

             VC.ModelViewInfo mvInfo;

             PassifyImpl(impl, out mvInfo);

             Hashtable/*<int, Absy!>*/ label2absy = null;

@@ -1050,6 +1061,7 @@ namespace Microsoft.Boogie
                 FuncDecl R = boogieContext.VCExprToTerm(info.funcExpr, linOptions).GetAppDecl();

                 relationToProc.Add(R, info);

                 info.node = rpfp.CreateNode(boogieContext.VCExprToTerm(info.funcExpr, linOptions));

+                rpfp.nodes.Add(info.node);

                 if (info.isMain || QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint"))

                     info.node.Bound.Formula = ctx.MkFalse();

             }

@@ -1075,16 +1087,18 @@ namespace Microsoft.Boogie
             if (kind == TermKind.App)

             {

                 var f = t.GetAppDecl();

+                var args = t.GetAppArgs();

+                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

                 StratifiedInliningInfo info;

                 if (relationToProc.TryGetValue(f, out info))

                 {

                     f = SuffixFuncDecl(t, parms.Count);

                     parms.Add(f);

                     nodes.Add(info.node);

+                    res = ctx.MkApp(f, args);

                 }

-                var args = t.GetAppArgs();

-                args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

-                res = ctx.MkApp(f, args);

+                else

+                    res = ctx.CloneApp(t, args);

             } // TODO: handle quantifiers

             else res = t;

             memo.Add(t, res);

@@ -1104,6 +1118,7 @@ namespace Microsoft.Boogie
             // vcTerm = foo.Item1;

             info.F = rpfp.CreateTransformer(relParams.ToArray(), paramTerms, vcTerm);

             info.edge = rpfp.CreateEdge(info.node, info.F, nodeParams.ToArray());

+            rpfp.edges.Add(info.edge);

             // TODO labels[info.edge.number] = foo.Item2;

         }

 

@@ -1178,6 +1193,8 @@ namespace Microsoft.Boogie
         public void Generate()

         {

 

+            var oldDagOption = CommandLineOptions.Clo.vcVariety;

+            CommandLineOptions.Clo.vcVariety = CommandLineOptions.VCVariety.Dag;

 

             // Run live variable analysis (TODO: should this be here?)

 #if false

@@ -1190,8 +1207,9 @@ namespace Microsoft.Boogie
             #region In Boogie mode, annotate the program

             if (mode == Mode.Boogie)

             {

+

                 // find the name of the main procedure

-                main_proc_name = "main"; // default in case no entry point defined

+                main_proc_name = null; // default in case no entry point defined

                 foreach (var d in program.TopLevelDeclarations)

                 {

                     var impl = d as Implementation;

@@ -1201,6 +1219,21 @@ namespace Microsoft.Boogie
                             main_proc_name = impl.Proc.Name;

                     }

                 }

+                if (main_proc_name == null)

+                {

+                    foreach (var d in program.TopLevelDeclarations)

+                    {

+                        var impl = d as Implementation;

+                        if (impl != null)

+                        {

+                            if (impl.Proc.Name == "main" || impl.Proc.Name.EndsWith(".main"))

+                                main_proc_name = impl.Proc.Name;

+                        }

+                    }

+                }

+                if (main_proc_name == null)

+                    main_proc_name = "main";

+

                 if (style == AnnotationStyle.Flat)

                 {

                     InlineAll();

@@ -1319,13 +1352,18 @@ namespace Microsoft.Boogie
 

             // save some information for debugging purposes

             // TODO rpfp.ls.SetAnnotationInfo(annotationInfo);

+

+            CommandLineOptions.Clo.vcVariety = oldDagOption;

         }

 

+        

         private class ErrorHandler : ProverInterface.ErrorHandler

         {

             //TODO: anything we need to handle?

         }

 

+        Dictionary<int, Dictionary<string, string>> varSubst = null;

+

         /** Check the RPFP, and return a counterexample if there is one. */

 

         public RPFP.LBool Check(ref RPFP.Node cexroot)

@@ -1334,7 +1372,9 @@ namespace Microsoft.Boogie
 

             ErrorHandler handler = new ErrorHandler();

             RPFP.Node cex;

-            ProverInterface.Outcome outcome = checker.TheoremProver.CheckRPFP("name", rpfp, handler, out cex);

+            varSubst = new Dictionary<int,Dictionary<string,string>>();

+            ProverInterface.Outcome outcome =

+                 checker.TheoremProver.CheckRPFP("name", rpfp, handler, out cex, varSubst);

             cexroot = cex;

           

             Console.WriteLine("solve: {0}s", (DateTime.Now - start).TotalSeconds);

@@ -1350,8 +1390,19 @@ namespace Microsoft.Boogie
             }

         }

 

+        private bool generated = false;

+

         public override VC.VCGen.Outcome VerifyImplementation(Implementation impl, VerifierCallback collector)

         {

+            var start = DateTime.Now; 

+            

+            if (!generated)

+            {

+                Generate();

+                Console.WriteLine("generate: {0}s", (DateTime.Now - start).TotalSeconds);

+                generated = true;

+            }

+            

             Procedure proc = impl.Proc;

             

             // we verify all the impls at once, so we need to execute only once

@@ -1360,16 +1411,12 @@ namespace Microsoft.Boogie
             if (mode == Mode.OldCorral)

                 needToCheck = proc.FindExprAttribute("inline") == null && !(proc is LoopProcedure);

             else if (mode == Mode.Corral)

-                needToCheck = proc.FindExprAttribute("entrypoint") != null && !(proc is LoopProcedure);

+                needToCheck = QKeyValue.FindBoolAttribute(impl.Attributes, "entrypoint") && !(proc is LoopProcedure);

             else

                 needToCheck = impl.Name == main_proc_name;

 

             if (needToCheck)

             {

-                var start = DateTime.Now;

-                Generate(); 

-                Console.WriteLine("generate: {0}s", (DateTime.Now - start).TotalSeconds);

-

                 Console.WriteLine("Verifying {0}...", impl.Name);

 

                 RPFP.Node cexroot = null;

@@ -1383,7 +1430,7 @@ namespace Microsoft.Boogie
                         // start = DateTime.Now;

                         Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl);

                         // cexroot.owner.DisposeDualModel();

-                        // cex.Print(0);  // TODO: just for testing

+                        cex.Print(0);  // TODO: just for testing

                         collector.OnCounterexample(cex, "assertion failure");

                         Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds);

                         return VC.ConditionGeneration.Outcome.Errors;

@@ -1477,17 +1524,40 @@ namespace Microsoft.Boogie
             return CodeLabelTrue(rpfp, root, code, info, prefix);

         }

 

+

+        private class StateId

+        {

+            public RPFP.Edge edge;

+            public int capturePoint;

+            public StratifiedInliningInfo info;

+            public StateId(RPFP.Edge e, int c, StratifiedInliningInfo i)

+            {

+                edge = e;

+                capturePoint = c;

+                info = i;

+            }

+        }

+

         public Counterexample CreateBoogieCounterExample(RPFP rpfp, RPFP.Node root, Implementation mainImpl)

         {

             FindLabels();

-            var orderedStateIds = new List<Tuple<int, int>>();

+            var orderedStateIds = new List<StateId>();

             Counterexample newCounterexample =

               GenerateTrace(rpfp, root, orderedStateIds, mainImpl,true);

+            if (CommandLineOptions.Clo.ModelViewFile != null)

+            {

+                Model m = new Model();

+                GetModelWithStates(m, root, implName2StratifiedInliningInfo[mainImpl.Name],

+                                   orderedStateIds, varSubst);

+                newCounterexample.Model = m;

+            }

             return newCounterexample;

         }

 

+        

+

         private Counterexample GenerateTrace(RPFP rpfp, RPFP.Node root,

-                                                 List<Tuple<int, int>> orderedStateIds, Implementation procImpl, bool toplevel)

+                                                 List<StateId> orderedStateIds, Implementation procImpl, bool toplevel)

         {

             Contract.Requires(procImpl != null);

 

@@ -1497,12 +1567,12 @@ namespace Microsoft.Boogie
             var info = implName2StratifiedInliningInfo[procImpl.Name]; 

             Block entryBlock = cce.NonNull(procImpl.Blocks[0]);

             Contract.Assert(entryBlock != null);

-            if (!CodeLabelFalse(rpfp, root, entryBlock, info, "+"))

-                Contract.Assert(false);

+           

             BlockSeq trace = new BlockSeq(); 

             trace.Add(entryBlock);

 

             var calleeCounterexamples = new Dictionary<TraceLocation, CalleeCounterexampleInfo>();

+

             Counterexample newCounterexample =

                 GenerateTraceRec(rpfp, root, orderedStateIds, entryBlock, trace, calleeCounterexamples, info, toplevel);

 

@@ -1533,7 +1603,7 @@ namespace Microsoft.Boogie
         

         private Counterexample GenerateTraceRec(

                               RPFP rpfp, RPFP.Node root,

-                              List<Tuple<int, int>> orderedStateIds,

+                              List<StateId> orderedStateIds,

                               Block/*!*/ b, BlockSeq/*!*/ trace,

                               Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ calleeCounterexamples,

                               StratifiedInliningInfo info,

@@ -1542,9 +1612,32 @@ namespace Microsoft.Boogie
             Contract.Requires(b != null);

             Contract.Requires(trace != null);

             Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples));

+

+            Stack<RPFP.Node> continuation_stack = new Stack<RPFP.Node>();

+

+            // If our block is not present, try diving into precondition

+            // and push a continuation.

+            // TODO: is the precondition always the first child?

+            while (!CodeLabelFalse(rpfp, root, b, info, "+"))

+            {

+                if (root.Outgoing != null && root.Outgoing.Children.Length > 0)

+                {

+                    continuation_stack.Push(root);

+                    root = root.Outgoing.Children[0];

+                }

+                else

+                {

+                    // can't find our block

+                    Contract.Assert(false);

+                    return null;

+                }

+            }

+

             // After translation, all potential errors come from asserts.

             while (true)

             {

+

+

                 CmdSeq cmds = b.Cmds;

                 TransferCmd transferCmd = cce.NonNull(b.TransferCmd);

                 for (int i = 0; i < cmds.Length; i++)

@@ -1560,11 +1653,19 @@ namespace Microsoft.Boogie
                         else

                             is_failed_assertion = CodeLabelTrue(rpfp, root, cmd, info, "@");

 

-                        Counterexample newCounterexample =

-                            AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, new Microsoft.Boogie.Model(), info.mvInfo,

-                            boogieContext);

-                        newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

-                        return newCounterexample;

+                        if (is_failed_assertion)

+                        {

+                            if (continuation_stack.Count == 0)

+                            {

+                                Counterexample newCounterexample =

+                                    AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, new Microsoft.Boogie.Model(), info.mvInfo,

+                                    boogieContext);

+                                newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

+                                return newCounterexample;

+                            }

+                            root = continuation_stack.Pop();

+                        }

+                        continue;

                     }

 

                     // Counterexample generation for inlined procedures

@@ -1588,7 +1689,7 @@ namespace Microsoft.Boogie
                             LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr;

                             // Debug.Assert(x != null);

                             int foo = x.asBigNum.ToInt;

-                            orderedStateIds.Add(new Tuple<int, int>(root.number, foo));

+                            orderedStateIds.Add(new StateId(root.Outgoing,foo,info));

                         }

                     }

 

@@ -1600,29 +1701,34 @@ namespace Microsoft.Boogie
 

                     {

                         Term code = CodeLabeledExpr(rpfp, root, cmd, info, "+si_fcall_");

-                        int pos = TransformerArgPosition(rpfp,root,code);

-                        if(pos >= 0)

+                        int pos = TransformerArgPosition(rpfp, root, code);

+                        if (pos >= 0)

                         {

                             RPFP.Node callee = root.Outgoing.Children[pos];

-                            orderedStateIds.Add(new Tuple<int, int>(callee.number, VC.StratifiedVCGen.StratifiedInliningErrorReporter.CALL));

+                            orderedStateIds.Add(new StateId(callee.Outgoing, CALL,info));

                             calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =

                                 new CalleeCounterexampleInfo(

-                                    cce.NonNull(GenerateTrace(rpfp, callee, orderedStateIds, 

-                                                implName2StratifiedInliningInfo[calleeName].impl,false)),

+                                    cce.NonNull(GenerateTrace(rpfp, callee, orderedStateIds,

+                                                implName2StratifiedInliningInfo[calleeName].impl, false)),

                                     new List<object>());

-                            orderedStateIds.Add(new Tuple<int, int>(root.number, VC.StratifiedVCGen.StratifiedInliningErrorReporter.RETURN));

+                            orderedStateIds.Add(new StateId(root.Outgoing, RETURN,info));

                         }

                     }

                 }

 

                 GotoCmd gotoCmd = transferCmd as GotoCmd;

+                List<Block> cuts = null;

+                if (edgesCut.ContainsKey(b))

+                    cuts = edgesCut[b];

+                b = null; 

+                

                 if (gotoCmd != null)

-                {

-                    b = null;

+                {    

+

                     foreach (Block bb in cce.NonNull(gotoCmd.labelTargets))

                     {

                         Contract.Assert(bb != null);

-                        if (CodeLabelFalse(rpfp,root,bb,info,"+"))

+                        if (CodeLabelFalse(rpfp, root, bb, info, "+"))

                         {

                             trace.Add(bb);

                             b = bb;

@@ -1631,12 +1737,186 @@ namespace Microsoft.Boogie
                     }

                     if (b != null) continue;

                 }

+                // HACK: we have to try edges that were cut in generating the VC

+

+                if (cuts != null)

+                    foreach (var bb in cuts)

+                    {

+                        if (CodeLabelFalse(rpfp, root, bb, info, "+"))

+                        {

+                            trace.Add(bb);

+                            b = bb;

+                            break;

+                        }

+                    }

+                if (b != null) continue;

+

                 return null;

             }

 

             

         }

 

+        public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)

+        {

+            // Construct the set of inlined procs in the original program

+            var inlinedProcs = new HashSet<string>();

+            foreach (var decl in program.TopLevelDeclarations)

+            {

+                // Implementations

+                if (decl is Implementation)

+                {

+                    var impl = decl as Implementation;

+                    if (!(impl.Proc is LoopProcedure))

+                    {

+                        inlinedProcs.Add(impl.Name);

+                    }

+                }

+

+                // And recording procedures

+                if (decl is Procedure)

+                {

+                    var proc = decl as Procedure;

+                    if (proc.Name.StartsWith(recordProcName))

+                    {

+                        // Debug.Assert(!(decl is LoopProcedure));

+                        inlinedProcs.Add(proc.Name);

+                    }

+                }

+            }

+            return extractLoopTraceRec(

+              new CalleeCounterexampleInfo(cex, new List<object>()),

+              mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;

+        }

+

+        protected override bool elIsLoop(string procname)

+        {

+            StratifiedInliningInfo info = null;

+            if (implName2StratifiedInliningInfo.ContainsKey(procname))

+            {

+                info = implName2StratifiedInliningInfo[procname];

+            }

+

+            if (info == null) return false;

+

+            var lp = info.impl.Proc as LoopProcedure;

+

+            if (lp == null) return false;

+            return true;

+        }

+

+        private void NumberCexEdges(RPFP.Node node, Dictionary<int,RPFP.Edge> map)

+        {

+            if (node.Outgoing == null)

+                return; // shouldn't happen

+            RPFP.Edge edge = node.Outgoing;

+            map[edge.number] = edge;

+            foreach (var c in edge.Children)

+                NumberCexEdges(c, map);

+        }

+

+        private void GetModelWithStates(Model m, RPFP.Node cex, StratifiedInliningInfo mainInfo,

+                                        List<StateId> orderedStateIds,

+                                        Dictionary<int,Dictionary<string,string>> varSubst)

+        {

+            if (m == null) return;

+            var mvInfo = mainInfo.mvInfo;

+            

+

+            foreach (Variable v in mvInfo.AllVariables)

+            {

+                m.InitialState.AddBinding(v.Name, GetModelValue(m, v, varSubst[cex.Outgoing.number]));

+            }

+

+            Dictionary<int, RPFP.Edge> edgeNumbering = new Dictionary<int,RPFP.Edge>();

+            NumberCexEdges(cex, edgeNumbering);

+

+            int lastCandidate = 0;

+            int lastCapturePoint = CALL;

+            for (int i = 0; i < orderedStateIds.Count; ++i)

+            {

+                var s = orderedStateIds[i];

+                RPFP.Edge edge = s.edge;

+                int candidate = edge.number;

+                int capturePoint = s.capturePoint;

+                Dictionary<string, string> subst = varSubst[candidate];

+

+                string implName = edge.Parent.Name.GetDeclName();

+                var info = s.info.mvInfo;

+

+                if (capturePoint == CALL || capturePoint == RETURN)

+                {

+                    lastCandidate = candidate;

+                    lastCapturePoint = capturePoint;

+                    continue;

+                }

+

+                Contract.Assume(0 <= capturePoint && capturePoint < info.CapturePoints.Count);

+                VC.ModelViewInfo.Mapping map = info.CapturePoints[capturePoint];

+                var prevInc = (lastCapturePoint != CALL && lastCapturePoint != RETURN && candidate == lastCandidate)

+                  ? info.CapturePoints[lastCapturePoint].IncarnationMap : new Hashtable();

+                var cs = m.MkState(map.Description);

+

+                foreach (Variable v in info.AllVariables)

+                {

+                    var e = (Expr)map.IncarnationMap[v];

+

+                    if (e == null)

+                    {

+                        if (lastCapturePoint == CALL || lastCapturePoint == RETURN)

+                        {

+                            cs.AddBinding(v.Name, GetModelValue(m, v, subst));

+                        }

+                        continue;

+                    }

+

+                    if (lastCapturePoint != CALL && lastCapturePoint != RETURN && prevInc[v] == e) continue; // skip unchanged variables

+

+                    Model.Element elt;

+                    if (e is IdentifierExpr)

+                    {

+                        IdentifierExpr ide = (IdentifierExpr)e;

+                        elt = GetModelValue(m, ide.Decl, subst);

+                    }

+                    else if (e is LiteralExpr)

+                    {

+                        LiteralExpr lit = (LiteralExpr)e;

+                        elt = m.MkElement(lit.Val.ToString());

+                    }

+                    else

+                    {

+                        Contract.Assume(false);

+                        elt = m.MkFunc(e.ToString(), 0).GetConstant();

+                    }

+                    cs.AddBinding(v.Name, elt);

+                }

+

+                lastCandidate = candidate;

+                lastCapturePoint = capturePoint;

+            }

+

+            return;

+        }

+

+

+        public readonly static int CALL = -1;

+        public readonly static int RETURN = -2;

+

+        private Model.Element GetModelValue(Model m, Variable v, Dictionary<string,string> subst)

+        {

+            // first, get the unique name

+            string uniqueName;

+

+            VCExprVar vvar = boogieContext.BoogieExprTranslator.TryLookupVariable(v);

+            

+            uniqueName = v.Name;

+            

+            if(subst.ContainsKey(uniqueName))

+                return m.MkElement(subst[uniqueName]);

+            return m.MkFunc("@undefined", 0).GetConstant();

+        }

+

+

     }

 

 

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index 96fdec97..9048f0f5 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -159,8 +159,7 @@ namespace Microsoft.Boogie
             public Edge map;

             public HashSet<string> labels;

             internal Term dual;

-            internal Dictionary<FuncDecl,int> relMap;

-            internal Dictionary<Term,Term> varMap;

+            internal Dictionary<Term,Term> valuation;

         }

 

         

@@ -175,7 +174,8 @@ namespace Microsoft.Boogie
             e.number = ++edgeCount;

             _Parent.Outgoing = e;

             foreach (var c in _Children)

-                c.Incoming.Add(e);

+                if(c != null)

+                  c.Incoming.Add(e);

             return e;

         }

 

@@ -262,10 +262,23 @@ namespace Microsoft.Boogie
 

         public Term Eval(Edge e, Term t)

         {

-            return ctx.MkFalse(); // TODO

+            if (e.valuation == null)

+                e.valuation = new Dictionary<Term, Term>();

+            if (e.valuation.ContainsKey(t))

+                return e.valuation[t];

+            return null; // TODO

+        }

+

+        /** Sets the value in the counterexample of a symbol occuring in the transformer formula of

+         *  a given edge. */

+

+        public void SetValue(Edge e, Term variable, Term value)

+        {

+            if (e.valuation == null)

+                e.valuation = new Dictionary<Term, Term>(); 

+            e.valuation.Add(variable, value);

         }

 

-        

 

         /** Returns true if the given node is empty in the primal solution. For proecudure summaries,

          this means that the procedure is not called in the current counter-model. */

@@ -374,7 +387,7 @@ namespace Microsoft.Boogie
                 }

                 var args = t.GetAppArgs();

                 args = args.Select(x => CollectParamsRec(memo, x, parms, nodes)).ToArray();

-                res = ctx.MkApp(f, args);

+                res = ctx.CloneApp(t, args);

             } // TODO: handle quantifiers

             else

                 res = t;

@@ -470,7 +483,9 @@ namespace Microsoft.Boogie
                 predSubst.Add(edge.F.RelParams[i], edge.Children[i].Name);

             Term body = SubstPreds(predSubst, edge.F.Formula);

             Term head = ctx.MkApp(edge.Parent.Name, edge.F.IndParams);

-            return BindVariables(ctx.MkImplies(body, head));

+            var rule = BindVariables(ctx.MkImplies(body, head));

+            rule = ctx.Letify(rule); // put in let bindings for theorem prover

+            return rule;

         }

 

         /** Get the Z3 query corresponding to the conjunction of the node bounds. */

@@ -484,7 +499,9 @@ namespace Microsoft.Boogie
                     conjuncts.Add(ctx.MkImplies(ctx.MkApp(node.Name, node.Bound.IndParams), node.Bound.Formula));

             }

             Term query = ctx.MkNot(ctx.MkAnd(conjuncts.ToArray()));

-            return BindVariables(query,false); // bind variables existentially

+            query = BindVariables(query,false); // bind variables existentially

+            query = ctx.Letify(query); // put in let bindings for theorem prover

+            return query;

         }

 

         private void CollectVariables(Dictionary<Term, bool> memo, Term t, List<Term> vars)

@@ -521,8 +538,13 @@ namespace Microsoft.Boogie
                 FuncDecl nf = null;

                 var f = t.GetAppDecl();

                 if (subst.TryGetValue(f, out nf))

-                    f = nf;

-                res = ctx.MkApp(f, args);

+                {

+                    res = ctx.MkApp(nf, args);

+                }

+                else

+                {

+                    res = ctx.CloneApp(t, args);

+                }

             } // TODO: handle quantifiers

             else

                 res = t;

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 3748d7f7..988d80fd 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1754,7 +1754,17 @@ namespace VC {
         }

       }

     }

-    public void ConvertCFG2DAG(Implementation impl)

+

+      private void RecordCutEdge(Dictionary<Block,List<Block>> edgesCut, Block from, Block to){

+          if (edgesCut != null)

+          {

+              if (!edgesCut.ContainsKey(from))

+                  edgesCut.Add(from, new List<Block>());

+              edgesCut[from].Add(to);

+          }

+      }

+

+    public void ConvertCFG2DAG(Implementation impl, Dictionary<Block,List<Block>> edgesCut = null)

     {

     Contract.Requires(impl != null);

       impl.PruneUnreachableBlocks();  // This is needed for VCVariety.BlockNested, and is otherwise just an optimization

@@ -1893,11 +1903,13 @@ namespace VC {
             Contract.Assume( gtc.labelNames != null);

             for (int i = 0, n = gtc.labelTargets.Length; i < n; i++)

             {

-              if ( gtc.labelTargets[i] != header )

-              {

-                remainingTargets.Add(gtc.labelTargets[i]);

-                remainingLabels.Add(gtc.labelNames[i]);

-              }

+                if (gtc.labelTargets[i] != header)

+                {

+                    remainingTargets.Add(gtc.labelTargets[i]);

+                    remainingLabels.Add(gtc.labelNames[i]);

+                }

+                else

+                    RecordCutEdge(edgesCut,backEdgeNode, header);

             }

             gtc.labelTargets = remainingTargets;

             gtc.labelNames = remainingLabels;

@@ -1910,6 +1922,8 @@ namespace VC {
             AssumeCmd ac = new AssumeCmd(Token.NoToken,Expr.False);

             backEdgeNode.Cmds.Add(ac);

             backEdgeNode.TransferCmd = new ReturnCmd(Token.NoToken);

+            if (gtc != null && gtc.labelTargets != null && gtc.labelTargets.Length == 1)

+                RecordCutEdge(edgesCut, backEdgeNode, gtc.labelTargets[0]);

           }

           #region Remove the backedge node from the list of predecessor nodes in the header

           BlockSeq newPreds = new BlockSeq();