First cut of lazy inlining. The option can be turned on by the flag /lazyInline:1. It is off by default. This option currently does not support loops and recursion and also does not allow assertions and specifications in inlined procedures. The usage is currently not documented.

5 files changed, 565 insertions, 59 deletions

diff --git a/Source/VCGeneration/Check.ssc b/Source/VCGeneration/Check.ssc
index ca434ec5..086c3b6d 100644
--- a/Source/VCGeneration/Check.ssc
+++ b/Source/VCGeneration/Check.ssc
@@ -12,6 +12,7 @@ using System.Diagnostics;
 using Microsoft.Contracts;

 using Microsoft.Boogie.AbstractInterpretation;

 using Microsoft.Boogie.VCExprAST;

+using Microsoft.Basetypes;

 

 namespace Microsoft.Boogie

 {

@@ -41,8 +42,9 @@ namespace Microsoft.Boogie
 

     public readonly AutoResetEvent! ProverDone = new AutoResetEvent(false);

 

-    private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation! impl)

+    private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl)

     {

+      if (impl == null) return CommandLineOptions.Clo.Bitvectors;

       bool force_int = false;

       bool force_native = false;

       ((!)impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int);

@@ -54,7 +56,7 @@ namespace Microsoft.Boogie
       return CommandLineOptions.Clo.Bitvectors;

     }

 

-    public bool WillingToHandle(Implementation! impl, int timeout)

+    public bool WillingToHandle(Implementation impl, int timeout)

     {

       return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl);

     }

@@ -100,9 +102,9 @@ namespace Microsoft.Boogie
     /////////////////////////////////////////////////////////////////////////////////

 

     /// <summary>

-    /// Constructor.  Initialize a the checker with the program and log file.

+    /// Constructor.  Initialize a checker with the program and log file.

     /// </summary>

-    public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation! impl, int timeout)

+    public Checker(VC.ConditionGeneration! vcgen, Program! prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout)

     {

       this.bitvectors = BvHandlingForImpl(impl);

       this.timeout = timeout;

@@ -310,6 +312,60 @@ namespace Microsoft.Boogie
     }

 

     public virtual void Print(TextWriter! writer) { }

+    

+    public int LookupPartitionValue(int partition)

+    {

+      BigNum bignum = (BigNum) (!)partitionToValue[partition];

+      return bignum.ToInt;

+    }

+        

+    public int LookupControlFlowFunctionAt(int cfc, int id)

+    {

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

+      foreach (List<int> tuple in tuples)

+      {

+        if (tuple == null) continue;

+        if (tuple.Count != 3) continue;

+        if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id)

+          return LookupPartitionValue(tuple[2]);

+      }

+      assert false;

+      return 0;

+    }

+    

+    private string! LookupSkolemFunction(string! name) {

+      foreach (string! functionName in definedFunctions.Keys)

+      {

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

+        if (index == -1) continue;

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

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

+      assert tuples.Count > 0;

+      // the last tuple is a dummy tuple

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

+      {

+        List<int>! tuple = (!)tuples[n];

+        assert tuple.Count - 1 <= values.Count;

+        for (int i = 0, j = 0; i < values.Count; i++)

+        {

+          if (values[i] == tuple[j]) {

+            // succeeded in matching tuple[j]

+            j++; 

+            if (j == tuple.Count-1) return tuple[tuple.Count - 1];

+          }

+        }

+      }

+      assert false;

+      return 0;

+    }

   }

 

   public abstract class ProverInterface

diff --git a/Source/VCGeneration/ConditionGeneration.ssc b/Source/VCGeneration/ConditionGeneration.ssc
index 7d71f166..6e63c296 100644
--- a/Source/VCGeneration/ConditionGeneration.ssc
+++ b/Source/VCGeneration/ConditionGeneration.ssc
@@ -23,13 +23,57 @@ namespace Microsoft.Boogie
     [Peer] public BlockSeq! Trace;

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

     

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

+    

     internal Counterexample(BlockSeq! trace)

     {

       this.Trace = trace;

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

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

       // base();

     }

     

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

+    {

+      calleeCounterexamples[absy] = cex;

+    }

+    

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

+    {

+      foreach (Absy! absy in cs.Keys)

+      {

+        AddCalleeCounterexample(absy, cs[absy]);

+      }

+    }

+    

+    public void Print(int spaces)

+    {

+      foreach (Block! b in Trace) {

+        if (b.tok == null) {

+           Console.WriteLine("    <intermediate block>");

+        } else {

+          // for ErrorTrace == 1 restrict the output; 

+          // do not print tokens with -17:-4 as their location because they have been 

+          // introduced in the translation and do not give any useful feedback to the user

+          if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {

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

+            Console.WriteLine("{0}({1},{2}): {3}", b.tok.filename, b.tok.line, b.tok.col, b.Label);

+            foreach (Cmd! cmd in b.Cmds) {

+              if (calleeCounterexamples.ContainsKey(cmd)) {

+                AssumeCmd! assumeCmd = (AssumeCmd!) cmd;

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

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

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

+              }

+            }

+          }

+        }

+      }

+    }

