Conjecture printing for duality and child user time tracking.

7 files changed, 366 insertions, 58 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 98086cf0..83572f2f 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -613,6 +613,8 @@ namespace Microsoft.Boogie {
     public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;

 		

     public string PrintFixedPoint = null;

+

+    public string PrintConjectures = null;

 		

     public bool ExtractLoopsUnrollIrreducible = true; // unroll irreducible loops? (set programmatically)

 

@@ -1135,6 +1137,12 @@ namespace Microsoft.Boogie {
               PrintFixedPoint = args[ps.i];

           }

           return true;

+        case "printConjectures":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              PrintConjectures = args[ps.i];

+          }

+          return true;

         case "siVerbose":

           if (ps.ConfirmArgumentCount(1)) {

             StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 4e895931..56907a89 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -66,6 +66,12 @@ namespace Microsoft.Boogie.SMTLib
       ctx.parent = this;

       this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);

 

+      if (CommandLineOptions.Clo.PrintFixedPoint != null || CommandLineOptions.Clo.PrintConjectures != null)

+      {

+          declHandler = new MyDeclHandler();

+          DeclCollector.SetDeclHandler(declHandler);

+      }

+

       SetupProcess();

 

       if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)

@@ -82,6 +88,7 @@ namespace Microsoft.Boogie.SMTLib
           }

           PrepareCommon();

       }

+		

     }

 

     private void SetupAxiomBuilder(VCExpressionGenerator gen)

@@ -677,27 +684,9 @@ namespace Microsoft.Boogie.SMTLib
 			// get all the predicate definitions

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

 				var line = lines [i];

-				if(line.Name != "define-fun"){

-					HandleProverError ("Prover error: expected define-fun but got:" + line.Name);

-					throw new BadExprFromProver ();

-				}

-				if(line.ArgCount != 4){

-					HandleProverError ("Prover error: define-fun has wrong number of arguments");

-					throw new BadExprFromProver ();

-				}

-				var pname = StripCruft(line.Arguments[0].Name);

-				var pvars = line.Arguments[1];

-				var pbody = line.Arguments[3]; // range has to be Bool

-				var binding = new Dictionary<string,VCExpr>();

-				var pvs = new List<VCExpr>();

-				foreach(var b in pvars.Arguments){

-					var e = SExprToVar (b);

-					pvs.Add (e);

-					binding.Add (b.Name,e);

-				}

-				VCExpr bexpr = SExprToVCExpr(pbody,binding);

-				

-				var annot = rpfp.CreateRelation(pvs.ToArray(),bexpr);

+                string pname;

+                RPFP.Transformer annot;

+                GetDefun(line, out pname, out annot);

 				

 				if(pmap.ContainsKey(pname)){

 					var node = pmap[pname];

@@ -710,6 +699,34 @@ namespace Microsoft.Boogie.SMTLib
 			}

 			

 		}

+

+        private void GetDefun(SExpr line, out string pname, out RPFP.Transformer annot)

+        {

+            if (line.Name != "define-fun")

+            {

+                HandleProverError("Prover error: expected define-fun but got:" + line.Name);

+                throw new BadExprFromProver();

+            }

+            if (line.ArgCount != 4)

+            {

+                HandleProverError("Prover error: define-fun has wrong number of arguments");

+                throw new BadExprFromProver();

+            }

+            pname = StripCruft(line.Arguments[0].Name);

+            var pvars = line.Arguments[1];

+            var pbody = line.Arguments[3]; // range has to be Bool

+            var binding = new Dictionary<string, VCExpr>();

+            var pvs = new List<VCExpr>();

+            foreach (var b in pvars.Arguments)

+            {

+                var e = SExprToVar(b);

+                pvs.Add(e);

+                binding.Add(StripCruft(b.Name), e);

+            }

+            VCExpr bexpr = SExprToVCExpr(pbody, binding);

+

+            annot = rpfp.CreateRelation(pvs.ToArray(), bexpr);

+        }

 		

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

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

@@ -887,10 +904,6 @@ namespace Microsoft.Boogie.SMTLib
         rpfp = _rpfp;

         cex = null;

 			

-		if(CommandLineOptions.Clo.PrintFixedPoint != null){

-			declHandler = new MyDeclHandler();

-		    DeclCollector.SetDeclHandler(declHandler);

-		}

 			

         if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen

 

@@ -900,6 +913,8 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        PrepareCommon(); 

+        

         Push();

         SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

@@ -907,8 +922,6 @@ namespace Microsoft.Boogie.SMTLib
             DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);

         }

 

-        PrepareCommon();

