From 3b15454ac18f93e8f42913af80f665a900fd4378 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 08:32:54 +0100 Subject: Large refactoring of Hashtable to Dictionary. --- Source/Core/Absy.cs | 12 ++++++------ Source/Core/AbsyCmd.cs | 8 ++++---- Source/Core/Duplicator.cs | 6 +++--- Source/Core/Inline.cs | 8 ++++---- Source/Core/LambdaHelper.cs | 2 +- Source/Core/OwickiGries.cs | 12 ++++++------ 6 files changed, 24 insertions(+), 24 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 5e69b179..520c6730 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -385,7 +385,7 @@ namespace Microsoft.Boogie { Dictionary/*!*/ loopHeaderToInputs = new Dictionary(); Dictionary/*!*/ loopHeaderToOutputs = new Dictionary(); - Dictionary/*!*/ loopHeaderToSubstMap = new Dictionary(); + Dictionary/*!*/>/*!*/ loopHeaderToSubstMap = new Dictionary/*!*/>(); Dictionary/*!*/ loopHeaderToLoopProc = new Dictionary(); Dictionary/*!*/ loopHeaderToCallCmd1 = new Dictionary(); Dictionary loopHeaderToCallCmd2 = new Dictionary(); @@ -402,7 +402,7 @@ namespace Microsoft.Boogie { IdentifierExprSeq callOutputs2 = new IdentifierExprSeq(); List lhss = new List(); List rhss = new List(); - Hashtable substMap = new Hashtable(); // Variable -> IdentifierExpr + Dictionary substMap = new Dictionary(); // Variable -> IdentifierExpr VariableSeq/*!*/ targets = new VariableSeq(); HashSet footprint = new HashSet(); @@ -2914,17 +2914,17 @@ namespace Microsoft.Boogie { } } - private Hashtable/*Variable->Expr*//*?*/ formalMap = null; + private Dictionary/*?*/ formalMap = null; public void ResetImplFormalMap() { this.formalMap = null; } - public Hashtable /*Variable->Expr*//*!*/ GetImplFormalMap() { + public Dictionary/*!*/ GetImplFormalMap() { Contract.Ensures(Contract.Result() != null); if (this.formalMap != null) return this.formalMap; else { - Hashtable /*Variable->Expr*//*!*/ map = new Hashtable /*Variable->Expr*/ (InParams.Length + OutParams.Length); + Dictionary/*!*/ map = new Dictionary (InParams.Length + OutParams.Length); Contract.Assume(this.Proc != null); Contract.Assume(InParams.Length == Proc.InParams.Length); @@ -2948,7 +2948,7 @@ namespace Microsoft.Boogie { if (CommandLineOptions.Clo.PrintWithUniqueASTIds) { Console.WriteLine("Implementation.GetImplFormalMap on {0}:", this.Name); using (TokenTextWriter stream = new TokenTextWriter("", Console.Out, false)) { - foreach (DictionaryEntry e in map) { + foreach (var e in map) { Console.Write(" "); cce.NonNull((Variable/*!*/)e.Key).Emit(stream, 0); Console.Write(" --> "); diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index 3005aaa6..cf6fa9ce 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2040,9 +2040,9 @@ namespace Microsoft.Boogie { protected override Cmd ComputeDesugaring() { Contract.Ensures(Contract.Result() != null); CmdSeq newBlockBody = new CmdSeq(); - Hashtable /*Variable -> Expr*/ substMap = new Hashtable/*Variable -> Expr*/(); - Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/(); - Hashtable /*Variable -> Expr*/ substMapBound = new Hashtable/*Variable -> Expr*/(); + Dictionary substMap = new Dictionary(); + Dictionary substMapOld = new Dictionary(); + Dictionary substMapBound = new Dictionary(); VariableSeq/*!*/ tempVars = new VariableSeq(); // proc P(ins) returns (outs) @@ -2335,7 +2335,7 @@ namespace Microsoft.Boogie { public class AssertCmd : PredicateCmd, IPotentialErrorNode { public Expr OrigExpr; - public Hashtable /*Variable -> Expr*/ IncarnationMap; + public Dictionary IncarnationMap; // TODO: convert to use generics private object errorData; diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index fe189f83..d8b45d09 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -353,20 +353,20 @@ namespace Microsoft.Boogie { public delegate Expr/*?*/ Substitution(Variable/*!*/ v); public static class Substituter { - public static Substitution SubstitutionFromHashtable(Hashtable/*Variable!->Expr!*/ map) { + public static Substitution SubstitutionFromHashtable(Dictionary map) { Contract.Requires(map != null); Contract.Ensures(Contract.Result() != null); // TODO: With Whidbey, could use anonymous functions. return new Substitution(new CreateSubstitutionClosure(map).Method); } private sealed class CreateSubstitutionClosure { - Hashtable/*Variable!->Expr!*//*!*/ map; + Dictionary/*!*/ map; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(map != null); } - public CreateSubstitutionClosure(Hashtable/*Variable!->Expr!*/ map) + public CreateSubstitutionClosure(Dictionary map) : base() { Contract.Requires(map != null); this.map = map; diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index 57910775..b7626d99 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -328,7 +328,7 @@ namespace Microsoft.Boogie { Contract.Requires(newModifies != null); Contract.Requires(newLocalVars != null); - Hashtable substMap = new Hashtable(); + Dictionary substMap = new Dictionary(); Procedure proc = impl.Proc; foreach (Variable/*!*/ locVar in cce.NonNull(impl.OriginalLocVars)) { @@ -365,7 +365,7 @@ namespace Microsoft.Boogie { } } - Hashtable /*Variable -> Expr*/ substMapOld = new Hashtable/*Variable -> Expr*/(); + Dictionary substMapOld = new Dictionary(); foreach (IdentifierExpr/*!*/ mie in proc.Modifies) { Contract.Assert(mie != null); @@ -588,12 +588,12 @@ namespace Microsoft.Boogie { public Substitution Subst; public Substitution OldSubst; - public CodeCopier(Hashtable substMap) { + public CodeCopier(Dictionary substMap) { Contract.Requires(substMap != null); Subst = Substituter.SubstitutionFromHashtable(substMap); } - public CodeCopier(Hashtable substMap, Hashtable oldSubstMap) { + public CodeCopier(Dictionary substMap, Dictionary oldSubstMap) { Contract.Requires(oldSubstMap != null); Contract.Requires(substMap != null); Subst = Substituter.SubstitutionFromHashtable(substMap); diff --git a/Source/Core/LambdaHelper.cs b/Source/Core/LambdaHelper.cs index b3b02724..6874f1c9 100644 --- a/Source/Core/LambdaHelper.cs +++ b/Source/Core/LambdaHelper.cs @@ -95,7 +95,7 @@ namespace Microsoft.Boogie { Set freeVars = new Set(); lambda.ComputeFreeVariables(freeVars); // this is ugly, the output will depend on hashing order - Hashtable subst = new Hashtable(); + Dictionary subst = new Dictionary(); VariableSeq formals = new VariableSeq(); ExprSeq callArgs = new ExprSeq(); ExprSeq axCallArgs = new ExprSeq(); diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index e353700f..63f9557f 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -281,7 +281,7 @@ namespace Microsoft.Boogie int count = 0; while (callCmd != null) { - Hashtable map = new Hashtable(); + Dictionary map = new Dictionary(); foreach (Variable x in callCmd.Proc.InParams) { Variable y = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "og_" + count + x.Name, x.TypedIdent.Type), true); @@ -317,7 +317,7 @@ namespace Microsoft.Boogie return proc; } - private void CreateYieldCheckerImpl(DeclWithFormals decl, List yields, Hashtable map) + private void CreateYieldCheckerImpl(DeclWithFormals decl, List yields, Dictionary map) { if (yields.Count == 0) return; @@ -354,8 +354,8 @@ namespace Microsoft.Boogie locals.Add(copy); map[decl.OutParams[i]] = new IdentifierExpr(Token.NoToken, copy); } - Hashtable ogOldLocalMap = new Hashtable(); - Hashtable assumeMap = new Hashtable(map); + Dictionary ogOldLocalMap = new Dictionary(); + Dictionary assumeMap = new Dictionary(map); foreach (IdentifierExpr ie in globalMods) { Variable g = ie.Decl; @@ -422,7 +422,7 @@ namespace Microsoft.Boogie Program program = linearTypechecker.program; ProcedureInfo info = procNameToInfo[impl.Name]; - Hashtable map = new Hashtable(); + Dictionary map = new Dictionary(); foreach (Variable local in impl.LocVars) { var copy = new LocalVariable(Token.NoToken, new TypedIdent(Token.NoToken, local.Name, local.TypedIdent.Type)); @@ -717,7 +717,7 @@ namespace Microsoft.Boogie yields.Add(cmds); cmds = new CmdSeq(); } - CreateYieldCheckerImpl(proc, yields, new Hashtable()); + CreateYieldCheckerImpl(proc, yields, new Dictionary()); } private void AddYieldProcAndImpl() -- cgit v1.2.3 From 0eb1f021dd9f0a24c03f8d9b5124f49840ee6f1d Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 09:49:33 +0100 Subject: Fixed bugs arising from differences between hashtables and dictionaries --- Source/Core/Duplicator.cs | 5 ++++- Source/VCGeneration/ConditionGeneration.cs | 7 ++++--- Source/VCGeneration/VC.cs | 2 +- 3 files changed, 9 insertions(+), 5 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Duplicator.cs b/Source/Core/Duplicator.cs index d8b45d09..1bea5880 100644 --- a/Source/Core/Duplicator.cs +++ b/Source/Core/Duplicator.cs @@ -373,7 +373,10 @@ namespace Microsoft.Boogie { } public Expr/*?*/ Method(Variable v) { Contract.Requires(v != null); - return (Expr)map[v]; + if(map.ContainsKey(v)) { + return map[v]; + } + return null; } } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index edab3bf8..202557ff 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -261,10 +261,11 @@ namespace Microsoft.Boogie { var cs = m.MkState(map.Description); foreach (Variable v in MvInfo.AllVariables) { - var e = (Expr)map.IncarnationMap[v]; + Expr e = map.IncarnationMap.ContainsKey(v) ? map.IncarnationMap[v] : null; if (e == null) continue; - if (prevInc[v] == e) continue; // skip unchanged variables + Expr prevIncV = prevInc.ContainsKey(v) ? prevInc[v] : null; + if (prevIncV == e) continue; // skip unchanged variables Model.Element elt; @@ -1254,7 +1255,7 @@ namespace VC { Dictionary predMap = (Dictionary)cce.NonNull(block2Incarnation[pred]); Expr pred_incarnation_exp; - Expr o = (Expr)predMap[v]; + Expr o = predMap.ContainsKey(v) ? predMap[v] : null; if (o == null) { Variable predIncarnation = v; IdentifierExpr ie2 = new IdentifierExpr(predIncarnation.tok, predIncarnation); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index bf2bf324..09874382 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -1751,7 +1751,7 @@ namespace VC { foreach (Block b in returnExample.Trace) { Contract.Assert(b != null); Contract.Assume(b.TransferCmd != null); - ReturnCmd cmd = (ReturnCmd)gotoCmdOrigins[b.TransferCmd]; + ReturnCmd cmd = gotoCmdOrigins.ContainsKey(b.TransferCmd) ? gotoCmdOrigins[b.TransferCmd] : null; if (cmd != null) { returnExample.FailingReturn = cmd; break; -- cgit v1.2.3 From cd8e597689abb89e64454cc042a2f28619ea44f4 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 10:27:35 +0100 Subject: Refactored RequiresSeq and EnsuresSeq so that they wrap List and List, respectively, as a first step towards simply using the List versions. --- Source/Core/Absy.cs | 33 ++++++--------------------------- 1 file changed, 6 insertions(+), 27 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 520c6730..5f6ecc26 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3224,36 +3224,15 @@ namespace Microsoft.Boogie { } } - public sealed class RequiresSeq : PureCollections.Sequence { - public RequiresSeq(params Requires[]/*!*/ args) - : base(args) { - Contract.Requires(args != null); - } - public new Requires/*!*/ this[int index] { - get { - Contract.Ensures(Contract.Result() != null); - - return cce.NonNull((Requires/*!*/)base[index]); - } - set { - base[index] = value; - } + public sealed class RequiresSeq : List { + public int Length { + get { return Count; } } } - public sealed class EnsuresSeq : PureCollections.Sequence { - public EnsuresSeq(params Ensures[]/*!*/ args) - : base(args) { - Contract.Requires(args != null); - } - public new Ensures/*!*/ this[int index] { - get { - Contract.Ensures(Contract.Result() != null); - return cce.NonNull((Ensures/*!*/)base[index]); - } - set { - base[index] = value; - } + public sealed class EnsuresSeq : List { + public int Length { + get { return Count; } } } -- cgit v1.2.3 From 8547ab2737f6bcb185398e4cbc3edde3847cb085 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 10:35:39 +0100 Subject: Requires/EnsuresSeq replaced by List --- Source/Core/Absy.cs | 22 +++++----------------- Source/Core/AbsyCmd.cs | 4 ++-- Source/Core/BoogiePL.atg | 8 ++++---- Source/Core/Inline.cs | 4 ++-- Source/Core/OwickiGries.cs | 14 +++++++------- Source/Core/Parser.cs | 8 ++++---- Source/Core/StandardVisitor.cs | 12 ++++++------ Source/Houdini/AbstractHoudini.cs | 4 ++-- Source/Houdini/CandidateDependenceAnalyser.cs | 4 ++-- Source/Houdini/Houdini.cs | 4 ++-- Source/Predication/BlockPredicator.cs | 4 ++-- Source/VCExpr/Boogie2VCExpr.cs | 8 ++++---- 12 files changed, 42 insertions(+), 54 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 5f6ecc26..0e9909cb 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -2359,9 +2359,9 @@ namespace Microsoft.Boogie { } public class Procedure : DeclWithFormals { - public RequiresSeq/*!*/ Requires; + public List/*!*/ Requires; public IdentifierExprSeq/*!*/ Modifies; - public EnsuresSeq/*!*/ Ensures; + public List/*!*/ Ensures; [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Requires != null); @@ -2376,7 +2376,7 @@ namespace Microsoft.Boogie { public readonly ProcedureSummary/*!*/ Summary; public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams, - RequiresSeq/*!*/ requires, IdentifierExprSeq/*!*/ modifies, EnsuresSeq/*!*/ ensures) + List/*!*/ requires, IdentifierExprSeq/*!*/ modifies, List/*!*/ ensures) : this(tok, name, typeParams, inParams, outParams, requires, modifies, ensures, null) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -2390,7 +2390,7 @@ namespace Microsoft.Boogie { } public Procedure(IToken/*!*/ tok, string/*!*/ name, TypeVariableSeq/*!*/ typeParams, VariableSeq/*!*/ inParams, VariableSeq/*!*/ outParams, - RequiresSeq/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, EnsuresSeq/*!*/ @ensures, QKeyValue kv + List/*!*/ @requires, IdentifierExprSeq/*!*/ @modifies, List/*!*/ @ensures, QKeyValue kv ) : base(tok, name, typeParams, inParams, outParams) { Contract.Requires(tok != null); @@ -2531,7 +2531,7 @@ namespace Microsoft.Boogie { VariableSeq inputs, VariableSeq outputs, IdentifierExprSeq globalMods) : base(Token.NoToken, impl.Name + "_loop_" + header.ToString(), new TypeVariableSeq(), inputs, outputs, - new RequiresSeq(), globalMods, new EnsuresSeq()) + new List(), globalMods, new List()) { enclosingImpl = impl; } @@ -3224,18 +3224,6 @@ namespace Microsoft.Boogie { } } - public sealed class RequiresSeq : List { - public int Length { - get { return Count; } - } - } - - public sealed class EnsuresSeq : List { - public int Length { - get { return Count; } - } - } - public sealed class VariableSeq : List { public VariableSeq(params Variable[]/*!*/ args) : base(args) { diff --git a/Source/Core/AbsyCmd.cs b/Source/Core/AbsyCmd.cs index cf6fa9ce..47f5505e 100644 --- a/Source/Core/AbsyCmd.cs +++ b/Source/Core/AbsyCmd.cs @@ -2113,7 +2113,7 @@ namespace Microsoft.Boogie { Substitution s = Substituter.SubstitutionFromHashtable(substMapBound); bool hasWildcard = (wildcardVars.Length != 0); Expr preConjunction = null; - for (int i = 0; i < this.Proc.Requires.Length; i++) { + for (int i = 0; i < this.Proc.Requires.Count; i++) { Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]); if (!req.Free && !IsFree) { if (hasWildcard) { @@ -2149,7 +2149,7 @@ namespace Microsoft.Boogie { #region assume Pre[ins := cins] with formal paramters if (hasWildcard) { s = Substituter.SubstitutionFromHashtable(substMap); - for (int i = 0; i < this.Proc.Requires.Length; i++) { + for (int i = 0; i < this.Proc.Requires.Count; i++) { Requires/*!*/ req = cce.NonNull(this.Proc.Requires[i]); if (!req.Free) { Requires/*!*/ reqCopy = (Requires/*!*/)cce.NonNull(req.Clone()); diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 64ddbb50..9cd7d524 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -588,9 +588,9 @@ Procedure = (. Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x; TypeVariableSeq/*!*/ typeParams; VariableSeq/*!*/ ins, outs; - RequiresSeq/*!*/ pre = new RequiresSeq(); + List/*!*/ pre = new List(); IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq(); - EnsuresSeq/*!*/ post = new EnsuresSeq(); + List/*!*/ post = new List(); VariableSeq/*!*/ locals = new VariableSeq(); StmtList/*!*/ stmtList; @@ -642,7 +642,7 @@ ProcSignature +Spec/*!*/ pre, IdentifierExprSeq/*!*/ mods, List/*!*/ post> = (.Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; .) ( "modifies" [ Idents (. foreach(IToken/*!*/ m in ms){ @@ -656,7 +656,7 @@ Spec ) . -SpecPrePost +SpecPrePost/*!*/ pre, List/*!*/ post> = (. Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; .) ( "requires" (. tok = t; .) { Attribute } diff --git a/Source/Core/Inline.cs b/Source/Core/Inline.cs index b7626d99..26d57f68 100644 --- a/Source/Core/Inline.cs +++ b/Source/Core/Inline.cs @@ -453,7 +453,7 @@ namespace Microsoft.Boogie { } // inject requires - for (int i = 0; i < proc.Requires.Length; i++) { + for (int i = 0; i < proc.Requires.Count; i++) { Requires/*!*/ req = cce.NonNull(proc.Requires[i]); inCmds.Add(InlinedRequires(callCmd, req)); } @@ -529,7 +529,7 @@ namespace Microsoft.Boogie { CmdSeq outCmds = new CmdSeq(); // inject ensures - for (int i = 0; i < proc.Ensures.Length; i++) { + for (int i = 0; i < proc.Ensures.Count; i++) { Ensures/*!*/ ens = cce.NonNull(proc.Ensures[i]); outCmds.Add(InlinedEnsures(callCmd, ens)); } diff --git a/Source/Core/OwickiGries.cs b/Source/Core/OwickiGries.cs index 63f9557f..bd6b1da3 100644 --- a/Source/Core/OwickiGries.cs +++ b/Source/Core/OwickiGries.cs @@ -176,7 +176,7 @@ namespace Microsoft.Boogie Formal f = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, string.Format("og_global_old_{0}", ie.Decl.Name), ie.Decl.TypedIdent.Type), true); inputs.Add(f); } - yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq()); + yieldProc = new Procedure(Token.NoToken, "og_yield", new TypeVariableSeq(), inputs, new VariableSeq(), new List(), new IdentifierExprSeq(), new List()); yieldProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); } @@ -275,8 +275,8 @@ namespace Microsoft.Boogie VariableSeq inParams = new VariableSeq(); VariableSeq outParams = new VariableSeq(); - RequiresSeq requiresSeq = new RequiresSeq(); - EnsuresSeq ensuresSeq = new EnsuresSeq(); + List requiresSeq = new List(); + List ensuresSeq = new List(); IdentifierExprSeq ieSeq = new IdentifierExprSeq(); int count = 0; while (callCmd != null) @@ -406,7 +406,7 @@ namespace Microsoft.Boogie // Create the yield checker procedure var yieldCheckerName = string.Format("{0}_YieldChecker_{1}", decl is Procedure ? "Proc" : "Impl", decl.Name); - var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), new EnsuresSeq()); + var yieldCheckerProc = new Procedure(Token.NoToken, yieldCheckerName, decl.TypeParameters, inputs, new VariableSeq(), new List(), new IdentifierExprSeq(), new List()); yieldCheckerProc.AddAttribute("inline", new LiteralExpr(Token.NoToken, Microsoft.Basetypes.BigNum.FromInt(1))); yieldCheckerProcs.Add(yieldCheckerProc); @@ -504,7 +504,7 @@ namespace Microsoft.Boogie { if (!asyncAndParallelCallDesugarings.ContainsKey(callCmd.Proc.Name)) { - asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new EnsuresSeq()); + asyncAndParallelCallDesugarings[callCmd.Proc.Name] = new Procedure(Token.NoToken, string.Format("DummyAsyncTarget_{0}", callCmd.Proc.Name), callCmd.Proc.TypeParameters, callCmd.Proc.InParams, callCmd.Proc.OutParams, callCmd.Proc.Requires, new IdentifierExprSeq(), new List()); } var dummyAsyncTargetProc = asyncAndParallelCallDesugarings[callCmd.Proc.Name]; CallCmd dummyCallCmd = new CallCmd(Token.NoToken, dummyAsyncTargetProc.Name, callCmd.Ins, callCmd.Outs); @@ -639,7 +639,7 @@ namespace Microsoft.Boogie // Collect the yield predicates and desugar yields List yields = new List(); CmdSeq cmds = new CmdSeq(); - if (proc.Requires.Length > 0) + if (proc.Requires.Count > 0) { Dictionary> domainNameToScope = new Dictionary>(); foreach (var domainName in linearTypechecker.linearDomains.Keys) @@ -678,7 +678,7 @@ namespace Microsoft.Boogie yields.Add(cmds); cmds = new CmdSeq(); } - if (info.inParallelCall && proc.Ensures.Length > 0) + if (info.inParallelCall && proc.Ensures.Count > 0) { Dictionary> domainNameToScope = new Dictionary>(); foreach (var domainName in linearTypechecker.linearDomains.Keys) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 95c46934..32e439f0 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -470,9 +470,9 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out proc) != null); IToken/*!*/ x; TypeVariableSeq/*!*/ typeParams; VariableSeq/*!*/ ins, outs; - RequiresSeq/*!*/ pre = new RequiresSeq(); + List/*!*/ pre = new List(); IdentifierExprSeq/*!*/ mods = new IdentifierExprSeq(); - EnsuresSeq/*!*/ post = new EnsuresSeq(); + List/*!*/ post = new List(); VariableSeq/*!*/ locals = new VariableSeq(); StmtList/*!*/ stmtList; @@ -867,7 +867,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { } } - void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) { + void Spec(List/*!*/ pre, IdentifierExprSeq/*!*/ mods, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms; if (la.kind == 34) { Get(); @@ -897,7 +897,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StmtList(out stmtList); } - void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) { + void SpecPrePost(bool free, List/*!*/ pre, List/*!*/ post) { Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null; if (la.kind == 36) { Get(); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index ee873bd4..800a5494 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -248,10 +248,10 @@ namespace Microsoft.Boogie { @requires.Condition = this.VisitExpr(@requires.Condition); return @requires; } - public virtual RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) { + public virtual List VisitRequiresSeq(List requiresSeq) { Contract.Requires(requiresSeq != null); - Contract.Ensures(Contract.Result() != null); - for (int i = 0, n = requiresSeq.Length; i < n; i++) + Contract.Ensures(Contract.Result>() != null); + for (int i = 0, n = requiresSeq.Count; i < n; i++) requiresSeq[i] = this.VisitRequires(requiresSeq[i]); return requiresSeq; } @@ -261,10 +261,10 @@ namespace Microsoft.Boogie { @ensures.Condition = this.VisitExpr(@ensures.Condition); return @ensures; } - public virtual EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) { + public virtual List VisitEnsuresSeq(List ensuresSeq) { Contract.Requires(ensuresSeq != null); - Contract.Ensures(Contract.Result() != null); - for (int i = 0, n = ensuresSeq.Length; i < n; i++) + Contract.Ensures(Contract.Result>() != null); + for (int i = 0, n = ensuresSeq.Count; i < n; i++) ensuresSeq[i] = this.VisitEnsures(ensuresSeq[i]); return ensuresSeq; } diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs index 157571f3..2ff5975e 100644 --- a/Source/Houdini/AbstractHoudini.cs +++ b/Source/Houdini/AbstractHoudini.cs @@ -2238,7 +2238,7 @@ namespace Microsoft.Boogie.Houdini { foreach (var proc in program.TopLevelDeclarations.OfType()) { - var nensures = new EnsuresSeq(); + var nensures = new List(); proc.Ensures.OfType() .Where(ens => !QKeyValue.FindBoolAttribute(ens.Attributes, "ah") && !QKeyValue.FindBoolAttribute(ens.Attributes, "pre") && @@ -3147,7 +3147,7 @@ namespace Microsoft.Boogie.Houdini { PosPrePreds[impl.Name].UnionWith(posPreT); // Pick up per-procedure pre-post - var nens = new EnsuresSeq(); + var nens = new List(); foreach (var ens in impl.Proc.Ensures.OfType()) { string s = null; diff --git a/Source/Houdini/CandidateDependenceAnalyser.cs b/Source/Houdini/CandidateDependenceAnalyser.cs index 9a2eb404..0f725ccf 100644 --- a/Source/Houdini/CandidateDependenceAnalyser.cs +++ b/Source/Houdini/CandidateDependenceAnalyser.cs @@ -437,7 +437,7 @@ namespace Microsoft.Boogie.Houdini { { #region Handle the preconditions - RequiresSeq newRequires = new RequiresSeq(); + List newRequires = new List(); foreach(Requires r in p.Requires) { string c; if (Houdini.MatchCandidate(r.Condition, candidates, out c)) { @@ -457,7 +457,7 @@ namespace Microsoft.Boogie.Houdini { #endregion #region Handle the postconditions - EnsuresSeq newEnsures = new EnsuresSeq(); + List newEnsures = new List(); foreach(Ensures e in p.Ensures) { string c; if (Houdini.MatchCandidate(e.Condition, candidates, out c)) { diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 06d606ff..5078d5a5 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -1165,7 +1165,7 @@ namespace Microsoft.Boogie.Houdini { } foreach (var proc in prog.TopLevelDeclarations.OfType()) { - RequiresSeq newRequires = new RequiresSeq(); + List newRequires = new List(); foreach (Requires r in proc.Requires) { string c; if (MatchCandidate(r.Condition, out c)) { @@ -1185,7 +1185,7 @@ namespace Microsoft.Boogie.Houdini { } proc.Requires = newRequires; - EnsuresSeq newEnsures = new EnsuresSeq(); + List newEnsures = new List(); foreach (Ensures e in proc.Ensures) { string c; if (MatchCandidate(e.Condition, out c)) { diff --git a/Source/Predication/BlockPredicator.cs b/Source/Predication/BlockPredicator.cs index 8419471e..83be688e 100644 --- a/Source/Predication/BlockPredicator.cs +++ b/Source/Predication/BlockPredicator.cs @@ -312,13 +312,13 @@ public class BlockPredicator { if (dwf is Procedure) { var proc = (Procedure)dwf; - var newRequires = new RequiresSeq(); + var newRequires = new List(); foreach (Requires r in proc.Requires) { newRequires.Add(new Requires(r.Free, new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition))); } - var newEnsures = new EnsuresSeq(); + var newEnsures = new List(); foreach (Ensures e in proc.Ensures) { newEnsures.Add(new Ensures(e.Free, diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index cac6d95b..37bcda96 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -704,9 +704,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false); throw new cce.UnreachableException(); } - public override RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) { + public override List VisitRequiresSeq(List requiresSeq) { //Contract.Requires(requiresSeq != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); Contract.Assert(false); throw new cce.UnreachableException(); } @@ -716,9 +716,9 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Assert(false); throw new cce.UnreachableException(); } - public override EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) { + public override List VisitEnsuresSeq(List ensuresSeq) { //Contract.Requires(ensuresSeq != null); - Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result>() != null); Contract.Assert(false); throw new cce.UnreachableException(); } -- cgit v1.2.3 From 5664c5e30f16b74eae4cdcb0b9ba65d5b030c815 Mon Sep 17 00:00:00 2001 From: Ally Donaldson Date: Mon, 22 Jul 2013 10:54:53 +0100 Subject: Refactoring of VariableSeq and TypeSeq --- Source/Core/Absy.cs | 22 ++---------- Source/Core/AbsyExpr.cs | 2 +- Source/Core/AbsyType.cs | 64 +++++++++++++++++------------------ Source/Core/BitvectorAnalysis.cs | 4 +-- Source/Core/LinearSets.cs | 2 +- Source/Core/Parser.cs | 4 +-- Source/Core/StandardVisitor.cs | 6 ++-- Source/VCExpr/TypeErasure.cs | 6 ++-- Source/VCExpr/TypeErasureArguments.cs | 2 +- Source/VCExpr/TypeErasurePremisses.cs | 6 ++-- 10 files changed, 50 insertions(+), 68 deletions(-) (limited to 'Source/Core') diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 0e9909cb..e7c1fb77 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -3233,14 +3233,6 @@ namespace Microsoft.Boogie { : base(varSeq) { Contract.Requires(varSeq != null); } - public new Variable this[int index] { - get { - return (Variable)base[index]; - } - set { - base[index] = value; - } - } public void Emit(TokenTextWriter stream, bool emitAttributes) { Contract.Requires(stream != null); string sep = ""; @@ -3270,7 +3262,7 @@ namespace Microsoft.Boogie { } } - public sealed class TypeSeq : PureCollections.Sequence { + public sealed class TypeSeq : List { public TypeSeq(params Type[]/*!*/ args) : base(args) { Contract.Requires(args != null); @@ -3279,19 +3271,9 @@ namespace Microsoft.Boogie { : base(varSeq) { Contract.Requires(varSeq != null); } - public new Type/*!*/ this[int index] { - get { - Contract.Ensures(Contract.Result() != null); - - return cce.NonNull((Type/*!*/)base[index]); - } - set { - base[index] = value; - } - } public List/*!*/ ToList() { Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ res = new List(Length); + List/*!*/ res = new List(Count); foreach (Type/*!*/ t in this) { Contract.Assert(t != null); res.Add(t); diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 14534929..24622d8b 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1817,7 +1817,7 @@ namespace Microsoft.Boogie { tpInstantiation = SimpleTypeParamInstantiation.EMPTY; return null; } else { - Contract.Assert(actualResultType.Length == 1); + Contract.Assert(actualResultType.Count == 1); tpInstantiation = SimpleTypeParamInstantiation.From(Func.TypeParameters, resultingTypeArgs); return actualResultType[0]; diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 8c355f72..81d44756 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -447,9 +447,9 @@ namespace Microsoft.Boogie { Contract.Requires(actualArgs != null); Contract.Requires(opName != null); Contract.Requires(tc != null); - Contract.Requires(formalArgs.Length == actualArgs.Length); + Contract.Requires(formalArgs.Count == actualArgs.Length); Contract.Requires((formalOuts == null) == (actualOuts == null)); - Contract.Requires(formalOuts == null || formalOuts.Length == cce.NonNull(actualOuts).Length); + Contract.Requires(formalOuts == null || formalOuts.Count == cce.NonNull(actualOuts).Length); Contract.Requires(tc == null || opName != null);//Redundant Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result>())); @@ -462,7 +462,7 @@ namespace Microsoft.Boogie { subst.Add(tv, proxy); } - for (int i = 0; i < formalArgs.Length; i++) { + for (int i = 0; i < formalArgs.Count; i++) { Type formal = formalArgs[i].Substitute(subst); Type actual = cce.NonNull(cce.NonNull(actualArgs[i]).Type); // if the type variables to be matched occur in the actual @@ -479,7 +479,7 @@ namespace Microsoft.Boogie { } if (formalOuts != null) { - for (int i = 0; i < formalOuts.Length; ++i) { + for (int i = 0; i < formalOuts.Count; ++i) { Type formal = formalOuts[i].Substitute(subst); Type actual = cce.NonNull(cce.NonNull(actualOuts)[i].Type); // if the type variables to be matched occur in the actual @@ -524,13 +524,13 @@ namespace Microsoft.Boogie { Contract.Requires(opName != null);Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out actualTypeParams))); actualTypeParams = new List(); - if (formalIns.Length != actualIns.Length) { + if (formalIns.Count != actualIns.Length) { tc.Error(typeCheckingSubject, "wrong number of arguments in {0}: {1}", opName, actualIns.Length); // if there are no type parameters, we can still return the result // type and hope that the type checking proceeds return typeParams.Length == 0 ? formalOuts : null; - } else if (actualOuts != null && formalOuts.Length != actualOuts.Length) { + } else if (actualOuts != null && formalOuts.Count != actualOuts.Length) { tc.Error(typeCheckingSubject, "wrong number of result variables in {0}: {1}", opName, actualOuts.Length); // if there are no type parameters, we can still return the result @@ -638,7 +638,7 @@ namespace Microsoft.Boogie { TypeSeq/*!*/ actualArgs) { Contract.Requires(typeParams != null); Contract.Requires(formalArgs != null); - Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Length == actualArgs.Length); + Contract.Requires(actualArgs != null);Contract.Requires(formalArgs.Count == actualArgs.Count); Contract.Ensures(cce.NonNullDictionaryAndValues(Contract.Result>())); @@ -651,7 +651,7 @@ namespace Microsoft.Boogie { subst.Add(tv, proxy); } - for (int i = 0; i < formalArgs.Length; i++) { + for (int i = 0; i < formalArgs.Count; i++) { Type formal = formalArgs[i].Substitute(subst); Type actual = actualArgs[i]; // if the type variables to be matched occur in the actual @@ -1296,7 +1296,7 @@ Contract.Requires(that != null); } } if (is_bv) { - if (Arguments.Length > 0) { + if (Arguments.Count > 0) { rc.Error(this, "bitvector types must not be applied to arguments: {0}", Name); @@ -1308,7 +1308,7 @@ Contract.Requires(that != null); // second case: the identifier is resolved to a type variable TypeVariable var = rc.LookUpTypeBinder(Name); if (var != null) { - if (Arguments.Length > 0) { + if (Arguments.Count > 0) { rc.Error(this, "type variables must not be applied to arguments: {0}", var); @@ -1320,7 +1320,7 @@ Contract.Requires(that != null); // recursively resolve the arguments TypeCtorDecl ctorDecl = rc.LookUpType(Name); if (ctorDecl != null) { - if (Arguments.Length != ctorDecl.Arity) { + if (Arguments.Count != ctorDecl.Arity) { rc.Error(this, "type constructor received wrong number of arguments: {0}", ctorDecl); @@ -1332,7 +1332,7 @@ Contract.Requires(that != null); // fourth case: the identifier denotes a type synonym TypeSynonymDecl synDecl = rc.LookUpTypeSynonym(Name); if (synDecl != null) { - if (Arguments.Length != synDecl.TypeParameters.Length) { + if (Arguments.Count != synDecl.TypeParameters.Length) { rc.Error(this, "type synonym received wrong number of arguments: {0}", synDecl); @@ -2304,7 +2304,7 @@ Contract.Requires(that != null); Contract.Requires(unifiableVariables != null); Contract.Requires(cce.NonNullDictionaryAndValues(result)); Contract.Requires(that != null); - Contract.Requires(Arguments.Length == that.Arguments.Length); + Contract.Requires(Arguments.Count == that.Arguments.Count); Dictionary/*!*/ subst = new Dictionary(); foreach (TypeVariable/*!*/ tv in that.TypeParameters) { Contract.Assert(tv != null); @@ -2313,7 +2313,7 @@ Contract.Requires(that != null); } bool good = true; - for (int i = 0; i < that.Arguments.Length; i++) { + for (int i = 0; i < that.Arguments.Count; i++) { Type t0 = that.Arguments[i].Substitute(subst); Type t1 = this.Arguments[i]; good &= t0.Unify(t1, unifiableVariables, result); @@ -2332,7 +2332,7 @@ Contract.Requires(that != null); } private void AddConstraint(Constraint c) { - Contract.Requires(c.Arguments.Length == Arity); + Contract.Requires(c.Arguments.Count == Arity); Type f = ProxyFor; MapType mf = f as MapType; @@ -2462,7 +2462,7 @@ Contract.Requires(that != null); return true; } else if (that is MapType) { MapType mapType = (MapType)that; - if (mapType.Arguments.Length == Arity) { + if (mapType.Arguments.Count == Arity) { bool good = true; foreach (Constraint c in constraints) good &= c.Unify(mapType, unifiableVariables, result); @@ -2500,7 +2500,7 @@ Contract.Requires(that != null); // of the substituted variables (otherwise, we are in big trouble) Contract.Assert(Contract.ForAll(constraints, c => Contract.ForAll(subst.Keys, var => - Contract.ForAll(0, c.Arguments.Length, t => !c.Arguments[t].FreeVariables.Has(var)) && + Contract.ForAll(0, c.Arguments.Count, t => !c.Arguments[t].FreeVariables.Has(var)) && !c.Result.FreeVariables.Has(var)))); } return base.Substitute(subst); @@ -2566,7 +2566,7 @@ Contract.Requires(that != null); Contract.Requires(token != null); Contract.Requires(decl != null); Contract.Requires(arguments != null); - Contract.Requires(arguments.Length == decl.TypeParameters.Length); + Contract.Requires(arguments.Count == decl.TypeParameters.Length); this.Decl = decl; this.Arguments = arguments; @@ -2574,7 +2574,7 @@ Contract.Requires(that != null); // the type synonym IDictionary/*!*/ subst = new Dictionary(); - for (int i = 0; i < arguments.Length; ++i) + for (int i = 0; i < arguments.Count; ++i) subst.Add(decl.TypeParameters[i], arguments[i]); ExpandedType = decl.Body.Substitute(subst); @@ -2830,7 +2830,7 @@ Contract.Requires(that != null); Contract.Requires(token != null); Contract.Requires(decl != null); Contract.Requires(arguments != null); - Contract.Requires(arguments.Length == decl.Arity); + Contract.Requires(arguments.Count == decl.Arity); this.Decl = decl; this.Arguments = arguments; } @@ -2878,7 +2878,7 @@ Contract.Requires(that != null); CtorType thatCtorType = thatType as CtorType; if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl)) return false; - if (Arguments.Length == 0) + if (Arguments.Count == 0) return true; return base.Equals(thatType); } @@ -2891,7 +2891,7 @@ Contract.Requires(that != null); CtorType thatCtorType = that as CtorType; if (thatCtorType == null || !this.Decl.Equals(thatCtorType.Decl)) return false; - for (int i = 0; i < Arguments.Length; ++i) { + for (int i = 0; i < Arguments.Count; ++i) { if (!Arguments[i].Equals(thatCtorType.Arguments[i], thisBoundVariables, thatBoundVariables)) return false; @@ -2913,7 +2913,7 @@ Contract.Requires(that != null); return false; } else { bool good = true; - for (int i = 0; i < Arguments.Length; ++i) + for (int i = 0; i < Arguments.Count; ++i) good &= Arguments[i].Unify(thatCtorType.Arguments[i], unifiableVariables, result); return good; } @@ -2982,12 +2982,12 @@ Contract.Requires(that != null); Contract.Requires(stream != null); Contract.Requires(args != null); Contract.Requires(name != null); - int opBindingStrength = args.Length > 0 ? 0 : 2; + int opBindingStrength = args.Count > 0 ? 0 : 2; if (opBindingStrength < contextBindingStrength) stream.Write("("); stream.Write("{0}", TokenTextWriter.SanitizeIdentifier(name)); - int i = args.Length; + int i = args.Count; foreach (Type/*!*/ t in args) { Contract.Assert(t != null); stream.Write(" "); @@ -3151,7 +3151,7 @@ Contract.Requires(that != null); MapType thatMapType = that as MapType; if (thatMapType == null || this.TypeParameters.Length != thatMapType.TypeParameters.Length || - this.Arguments.Length != thatMapType.Arguments.Length) + this.Arguments.Count != thatMapType.Arguments.Count) return false; foreach (TypeVariable/*!*/ var in this.TypeParameters) { @@ -3165,7 +3165,7 @@ Contract.Requires(that != null); try { - for (int i = 0; i < Arguments.Length; ++i) { + for (int i = 0; i < Arguments.Count; ++i) { if (!Arguments[i].Equals(thatMapType.Arguments[i], thisBoundVariables, thatBoundVariables)) return false; @@ -3197,7 +3197,7 @@ Contract.Requires(that != null); MapType thatMapType = that as MapType; if (thatMapType == null || this.TypeParameters.Length != thatMapType.TypeParameters.Length || - this.Arguments.Length != thatMapType.Arguments.Length) + this.Arguments.Count != thatMapType.Arguments.Count) return false; // treat the bound variables of the two map types as equal... @@ -3216,7 +3216,7 @@ Contract.Requires(that != null); } // ... and then unify the domain and range types bool good = true; - for (int i = 0; i < this.Arguments.Length; i++) { + for (int i = 0; i < this.Arguments.Count; i++) { Type t0 = this.Arguments[i].Substitute(subst0); Type t1 = thatMapType.Arguments[i].Substitute(subst1); good &= t0.Unify(t1, unifiableVariables, result); @@ -3357,7 +3357,7 @@ Contract.Assert(var != null); [Pure] public override int GetHashCode(TypeVariableSeq boundVariables) { //Contract.Requires(boundVariables != null); - int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Length; + int res = 7643761 * TypeParameters.Length + 65121 * Arguments.Count; foreach (TypeVariable/*!*/ var in this.TypeParameters) { Contract.Assert(var != null); @@ -3470,7 +3470,7 @@ Contract.Assert(var != null); } public override int MapArity { get { - return Arguments.Length; + return Arguments.Count; } } @@ -3498,7 +3498,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); tpInstantiation = SimpleTypeParamInstantiation.EMPTY; return null; } else { - Contract.Assert(actualResult.Length == 1); + Contract.Assert(actualResult.Count == 1); tpInstantiation = SimpleTypeParamInstantiation.From(TypeParameters, actualTypeParams); return actualResult[0]; } diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs index 30ca85ba..cac5068a 100644 --- a/Source/Core/BitvectorAnalysis.cs +++ b/Source/Core/BitvectorAnalysis.cs @@ -128,7 +128,7 @@ namespace Microsoft.Boogie { TypeSeq newArguments = new TypeSeq(); Type result = NewType(mapType.Result, mapDisjointSet.Result); bool newTypeNeeded = (result != mapType.Result); - for (int i = 0; i < mapType.Arguments.Length; i++) { + for (int i = 0; i < mapType.Arguments.Count; i++) { if (mapDisjointSet.Args(i).Find() == uniqueBv32Set.Find()) { newArguments.Add(new BvType(32)); newTypeNeeded = true; @@ -151,7 +151,7 @@ namespace Microsoft.Boogie { if (mapType == null) { return new DisjointSet(); } - DisjointSet[] args = new DisjointSet[mapType.Arguments.Length]; + DisjointSet[] args = new DisjointSet[mapType.Arguments.Count]; for (int i = 0; i < args.Length; i++) { args[i] = MakeDisjointSet(mapType.Arguments[i]); } diff --git a/Source/Core/LinearSets.cs b/Source/Core/LinearSets.cs index 27312f38..1d541183 100644 --- a/Source/Core/LinearSets.cs +++ b/Source/Core/LinearSets.cs @@ -216,7 +216,7 @@ namespace Microsoft.Boogie MapType mapType = type as MapType; if (mapType != null) { - if (mapType.Arguments.Length == 1 && mapType.Result.Equals(Type.Bool)) + if (mapType.Arguments.Count == 1 && mapType.Result.Equals(Type.Bool)) { type = mapType.Arguments[0]; if (type is MapType) diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 32e439f0..7bd21d02 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -403,7 +403,7 @@ private class BvBounds : Expr { } Bpl.Type ty = curr.Type; var uti = ty as UnresolvedTypeIdentifier; - if (uti != null && uti.Arguments.Length == 0) { + if (uti != null && uti.Arguments.Count == 0) { // the given "thing" was just an identifier, so let's use it as the name of the parameter curr.Name = uti.Name; curr.Type = prevType; @@ -798,7 +798,7 @@ private class BvBounds : Expr { if (la.kind == 11) { Get(); var uti = ty as UnresolvedTypeIdentifier; - if (uti != null && uti.Arguments.Length == 0) { + if (uti != null && uti.Arguments.Count == 0) { varName = uti.Name; } else { this.SemErr("expected identifier before ':'"); diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 800a5494..927b73fe 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -194,7 +194,7 @@ namespace Microsoft.Boogie { public virtual CtorType VisitCtorType(CtorType node) { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); - for (int i = 0; i < node.Arguments.Length; ++i) + for (int i = 0; i < node.Arguments.Count; ++i) node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i])); return node; } @@ -362,7 +362,7 @@ namespace Microsoft.Boogie { // // NOTE: when overriding this method, you have to make sure that // the bound variables of the map type are updated correctly - for (int i = 0; i < node.Arguments.Length; ++i) + for (int i = 0; i < node.Arguments.Count; ++i) node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i])); node.Result = cce.NonNull((Type/*!*/)this.Visit(node.Result)); return node; @@ -512,7 +512,7 @@ namespace Microsoft.Boogie { Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); node.ExpandedType = cce.NonNull((Type/*!*/)this.Visit(node.ExpandedType)); - for (int i = 0; i < node.Arguments.Length; ++i) + for (int i = 0; i < node.Arguments.Count; ++i) node.Arguments[i] = cce.NonNull((Type/*!*/)this.Visit(node.Arguments[i])); return node; } diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 9d366c9f..c4a54300 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -469,7 +469,7 @@ namespace Microsoft.Boogie.TypeErasure { // CtorType ctype = type.AsCtor; Function/*!*/ repr = GetTypeCtorRepr(ctype.Decl); - List/*!*/ args = new List(ctype.Arguments.Length); + List/*!*/ args = new List(ctype.Arguments.Count); foreach (Type/*!*/ t in ctype.Arguments) { Contract.Assert(t != null); args.Add(Type2Term(t, varMapping)); @@ -970,7 +970,7 @@ namespace Microsoft.Boogie.TypeErasure { MapType/*!*/ abstraction = ThinOutMapType(rawType, instantiations); MapTypeClassRepresentation repr = GetClassRepresentation(abstraction); - Contract.Assume(repr.RepresentingType.Arity == instantiations.Length); + Contract.Assume(repr.RepresentingType.Arity == instantiations.Count); return new CtorType(Token.NoToken, repr.RepresentingType, instantiations); } @@ -1004,7 +1004,7 @@ namespace Microsoft.Boogie.TypeErasure { // Bingo! // if the type does not contain any bound variables, we can simply // replace it with a type variable - TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Length); + TypeVariable/*!*/ abstractionVar = AbstractionVariable(instantiations.Count); Contract.Assume(!boundTypeParams.Has(abstractionVar)); instantiations.Add(rawType); return abstractionVar; diff --git a/Source/VCExpr/TypeErasureArguments.cs b/Source/VCExpr/TypeErasureArguments.cs index 57218a73..49c7fe8e 100644 --- a/Source/VCExpr/TypeErasureArguments.cs +++ b/Source/VCExpr/TypeErasureArguments.cs @@ -180,7 +180,7 @@ Contract.Ensures(Contract.ValueAtReturn(out store) != null); int typeParamNum = abstractedType.FreeVariables.Length + abstractedType.TypeParameters.Length; - int arity = typeParamNum + abstractedType.Arguments.Length; + int arity = typeParamNum + abstractedType.Arguments.Count; Type/*!*/[]/*!*/ selectTypes = new Type/*!*/ [arity + 2]; Type/*!*/[]/*!*/ storeTypes = new Type/*!*/ [arity + 3]; diff --git a/Source/VCExpr/TypeErasurePremisses.cs b/Source/VCExpr/TypeErasurePremisses.cs index df14eb01..44eb7dbb 100644 --- a/Source/VCExpr/TypeErasurePremisses.cs +++ b/Source/VCExpr/TypeErasurePremisses.cs @@ -307,11 +307,11 @@ namespace Microsoft.Boogie.TypeErasure // nothing } else if (completeType.IsCtor) { CtorType/*!*/ ctorType = completeType.AsCtor; - if (ctorType.Arguments.Length > 0) { + if (ctorType.Arguments.Count > 0) { // otherwise there are no chances of extracting any // instantiations from this type TypeCtorRepr repr = GetTypeCtorReprStruct(ctorType.Decl); - for (int i = 0; i < ctorType.Arguments.Length; ++i) { + for (int i = 0; i < ctorType.Arguments.Count; ++i) { VCExpr/*!*/ newInnerTerm = Gen.Function(repr.Dtors[i], innerTerm); Contract.Assert(newInnerTerm != null); TypeVarExtractors(var, ctorType.Arguments[i], newInnerTerm, extractors); @@ -644,7 +644,7 @@ namespace Microsoft.Boogie.TypeErasure typeParams.AddRange(abstractedType.TypeParameters.ToList()); typeParams.AddRange(abstractedType.FreeVariables.ToList()); - originalIndexTypes = new List(abstractedType.Arguments.Length + 1); + originalIndexTypes = new List(abstractedType.Arguments.Count + 1); TypeSeq/*!*/ mapTypeParams = new TypeSeq(); foreach (TypeVariable/*!*/ var in abstractedType.FreeVariables) { Contract.Assert(var != null); -- cgit v1.2.3