+    

     public abstract int GetLocation();

   }

 

@@ -41,7 +85,7 @@ namespace Microsoft.Boogie
       return -1;

     }

   }

-    

+  

   public class AssertCounterexample : Counterexample

   {

     [Peer] public AssertCmd! FailingAssert;

@@ -158,16 +202,15 @@ namespace VC
 

     public enum Outcome { Correct, Errors, TimedOut, OutOfMemory, Inconclusive }

  

-    protected readonly List<Checker!>! provers = new List<Checker!>();

+    protected readonly List<Checker!>! checkers = new List<Checker!>();

     protected Implementation current_impl = null;

 

-

     // shared across each implementation; created anew for each implementation

     protected Hashtable /*Variable -> int*/ variable2SequenceNumber;

     public Dictionary<Incarnation, Absy!>! incarnationOriginMap = new Dictionary<Incarnation, Absy!>();

 

     // used only by FindCheckerFor

-    protected Program! program;

+    public Program! program;

     protected string/*?*/ logFilePath;

     protected bool appendLogFile;

     

@@ -496,28 +539,28 @@ namespace VC
 #endregion

 

     

-    protected Checker! FindCheckerFor(Implementation! impl, int timeout)

+    protected Checker! FindCheckerFor(Implementation impl, int timeout)

     {

       int i = 0;

-      while (i < provers.Count) {

-        if (provers[i].Closed) {

-          provers.RemoveAt(i);

+      while (i < checkers.Count) {

+        if (checkers[i].Closed) {

+          checkers.RemoveAt(i);

           continue;

         } else {

-          if (!provers[i].IsBusy && provers[i].WillingToHandle(impl, timeout)) return provers[i];

+          if (!checkers[i].IsBusy && checkers[i].WillingToHandle(impl, timeout)) return checkers[i];

         }

         ++i;

       }

       string? log = logFilePath;

-      if (log != null && !log.Contains("@PROC@") && provers.Count > 0)

-        log = log + "." + provers.Count;

+      if (log != null && !log.Contains("@PROC@") && checkers.Count > 0)

+        log = log + "." + checkers.Count;

       Checker! ch = new Checker(this, program, log, appendLogFile, impl, timeout); 

-      provers.Add(ch);

+      checkers.Add(ch);

       return ch;

     }

     

 

-    public void Close() { foreach (Checker! prover in provers) prover.Close(); }

+    public void Close() { foreach (Checker! checker in checkers) checker.Close(); }

 

 

     protected class CounterexampleCollector : VerifierCallback

@@ -636,7 +679,6 @@ namespace VC
       return new List<Block!>();

     }

 

-

     protected Variable! CreateIncarnation(Variable! x, Absy a)

       requires this.variable2SequenceNumber != null;

       requires this.current_impl != null;

@@ -675,7 +717,7 @@ namespace VC
     {

       if (b.Predecessors.Length == 0)

       {

-        return new Hashtable /*Variable -> Expr*/ ();

+        return new Hashtable();

       }

 

       Hashtable /*Variable -> Expr*/ incarnationMap = null;

@@ -788,8 +830,7 @@ namespace VC
       #endregion

     }

 

-

-    protected void Convert2PassiveCmd(Implementation! impl)

+    protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation! impl)

     {

       #region Convert to Passive Commands

 

@@ -824,6 +865,7 @@ namespace VC
       // Now we can process the nodes in an order so that we're guaranteed to have

       // processed all of a node's predecessors before we process the node.

       Hashtable /*Block -> IncarnationMap*/ block2Incarnation = new Hashtable/*Block -> IncarnationMap*/();

+      Block exitBlock = null;

       foreach (Block! b in sortedNodes )

       {

         assert !block2Incarnation.Contains(b);

@@ -834,8 +876,13 @@ namespace VC
         #endregion Each block's map needs to be available to successor blocks

 

         TurnIntoPassiveBlock(b, incarnationMap, oldFrameSubst);

+        exitBlock = b;

       }

       

+      // Verify that exitBlock is indeed the unique exit block

+      assert exitBlock != null;

+      assert exitBlock.TransferCmd is ReturnCmd;

+      

       // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation

       foreach (Formal! f in impl.OutParams) {

         f.TypedIdent.WhereExpr = null;

@@ -849,6 +896,8 @@ namespace VC
         EmitImpl(impl, true);

       }

       #endregion    

+      

+      return (Hashtable) block2Incarnation[exitBlock];

     }

         

     /// <summary> 

@@ -879,7 +928,7 @@ namespace VC
         {

           AssignCmd! assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments

           #region Substitute all variables in E with the current map

-          List<Expr!>! copies = new List<Expr!> ();

+          List<Expr!> copies = new List<Expr!> ();

           foreach (Expr! e in assign.Rhss)

             copies.Add(Substituter.ApplyReplacingOldExprs(incarnationSubst,

                                                           oldFrameSubst,

diff --git a/Source/VCGeneration/Context.ssc b/Source/VCGeneration/Context.ssc
index be32cabe..2db00964 100644
--- a/Source/VCGeneration/Context.ssc
+++ b/Source/VCGeneration/Context.ssc
@@ -28,7 +28,7 @@ namespace Microsoft.Boogie
     public virtual void AddAxiom(Axiom! a, string attributes) { ProcessDeclaration(a); }

     public abstract void AddAxiom(VCExpr! vc);

     public virtual void DeclareGlobalVariable(GlobalVariable! v, string attributes) { ProcessDeclaration(v); }

-

+    

     public abstract VCExpressionGenerator! ExprGen { get; }

     public abstract Boogie2VCExprTranslator! BoogieExprTranslator { get; }

     public abstract VCGenerationOptions! VCGenOptions { get; }

@@ -194,6 +194,7 @@ namespace Microsoft.Boogie
   // by the various provers

   public abstract class VCExprTranslator : ICloneable {

     public abstract string! translate(VCExpr! expr, int polarity);

+    public abstract string! Lookup(VCExprVar! var);

     public abstract Object! Clone();    

   }

 }

diff --git a/Source/VCGeneration/VC.ssc b/Source/VCGeneration/VC.ssc
index ee5d3d10..faa9e55b 100644
--- a/Source/VCGeneration/VC.ssc
+++ b/Source/VCGeneration/VC.ssc
@@ -27,12 +27,18 @@ namespace VC
     /// <summary>

     /// Constructor.  Initializes the theorem prover.

     /// </summary>

+    [NotDelayed]

     public VCGen(Program! program, string/*?*/ logFilePath, bool appendLogFile)

       // throws ProverException

     {

-      base(program);

       this.appendLogFile = appendLogFile;

       this.logFilePath = logFilePath;

+      implName2LazyInliningInfo = new Dictionary<string!, LazyInliningInfo!>();

+      base(program);

+      if (CommandLineOptions.Clo.LazyInlining)

+      {

+        this.GenerateVCsForLazyInlining(program);

+      }

       // base();

     }

 

@@ -58,10 +64,195 @@ namespace VC
       return new AssumeCmd(assrt.tok, expr);

     }

     

-

-

-   

-

+    #region LazyInlining

+    public class LazyInliningInfo {

+      public Implementation! impl;

+      public int uniqueId;

+      public Function! function;

+      public Variable! controlFlowVariable;

+      public VCExpr vcexpr;

+      public Dictionary<Incarnation, Absy!> incarnationOriginMap;

+      public Hashtable /*Variable->Expr*/ exitIncarnationMap;

+      public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins;

+      public Hashtable/*<int, Absy!>*/ label2absy;

+      

+      public LazyInliningInfo(Implementation! impl, Program! program, int uniqueId)

+      {

+        this.impl = impl;

+        this.uniqueId = uniqueId;

+        this.controlFlowVariable = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "cfc", Microsoft.Boogie.Type.Int));

+        

+        Procedure! proc = (!)impl.Proc;

+        VariableSeq! interfaceVars = new VariableSeq();

+        foreach (Variable! v in program.GlobalVariables())

+        {

+          interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));

+        }