-

         LineariserOptions.Default.LabelsBelowQuantifiers = true;

         List<string> ruleStrings = new List<string>();

         foreach (var edge in rpfp.edges)

@@ -1047,11 +1060,74 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(fixedpoint-pop)");

         Pop();

         AxiomsAreSetup = false;

-		DeclCollector.SetDeclHandler(null);

-		declHandler = null; // just so we can GC it

+

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

+        {

+            ReadConjectures(CommandLineOptions.Clo.PrintConjectures);

+        }

+

         return result;

     }

 

+    class MyFileParser : SExpr.Parser

+    {

+        SMTLibProcessTheoremProver parent;

+

+        public MyFileParser(System.IO.StreamReader _sr, SMTLibProcessTheoremProver _parent)

+            : base(_sr)

+        {

+            parent = _parent;

+        }

+        public override void ParseError(string msg)

+        {

+            parent.HandleProverError("Error in conjecture file from prover: " + msg);

+        }

+    }

+

+    void ReadConjectures(string filename)

+    {

+        try

+        {

+            System.IO.StreamReader sr = new StreamReader(filename + ".tmp");

+            SExpr.Parser p = new MyFileParser(sr, this);

+            var sexps = p.ParseSExprs(false);

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

+            foreach (var e in sexps)

+            {

+                string pname;

+                RPFP.Transformer annot;

+                GetDefun(e, out pname, out annot);

+

+                if (pmap.ContainsKey(pname))

+                {

+                    var c = new RPFP.Conjecture();

+                    c.node = pmap[pname];

+                    c.bound = annot;

+                    rpfp.conjectures.Add(c);

+                }

+                else if (pname[0] != '@')

+                { // if not an internal symbol

+                    HandleProverError("Prover error: got unknown predicate:" + pname);

+                    throw new BadExprFromProver();

+                }

+            }

+            sr.Close();

+        }

+        catch (Exception)

+        {

+            HandleProverError("No conjecture file from prover");

+            throw new BadExprFromProver();

+        }

+    }

+

+    private Dictionary<string, RPFP.Node> GetNodeMap()

+    {

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

+        foreach (var node in rpfp.nodes)

+            pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name, node);

+        return pmap;

+    }

+

     private static HashSet<string> usedLogNames = new HashSet<string>();

 

     private TextWriter OpenOutputFile(string descriptiveName)

diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs
index 461e1ee8..ba07ec27 100644
--- a/Source/Provers/SMTLib/SExpr.cs
+++ b/Source/Provers/SMTLib/SExpr.cs
@@ -106,6 +106,156 @@ namespace Microsoft.Boogie
     }

     #endregion

 

+    #region parsing

+

+    public abstract class Parser

+    {

+        System.IO.StreamReader sr;

+        int linePos = 0;

+        string currLine = null;

+

+        public Parser(System.IO.StreamReader _sr)

+        {

+            sr = _sr;

+        }

+        string Read()

+        {

+            return sr.ReadLine();

+        }

+        char SkipWs()

+        {

+            while (true)

+            {

+                if (currLine == null)

+                {

+                    currLine = Read();

+                    if (currLine == null)

+                        return '\0';

+                }

+

+                while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))

+                    linePos++;

+

+                if (linePos < currLine.Length)

+                    return currLine[linePos];

+                else

+                {

+                    currLine = null;

+                    linePos = 0;

+                }

+            }

+        }

+

+        void Shift()

+        {

+            linePos++;

+        }

+

+        string ParseId()

+        {

+            var sb = new StringBuilder();

+

+            var beg = SkipWs();

+

+            var quoted = beg == '"' || beg == '|';

+            if (quoted)

+                Shift();

+            while (true)

+            {

+                if (linePos >= currLine.Length)

+                {

+                    if (quoted)

+                    {

+                        sb.Append("\n");

+                        currLine = Read();

+                        linePos = 0;

+                        if (currLine == null)

+                            break;

+                    }

+                    else break;

+                }

+

+                var c = currLine[linePos++];

+                if (quoted && c == beg)

+                    break;

+                if (!quoted && (char.IsWhiteSpace(c) || c == '(' || c == ')'))

+                {

+                    linePos--;

+                    break;

+                }

+                if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"')

+                {

+                    sb.Append('"');

+                    linePos++;

+                    continue;

+                }

+                sb.Append(c);

+            }

+

+            return sb.ToString();

+        }

+

+        public abstract void ParseError(string msg);

+

+        public IEnumerable<SExpr> ParseSExprs(bool top)

