diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-05-01 19:46:44 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-05-01 19:46:44 -0700 |
| commit | c250cacedbdf5adbc286349a690f309a6b783d20 (patch) | |
| tree | 65ba1cc35cb029f633d44e074dab5319c2456178 /Source | |
| parent | eef04fec7b9bc9e40e7dda4b9876085220ae0c9f (diff) | |
added counterexample generation based on labels back to stratified inlining
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 1 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 233 |
2 files changed, 223 insertions, 11 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 2180efa7..f2148158 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -1265,7 +1265,6 @@ namespace Microsoft.Boogie { }
if (StratifiedInlining > 0) {
- UseLabels = false;
TypeEncodingMethod = TypeEncoding.Monomorphic;
UseArrayTheory = true;
UseAbstractInterpretation = false;
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<string> labels, Model model) {
- List<Absy> absyList = new List<Absy>();
- foreach (var label in labels) {
- absyList.Add(Label2Absy(label));
+ public void OnModelOld(IList<string/*!*/>/*!*/ labels, Model model) {
+ Contract.Assert(CommandLineOptions.Clo.StratifiedInliningWithoutModels || model != null);
+
+ candidatesToExpand = new List<int>();
+
+ 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<string/*!*/>/*!*/ 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<Tuple<int, int>>();
- candidatesToExpand = new List<int>();
+ 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<string/*!*/>/*!*/ 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<TraceLocation, CalleeCounterexampleInfo>();
+ Counterexample newCounterexample = GenerateTraceRec(labels, errModel, mvInfo, candidateId, entryBlock, traceNodes, trace, calleeCounterexamples);
+
+ return newCounterexample;
+ }
+
+ private Counterexample GenerateTraceRec(
+ IList<string/*!*/>/*!*/ labels, Model/*!*/ errModel, ModelViewInfo mvInfo,
+ int candidateId,
+ Block/*!*/ b, Hashtable/*!*/ traceNodes, BlockSeq/*!*/ trace,
+ Dictionary<TraceLocation/*!*/, CalleeCounterexampleInfo/*!*/>/*!*/ 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<int, int>(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<Model.Element>();
+ 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<int, int>(calleeId, StratifiedInliningErrorReporter.CALL));
+ calleeCounterexamples[new TraceLocation(trace.Length - 1, i)] =
+ new CalleeCounterexampleInfo(
+ cce.NonNull(GenerateTrace(labels, errModel, calleeId, implName2StratifiedInliningInfo[calleeName].impl)),
+ new List<Model.Element>());
+ orderedStateIds.Add(new Tuple<int, int>(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<string> labels, Model model) {
+ if (CommandLineOptions.Clo.UseLabels) {
+ OnModelOld(labels, model);
+ }
+ else {
+ List<Absy> absyList = new List<Absy>();
+ foreach (var label in labels) {
+ absyList.Add(Label2Absy(label));
+ }
+
+ orderedStateIds = new List<Tuple<int, int>>();
+ candidatesToExpand = new List<int>();
+
+ var cex = NewTrace(0, absyList, model);
+
+ if (underapproximationMode) {
+ GetModelWithStates(model);
+ callback.OnCounterexample(cex, null);
+ this.PrintModel(model);
+ }
}
}
|