+        foreach (Variable! v in proc.InParams)

+        {

+          interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));

+        }

+        foreach (Variable! v in proc.OutParams)

+        {

+          interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));

+        }

+        foreach (IdentifierExpr! e in proc.Modifies)

+        {

+          if (e.Decl == null) continue;

+          Variable! v = e.Decl;

+          interfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));

+        }

+        TypedIdent! ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);

+        Formal! returnVar = new Formal(Token.NoToken, ti, false);

+        this.function = new Function(Token.NoToken, proc.Name, interfaceVars, returnVar);

+      }

+    }

+    

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

+    

+    public void GenerateVCsForLazyInlining(Program! program)

+    {

+      Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime);

+      foreach (Declaration! decl in program.TopLevelDeclarations)

+      {

+        Implementation impl = decl as Implementation;

+        if (impl == null) continue;

+        Procedure! proc = (!)impl.Proc;

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

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

+          implName2LazyInliningInfo[impl.Name] = info;

+          impl.LocVars.Add(info.controlFlowVariable);

+          ExprSeq! exprs = new ExprSeq();

+          foreach (Variable! v in program.GlobalVariables())

+          {

+            exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

+          }

+          foreach (Variable! v in proc.InParams)

+          {

+            exprs.Add(new IdentifierExpr(Token.NoToken, v));

+          }

+          foreach (Variable! v in proc.OutParams)

+          {

+            exprs.Add(new IdentifierExpr(Token.NoToken, v));

+          }

+          foreach (IdentifierExpr! ie in proc.Modifies)

+          {

+            exprs.Add(ie);

+          }

+          Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(info.function), exprs);

