diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 8 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 14 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 8 | ||||
| -rw-r--r-- | Source/VCGeneration/Check.cs | 428 | ||||
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 6 | ||||
| -rw-r--r-- | Source/VCGeneration/DoomErrorHandler.cs | 3 | ||||
| -rw-r--r-- | Source/VCGeneration/StratifiedVC.cs | 7 | ||||
| -rw-r--r-- | Source/VCGeneration/VC.cs | 504 |
8 files changed, 32 insertions, 946 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 48791385..c65406b4 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -428,8 +428,8 @@ namespace Microsoft.Boogie.SMTLib labels = CalculatePath(0);
xlabels = labels;
}
- ErrorModel errorModel = GetErrorModel();
- handler.OnModel(xlabels, errorModel);
+ Model model = GetErrorModel();
+ handler.OnModel(xlabels, model);
}
if (labels == null || errorsLeft == 0) break;
@@ -489,7 +489,7 @@ namespace Microsoft.Boogie.SMTLib return path.ToArray();
}
- private ErrorModel GetErrorModel() {
+ private Model GetErrorModel() {
if (!options.ExpectingModel())
return null;
SendThisVC("(get-model)");
@@ -528,7 +528,7 @@ namespace Microsoft.Boogie.SMTLib else
theModel = models[0];
}
- return new ErrorModel(theModel);
+ return theModel;
}
private string[] GetLabelsInfo()
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index f0aa3906..e0fddc63 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -261,7 +261,7 @@ namespace Microsoft.Boogie.Z3 { sw.WriteLine("*** END_MODEL");
var sr = new StringReader(sw.ToString());
var models = Microsoft.Boogie.Model.ParseModels(sr);
- Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
boogieErrors.Add(e);
if (boogieErrors.Count < this.counterexamples) {
@@ -332,7 +332,7 @@ namespace Microsoft.Boogie.Z3 { sw.WriteLine("*** END_MODEL");
var sr = new StringReader(sw.ToString());
var models = Microsoft.Boogie.Model.ParseModels(sr);
- Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List<string>(labelStrings));
+ Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
boogieErrors.Add(e);
labels.Dispose();
@@ -442,16 +442,16 @@ namespace Microsoft.Boogie.Z3 { }
public class Z3ErrorModelAndLabels {
- private ErrorModel _errorModel;
+ private Model _model;
private List<string> _relevantLabels;
- public ErrorModel ErrorModel {
- get { return this._errorModel; }
+ public Model Model {
+ get { return this._model; }
}
public List<string> RelevantLabels {
get { return this._relevantLabels; }
}
- public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels) {
- this._errorModel = errorModel;
+ public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) {
+ this._model = model;
this._relevantLabels = relevantLabels;
}
}
diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 3b7b8f43..d72705f3 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -230,10 +230,10 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. outcome = context.Check(out z3LabelModels);
}
- public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
+ public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- outcome = context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
+ return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
}
public override void Push()
@@ -285,7 +285,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
{
List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
- handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
+ handler.OnModel(unprefixedLabels, z3LabelModel.Model);
}
}
return outcome;
@@ -295,7 +295,7 @@ REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. if (outcome == Outcome.Invalid) {
foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {
List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
- handler.OnModel(unprefixedLabels, z3LabelModel.ErrorModel);
+ handler.OnModel(unprefixedLabels, z3LabelModel.Model);
}
}
return outcome;
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index 9ebf4d63..9babf16c 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -299,432 +299,6 @@ namespace Microsoft.Boogie { // -----------------------------------------------------------------------------------------------
// -----------------------------------------------------------------------------------------------
- // This class will go away soon. Use Model class instead.
- public class ErrorModel {
- public Dictionary<string/*!*/, int>/*!*/ identifierToPartition;
- public List<List<string/*!>>!*/>> partitionToIdentifiers;
- public List<Object>/*!*/ partitionToValue;
- public Dictionary<object, int>/*!*/ valueToPartition;
- public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;
- public Model comesFrom;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(identifierToPartition != null);
- Contract.Invariant(partitionToIdentifiers != null);
- Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
- Contract.Invariant(partitionToValue != null);
- Contract.Invariant(valueToPartition != null);
- Contract.Invariant(cce.NonNullDictionaryAndValues(definedFunctions));
- }
-
-
- public ErrorModel(Dictionary<string, int> identifierToPartition, List<List<string>> partitionToIdentifiers, List<Object> partitionToValue, Dictionary<object, int> valueToPartition, Dictionary<string, List<List<int>>> definedFunctions) {
- Contract.Requires(identifierToPartition != null);
- Contract.Requires(partitionToIdentifiers != null);
- Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i)));
- Contract.Requires(partitionToValue != null);
- Contract.Requires(valueToPartition != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(definedFunctions));
- this.identifierToPartition = identifierToPartition;
- this.partitionToIdentifiers = partitionToIdentifiers;
- this.partitionToValue = partitionToValue;
- this.valueToPartition = valueToPartition;
- this.definedFunctions = definedFunctions;
- }
-
- public ErrorModel(Model m)
- {
- // this.comesFrom = m;
-
- this.identifierToPartition = new Dictionary<string, int>();
- this.partitionToValue = new List<object>();
- this.partitionToIdentifiers = new List<List<string>>();
- this.valueToPartition = new Dictionary<object, int>();
- this.definedFunctions = new Dictionary<string, List<List<int>>>();
-
- var elseElt = m.MkElement("*#unspecified");
-
- foreach (var e in m.Elements) {
- Contract.Assert(e.Id == this.partitionToValue.Count);
- object val;
- switch (e.Kind) {
- case Model.ElementKind.Uninterpreted:
- val = null;
- break;
- case Model.ElementKind.Integer:
- val = BigNum.FromString(((Model.Integer)e).Numeral);
- break;
- case Model.ElementKind.BitVector:
- val = new BvConst(BigNum.FromString(((Model.BitVector)e).Numeral), ((Model.BitVector)e).Size);
- break;
- case Model.ElementKind.Boolean:
- val = ((Model.Boolean)e).Value;
- break;
- case Model.ElementKind.Array:
- val = null;
- break;
- case Model.ElementKind.DataValue:
- val = null;
- break;
- default:
- Contract.Assert(false);
- val = null;
- break;
- }
- this.partitionToValue.Add(val);
- if (val != null)
- this.valueToPartition[val] = e.Id;
-
- var names = new List<string>();
- this.partitionToIdentifiers.Add(names);
- foreach (var app in e.Names) {
- if (app.Func.Arity == 0) {
- names.Add(app.Func.Name);
- this.identifierToPartition[app.Func.Name] = e.Id;
- }
- }
- }
-
- foreach (var f in m.Functions) {
- if (f.Arity > 0) {
- var tuples = new List<List<int>>();
- this.definedFunctions[f.Name] = tuples;
- foreach (var app in f.Apps) {
- var tpl = new List<int>(f.Arity + 1);
- foreach (var a in app.Args) tpl.Add(a.Id);
- tpl.Add(app.Result.Id);
- tuples.Add(tpl);
- }
- var elseTpl = new List<int>();
- if (f.Else != null)
- elseTpl.Add(f.Else.Id);
- else
- elseTpl.Add(elseElt.Id);
- tuples.Add(elseTpl);
- }
- }
-
- foreach (var e in m.Elements) {
- var arr = e as Model.Array;
- if (arr != null) {
- var tuples = this.definedFunctions[arr.Value.Name];
- this.partitionToValue[arr.Id] = tuples;
- this.valueToPartition[tuples] = arr.Id;
- }
- }
- }
-
- public Model ToModel()
- {
- if (comesFrom != null)
- return comesFrom;
-
- Model m = new Model();
- // create an Element for every partition
- Model.Element[] elts = new Model.Element[partitionToValue.Count];
- var asArrayIdx = 0;
- for (int i = 0; i < partitionToValue.Count; ++i) {
- var v = partitionToValue[i];
- if (v == null)
- elts[i] = m.MkElement(string.Format("*{0}", i));
- else {
- var ll = v as List<List<int>>;
- if (ll != null) {
- var arrName = "boogie-array#" + asArrayIdx++;
- this.definedFunctions[arrName] = ll;
- elts[i] = m.MkElement("as-array[" + arrName + "]");
- }
- else
- elts[i] = m.MkElement(v.ToString());
- }
-
- foreach (var id in partitionToIdentifiers[i]) {
- var f = m.MkFunc(id, 0);
- f.SetConstant(elts[i]);
- }
- }
- // compute and apply redirections
- foreach (var pr in Redirections(definedFunctions)) {
- elts[pr.Key] = elts[pr.Value];
- }
-
- // create functions
- var selectFunctions = new Dictionary<int, Model.Func>();
- var storeFunctions = new Dictionary<int, Model.Func>();
- foreach (var t in definedFunctions) {
- var tuples = t.Value;
- if (tuples.Count == 0) continue;
-
- // get the Func ("it doesn't matter if you get the funk, just as long as the funk gets you", from Ulco Bed's "Get The Funk" on Candy Dulfer's 1990 album Saxuality)
- var name = t.Key;
- var arity = tuples[0].Count - 1;
-
- // this may happen if the function only has the else clause; the 1 is just the best guess in such case
- if (arity == 0)
- arity = 1;
-
- Model.Func f;
- if (Regex.IsMatch(name, "^MapType[0-9]*Select$")) {
- name = string.Format("[{0}]", arity);
- if (!selectFunctions.TryGetValue(arity, out f)) {
- f = m.MkFunc(name, arity);
- selectFunctions.Add(arity, f);
- }
- } else if (Regex.IsMatch(name, "^MapType[0-9]*Store$")) {
- name = string.Format("[{0}:=]", arity);
- if (!storeFunctions.TryGetValue(arity, out f)) {
- f = m.MkFunc(name, arity);
- storeFunctions.Add(arity, f);
- }
- } else {
- f = m.MkFunc(name, arity);
- }
-
- var args = new Model.Element[arity];
- foreach (var l in tuples) {
- if (l.Count == 1) {
- if (f.Else == null)
- f.Else = elts[l[0]];
- } else {
- for (int i = 0; i < f.Arity; ++i)
- args[i] = elts[l[i]];
- f.AddApp(elts[l[f.Arity]], args);
- }
- }
- }
-
- return m;
- }
-
- IEnumerable<KeyValuePair<int,int>> Redirections(Dictionary<string, List<List<int>>> functions) {
- List<List<int>> fn;
- if (functions.TryGetValue("U_2_bool", out fn)) {
- foreach (var tpl in fn) {
- if (tpl.Count == 2) // the last tuple (the default value) has length 1
- yield return new KeyValuePair<int,int>(tpl[0], tpl[1]);
- }
- }
- if (functions.TryGetValue("U_2_int", out fn)) {
- foreach (var tpl in fn) {
- if (tpl.Count == 2) // the last tuple (the default value) has length 1
- yield return new KeyValuePair<int,int>(tpl[0], tpl[1]);
- }
- }
- }
-
- public virtual void Print(TextWriter writer)
- {
- Contract.Requires(writer != null);
-
- writer.WriteLine("Z3 error model: ");
-
- writer.WriteLine("partitions:");
- Contract.Assert(partitionToIdentifiers.Count == partitionToValue.Count);
- for (int i = 0; i < partitionToIdentifiers.Count; i++) {
- writer.Write("*" + i);
- List<string> pti = partitionToIdentifiers[i];
- if (pti != null && pti.Count != 0) {
- writer.Write(" {");
- for (int k = 0; k < pti.Count - 1; k++) {
- writer.Write(pti[k] + " ");
- }
- //extra work to make sure no " " is at the end of the list of identifiers
- if (pti.Count != 0) {
- writer.Write(pti[pti.Count - 1]);
- }
- writer.Write("}");
- }
- // temp object needed for non-null checking
- object tempPTVI = partitionToValue[i];
- if (tempPTVI != null) {
- if (tempPTVI.ToString() == "True") {
- writer.Write(" -> " + "true" + "");
- } else if (tempPTVI.ToString() == "False") {
- writer.Write(" -> " + "false" + "");
- } else if (tempPTVI is BigNum) {
- writer.Write(" -> " + tempPTVI + ":int");
- } else if (tempPTVI is List<List<int>>) {
- List<List<int>> array = tempPTVI as List<List<int>>;
- Contract.Assume(array != null);
- writer.Write(" -> {");
- foreach (List<int> l in array) {
- if (l.Count == 2) {
- writer.Write("*" + l[0] + " -> " + "*" + l[1] + "; ");
- } else {
- Contract.Assert((l.Count == 1));
- writer.Write("else -> *" + l[0] + "}");
- }
- }
- } else {
- writer.Write(" -> " + tempPTVI + "");
- }
- } else {
- writer.Write(" ");
- }
- writer.WriteLine();
- }
-
- writer.WriteLine("function interpretations:");
- foreach (KeyValuePair<string, List<List<int>>> kvp in definedFunctions) {
- Contract.Assert(kvp.Key != null);
- writer.WriteLine(kvp.Key + " -> {");
- List<List<int>> kvpValue = kvp.Value;
- if (kvpValue != null) {
- foreach (List<int> l in kvpValue) {
- writer.Write(" ");
- if (l != null) {
- for (int i = 0; i < l.Count - 1; i++) {
- writer.Write("*" + l[i] + " ");
- }
- if (l.Count == 1) {
- writer.WriteLine("else -> #unspecified");
- } else {
- writer.WriteLine("-> " + "*" + l[l.Count - 1]);
- }
- }
- }
- }
- writer.WriteLine("}");
- }
- writer.WriteLine("END_OF_MODEL");
- writer.WriteLine(".");
-
- if (CommandLineOptions.Clo.PrintErrorModel >= 2) {
- writer.WriteLine("identifierToPartition:");
- foreach (KeyValuePair<string, int> kvp in identifierToPartition) {
- Contract.Assert(kvp.Key != null);
- writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
- }
-
- writer.WriteLine("valueToPartition:");
- foreach (KeyValuePair<object, int> kvp in valueToPartition) {
- writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value);
- }
- writer.WriteLine("End of model.");
- }
- }
-
-
-
- public int LookupPartitionValue(int partition) {
- BigNum bignum = (BigNum)cce.NonNull(partitionToValue[partition]);
- return bignum.ToInt;
- }
-
- public int LookupControlFlowFunctionAt(int cfc, int id) {
- List<List<int>> tuples = this.definedFunctions["ControlFlow"];
- Contract.Assert(tuples != null);
- 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]);
- }
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
-
- private string LookupSkolemConstant(string name) {
- Contract.Requires(name != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- foreach (string functionName in identifierToPartition.Keys) {
- Contract.Assert(functionName != null);
-
- int index = functionName.LastIndexOf("!");
- if (index == -1)
- continue;
- string newFunctionName = cce.NonNull(functionName.Remove(index));
- if (newFunctionName.Equals(name))
- return functionName;
- }
- return "";
- }
- private string LookupSkolemFunction(string name) {
- Contract.Requires(name != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- foreach (string functionName in definedFunctions.Keys) {
- Contract.Assert(functionName != null);
- int index = functionName.LastIndexOf("!");
- if (index == -1)
- continue;
- string newFunctionName = cce.NonNull(functionName.Remove(index));
- if (newFunctionName.Equals(name))
- return functionName;
- }
- return "";
- }
- public int LookupSkolemFunctionAt(string functionName, List<int> values) {
- Contract.Requires(functionName != null);
- Contract.Requires(values != null);
-
- string actualFunctionName = LookupSkolemFunction(functionName);
- Contract.Assert(actualFunctionName != null);
- if (actualFunctionName.Equals("")) {
- // The skolem function is actually a skolem constant
- actualFunctionName = LookupSkolemConstant(functionName);
- Contract.Assert(!actualFunctionName.Equals(""));
- return identifierToPartition[actualFunctionName];
- }
- List<List<int>> tuples = this.definedFunctions[actualFunctionName];
- Contract.Assert(tuples.Count > 0);
- // the last tuple is a dummy tuple
- for (int n = 0; n < tuples.Count - 1; n++) {
- List<int> tuple = cce.NonNull(tuples[n]);
- Contract.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];
- }
- }
- }
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
-
- public List<object>/*!>!*/ PartitionsToValues(List<int> args) {
- Contract.Requires(args != null);
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<object>>()));
-
- List<object> vals = new List<object>();
- foreach (int i in args) {
- object o = partitionToValue[i];
- if (o == null) {
- // uninterpreted value
- vals.Add(string.Format("UI({0})", i.ToString()));
- } else if (o is bool) {
- vals.Add(o);
- } else if (o is BigNum) {
- vals.Add(o);
- } else if (o is List<List<int>>) {
- List<List<int>> array = (List<List<int>>)o;
- List<List<object>> arrayVal = new List<List<object>>();
- foreach (List<int> tuple in array) {
- Contract.Assert(tuple != null);
-
- List<object> tupleVal = new List<object>();
- foreach (int j in tuple) {
- tupleVal.Add(cce.NonNull(partitionToValue[j]));
- }
- arrayVal.Add(tupleVal);
- }
- vals.Add(arrayVal);
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
- return vals;
- }
- }
-
public abstract class ProverInterface {
public enum Outcome {
Valid,
@@ -734,7 +308,7 @@ namespace Microsoft.Boogie { Undetermined
}
public class ErrorHandler {
- public virtual void OnModel(IList<string> labels, ErrorModel errModel) {
+ public virtual void OnModel(IList<string> labels, Model model) {
Contract.Requires(cce.NonNullElements(labels));
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index bdbdd0f2..cc81be5b 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -493,7 +493,7 @@ namespace VC { protected string/*?*/ logFilePath;
protected bool appendLogFile;
- public static List<ErrorModel> errorModelList;
+ public static List<Model> errorModelList;
public ConditionGeneration(Program p) {
Contract.Requires(p != null);
@@ -535,14 +535,14 @@ namespace VC { /// each counterexample consisting of an array of labels.
/// </summary>
/// <param name="impl"></param>
- public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<ErrorModel> errorsModel)
+ public Outcome VerifyImplementation(Implementation impl, Program program, out List<Counterexample> errors, out List<Model> errorsModel)
{
Contract.Ensures(Contract.Result<Outcome>() != Outcome.Errors || Contract.ValueAtReturn(out errors) != null);
Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
List<Counterexample> errorsOut;
Outcome outcome;
- errorModelList = new List<ErrorModel>();
+ errorModelList = new List<Model>();
outcome = VerifyImplementation(impl, program, out errorsOut);
errors = errorsOut;
errorsModel = errorModelList;
diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs index 76893b8c..b0821240 100644 --- a/Source/VCGeneration/DoomErrorHandler.cs +++ b/Source/VCGeneration/DoomErrorHandler.cs @@ -63,7 +63,7 @@ namespace VC }
}
- public override void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel)
+ public override void OnModel(IList<string>/*!>!*/ labels, Model model)
{
// TODO: it would be better to check which reachability variables are actually set to one!
List<Block> traceNodes = new List<Block>();
@@ -80,7 +80,6 @@ namespace VC }
}
m_CurrentTrace.AddRange(traceNodes);
-
}
}
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 18ff4c87..7e04e172 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2714,7 +2714,7 @@ namespace VC public class EmptyErrorHandler : ProverInterface.ErrorHandler
{
- public override void OnModel(IList<string> labels, ErrorModel errModel)
+ public override void OnModel(IList<string> labels, Model model)
{
}
@@ -2898,7 +2898,7 @@ namespace VC return;
}
- public override void OnModel(IList<string> labels, ErrorModel errModel) {
+ public override void OnModel(IList<string> labels, Model model) {
List<Absy> absyList = new List<Absy>();
foreach (var label in labels) {
absyList.Add(Label2Absy(label));
@@ -2907,9 +2907,6 @@ namespace VC orderedStateIds = new List<Tuple<int, int>>();
candidatesToExpand = new List<int>();
- Model model = null;
- if (errModel != null) model = errModel.ToModel();
-
if (underapproximationMode) {
var cex = NewTrace(0, absyList, model);
Debug.Assert(candidatesToExpand.Count == 0);
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 567a5936..4ad6f182 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1624,14 +1624,15 @@ namespace VC { this.program = program;
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
//Contract.Requires(cce.NonNullElements(labels));
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
if (VC.ConditionGeneration.errorModelList != null)
{
- VC.ConditionGeneration.errorModelList.Add(errModel);
+ VC.ConditionGeneration.errorModelList.Add(model);
}
- errModel.Print(ErrorReporter.ModelWriter);
+
+ model.Write(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
@@ -1651,7 +1652,7 @@ namespace VC { Contract.Assert(traceNodes.Contains(entryBlock));
trace.Add(entryBlock);
- Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, errModel == null ? null : errModel.ToModel(), MvInfo, incarnationOriginMap, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());
+ Counterexample newCounterexample = TraceCounterexample(entryBlock, traceNodes, trace, model, MvInfo, incarnationOriginMap, context, program, new Dictionary<TraceLocation, CalleeCounterexampleInfo>());
if (newCounterexample == null)
return;
@@ -1712,13 +1713,13 @@ namespace VC { Contract.Requires(program != null);
}
- public override void OnModel(IList<string/*!*/>/*!*/ labels, ErrorModel errModel) {
+ public override void OnModel(IList<string/*!*/>/*!*/ labels, Model model) {
//Contract.Requires(cce.NonNullElements(labels));
// We ignore the error model here for enhanced error message purposes.
// It is only printed to the command line.
- if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) {
+ if (CommandLineOptions.Clo.PrintErrorModel >= 1 && model != null) {
if (CommandLineOptions.Clo.PrintErrorModelFile != null) {
- errModel.Print(ErrorReporter.ModelWriter);
+ model.Write(ErrorReporter.ModelWriter);
ErrorReporter.ModelWriter.Flush();
}
}
@@ -1744,7 +1745,7 @@ namespace VC { if (b.Cmds.Has(a)) {
BlockSeq trace = new BlockSeq();
trace.Add(b);
- Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, errModel == null ? null : errModel.ToModel(), MvInfo, context);
+ Counterexample newCounterexample = AssertCmdToCounterexample(a, cce.NonNull(b.TransferCmd), trace, model, MvInfo, context);
callback.OnCounterexample(newCounterexample, null);
goto NEXT_ASSERT;
}
@@ -2369,490 +2370,6 @@ namespace VC { return null;
}
-
- static void /*return printable error!*/ ApplyEnhancedErrorPrintingStrategy(Bpl.Expr/*!*/ expr, Hashtable /*Variable -> Expr*//*!*/ incarnationMap,
- MiningStrategy errorDataEnhanced, ErrorModel/*!*/ errModel, Dictionary<Expr/*!*/, object>/*!*/ exprToPrintableValue,
- List<string/*!*/>/*!*/ relatedInformation, bool printInternalStateDumpOnce, Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap) {
- Contract.Requires(expr != null);
- Contract.Requires(incarnationMap != null);
- Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(exprToPrintableValue));
- Contract.Requires(cce.NonNullElements(relatedInformation));
- Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
- if (errorDataEnhanced is ListOfMiningStrategies) {
- ListOfMiningStrategies loms = (ListOfMiningStrategies)errorDataEnhanced;
- List < MiningStrategy > l = loms.msList;
- for (int i = 0; i < l.Count; i++) {
- MiningStrategy ms = l[i];
- if (ms != null) {
- ApplyEnhancedErrorPrintingStrategy(expr, incarnationMap, l[i], errModel, exprToPrintableValue, relatedInformation, false, incarnationOriginMap);
- }
- }
- } else if (errorDataEnhanced is EEDTemplate /*EDEverySubExpr*/) {
- EEDTemplate eedT = (EEDTemplate)errorDataEnhanced;
- string reason = eedT.reason;
- List<Bpl.Expr> listOfExprs = eedT.exprList;
- Contract.Assert(cce.NonNullElements(listOfExprs));
- if (listOfExprs != null) {
- List<string> holeFillers = new List<string>();
- for (int i = 0; i < listOfExprs.Count; i++) {
- bool alreadySet = false;
- foreach (KeyValuePair<Bpl.Expr, object> kvp in exprToPrintableValue) {
- Contract.Assert(kvp.Key != null);
- Bpl.Expr e = kvp.Key;
- Bpl.Expr f = listOfExprs[i];
- // the strings are compared instead of the actual expressions because
- // the expressions might not be identical, but their print-out strings will be
- if (e.ToString() == f.ToString()) {
- object o = kvp.Value;
- if (o != null) {
- holeFillers.Add(o.ToString());
- alreadySet = true;
- break;
- }
- }
- }
- if (!alreadySet) {
- // no information about that Expression found, so put in <unknown>
- holeFillers.Add("<unknown>");
- }
- }
- reason = FormatReasonString(reason, holeFillers);
- }
- if (reason != null) {
- relatedInformation.Add("(related information): " + reason);
- }
- } else {
- // define new templates here!
- }
-
- if (printInternalStateDumpOnce) {
- ComputeAndTreatHeapSuccessions(incarnationMap, errModel, incarnationOriginMap, relatedInformation);
-
- // default action: print all values!
- foreach (KeyValuePair<Bpl.Expr, object> kvp in exprToPrintableValue) {
- Contract.Assert(kvp.Key != null);
- object o = kvp.Value;
- if (o != null) {
- // We do not want to print LiteralExprs because that gives things like 0 == 0.
- // If both arguments to the string.Format are the same it is also useless,
- // as that would print e.g. $a == $a.
- if (!(kvp.Key is LiteralExpr) && kvp.Key.ToString() != o.ToString()) {
- string boogieExpr;
- // check whether we are handling BPL or SSC input
- bool runningOnBpl = CommandLineOptions.Clo.Files.Exists(fn => Path.GetExtension(fn).ToLower() == "bpl");
- if (runningOnBpl) {
- boogieExpr = kvp.Key.ToString();
- } else {
- boogieExpr = Helpers.PrettyPrintBplExpr(kvp.Key);
- }
- relatedInformation.Add("(internal state dump): " + string.Format("{0} == {1}", boogieExpr, o));
- }
- }
- }
- }
- }
-
- static void ComputeAndTreatHeapSuccessions(System.Collections.Hashtable/*!*/ incarnationMap, ErrorModel/*!*/ errModel,
- Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap, List<string/*!*/>/*!*/ relatedInformation) {
- Contract.Requires(incarnationMap != null);
- Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
- Contract.Requires(cce.NonNullElements(relatedInformation));
- List<int> heapSuccList = ComputeHeapSuccessions(incarnationMap, errModel);
- TreatHeapSuccessions(heapSuccList, incarnationMap, errModel, incarnationOriginMap, relatedInformation);
- }
-
- static List<int> ComputeHeapSuccessions(System.Collections.Hashtable incarnationMap, ErrorModel errModel) {
- Contract.Requires(incarnationMap != null);
- Contract.Requires(errModel != null);
- // find the heap variable
- Variable heap = null;
- ICollection ic = incarnationMap.Keys;
- foreach (object o in ic) {
- if (o is GlobalVariable) {
- GlobalVariable gv = (GlobalVariable)o;
- if (gv.Name == "$Heap") {
- heap = gv;
- }
- }
- }
- List<int> heapIdSuccession = new List<int>();
- if (heap == null) {
- // without knowing the name of the current heap we cannot create a heap succession!
- } else {
- object oHeap = incarnationMap[heap];
- if (oHeap != null) {
- string currentHeap = oHeap.ToString();
- int currentHeapId;
- if (errModel.identifierToPartition.TryGetValue(currentHeap, out currentHeapId)) {
- while (currentHeapId != -1) {
- if (!heapIdSuccession.Contains(currentHeapId)) {
- heapIdSuccession.Add(currentHeapId);
- currentHeapId = ComputePredecessorHeapId(currentHeapId, errModel);
- } else {
- // looping behavior, just stop here and do not add this value (again!)
- break;
- }
- }
- }
- }
- }
- if (heapIdSuccession.Count > 0) {
- int heapId = heapIdSuccession[heapIdSuccession.Count - 1];
- List<string> strl = errModel.partitionToIdentifiers[heapId];
- Contract.Assert(strl != null);
- if (strl != null && strl.Contains("$Heap")) {
- // we have a proper succession of heaps that starts with $Heap
- return heapIdSuccession;
- } else {
- // no proper heap succession, not starting with $Heap!
- return null;
- }
- } else {
- // no heap succession found because either the $Heap does not have a current incarnation
- // or because (unlikely!) the model is somehow messed up
- return null;
- }
- }
-
- static int ComputePredecessorHeapId(int id, ErrorModel errModel) {
- Contract.Requires(errModel != null);
- //check "$HeapSucc" and "store2" functions:
- List<int> heapSuccPredIdList = new List<int>();
- List<List<int>> heapSuccFunc;
- errModel.definedFunctions.TryGetValue("$HeapSucc", out heapSuccFunc);
- if (heapSuccFunc != null) {
- foreach (List<int> heapSuccFuncDef in heapSuccFunc) {
- // do not look at the else case of the function def, so check .Count
- if (heapSuccFuncDef != null && heapSuccFuncDef.Count == 3 && heapSuccFuncDef[1] == id) {
- // make sure each predecessor is put into the list at most once
- if (!heapSuccPredIdList.Contains(heapSuccFuncDef[0])) {
- heapSuccPredIdList.Add(heapSuccFuncDef[0]);
- }
- }
- }
- }
- List<int> store2PredIdList = new List<int>();
- ;
- List<List<int>> store2Func;
- errModel.definedFunctions.TryGetValue("store2", out store2Func);
- if (store2Func != null) {
- foreach (List<int> store2FuncDef in store2Func) {
- // do not look at the else case of the function def, so check .Count
- if (store2FuncDef != null && store2FuncDef.Count == 5 && store2FuncDef[4] == id) {
- // make sure each predecessor is put into the list at most once
- if (!store2PredIdList.Contains(store2FuncDef[0])) {
- store2PredIdList.Add(store2FuncDef[0]);
- }
- }
- }
- }
- if (heapSuccPredIdList.Count + store2PredIdList.Count > 0) {
- if (store2PredIdList.Count == 1) {
- return store2PredIdList[0];
- } else if (store2PredIdList.Count == 0) {
- if (heapSuccPredIdList.Count == 1) {
- return heapSuccPredIdList[0];
- } else { //(heapSuccPredIdList.Count > 1)
- if (heapSuccPredIdList.Count == 2) {
- // if one of the 2 is a self-loop, take the other!
- if (heapSuccPredIdList[0] == id) {
- return heapSuccPredIdList[1];
- } else if (heapSuccPredIdList[1] == id) {
- return heapSuccPredIdList[0];
- } else {
- //no self-loop, two different predecessors, cannot choose
- return -1;
- }
- } else {
- // at least 3 different predecessors available, one of them could be a self-loop, but
- // we cannot choose between the other 2 (or more) candidates
- return -1;
- }
- }
- } else {
- // more than one result in the succession coming from store2, no way
- // to decide which is right, end here
- return -1;
- }
- } else {
- // no predecessor found
- return -1;
- }
- }
-
- static void TreatHeapSuccessions(List<int> heapSuccessionList, System.Collections.Hashtable incarnationMap, ErrorModel errModel,
- Dictionary<Incarnation, Absy/*!*/>/*!*/ incarnationOriginMap, List<string/*!*/>/*!*/ relatedInformation) {
- Contract.Requires(incarnationMap != null);
- Contract.Requires(errModel != null);
- Contract.Requires(cce.NonNullDictionaryAndValues(incarnationOriginMap));
- Contract.Requires(cce.NonNullElements(relatedInformation));
- if (heapSuccessionList == null) {
- // empty list of heap successions, nothing we can do!
- return;
- }
- // primarily look for $o and $f (with skolem-id stuff) and then look where they were last changed!
- // find the o and f variables
- Variable dollarO = null;
- Variable dollarF = null;
- ICollection ic = incarnationMap.Keys;
- foreach (object o in ic) {
- if (o is BoundVariable) {
- BoundVariable bv = (BoundVariable)o;
- if (bv.Name == "$o") {
- dollarO = bv;
- } else if (bv.Name == "$f") {
- dollarF = bv;
- }
- }
- }
- if (dollarO == null || dollarF == null) {
- // without knowing the name of the current incarnation of $Heap, $o and $f we don't do anything here
- } else {
- object objO = incarnationMap[dollarO];
- object objF = incarnationMap[dollarF];
- if (objO != null && objF != null) {
- int zidO = errModel.identifierToPartition[objO.ToString()];
- int zidF = errModel.identifierToPartition[objF.ToString()];
-
- List<List<int>> select2Func = null;
- if (errModel.definedFunctions.TryGetValue("select2", out select2Func) && select2Func != null) {
- // check for all changes to $o.$f!
- List<int> heapsChangedOFZid = new List<int>();
- int oldValueZid = -1;
- int newValueZid = -1;
-
- for (int i = 0; i < heapSuccessionList.Count; i++) {
- bool foundValue = false;
- foreach (List<int> f in select2Func) {
- if (f != null && f.Count == 4 && f[0] == heapSuccessionList[i] && f[1] == zidO && f[2] == zidF) {
- newValueZid = f[3];
- foundValue = true;
- break;
- }
- }
- if (!foundValue) {
- // get default of the function once Leo&Nikolaj have changed it so the default is type correct
- // for now treat it as a -1 !
- // the last element of select2Func is the else case, it has only 1 element, so grab that:
- // newValueZid = (select2Func[select2Func.Count-1])[0];
- newValueZid = -1;
- }
-
- if (oldValueZid != newValueZid) {
- // there was a change here, record that in the list:
- if (oldValueZid != -1) {
- // don't record a change at the "initial" location, which refers to the $Heap in
- // its current incarnation, and is marked by the oldValueZid being uninitialized
- heapsChangedOFZid.Add(heapSuccessionList[i - 1]);
- }
- oldValueZid = newValueZid;
- }
- }
-
- foreach (int id in heapsChangedOFZid) {
- //get the heap name out of the errModel for this zid:
- List<string> l = errModel.partitionToIdentifiers[id];
- Contract.Assert(l != null);
- List<string> heaps = new List<string>();
- if (l != null) {
- foreach (string s in l) {
- if (s.StartsWith("$Heap")) {
- heaps.Add(s);
- }
- }
- }
- // easy case first:
- if (heaps.Count == 1) {
- string heapName = heaps[0];
- // we have a string with the name of the heap, but we need to get the
- // source location out of a map that uses Incarnations!
-
- ICollection incOrgMKeys = incarnationOriginMap.Keys;
- foreach (Incarnation inc in incOrgMKeys) {
- if (inc != null) {
- if (inc.Name == heapName) {
- Absy source = null;
- incarnationOriginMap.TryGetValue(inc, out source);
- if (source != null) {
- if (source is Block) {
- Block b = (Block)source;
- string fileName = b.tok.filename;
- if (fileName != null) {
- fileName = fileName.Substring(fileName.LastIndexOf('\\') + 1);
- }
- relatedInformation.Add("(related information): Changed $o.$f here: " + fileName + "(" + b.tok.line + "," + b.tok.col + ")");
- } else if (source is Cmd) {
- Cmd c = (Cmd)source;
- string fileName = c.tok.filename;
- if (fileName != null) {
- fileName = fileName.Substring(fileName.LastIndexOf('\\') + 1);
- }
- relatedInformation.Add("(related information) Changed $o.$f here: " + fileName + "(" + c.tok.line + "," + c.tok.col + ")");
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
- }
- }
- }
- } else {
- // more involved! best use some of the above code and try to synchronize joint parts
- // here there is more than one "$Heap@i" in the partition, check if they all agree on one
- // source location or maybe if some of them are joins (i.e. blocks) that should be ignored
- }
-
- }
- }
- }
- }
- }
-
- static string FormatReasonString(string reason, List<string> holeFillers) {
- if (holeFillers != null) {
- // in case all elements of holeFillers are "<unknown>" we can not say anything useful
- // so just say nothing and return null
- bool allUnknown = true;
- foreach (string s in holeFillers) {
- if (s != "<unknown>") {
- allUnknown = false;
- break;
- }
- }
- if (allUnknown) {
- return null;
- }
- string[] a = holeFillers.ToArray();
- reason = string.Format(reason, a);
- }
- return reason;
- }
-
- static object ValueFromZID(ErrorModel errModel, int id) {
- Contract.Requires(errModel != null);
- return ValueFromZID(errModel, id, null);
- }
-
- static object ValueFromZID(ErrorModel errModel, int id, string searchForAlternate) {
- Contract.Requires(errModel != null);
- object o = errModel.partitionToValue[id];
- if (o != null) {
- return o;
- } else {
- // more elaborate scheme to find something better, as in: look at the identifiers that
- // this partition maps to, or similar things!
-
- //treatment for 'null':
- int idForNull = -1;
- if (errModel.valueToPartition.TryGetValue("nullObject", out idForNull) && idForNull == id) {
- return "nullObject";
- }
-
- string returnStr = null;
-
- // "good identifiers" if there is no value found are 'unique consts' or
- // '$in' parameters; '$in' parameters are treated, unclear how to get 'unique const' info
- List<string> identifiers = errModel.partitionToIdentifiers[id];
- if (identifiers != null) {
- foreach (string s in identifiers) {
- Contract.Assert(s != null);
- //$in parameters are (more) interesting than other identifiers, return the
- // first one found
- if (s.EndsWith("$in")) {
- returnStr = s;
- break;
- }
- }
- }
-
- // try to get mappings from one identifier to another if there are exactly
- // two identifiers in the partition, where one of them is the identifier for which
- // we search for alternate encodings (third parameter of the method) [or an incarnation
- // of such an identifier]
- if (returnStr == null && searchForAlternate != null && identifiers != null && identifiers.Count == 2) {
- if (identifiers[0] == searchForAlternate || identifiers[0].StartsWith(searchForAlternate + ".sk.")) {
- returnStr = identifiers[1];
- } else if (identifiers[1] == searchForAlternate || identifiers[1].StartsWith(searchForAlternate + ".sk.")) {
- returnStr = identifiers[0];
- }
- }
-
- if (returnStr != null) {
- return Helpers.BeautifyBplString(returnStr);
- }
-
- return null;
- }
- }
-
- static int TreatInterpretedFunction(string functionName, List<int> zargs, ErrorModel errModel) {
- Contract.Requires(functionName != null);
- Contract.Requires(zargs != null);
- Contract.Requires(errModel != null);
- if (zargs.Count != 2) {
- //all interpreted functions are binary, so there have to be exactly two arguments
- return -1;
- } else {
- object arg0 = ValueFromZID(errModel, zargs[0]);
- object arg1 = ValueFromZID(errModel, zargs[1]);
- if (arg0 is BigNum && arg1 is BigNum) {
- BigNum arg0i = (BigNum)arg0;
- BigNum arg1i = (BigNum)arg1;
- BigNum result;
- if (functionName == "+") {
- result = arg0i + arg1i;
- } else if (functionName == "-") {
- result = arg0i - arg1i;
- } else /*if (functionName == "*")*/ {
- result = arg0i * arg1i;
- }
- int returnId = -1;
- if (errModel.valueToPartition.TryGetValue(result, out returnId)) {
- return returnId;
- } else {
- return -1;
- }
- } else {
- //both arguments need to be integers for this to work!
- return -1;
- }
- }
- }
-
- static int TreatFunction(string functionName, List<int> zargs, bool undefined, ErrorModel errModel) {
- Contract.Requires(functionName != null);
- Contract.Requires(zargs != null);
- Contract.Requires(errModel != null);
- List<List<int>> functionDef;
- if ((!errModel.definedFunctions.TryGetValue(functionName, out functionDef) && functionName != "+" && functionName != "-" && functionName != "*") || undefined) {
- // no fitting function found or one of the arguments is undefined
- return -1;
- } else {
- if (functionName == "+" || functionName == "-" || functionName == "*") {
- return TreatInterpretedFunction(functionName, zargs, errModel);
- }
- Contract.Assert(functionDef != null);
- foreach (List<int> pWiseF in functionDef) {
- Contract.Assert(pWiseF != null);
- // else case in the function definition:
- if (pWiseF.Count == 1) {
- return pWiseF[0];
- }
- // number of arguments is exactly the right number
- Contract.Assert(zargs.Count == pWiseF.Count - 1);
- if (Contract.ForAll(zargs, i => i == pWiseF[i])) {
- return pWiseF[pWiseF.Count - 1];
- }
- }
- // all functions should have an 'else ->' case defined, therefore this should be
- // unreachable code!
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
-
protected static Counterexample AssertCmdToCounterexample(AssertCmd cmd, TransferCmd transferCmd, BlockSeq trace, Model errModel, ModelViewInfo mvInfo, ProverContext context)
{
Contract.Requires(cmd != null);
@@ -2863,7 +2380,6 @@ namespace VC { List<string> relatedInformation = new List<string>();
-
// See if it is a special assert inserted in translation
if (cmd is AssertRequiresCmd)
{
|