Getting fixed point backend to work with Corral.

6 files changed, 185 insertions, 8 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 3e923ee9..fcef6082 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -460,6 +460,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 {

@@ -1276,6 +1277,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 f2628130..be98eb5b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -560,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);

@@ -649,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/ExprExtensions.cs b/Source/VCGeneration/ExprExtensions.cs
index e242257f..d63f4fc2 100644
--- a/Source/VCGeneration/ExprExtensions.cs
+++ b/Source/VCGeneration/ExprExtensions.cs
@@ -205,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);

@@ -213,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 5750a738..bc6a7ce0 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -615,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

@@ -1061,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();

             }

@@ -1117,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;

         }

 

@@ -1191,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

@@ -1348,8 +1352,11 @@ 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?

@@ -1404,7 +1411,7 @@ 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;

 

@@ -1423,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;

@@ -1750,6 +1757,54 @@ namespace Microsoft.Boogie
             

         }

 

+        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)

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index 5d055b57..9048f0f5 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -174,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;

         }

 

@@ -482,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. */

@@ -496,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)