+          proc.Ensures.Add(new Ensures(true, freePostExpr));

+        }

+      }

+      

+      bool oldOptionLiveVariableAnalysis = CommandLineOptions.Clo.LiveVariableAnalysis;

+      CommandLineOptions.Clo.LiveVariableAnalysis = false;

+      foreach (LazyInliningInfo! info in implName2LazyInliningInfo.Values)

+      {

+        GenerateVCForLazyInlining(program, info, checker);

+      }

+      CommandLineOptions.Clo.LiveVariableAnalysis = oldOptionLiveVariableAnalysis;

+    }

+    

+    private void GenerateVCForLazyInlining(Program! program, LazyInliningInfo! info, Checker! checker)

+    requires info.impl != null;

+    requires info.impl.Proc != null;

+    {

+      Implementation! impl = info.impl;

+      ConvertCFG2DAG(impl, program);

+      info.gotoCmdOrigins = PassifyImpl(impl, program);

+      assert info.exitIncarnationMap != null;

+      Hashtable/*<int, Absy!>*/! label2absy;

+      VCExpressionGenerator! gen = checker.VCExprGen;

+      VCExpr! vcexpr = gen.Not(GenerateVC(impl, info.controlFlowVariable, out label2absy, checker));

+      info.label2absy = label2absy;

+      

+      Boogie2VCExprTranslator! translator = checker.TheoremProver.Context.BoogieExprTranslator; 

+      List<VCExprVar!> interfaceExprVars = new List<VCExprVar!>();

+      foreach (Variable! v in program.GlobalVariables())

+      {

+        interfaceExprVars.Add(translator.LookupVariable(v));

+      }

+      

+      foreach (Variable! v in impl.InParams)

+      {

+        interfaceExprVars.Add(translator.LookupVariable(v));

+      }

+      

+      VCExpr! allAssumeExpr = VCExpressionGenerator.True;

+      foreach (Variable! v in impl.OutParams)

+      {

+        VCExprVar! vcvar = gen.Variable(v.Name, v.TypedIdent.Type);

+        interfaceExprVars.Add(vcvar);

+        VCExpr assumeExpr = null;

+        if (info.exitIncarnationMap.ContainsKey(v))

+        {

+          Expr! ie = (Expr!) info.exitIncarnationMap[v];

+          assumeExpr = gen.Eq(vcvar, translator.Translate(ie));

+        }

+        else

+        {

+          assumeExpr = gen.Eq(vcvar, translator.LookupVariable(v));

+        }

+        allAssumeExpr = gen.And(allAssumeExpr, assumeExpr);

+      }

+      foreach (IdentifierExpr! e in impl.Proc.Modifies)

+      {

+        if (e.Decl == null) continue;

+        Variable! v = e.Decl;

+        VCExprVar! vcvar = gen.Variable(v.Name, v.TypedIdent.Type);

+        interfaceExprVars.Add(vcvar);

+        VCExpr assumeExpr = null;

+        if (info.exitIncarnationMap.ContainsKey(v))

+        {

+          Expr! ie = (Expr!) info.exitIncarnationMap[v];

+          assumeExpr = gen.Eq(vcvar, translator.Translate(ie));

+        }

+        else

+        {

+          assumeExpr = gen.Eq(vcvar, translator.LookupVariable(v));

+        }

+        allAssumeExpr = gen.And(allAssumeExpr, assumeExpr);

+      }

+      vcexpr = gen.And(vcexpr, allAssumeExpr);

+      

+      List<VCExprVar!> privateVars = new List<VCExprVar!>();

+      foreach (Variable! v in impl.LocVars)

+      {

+        privateVars.Add(translator.LookupVariable(v));

+      }

+      foreach (Variable! v in impl.OutParams)

+      {

+        privateVars.Add(translator.LookupVariable(v));

+      }

+      if (privateVars.Count > 0)

+      {

+        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!>();

+      foreach (VCExprVar! ev in interfaceExprVars)

+      {

+        interfaceExprs.Add(ev);

+      }

+      Function! function = (!)info.function;

+      VCExpr! expr = gen.Function(function, interfaceExprs);

+      

+      vcexpr = gen.Implies(expr, vcexpr);

+      

+      List<VCExpr!> exprs = new List<VCExpr!>();

+      exprs.Add(expr);

+      VCTrigger! trigger = new VCTrigger(true, exprs);

+      List<VCTrigger!> triggers = new List<VCTrigger!>();

+      triggers.Add(trigger);

+      

+      interfaceExprVars.Reverse();

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

+      checker.TheoremProver.PushVCExpression(vcexpr);

+      

+      info.vcexpr = vcexpr;

+    }

+    #endregion

+    

     #region Soundness smoke tester

     class SmokeTester

     {

@@ -272,7 +463,7 @@ namespace VC
         parent.PassifyImpl(impl, program);

         Hashtable! label2Absy;

         Checker! ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);

-        VCExpr! vc = parent.GenerateVC(impl, out label2Absy, ch);

+        VCExpr! vc = parent.GenerateVC(impl, null, out label2Absy, ch);

         impl.Blocks = backup;

 

         if (CommandLineOptions.Clo.TraceVerify) {

@@ -1066,12 +1257,12 @@ namespace VC
         checker = parent.FindCheckerFor(impl, timeout);

 

         Hashtable/*<int, Absy!>*/! label2absy;

-        VCExpr! vc = parent.GenerateVC(impl, out label2absy, checker);

+        VCExpr! vc = parent.GenerateVC(impl, null, out label2absy, checker);

         

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {

-          reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback);

+          reporter = new ErrorReporterLocal(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, (DeclFreeProverContext!) this.Checker.TheoremProver.Context, parent.program);

         } else {

-          reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback);

+          reporter = new ErrorReporter(gotoCmdOrigins, label2absy, impl.Blocks, parent.incarnationOriginMap, callback, parent.implName2LazyInliningInfo, (DeclFreeProverContext!) this.Checker.TheoremProver.Context, parent.program);

         }

         

         if (CommandLineOptions.Clo.TraceVerify && no >= 0) 