+        {

+            while (true)

+            {

+                var c = SkipWs();

+                if (c == '\0')

+                    break;

+

+                if (c == ')')

+                {

+                    if (top)

+                        ParseError("stray ')'");

+                    break;

+                }

+

+                string id;

+

+                if (c == '(')

+                {

+                    Shift();

+                    c = SkipWs();

+                    if (c == '\0')

+                    {

+                        ParseError("expecting something after '('");

+                        break;

+                    }

+                    else if (c == '(')

+                    {

+                        id = "";

+                    }

+                    else

+                    {

+                        id = ParseId();

+                    }

+

+                    var args = ParseSExprs(false).ToArray();

+

+                    c = SkipWs();

+                    if (c == ')')

+                    {

+                        Shift();

+                    }

+                    else

+                    {

+                        ParseError("unclosed '(" + id + "'");

+                    }

+                    yield return new SExpr(id, args);

+                }

+                else

+                {

+                    id = ParseId();

+                    yield return new SExpr(id);

+                }

+

+                if (top) break;

+            }

+        }

+    }

+    #endregion

   }

 }

 

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 2374a157..439557c0 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -175,8 +175,11 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    public static System.TimeSpan TotalUserTime = System.TimeSpan.Zero;

+

     public void Close()

     {

+      TotalUserTime += prover.UserProcessorTime;

       try {

         prover.Kill();

       } catch {

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index ed8f0908..c8f49603 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -4,6 +4,7 @@
 //

 //-----------------------------------------------------------------------------

 

+

 using System;

 using System.Collections.Generic;

 using System.Linq;

@@ -200,6 +201,7 @@ namespace Microsoft.Boogie.SMTLib
         // options that work only on the command line

         static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };

 

+

         public static void SetupOptions(SMTLibProverOptions options)

         {

           FindExecutable();

@@ -208,8 +210,10 @@ namespace Microsoft.Boogie.SMTLib
           if (major > 4 || major == 4 && minor >= 3)

           {

 

+              bool fp = false; // CommandLineOptions.Clo.FixedPointEngine != null;

+

             // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

-            options.AddWeakSmtOption("AUTO_CONFIG", "false");

+            if(!fp) options.AddWeakSmtOption("AUTO_CONFIG", "false");

 

             //options.AddWeakSmtOption("MODEL_PARTIAL", "true");

             //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");

@@ -232,7 +236,8 @@ namespace Microsoft.Boogie.SMTLib
 

               // The left-to-right structural case-splitting strategy.

               //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now

-              options.AddWeakSmtOption("smt.CASE_SPLIT", "3");

+

+              if (!fp) options.AddWeakSmtOption("smt.CASE_SPLIT", "3");

 

               // In addition delay adding unit conflicts.

               options.AddWeakSmtOption("smt.DELAY_UNITS", "true");

@@ -251,7 +256,7 @@ namespace Microsoft.Boogie.SMTLib
             // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.

 

             // the following will make the :weight option more usable

-            options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work

+            if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work

 

             //if (options.Inspector != null)

             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

@@ -275,6 +280,11 @@ namespace Microsoft.Boogie.SMTLib
               options.AddWeakSmtOption("smt.array.weak", "true");

               options.AddWeakSmtOption("smt.array.extensional", "false");

             }

+

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

+            {

+                options.AddWeakSmtOption("fixedpoint.conjecture_file", CommandLineOptions.Clo.PrintConjectures + ".tmp");

+            }

           }

           else

           {

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index deb3f2c2..0dc81b0c 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -78,6 +78,15 @@ namespace Microsoft.Boogie
 

         private static Checker old_checker = null;

 

+        public static void CleanUp()

+        {

+            if (old_checker != null)

+            {

+                old_checker.Close();

+                old_checker = null;

+            }

+        }

+

         public FixedpointVC( Program _program, string/*?*/ logFilePath, bool appendLogFile, List<Checker> checkers, Dictionary<string,int> _extraRecBound = null)

             : base(_program, logFilePath, appendLogFile, checkers) 

         {

@@ -763,38 +772,75 @@ namespace Microsoft.Boogie
                     List<Expr> exprs = new List<Expr>();

 

                     {

-						// last ensures clause will be the symbolic one

-						if(info.isMain)

-							continue;

-						var ens = proc.Ensures[proc.Ensures.Count - 1];

-						if(ens.Condition == Expr.False) // this is main

-							continue;

-                        var postExpr = ens.Condition as NAryExpr;

-						var args = postExpr.Args;

-						if(pmap.ContainsKey (impl.Name)){

-							RPFP.Node node = pmap[impl.Name];

-							var ind = node.Annotation.IndParams;

-							var bound = new Dictionary<VCExpr,Expr>(); 

-							for(int i = 0; i < args.Count; i++){

-								bound[ind[i]] = args[i];

-							}

-							var new_ens_cond = VCExprToExpr(node.Annotation.Formula,bound);

-                            if (new_ens_cond != Expr.True)

-                            {

-                                var new_ens = new Ensures(false, new_ens_cond);

-                                var enslist = new List<Ensures>();

-                                enslist.Add(new_ens);

-                                var new_proc = new Procedure(proc.tok, proc.Name, proc.TypeParameters, proc.InParams,

-                                                             proc.OutParams, new List<Requires>(), new List<IdentifierExpr>(), enslist);

-                                new_proc.Emit(twr, 0);

-                            }

-						}

+                        if (pmap.ContainsKey(impl.Name))

+                        {

+                            RPFP.Node node = pmap[impl.Name];

+                            var annot = node.Annotation;

+                            EmitProcSpec(twr, proc, info, annot);

+                        }

                     }

                 }

             }

 			twr.Close ();

 		}

 

