Added callee args information to calleeCounterexamples

3 files changed, 59 insertions, 10 deletions

diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc
index 086c3b6d..c77c3dc8 100644
--- a/Source/VCGeneration/Check.ssc
+++ b/Source/VCGeneration/Check.ssc
@@ -366,6 +366,34 @@ namespace Microsoft.Boogie
       assert false;

       return 0;

     }

+    

+    public List<object!>! PartitionsToValues(List<int>! args)

+    {

+      List<object!>! vals = new List<object!>();

+      foreach(int i in args)

+      {

+        object! o = (!)partitionToValue[i];

+        if (o is bool) {

+          vals.Add(o);

+        } else if (o is BigNum) {

+          vals.Add(o);

+        } else if (o is List<List<int>!>) {

+          List<List<int>!> array = (List<List<int>!>) o;

+          List<List<object!>!> arrayVal = new List<List<object!>!>();

+          foreach (List<int>! tuple in array) {

+            List<object!> tupleVal = new List<object!>();

+            foreach (int i in tuple) {

+              tupleVal.Add((!)partitionToValue[i]);

+            }

+            arrayVal.Add(tupleVal);

+          }

+          vals.Add(arrayVal);

+        } else {

+          assert false;

+        }

+      }

+      return vals;

+    }

   }

 

   public abstract class ProverInterface

diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc
index 6e63c296..6e87fd0e 100644
--- a/Source/VCGeneration/ConditionGeneration.ssc
+++ b/Source/VCGeneration/ConditionGeneration.ssc
@@ -18,27 +18,37 @@ using Microsoft.Boogie.VCExprAST;
 

 namespace Microsoft.Boogie

 {

+  public class CalleeCounterexampleInfo {

+    public Counterexample! counterexample;

+    public List<object!>! args;

+    

+    public CalleeCounterexampleInfo(Counterexample! cex, List<object!>! x) {

+      counterexample = cex;

+      args = x;

+    }  

+  }

+    

   public abstract class Counterexample 

   {

     [Peer] public BlockSeq! Trace;

     [Peer] public List<string!>! relatedInformation;

     

-    public Dictionary<Absy!, Counterexample!>! calleeCounterexamples;

+    public Dictionary<Absy!, CalleeCounterexampleInfo!>! calleeCounterexamples;

     

     internal Counterexample(BlockSeq! trace)

     {

       this.Trace = trace;

       this.relatedInformation = new List<string!>();

-      this.calleeCounterexamples = new Dictionary<Absy!, Counterexample!>();

+      this.calleeCounterexamples = new Dictionary<Absy!, CalleeCounterexampleInfo!>();

       // base();

     }

     

-    public void AddCalleeCounterexample(Absy! absy, Counterexample! cex)

+    public void AddCalleeCounterexample(Absy! absy, CalleeCounterexampleInfo! cex)

     {

       calleeCounterexamples[absy] = cex;

     }

     

-    public void AddCalleeCounterexample(Dictionary<Absy!, Counterexample!>! cs)

+    public void AddCalleeCounterexample(Dictionary<Absy!, CalleeCounterexampleInfo!>! cs)

     {

       foreach (Absy! absy in cs.Keys)

       {

@@ -64,7 +74,7 @@ namespace Microsoft.Boogie
                 NAryExpr! naryExpr = (NAryExpr!) assumeCmd.Expr;

                 for (int i = 0; i < spaces+4; i++) Console.Write(" ");

                 Console.WriteLine("Inlined call to procedure {0} begins", naryExpr.Fun.FunctionName);

-                calleeCounterexamples[cmd].Print(spaces+4);

+                calleeCounterexamples[cmd].counterexample.Print(spaces+4);

                 for (int i = 0; i < spaces+4; i++) Console.Write(" ");

                 Console.WriteLine("Inlined call to procedure {0} ends", naryExpr.Fun.FunctionName);

               }

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index 5debbfc3..c0144b24 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -1593,7 +1593,7 @@ namespace VC
         assert traceNodes.Contains(entryBlock);

         trace.Add(entryBlock);

 

-        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<Absy!, Counterexample!>());

+        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program, new Dictionary<Absy!, CalleeCounterexampleInfo!>());

 

         if (newCounterexample == null) return;

         

@@ -2045,7 +2045,7 @@ namespace VC
       int cfcPartition = errModel.LookupSkolemFunctionAt(cfcName + "!" + info.uniqueId, values);

       int cfcValue = errModel.LookupPartitionValue(cfcPartition);

       

-      Dictionary<Absy!, Counterexample!> calleeCounterexamples = new Dictionary<Absy!,Counterexample!>();

+      Dictionary<Absy!, CalleeCounterexampleInfo!> calleeCounterexamples = new Dictionary<Absy!, CalleeCounterexampleInfo!>();

       while (true) {

         CmdSeq! cmds = b.Cmds;

         TransferCmd! transferCmd = (!)b.TransferCmd;

@@ -2122,7 +2122,10 @@ namespace VC
             int partition = errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values);

             args.Add(partition);

           }

-          calleeCounterexamples[assumeCmd] = LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args);

+          calleeCounterexamples[assumeCmd] = 

+            new CalleeCounterexampleInfo(

+              LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args),

+              errModel.PartitionsToValues(args));

         }

           

         GotoCmd gotoCmd = transferCmd as GotoCmd;

@@ -2141,7 +2144,12 @@ namespace VC
       return null;

     }

     

-    static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap, Dictionary<string!, LazyInliningInfo!>! implName2LazyInliningInfo, DeclFreeProverContext! context, Program! program, Dictionary<Absy!, Counterexample!>! calleeCounterexamples)

+    static Counterexample TraceCounterexample(

+                          Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, 

+                          Dictionary<Incarnation, Absy!>! incarnationOriginMap, 

+                          Dictionary<string!, LazyInliningInfo!>! implName2LazyInliningInfo, 

+                          DeclFreeProverContext! context, Program! program, 

+                          Dictionary<Absy!, CalleeCounterexampleInfo!>! calleeCounterexamples)

     {

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

       CmdSeq! cmds = b.Cmds;

@@ -2185,7 +2193,10 @@ namespace VC
           string! name = vcExprTranslator.Lookup(var);

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

         }

-        calleeCounterexamples[assumeCmd] = LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args);

+        calleeCounterexamples[assumeCmd] = 

+            new CalleeCounterexampleInfo(

+                LazyCounterexample(errModel, implName2LazyInliningInfo, context, program, calleeName, args),

+                errModel.PartitionsToValues(args));

         #endregion

       }