diff options
Diffstat (limited to 'Source/VCGeneration')
| -rw-r--r-- | Source/VCGeneration/Check.ssc | 64 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.ssc | 85 | ||||
| -rw-r--r-- | Source/VCGeneration/Context.ssc | 3 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.ssc | 432 | ||||
| -rw-r--r-- | Source/VCGeneration/Wlp.ssc | 40 |
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) {
|