+        private void EmitProcSpec(TokenTextWriter twr, Procedure proc, StratifiedInliningInfo info, RPFP.Transformer annot)

+        {

+            // last ensures clause will be the symbolic one

+            if (!info.isMain)

+            {

+                var ens = proc.Ensures[proc.Ensures.Count - 1];

+                if (ens.Condition != Expr.False) // this is main

+                {

+                    var postExpr = ens.Condition as NAryExpr;

+                    var args = postExpr.Args;

+

+                    var ind = annot.IndParams;

+                    var bound = new Dictionary<VCExpr, Expr>();

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

+                    {

+                        bound[ind[i]] = args[i];

+                    }

+                    var new_ens_cond = VCExprToExpr(annot.Formula, bound);

+                    if (new_ens_cond != Expr.True)

+                    {

+                        var new_ens = new Ensures(false, new_ens_cond);

+                        var enslist = new List<Ensures>();

+                        enslist.Add(new_ens);

+                        var new_proc = new Procedure(proc.tok, proc.Name, proc.TypeParameters, proc.InParams,

+                                                     proc.OutParams, new List<Requires>(), new List<IdentifierExpr>(), enslist);

+                        new_proc.Emit(twr, 0);

+                    }

+                }

+            }

+        }

+

+        static int ConjectureFileCounter = 0;

+

+        private void ConjecturesToSpecs()

+        {

+

+            if (mode != Mode.Corral || CommandLineOptions.Clo.PrintConjectures == null)

+                return; // not implemented for other annotation modes yet

+

+            var twr = new TokenTextWriter(CommandLineOptions.Clo.PrintConjectures + "." + ConjectureFileCounter.ToString());

+            ConjectureFileCounter++;

+

+            foreach (var c in rpfp.conjectures)

+            {

+                var name = c.node.Name.GetDeclName();

+                if (implName2StratifiedInliningInfo.ContainsKey(name))

+                {

+                    StratifiedInliningInfo info = implName2StratifiedInliningInfo[c.node.Name.GetDeclName()];

+                    Implementation impl = info.impl;

+                    Procedure proc = impl.Proc;

+                    EmitProcSpec(twr, proc, info, c.bound);

+                }

+            }

+

+            twr.Close ();     

+        }

+

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

         {

             Term res;

@@ -1603,15 +1649,19 @@ namespace Microsoft.Boogie
                             // cex.Print(0);  // just for testing

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

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

+                            ConjecturesToSpecs();

                             return VC.ConditionGeneration.Outcome.Errors;

                         case RPFP.LBool.False:

                             Console.WriteLine("Procedure is correct.");

 							FixedPointToSpecs();

+                            ConjecturesToSpecs();

                             return Outcome.Correct;

                         case RPFP.LBool.Undef:

                             Console.WriteLine("Inconclusive result.");

+                            ConjecturesToSpecs();

                             return Outcome.ReachedBound;

                     }

+                    

                 }

 

                 return Outcome.Inconclusive;

diff --git a/Source/VCGeneration/RPFP.cs b/Source/VCGeneration/RPFP.cs
index e7df7be6..ed3842d5 100644
--- a/Source/VCGeneration/RPFP.cs
+++ b/Source/VCGeneration/RPFP.cs
@@ -325,6 +325,17 @@ namespace Microsoft.Boogie
             return res;

         }

 

+        /** This represents a conjecture that a given node is upper-boudned

+            by bound. */

+        public class Conjecture

+        {

+            public Node node;

+            public Transformer bound;

+        }

+

+        /** This is a list of conjectures generated during solving. */

+

+        public List<Conjecture> conjectures = new List<Conjecture>();

 

         /** Construct an RPFP graph with a given interpolating prover context. It is allowed to

             have multiple RPFP's use the same context, but you should never have teo RPFP's