@@ -1084,7 +1275,6 @@ namespace VC
         if (no >= 0)

           desc += "_split" + no;

         checker.BeginCheck(desc, vc, reporter);

-

       }

 

       private void SoundnessCheck(Dictionary<PureCollections.Tuple!, bool>! cache, Block! orig, List<Block!>! copies)

@@ -1134,7 +1324,7 @@ namespace VC
     #endregion

 

 

-    protected VCExpr! GenerateVC(Implementation! impl, out Hashtable/*<int, Absy!>*/! label2absy, Checker! ch)

+    protected VCExpr! GenerateVC(Implementation! impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*/! label2absy, Checker! ch)

     {

       TypecheckingContext tc = new TypecheckingContext(null);

       impl.Typecheck(tc);

@@ -1164,7 +1354,7 @@ namespace VC
         if (((!)CommandLineOptions.Clo.TheProverFactory).SupportsDags) {

           vc = DagVC((!)impl.Blocks[0], label2absy, new Hashtable/*<Block, VCExpr!>*/(), ch.TheoremProver.Context);

         } else {

-          vc = LetVC((!)impl.Blocks[0], label2absy, ch.TheoremProver.Context);

+          vc = LetVC((!)impl.Blocks[0], controlFlowVariable, label2absy, ch.TheoremProver.Context);

         }

         break;

       case CommandLineOptions.VCVariety.Doomed:

@@ -1182,7 +1372,6 @@ namespace VC
         Console.WriteLine("ignoring ill-formed {:{0} ...} attribute on {1}, parameter should be an int", name, impl.Name);

       }

     }

-

     

     public override Outcome VerifyImplementation(Implementation! impl, Program! program, VerifierCallback! callback)

       throws UnexpectedProverOutputException;

@@ -1360,20 +1549,31 @@ namespace VC
         }

       } 

       

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

+      DeclFreeProverContext! context;

+      Program! program;

+      

       public ErrorReporter(Hashtable/*TransferCmd->ReturnCmd*/! gotoCmdOrigins,

           Hashtable/*<int, Absy!>*/! label2absy,

           List<Block!>! blocks,

           Dictionary<Incarnation, Absy!>! incarnationOriginMap,

-          VerifierCallback! callback)

+          VerifierCallback! callback,

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

+          DeclFreeProverContext! context,

+          Program! program)

       {

         this.gotoCmdOrigins = gotoCmdOrigins;

         this.label2absy = label2absy;

         this.blocks = blocks;

         this.incarnationOriginMap = incarnationOriginMap;

         this.callback = callback;

+        

+        this.implName2LazyInliningInfo = implName2LazyInliningInfo;

+        this.context = context;

+        this.program = program;

         // base();

       }

-      

