From c250cacedbdf5adbc286349a690f309a6b783d20 Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 1 May 2012 19:46:44 -0700 Subject: added counterexample generation based on labels back to stratified inlining --- Source/VCGeneration/StratifiedVC.cs | 233 ++++++++++++++++++++++++++++++++++-- 1 file changed, 223 insertions(+), 10 deletions(-) (limited to 'Source/VCGeneration') diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 5a6e782d..edbba25a 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2596,21 +2596,234 @@ namespace VC return; } - public override void OnModel(IList labels, Model model) { - List absyList = new List(); - foreach (var label in labels) { - absyList.Add(Label2Absy(label)); + public void OnModelOld(IList/*!*/ labels, Model model) { + Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null); + + candidatesToExpand = new List(); + + if (underapproximationMode) { + var cex = GenerateTraceMain(labels, model, mvInfo); + Debug.Assert(candidatesToExpand.All(calls.isSkipped)); + if (cex != null) { + GetModelWithStates(model); + callback.OnCounterexample(cex, null); + this.PrintModel(model); + } + return; + } + + Contract.Assert(calls != null); + + GenerateTraceMain(labels, model, mvInfo); + } + + // Construct the interprocedural trace + private Counterexample GenerateTraceMain(IList/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo) { + Contract.Requires(cce.NonNullElements(labels)); + if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) { + errModel.Write(ErrorReporter.ModelWriter); + ErrorReporter.ModelWriter.Flush(); } orderedStateIds = new List>(); - candidatesToExpand = new List(); + Counterexample newCounterexample = + GenerateTrace(labels, errModel, 0, mainImpl); + + if (newCounterexample == null) + return null; + + #region Map passive program errors back to original program errors + ReturnCounterexample returnExample = newCounterexample as ReturnCounterexample; + if (returnExample != null && gotoCmdOrigins != null) { + foreach (Block b in returnExample.Trace) { + Contract.Assert(b != null); + Contract.Assume(b.TransferCmd != null); + ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd]; + if (cmd != null) { + returnExample.FailingReturn = cmd; + break; + } + } + } + #endregion - var cex = NewTrace(0, absyList, model); + return newCounterexample; + } - if (underapproximationMode) { - GetModelWithStates(model); - callback.OnCounterexample(cex, null); - this.PrintModel(model); + private Counterexample GenerateTrace(IList/*!*/ labels, Model/*!*/ errModel, + int candidateId, Implementation procImpl) { + Contract.Requires(cce.NonNullElements(labels)); + Contract.Requires(procImpl != null); + + Hashtable traceNodes = new Hashtable(); + //string procPrefix = "si_inline_" + candidateId.ToString() + "_"; + + //Console.WriteLine("GenerateTrace: {0}", procImpl.Name); + foreach (string s in labels) { + Contract.Assert(s != null); + var absylabel = calls.ParseRenamedAbsyLabel(s, candidateId); + + if (absylabel == null) continue; + + Absy absy; + + if (candidateId == 0) { + absy = Label2Absy(absylabel); + } + else { + absy = Label2Absy(procImpl.Name, absylabel); + } + + if (traceNodes.ContainsKey(absy)) + System.Console.WriteLine("Warning: duplicate label: " + s + " read while tracing nodes"); + else + traceNodes.Add(absy, null); + } + + BlockSeq trace = new BlockSeq(); + Block entryBlock = cce.NonNull(procImpl.Blocks[0]); + Contract.Assert(entryBlock != null); + Contract.Assert(traceNodes.Contains(entryBlock)); + trace.Add(entryBlock); + + var calleeCounterexamples = new Dictionary(); + Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples); + + return newCounterexample; + } + + private Counterexample GenerateTraceRec( + IList/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo, + int candidateId, + Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace, + Dictionary/*!*/ calleeCounterexamples) { + Contract.Requires(cce.NonNullElements(labels)); + Contract.Requires(b != null); + Contract.Requires(traceNodes != null); + Contract.Requires(trace != null); + Contract.Requires(cce.NonNullDictionaryAndValues(calleeCounterexamples)); + // After translation, all potential errors come from asserts. + while (true) { + CmdSeq cmds = b.Cmds; + TransferCmd transferCmd = cce.NonNull(b.TransferCmd); + for (int i = 0; i < cmds.Length; i++) { + Cmd cmd = cce.NonNull(cmds[i]); + + // Skip if 'cmd' not contained in the trace or not an assert + if (cmd is AssertCmd && traceNodes.Contains(cmd)) { + Counterexample newCounterexample = AssertCmdToCounterexample((AssertCmd)cmd, transferCmd, trace, errModel, mvInfo, context); + newCounterexample.AddCalleeCounterexample(calleeCounterexamples); + return newCounterexample; + } + + // Counterexample generation for inlined procedures + AssumeCmd assumeCmd = cmd as AssumeCmd; + if (assumeCmd == null) + continue; + NAryExpr naryExpr = assumeCmd.Expr as NAryExpr; + if (naryExpr == null) + continue; + string calleeName = naryExpr.Fun.FunctionName; + Contract.Assert(calleeName != null); + + BinaryOperator binOp = naryExpr.Fun as BinaryOperator; + if (binOp != null && binOp.Op == BinaryOperator.Opcode.And) { + Expr expr = naryExpr.Args[0]; + NAryExpr mvStateExpr = expr as NAryExpr; + if (mvStateExpr != null && mvStateExpr.Fun.FunctionName == ModelViewInfo.MVState_FunctionDef.Name) { + LiteralExpr x = mvStateExpr.Args[1] as LiteralExpr; + orderedStateIds.Add(new Tuple(candidateId, x.asBigNum.ToInt)); + } + } + + if (calleeName.StartsWith(recordProcName) && errModel != null) { + 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.MkElement((expr as VCExprIntLit).Val.ToString())); + } + else if (expr == VCExpressionGenerator.True) { + args.Add(errModel.MkElement("true")); + } + else if (expr == VCExpressionGenerator.False) { + args.Add(errModel.MkElement("false")); + } + else if (expr is VCExprVar) { + var idExpr = expr as VCExprVar; + string name = context.Lookup(idExpr); + Contract.Assert(name != null); + Model.Func f = errModel.TryGetFunc(name); + if (f != null) { + args.Add(f.GetConstant()); + } + } + else { + Contract.Assert(false); + } + calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = + new CalleeCounterexampleInfo(null, args); + continue; + } + + if (!implName2StratifiedInliningInfo.ContainsKey(calleeName)) + continue; + + Contract.Assert(calls != null); + + int calleeId = calls.boogieExpr2Id[new BoogieCallExpr(naryExpr, candidateId)]; + + if (calls.currCandidates.Contains(calleeId)) { + candidatesToExpand.Add(calleeId); + } + else { + orderedStateIds.Add(new Tuple(calleeId, StratifiedInliningErrorReporter.CALL)); + calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] = + new CalleeCounterexampleInfo( + cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)), + new List()); + orderedStateIds.Add(new Tuple(candidateId, StratifiedInliningErrorReporter.RETURN)); + } + } + + GotoCmd gotoCmd = transferCmd as GotoCmd; + if (gotoCmd != null) { + b = null; + foreach (Block bb in cce.NonNull(gotoCmd.labelTargets)) { + Contract.Assert(bb != null); + if (traceNodes.Contains(bb)) { + trace.Add(bb); + b = bb; + break; + } + } + if (b != null) continue; + } + return null; + } + } + + public override void OnModel(IList labels, Model model) { + if (CommandLineOptions.Clo.UseLabels) { + OnModelOld(labels, model); + } + else { + List absyList = new List(); + foreach (var label in labels) { + absyList.Add(Label2Absy(label)); + } + + orderedStateIds = new List>(); + candidatesToExpand = new List(); + + var cex = NewTrace(0, absyList, model); + + if (underapproximationMode) { + GetModelWithStates(model); + callback.OnCounterexample(cex, null); + this.PrintModel(model); + } } } -- cgit v1.2.3