From 6f9c19ac2ae18cb8ea3cc3814109f6bb3004c330 Mon Sep 17 00:00:00 2001 From: qadeer Date: Sat, 28 Apr 2012 19:06:03 -0700 Subject: eliminated class ErrorModel --- Source/VCGeneration/Check.cs | 428 +------------------------------------------ 1 file changed, 1 insertion(+), 427 deletions(-) (limited to 'Source/VCGeneration/Check.cs') 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/*!*/ identifierToPartition; - public List>!*/>> partitionToIdentifiers; - public List/*!*/ partitionToValue; - public Dictionary/*!*/ valueToPartition; - public Dictionary>/*!*/>/*!*/ 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 identifierToPartition, List> partitionToIdentifiers, List partitionToValue, Dictionary valueToPartition, Dictionary>> 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(); - this.partitionToValue = new List(); - this.partitionToIdentifiers = new List>(); - this.valueToPartition = new Dictionary(); - this.definedFunctions = new Dictionary>>(); - - 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(); - 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>(); - this.definedFunctions[f.Name] = tuples; - foreach (var app in f.Apps) { - var tpl = new List(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(); - 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>; - 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(); - var storeFunctions = new Dictionary(); - 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> Redirections(Dictionary>> functions) { - List> 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(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(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 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> array = tempPTVI as List>; - Contract.Assume(array != null); - writer.Write(" -> {"); - foreach (List 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>> kvp in definedFunctions) { - Contract.Assert(kvp.Key != null); - writer.WriteLine(kvp.Key + " -> {"); - List> kvpValue = kvp.Value; - if (kvpValue != null) { - foreach (List 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 kvp in identifierToPartition) { - Contract.Assert(kvp.Key != null); - writer.WriteLine(kvp.Key + " : " + "*" + kvp.Value); - } - - writer.WriteLine("valueToPartition:"); - foreach (KeyValuePair 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> tuples = this.definedFunctions["ControlFlow"]; - Contract.Assert(tuples != null); - foreach (List 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() != 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() != 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 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> 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 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/*!>!*/ PartitionsToValues(List args) { - Contract.Requires(args != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - - List vals = new List(); - 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> array = (List>)o; - List> arrayVal = new List>(); - foreach (List tuple in array) { - Contract.Assert(tuple != null); - - List tupleVal = new List(); - 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 labels, ErrorModel errModel) { + public virtual void OnModel(IList labels, Model model) { Contract.Requires(cce.NonNullElements(labels)); } -- cgit v1.2.3