From df0fd34ecd8e381083e6c0839dbbb9944803a28c Mon Sep 17 00:00:00 2001 From: akashlal Date: Thu, 17 Mar 2011 21:55:38 +0000 Subject: Print out requested values in the counterexample trace --- Source/VCGeneration/ConditionGeneration.cs | 12 ++-- Source/VCGeneration/StratifiedVC.cs | 106 ++++++++++++++++++++--------- 2 files changed, 79 insertions(+), 39 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 6400aaf2..02af08ad 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -168,16 +168,18 @@ namespace Microsoft.Boogie { { var cmd = getTraceCmd(loc); var calleeName = getCalledProcName(cmd); - if (calleeName == "boogie_si_record_int" && CommandLineOptions.Clo.StratifiedInlining > 0) + if (calleeName == VC.StratifiedVCGen.recordArgProcName && 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", calleeName, ind); - + else + { + 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", calleeName, ind); + } } } } diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 48029154..f847638a 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -22,6 +22,8 @@ namespace VC private Dictionary implName2StratifiedInliningInfo; public bool PersistCallTree; public static Dictionary callTree = null; + public readonly static string recordArgProcName = "boogie_si_record_int"; + private Function recordArgFunc; [ContractInvariantMethod] void ObjectInvariant() @@ -38,6 +40,7 @@ namespace VC { Contract.Requires(program != null); implName2StratifiedInliningInfo = new Dictionary(); + recordArgFunc = null; this.GenerateVCsForStratifiedInlining(program); PersistCallTree = false; } @@ -82,6 +85,8 @@ namespace VC Implementation impl = decl as Implementation; if (impl == null) continue; + Contract.Assert(impl.Name != recordArgProcName, "Not allowed to have an implementation for this guy"); + Procedure proc = cce.NonNull(impl.Proc); if (proc.FindExprAttribute("inline") != null) { @@ -117,6 +122,32 @@ namespace VC } } + foreach (var decl in program.TopLevelDeclarations) + { + var proc = decl as Procedure; + if (proc == null) continue; + if (proc.Name != recordArgProcName) continue; + Contract.Assert(proc.InParams.Length == 1); + + // Make a new function + TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool); + Contract.Assert(ti != null); + Formal returnVar = new Formal(Token.NoToken, ti, false); + Contract.Assert(returnVar != null); + + var ins = new VariableSeq(); + ins.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "x", Bpl.Type.Int), true)); + + recordArgFunc = new Function(Token.NoToken, proc.Name, ins, returnVar); + checker.TheoremProver.Context.DeclareFunction(recordArgFunc, ""); + + var exprs = new ExprSeq(); + exprs.Add(new IdentifierExpr(Token.NoToken, proc.InParams[0])); + + Expr freePostExpr = new NAryExpr(Token.NoToken, new FunctionCall(recordArgFunc), exprs); + proc.Ensures.Add(new Ensures(true, freePostExpr)); + break; + } } private void GenerateVCForStratifiedInlining(Program program, StratifiedInliningInfo info, Checker checker) @@ -1440,11 +1471,6 @@ 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()); SubstitutingVCExprVisitor subst = new SubstitutingVCExprVisitor(checker.VCExprGen); @@ -1525,11 +1551,6 @@ 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()); @@ -1645,6 +1666,7 @@ namespace VC Dictionary/*!*/ implName2StratifiedInliningInfo; public readonly Hashtable/**//*!*/ mainLabel2absy; public Dictionary/*!*/ boogieExpr2Id; + public Dictionary/*!*/ recordExpr2Var; public Dictionary/*!*/ id2Candidate; public Dictionary/*!*/ id2ControlVar; public Dictionary/*!*/ label2Id; @@ -1720,6 +1742,7 @@ namespace VC persistentNameInv["0"] = 0; recentlyAddedCandidates = new HashSet(); argExprMap = new Dictionary(); + recordExpr2Var = new Dictionary(); forcedCandidates = new HashSet(); } @@ -1995,6 +2018,13 @@ namespace VC //return Gen.LabelPos(label, callExpr); return Gen.LabelPos(label, id2ControlVar[candidateId]); } + else if (calleeName == recordArgProcName) + { + Debug.Assert(callExpr.Length == 1); + Debug.Assert(callExpr[0] != null); + recordExpr2Var[new BoogieCallExpr(naryExpr, currInlineCount)] = callExpr[0]; + return callExpr; + } else { return callExpr; @@ -2295,6 +2325,37 @@ namespace VC continue; string calleeName = naryExpr.Fun.FunctionName; Contract.Assert(calleeName != null); + + if (calleeName == recordArgProcName) + { + var expr = calls.recordExpr2Var[new BoogieCallExpr(naryExpr, candidateId)]; + + // Record concrete value of the argument to this procedure + var args = new List(); + 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); + if (errModel.identifierToPartition.ContainsKey(name)) + { + args.Add(errModel.identifierToPartition[name]); + } + } + else + { + Contract.Assert(false); + } + var values = errModel.PartitionsToValues(args); + calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = + new CalleeCounterexampleInfo(null, values); + continue; + } + if (!implName2StratifiedInliningInfo.ContainsKey(calleeName)) continue; @@ -2306,34 +2367,11 @@ namespace VC } else { - var values = new List(); - if (calleeName == "boogie_si_record_int") - { - // Record concrete value of the argument to this procedure - var args = new List(); - 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)), - values); + null); } } -- cgit v1.2.3