+

       public override void OnModel(IList<string!>! labels, ErrorModel errModel) {

         if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {

             errModel.Print(ErrorReporter.ModelWriter);

@@ -1381,7 +1581,7 @@ namespace VC
         }

         Hashtable traceNodes = new Hashtable();

         foreach (string! s in labels) {

-          Absy! absy =Label2Absy(s); 

+          Absy! absy = Label2Absy(s); 

           if (traceNodes.ContainsKey(absy))

             System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes");

           else

@@ -1393,7 +1593,7 @@ namespace VC
         assert traceNodes.Contains(entryBlock);

         trace.Add(entryBlock);

 

-        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap);

+        Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program);

 

         if (newCounterexample == null) return;

         

@@ -1437,9 +1637,12 @@ namespace VC
           Hashtable/*<int, Absy!>*/! label2absy,

           List<Block!>! blocks,

           Dictionary<Incarnation, Absy!>! incarnationOriginMap,

-          VerifierCallback! callback)

+          VerifierCallback! callback,

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

+          DeclFreeProverContext! context,

+          Program! program)

       {

-        base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback); // here for aesthetic purposes

+        base(gotoCmdOrigins, label2absy, blocks, incarnationOriginMap, callback, implName2LazyInliningInfo, context, program); // here for aesthetic purposes

       }

 

       public override void OnModel(IList<string!>! labels, ErrorModel errModel) {

@@ -1730,6 +1933,13 @@ namespace VC
       }

       #endregion

       

+      #region Support for lazy inlining

+      if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name))

+      {

+        exitBlock.Cmds.Add(new AssertCmd(Token.NoToken, Expr.False));

+      }

+      #endregion

+      

       #region Debug Tracing

       if (CommandLineOptions.Clo.TraceVerify) 

       {

@@ -1752,7 +1962,13 @@ namespace VC
         Microsoft.Boogie.LiveVariableAnalysis.ComputeLiveVariables(impl);

       }

       

-      Convert2PassiveCmd(impl);

+      Hashtable exitIncarnationMap = Convert2PassiveCmd(impl);

+      if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name))

+      {

+        LazyInliningInfo! info = implName2LazyInliningInfo[impl.Name];

+        info.exitIncarnationMap = exitIncarnationMap;

+        info.incarnationOriginMap = this.incarnationOriginMap;

+      }

       

       if (CommandLineOptions.Clo.LiveVariableAnalysis) {

         Microsoft.Boogie.LiveVariableAnalysis.ClearLiveVariables(impl);

@@ -1811,20 +2027,167 @@ namespace VC
       return gotoCmdOrigins;

     }

 

-    static Counterexample TraceCounterexample(Block! b, Hashtable! traceNodes, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap)

+    private static Counterexample! LazyCounterexample(

+                                       ErrorModel! errModel, 

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

+                                       DeclFreeProverContext! context, 

+                                       Program! program,

+                                       string! implName, List<int>! values)

+    { 

+      VCExprTranslator! vcExprTranslator = (!)context.exprTranslator;

+      Boogie2VCExprTranslator! boogieExprTranslator = context.BoogieExprTranslator;

+      LazyInliningInfo! info = implName2LazyInliningInfo[implName];

+      BlockSeq! trace = new BlockSeq();

+      Block! b = ((!) info.impl).Blocks[0];

+      trace.Add(b);

+      VCExprVar! cfcVar = boogieExprTranslator.LookupVariable(info.controlFlowVariable);

+      string! cfcName = vcExprTranslator.Lookup(cfcVar);

+      int cfcPartition = errModel.LookupSkolemFunctionAt(cfcName + "!" + info.uniqueId, values);

+      int cfcValue = errModel.LookupPartitionValue(cfcPartition);

+      

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

+      while (true) {

+        CmdSeq! cmds = b.Cmds;

+        TransferCmd! transferCmd = (!)b.TransferCmd;

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

+        {

+          Cmd! cmd = (!) cmds[i];

+          AssertCmd assertCmd = cmd as AssertCmd;  

+          if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)

+          {

+            Counterexample newCounterexample;

+            newCounterexample = AssertCmdToCounterexample(assertCmd, transferCmd, trace, errModel, (!)info.incarnationOriginMap);

+            newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

+            return newCounterexample;

+          }

+            

+          AssumeCmd assumeCmd = cmd as AssumeCmd;

+          if (assumeCmd == null) continue;

+          NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

+          if (naryExpr == null) continue;

+          string! calleeName = naryExpr.Fun.FunctionName;

+          if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;

+      

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

+          foreach (Expr! expr in naryExpr.Args)

+          {

+            LiteralExpr litExpr = expr as LiteralExpr;

+            if (litExpr != null) 

+            {

+              args.Add(errModel.valueToPartition[litExpr.Val]);

+              continue;

+            }

+          

+            IdentifierExpr idExpr = expr as IdentifierExpr;

+            assert idExpr != null;

+            Variable! var = (!)idExpr.Decl;

+            

+            int index = 0;

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

+            foreach (Variable! global in globalVars)

+            {

+              if (global == var) break;

+              index++;

+            }

+            if (index < globalVars.Count)

+            {

+              args.Add(values[index]);

+              continue;

+            }

+            

+            foreach (Variable! input in info.impl.InParams)

+            {

+              if (input == var) break;

+              index++;

+            }

+            if (index < globalVars.Count + info.impl.InParams.Length)

+            {

+              args.Add(values[index]);

+              continue;

+            }

+              

+            foreach (Variable! output in info.impl.OutParams)

+            {

+              if (output == var) break;

+              index++;

+            }

+            if (index < globalVars.Count + info.impl.InParams.Length + info.impl.OutParams.Length)

+            {

+              args.Add(values[index]);

+              continue;

+            }

+            

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

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

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

+            args.Add(partition);

+          }

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

+        }

+          

+        GotoCmd gotoCmd = transferCmd as GotoCmd;

+        if (gotoCmd == null) break;

+        int nextBlockId = errModel.LookupControlFlowFunctionAt(cfcValue, b.UniqueId);

+        b = (Block!) ((!)info.label2absy)[nextBlockId];

+        trace.Add(b);

+      }

