Stratified inlining: Added concrete values to error traces. Added an extra flag "inferLeastForUnsat".

2 files changed, 50 insertions, 3 deletions

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 78cf4085..5323bb03 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -167,9 +167,17 @@ namespace Microsoft.Boogie {
                 if (calleeCounterexamples.ContainsKey(loc))

                 {

                     var cmd = getTraceCmd(loc);

-                    Console.WriteLine("{1}Inlined call to procedure {0} begins", getCalledProcName(cmd), ind);

+                    var calleeName = getCalledProcName(cmd);

+                    if (calleeName == "boogie_si_record_int" && CommandLineOptions.Clo.StratifiedInlining > 0)

+                    {

+                        Contract.Assert(calleeCounterexamples[loc].args.Count == 1);

+                        var arg = calleeCounterexamples[loc].args[0];

+                        Console.WriteLine("{0}value = {1}", ind, arg.ToString());

+                    }

+                    Console.WriteLine("{1}Inlined call to procedure {0} begins", calleeName, ind);

                     calleeCounterexamples[loc].counterexample.Print(indent + 4);

-                    Console.WriteLine("{1}Inlined call to procedure {0} ends", getCalledProcName(cmd), ind);

+                    Console.WriteLine("{1}Inlined call to procedure {0} ends", calleeName, ind);

+                    

                 }

             }

           }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index a234a0dc..c57863a3 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -1440,6 +1440,11 @@ namespace VC
                 {

                     substForallDict.Add(info.interfaceExprVars[i], expr[i]);

                 }

+                if (procName == "boogie_si_record_int")

+                {

+                    Contract.Assert(expr.Length > program.GlobalVariables().Count);

+                    calls.argExprMap.Add(id, expr[program.GlobalVariables().Count]);

+                }

                 VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

 

                 SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen);

@@ -1521,6 +1526,12 @@ namespace VC
                 {

                     substForallDict.Add(info.interfaceExprVars[i], expr[i]);

                 }

+                if (procName == "boogie_si_record_int")

+                {

+                    Contract.Assert(expr.Length > program.GlobalVariables().Count);

+                    calls.argExprMap.Add(id, expr[program.GlobalVariables().Count]);

+                }

+

                 VCExprSubstitution substForall = new VCExprSubstitution(substForallDict, new Dictionary<TypeVariable, Microsoft.Boogie.Type>());

 

                 SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen); Contract.Assert(subst != null);

@@ -1652,6 +1663,9 @@ namespace VC
             public HashSet<int> recentlyAddedCandidates;

             // Name of main procedure

             private string mainProcName;

+            // A map from candidate id to the VCExpr that represents its

+            // first argument (used for obtaining concrete values in error trace)

+            public Dictionary<int, VCExpr> argExprMap;

 

             public HashSet<int> forcedCandidates;

 

@@ -1706,6 +1720,7 @@ namespace VC
                 persistentNameCache[0] = "0";

                 persistentNameInv["0"] = 0;

                 recentlyAddedCandidates = new HashSet<int>();

+                argExprMap = new Dictionary<int, VCExpr>();

 

                 forcedCandidates = new HashSet<int>();

             }

@@ -2292,10 +2307,34 @@ namespace VC
                         }

                         else

                         {

+                            var values = new List<object>();

+                            if (calleeName == "boogie_si_record_int")

+                            {

+                                // Record concrete value of the argument to this procedure

+                                var args = new List<int>();

+                                var expr = calls.argExprMap[calleeId];

+                                if (expr is VCExprIntLit)

+                                {

+                                    args.Add(errModel.valueToPartition[(expr as VCExprIntLit).Val.ToInt]);

+                                }

+                                else if (expr is VCExprVar)

+                                {

+                                    var idExpr = expr as VCExprVar;

+                                    string name = context.Lookup(idExpr);

+                                    Contract.Assert(name != null);

+                                    args.Add(errModel.identifierToPartition[name]);

+                                }

+                                else

+                                {

+                                    Contract.Assert(false);

+                                }

+                                values = errModel.PartitionsToValues(args);

+                            }

+

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

                                 new CalleeCounterexampleInfo(

                                     cce.NonNull(GenerateTrace(labels, errModel, mvInfo, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),

-                                    new List<object>());

+                                    values);

                         }

                     }