1. couple of bug fixes in interprocedural error trace generation

2. added facility for giving weights to the generated quantifiers for lazy inlining; however, left the weights at default 1.

2 files changed, 40 insertions, 9 deletions

diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc
index c77c3dc8..0ccbd843 100644
--- a/Source/VCGeneration/Check.ssc
+++ b/Source/VCGeneration/Check.ssc
@@ -333,6 +333,17 @@ namespace Microsoft.Boogie
       return 0;

     }

     

+    private string! LookupSkolemConstant(string! name) {

+      foreach (string! functionName in identifierToPartition.Keys)

+      {

+        int index = functionName.LastIndexOf("!");

+        if (index == -1) continue;

+        string! newFunctionName = (!)functionName.Remove(index);

+        if (newFunctionName.Equals(name))

+          return functionName;

+      }

+      return "";

+    }

     private string! LookupSkolemFunction(string! name) {

       foreach (string! functionName in definedFunctions.Keys)

       {

@@ -342,12 +353,19 @@ namespace Microsoft.Boogie
         if (newFunctionName.Equals(name))

           return functionName;

       }

-      assert false;

       return "";

     }

     public int LookupSkolemFunctionAt(string! functionName, List<int>! values)

     {

-      List<List<int>>! tuples = this.definedFunctions[LookupSkolemFunction(functionName)];

+      string! actualFunctionName = LookupSkolemFunction(functionName);

+      if (actualFunctionName.Equals(""))

+      {

+        // The skolem function is actually a skolem constant

+        actualFunctionName = LookupSkolemConstant(functionName);

+        assert !actualFunctionName.Equals("");

+        return identifierToPartition[actualFunctionName];

+      }

+      List<List<int>>! tuples = this.definedFunctions[actualFunctionName];

       assert tuples.Count > 0;

       // the last tuple is a dummy tuple

       for (int n = 0; n < tuples.Count - 1; n++)

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index c0144b24..f7afc6cf 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -119,7 +119,7 @@ namespace VC
         if (impl == null) continue;

         Procedure! proc = (!)impl.Proc;

         if (proc.FindExprAttribute("inline") != null) {

-          LazyInliningInfo info = new LazyInliningInfo(impl, program, implName2LazyInliningInfo.Count);

+          LazyInliningInfo info = new LazyInliningInfo(impl, program, QuantifierExpr.GetNextSkolemId());

           implName2LazyInliningInfo[impl.Name] = info;

           impl.LocVars.Add(info.controlFlowVariable);

           ExprSeq! exprs = new ExprSeq();

@@ -226,7 +226,8 @@ namespace VC
       }

       if (privateVars.Count > 0)

       {

-        vcexpr = gen.Exists(new List<TypeVariable!>(), privateVars, new List<VCTrigger!>(), new VCQuantifierInfos(impl.Name, info.uniqueId, false, null), vcexpr);

+        vcexpr = gen.Exists(new List<TypeVariable!>(), privateVars, new List<VCTrigger!>(), 

+                            new VCQuantifierInfos(impl.Name, info.uniqueId, false, null), vcexpr);

       }

       

       List<VCExpr!> interfaceExprs = new List<VCExpr!>();

@@ -246,7 +247,10 @@ namespace VC
       triggers.Add(trigger);

       

       interfaceExprVars.Reverse();

-      vcexpr = gen.Forall(interfaceExprVars, triggers, vcexpr);

+      Expr e = new LiteralExpr(Token.NoToken, BigNum.FromInt(1));

+      QKeyValue q = new QKeyValue(Token.NoToken, "weight", new List<object!>(new object![] { e }), null);

+      vcexpr = gen.Forall(new List<TypeVariable!>(), interfaceExprVars, triggers, 

+                          new VCQuantifierInfos(impl.Name, QuantifierExpr.GetNextSkolemId(), false, q), vcexpr);

       checker.TheoremProver.PushVCExpression(vcexpr);

       

       info.vcexpr = vcexpr;

@@ -2071,6 +2075,8 @@ namespace VC
           List<int>! args = new List<int>();

           foreach (Expr! expr in naryExpr.Args)

           {

+            VCExprVar exprVar;

+            string name;

             LiteralExpr litExpr = expr as LiteralExpr;

             if (litExpr != null) 

             {

@@ -2082,6 +2088,14 @@ namespace VC
             assert idExpr != null;

             Variable! var = (!)idExpr.Decl;

             

+            if (var is Constant) 

+            {

+              exprVar = boogieExprTranslator.LookupVariable(var);

+              name = vcExprTranslator.Lookup(exprVar);

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

+              continue;

+            }

+            

             int index = 0;

             List<GlobalVariable!> globalVars = program.GlobalVariables();

             foreach (Variable! global in globalVars)

@@ -2117,10 +2131,9 @@ namespace VC
               continue;

             }

             

-            VCExprVar! exprVar = boogieExprTranslator.LookupVariable(var);

-            string! name = vcExprTranslator.Lookup(exprVar);

-            int partition = errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values);

-            args.Add(partition);

+            exprVar = boogieExprTranslator.LookupVariable(var);

+            name = vcExprTranslator.Lookup(exprVar);

+            args.Add(errModel.LookupSkolemFunctionAt(name + "!" + info.uniqueId, values));

           }

           calleeCounterexamples[assumeCmd] = 

             new CalleeCounterexampleInfo(