+      assert false;

+    }

+        

+    static Counterexample TraceCounterexample(Block! b, BlockSeq! trace, ErrorModel errModel, Dictionary<Incarnation, Absy!>! incarnationOriginMap)

     {

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

+      

+      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 = new Dictionary<Absy!, Counterexample!>();

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

       CmdSeq! cmds = b.Cmds;

       TransferCmd! transferCmd = (!)b.TransferCmd;

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

       {

         Cmd! cmd = (!) cmds[i];

-        

+            

         // Skip if 'cmd' not contained in the trace or not an assert

-        if (!(cmd is AssertCmd) || !traceNodes.Contains(cmd))

-          continue;

-

-        return AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, incarnationOriginMap);

+        if (cmd is AssertCmd && traceNodes.Contains(cmd))

+        {

+          Counterexample! newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, incarnationOriginMap);

+          newCounterexample.AddCalleeCounterexample(calleeCounterexamples);

+          return newCounterexample;

+        }

+        

+        #region Counterexample generation for lazily inlined procedures

+        if (errModel == null) continue;

+        AssumeCmd assumeCmd = cmd as AssumeCmd;

+        if (assumeCmd == null) continue;

+        NAryExpr naryExpr = assumeCmd.Expr as NAryExpr;

+        if (naryExpr == null) continue;

+        string! calleeName = naryExpr.Fun.FunctionName;

+        if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;

+        VCExprTranslator! vcExprTranslator = (!)context.exprTranslator;

+        Boogie2VCExprTranslator! boogieExprTranslator = context.BoogieExprTranslator;  

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

+        foreach (Expr! expr in naryExpr.Args)

+        {

+          LiteralExpr litExpr = expr as LiteralExpr;

+          if (litExpr != null) 

+          {

+            args.Add(errModel.valueToPartition[litExpr.Val]);

+            continue;

+          }

+          

+          IdentifierExpr idExpr = expr as IdentifierExpr;

+          assert idExpr != null;

+          assert idExpr.Decl != null;

+          VCExprVar! var = boogieExprTranslator.LookupVariable(idExpr.Decl);

+          string! name = vcExprTranslator.Lookup(var);

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

+        }

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

+        #endregion

       }

       

       GotoCmd gotoCmd = transferCmd as GotoCmd;

@@ -1834,7 +2197,7 @@ namespace VC
         {

           if (traceNodes.Contains(bb)){

             trace.Add(bb);

-            return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap);

+            return TraceCounterexample(bb, traceNodes, trace, errModel, incarnationOriginMap, implName2LazyInliningInfo, context, program);

           }

         }

       }

@@ -2559,16 +2922,18 @@ namespace VC
 //    }

 

     static VCExpr! LetVC(Block! startBlock,

+                         Variable controlFlowVariable,

                          Hashtable/*<int, Absy!>*/! label2absy,

                          ProverContext! proverCtxt)

     {

       Hashtable/*<Block, LetVariable!>*/! blockVariables = new Hashtable/*<Block, LetVariable!!>*/();

       List<VCExprLetBinding!>! bindings = new List<VCExprLetBinding!>();

-      VCExpr startCorrect = LetVC(startBlock, label2absy, blockVariables, bindings, proverCtxt);

+      VCExpr startCorrect = LetVC(startBlock, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt);

       return proverCtxt.ExprGen.Let(bindings, startCorrect);

     }

 

     static VCExpr! LetVC(Block! block,

+                         Variable controlFlowVariable,

                          Hashtable/*<int, Absy!>*/! label2absy,

                          Hashtable/*<Block, VCExprVar!>*/! blockVariables,

                          List<VCExprLetBinding!>! bindings,

@@ -2591,13 +2956,20 @@ namespace VC
           assert gotocmd.labelTargets != null;

           List<VCExpr!> SuccCorrectVars = new List<VCExpr!>(gotocmd.labelTargets.Length);

           foreach (Block! successor in gotocmd.labelTargets) {

-            VCExpr s = LetVC(successor, label2absy, blockVariables, bindings, proverCtxt);

+            VCExpr s = LetVC(successor, controlFlowVariable, label2absy, blockVariables, bindings, proverCtxt);

+            if (controlFlowVariable != null) 

+            {

+              VCExprVar controlFlowVariableExpr = proverCtxt.BoogieExprTranslator.LookupVariable(controlFlowVariable);

+              VCExpr controlFlowFunctionAppl = gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(block.UniqueId)));

+              VCExpr controlTransferExpr = gen.Eq(controlFlowFunctionAppl, gen.Integer(BigNum.FromInt(successor.UniqueId)));

+              s = gen.Implies(controlTransferExpr, s);

+            }  

             SuccCorrectVars.Add(s);

           }

           SuccCorrect = gen.NAry(VCExpressionGenerator.AndOp, SuccCorrectVars);

         }

 

-        VCContext context = new VCContext(label2absy, proverCtxt);

+        VCContext context = new VCContext(label2absy, proverCtxt, controlFlowVariable);

         VCExpr vc = Wlp.Block(block, SuccCorrect, context);

         

         v = gen.Variable(block.Label + "_correct", Bpl.Type.Bool);

diff --git a/Source/VCGeneration/Wlp.ssc b/Source/VCGeneration/Wlp.ssc
index e70b332f..38aa6af8 100644
--- a/Source/VCGeneration/Wlp.ssc
+++ b/Source/VCGeneration/Wlp.ssc
@@ -8,12 +8,15 @@ using System.Collections;
 using Microsoft.Boogie;

 using Microsoft.Boogie.VCExprAST;

 using Microsoft.Contracts;

+using System.Collections.Generic;

+using Microsoft.Basetypes;

 

 namespace VC {

   public class VCContext 

   {

     [Rep] public readonly Hashtable/*<int, Absy!>*/! Label2absy;

     [Rep] public readonly ProverContext! Ctxt;

+    public readonly Variable ControlFlowVariable;

     

     public VCContext(Hashtable/*<int, Absy!>*/! label2absy, ProverContext! ctxt)

     {

@@ -21,6 +24,13 @@ namespace VC {
       this.Ctxt = ctxt;

       // base();

     }

+    

+    public VCContext(Hashtable/*<int, Absy!>*/! label2absy, ProverContext! ctxt, Variable controlFlowVariable)

+    {

+      this.Label2absy = label2absy;

+      this.Ctxt = ctxt;

+      this.ControlFlowVariable = controlFlowVariable;

+    }

   }

 

   #region A class to compute wlp of a passive command program

@@ -41,7 +51,10 @@ namespace VC {
       int id = b.UniqueId;

       expose (ctxt) {

         ctxt.Label2absy[id] = b;

-        return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res);

+        if (ctxt.ControlFlowVariable != null)

+          return res;

+        else 

+          return gen.Implies(gen.LabelPos((!)id.ToString(), VCExpressionGenerator.True), res);

       }

     }

 

@@ -73,11 +86,26 @@ namespace VC {
             default:

               assert false;  // unexpected case

           }

-// (MSchaef) Hack: This line might be useless, but at least it is not harmfull

-// need to test it

-        if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) return gen.Implies(C, N);

-      

-          return gen.AndSimp(gen.LabelNeg((!)id.ToString(), C), N);

+          

+          // (MSchaef) Hack: This line might be useless, but at least it is not harmfull

+          // need to test it

+          if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) 

+            return gen.Implies(C, N);

+          

+          if (ctxt.ControlFlowVariable != null)

+          {

+            VCExpr! controlFlowVariableExpr = 

+              ctxt.Ctxt.BoogieExprTranslator.LookupVariable(ctxt.ControlFlowVariable);

+            VCExpr! controlFlowFunctionAppl1 = 

+              gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

+            VCExpr! controlFlowFunctionAppl2 = 

+              gen.ControlFlowFunctionApplication(controlFlowVariableExpr, gen.Integer(BigNum.FromInt(id)));

+            VCExpr! assertFailure = gen.Eq(controlFlowFunctionAppl1, gen.Integer(BigNum.FromInt(0)));

+            VCExpr! assertSuccess = gen.Neq(controlFlowFunctionAppl2, gen.Integer(BigNum.FromInt(0)));

+            return gen.And(gen.Implies(assertFailure, C), gen.Implies(assertSuccess, N));

+          }

+          else

+            return gen.AndSimp(gen.LabelNeg((!)id.ToString(), C), N);

         }

 

       } else if (cmd is AssumeCmd) {